[STATEMENT]
lemma permutes_bij': assumes ab: "\<And> a. a \<in> A \<Longrightarrow> a_to_b a \<in> B"
    and ba: "\<And> b. b \<in> B \<Longrightarrow> b_to_a b \<in> A"
    and ab_ba: "\<And> a. a \<in> A \<Longrightarrow> b_to_a (a_to_b a) = a"
    and ba_ab: "\<And> b. b \<in> B \<Longrightarrow> a_to_b (b_to_a b) = b"
  shows "{p . p permutes A} = (\<lambda> p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}"
  (is "?A = ?f ` ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
note one_dir = ab ba ab_ba ba_ab
[PROOF STATE]
proof (state)
this:
?a \<in> A \<Longrightarrow> a_to_b ?a \<in> B
?b \<in> B \<Longrightarrow> b_to_a ?b \<in> A
?a \<in> A \<Longrightarrow> b_to_a (a_to_b ?a) = ?a
?b \<in> B \<Longrightarrow> a_to_b (b_to_a ?b) = ?b

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
note other_dir = ba ab ba_ab ab_ba
[PROOF STATE]
proof (state)
this:
?b \<in> B \<Longrightarrow> b_to_a ?b \<in> A
?a \<in> A \<Longrightarrow> a_to_b ?a \<in> B
?b \<in> B \<Longrightarrow> a_to_b (b_to_a ?b) = ?b
?a \<in> A \<Longrightarrow> b_to_a (a_to_b ?a) = ?a

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
let ?g = "(\<lambda> p b. if b \<in> B then a_to_b (p (b_to_a b)) else b)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
define PA where "PA = ?A"
[PROOF STATE]
proof (state)
this:
PA = {p. p permutes A}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
define f where "f = ?f"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a)

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
define g where "g = ?g"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b)

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g = (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b)

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
assume "p \<in> PA"
[PROOF STATE]
proof (state)
this:
p \<in> PA

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
hence p: "p permutes A"
[PROOF STATE]
proof (prove)
using this:
p \<in> PA

goal (1 subgoal):
 1. p permutes A
[PROOF STEP]
unfolding PA_def
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. p permutes A}

goal (1 subgoal):
 1. p permutes A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p permutes A

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
from p[unfolded permutes_def]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. x \<notin> A \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)
[PROOF STEP]
have pnA: "\<And> a. a \<notin> A \<Longrightarrow> p a = a"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. x \<notin> A \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)

