[STATEMENT]
lemma integrable_ident_ivl[intro, simp]: "(\<lambda>x. x) integrable_on closed_segment a (b::real)"
  and integrable_ident_cbox[intro, simp]: "(\<lambda>x. x) integrable_on cbox a (b::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x) integrable_on {a--b} &&& (\<lambda>x. x) integrable_on cbox a b
[PROOF STEP]
by (auto simp: closed_segment_eq_real_ivl ident_integrable_on)


[STATEMENT]
lemma compress_irule_set_eq[simp]: "compress_irule_set rs = rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compress_irule_set rs = rs
[PROOF STEP]
unfolding compress_irule_set_def map_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fcompress \<circ> (|`|) (\<lambda>(x, y). (id x, (fcompress \<circ> (|`|) (\<lambda>(x, y). (id x, compress_pterm y))) y))) rs = rs
[PROOF STEP]
by simp


[STATEMENT]
lemma \<Delta>_trancl_sound:
  "\<Delta>_trancl_set A B = saturate"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Delta>_trancl_set A B = saturate
[PROOF STEP]
proof (intro set_eqI iffI, goal_cases lr rl)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<Delta>_trancl_set A B \<Longrightarrow> x \<in> saturate
 2. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
case (lr x)
[PROOF STATE]
proof (state)
this:
x \<in> \<Delta>_trancl_set A B

goal (2 subgoals):
 1. \<And>x. x \<in> \<Delta>_trancl_set A B \<Longrightarrow> x \<in> saturate
 2. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
obtain p q where x: "x = (p, q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. x = (p, q) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x)
[PROOF STATE]
proof (state)
this:
x = (p, q)

goal (2 subgoals):
 1. \<And>x. x \<in> \<Delta>_trancl_set A B \<Longrightarrow> x \<in> saturate
 2. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> saturate
[PROOF STEP]
using lr
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Delta>_trancl_set A B

goal (1 subgoal):
 1. x \<in> saturate
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> \<Delta>_trancl_set A B

goal (1 subgoal):
 1. (p, q) \<in> saturate
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>f ps p qs q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules A; f qs \<rightarrow> q |\<in>| rules B; length ps = length qs; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) \<in> \<Delta>_trancl_set A B; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q) \<in> saturate
 2. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps A; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p', q) \<in> saturate
 3. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 4. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
case (\<Delta>_set_cong f ps p qs q)
[PROOF STATE]
proof (state)
this:
f ps \<rightarrow> p |\<in>| rules A
f qs \<rightarrow> q |\<in>| rules B
length ps = length qs
?i < length qs \<Longrightarrow> (ps ! ?i, qs ! ?i) \<in> \<Delta>_trancl_set A B
?i < length qs \<Longrightarrow> (ps ! ?i, qs ! ?i) \<in> saturate

goal (4 subgoals):
 1. \<And>f ps p qs q. \<lbrakk>f ps \<rightarrow> p |\<in>| rules A; f qs \<rightarrow> q |\<in>| rules B; length ps = length qs; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) \<in> \<Delta>_trancl_set A B; \<And>i. i < length qs \<Longrightarrow> (ps ! i, qs ! i) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q) \<in> saturate
 2. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps A; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p', q) \<in> saturate
 3. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 4. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p, q) \<in> saturate