goal (1 subgoal):
 1. \<And>a. a \<notin> A \<Longrightarrow> p a = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?a \<notin> A \<Longrightarrow> p ?a = ?a

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
have "?f (?g p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p
[PROOF STEP]
proof (rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
show "?f (?g p) a = p a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
proof (cases "a \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
 2. a \<notin> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> A

goal (2 subgoals):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
 2. a \<notin> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<notin> A

goal (1 subgoal):
 1. (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
by (simp add: pnA)
[PROOF STATE]
proof (state)
this:
(if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a

goal (1 subgoal):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
note a = this
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
hence "p a \<in> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A

goal (1 subgoal):
 1. p a \<in> A
[PROOF STEP]
unfolding permutes_in_image[OF p]
[PROOF STATE]
proof (prove)
using this:
a \<in> A

goal (1 subgoal):
 1. a \<in> A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
p a \<in> A

goal (1 subgoal):
 1. a \<in> A \<Longrightarrow> (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p a \<in> A

goal (1 subgoal):
 1. (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
p a \<in> A
a \<in> A

goal (1 subgoal):
 1. (if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a
[PROOF STEP]
by (simp add: ab_ba ba_ab ab)
[PROOF STATE]
proof (state)
this:
(if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>a. if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
hence "f (g p) = p"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>a. if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p

goal (1 subgoal):
 1. f (g p) = p
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>a. if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p

goal (1 subgoal):
 1. (\<lambda>a. if a \<in> A then b_to_a (if a_to_b a \<in> B then a_to_b (p (b_to_a (a_to_b a))) else a_to_b a) else a) = p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f (g p) = p

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?p2 \<in> PA \<Longrightarrow> f (g ?p2) = ?p2

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
hence "f ` g ` PA = PA"
[PROOF STATE]
proof (prove)
using this:
?p2 \<in> PA \<Longrightarrow> f (g ?p2) = ?p2

goal (1 subgoal):
 1. f ` g ` PA = PA
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f ` g ` PA = PA

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
hence id: "?f ` ?g ` ?A = ?A"
[PROOF STATE]
proof (prove)
using this:
f ` g ` PA = PA

goal (1 subgoal):
 1. (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} = {p. p permutes A}
[PROOF STEP]
unfolding PA_def f_def g_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} = {p. p permutes A}

goal (1 subgoal):
 1. (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} = {p. p permutes A}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} = {p. p permutes A}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
have "?f ` ?B \<subseteq> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<subseteq> {p. p permutes A}
[PROOF STEP]
by (rule permutes_bij_main[OF one_dir])
[PROOF STATE]
proof (state)
this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<subseteq> {p. p permutes A}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<subseteq> {p. p permutes A}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
have "?g ` ?A \<subseteq> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} \<subseteq> {p. p permutes B}
[PROOF STEP]
by (rule permutes_bij_main[OF ba ab ba_ab ab_ba])
[PROOF STATE]
proof (state)
this:
(\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} \<subseteq> {p. p permutes B}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
hence "?f ` ?g ` ?A \<subseteq> ?f ` ?B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} \<subseteq> {p. p permutes B}

goal (1 subgoal):
 1. (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
hence "?A \<subseteq> ?f ` ?B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` (\<lambda>p b. if b \<in> B then a_to_b (p (b_to_a b)) else b) ` {p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. {p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
{p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. {p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
{p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<subseteq> {p. p permutes A}
{p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<subseteq> {p. p permutes A}
{p. p permutes A} \<subseteq> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. {p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{p. p permutes A} = (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permutes_others:
  assumes p: "p permutes S" and x: "x \<notin> S" shows "p x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p x = x
[PROOF STEP]
using p x
[PROOF STATE]
proof (prove)
using this:
p permutes S
x \<notin> S

goal (1 subgoal):
 1. p x = x
[PROOF STEP]
by (rule permutes_not_in)


[STATEMENT]
lemma inj_on_nat_permutes: assumes i: "inj_on f (S :: nat set)"
  and fS: "f \<in> S \<rightarrow> S"
  and fin: "finite S"
  and f: "\<And> i. i \<notin> S \<Longrightarrow> f i = i"
  shows "f permutes S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f permutes S
[PROOF STEP]
unfolding permutes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. x \<notin> S \<longrightarrow> f x = x) \<and> (\<forall>y. \<exists>!x. f x = y)
[PROOF STEP]
proof (intro conjI allI impI, rule f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<notin> S \<Longrightarrow> x \<notin> S
 2. \<And>y. \<exists>!x. f x = y
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<notin> S \<Longrightarrow> x \<notin> S
 2. \<And>y. \<exists>!x. f x = y
[PROOF STEP]
from endo_inj_surj[OF fin _ i] fS
[PROOF STATE]
proof (chain)
picking this:
f ` S \<subseteq> S \<Longrightarrow> f ` S = S
f \<in> S \<rightarrow> S
[PROOF STEP]
have fs: "f ` S = S"
[PROOF STATE]
proof (prove)
using this:
f ` S \<subseteq> S \<Longrightarrow> f ` S = S
f \<in> S \<rightarrow> S

goal (1 subgoal):
 1. f ` S = S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` S = S

goal (2 subgoals):
 1. \<And>x. x \<notin> S \<Longrightarrow> x \<notin> S
 2. \<And>y. \<exists>!x. f x = y
[PROOF STEP]
show "\<exists>!x. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. f x = y
[PROOF STEP]
proof (cases "y \<in> S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> S \<Longrightarrow> \<exists>!x. f x = y
 2. y \<notin> S \<Longrightarrow> \<exists>!x. f x = y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin> S

goal (2 subgoals):
 1. y \<in> S \<Longrightarrow> \<exists>!x. f x = y
 2. y \<notin> S \<Longrightarrow> \<exists>!x. f x = y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<notin> S

goal (1 subgoal):
 1. \<exists>!x. f x = y
[PROOF STEP]
by (intro ex1I[of _ y], insert fS f, auto)
[PROOF STATE]
proof (state)
this:
\<exists>!x. f x = y

goal (1 subgoal):
 1. y \<in> S \<Longrightarrow> \<exists>!x. f x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<in> S \<Longrightarrow> \<exists>!x. f x = y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in> S

goal (1 subgoal):
 1. y \<in> S \<Longrightarrow> \<exists>!x. f x = y
[PROOF STEP]
with fs
[PROOF STATE]
proof (chain)
picking this:
f ` S = S
y \<in> S
[PROOF STEP]
obtain x where x: "x \<in> S" and fx: "f x = y"
[PROOF STATE]
proof (prove)
using this:
f ` S = S
y \<in> S

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; f x = y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<in> S
f x = y

goal (1 subgoal):
 1. y \<in> S \<Longrightarrow> \<exists>!x. f x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. f x = y
[PROOF STEP]
proof (rule ex1I, rule fx)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. f xa = y \<Longrightarrow> xa = x
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. f xa = y \<Longrightarrow> xa = x
[PROOF STEP]
assume fx': "f x' = y"
[PROOF STATE]
proof (state)
this:
f x' = y

goal (1 subgoal):
 1. \<And>xa. f xa = y \<Longrightarrow> xa = x
[PROOF STEP]
with True f[of x']
[PROOF STATE]
proof (chain)
picking this:
y \<in> S
x' \<notin> S \<Longrightarrow> f x' = x'
f x' = y
[PROOF STEP]
have "x' \<in> S"
[PROOF STATE]
proof (prove)
using this:
y \<in> S
x' \<notin> S \<Longrightarrow> f x' = x'
f x' = y

goal (1 subgoal):
 1. x' \<in> S
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x' \<in> S

goal (1 subgoal):
 1. \<And>xa. f xa = y \<Longrightarrow> xa = x
[PROOF STEP]
from inj_onD[OF i fx[folded fx'] x this]
[PROOF STATE]
proof (chain)
picking this:
x = x'
[PROOF STEP]
show "x' = x"
[PROOF STATE]
proof (prove)
using this:
x = x'

goal (1 subgoal):
 1. x' = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' = x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!x. f x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!x. f x = y

goal (1 subgoal):
 1. \<And>x. x \<notin> S \<Longrightarrow> x \<notin> S
[PROOF STEP]
qed


[STATEMENT]
lemma signof_id:
  "signof id = 1"
  "signof (\<lambda>x. x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sign id) = (1::'a) &&& of_int (sign (\<lambda>x. x)) = (1::'b)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma signof_inv: "finite S \<Longrightarrow> p permutes S \<Longrightarrow> signof (inv p) = signof p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; p permutes S\<rbrakk> \<Longrightarrow> of_int (sign (inv p)) = of_int (sign p)
[PROOF STEP]
by (simp add: permutes_imp_permutation sign_inverse)


[STATEMENT]
lemma signof_pm_one: "signof p \<in> {1, - 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sign p) \<in> {1::'a, - (1::'a)}
[PROOF STEP]
by (simp add: sign_def)


[STATEMENT]
lemma signof_compose:
  assumes "p permutes {0..<(n :: nat)}"
  and "q permutes {0 ..<(m :: nat)}"
  shows "signof (p o q) = signof p * signof q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (sign (p \<circ> q)) = of_int (sign p) * of_int (sign q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int (sign (p \<circ> q)) = of_int (sign p) * of_int (sign q)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
p permutes {0..<n}
q permutes {0..<m}
[PROOF STEP]
have pp: "permutation p" "permutation q"
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}
q permutes {0..<m}

goal (1 subgoal):
 1. permutation p &&& permutation q
[PROOF STEP]
by (auto simp: permutation_permutes)
[PROOF STATE]
proof (state)
this:
permutation p
permutation q

goal (1 subgoal):
 1. of_int (sign (p \<circ> q)) = of_int (sign p) * of_int (sign q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
permutation p
permutation q
[PROOF STEP]
show "signof (p o q) = signof p * signof q"
[PROOF STATE]
proof (prove)
using this:
permutation p
permutation q

goal (1 subgoal):
 1. of_int (sign (p \<circ> q)) = of_int (sign p) * of_int (sign q)
[PROOF STEP]
by (simp add: sign_compose)
[PROOF STATE]
proof (state)
this:
of_int (sign (p \<circ> q)) = of_int (sign p) * of_int (sign q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dual_rel1: "\<forall>A. (\<C>\<^sub>R R) A \<^bold>\<approx> (\<I>\<^sub>R R)\<^sup>d A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. \<C>\<^sub>R R A w = \<I>\<^sub>R R\<^sup>d A w
[PROOF STEP]
unfolding Cl_rel_def Int_rel_def dual_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. nonEmpty (\<lambda>v. R w v \<and> A v) = (\<not> contains (\<lambda>v. \<not> A v) (R w))
[PROOF STEP]
by simp


[STATEMENT]
lemma dual_rel2: "\<forall>A. (\<I>\<^sub>R R) A \<^bold>\<approx> (\<C>\<^sub>R R)\<^sup>d A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. \<I>\<^sub>R R A w = \<C>\<^sub>R R\<^sup>d A w
[PROOF STEP]
unfolding Cl_rel_def Int_rel_def dual_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A w. contains A (R w) = (\<not> nonEmpty (\<lambda>v. R w v \<and> \<not> A v))
[PROOF STEP]
by simp


[STATEMENT]
lemma rC1: "ADDI (\<C>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ADDI (\<C>\<^sub>R R)
[PROOF STEP]
unfolding Cl_rel_def ADDI_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A B w. nonEmpty (\<lambda>v. R w v \<and> (A v \<or> B v)) = (nonEmpty (\<lambda>v. R w v \<and> A v) \<or> nonEmpty (\<lambda>v. R w v \<and> B v))
[PROOF STEP]
by blast


[STATEMENT]
lemma rC1i:"iADDI (\<C>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI (\<C>\<^sub>R R)
[PROOF STEP]
by (smt Cl_rel_def Ra_restr_ex iADDI_def supremum_def)


[STATEMENT]
lemma rC2: "reflexive R \<longrightarrow> EXP (\<C>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive R \<longrightarrow> EXP (\<C>\<^sub>R R)
[PROOF STEP]
unfolding EXP_def Cl_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive R \<longrightarrow> (\<forall>A. contains (\<lambda>w. nonEmpty (\<lambda>v. R w v \<and> A v)) A)
[PROOF STEP]
by auto


[STATEMENT]
lemma rC3: "NOR (\<C>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NOR (\<C>\<^sub>R R)
[PROOF STEP]
unfolding Cl_rel_def NOR_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. nonEmpty (\<lambda>v. R w v \<and> False) = False
[PROOF STEP]
by blast


[STATEMENT]
lemma rC4: "reflexive R \<and> transitive R \<longrightarrow> IDEM (\<C>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive R \<and> transitive R \<longrightarrow> IDEM (\<C>\<^sub>R R)
[PROOF STEP]
unfolding Cl_rel_def IDEM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive R \<and> transitive R \<longrightarrow> (\<forall>A w. nonEmpty (\<lambda>v. R w v \<and> A v) = nonEmpty (\<lambda>v. R w v \<and> nonEmpty (\<lambda>va. R v va \<and> A va)))
[PROOF STEP]
by smt


[STATEMENT]
lemma rC_Barcan: "\<forall>\<pi>. (\<C>\<^sub>R R)(\<^bold>\<exists>x. \<pi> x) \<^bold>\<preceq> (\<^bold>\<exists>x. (\<C>\<^sub>R R)(\<pi> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. contains (\<lambda>w. nonEmpty (\<lambda>X. \<C>\<^sub>R R (\<pi> X) w)) (\<C>\<^sub>R R (mexistsB \<pi>))
[PROOF STEP]
unfolding Cl_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. contains (\<lambda>w. nonEmpty (\<lambda>X. nonEmpty (\<lambda>v. R w v \<and> \<pi> X v))) (\<lambda>w. nonEmpty (\<lambda>v. R w v \<and> mexistsB \<pi> v))
[PROOF STEP]
by auto


[STATEMENT]
lemma rI1: "MULT (\<I>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MULT (\<I>\<^sub>R R)
[PROOF STEP]
unfolding Int_rel_def MULT_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A B w. contains (\<lambda>v. A v \<and> B v) (R w) = (contains A (R w) \<and> contains B (R w))
[PROOF STEP]
by blast


[STATEMENT]
lemma rI1i:"iMULT (\<I>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMULT (\<I>\<^sub>R R)
[PROOF STEP]
by (smt Int_rel_def Ra_restr_all iMULT_def infimum_def)


[STATEMENT]
lemma rI2: "reflexive R \<Longrightarrow> dEXP (\<I>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive R \<Longrightarrow> dEXP (\<I>\<^sub>R R)
[PROOF STEP]
unfolding Int_rel_def dEXP_def Int_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive R \<Longrightarrow> \<forall>A. contains A (\<lambda>w. contains A (R w))
[PROOF STEP]
by auto


[STATEMENT]
lemma rI3: "dNOR (\<I>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dNOR (\<I>\<^sub>R R)
[PROOF STEP]
unfolding Int_rel_def dNOR_def conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. contains (\<lambda>v. True) (R w) = True
[PROOF STEP]
by simp


[STATEMENT]
lemma rI4: "reflexive R \<Longrightarrow> transitive R \<Longrightarrow> IDEM (\<I>\<^sub>R R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive R; transitive R\<rbrakk> \<Longrightarrow> IDEM (\<I>\<^sub>R R)
[PROOF STEP]
unfolding IDEM_def Int_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive R; transitive R\<rbrakk> \<Longrightarrow> \<forall>A w. contains A (R w) = contains (\<lambda>v. contains A (R v)) (R w)
[PROOF STEP]
by smt


[STATEMENT]
lemma rI_Barcan: "\<forall>\<pi>. (\<^bold>\<forall>x. (\<I>\<^sub>R R)(\<pi> x)) \<^bold>\<preceq> (\<I>\<^sub>R R)(\<^bold>\<forall>x. \<pi> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. contains (\<I>\<^sub>R R (mforallB \<pi>)) (\<lambda>w. \<forall>X. \<I>\<^sub>R R (\<pi> X) w)
[PROOF STEP]
unfolding Int_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. contains (\<lambda>w. contains (mforallB \<pi>) (R w)) (\<lambda>w. \<forall>X. contains (\<pi> X) (R w))
[PROOF STEP]
by simp


[STATEMENT]
lemma sp_rel_reflex: "EXP \<C> \<Longrightarrow> reflexive (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EXP \<C> \<Longrightarrow> reflexive (\<R>\<^sup>C \<C>)
[PROOF STEP]
by (simp add: EXP_def sp_rel_def)


[STATEMENT]
lemma sp_rel_trans: "MONO \<C> \<Longrightarrow> IDEM \<C> \<Longrightarrow> transitive (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>MONO \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> transitive (\<R>\<^sup>C \<C>)
[PROOF STEP]
by (smt IDEM_def MONO_def sp_rel_def)


[STATEMENT]
lemma "iADDI \<C> \<Longrightarrow> EXP \<C> \<Longrightarrow> NOR \<C> \<Longrightarrow> IDEM \<C> \<Longrightarrow> antisymmetric (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iADDI \<C>; EXP \<C>; NOR \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> antisymmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iADDI \<C>; EXP \<C>; NOR \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> antisymmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
oops


[STATEMENT]
lemma "iADDI \<C> \<Longrightarrow> EXP \<C> \<Longrightarrow> NOR \<C> \<Longrightarrow> IDEM \<C> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iADDI \<C>; EXP \<C>; NOR \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>iADDI \<C>; EXP \<C>; NOR \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
oops


[STATEMENT]
lemma sp_rel_a:   "MONO \<C>  \<Longrightarrow> \<forall>A. (\<C>\<^sub>R (\<R>\<^sup>C \<C>)) A \<^bold>\<preceq> \<C> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MONO \<C> \<Longrightarrow> \<forall>A. contains (\<C> A) (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A)
[PROOF STEP]
by (smt Cl_rel_def MONO_def sp_rel_def)


[STATEMENT]
lemma sp_rel_b: "iADDI_a \<C> \<Longrightarrow> \<forall>A. (\<C>\<^sub>R (\<R>\<^sup>C \<C>)) A \<^bold>\<succeq> \<C> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
assume iaddia: "iADDI_a \<C>"
[PROOF STATE]
proof (state)
this:
iADDI_a \<C>

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
iADDI_a \<C>

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
let ?S="\<lambda>B::\<sigma>. \<exists>w::w. A w \<and> B=(\<lambda>u. u=w)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
have "A \<^bold>\<approx> (\<^bold>\<Or>?S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. A w = \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w
[PROOF STEP]
using supremum_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<Or>?S \<equiv> \<lambda>w. nonEmpty (\<lambda>X. ?S X \<and> X w)

goal (1 subgoal):
 1. \<forall>w. A w = \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w. A w = \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
hence "\<C>(A) \<^bold>\<approx> \<C>(\<^bold>\<Or>?S)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. A w = \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w

goal (1 subgoal):
 1. \<forall>w. \<C> A w = \<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w
[PROOF STEP]
by (smt eq_ext)
[PROOF STATE]
proof (state)
this:
\<forall>w. \<C> A w = \<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w. \<C> A w = \<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
have "\<^bold>\<Or>Ra[\<C>|?S] \<^bold>\<approx> (\<C>\<^sub>R (\<R>\<^sup>C \<C>)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] w = \<C>\<^sub>R (\<R>\<^sup>C \<C>) A w
[PROOF STEP]
by (smt Cl_rel_def Ra_restr_ex sp_rel_def)
[PROOF STATE]
proof (state)
this:
\<forall>w. \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] w = \<C>\<^sub>R (\<R>\<^sup>C \<C>) A w

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w. \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] w = \<C>\<^sub>R (\<R>\<^sup>C \<C>) A w

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
from iaddia
[PROOF STATE]
proof (chain)
picking this:
iADDI_a \<C>
[PROOF STEP]
have "\<C>(\<^bold>\<Or>?S) \<^bold>\<preceq> \<^bold>\<Or>Ra[\<C>|?S]"
[PROOF STATE]
proof (prove)
using this:
iADDI_a \<C>

goal (1 subgoal):
 1. contains \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] (\<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)))
[PROOF STEP]
unfolding iADDI_a_def
[PROOF STATE]
proof (prove)
using this:
\<forall>S. contains \<^bold>\<Or>Ra[\<C>|S] (\<C> \<^bold>\<Or>S)

goal (1 subgoal):
 1. contains \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] (\<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] (\<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)))

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. \<C> A w = \<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w
\<forall>w. \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] w = \<C>\<^sub>R (\<R>\<^sup>C \<C>) A w
contains \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] (\<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)))
[PROOF STEP]
have "\<C> A \<^bold>\<preceq> (\<C>\<^sub>R (\<R>\<^sup>C \<C>)) A"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. \<C> A w = \<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)) w
\<forall>w. \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] w = \<C>\<^sub>R (\<R>\<^sup>C \<C>) A w
contains \<^bold>\<Or>Ra[\<C>|\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w))] (\<C> \<^bold>\<Or>\<lambda>B. nonEmpty (\<lambda>w. A w \<and> B = (\<lambda>u. u = w)))

goal (1 subgoal):
 1. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) ?A2) (\<C> ?A2)

goal (1 subgoal):
 1. iADDI_a \<C> \<Longrightarrow> \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) ?A2) (\<C> ?A2)

goal (1 subgoal):
 1. \<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>A. contains (\<C>\<^sub>R (\<R>\<^sup>C \<C>) A) (\<C> A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sp_rel: "iADDI \<C> \<Longrightarrow> \<forall>A. \<C> A \<^bold>\<approx> (\<C>\<^sub>R (\<R>\<^sup>C \<C>)) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI \<C> \<Longrightarrow> \<forall>A w. \<C> A w = \<C>\<^sub>R (\<R>\<^sup>C \<C>) A w
[PROOF STEP]
by (metis MONO_iADDIb iADDI_a_def iADDI_b_def iADDI_def sp_rel_a sp_rel_b)


[STATEMENT]
lemma "iADDI \<C> \<Longrightarrow>  \<forall>A. \<forall>w. (\<C> A) w \<longleftrightarrow> (\<exists>v. A v \<and> (\<C> (\<lambda>u. u=v)) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI \<C> \<Longrightarrow> \<forall>A w. \<C> A w = nonEmpty (\<lambda>v. A v \<and> \<C> (\<lambda>u. u = v) w)
[PROOF STEP]
using Cl_rel_def sp_rel
[PROOF STATE]
proof (prove)
using this:
\<C>\<^sub>R ?R \<equiv> \<lambda>A w. nonEmpty (\<lambda>v. ?R w v \<and> A v)
iADDI ?\<C> \<Longrightarrow> \<forall>A w. ?\<C> A w = \<C>\<^sub>R (\<R>\<^sup>C ?\<C>) A w

goal (1 subgoal):
 1. iADDI \<C> \<Longrightarrow> \<forall>A w. \<C> A w = nonEmpty (\<lambda>v. A v \<and> \<C> (\<lambda>u. u = v) w)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma "ADDI(\<phi>) \<Longrightarrow> supremum_closed (fp \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ADDI \<phi> \<Longrightarrow> contains (\<lambda>D. \<forall>w. \<phi> \<^bold>\<Or>D w = \<^bold>\<Or>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<phi> X w = X w) D)
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ADDI \<phi> \<Longrightarrow> contains (\<lambda>D. \<forall>w. \<phi> \<^bold>\<Or>D w = \<^bold>\<Or>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<phi> X w = X w) D)
[PROOF STEP]
oops


[STATEMENT]
lemma "MULT(\<phi>) \<Longrightarrow> infimum_closed  (fp \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MULT \<phi> \<Longrightarrow> contains (\<lambda>D. \<forall>w. \<phi> \<^bold>\<And>D w = \<^bold>\<And>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<phi> X w = X w) D)
[PROOF STEP]
(*nitpick*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MULT \<phi> \<Longrightarrow> contains (\<lambda>D. \<forall>w. \<phi> \<^bold>\<And>D w = \<^bold>\<And>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<phi> X w = X w) D)
[PROOF STEP]
oops


[STATEMENT]
lemma "iADDI(\<phi>) \<Longrightarrow> supremum_closed (fp \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iADDI \<phi> \<Longrightarrow> contains (\<lambda>D. \<forall>w. \<phi> \<^bold>\<Or>D w = \<^bold>\<Or>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<phi> X w = X w) D)
[PROOF STEP]
by (metis (full_types) Ra_restr_ex iADDI_def supremum_def)


[STATEMENT]
lemma "iMULT(\<phi>) \<Longrightarrow> infimum_closed  (fp \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iMULT \<phi> \<Longrightarrow> contains (\<lambda>D. \<forall>w. \<phi> \<^bold>\<And>D w = \<^bold>\<And>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<phi> X w = X w) D)
[PROOF STEP]
by (metis (full_types) Ra_restr_all iMULT_def infimum_def)


[STATEMENT]
lemma "supremum_closed (fp (\<C>\<^sub>R R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains (\<lambda>D. \<forall>w. \<C>\<^sub>R R \<^bold>\<Or>D w = \<^bold>\<Or>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<C>\<^sub>R R X w = X w) D)
[PROOF STEP]
by (smt Cl_rel_def supremum_def)


[STATEMENT]
lemma "infimum_closed  (fp (\<I>\<^sub>R R))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. contains (\<lambda>D. \<forall>w. \<I>\<^sub>R R \<^bold>\<And>D w = \<^bold>\<And>D w) (\<lambda>D. nonEmpty D \<and> contains (\<lambda>X. \<forall>w. \<I>\<^sub>R R X w = X w) D)
[PROOF STEP]
by (smt Int_rel_def infimum_def)


[STATEMENT]
lemma "T0_sep \<C> \<Longrightarrow> T1_sep \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w) \<Longrightarrow> \<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w)
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w) \<Longrightarrow> \<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w)
[PROOF STEP]
oops


[STATEMENT]
lemma "T1_sep \<C> \<Longrightarrow> T0_sep \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w) \<Longrightarrow> \<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)
[PROOF STEP]
by (smt compl_def dual_def dual_symm)


[STATEMENT]
lemma "T0_sep \<C> \<longleftrightarrow> antisymmetric (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)) = antisymmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)) = antisymmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
oops