[PROOF STEP]
apply (intro infer[of "zip ps qs" "(p, q)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. zip ps qs \<rightarrow>\<^sub>h (p, q) \<in> \<Delta>_trancl_rules A B
 2. \<And>x. x \<in> set (zip ps qs) \<Longrightarrow> x \<in> saturate
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zip ps qs \<rightarrow>\<^sub>h (p, q) \<in> \<Delta>_trancl_rules A B
[PROOF STEP]
using \<Delta>_set_cong(1-3)
[PROOF STATE]
proof (prove)
using this:
f ps \<rightarrow> p |\<in>| rules A
f qs \<rightarrow> q |\<in>| rules B
length ps = length qs

goal (1 subgoal):
 1. zip ps qs \<rightarrow>\<^sub>h (p, q) \<in> \<Delta>_trancl_rules A B
[PROOF STEP]
by (auto simp: \<Delta>_trancl_rules_def \<Delta>\<^sub>\<epsilon>_rules_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (zip ps qs) \<Longrightarrow> x \<in> saturate
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x_ \<in> set (zip ps qs) \<Longrightarrow> x_ \<in> saturate
[PROOF STEP]
using \<Delta>_set_cong(3,5)
[PROOF STATE]
proof (prove)
using this:
length ps = length qs
?i < length qs \<Longrightarrow> (ps ! ?i, qs ! ?i) \<in> saturate

goal (1 subgoal):
 1. x_ \<in> set (zip ps qs) \<Longrightarrow> x_ \<in> saturate
[PROOF STEP]
by (auto simp: zip_nth_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(p, q) \<in> saturate

goal (3 subgoals):
 1. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps A; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p', q) \<in> saturate
 2. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 3. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps A; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p', q) \<in> saturate
 2. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 3. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
case (\<Delta>_set_eps1 p p' q)
[PROOF STATE]
proof (state)
this:
(p, p') |\<in>| eps A
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate

goal (3 subgoals):
 1. \<And>p p' q. \<lbrakk>(p, p') |\<in>| eps A; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p', q) \<in> saturate
 2. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 3. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, p') |\<in>| eps A
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(p, p') |\<in>| eps A
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate

goal (1 subgoal):
 1. (p', q) \<in> saturate
[PROOF STEP]
by (intro infer[of "[(p, q)]" "(p', q)"]) (auto simp: \<Delta>_trancl_rules_def \<Delta>\<^sub>\<epsilon>_rules_def)
[PROOF STATE]
proof (state)
this:
(p', q) \<in> saturate

goal (2 subgoals):
 1. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 2. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 2. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
case (\<Delta>_set_eps2 q q' p)
[PROOF STATE]
proof (state)
this:
(q, q') |\<in>| eps B
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate

goal (2 subgoals):
 1. \<And>q q' p. \<lbrakk>(q, q') |\<in>| eps B; (p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate\<rbrakk> \<Longrightarrow> (p, q') \<in> saturate
 2. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q, q') |\<in>| eps B
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(q, q') |\<in>| eps B
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate

goal (1 subgoal):
 1. (p, q') \<in> saturate
[PROOF STEP]
by (intro infer[of "[(p, q)]" "(p, q')"]) (auto simp: \<Delta>_trancl_rules_def \<Delta>\<^sub>\<epsilon>_rules_def)
[PROOF STATE]
proof (state)
this:
(p, q') \<in> saturate

goal (1 subgoal):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
case (\<Delta>_set_trans p q r)
[PROOF STATE]
proof (state)
this:
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate
(q, r) \<in> \<Delta>_trancl_set A B
(q, r) \<in> saturate

goal (1 subgoal):
 1. \<And>p q r. \<lbrakk>(p, q) \<in> \<Delta>_trancl_set A B; (p, q) \<in> saturate; (q, r) \<in> \<Delta>_trancl_set A B; (q, r) \<in> saturate\<rbrakk> \<Longrightarrow> (p, r) \<in> saturate
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate
(q, r) \<in> \<Delta>_trancl_set A B
(q, r) \<in> saturate
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> \<Delta>_trancl_set A B
(p, q) \<in> saturate
(q, r) \<in> \<Delta>_trancl_set A B
(q, r) \<in> saturate

goal (1 subgoal):
 1. (p, r) \<in> saturate
[PROOF STEP]
by (intro infer[of "[(p,q), (q,r)]" "(p, r)"]) (auto simp: \<Delta>_trancl_rules_def \<Delta>\<^sub>\<epsilon>_rules_def)
[PROOF STATE]
proof (state)
this:
(p, r) \<in> saturate

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> saturate

goal (1 subgoal):
 1. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
case (rl x)
[PROOF STATE]
proof (state)
this:
x \<in> saturate

goal (1 subgoal):
 1. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
obtain p q where x: "x = (p, q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q. x = (p, q) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases x)
[PROOF STATE]
proof (state)
this:
x = (p, q)

goal (1 subgoal):
 1. \<And>x. x \<in> saturate \<Longrightarrow> x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
using rl
[PROOF STATE]
proof (prove)
using this:
x \<in> saturate

goal (1 subgoal):
 1. x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
(p, q) \<in> saturate

goal (1 subgoal):
 1. (p, q) \<in> \<Delta>_trancl_set A B
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>as a. \<lbrakk>as \<rightarrow>\<^sub>h a \<in> \<Delta>_trancl_rules A B; \<And>x. x \<in> set as \<Longrightarrow> x \<in> saturate; \<And>x. x \<in> set as \<Longrightarrow> x \<in> \<Delta>_trancl_set A B\<rbrakk> \<Longrightarrow> a \<in> \<Delta>_trancl_set A B
[PROOF STEP]
case (infer as a)
[PROOF STATE]
proof (state)
this:
as \<rightarrow>\<^sub>h a \<in> \<Delta>_trancl_rules A B
?x \<in> set as \<Longrightarrow> ?x \<in> saturate
?x \<in> set as \<Longrightarrow> ?x \<in> \<Delta>_trancl_set A B

goal (1 subgoal):
 1. \<And>as a. \<lbrakk>as \<rightarrow>\<^sub>h a \<in> \<Delta>_trancl_rules A B; \<And>x. x \<in> set as \<Longrightarrow> x \<in> saturate; \<And>x. x \<in> set as \<Longrightarrow> x \<in> \<Delta>_trancl_set A B\<rbrakk> \<Longrightarrow> a \<in> \<Delta>_trancl_set A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
as \<rightarrow>\<^sub>h a \<in> \<Delta>_trancl_rules A B
?x \<in> set as \<Longrightarrow> ?x \<in> saturate
?x \<in> set as \<Longrightarrow> ?x \<in> \<Delta>_trancl_set A B
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
as \<rightarrow>\<^sub>h a \<in> \<Delta>_trancl_rules A B
?x \<in> set as \<Longrightarrow> ?x \<in> saturate
?x \<in> set as \<Longrightarrow> ?x \<in> \<Delta>_trancl_set A B

goal (1 subgoal):
 1. a \<in> \<Delta>_trancl_set A B
[PROOF STEP]
using \<Delta>_set_cong[of _ "map fst as" "fst a" A "map snd as" "snd a" B]
        \<Delta>_set_eps1[of _ "fst a" A "snd a" B] \<Delta>_set_eps2[of _ "snd a" B "fst a" A]
        \<Delta>_set_trans[of "fst a" "snd (hd as)" A B "snd a"]
[PROOF STATE]
proof (prove)
using this:
as \<rightarrow>\<^sub>h a \<in> \<Delta>_trancl_rules A B
?x \<in> set as \<Longrightarrow> ?x \<in> saturate
?x \<in> set as \<Longrightarrow> ?x \<in> \<Delta>_trancl_set A B
\<lbrakk>?f map fst as \<rightarrow> fst a |\<in>| rules A; ?f map snd as \<rightarrow> snd a |\<in>| rules B; length (map fst as) = length (map snd as); \<And>i. i < length (map snd as) \<Longrightarrow> (map fst as ! i, map snd as ! i) \<in> \<Delta>_trancl_set A B\<rbrakk> \<Longrightarrow> (fst a, snd a) \<in> \<Delta>_trancl_set A B
\<lbrakk>(?p, fst a) |\<in>| eps A; (?p, snd a) \<in> \<Delta>_trancl_set A B\<rbrakk> \<Longrightarrow> (fst a, snd a) \<in> \<Delta>_trancl_set A B
\<lbrakk>(?q, snd a) |\<in>| eps B; (fst a, ?q) \<in> \<Delta>_trancl_set A B\<rbrakk> \<Longrightarrow> (fst a, snd a) \<in> \<Delta>_trancl_set A B
\<lbrakk>(fst a, snd (hd as)) \<in> \<Delta>_trancl_set A B; (snd (hd as), snd a) \<in> \<Delta>_trancl_set A B\<rbrakk> \<Longrightarrow> (fst a, snd a) \<in> \<Delta>_trancl_set A B

goal (1 subgoal):
 1. a \<in> \<Delta>_trancl_set A B
[PROOF STEP]
by (auto simp: \<Delta>_trancl_rules_def \<Delta>\<^sub>\<epsilon>_rules_def)
[PROOF STATE]
proof (state)
this:
a \<in> \<Delta>_trancl_set A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> \<Delta>_trancl_set A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<Delta>_Atr_infer1:
  "infer1 pq X = {(p, snd pq) | p q. (p, q) \<in> X \<and> (q, fst pq) |\<in>| \<Delta>\<^sub>\<epsilon> B A} \<union>
   {(fst pq, v) | q r v. (snd pq, r) |\<in>| \<Delta>\<^sub>\<epsilon> B A \<and> (r, v) \<in> X} \<union>
   {(fst pq, snd pq) | q . (snd pq, fst pq) |\<in>| \<Delta>\<^sub>\<epsilon> B A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infer1 pq X = {uu_. \<exists>p q. uu_ = (p, snd pq) \<and> (p, q) \<in> X \<and> (q, fst pq) |\<in>| \<Delta>\<^sub>\<epsilon> B A} \<union> {uu_. \<exists>q r v. uu_ = (fst pq, v) \<and> (snd pq, r) |\<in>| \<Delta>\<^sub>\<epsilon> B A \<and> (r, v) \<in> X} \<union> {uu_. \<exists>q. uu_ = (fst pq, snd pq) \<and> (snd pq, fst pq) |\<in>| \<Delta>\<^sub>\<epsilon> B A}
[PROOF STEP]
unfolding \<Delta>_Atr_rules_def horn_infer1_union
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horn.infer1 {[] \<rightarrow>\<^sub>h (p, q) |p q. (p, q) |\<in>| Q} pq X \<union> horn.infer1 {[(p, q), (r, v)] \<rightarrow>\<^sub>h (p, v) |p q r v. (q, r) |\<in>| \<Delta>\<^sub>\<epsilon> B A} pq X = {uu_. \<exists>p q. uu_ = (p, snd pq) \<and> (p, q) \<in> X \<and> (q, fst pq) |\<in>| \<Delta>\<^sub>\<epsilon> B A} \<union> {uu_. \<exists>q r v. uu_ = (fst pq, v) \<and> (snd pq, r) |\<in>| \<Delta>\<^sub>\<epsilon> B A \<and> (r, v) \<in> X} \<union> {uu_. \<exists>q. uu_ = (fst pq, snd pq) \<and> (snd pq, fst pq) |\<in>| \<Delta>\<^sub>\<epsilon> B A}
[PROOF STEP]
by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+


[STATEMENT]
lemma SN_Ret: "SN u \<Longrightarrow> SN [u]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SN u \<Longrightarrow> SN [u]
[PROOF STEP]
by(induct rule:SN.induct) (metis SN.intros red_Ret)


[STATEMENT]
lemma gen_boolean_algebra_subalgebra:
  assumes "Xs \<subseteq> gen_boolean_algebra S B"
  shows "gen_boolean_algebra S Xs \<subseteq> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_boolean_algebra S Xs \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> gen_boolean_algebra S Xs \<Longrightarrow> x \<in> gen_boolean_algebra S B
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> gen_boolean_algebra S Xs \<Longrightarrow> x \<in> gen_boolean_algebra S B
[PROOF STEP]
assume A: "x \<in> gen_boolean_algebra S Xs"
[PROOF STATE]
proof (state)
this:
x \<in> gen_boolean_algebra S Xs

goal (1 subgoal):
 1. \<And>x. x \<in> gen_boolean_algebra S Xs \<Longrightarrow> x \<in> gen_boolean_algebra S B
[PROOF STEP]
show "x \<in> gen_boolean_algebra S B "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> gen_boolean_algebra S B
[PROOF STEP]
apply(rule gen_boolean_algebra.induct[of x S Xs])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. x \<in> gen_boolean_algebra S Xs
 2. S \<in> gen_boolean_algebra S B
 3. \<And>A. A \<in> Xs \<Longrightarrow> A \<inter> S \<in> gen_boolean_algebra S B
 4. \<And>A C. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B; C \<in> gen_boolean_algebra S Xs; C \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> A \<union> C \<in> gen_boolean_algebra S B
 5. \<And>A. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> S - A \<in> gen_boolean_algebra S B
[PROOF STEP]
apply (simp add: A; fail)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. S \<in> gen_boolean_algebra S B
 2. \<And>A. A \<in> Xs \<Longrightarrow> A \<inter> S \<in> gen_boolean_algebra S B
 3. \<And>A C. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B; C \<in> gen_boolean_algebra S Xs; C \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> A \<union> C \<in> gen_boolean_algebra S B
 4. \<And>A. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> S - A \<in> gen_boolean_algebra S B
[PROOF STEP]
apply (simp add: gen_boolean_algebra.universe; fail)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A. A \<in> Xs \<Longrightarrow> A \<inter> S \<in> gen_boolean_algebra S B
 2. \<And>A C. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B; C \<in> gen_boolean_algebra S Xs; C \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> A \<union> C \<in> gen_boolean_algebra S B
 3. \<And>A. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> S - A \<in> gen_boolean_algebra S B
[PROOF STEP]
using assms gen_boolean_algebra.universe gen_boolean_algebra_intersect
[PROOF STATE]
proof (prove)
using this:
Xs \<subseteq> gen_boolean_algebra S B
?S \<in> gen_boolean_algebra ?S ?B
\<lbrakk>?A \<in> gen_boolean_algebra ?S ?B; ?C \<in> gen_boolean_algebra ?S ?B\<rbrakk> \<Longrightarrow> ?A \<inter> ?C \<in> gen_boolean_algebra ?S ?B

goal (3 subgoals):
 1. \<And>A. A \<in> Xs \<Longrightarrow> A \<inter> S \<in> gen_boolean_algebra S B
 2. \<And>A C. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B; C \<in> gen_boolean_algebra S Xs; C \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> A \<union> C \<in> gen_boolean_algebra S B
 3. \<And>A. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> S - A \<in> gen_boolean_algebra S B
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A C. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B; C \<in> gen_boolean_algebra S Xs; C \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> A \<union> C \<in> gen_boolean_algebra S B
 2. \<And>A. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> S - A \<in> gen_boolean_algebra S B
[PROOF STEP]
apply (simp add: gen_boolean_algebra.union; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A. \<lbrakk>A \<in> gen_boolean_algebra S Xs; A \<in> gen_boolean_algebra S B\<rbrakk> \<Longrightarrow> S - A \<in> gen_boolean_algebra S B
[PROOF STEP]
by (simp add: gen_boolean_algebra.complement)
[PROOF STATE]
proof (state)
this:
x \<in> gen_boolean_algebra S B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rec_disjointify_in_gen_boolean_algebra:
  assumes "f ` {..<m} \<subseteq> gen_boolean_algebra S B"
  shows  "rec_disjointify m f \<subseteq> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_disjointify m f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rec_disjointify m f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
have "\<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
show "k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
apply(induction k)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> m \<longrightarrow> rec_disjointify 0 f \<subseteq> gen_boolean_algebra S B
 2. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B \<Longrightarrow> Suc k \<le> m \<longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
unfolding rec_disjointify.simps(1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> m \<longrightarrow> {} \<subseteq> gen_boolean_algebra S B
 2. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B \<Longrightarrow> Suc k \<le> m \<longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f ` {..<m} \<subseteq> gen_boolean_algebra S B

goal (2 subgoals):
 1. 0 \<le> m \<longrightarrow> {} \<subseteq> gen_boolean_algebra S B
 2. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B \<Longrightarrow> Suc k \<le> m \<longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B \<Longrightarrow> Suc k \<le> m \<longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B; Suc k \<le> m\<rbrakk> \<Longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B; Suc k \<le> m\<rbrakk> \<Longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
assume IH: " k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B"
                 "Suc k \<le> m"
[PROOF STATE]
proof (state)
this:
k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
Suc k \<le> m

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B; Suc k \<le> m\<rbrakk> \<Longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
Suc k \<le> m
[PROOF STEP]
have 0: "rec_disjointify k f \<subseteq> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
using this:
k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B
Suc k \<le> m

goal (1 subgoal):
 1. rec_disjointify k f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
by (simp add: IH(2))
[PROOF STATE]
proof (state)
this:
rec_disjointify k f \<subseteq> gen_boolean_algebra S B

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B; Suc k \<le> m\<rbrakk> \<Longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
have 1: "finite (rec_disjointify k f )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (rec_disjointify k f)
[PROOF STEP]
using rec_disjointify_finite
[PROOF STATE]
proof (prove)
using this:
finite (rec_disjointify ?m ?f)

goal (1 subgoal):
 1. finite (rec_disjointify k f)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (rec_disjointify k f)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B; Suc k \<le> m\<rbrakk> \<Longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
have 2: "f k \<in> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f k \<in> gen_boolean_algebra S B
[PROOF STEP]
using IH(2) assms
[PROOF STATE]
proof (prove)
using this:
Suc k \<le> m
f ` {..<m} \<subseteq> gen_boolean_algebra S B

goal (1 subgoal):
 1. f k \<in> gen_boolean_algebra S B
[PROOF STEP]
by (simp add: image_subset_iff)
[PROOF STATE]
proof (state)
this:
f k \<in> gen_boolean_algebra S B

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B; Suc k \<le> m\<rbrakk> \<Longrightarrow> rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
show "rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
using 0 1 2
[PROOF STATE]
proof (prove)
using this:
rec_disjointify k f \<subseteq> gen_boolean_algebra S B
finite (rec_disjointify k f)
f k \<in> gen_boolean_algebra S B

goal (1 subgoal):
 1. rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
unfolding rec_disjointify.simps
[PROOF STATE]
proof (prove)
using this:
rec_disjointify k f \<subseteq> gen_boolean_algebra S B
finite (rec_disjointify k f)
f k \<in> gen_boolean_algebra S B

goal (1 subgoal):
 1. insert (f k - \<Union> (rec_disjointify k f)) (rec_disjointify k f) \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
by (simp add: gen_boolean_algebra_diff gen_boolean_algebra_finite_union subset_iff)
[PROOF STATE]
proof (state)
this:
rec_disjointify (Suc k) f \<subseteq> gen_boolean_algebra S B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k \<le> m \<longrightarrow> rec_disjointify k f \<subseteq> gen_boolean_algebra S B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?k \<le> m \<longrightarrow> rec_disjointify ?k f \<subseteq> gen_boolean_algebra S B

goal (1 subgoal):
 1. rec_disjointify m f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?k \<le> m \<longrightarrow> rec_disjointify ?k f \<subseteq> gen_boolean_algebra S B

goal (1 subgoal):
 1. rec_disjointify m f \<subseteq> gen_boolean_algebra S B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rec_disjointify m f \<subseteq> gen_boolean_algebra S B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fmap_maybe_simps [simp]:
  "fmap\<cdot>f\<cdot>(\<bottom>::'a\<cdot>maybe) = \<bottom>"
  "fmap\<cdot>f\<cdot>Nothing = Nothing"
  "fmap\<cdot>f\<cdot>(Just\<cdot>x) = Just\<cdot>(f\<cdot>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap\<cdot>f\<cdot>\<bottom> = \<bottom> &&& fmap\<cdot>f\<cdot>Nothing = Nothing &&& fmap\<cdot>f\<cdot>(Just\<cdot>x) = Just\<cdot>(f\<cdot>x)
[PROOF STEP]
unfolding fmap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>maybe \<rightarrow> udom\<cdot>maybe, ('a \<rightarrow> 'b) \<rightarrow> 'a\<cdot>maybe \<rightarrow> 'b\<cdot>maybe)\<cdot>fmapU\<cdot>f\<cdot>\<bottom> = \<bottom> &&& COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>maybe \<rightarrow> udom\<cdot>maybe, ('a \<rightarrow> 'b) \<rightarrow> 'a\<cdot>maybe \<rightarrow> 'b\<cdot>maybe)\<cdot>fmapU\<cdot>f\<cdot>Nothing = Nothing &&& COERCE((udom \<rightarrow> udom) \<rightarrow> udom\<cdot>maybe \<rightarrow> udom\<cdot>maybe, ('a \<rightarrow> 'b) \<rightarrow> 'a\<cdot>maybe \<rightarrow> 'b\<cdot>maybe)\<cdot>fmapU\<cdot>f\<cdot>(Just\<cdot>x) = Just\<cdot>(f\<cdot>x)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma new_element_no_shadow_root:
  "h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr \<Longrightarrow> h \<turnstile> new_element \<rightarrow>\<^sub>h h'
   \<Longrightarrow> h' \<turnstile> get_shadow_root new_element_ptr \<rightarrow>\<^sub>r None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<turnstile> new_element \<rightarrow>\<^sub>r new_element_ptr; h \<turnstile> new_element \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h' \<turnstile> get_shadow_root new_element_ptr \<rightarrow>\<^sub>r None
[PROOF STEP]
by(simp add: get_shadow_root_def new_element_shadow_root_opt)


[STATEMENT]
lemma get_shadow_root_new_shadow_root:
  "h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr \<Longrightarrow> h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'
     \<Longrightarrow> r \<in> get_shadow_root_locs ptr' \<Longrightarrow> r h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>r new_shadow_root_ptr; h \<turnstile> new\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M \<rightarrow>\<^sub>h h'; r \<in> get_shadow_root_locs ptr'\<rbrakk> \<Longrightarrow> r h h'
[PROOF STEP]
by (auto simp add: get_shadow_root_locs_def new_shadow_root_get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t new_shadow_root_get_M\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t
      split: prod.splits if_splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)


[STATEMENT]
lemma insert_before_wf2_is_l_insert_before_wf2 [instances]:
  "l_insert_before_wf2 ShadowRootClass.type_wf ShadowRootClass.known_ptr ShadowRootClass.known_ptrs
Shadow_DOM.insert_before
     Shadow_DOM.heap_is_wellformed"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_insert_before_wf2 ShadowRootClass.type_wf ShadowRootClass.known_ptr ShadowRootClass.known_ptrs Shadow_DOM.insert_before Shadow_DOM.heap_is_wellformed
[PROOF STEP]
apply(auto simp add: l_insert_before_wf2_def l_insert_before_wf2_axioms_def instances)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>h ptr child ref h'. \<lbrakk>Shadow_DOM.heap_is_wellformed h; ShadowRootClass.type_wf h; ShadowRootClass.known_ptrs h; h \<turnstile> Shadow_DOM.insert_before ptr child ref \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ShadowRootClass.type_wf h'
 2. \<And>h ptr child ref h'. \<lbrakk>Shadow_DOM.heap_is_wellformed h; ShadowRootClass.type_wf h; ShadowRootClass.known_ptrs h; h \<turnstile> Shadow_DOM.insert_before ptr child ref \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ShadowRootClass.known_ptrs h'
 3. \<And>h ptr child ref h'. \<lbrakk>ShadowRootClass.type_wf h; ShadowRootClass.known_ptrs h; Shadow_DOM.heap_is_wellformed h; h \<turnstile> Shadow_DOM.insert_before ptr child ref \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> Shadow_DOM.heap_is_wellformed h'
[PROOF STEP]
using insert_before_child_preserves
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Shadow_DOM.heap_is_wellformed ?h; ShadowRootClass.type_wf ?h; ShadowRootClass.known_ptrs ?h; ?h \<turnstile> Shadow_DOM.insert_before ?ptr ?node ?child \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> ShadowRootClass.type_wf ?h'
\<lbrakk>Shadow_DOM.heap_is_wellformed ?h; ShadowRootClass.type_wf ?h; ShadowRootClass.known_ptrs ?h; ?h \<turnstile> Shadow_DOM.insert_before ?ptr ?node ?child \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> ShadowRootClass.known_ptrs ?h'
\<lbrakk>Shadow_DOM.heap_is_wellformed ?h; ShadowRootClass.type_wf ?h; ShadowRootClass.known_ptrs ?h; ?h \<turnstile> Shadow_DOM.insert_before ?ptr ?node ?child \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> Shadow_DOM.heap_is_wellformed ?h'

goal (3 subgoals):
 1. \<And>h ptr child ref h'. \<lbrakk>Shadow_DOM.heap_is_wellformed h; ShadowRootClass.type_wf h; ShadowRootClass.known_ptrs h; h \<turnstile> Shadow_DOM.insert_before ptr child ref \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ShadowRootClass.type_wf h'
 2. \<And>h ptr child ref h'. \<lbrakk>Shadow_DOM.heap_is_wellformed h; ShadowRootClass.type_wf h; ShadowRootClass.known_ptrs h; h \<turnstile> Shadow_DOM.insert_before ptr child ref \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ShadowRootClass.known_ptrs h'
 3. \<And>h ptr child ref h'. \<lbrakk>ShadowRootClass.type_wf h; ShadowRootClass.known_ptrs h; Shadow_DOM.heap_is_wellformed h; h \<turnstile> Shadow_DOM.insert_before ptr child ref \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> Shadow_DOM.heap_is_wellformed h'
[PROOF STEP]
apply(fast, fast, fast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_to_list_last:
  assumes "card S > 0"
  shows "Max S = last (set_to_list S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max S = last (sorted_list_of_set S)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Max S = last (sorted_list_of_set S)
[PROOF STEP]
have 0: "set (set_to_list S) = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (sorted_list_of_set S) = S
[PROOF STEP]
using assms card_ge_0_finite set_sorted_list_of_set
[PROOF STATE]
proof (prove)
using this:
0 < card S
0 < card ?A \<Longrightarrow> finite ?A
finite ?A \<Longrightarrow> set (sorted_list_of_set ?A) = ?A

goal (1 subgoal):
 1. set (sorted_list_of_set S) = S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (sorted_list_of_set S) = S

goal (1 subgoal):
 1. Max S = last (sorted_list_of_set S)
[PROOF STEP]
have 1: "sorted (set_to_list S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted (sorted_list_of_set S)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted (sorted_list_of_set S)

goal (1 subgoal):
 1. Max S = last (sorted_list_of_set S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max S = last (sorted_list_of_set S)
[PROOF STEP]
apply(rule Max_eqI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite S
 2. \<And>y. y \<in> S \<Longrightarrow> y \<le> last (sorted_list_of_set S)
 3. last (sorted_list_of_set S) \<in> S
[PROOF STEP]
using assms card_ge_0_finite
[PROOF STATE]
proof (prove)
using this:
0 < card S
0 < card ?A \<Longrightarrow> finite ?A

goal (3 subgoals):
 1. finite S
 2. \<And>y. y \<in> S \<Longrightarrow> y \<le> last (sorted_list_of_set S)
 3. last (sorted_list_of_set S) \<in> S
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. y \<in> S \<Longrightarrow> y \<le> last (sorted_list_of_set S)
 2. last (sorted_list_of_set S) \<in> S
[PROOF STEP]
apply (smt "0" "1" Suc_diff_1 in_set_conv_nth last_conv_nth le_simps(2) length_greater_0_conv
        less_or_eq_imp_le nat_neq_iff neq0_conv not_less_eq sorted_iff_nth_mono_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (sorted_list_of_set S) \<in> S
[PROOF STEP]
by (metis "0" assms card.empty empty_set last_in_set less_numeral_extra(3))
[PROOF STATE]
proof (state)
this:
Max S = last (sorted_list_of_set S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wellformed_items_Scan:
  "wellformed_items I \<Longrightarrow> T \<subseteq> \<X> k \<Longrightarrow> wellformed_items (Scan T k I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_items I; T \<subseteq> \<X> k\<rbrakk> \<Longrightarrow> wellformed_items (Scan T k I)
[PROOF STEP]
apply (auto simp add: wellformed_items_def wellformed_item_def Scan_def bin_def \<X>_length_bound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa t c. \<lbrakk>\<forall>x\<in>I. item_rule x \<in> \<RR> \<and> item_origin x \<le> item_end x \<and> item_end x \<le> length Doc \<and> item_dot x \<le> length (item_rhs x); T \<subseteq> \<X> (item_end xa); xa \<in> I; k = item_end xa; (t, c) \<in> T; next_symbol xa = Some t\<rbrakk> \<Longrightarrow> Suc (item_dot xa) \<le> length (item_rhs xa)
[PROOF STEP]
using is_complete_def next_symbol_not_complete not_less_eq_eq
[PROOF STATE]
proof (prove)
using this:
is_complete ?x = (length (item_rhs ?x) \<le> item_dot ?x)
next_symbol ?x = Some ?t \<Longrightarrow> \<not> is_complete ?x
(\<not> ?m \<le> ?n) = (Suc ?n \<le> ?m)

goal (1 subgoal):
 1. \<And>xa t c. \<lbrakk>\<forall>x\<in>I. item_rule x \<in> \<RR> \<and> item_origin x \<le> item_end x \<and> item_end x \<le> length Doc \<and> item_dot x \<le> length (item_rhs x); T \<subseteq> \<X> (item_end xa); xa \<in> I; k = item_end xa; (t, c) \<in> T; next_symbol xa = Some t\<rbrakk> \<Longrightarrow> Suc (item_dot xa) \<le> length (item_rhs xa)
[PROOF STEP]
by blast


[STATEMENT]
lemma obj_fields_marked_eq_imp:
  "eq_imp (\<lambda>r'. gc_field_set \<^bold>\<otimes> gc_tmp_ref \<^bold>\<otimes> (\<lambda>s. map_option obj_fields (sys_heap s r')) \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')) \<^bold>\<otimes> sys_fM \<^bold>\<otimes> tso_pending_mutate gc)
          obj_fields_marked"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (gc_field_set s, gc_tmp_ref s, map_option obj_fields (sys_heap s r'), map_option obj_mark (sys_heap s r'), sys_fM s, filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s))) obj_fields_marked
[PROOF STEP]
unfolding eq_imp_def obj_fields_marked_def obj_at_field_on_heap_def obj_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (gc_field_set s, gc_tmp_ref s, map_option obj_fields (sys_heap s x), map_option obj_mark (sys_heap s x), sys_fM s, filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s)) = (gc_field_set s', gc_tmp_ref s', map_option obj_fields (sys_heap s' x), map_option obj_mark (sys_heap s' x), sys_fM s', filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'))) \<longrightarrow> (\<forall>x. x \<in> (- gc_field_set) s \<longrightarrow> (case map_option obj_fields (sys_heap s (gc_tmp_ref s)) of None \<Rightarrow> False | Some fs \<Rightarrow> case fs x of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s)) = (\<forall>x. x \<in> (- gc_field_set) s' \<longrightarrow> (case map_option obj_fields (sys_heap s' (gc_tmp_ref s')) of None \<Rightarrow> False | Some fs \<Rightarrow> case fs x of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s' r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s'))
[PROOF STEP]
apply (clarsimp simp: all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (\<forall>x. x \<notin> gc_field_set s' \<longrightarrow> (case sys_heap s' (gc_tmp_ref s') of None \<Rightarrow> False | Some xa \<Rightarrow> ((\<lambda>fs. case fs x of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s) \<circ> obj_fields) xa)) = (\<forall>x. x \<notin> gc_field_set s' \<longrightarrow> (case sys_heap s' (gc_tmp_ref s') of None \<Rightarrow> False | Some xa \<Rightarrow> ((\<lambda>fs. case fs x of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s' r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s') \<circ> obj_fields) xa))
[PROOF STEP]
apply (rule iffI; clarsimp split: option.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (sys_heap s' (gc_tmp_ref s') = None \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2 x2a. (sys_heap s' x2a = None \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2b. sys_heap s' x2a = Some x2b \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<notin> gc_field_set s' \<longrightarrow> obj_mark x2b = sys_fM s'))
 2. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (sys_heap s' (gc_tmp_ref s') = None \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2 x2a. (sys_heap s x2a = None \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2b. sys_heap s x2a = Some x2b \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<notin> gc_field_set s' \<longrightarrow> obj_mark x2b = sys_fM s'))
[PROOF STEP]
apply (intro allI conjI impI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' (gc_tmp_ref s') = None\<rbrakk> \<Longrightarrow> x \<in> gc_field_set s'
 2. \<And>s s' x x2 x2a. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' x2a = None; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2\<rbrakk> \<Longrightarrow> x \<in> gc_field_set s'
 3. \<And>s s' x x2 x2a x2b. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' x2a = Some x2b; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2; x \<notin> gc_field_set s'\<rbrakk> \<Longrightarrow> obj_mark x2b = sys_fM s'
 4. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (sys_heap s' (gc_tmp_ref s') = None \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2 x2a. (sys_heap s x2a = None \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2b. sys_heap s x2a = Some x2b \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<notin> gc_field_set s' \<longrightarrow> obj_mark x2b = sys_fM s'))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' x x2 x2a. \<lbrakk>\<forall>x x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' x2a = None; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2\<rbrakk> \<Longrightarrow> x \<in> gc_field_set s'
 2. \<And>s s' x x2 x2a x2b. \<lbrakk>\<forall>x x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' x2a = Some x2b; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2; x \<notin> gc_field_set s'\<rbrakk> \<Longrightarrow> obj_mark x2b = sys_fM s'
 3. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (sys_heap s' (gc_tmp_ref s') = None \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2 x2a. (sys_heap s x2a = None \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2b. sys_heap s x2a = Some x2b \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<notin> gc_field_set s' \<longrightarrow> obj_mark x2b = sys_fM s'))
[PROOF STEP]
apply (metis (no_types, opaque_lifting) option.distinct(1) option.map_disc_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x x2 x2a x2b. \<lbrakk>\<forall>x x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' x2a = Some x2b; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2; x \<notin> gc_field_set s'\<rbrakk> \<Longrightarrow> obj_mark x2b = sys_fM s'
 2. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (sys_heap s' (gc_tmp_ref s') = None \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2 x2a. (sys_heap s x2a = None \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2b. sys_heap s x2a = Some x2b \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<notin> gc_field_set s' \<longrightarrow> obj_mark x2b = sys_fM s'))
[PROOF STEP]
apply (metis (no_types, lifting) option.distinct(1) option.map_sel option.sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s')\<rbrakk> \<Longrightarrow> (sys_heap s' (gc_tmp_ref s') = None \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2 x2a. (sys_heap s x2a = None \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<in> gc_field_set s') \<and> (\<forall>x2b. sys_heap s x2a = Some x2b \<longrightarrow> obj_fields x2 x = Some x2a \<longrightarrow> sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> x \<notin> gc_field_set s' \<longrightarrow> obj_mark x2b = sys_fM s'))
[PROOF STEP]
apply (intro allI conjI impI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' x. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s' (gc_tmp_ref s') = None\<rbrakk> \<Longrightarrow> x \<in> gc_field_set s'
 2. \<And>s s' x x2 x2a. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s x2a = None; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2\<rbrakk> \<Longrightarrow> x \<in> gc_field_set s'
 3. \<And>s s' x x2 x2a x2b. \<lbrakk>\<forall>x. ((\<exists>y. sys_heap s' (gc_tmp_ref s') = Some y) \<or> x \<in> gc_field_set s') \<and> (\<forall>x2. sys_heap s' (gc_tmp_ref s') = Some x2 \<longrightarrow> (\<forall>x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')))); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s x2a = Some x2b; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2; x \<notin> gc_field_set s'\<rbrakk> \<Longrightarrow> obj_mark x2b = sys_fM s'
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x x2 x2a. \<lbrakk>\<forall>x x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s x2a = None; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2\<rbrakk> \<Longrightarrow> x \<in> gc_field_set s'
 2. \<And>s s' x x2 x2a x2b. \<lbrakk>\<forall>x x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s x2a = Some x2b; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2; x \<notin> gc_field_set s'\<rbrakk> \<Longrightarrow> obj_mark x2b = sys_fM s'
[PROOF STEP]
apply (metis (no_types, opaque_lifting) option.distinct(1) option.map_disc_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x x2 x2a x2b. \<lbrakk>\<forall>x x2a. (obj_fields x2 x = Some x2a \<longrightarrow> (\<exists>y. sys_heap s' x2a = Some y) \<or> x \<in> gc_field_set s') \<and> (obj_fields x2 x = Some x2a \<longrightarrow> (\<forall>x2. sys_heap s' x2a = Some x2 \<longrightarrow> x \<in> gc_field_set s' \<or> obj_mark x2 = sys_fM s')); gc_field_set s = gc_field_set s'; gc_tmp_ref s = gc_tmp_ref s'; \<forall>x. map_option obj_fields (sys_heap s x) = map_option obj_fields (sys_heap s' x); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers gc s'); sys_heap s x2a = Some x2b; obj_fields x2 x = Some x2a; sys_heap s' (gc_tmp_ref s') = Some x2; x \<notin> gc_field_set s'\<rbrakk> \<Longrightarrow> obj_mark x2b = sys_fM s'
[PROOF STEP]
apply (metis (no_types, lifting) option.distinct(1) option.map_sel option.sel)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mult_lc_monic:
  assumes "p \<noteq> 0"
  shows "monom_mult (lc p) 0 (monic p) = p" (is "?q = p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (lc p) (0::'a) (monic p) = p
[PROOF STEP]
proof (rule poly_mapping_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
[PROOF STEP]
have "lc p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. lc p \<noteq> (0::'b)
[PROOF STEP]
by (rule lc_not_0)
[PROOF STATE]
proof (state)
this:
lc p \<noteq> (0::'b)

goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
have "lookup ?q (0 \<oplus> v) = (lc p) * (lookup (monic p) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (monom_mult (lc p) (0::'a) (monic p)) ((0::'a) \<oplus> v) = lc p * lookup (monic p) v
[PROOF STEP]
by (rule lookup_monom_mult_plus)
[PROOF STATE]
proof (state)
this:
lookup (monom_mult (lc p) (0::'a) (monic p)) ((0::'a) \<oplus> v) = lc p * lookup (monic p) v

goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (monom_mult (lc p) (0::'a) (monic p)) ((0::'a) \<oplus> v) = lc p * lookup (monic p) v

goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
have "... = (lc p) * ((lookup p v) / lc p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lc p * lookup (monic p) v = lc p * (lookup p v / lc p)
[PROOF STEP]
by (simp add: lookup_monic)
[PROOF STATE]
proof (state)
this:
lc p * lookup (monic p) v = lc p * (lookup p v / lc p)

goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lc p * lookup (monic p) v = lc p * (lookup p v / lc p)

goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
have "... = lookup p v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lc p * (lookup p v / lc p) = lookup p v
[PROOF STEP]
using \<open>lc p \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
lc p \<noteq> (0::'b)

goal (1 subgoal):
 1. lc p * (lookup p v / lc p) = lookup p v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lc p * (lookup p v / lc p) = lookup p v

goal (1 subgoal):
 1. \<And>k. lookup (monom_mult (lc p) (0::'a) (monic p)) k = lookup p k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (monom_mult (lc p) (0::'a) (monic p)) ((0::'a) \<oplus> v) = lookup p v
[PROOF STEP]
show "lookup ?q v = lookup p v"
[PROOF STATE]
proof (prove)
using this:
lookup (monom_mult (lc p) (0::'a) (monic p)) ((0::'a) \<oplus> v) = lookup p v

goal (1 subgoal):
 1. lookup (monom_mult (lc p) (0::'a) (monic p)) v = lookup p v
[PROOF STEP]
by (simp add: term_simps)
[PROOF STATE]
proof (state)
this:
lookup (monom_mult (lc p) (0::'a) (monic p)) v = lookup p v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma apply_ncrit_superset:
  "set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))" (is "?l \<subseteq> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
have "?l = set (rev (apply_ncrit crit data gs bs hs ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) = set (rev (apply_ncrit crit data gs bs hs ps))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (apply_ncrit crit data gs bs hs ps) = set (rev (apply_ncrit crit data gs bs hs ps))

goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (apply_ncrit crit data gs bs hs ps) = set (rev (apply_ncrit crit data gs bs hs ps))

goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
have "... \<subseteq> set (fold (\<lambda>(ic, q_in_bs, p, q) ps'.
                          if \<not> ic \<and> crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps')
                  qs (rev (apply_ncrit crit data gs bs hs ps)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rev (apply_ncrit crit data gs bs hs ps)) \<subseteq> set (fold (\<lambda>(ic, q_in_bs, p, q) ps'. if \<not> ic \<and> crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') qs (rev (apply_ncrit crit data gs bs hs ps)))
[PROOF STEP]
by (fact fold_superset)
[PROOF STATE]
proof (state)
this:
set (rev (apply_ncrit crit data gs bs hs ps)) \<subseteq> set (fold (\<lambda>(ic, q_in_bs, p, q) ps'. if \<not> ic \<and> crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') qs (rev (apply_ncrit crit data gs bs hs ps)))

goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (rev (apply_ncrit crit data gs bs hs ps)) \<subseteq> set (fold (\<lambda>(ic, q_in_bs, p, q) ps'. if \<not> ic \<and> crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') qs (rev (apply_ncrit crit data gs bs hs ps)))

goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
have "... = ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (fold (\<lambda>(ic, q_in_bs, p, q) ps'. if \<not> ic \<and> crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') qs (rev (apply_ncrit crit data gs bs hs ps))) = set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
by (simp add: apply_ncrit_append)
[PROOF STATE]
proof (state)
this:
set (fold (\<lambda>(ic, q_in_bs, p, q) ps'. if \<not> ic \<and> crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') qs (rev (apply_ncrit crit data gs bs hs ps))) = set (apply_ncrit crit data gs bs hs (ps @ qs))

goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))

goal (1 subgoal):
 1. set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (apply_ncrit crit data gs bs hs ps) \<subseteq> set (apply_ncrit crit data gs bs hs (ps @ qs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nextVertex_in_face'[simp]:
  "vertices f \<noteq> [] \<Longrightarrow> f \<bullet> v \<in> \<V> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertices f \<noteq> [] \<Longrightarrow> f \<bullet> v \<in> \<V> f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vertices f \<noteq> [] \<Longrightarrow> f \<bullet> v \<in> \<V> f
[PROOF STEP]
assume f: "vertices f \<noteq> []"
[PROOF STATE]
proof (state)
this:
vertices f \<noteq> []

goal (1 subgoal):
 1. vertices f \<noteq> [] \<Longrightarrow> f \<bullet> v \<in> \<V> f
[PROOF STEP]
define c where "c = nextElem (vertices f) (hd (vertices f)) v"
[PROOF STATE]
proof (state)
this:
c = nextElem (vertices f) (hd (vertices f)) v

goal (1 subgoal):
 1. vertices f \<noteq> [] \<Longrightarrow> f \<bullet> v \<in> \<V> f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = nextElem (vertices f) (hd (vertices f)) v
[PROOF STEP]
have "nextElem (vertices f) (hd (vertices f)) v = c"
[PROOF STATE]
proof (prove)
using this:
c = nextElem (vertices f) (hd (vertices f)) v

goal (1 subgoal):
 1. nextElem (vertices f) (hd (vertices f)) v = c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nextElem (vertices f) (hd (vertices f)) v = c

goal (1 subgoal):
 1. vertices f \<noteq> [] \<Longrightarrow> f \<bullet> v \<in> \<V> f
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
vertices f \<noteq> []
nextElem (vertices f) (hd (vertices f)) v = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
vertices f \<noteq> []
nextElem (vertices f) (hd (vertices f)) v = c

goal (1 subgoal):
 1. f \<bullet> v \<in> \<V> f
[PROOF STEP]
apply (simp add: nextVertex_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vertices f \<noteq> []; nextElem (vertices f) (hd (vertices f)) v = c\<rbrakk> \<Longrightarrow> c \<in> \<V> f
[PROOF STEP]
apply (drule_tac nextElem_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vertices f \<noteq> []; v \<notin> \<V> f \<and> c = hd (vertices f) \<or> vertices f \<noteq> [] \<and> v = last (vertices f) \<and> c = hd (vertices f) \<and> v \<notin> set (butlast (vertices f)) \<or> (\<exists>us vs. vertices f = us @ [v, c] @ vs \<and> v \<notin> set us)\<rbrakk> \<Longrightarrow> c \<in> \<V> f
[PROOF STEP]
apply(fastforce simp:neq_Nil_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
f \<bullet> v \<in> \<V> f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WildStar1:
  "Wildcard (Star A B), \<Delta> \<turnstile> Star (Wildcard A) (Wildcard B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Wildcard (Star A B), \<Delta> \<turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
proof (rule entailsI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
fix \<sigma> s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
assume asm0: "\<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B)"
[PROOF STATE]
proof (state)
this:
\<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B)

goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B)
[PROOF STEP]
obtain p ab a b where "\<sigma> = p \<odot> ab" "Some ab = a \<oplus> b" "a, s, \<Delta> \<Turnstile> A" "b, s, \<Delta> \<Turnstile> B"
[PROOF STATE]
proof (prove)
using this:
\<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B)

goal (1 subgoal):
 1. (\<And>p ab a b. \<lbrakk>\<sigma> = p \<odot> ab; Some ab = a \<oplus> b; a, s, \<Delta> \<Turnstile> A; b, s, \<Delta> \<Turnstile> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> = p \<odot> ab
Some ab = a \<oplus> b
a, s, \<Delta> \<Turnstile> A
b, s, \<Delta> \<Turnstile> B

goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<sigma> = p \<odot> ab
Some ab = a \<oplus> b
a, s, \<Delta> \<Turnstile> A
b, s, \<Delta> \<Turnstile> B
[PROOF STEP]
have "Some \<sigma> = (p \<odot> a) \<oplus> (p \<odot> b)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> = p \<odot> ab
Some ab = a \<oplus> b
a, s, \<Delta> \<Turnstile> A
b, s, \<Delta> \<Turnstile> B

goal (1 subgoal):
 1. Some \<sigma> = p \<odot> a \<oplus> p \<odot> b
[PROOF STEP]
using plus_mult
[PROOF STATE]
proof (prove)
using this:
\<sigma> = p \<odot> ab
Some ab = a \<oplus> b
a, s, \<Delta> \<Turnstile> A
b, s, \<Delta> \<Turnstile> B
Some ?a = ?b \<oplus> ?c \<Longrightarrow> Some (?p \<odot> ?a) = ?p \<odot> ?b \<oplus> ?p \<odot> ?c

goal (1 subgoal):
 1. Some \<sigma> = p \<odot> a \<oplus> p \<odot> b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Some \<sigma> = p \<odot> a \<oplus> p \<odot> b

goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Wildcard (Star A B) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Some \<sigma> = p \<odot> a \<oplus> p \<odot> b
[PROOF STEP]
show "\<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)"
[PROOF STATE]
proof (prove)
using this:
Some \<sigma> = p \<odot> a \<oplus> p \<odot> b

goal (1 subgoal):
 1. \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
using \<open>a, s, \<Delta> \<Turnstile> A\<close> \<open>b, s, \<Delta> \<Turnstile> B\<close>
[PROOF STATE]
proof (prove)
using this:
Some \<sigma> = p \<odot> a \<oplus> p \<odot> b
a, s, \<Delta> \<Turnstile> A
b, s, \<Delta> \<Turnstile> B

goal (1 subgoal):
 1. \<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>, s, \<Delta> \<Turnstile> Star (Wildcard A) (Wildcard B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dot_forall1:
  "Mult p (Forall x A), \<Delta> \<turnstile> Forall x (Mult p A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mult p (Forall x A), \<Delta> \<turnstile> Forall x (Mult p A)
[PROOF STEP]
proof (rule entailsI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Forall x (Mult p A)
[PROOF STEP]
fix \<sigma> s \<Delta>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Forall x (Mult p A)
[PROOF STEP]
assume "\<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A)"
[PROOF STATE]
proof (state)
this:
\<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A)

goal (1 subgoal):
 1. \<And>\<sigma> s. \<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A) \<Longrightarrow> \<sigma>, s, \<Delta> \<Turnstile> Forall x (Mult p A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A)
[PROOF STEP]
show "\<sigma>, s, \<Delta> \<Turnstile> Forall x (Mult p A)"
[PROOF STATE]
proof (prove)
using this:
\<sigma>, s, \<Delta> \<Turnstile> Mult p (Forall x A)

goal (1 subgoal):
 1. \<sigma>, s, \<Delta> \<Turnstile> Forall x (Mult p A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma>, s, \<Delta> \<Turnstile> Forall x (Mult p A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adj_sum:"RSadj x y (\<nu>1 + \<nu>2) = (RSadj x y \<nu>1) + (RSadj x y \<nu>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RSadj x y (\<nu>1 + \<nu>2) = RSadj x y \<nu>1 + RSadj x y \<nu>2
[PROOF STEP]
unfolding RSadj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>z. (\<nu>1 + \<nu>2) $ swap x y z) = (\<chi>z. \<nu>1 $ swap x y z) + (\<chi>z. \<nu>2 $ swap x y z)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) = (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))
[PROOF STEP]
apply (rule vec_extensionality)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
[PROOF STEP]
subgoal for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
[PROOF STEP]
apply (cases "i = x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. i = x \<Longrightarrow> (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
 2. i \<noteq> x \<Longrightarrow> (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
[PROOF STEP]
apply (cases "i = y")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i = x; i = y\<rbrakk> \<Longrightarrow> (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
 2. \<lbrakk>i = x; i \<noteq> y\<rbrakk> \<Longrightarrow> (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
 3. i \<noteq> x \<Longrightarrow> (\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z) + \<nu>2 $ (if z = x then y else if z = y then x else z)) $ i = ((\<chi>z. \<nu>1 $ (if z = x then y else if z = y then x else z)) + (\<chi>z. \<nu>2 $ (if z = x then y else if z = y then x else z))) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pratt_triple_extend:
  assumes "prime q" "pratt_triple p a y"
          "p > 1" "x > 0" "x = q * y" "[a ^ ((p - 1) div q) \<noteq> 1] (mod p)"
  shows   "pratt_triple p a x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
have "prime_factors x = insert q (prime_factors y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors x = insert q (prime_factors y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime q
pratt_triple p a y
1 < p
0 < x
x = q * y
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. prime_factors x = insert q (prime_factors y)
[PROOF STEP]
by (simp add: prime_factors_product prime_prime_factors)
[PROOF STATE]
proof (state)
this:
prime_factors x = insert q (prime_factors y)

goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors x = insert q (prime_factors y)

goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
have "\<forall>r\<in>\<dots>. [a ^ ((p - 1) div r) \<noteq> 1] (mod p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>insert q (prime_factors y). [a ^ ((p - 1) div r) \<noteq> 1] (mod p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime q
pratt_triple p a y
1 < p
0 < x
x = q * y
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. \<forall>r\<in>insert q (prime_factors y). [a ^ ((p - 1) div r) \<noteq> 1] (mod p)
[PROOF STEP]
by (auto simp: pratt_triple_def)
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>insert q (prime_factors y). [a ^ ((p - 1) div r) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<forall>r\<in>#prime_factorization x. [a ^ ((p - 1) div r) \<noteq> 1] (mod p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>#prime_factorization x. [a ^ ((p - 1) div r) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>#prime_factorization x. [a ^ ((p - 1) div r) \<noteq> 1] (mod p)
prime q
pratt_triple p a y
1 < p
0 < x
x = q * y
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. pratt_triple p a x
[PROOF STEP]
unfolding pratt_triple_def
[PROOF STATE]
proof (prove)
using this:
\<forall>r\<in>#prime_factorization x. [a ^ ((p - 1) div r) \<noteq> 1] (mod p)
prime q
0 < y \<and> (\<forall>q\<in>#prime_factorization y. [a ^ ((p - 1) div q) \<noteq> 1] (mod p))
1 < p
0 < x
x = q * y
[a ^ ((p - 1) div q) \<noteq> 1] (mod p)

goal (1 subgoal):
 1. 0 < x \<and> (\<forall>q\<in>#prime_factorization x. [a ^ ((p - 1) div q) \<noteq> 1] (mod p))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pratt_triple p a x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_factors_list_prime:
  fixes n :: nat
  assumes "prime n"
  shows "\<exists> qs. prime_factors n = set qs \<and> prod_list qs = n \<and> length qs = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>qs. prime_factors n = set qs \<and> prod_list qs = n \<and> length qs = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime n

goal (1 subgoal):
 1. \<exists>qs. prime_factors n = set qs \<and> prod_list qs = n \<and> length qs = 1
[PROOF STEP]
by (auto simp add: prime_factorization_prime intro: exI [of _ "[n]"])