[STATEMENT]
lemma T0_antisymm_a: "MONO \<C> \<Longrightarrow> T0_sep \<C> \<longrightarrow> antisymmetric (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MONO \<C> \<Longrightarrow> (\<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)) \<longrightarrow> antisymmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
by (smt Cl_rel_def compl_def dual_def sp_rel_a)


[STATEMENT]
lemma T0_antisymm_b: "EXP \<C> \<Longrightarrow> IDEM \<C> \<Longrightarrow> antisymmetric (\<R>\<^sup>C \<C>) \<longrightarrow> T0_sep \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>EXP \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> antisymmetric (\<R>\<^sup>C \<C>) \<longrightarrow> (\<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w))
[PROOF STEP]
by (metis (full_types) EXP_dual1 IDEM_def IDEM_dual2 IDEMa_def IDEMb_def compl_def dEXP_def dual_def dual_symm sp_rel_def)


[STATEMENT]
lemma T0_antisymm: "MONO \<C> \<Longrightarrow> EXP \<C> \<Longrightarrow> IDEM \<C> \<Longrightarrow> T0_sep \<C> = antisymmetric (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>MONO \<C>; EXP \<C>; IDEM \<C>\<rbrakk> \<Longrightarrow> (\<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)) = antisymmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
by (metis T0_antisymm_a T0_antisymm_b)


[STATEMENT]
lemma T1_symm_a: "T1_sep \<C> \<longrightarrow> symmetric (\<R>\<^sup>C \<C>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w)) \<longrightarrow> symmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
using sp_rel_def
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sup>C ?\<C> \<equiv> \<lambda>w v. ?\<C> (\<lambda>u. u = v) w

goal (1 subgoal):
 1. (\<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w)) \<longrightarrow> symmetric (\<R>\<^sup>C \<C>)
[PROOF STEP]
by auto


[STATEMENT]
lemma T1_symm_b: "MONO \<C> \<Longrightarrow> EXP \<C> \<Longrightarrow> T0_sep \<C> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>) \<longrightarrow> T1_sep \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>MONO \<C>; EXP \<C>; \<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)\<rbrakk> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>) \<longrightarrow> (\<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w))
[PROOF STEP]
by (metis T0_antisymm_a sp_rel_def sp_rel_reflex)


[STATEMENT]
lemma T1_symm: "MONO \<C> \<Longrightarrow> EXP \<C> \<Longrightarrow> T0_sep \<C> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>) = T1_sep \<C>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>MONO \<C>; EXP \<C>; \<forall>w. contains (\<lambda>v. nonEmpty (\<lambda>G. (\<forall>w. \<C>\<^sup>d G w = G w) \<and> G w \<noteq> G v)) ((\<noteq>) w)\<rbrakk> \<Longrightarrow> symmetric (\<R>\<^sup>C \<C>) = (\<forall>w wa. \<C> (\<lambda>u. u = w) wa = (wa = w))
[PROOF STEP]
by (metis T1_symm_a T1_symm_b)


[STATEMENT]
lemma rec_addr_loc [simp]: "rec_addr_loc = case_addr_loc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_addr_loc = case_addr_loc
[PROOF STEP]
by(auto simp add: fun_eq_iff split: addr_loc.splits)


[STATEMENT]
lemma typeof_lit_eq_Boolean [simp]: "(typeof v = Some Boolean) = (\<exists>b. v = Bool b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof v = \<lfloor>Boolean\<rfloor>) = (\<exists>b. v = Bool b)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma typeof_lit_eq_Integer [simp]: "(typeof v = Some Integer) = (\<exists>i. v = Intg i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof v = \<lfloor>Integer\<rfloor>) = (\<exists>i. v = Intg i)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma typeof_lit_eq_NT [simp]: "(typeof v = Some NT) = (v = Null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof v = \<lfloor>NT\<rfloor>) = (v = Null)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma typeof_lit_eq_Void [simp]: "typeof v = Some Void \<longleftrightarrow> v = Unit"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof v = \<lfloor>Void\<rfloor>) = (v = Unit)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma typeof_lit_neq_Class [simp]: "typeof v \<noteq> Some (Class C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v \<noteq> \<lfloor>Class C\<rfloor>
[PROOF STEP]
by(cases v) auto


[STATEMENT]
lemma typeof_lit_neq_Array [simp]: "typeof v \<noteq> Some (Array T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v \<noteq> \<lfloor>T\<lfloor>\<rceil>\<rfloor>
[PROOF STEP]
by(cases v) auto


[STATEMENT]
lemma typeof_NoneD [simp,dest]:
  "typeof v = Some x \<Longrightarrow> \<not> is_Addr v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v = \<lfloor>x\<rfloor> \<Longrightarrow> \<not> is_Addr v
[PROOF STEP]
by (cases v) auto


[STATEMENT]
lemma typeof_lit_is_type:
  "typeof v = Some T \<Longrightarrow> is_type P T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> is_type P T
[PROOF STEP]
by(cases v) auto


[STATEMENT]
lemma typeof_h_eq_Boolean [simp]: "(typeof\<^bsub>h\<^esub> v = Some Boolean) = (\<exists>b. v = Bool b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof\<^bsub>h\<^esub> v = \<lfloor>Boolean\<rfloor>) = (\<exists>b. v = Bool b)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma typeof_h_eq_Integer [simp]: "(typeof\<^bsub>h\<^esub> v = Some Integer) = (\<exists>i. v = Intg i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof\<^bsub>h\<^esub> v = \<lfloor>Integer\<rfloor>) = (\<exists>i. v = Intg i)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma typeof_h_eq_NT [simp]: "(typeof\<^bsub>h\<^esub> v = Some NT) = (v = Null)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (typeof\<^bsub>h\<^esub> v = \<lfloor>NT\<rfloor>) = (v = Null)
[PROOF STEP]
by(cases v)(auto)


[STATEMENT]
lemma hextI:
  "\<lbrakk> \<And>a C. typeof_addr h a = \<lfloor>Class_type C\<rfloor> \<Longrightarrow> typeof_addr h' a = \<lfloor>Class_type C\<rfloor>;
     \<And>a T n. typeof_addr h a = \<lfloor>Array_type T n\<rfloor> \<Longrightarrow> typeof_addr h' a = \<lfloor>Array_type T n\<rfloor> \<rbrakk>
  \<Longrightarrow> h \<unlhd> h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a C. typeof_addr h a = \<lfloor>Class_type C\<rfloor> \<Longrightarrow> typeof_addr h' a = \<lfloor>Class_type C\<rfloor>; \<And>a T n. typeof_addr h a = \<lfloor>Array_type T n\<rfloor> \<Longrightarrow> typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>\<rbrakk> \<Longrightarrow> h \<unlhd> h'
[PROOF STEP]
unfolding hext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a C. typeof_addr h a = \<lfloor>Class_type C\<rfloor> \<Longrightarrow> typeof_addr h' a = \<lfloor>Class_type C\<rfloor>; \<And>a T n. typeof_addr h a = \<lfloor>Array_type T n\<rfloor> \<Longrightarrow> typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>\<rbrakk> \<Longrightarrow> typeof_addr h \<subseteq>\<^sub>m typeof_addr h'
[PROOF STEP]
by(rule map_leI)(case_tac v, simp_all)


[STATEMENT]
lemma hext_objD:
  assumes "h \<unlhd> h'"
  and "typeof_addr h a = \<lfloor>Class_type C\<rfloor>"
  shows "typeof_addr h' a = \<lfloor>Class_type C\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<unlhd> h'
typeof_addr h a = \<lfloor>Class_type C\<rfloor>

goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
unfolding hext_def
[PROOF STATE]
proof (prove)
using this:
typeof_addr h \<subseteq>\<^sub>m typeof_addr h'
typeof_addr h a = \<lfloor>Class_type C\<rfloor>

goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
by(auto dest: map_le_SomeD)


[STATEMENT]
lemma hext_arrD:
  assumes "h \<unlhd> h'" "typeof_addr h a = \<lfloor>Array_type T n\<rfloor>"
  shows "typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<unlhd> h'
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
unfolding hext_def
[PROOF STATE]
proof (prove)
using this:
typeof_addr h \<subseteq>\<^sub>m typeof_addr h'
typeof_addr h a = \<lfloor>Array_type T n\<rfloor>

goal (1 subgoal):
 1. typeof_addr h' a = \<lfloor>Array_type T n\<rfloor>
[PROOF STEP]
by(blast dest: map_le_SomeD)


[STATEMENT]
lemma hext_refl [iff]: "h \<unlhd> h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<unlhd> h
[PROOF STEP]
by (rule hextI) blast+


[STATEMENT]
lemma hext_trans [trans]: "\<lbrakk> h \<unlhd> h'; h' \<unlhd> h'' \<rbrakk> \<Longrightarrow> h \<unlhd> h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; h' \<unlhd> h''\<rbrakk> \<Longrightarrow> h \<unlhd> h''
[PROOF STEP]
unfolding hext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr h \<subseteq>\<^sub>m typeof_addr h'; typeof_addr h' \<subseteq>\<^sub>m typeof_addr h''\<rbrakk> \<Longrightarrow> typeof_addr h \<subseteq>\<^sub>m typeof_addr h''
[PROOF STEP]
by(rule map_le_trans)


[STATEMENT]
lemma typeof_lit_typeof:
  "typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. typeof v = \<lfloor>T\<rfloor> \<Longrightarrow> typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
by(cases v)(simp_all)


[STATEMENT]
lemma addr_loc_type_fun:
  "\<lbrakk> P,h \<turnstile> a@al : T; P,h \<turnstile> a@al : T' \<rbrakk> \<Longrightarrow> T = T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> a@al : T; P,h \<turnstile> a@al : T'\<rbrakk> \<Longrightarrow> T = T'
[PROOF STEP]
by(auto elim!: addr_loc_type.cases dest: has_field_fun)


[STATEMENT]
lemma THE_addr_loc_type:
  "P,h \<turnstile> a@al : T \<Longrightarrow> (THE T. P,h \<turnstile> a@al : T) = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> a@al : T \<Longrightarrow> (THE T. P,h \<turnstile> a@al : T) = T
[PROOF STEP]
by(rule the_equality)(auto dest: addr_loc_type_fun)


[STATEMENT]
lemma typeof_addr_locI [simp]:
  "P,h \<turnstile> a@al : T \<Longrightarrow> typeof_addr_loc P h a al = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> a@al : T \<Longrightarrow> typeof_addr_loc P h a al = T
[PROOF STEP]
by(auto simp add: typeof_addr_loc_def dest: addr_loc_type_fun)


[STATEMENT]
lemma deterministic_heap_opsI:
  "\<lbrakk> \<And>h ad al v v'. \<lbrakk> heap_read h ad al v; heap_read h ad al v' \<rbrakk> \<Longrightarrow> v = v';
     \<And>h ad al v h' h''. \<lbrakk> heap_write h ad al v h'; heap_write h ad al v h'' \<rbrakk> \<Longrightarrow> h' = h'';
     \<And>h hT h' a h'' a'. \<lbrakk> (h', a) \<in> allocate h hT; (h'', a') \<in> allocate h hT \<rbrakk> \<Longrightarrow> h' = h'' \<and> a = a';
     \<not> spurious_wakeups \<rbrakk>
  \<Longrightarrow> deterministic_heap_ops"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>h ad al v v'. \<lbrakk>heap_read h ad al v; heap_read h ad al v'\<rbrakk> \<Longrightarrow> v = v'; \<And>h ad al v h' h''. \<lbrakk>heap_write h ad al v h'; heap_write h ad al v h''\<rbrakk> \<Longrightarrow> h' = h''; \<And>h hT h' a h'' a'. \<lbrakk>(h', a) \<in> allocate h hT; (h'', a') \<in> allocate h hT\<rbrakk> \<Longrightarrow> h' = h'' \<and> a = a'; \<not> spurious_wakeups\<rbrakk> \<Longrightarrow> deterministic_heap_ops
[PROOF STEP]
unfolding deterministic_heap_ops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>h ad al v v'. \<lbrakk>heap_read h ad al v; heap_read h ad al v'\<rbrakk> \<Longrightarrow> v = v'; \<And>h ad al v h' h''. \<lbrakk>heap_write h ad al v h'; heap_write h ad al v h''\<rbrakk> \<Longrightarrow> h' = h''; \<And>h hT h' a h'' a'. \<lbrakk>(h', a) \<in> allocate h hT; (h'', a') \<in> allocate h hT\<rbrakk> \<Longrightarrow> h' = h'' \<and> a = a'; \<not> spurious_wakeups\<rbrakk> \<Longrightarrow> (\<forall>h ad al v v'. heap_read h ad al v \<longrightarrow> heap_read h ad al v' \<longrightarrow> v = v') \<and> (\<forall>h ad al v h' h''. heap_write h ad al v h' \<longrightarrow> heap_write h ad al v h'' \<longrightarrow> h' = h'') \<and> (\<forall>h hT h' a h'' a'. (h', a) \<in> allocate h hT \<longrightarrow> (h'', a') \<in> allocate h hT \<longrightarrow> h' = h'' \<and> a = a') \<and> \<not> spurious_wakeups
[PROOF STEP]
by blast


[STATEMENT]
lemma deterministic_heap_ops_readD:
  "\<lbrakk> deterministic_heap_ops; heap_read h ad al v; heap_read h ad al v' \<rbrakk> \<Longrightarrow> v = v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>deterministic_heap_ops; heap_read h ad al v; heap_read h ad al v'\<rbrakk> \<Longrightarrow> v = v'
[PROOF STEP]
unfolding deterministic_heap_ops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>h ad al v v'. heap_read h ad al v \<longrightarrow> heap_read h ad al v' \<longrightarrow> v = v') \<and> (\<forall>h ad al v h' h''. heap_write h ad al v h' \<longrightarrow> heap_write h ad al v h'' \<longrightarrow> h' = h'') \<and> (\<forall>h hT h' a h'' a'. (h', a) \<in> allocate h hT \<longrightarrow> (h'', a') \<in> allocate h hT \<longrightarrow> h' = h'' \<and> a = a') \<and> \<not> spurious_wakeups; heap_read h ad al v; heap_read h ad al v'\<rbrakk> \<Longrightarrow> v = v'
[PROOF STEP]
by blast


[STATEMENT]
lemma deterministic_heap_ops_writeD:
  "\<lbrakk> deterministic_heap_ops; heap_write h ad al v h'; heap_write h ad al v h'' \<rbrakk> \<Longrightarrow> h' = h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>deterministic_heap_ops; heap_write h ad al v h'; heap_write h ad al v h''\<rbrakk> \<Longrightarrow> h' = h''
[PROOF STEP]
unfolding deterministic_heap_ops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>h ad al v v'. heap_read h ad al v \<longrightarrow> heap_read h ad al v' \<longrightarrow> v = v') \<and> (\<forall>h ad al v h' h''. heap_write h ad al v h' \<longrightarrow> heap_write h ad al v h'' \<longrightarrow> h' = h'') \<and> (\<forall>h hT h' a h'' a'. (h', a) \<in> allocate h hT \<longrightarrow> (h'', a') \<in> allocate h hT \<longrightarrow> h' = h'' \<and> a = a') \<and> \<not> spurious_wakeups; heap_write h ad al v h'; heap_write h ad al v h''\<rbrakk> \<Longrightarrow> h' = h''
[PROOF STEP]
by blast


[STATEMENT]
lemma deterministic_heap_ops_allocateD:
  "\<lbrakk> deterministic_heap_ops; (h', a) \<in> allocate h hT; (h'', a') \<in> allocate h hT \<rbrakk> \<Longrightarrow> h' = h'' \<and> a = a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>deterministic_heap_ops; (h', a) \<in> allocate h hT; (h'', a') \<in> allocate h hT\<rbrakk> \<Longrightarrow> h' = h'' \<and> a = a'
[PROOF STEP]
unfolding deterministic_heap_ops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>h ad al v v'. heap_read h ad al v \<longrightarrow> heap_read h ad al v' \<longrightarrow> v = v') \<and> (\<forall>h ad al v h' h''. heap_write h ad al v h' \<longrightarrow> heap_write h ad al v h'' \<longrightarrow> h' = h'') \<and> (\<forall>h hT h' a h'' a'. (h', a) \<in> allocate h hT \<longrightarrow> (h'', a') \<in> allocate h hT \<longrightarrow> h' = h'' \<and> a = a') \<and> \<not> spurious_wakeups; (h', a) \<in> allocate h hT; (h'', a') \<in> allocate h hT\<rbrakk> \<Longrightarrow> h' = h'' \<and> a = a'
[PROOF STEP]
by blast


[STATEMENT]
lemma deterministic_heap_ops_no_spurious_wakeups:
  "deterministic_heap_ops \<Longrightarrow> \<not> spurious_wakeups"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deterministic_heap_ops \<Longrightarrow> \<not> spurious_wakeups
[PROOF STEP]
unfolding deterministic_heap_ops_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>h ad al v v'. heap_read h ad al v \<longrightarrow> heap_read h ad al v' \<longrightarrow> v = v') \<and> (\<forall>h ad al v h' h''. heap_write h ad al v h' \<longrightarrow> heap_write h ad al v h'' \<longrightarrow> h' = h'') \<and> (\<forall>h hT h' a h'' a'. (h', a) \<in> allocate h hT \<longrightarrow> (h'', a') \<in> allocate h hT \<longrightarrow> h' = h'' \<and> a = a') \<and> \<not> spurious_wakeups \<Longrightarrow> \<not> spurious_wakeups
[PROOF STEP]
by blast


[STATEMENT]
lemma typeof_addr_thread_id2_addr_addr2thread_id [simp]:
  "\<lbrakk> typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread \<rbrakk> \<Longrightarrow> typeof_addr h (thread_id2addr (addr2thread_id a)) = \<lfloor>Class_type C\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> typeof_addr h (thread_id2addr (addr2thread_id a)) = \<lfloor>Class_type C\<rfloor>
[PROOF STEP]
by(simp add: addr2thread_id_inverse)


[STATEMENT]
lemma typeof_addr_hext_mono:
  "\<lbrakk> h \<unlhd> h'; typeof_addr h a = \<lfloor>hT\<rfloor> \<rbrakk> \<Longrightarrow> typeof_addr h' a = \<lfloor>hT\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; typeof_addr h a = \<lfloor>hT\<rfloor>\<rbrakk> \<Longrightarrow> typeof_addr h' a = \<lfloor>hT\<rfloor>
[PROOF STEP]
unfolding hext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr h \<subseteq>\<^sub>m typeof_addr h'; typeof_addr h a = \<lfloor>hT\<rfloor>\<rbrakk> \<Longrightarrow> typeof_addr h' a = \<lfloor>hT\<rfloor>
[PROOF STEP]
by(rule map_le_SomeD)


[STATEMENT]
lemma hext_typeof_mono:
  "\<lbrakk> h \<unlhd> h'; typeof\<^bsub>h\<^esub> v = Some T \<rbrakk> \<Longrightarrow> typeof\<^bsub>h'\<^esub> v = Some T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> typeof\<^bsub>h'\<^esub> v = \<lfloor>T\<rfloor>
[PROOF STEP]
by (cases v)(auto intro: typeof_addr_hext_mono)


[STATEMENT]
lemma addr_loc_type_hext_mono:
  "\<lbrakk> P,h \<turnstile> a@al : T; h \<unlhd> h' \<rbrakk> \<Longrightarrow> P,h' \<turnstile> a@al : T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,h \<turnstile> a@al : T; h \<unlhd> h'\<rbrakk> \<Longrightarrow> P,h' \<turnstile> a@al : T
[PROOF STEP]
by(force elim!: addr_loc_type.cases intro: addr_loc_type.intros elim: typeof_addr_hext_mono dest: hext_arrD)


[STATEMENT]
lemma type_of_hext_type_of: \<comment> \<open>FIXME: What's this rule good for?\<close>
  "\<lbrakk> typeof\<^bsub>h\<^esub> w = \<lfloor>T\<rfloor>; hext h h' \<rbrakk> \<Longrightarrow> typeof\<^bsub>h'\<^esub> w = \<lfloor>T\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof\<^bsub>h\<^esub> w = \<lfloor>T\<rfloor>; h \<unlhd> h'\<rbrakk> \<Longrightarrow> typeof\<^bsub>h'\<^esub> w = \<lfloor>T\<rfloor>
[PROOF STEP]
by(rule hext_typeof_mono)


[STATEMENT]
lemma hext_None: "\<lbrakk> h \<unlhd> h'; typeof_addr h' a = None \<rbrakk> \<Longrightarrow> typeof_addr h a = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<unlhd> h'; typeof_addr h' a = None\<rbrakk> \<Longrightarrow> typeof_addr h a = None
[PROOF STEP]
by(rule ccontr)(auto dest: typeof_addr_hext_mono)


[STATEMENT]
lemma map_typeof_hext_mono:
  "\<lbrakk> map typeof\<^bsub>h\<^esub> vs = map Some Ts; h \<unlhd> h' \<rbrakk> \<Longrightarrow>  map typeof\<^bsub>h'\<^esub> vs = map Some Ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map typeof\<^bsub>h\<^esub> vs = map Some Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> map typeof\<^bsub>h'\<^esub> vs = map Some Ts
[PROOF STEP]
apply(induct vs arbitrary: Ts)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Ts. \<lbrakk>map typeof\<^bsub>h\<^esub> [] = map Some Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> map typeof\<^bsub>h'\<^esub> [] = map Some Ts
 2. \<And>a vs Ts. \<lbrakk>\<And>Ts. \<lbrakk>map typeof\<^bsub>h\<^esub> vs = map Some Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> map typeof\<^bsub>h'\<^esub> vs = map Some Ts; map typeof\<^bsub>h\<^esub> (a # vs) = map Some Ts; h \<unlhd> h'\<rbrakk> \<Longrightarrow> map typeof\<^bsub>h'\<^esub> (a # vs) = map Some Ts
[PROOF STEP]
apply(auto simp add: Cons_eq_map_conv intro: hext_typeof_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hext_typeof_addr_map_le:
  "h \<unlhd> h' \<Longrightarrow> typeof_addr h \<subseteq>\<^sub>m typeof_addr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<unlhd> h' \<Longrightarrow> typeof_addr h \<subseteq>\<^sub>m typeof_addr h'
[PROOF STEP]
by(auto simp add: map_le_def dest: typeof_addr_hext_mono)


[STATEMENT]
lemma hext_dom_typeof_addr_subset:
  "h \<unlhd> h' \<Longrightarrow> dom (typeof_addr h) \<subseteq> dom (typeof_addr h')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<unlhd> h' \<Longrightarrow> dom (typeof_addr h) \<subseteq> dom (typeof_addr h')
[PROOF STEP]
by (metis hext_typeof_addr_map_le map_le_implies_dom_le)


[STATEMENT]
lemma entry_dominate_dom:
  assumes "i \<in> set (g_V G)"
      and "dominate i 0"
    shows "dom i 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom i 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> set (g_V G)
dominate i 0

goal (1 subgoal):
 1. local.dom i 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<in> set (g_V G); dominate i 0\<rbrakk> \<Longrightarrow> local.dom i 0
[PROOF STEP]
from assms(1) entry0_dominates_all
[PROOF STATE]
proof (chain)
picking this:
i \<in> set (g_V G)
\<forall>p\<in>set (g_V G). dominate 0 p
[PROOF STEP]
have "dominate 0 i"
[PROOF STATE]
proof (prove)
using this:
i \<in> set (g_V G)
\<forall>p\<in>set (g_V G). dominate 0 p

goal (1 subgoal):
 1. dominate 0 i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dominate 0 i

goal (1 subgoal):
 1. \<lbrakk>i \<in> set (g_V G); dominate i 0\<rbrakk> \<Longrightarrow> local.dom i 0
[PROOF STEP]
with assms(2) reachable
[PROOF STATE]
proof (chain)
picking this:
dominate i 0
\<forall>v\<in>set (g_V G). v \<in> (g_E G)\<^sup>* `` {0}
dominate 0 i
[PROOF STEP]
have "i = 0"
[PROOF STATE]
proof (prove)
using this:
dominate i 0
\<forall>v\<in>set (g_V G). v \<in> (g_E G)\<^sup>* `` {0}
dominate 0 i

goal (1 subgoal):
 1. i = 0
[PROOF STEP]
using reachable_dom_acyclic
[PROOF STATE]
proof (prove)
using this:
dominate i 0
\<forall>v\<in>set (g_V G). v \<in> (g_E G)\<^sup>* `` {0}
dominate 0 i
\<lbrakk>reachable ?n2.0; dominate ?n1.0 ?n2.0; dominate ?n2.0 ?n1.0\<rbrakk> \<Longrightarrow> ?n1.0 = ?n2.0

goal (1 subgoal):
 1. i = 0
[PROOF STEP]
by (auto simp add:reachable_def)
[PROOF STATE]
proof (state)
this:
i = 0

goal (1 subgoal):
 1. \<lbrakk>i \<in> set (g_V G); dominate i 0\<rbrakk> \<Longrightarrow> local.dom i 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = 0

goal (1 subgoal):
 1. local.dom i 0
[PROOF STEP]
using dom_refl
[PROOF STATE]
proof (prove)
using this:
i = 0
local.dom ?i ?i

goal (1 subgoal):
 1. local.dom i 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.dom i 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_entry_dom:
  fixes pa i d
  assumes "path_entry (g_E G) pa i"
      and "dom d i"
    shows "d \<in> set pa \<or> d = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> set pa \<or> d = i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path_entry (g_E G) pa i
local.dom d i

goal (1 subgoal):
 1. d \<in> set pa \<or> d = i
[PROOF STEP]
proof(induct rule:path_entry.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.dom d 0 \<Longrightarrow> d \<in> set [] \<or> d = 0
 2. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
case path_entry0
[PROOF STATE]
proof (state)
this:
local.dom d 0

goal (2 subgoals):
 1. local.dom d 0 \<Longrightarrow> d \<in> set [] \<or> d = 0
 2. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.dom d 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
local.dom d 0

goal (1 subgoal):
 1. d \<in> set [] \<or> d = 0
[PROOF STEP]
using zero_dom_zero
[PROOF STATE]
proof (prove)
using this:
local.dom d 0
local.dom ?i 0 = (?i = 0)

goal (1 subgoal):
 1. d \<in> set [] \<or> d = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<in> set [] \<or> d = 0

goal (1 subgoal):
 1. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
case (path_entry_prepend u v l)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> g_E G
path_entry (g_E G) l u
local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u
local.dom d v

goal (1 subgoal):
 1. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
note u_v = path_entry_prepend.hyps(1)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> g_E G

goal (1 subgoal):
 1. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
note ind = path_entry_prepend.hyps(3)
[PROOF STATE]
proof (state)
this:
local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u

goal (1 subgoal):
 1. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
note d_v = path_entry_prepend.prems
[PROOF STATE]
proof (state)
this:
local.dom d v

goal (1 subgoal):
 1. \<And>u v l. \<lbrakk>(u, v) \<in> g_E G; path_entry (g_E G) l u; local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u; local.dom d v\<rbrakk> \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d \<in> set (u # l) \<or> d = v
[PROOF STEP]
proof(cases "d \<noteq> v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
 2. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
d \<noteq> v

goal (2 subgoals):
 1. d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
 2. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
note d_n_v = this
[PROOF STATE]
proof (state)
this:
d \<noteq> v

goal (2 subgoals):
 1. d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
 2. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
from u_v
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> g_E G
[PROOF STEP]
have "v \<in> succs u"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> g_E G

goal (1 subgoal):
 1. v \<in> succs u
[PROOF STEP]
by (simp add:succs_def)
[PROOF STATE]
proof (state)
this:
v \<in> succs u

goal (2 subgoals):
 1. d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
 2. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
with d_v d_n_v
[PROOF STATE]
proof (chain)
picking this:
local.dom d v
d \<noteq> v
v \<in> succs u
[PROOF STEP]
have "dom d u"
[PROOF STATE]
proof (prove)
using this:
local.dom d v
d \<noteq> v
v \<in> succs u

goal (1 subgoal):
 1. local.dom d u
[PROOF STEP]
by (auto intro:adom_succs)
[PROOF STATE]
proof (state)
this:
local.dom d u

goal (2 subgoals):
 1. d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
 2. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
with ind
[PROOF STATE]
proof (chain)
picking this:
local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u
local.dom d u
[PROOF STEP]
have "d \<in> set l \<or> d = u"
[PROOF STATE]
proof (prove)
using this:
local.dom d u \<Longrightarrow> d \<in> set l \<or> d = u
local.dom d u

goal (1 subgoal):
 1. d \<in> set l \<or> d = u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<in> set l \<or> d = u

goal (2 subgoals):
 1. d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
 2. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d \<in> set l \<or> d = u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d \<in> set l \<or> d = u

goal (1 subgoal):
 1. d \<in> set (u # l) \<or> d = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<in> set (u # l) \<or> d = v

goal (1 subgoal):
 1. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> d \<noteq> v

goal (1 subgoal):
 1. \<not> d \<noteq> v \<Longrightarrow> d \<in> set (u # l) \<or> d = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> d \<noteq> v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> d \<noteq> v

goal (1 subgoal):
 1. d \<in> set (u # l) \<or> d = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d \<in> set (u # l) \<or> d = v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d \<in> set (u # l) \<or> d = v

goal:
No subgoals!
[PROOF STEP]
qed

\<comment>\<open>soundenss\<close>


[STATEMENT]
lemma dom_sound: "dom i j \<Longrightarrow> dominate i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dom i j \<Longrightarrow> dominate i j
[PROOF STEP]
by (fastforce simp add: dominate_def dest:path_entry_dom)


[STATEMENT]
lemma sdom_sound: "strict_dom i j \<Longrightarrow> j \<in> set (g_V G) \<Longrightarrow> strict_dominate i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> strict_dominate i j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> strict_dominate i j
[PROOF STEP]
assume sdom: "strict_dom i j" and "j \<in> set (g_V G)"
[PROOF STATE]
proof (state)
this:
strict_dom i j
j \<in> set (g_V G)

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> strict_dominate i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
strict_dom i j
j \<in> set (g_V G)
[PROOF STEP]
have i_n_j: "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
j \<in> set (g_V G)

goal (1 subgoal):
 1. i \<noteq> j
[PROOF STEP]
by (rule sdom_asyc)
[PROOF STATE]
proof (state)
this:
i \<noteq> j

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> strict_dominate i j
[PROOF STEP]
from sdom
[PROOF STATE]
proof (chain)
picking this:
strict_dom i j
[PROOF STEP]
have "dom i j"
[PROOF STATE]
proof (prove)
using this:
strict_dom i j

goal (1 subgoal):
 1. local.dom i j
[PROOF STEP]
using sdom_dom
[PROOF STATE]
proof (prove)
using this:
strict_dom i j
strict_dom ?i ?j \<Longrightarrow> local.dom ?i ?j

goal (1 subgoal):
 1. local.dom i j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.dom i j

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> strict_dominate i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
local.dom i j
[PROOF STEP]
have domi: "dominate i j"
[PROOF STATE]
proof (prove)
using this:
local.dom i j

goal (1 subgoal):
 1. dominate i j
[PROOF STEP]
by (rule dom_sound)
[PROOF STATE]
proof (state)
this:
dominate i j

goal (1 subgoal):
 1. \<lbrakk>strict_dom i j; j \<in> set (g_V G)\<rbrakk> \<Longrightarrow> strict_dominate i j
[PROOF STEP]
with i_n_j
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> j
dominate i j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<noteq> j
dominate i j

goal (1 subgoal):
 1. strict_dominate i j
[PROOF STEP]
by (fastforce dest: dominate_sdominate)
[PROOF STATE]
proof (state)
this:
strict_dominate i j

goal:
No subgoals!
[PROOF STEP]
qed

\<comment>\<open>completeness\<close>


[STATEMENT]
lemma dom_complete_auxi: "i < length start \<Longrightarrow> (dom_kildall start)!i = ss' \<and> k \<notin> set ss' \<Longrightarrow> non_strict_dominate k i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length start; dom_kildall start ! i = ss' \<and> k \<notin> set ss'\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i < length start; dom_kildall start ! i = ss' \<and> k \<notin> set ss'\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
assume i_lt: "i < length start" and dom_kil: "(dom_kildall start)!i = ss'\<and> k \<notin> set ss'"
[PROOF STATE]
proof (state)
this:
i < length start
dom_kildall start ! i = ss' \<and> k \<notin> set ss'

goal (1 subgoal):
 1. \<lbrakk>i < length start; dom_kildall start ! i = ss' \<and> k \<notin> set ss'\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length start
dom_kildall start ! i = ss' \<and> k \<notin> set ss'
[PROOF STEP]
have dom_iter: "(fst (iter f step start (unstables r step start)))!i = ss'" and k_nin: "k \<notin> set ss'"
[PROOF STATE]
proof (prove)
using this:
i < length start
dom_kildall start ! i = ss' \<and> k \<notin> set ss'

goal (1 subgoal):
 1. fst (iter f step start (unstables r step start)) ! i = ss' &&& k \<notin> set ss'
[PROOF STEP]
using nodes_semi_def r_def f_def step_def dom_kildall_def kildall_def
[PROOF STATE]
proof (prove)
using this:
i < length start
dom_kildall start ! i = ss' \<and> k \<notin> set ss'
nodes_semi \<equiv> ((rev \<circ> sorted_list_of_set) ` Pow (set nodes), nodes_le, nodes_sup)
r \<equiv> nodes_le
f \<equiv> nodes_sup
step \<equiv> exec
dom_kildall = kildall (fst (snd nodes_semi)) (snd (snd nodes_semi)) exec
kildall ?r ?f ?step ?\<tau>s = fst (iter ?f ?step ?\<tau>s (unstables ?r ?step ?\<tau>s))

goal (1 subgoal):
 1. fst (iter f step start (unstables r step start)) ! i = ss' &&& k \<notin> set ss'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst (iter f step start (unstables r step start)) ! i = ss'
k \<notin> set ss'

goal (1 subgoal):
 1. \<lbrakk>i < length start; dom_kildall start ! i = ss' \<and> k \<notin> set ss'\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst (iter f step start (unstables r step start)) ! i = ss'
k \<notin> set ss'
[PROOF STEP]
obtain s w where iter: " iter f step start (unstables r step start) = (s, w)"
[PROOF STATE]
proof (prove)
using this:
fst (iter f step start (unstables r step start)) ! i = ss'
k \<notin> set ss'

goal (1 subgoal):
 1. (\<And>s w. iter f step start (unstables r step start) = (s, w) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
iter f step start (unstables r step start) = (s, w)

goal (1 subgoal):
 1. \<lbrakk>i < length start; dom_kildall start ! i = ss' \<and> k \<notin> set ss'\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with dom_iter
[PROOF STATE]
proof (chain)
picking this:
fst (iter f step start (unstables r step start)) ! i = ss'
iter f step start (unstables r step start) = (s, w)
[PROOF STEP]
have "s!i = ss'"
[PROOF STATE]
proof (prove)
using this:
fst (iter f step start (unstables r step start)) ! i = ss'
iter f step start (unstables r step start) = (s, w)

goal (1 subgoal):
 1. s ! i = ss'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s ! i = ss'

goal (1 subgoal):
 1. \<lbrakk>i < length start; dom_kildall start ! i = ss' \<and> k \<notin> set ss'\<rbrakk> \<Longrightarrow> non_strict_dominate k i
[PROOF STEP]
with iter_dom_invariant_complete iter k_nin i_lt len_start_is_n
[PROOF STATE]
proof (chain)
picking this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> ?i < n \<and> ?ss' ! ?i = ?res \<and> ?k \<notin> set ?res \<longrightarrow> non_strict_dominate ?k ?i
iter f step start (unstables r step start) = (s, w)
k \<notin> set ss'
i < length start
length start = n
s ! i = ss'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
iter f step start (unstables r step start) = (?ss', ?w') \<longrightarrow> ?i < n \<and> ?ss' ! ?i = ?res \<and> ?k \<notin> set ?res \<longrightarrow> non_strict_dominate ?k ?i
iter f step start (unstables r step start) = (s, w)
k \<notin> set ss'
i < length start
length start = n
s ! i = ss'

goal (1 subgoal):
 1. non_strict_dominate k i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
non_strict_dominate k i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma notsdom_notsdominate: "\<not> strict_dom i j \<Longrightarrow> j < length start \<Longrightarrow> non_strict_dominate i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate i j
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate i j
[PROOF STEP]
assume i_not_sdom_j: "\<not> strict_dom i j" and j_lt: "j < length start"
[PROOF STATE]
proof (state)
this:
\<not> strict_dom i j
j < length start

goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> strict_dom i j
j < length start
[PROOF STEP]
obtain res where j_res: "dom_kildall start ! j = res"
[PROOF STATE]
proof (prove)
using this:
\<not> strict_dom i j
j < length start

goal (1 subgoal):
 1. (\<And>res. dom_kildall start ! j = res \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add:strict_dom_def)
[PROOF STATE]
proof (state)
this:
dom_kildall start ! j = res

goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate i j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dom_kildall start ! j = res
[PROOF STEP]
have "strict_dom i j = (i \<in> set res)"
[PROOF STATE]
proof (prove)
using this:
dom_kildall start ! j = res

goal (1 subgoal):
 1. strict_dom i j = (i \<in> set res)
[PROOF STEP]
by (auto simp add:strict_dom_def start_def n_def nodes_def)
[PROOF STATE]
proof (state)
this:
strict_dom i j = (i \<in> set res)

goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate i j
[PROOF STEP]
with i_not_sdom_j
[PROOF STATE]
proof (chain)
picking this:
\<not> strict_dom i j
strict_dom i j = (i \<in> set res)
[PROOF STEP]
have i_nin: "i \<notin> set res"
[PROOF STATE]
proof (prove)
using this:
\<not> strict_dom i j
strict_dom i j = (i \<in> set res)

goal (1 subgoal):
 1. i \<notin> set res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<notin> set res

goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate i j
[PROOF STEP]
with j_res j_lt
[PROOF STATE]
proof (chain)
picking this:
dom_kildall start ! j = res
j < length start
i \<notin> set res
[PROOF STEP]
show "non_strict_dominate i j"
[PROOF STATE]
proof (prove)
using this:
dom_kildall start ! j = res
j < length start
i \<notin> set res

goal (1 subgoal):
 1. non_strict_dominate i j
[PROOF STEP]
using dom_complete_auxi
[PROOF STATE]
proof (prove)
using this:
dom_kildall start ! j = res
j < length start
i \<notin> set res
\<lbrakk>?i < length start; dom_kildall start ! ?i = ?ss' \<and> ?k \<notin> set ?ss'\<rbrakk> \<Longrightarrow> non_strict_dominate ?k ?i

goal (1 subgoal):
 1. non_strict_dominate i j
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
non_strict_dominate i j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma notsdom_notsdominate': "\<not> strict_dom i j \<Longrightarrow> j < length start \<Longrightarrow> \<not> strict_dominate i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> \<not> strict_dominate i j
[PROOF STEP]
using notsdom_notsdominate nonstrict_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> strict_dom ?i ?j; ?j < length start\<rbrakk> \<Longrightarrow> non_strict_dominate ?i ?j
non_strict_dominate ?i ?j \<Longrightarrow> \<not> strict_dominate ?i ?j

goal (1 subgoal):
 1. \<lbrakk>\<not> strict_dom i j; j < length start\<rbrakk> \<Longrightarrow> \<not> strict_dominate i j
[PROOF STEP]
by auto


[STATEMENT]
lemma dom_complete: "strict_dominate i j \<Longrightarrow> j < size start \<Longrightarrow> strict_dom i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strict_dominate i j; j < length start\<rbrakk> \<Longrightarrow> strict_dom i j
[PROOF STEP]
by (insert notsdom_notsdominate') (auto intro: contrapos_nn nonstrict_eq)


[STATEMENT]
lemma (in wf_digraph) sp_non_neg_if_w_non_neg:
  assumes w_non_neg: "\<forall>e \<in> arcs G. w e \<ge> 0"
  shows "\<mu> w u v \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<mu> w u v
[PROOF STEP]
proof(cases "u \<rightarrow>\<^sup>*\<^bsub>G\<^esub> v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
 2. \<not> u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u \<rightarrow>\<^sup>* v

goal (2 subgoals):
 1. u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
 2. \<not> u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
[PROOF STEP]
have *: "awalk u p v \<Longrightarrow> awalk_cost w p \<ge> 0" for p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. awalk u p v \<Longrightarrow> 0 \<le> awalk_cost w p
[PROOF STEP]
by (simp add: pos_cost_pos_awalk_cost w_non_neg)
[PROOF STATE]
proof (state)
this:
awalk u ?p2 v \<Longrightarrow> 0 \<le> awalk_cost w ?p2

goal (2 subgoals):
 1. u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
 2. \<not> u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
awalk u ?p2 v \<Longrightarrow> 0 \<le> awalk_cost w ?p2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
awalk u ?p2 v \<Longrightarrow> 0 \<le> awalk_cost w ?p2

goal (1 subgoal):
 1. 0 \<le> \<mu> w u v
[PROOF STEP]
unfolding \<mu>_def
[PROOF STATE]
proof (prove)
using this:
awalk u ?p2 v \<Longrightarrow> 0 \<le> awalk_cost w ?p2

goal (1 subgoal):
 1. 0 \<le> (INF p\<in>{p. awalk u p v}. ereal (awalk_cost w p))
[PROOF STEP]
by (metis (mono_tags, lifting) INF_less_iff ereal_less_eq(5) mem_Collect_eq not_less)
[PROOF STATE]
proof (state)
this:
0 \<le> \<mu> w u v

goal (1 subgoal):
 1. \<not> u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> u \<rightarrow>\<^sup>* v

goal (1 subgoal):
 1. \<not> u \<rightarrow>\<^sup>* v \<Longrightarrow> 0 \<le> \<mu> w u v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> u \<rightarrow>\<^sup>* v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> u \<rightarrow>\<^sup>* v

goal (1 subgoal):
 1. 0 \<le> \<mu> w u v
[PROOF STEP]
by (simp add: shortest_path_inf)
[PROOF STATE]
proof (state)
this:
0 \<le> \<mu> w u v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in wf_digraph) sp_to_self_if_w_non_neg:
  assumes w_non_neg: "\<forall>e \<in> arcs G. w e \<ge> 0" and "u \<in> verts G"
  shows "\<mu> w u u = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> w u u = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<mu> w u u = 0
[PROOF STEP]
have "awalk u [] u" and "awalk_cost w [] = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. awalk u [] u &&& awalk_cost w [] = 0
[PROOF STEP]
by (auto simp: assms(2) awalk_Nil_iff)
[PROOF STATE]
proof (state)
this:
awalk u [] u
awalk_cost w [] = 0

goal (1 subgoal):
 1. \<mu> w u u = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
awalk u [] u
awalk_cost w [] = 0

goal (1 subgoal):
 1. \<mu> w u u = 0
[PROOF STEP]
have "\<mu> w u u \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> \<mu> w u u
[PROOF STEP]
by (simp add: sp_non_neg_if_w_non_neg w_non_neg)
[PROOF STATE]
proof (state)
this:
0 \<le> \<mu> w u u

goal (1 subgoal):
 1. \<mu> w u u = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
awalk u [] u
awalk_cost w [] = 0
0 \<le> \<mu> w u u
[PROOF STEP]
show "\<mu> w u u = 0"
[PROOF STATE]
proof (prove)
using this:
awalk u [] u
awalk_cost w [] = 0
0 \<le> \<mu> w u u

goal (1 subgoal):
 1. \<mu> w u u = 0
[PROOF STEP]
by (metis antisym ereal_eq_0(2) min_cost_le_walk_cost)
[PROOF STATE]
proof (state)
this:
\<mu> w u u = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in fin_digraph) reachable_verts_finite: "finite {x. u \<rightarrow>\<^sup>* x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. u \<rightarrow>\<^sup>* x}
[PROOF STEP]
using finite_verts
[PROOF STATE]
proof (prove)
using this:
finite (verts G)

goal (1 subgoal):
 1. finite {x. u \<rightarrow>\<^sup>* x}
[PROOF STEP]
by (metis finite_subset mem_Collect_eq reachable_in_vertsE subsetI)


[STATEMENT]
lemma (in wf_digraph) awalk_not_distinct:
  assumes "finite (verts G)" and "awalk u p v" and "length p \<ge> card (verts G)"
  shows "\<not> distinct (awalk_verts u p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
have *: "length (awalk_verts u p) > length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p < length (awalk_verts u p)
[PROOF STEP]
by (induction p arbitrary: u) auto
[PROOF STATE]
proof (state)
this:
length p < length (awalk_verts u p)

goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
proof(cases "length p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length p = 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
 2. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length p = 0

goal (2 subgoals):
 1. length p = 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
 2. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite (verts G)
awalk u p v
card (verts G) \<le> length p
length p = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (verts G)
awalk u p v
card (verts G) \<le> length p
length p = 0

goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
unfolding awalk_def
[PROOF STATE]
proof (prove)
using this:
finite (verts G)
u \<in> verts G \<and> set p \<subseteq> arcs G \<and> cas u p v
card (verts G) \<le> length p
length p = 0

goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> distinct (awalk_verts u p)

goal (1 subgoal):
 1. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
length p \<noteq> 0

goal (1 subgoal):
 1. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
with assms *
[PROOF STATE]
proof (chain)
picking this:
finite (verts G)
awalk u p v
card (verts G) \<le> length p
length p < length (awalk_verts u p)
length p \<noteq> 0
[PROOF STEP]
have "length (awalk_verts u p) > card (verts G)"
[PROOF STATE]
proof (prove)
using this:
finite (verts G)
awalk u p v
card (verts G) \<le> length p
length p < length (awalk_verts u p)
length p \<noteq> 0

goal (1 subgoal):
 1. card (verts G) < length (awalk_verts u p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (verts G) < length (awalk_verts u p)

goal (1 subgoal):
 1. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (verts G) < length (awalk_verts u p)

goal (1 subgoal):
 1. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
have "set (awalk_verts u p) \<subseteq> verts G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (awalk_verts u p) \<subseteq> verts G
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
awalk u p v

goal (1 subgoal):
 1. set (awalk_verts u p) \<subseteq> verts G
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (awalk_verts u p) \<subseteq> verts G

goal (1 subgoal):
 1. length p \<noteq> 0 \<Longrightarrow> \<not> distinct (awalk_verts u p)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (verts G) < length (awalk_verts u p)
set (awalk_verts u p) \<subseteq> verts G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (verts G) < length (awalk_verts u p)
set (awalk_verts u p) \<subseteq> verts G

goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
card (verts G) < length (awalk_verts u p)
set (awalk_verts u p) \<subseteq> verts G
finite (verts G)

goal (1 subgoal):
 1. \<not> distinct (awalk_verts u p)
[PROOF STEP]
by (induction p arbitrary: u)
         (auto, metis card_subset_eq distinct_card less_antisym)
[PROOF STATE]
proof (state)
this:
\<not> distinct (awalk_verts u p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> distinct (awalk_verts u p)

goal:
No subgoals!
[PROOF STEP]
qed