[STATEMENT]
lemma RID\<^sub>L_finite_invariant:
  assumes
    step: "revision_step r s s'" and
    fin: "finite (LID\<^sub>G s)"
shows
    "finite (LID\<^sub>G s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (LID\<^sub>G s')
[PROOF STEP]
proof (use step in \<open>cases rule: revision_stepE\<close>)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
[PROOF STEP]
case (join \<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v)
[PROOF STATE]
proof (state)
this:
s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None)
s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))])
s r' = Some (\<sigma>', \<tau>', VE v)

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
[PROOF STEP]
hence "r \<noteq> r'"
[PROOF STATE]
proof (prove)
using this:
s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None)
s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))])
s r' = Some (\<sigma>', \<tau>', VE v)

goal (1 subgoal):
 1. r \<noteq> r'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<noteq> r'

goal (9 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r' \<sigma>' \<tau>' v. \<lbrakk>s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None); s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = Some (\<sigma>', \<tau>', VE v)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 9. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<noteq> r'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<noteq> r'

goal (1 subgoal):
 1. finite (LID\<^sub>G s')
[PROOF STEP]
using join assms
[PROOF STATE]
proof (prove)
using this:
r \<noteq> r'
s' = (s(r \<mapsto> (\<sigma>, \<tau>;;\<tau>', \<E> [VE (CV Unit)])))(r' := None)
s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))])
s r' = Some (\<sigma>', \<tau>', VE v)
revision_step r s s'
finite (LID\<^sub>G s)

goal (1 subgoal):
 1. finite (LID\<^sub>G s')
[PROOF STEP]
by (metis (mono_tags, lifting) ID_distr_global(2) ID_distr_local(1) fin finite_Un finite_combination(2) finite_occurrences_val_expr(4) finite_state_imp_restriction_finite(2) join local_state_of_finite_restricted_global_state_is_finite(2))
[PROOF STATE]
proof (state)
this:
finite (LID\<^sub>G s')

goal (8 subgoals):
 1. \<And>\<sigma> \<tau> \<E> x e v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [subst (VE v) x e])); s r = Some (\<sigma>, \<tau>, \<E> [Apply (VE (Lambda x e)) (VE v)])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 2. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e1])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV T)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 3. \<And>\<sigma> \<tau> \<E> e1 e2. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [e2])); s r = Some (\<sigma>, \<tau>, \<E> [Ite (VE (CV F)) e1 e2])\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 4. \<And>\<sigma> \<tau> \<E> v l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (Loc l)])); s r = Some (\<sigma>, \<tau>, \<E> [Ref (VE v)]); l \<notin> LID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 5. \<And>\<sigma> \<tau> \<E> l. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (the (if \<tau> l = None then \<sigma> l else \<tau> l))])); s r = Some (\<sigma>, \<tau>, \<E> [Read (VE (Loc l))]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 6. \<And>\<sigma> \<tau> \<E> l v. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>(l \<mapsto> v), \<E> [VE (CV Unit)])); s r = Some (\<sigma>, \<tau>, \<E> [Assign (VE (Loc l)) (VE v)]); l \<in> dom (\<sigma>;;\<tau>)\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 7. \<And>\<sigma> \<tau> \<E> e r'. \<lbrakk>s' = s(r \<mapsto> (\<sigma>, \<tau>, \<E> [VE (Rid r')]), r' \<mapsto> (\<sigma>;;\<tau>, \<epsilon>, e)); s r = Some (\<sigma>, \<tau>, \<E> [Rfork e]); r' \<notin> RID\<^sub>G s\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
 8. \<And>\<sigma> \<tau> \<E> r'. \<lbrakk>s' = \<epsilon>; s r = Some (\<sigma>, \<tau>, \<E> [Rjoin (VE (Rid r'))]); s r' = None\<rbrakk> \<Longrightarrow> finite (LID\<^sub>G s')
[PROOF STEP]
qed (use fin in \<open>auto simp add: ID_distr_global_conditional\<close>)


[STATEMENT]
lemma reachable_imp_identifiers_finite:
  assumes reach: "reachable s"
  shows
    "finite (RID\<^sub>G s)"
    "finite (LID\<^sub>G s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RID\<^sub>G s) &&& finite (LID\<^sub>G s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (RID\<^sub>G s)
 2. finite (LID\<^sub>G s)
[PROOF STEP]
from reach
[PROOF STATE]
proof (chain)
picking this:
reachable s
[PROOF STEP]
obtain e r where exec: "execution e (\<epsilon>(r \<mapsto> (\<epsilon>,\<epsilon>,e))) s"
[PROOF STATE]
proof (prove)
using this:
reachable s

goal (1 subgoal):
 1. (\<And>e r. execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reachable_def execution_def
[PROOF STATE]
proof (prove)
using this:
reachable s
reachable ?s \<equiv> \<exists>e s'. execution e s' ?s
execution ?e ?s ?s' \<equiv> (\<exists>r. ?s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, ?e)) \<and> program_expr ?e) \<and> ?s \<leadsto>\<^sup>* ?s'

goal (1 subgoal):
 1. (\<And>e r. execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) s

goal (2 subgoals):
 1. finite (RID\<^sub>G s)
 2. finite (LID\<^sub>G s)
[PROOF STEP]
hence prog_exp: "program_expr e"
[PROOF STATE]
proof (prove)
using this:
execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) s

goal (1 subgoal):
 1. program_expr e
[PROOF STEP]
by (meson execution_def)
[PROOF STATE]
proof (state)
this:
program_expr e

goal (2 subgoals):
 1. finite (RID\<^sub>G s)
 2. finite (LID\<^sub>G s)
[PROOF STEP]
obtain n where n_reachable: "(\<epsilon>(r \<mapsto> (\<epsilon>,\<epsilon>,e)), s) \<in> [\<leadsto>]^^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) s

goal (1 subgoal):
 1. (\<And>n. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson execution_def rtrancl_imp_relpow)
[PROOF STATE]
proof (state)
this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n

goal (2 subgoals):
 1. finite (RID\<^sub>G s)
 2. finite (LID\<^sub>G s)
[PROOF STEP]
hence "finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)"
[PROOF STATE]
proof (prove)
using this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
proof (induct n arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
hence s: "s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))"
[PROOF STATE]
proof (prove)
using this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0

goal (1 subgoal):
 1. s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
hence rid_dom: "dom s = {r}"
[PROOF STATE]
proof (prove)
using this:
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))

goal (1 subgoal):
 1. dom s = {r}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dom s = {r}

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
hence rid_ran: "\<Union> (RID\<^sub>L ` ran s) = {}"
[PROOF STATE]
proof (prove)
using this:
dom s = {r}

goal (1 subgoal):
 1. \<Union> (RID\<^sub>L ` ran s) = {}
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
dom s = {r}
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))

goal (1 subgoal):
 1. \<Union> (RID\<^sub>L ` ran s) = {}
[PROOF STEP]
by (auto simp add: prog_exp)
[PROOF STATE]
proof (state)
this:
\<Union> (RID\<^sub>L ` ran s) = {}

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
have rids: "RID\<^sub>G s = {r}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RID\<^sub>G s = {r}
[PROOF STEP]
by (unfold RID\<^sub>G_def, use rid_dom rid_ran in auto)
[PROOF STATE]
proof (state)
this:
RID\<^sub>G s = {r}

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
have lid_ran: "\<Union> (LID\<^sub>L ` ran s) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (LID\<^sub>L ` ran s) = {}
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
s = \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))

goal (1 subgoal):
 1. \<Union> (LID\<^sub>L ` ran s) = {}
[PROOF STEP]
by (auto simp add: prog_exp)
[PROOF STATE]
proof (state)
this:
\<Union> (LID\<^sub>L ` ran s) = {}

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
hence lids: "LID\<^sub>G s = {}"
[PROOF STATE]
proof (prove)
using this:
\<Union> (LID\<^sub>L ` ran s) = {}

goal (1 subgoal):
 1. LID\<^sub>G s = {}
[PROOF STEP]
by (unfold LID\<^sub>G_def, simp)
[PROOF STATE]
proof (state)
this:
LID\<^sub>G s = {}

goal (2 subgoals):
 1. \<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
 2. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>G s = {}

goal (1 subgoal):
 1. finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
using rids lids
[PROOF STATE]
proof (prove)
using this:
LID\<^sub>G s = {}
RID\<^sub>G s = {r}
LID\<^sub>G s = {}

goal (1 subgoal):
 1. finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), ?s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G ?s) \<and> finite (LID\<^sub>G ?s)
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), ?s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G ?s) \<and> finite (LID\<^sub>G ?s)
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n
[PROOF STEP]
obtain s' where
      n_steps: "(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s') \<in> [\<leadsto>]^^n" and
      step: "s' \<leadsto> s"
[PROOF STATE]
proof (prove)
using this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), ?s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G ?s) \<and> finite (LID\<^sub>G ?s)
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s') \<in> [\<leadsto>] ^^ n; s' \<leadsto> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson relpow_Suc_E)
[PROOF STATE]
proof (state)
this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s') \<in> [\<leadsto>] ^^ n
s' \<leadsto> s

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
have fin_rid: "finite (RID\<^sub>G s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (RID\<^sub>G s')
[PROOF STEP]
using Suc.hyps n_steps
[PROOF STATE]
proof (prove)
using this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), ?s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G ?s) \<and> finite (LID\<^sub>G ?s)
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s') \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. finite (RID\<^sub>G s')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s')

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
have fin_lid: "finite (LID\<^sub>G s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (LID\<^sub>G s')
[PROOF STEP]
using Suc.hyps n_steps
[PROOF STATE]
proof (prove)
using this:
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), ?s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G ?s) \<and> finite (LID\<^sub>G ?s)
(\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s') \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. finite (LID\<^sub>G s')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite (LID\<^sub>G s')

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>\<And>s. (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ n \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s); (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)), s) \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite (LID\<^sub>G s')

goal (1 subgoal):
 1. finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)
[PROOF STEP]
by (meson RID\<^sub>G_finite_invariant RID\<^sub>L_finite_invariant fin_rid local.step valid_stepE)
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)

goal (2 subgoals):
 1. finite (RID\<^sub>G s)
 2. finite (LID\<^sub>G s)
[PROOF STEP]
thus "finite (RID\<^sub>G s)" "finite (LID\<^sub>G s)"
[PROOF STATE]
proof (prove)
using this:
finite (RID\<^sub>G s) \<and> finite (LID\<^sub>G s)

goal (1 subgoal):
 1. finite (RID\<^sub>G s) &&& finite (LID\<^sub>G s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (RID\<^sub>G s)
finite (LID\<^sub>G s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_imp_identifiers_available:
  assumes
    "reachable (s :: ('r,'l,'v) global_state)"
  shows
    "infinite (UNIV :: 'r set) \<Longrightarrow> \<exists>r. r \<notin> RID\<^sub>G s"
    "infinite (UNIV :: 'l set) \<Longrightarrow> \<exists>l. l \<notin> LID\<^sub>G s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (infinite UNIV \<Longrightarrow> \<exists>r. r \<notin> RID\<^sub>G s) &&& (infinite UNIV \<Longrightarrow> \<exists>l. l \<notin> LID\<^sub>G s)
[PROOF STEP]
by (simp add: assms ex_new_if_finite reachable_imp_identifiers_finite)+


[STATEMENT]
lemma initial_state_reachable:
  assumes "program_expr e"
  shows "reachable (\<epsilon>(r \<mapsto> (\<epsilon>,\<epsilon>,e)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
have "initializes (\<epsilon>(r \<mapsto> (\<epsilon>,\<epsilon>,e))) e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ra. \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) = \<epsilon>(ra \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
program_expr e

goal (1 subgoal):
 1. \<exists>ra. \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) = \<epsilon>(ra \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ra. \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) = \<epsilon>(ra \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (1 subgoal):
 1. reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
hence "execution e (\<epsilon>(r \<mapsto> (\<epsilon>,\<epsilon>,e))) (\<epsilon>(r \<mapsto> (\<epsilon>,\<epsilon>,e)))"
[PROOF STATE]
proof (prove)
using this:
\<exists>ra. \<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)) = \<epsilon>(ra \<mapsto> (\<epsilon>, \<epsilon>, e)) \<and> program_expr e

goal (1 subgoal):
 1. execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
by (simp add: execution_def)
[PROOF STATE]
proof (state)
this:
execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))

goal (1 subgoal):
 1. reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))

goal (1 subgoal):
 1. reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
using reachable_def
[PROOF STATE]
proof (prove)
using this:
execution e (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e))) (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
reachable ?s \<equiv> \<exists>e s'. execution e s' ?s

goal (1 subgoal):
 1. reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
reachable (\<epsilon>(r \<mapsto> (\<epsilon>, \<epsilon>, e)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachability_closed_under_execution_step:
  assumes
    reach: "reachable s" and
    step: "revision_step r s s'"
  shows "reachable s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
obtain init e where exec: "execution e init s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e init. execution e init s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reach reachable_def
[PROOF STATE]
proof (prove)
using this:
reachable s
reachable ?s \<equiv> \<exists>e s'. execution e s' ?s

goal (1 subgoal):
 1. (\<And>e init. execution e init s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
execution e init s

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
hence init_s:"init \<leadsto>\<^sup>* s"
[PROOF STATE]
proof (prove)
using this:
execution e init s

goal (1 subgoal):
 1. init \<leadsto>\<^sup>* s
[PROOF STEP]
by (simp add: execution_def)
[PROOF STATE]
proof (state)
this:
init \<leadsto>\<^sup>* s

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
have s_s': "s \<leadsto> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<leadsto> s'
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
revision_step r s s'

goal (1 subgoal):
 1. s \<leadsto> s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<leadsto> s'

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
have "init \<leadsto>\<^sup>* s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init \<leadsto>\<^sup>* s'
[PROOF STEP]
using init_s s_s'
[PROOF STATE]
proof (prove)
using this:
init \<leadsto>\<^sup>* s
s \<leadsto> s'

goal (1 subgoal):
 1. init \<leadsto>\<^sup>* s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
init \<leadsto>\<^sup>* s'

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
hence "execution e init s'"
[PROOF STATE]
proof (prove)
using this:
init \<leadsto>\<^sup>* s'

goal (1 subgoal):
 1. execution e init s'
[PROOF STEP]
using exec
[PROOF STATE]
proof (prove)
using this:
init \<leadsto>\<^sup>* s'
execution e init s

goal (1 subgoal):
 1. execution e init s'
[PROOF STEP]
by (simp add: execution_def)
[PROOF STATE]
proof (state)
this:
execution e init s'

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
execution e init s'

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
using reachable_def
[PROOF STATE]
proof (prove)
using this:
execution e init s'
reachable ?s \<equiv> \<exists>e s'. execution e s' ?s

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reachable s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachability_closed_under_execution: "reachable s \<Longrightarrow> s \<leadsto>\<^sup>* s' \<Longrightarrow> reachable s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; s \<leadsto>\<^sup>* s'\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>reachable s; s \<leadsto>\<^sup>* s'\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
assume reach: "reachable s" and "s \<leadsto>\<^sup>* s'"
[PROOF STATE]
proof (state)
this:
reachable s
s \<leadsto>\<^sup>* s'

goal (1 subgoal):
 1. \<lbrakk>reachable s; s \<leadsto>\<^sup>* s'\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable s
s \<leadsto>\<^sup>* s'
[PROOF STEP]
obtain n where "(s, s') \<in> [\<leadsto>]^^n"
[PROOF STATE]
proof (prove)
using this:
reachable s
s \<leadsto>\<^sup>* s'

goal (1 subgoal):
 1. (\<And>n. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using rtrancl_imp_relpow
[PROOF STATE]
proof (prove)
using this:
reachable s
s \<leadsto>\<^sup>* s'
?p \<in> ?R\<^sup>* \<Longrightarrow> \<exists>n. ?p \<in> ?R ^^ n

goal (1 subgoal):
 1. (\<And>n. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(s, s') \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. \<lbrakk>reachable s; s \<leadsto>\<^sup>* s'\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
thus "reachable s'"
[PROOF STATE]
proof (prove)
using this:
(s, s') \<in> [\<leadsto>] ^^ n

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
proof (induct n arbitrary: s')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s'. (s, s') \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> reachable s'
 2. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(s, s') \<in> [\<leadsto>] ^^ 0

goal (2 subgoals):
 1. \<And>s'. (s, s') \<in> [\<leadsto>] ^^ 0 \<Longrightarrow> reachable s'
 2. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(s, s') \<in> [\<leadsto>] ^^ 0

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
using reach
[PROOF STATE]
proof (prove)
using this:
(s, s') \<in> [\<leadsto>] ^^ 0
reachable s

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reachable s'

goal (1 subgoal):
 1. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(s, ?s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable ?s'
(s, s') \<in> [\<leadsto>] ^^ Suc n

goal (1 subgoal):
 1. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
obtain s'' where "(s,s'') \<in> [\<leadsto>]^^n" "s'' \<leadsto> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>(s, s'') \<in> [\<leadsto>] ^^ n; s'' \<leadsto> s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
(s, s') \<in> [\<leadsto>] ^^ Suc n

goal (1 subgoal):
 1. (\<And>s''. \<lbrakk>(s, s'') \<in> [\<leadsto>] ^^ n; s'' \<leadsto> s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(s, s'') \<in> [\<leadsto>] ^^ n
s'' \<leadsto> s'

goal (1 subgoal):
 1. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
have "reachable s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reachable s''
[PROOF STEP]
by (simp add: Suc.hyps \<open>(s, s'') \<in> [\<leadsto>]^^n\<close>)
[PROOF STATE]
proof (state)
this:
reachable s''

goal (1 subgoal):
 1. \<And>n s'. \<lbrakk>\<And>s'. (s, s') \<in> [\<leadsto>] ^^ n \<Longrightarrow> reachable s'; (s, s') \<in> [\<leadsto>] ^^ Suc n\<rbrakk> \<Longrightarrow> reachable s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
reachable s''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
reachable s''

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
using \<open>s'' \<leadsto> s'\<close> reachability_closed_under_execution_step
[PROOF STATE]
proof (prove)
using this:
reachable s''
s'' \<leadsto> s'
\<lbrakk>reachable ?s; revision_step ?r ?s ?s'\<rbrakk> \<Longrightarrow> reachable ?s'

goal (1 subgoal):
 1. reachable s'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
reachable s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
reachable s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proper_itI[intro?]:
    fixes it :: "('x,'\<sigma>1) set_iterator"
    and it' :: "('x,'\<sigma>2) set_iterator"
    assumes "it=foldli l \<and> it'=foldli l"
    shows "proper_it it it'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it it it'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
it = foldli l \<and> it' = foldli l

goal (1 subgoal):
 1. proper_it it it'
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
using this:
it = foldli l \<and> it' = foldli l

goal (1 subgoal):
 1. \<exists>l. it = foldli l \<and> it' = foldli l
[PROOF STEP]
by auto


[STATEMENT]
lemma proper_itE:
    fixes it :: "('x,'\<sigma>1) set_iterator"
    and it' :: "('x,'\<sigma>2) set_iterator"
    assumes "proper_it it it'"
    obtains l where "it=foldli l" and "it'=foldli l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
proper_it it it'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
using this:
\<exists>l. it = foldli l \<and> it' = foldli l

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma proper_it_parE:
    fixes it :: "'a \<Rightarrow> ('x,'\<sigma>1) set_iterator"
    and it' :: "'a \<Rightarrow> ('x,'\<sigma>2) set_iterator"
    assumes "\<forall>x. proper_it (it x) (it' x)"
    obtains f where "it = (\<lambda>x. foldli (f x))" and "it' = (\<lambda>x. foldli (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>it = (\<lambda>x. foldli (f x)); it' = (\<lambda>x. foldli (f x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x. proper_it (it x) (it' x)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>it = (\<lambda>x. foldli (f x)); it' = (\<lambda>x. foldli (f x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x. \<exists>l. it x = foldli l \<and> it' x = foldli l

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>it = (\<lambda>x. foldli (f x)); it' = (\<lambda>x. foldli (f x))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis


[STATEMENT]
lemma proper_it'D:
    "proper_it' it it' \<Longrightarrow> proper_it (it s) (it' s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' it it' \<Longrightarrow> proper_it (it s) (it' s)
[PROOF STEP]
unfolding proper_it'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. proper_it (it s) (it' s) \<Longrightarrow> proper_it (it s) (it' s)
[PROOF STEP]
by blast


[STATEMENT]
lemma proper_iterator_trigger:
    "proper_it it it' \<Longrightarrow> proper_it it it'"
    "proper_it' itf itf' \<Longrightarrow> proper_it' itf itf'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (proper_it it it' \<Longrightarrow> proper_it it it') &&& (proper_it' itf itf' \<Longrightarrow> proper_it' itf itf')
[PROOF STEP]
.


[STATEMENT]
lemma pi_foldli[icf_proper_iteratorI]:
    "proper_it (foldli l :: ('a,'\<sigma>) set_iterator) (foldli l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (foldli l) (foldli l)
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>la. foldli l = foldli la \<and> foldli l = foldli la
[PROOF STEP]
by auto


[STATEMENT]
lemma pi_foldri[icf_proper_iteratorI]:
    "proper_it (foldri l :: ('a,'\<sigma>) set_iterator) (foldri l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (foldri l) (foldri l)
[PROOF STEP]
unfolding proper_it_def foldri_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>la. foldli (rev l) = foldli la \<and> foldli (rev l) = foldli la
[PROOF STEP]
by auto


[STATEMENT]
lemma pi'_foldli[icf_proper_iteratorI]:
    "proper_it' (foldli o tsl) (foldli o tsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' (foldli \<circ> tsl) (foldli \<circ> tsl)
[PROOF STEP]
apply (clarsimp simp add: proper_it'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it (foldli (tsl s)) (foldli (tsl s))
[PROOF STEP]
apply (tagged_solver)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pi'_foldri[icf_proper_iteratorI]:
    "proper_it' (foldri o tsl) (foldri o tsl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' (foldri \<circ> tsl) (foldri \<circ> tsl)
[PROOF STEP]
apply (clarsimp simp add: proper_it'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it (foldri (tsl s)) (foldri (tsl s))
[PROOF STEP]
apply (tagged_solver)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pi_emp[icf_proper_iteratorI]:
    "proper_it set_iterator_emp set_iterator_emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it set_iterator_emp set_iterator_emp
[PROOF STEP]
unfolding proper_it_def set_iterator_emp_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>c f \<sigma>0. \<sigma>0) = foldli l \<and> (\<lambda>c f \<sigma>0. \<sigma>0) = foldli l
[PROOF STEP]
by (auto intro!: ext exI[where x="[]"])


[STATEMENT]
lemma pi_sng[icf_proper_iteratorI]:
    "proper_it (set_iterator_sng x) (set_iterator_sng x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_sng x) (set_iterator_sng x)
[PROOF STEP]
unfolding proper_it_def set_iterator_sng_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. (\<lambda>c f \<sigma>0. if c \<sigma>0 then f x \<sigma>0 else \<sigma>0) = foldli l \<and> (\<lambda>c f \<sigma>0. if c \<sigma>0 then f x \<sigma>0 else \<sigma>0) = foldli l
[PROOF STEP]
by (auto intro!: ext exI[where x="[x]"])


[STATEMENT]
lemma pi_union[icf_proper_iteratorI]:
    assumes PA: "proper_it it_a it_a'"
    assumes PB: "proper_it it_b it_b'"
    shows "proper_it (set_iterator_union it_a it_b)
      (set_iterator_union it_a' it_b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_union it_a it_b) (set_iterator_union it_a' it_b')
[PROOF STEP]
unfolding set_iterator_union_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (\<lambda>c f \<sigma>0. it_b c f (it_a c f \<sigma>0)) (\<lambda>c f \<sigma>0. it_b' c f (it_a' c f \<sigma>0))
[PROOF STEP]
apply (rule proper_itE[OF PA])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it_a = foldli l; it_a' = foldli l\<rbrakk> \<Longrightarrow> proper_it (\<lambda>c f \<sigma>0. it_b c f (it_a c f \<sigma>0)) (\<lambda>c f \<sigma>0. it_b' c f (it_a' c f \<sigma>0))
[PROOF STEP]
apply (rule proper_itE[OF PB])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l la. \<lbrakk>it_a = foldli l; it_a' = foldli l; it_b = foldli la; it_b' = foldli la\<rbrakk> \<Longrightarrow> proper_it (\<lambda>c f \<sigma>0. it_b c f (it_a c f \<sigma>0)) (\<lambda>c f \<sigma>0. it_b' c f (it_a' c f \<sigma>0))
[PROOF STEP]
apply (rule_tac l="l@la" in proper_itI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l la. \<lbrakk>it_a = foldli l; it_a' = foldli l; it_b = foldli la; it_b' = foldli la\<rbrakk> \<Longrightarrow> (\<lambda>c f \<sigma>0. it_b c f (it_a c f \<sigma>0)) = foldli (l @ la) \<and> (\<lambda>c f \<sigma>0. it_b' c f (it_a' c f \<sigma>0)) = foldli (l @ la)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l la. \<lbrakk>it_a = foldli l; it_a' = foldli l; it_b = foldli la; it_b' = foldli la\<rbrakk> \<Longrightarrow> (\<lambda>c f \<sigma>0. foldli la c f (foldli l c f \<sigma>0)) = foldli (l @ la) \<and> (\<lambda>c f \<sigma>0. foldli la c f (foldli l c f \<sigma>0)) = foldli (l @ la)
[PROOF STEP]
apply (intro conjI ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l la c f \<sigma>0. \<lbrakk>it_a = foldli l; it_a' = foldli l; it_b = foldli la; it_b' = foldli la\<rbrakk> \<Longrightarrow> foldli la c f (foldli l c f \<sigma>0) = foldli (l @ la) c f \<sigma>0
 2. \<And>l la c f \<sigma>0. \<lbrakk>it_a = foldli l; it_a' = foldli l; it_b = foldli la; it_b' = foldli la\<rbrakk> \<Longrightarrow> foldli la c f (foldli l c f \<sigma>0) = foldli (l @ la) c f \<sigma>0
[PROOF STEP]
apply (simp_all add: foldli_append)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pi_product[icf_proper_iteratorI]:
    fixes it_a :: "('a,'\<sigma>a) set_iterator"
    fixes it_b :: "'a \<Rightarrow> ('b,'\<sigma>a) set_iterator"
    assumes PA: "proper_it it_a it_a'"
    and PB: "\<And>x. proper_it (it_b x) (it_b' x)"
    shows "proper_it (set_iterator_product it_a it_b)
      (set_iterator_product it_a' it_b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_product it_a it_b) (set_iterator_product it_a' it_b')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proper_it (set_iterator_product it_a it_b) (set_iterator_product it_a' it_b')
[PROOF STEP]
from PB
[PROOF STATE]
proof (chain)
picking this:
proper_it (it_b ?x) (it_b' ?x)
[PROOF STEP]
have PB': "\<forall>x. proper_it (it_b x) (it_b' x)"
[PROOF STATE]
proof (prove)
using this:
proper_it (it_b ?x) (it_b' ?x)

goal (1 subgoal):
 1. \<forall>x. proper_it (it_b x) (it_b' x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>x. proper_it (it_b x) (it_b' x)

goal (1 subgoal):
 1. proper_it (set_iterator_product it_a it_b) (set_iterator_product it_a' it_b')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_product it_a it_b) (set_iterator_product it_a' it_b')
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. set_iterator_product it_a it_b = foldli l \<and> set_iterator_product it_a' it_b' = foldli l
[PROOF STEP]
apply (rule proper_itE[OF PA])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it_a = foldli l; it_a' = foldli l\<rbrakk> \<Longrightarrow> \<exists>l. set_iterator_product it_a it_b = foldli l \<and> set_iterator_product it_a' it_b' = foldli l
[PROOF STEP]
apply (rule proper_it_parE[OF PB'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l f. \<lbrakk>it_a = foldli l; it_a' = foldli l; it_b = (\<lambda>x. foldli (f x)); it_b' = (\<lambda>x. foldli (f x))\<rbrakk> \<Longrightarrow> \<exists>l. set_iterator_product it_a it_b = foldli l \<and> set_iterator_product it_a' it_b' = foldli l
[PROOF STEP]
apply (auto simp add: set_iterator_product_foldli_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
proper_it (set_iterator_product it_a it_b) (set_iterator_product it_a' it_b')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pi_image_filter[icf_proper_iteratorI]:
    fixes it :: "('x,'\<sigma>1) set_iterator"
    and it' :: "('x,'\<sigma>2) set_iterator"
    and g :: "'x \<Rightarrow> 'y option"
    assumes P: "proper_it it it'"
    shows "proper_it (set_iterator_image_filter g it)
      (set_iterator_image_filter g it')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_image_filter g it) (set_iterator_image_filter g it')
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. set_iterator_image_filter g it = foldli l \<and> set_iterator_image_filter g it' = foldli l
[PROOF STEP]
apply (rule proper_itE[OF P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> \<exists>l. set_iterator_image_filter g it = foldli l \<and> set_iterator_image_filter g it' = foldli l
[PROOF STEP]
apply (auto simp: set_iterator_image_filter_foldli_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pi_filter[icf_proper_iteratorI]:
    assumes P: "proper_it it it'"
    shows "proper_it (set_iterator_filter P it)
      (set_iterator_filter P it')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_filter P it) (set_iterator_filter P it')
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. set_iterator_filter P it = foldli l \<and> set_iterator_filter P it' = foldli l
[PROOF STEP]
apply (rule proper_itE[OF P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> \<exists>l. set_iterator_filter P it = foldli l \<and> set_iterator_filter P it' = foldli l
[PROOF STEP]
by (auto simp: set_iterator_filter_foldli_conv)


[STATEMENT]
lemma pi_image[icf_proper_iteratorI]:
    assumes P: "proper_it it it'"
    shows "proper_it (set_iterator_image g it)
      (set_iterator_image g it')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (set_iterator_image g it) (set_iterator_image g it')
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. set_iterator_image g it = foldli l \<and> set_iterator_image g it' = foldli l
[PROOF STEP]
apply (rule proper_itE[OF P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> \<exists>l. set_iterator_image g it = foldli l \<and> set_iterator_image g it' = foldli l
[PROOF STEP]
by (auto simp: set_iterator_image_foldli_conv)


[STATEMENT]
lemma pi_dom[icf_proper_iteratorI]:
    assumes P: "proper_it it it'"
    shows "proper_it (map_iterator_dom it)
      (map_iterator_dom it')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (map_iterator_dom it) (map_iterator_dom it')
[PROOF STEP]
unfolding proper_it_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. map_iterator_dom it = foldli l \<and> map_iterator_dom it' = foldli l
[PROOF STEP]
apply (rule proper_itE[OF P])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>it = foldli l; it' = foldli l\<rbrakk> \<Longrightarrow> \<exists>l. map_iterator_dom it = foldli l \<and> map_iterator_dom it' = foldli l
[PROOF STEP]
by (auto simp: map_iterator_dom_foldli_conv)


[STATEMENT]
lemma set_iterator_product_eq2:
    assumes "\<forall>a\<in>set la. itb a = itb' a"
    shows "set_iterator_product (foldli la) itb
    = set_iterator_product (foldli la) itb'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_product (foldli la) itb = set_iterator_product (foldli la) itb'
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. set_iterator_product (foldli la) itb x xa xb = set_iterator_product (foldli la) itb' x xa xb
[PROOF STEP]
fix c f \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. set_iterator_product (foldli la) itb x xa xb = set_iterator_product (foldli la) itb' x xa xb
[PROOF STEP]
show "set_iterator_product (foldli la) itb c f \<sigma>
      = set_iterator_product (foldli la) itb' c f \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_iterator_product (foldli la) itb c f \<sigma> = set_iterator_product (foldli la) itb' c f \<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set la. itb a = itb' a

goal (1 subgoal):
 1. set_iterator_product (foldli la) itb c f \<sigma> = set_iterator_product (foldli la) itb' c f \<sigma>
[PROOF STEP]
unfolding set_iterator_product_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set la. itb a = itb' a

goal (1 subgoal):
 1. foldli la c (\<lambda>a. itb a c (\<lambda>b. f (a, b))) \<sigma> = foldli la c (\<lambda>a. itb' a c (\<lambda>b. f (a, b))) \<sigma>
[PROOF STEP]
apply (induct la arbitrary: \<sigma>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<forall>a\<in>set []. itb a = itb' a \<Longrightarrow> foldli [] c (\<lambda>a. itb a c (\<lambda>b. f (a, b))) \<sigma> = foldli [] c (\<lambda>a. itb' a c (\<lambda>b. f (a, b))) \<sigma>
 2. \<And>a la \<sigma>. \<lbrakk>\<And>\<sigma>. \<forall>a\<in>set la. itb a = itb' a \<Longrightarrow> foldli la c (\<lambda>a. itb a c (\<lambda>b. f (a, b))) \<sigma> = foldli la c (\<lambda>a. itb' a c (\<lambda>b. f (a, b))) \<sigma>; \<forall>a\<in>set (a # la). itb a = itb' a\<rbrakk> \<Longrightarrow> foldli (a # la) c (\<lambda>a. itb a c (\<lambda>b. f (a, b))) \<sigma> = foldli (a # la) c (\<lambda>a. itb' a c (\<lambda>b. f (a, b))) \<sigma>
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set_iterator_product (foldli la) itb c f \<sigma> = set_iterator_product (foldli la) itb' c f \<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_it_to_list_genord_correct:
    assumes A: "map_iterator_genord (it s) m (\<lambda>(k,_) (k',_). R k k')"
    shows "map_of (it_to_list it s) = m
      \<and> distinct (map fst (it_to_list it s))
      \<and> sorted_wrt R ((map fst (it_to_list it s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted_wrt R (map fst (it_to_list it s))
[PROOF STEP]
unfolding it_to_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (it s (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) = m \<and> distinct (map fst (it s (\<lambda>_. True) (\<lambda>x l. l @ [x]) [])) \<and> sorted_wrt R (map fst (it s (\<lambda>_. True) (\<lambda>x l. l @ [x]) []))
[PROOF STEP]
apply (rule map_iterator_genord_rule_insert_P[OF A, where I="
      \<lambda>it l. map_of l = m |` it
        \<and> distinct (map fst l)
        \<and> sorted_wrt R ((map fst l))
      "])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. map_of [] = m |` {} \<and> distinct (map fst []) \<and> sorted_wrt R (map fst [])
 2. \<And>k v it \<sigma>. \<lbrakk>True; k \<in> dom m - it; m k = Some v; it \<subseteq> dom m; map_of \<sigma> = m |` it \<and> distinct (map fst \<sigma>) \<and> sorted_wrt R (map fst \<sigma>); \<forall>k' v'. k' \<in> dom m - it - {k} \<and> m k' = Some v' \<longrightarrow> (case (k, v) of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). R k k') (k', v'); \<forall>k' v'. k' \<in> it \<and> m k' = Some v' \<longrightarrow> (case (k', v') of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). R k k') (k, v)\<rbrakk> \<Longrightarrow> map_of (\<sigma> @ [(k, v)]) = m |` insert k it \<and> distinct (map fst (\<sigma> @ [(k, v)])) \<and> sorted_wrt R (map fst (\<sigma> @ [(k, v)]))
 3. \<And>\<sigma>. map_of \<sigma> = m |` dom m \<and> distinct (map fst \<sigma>) \<and> sorted_wrt R (map fst \<sigma>) \<Longrightarrow> map_of \<sigma> = m \<and> distinct (map fst \<sigma>) \<and> sorted_wrt R (map fst \<sigma>)
 4. \<And>\<sigma> it. \<lbrakk>it \<subseteq> dom m; it \<noteq> dom m; \<not> True; map_of \<sigma> = m |` it \<and> distinct (map fst \<sigma>) \<and> sorted_wrt R (map fst \<sigma>); \<forall>k v k' v'. k \<in> it \<and> m k = Some v \<and> k' \<notin> it \<and> m k' = Some v' \<longrightarrow> (case (k, v) of (k, uu_) \<Rightarrow> \<lambda>(k', uu_). R k k') (k', v')\<rbrakk> \<Longrightarrow> map_of \<sigma> = m \<and> distinct (map fst \<sigma>) \<and> sorted_wrt R (map fst \<sigma>)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> k \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' k; k \<notin> it; m k = Some v; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>)\<rbrakk> \<Longrightarrow> (m |` it)(k \<mapsto> v) = m |` insert k it
 2. \<And>it \<sigma> y a b. \<lbrakk>m a = Some y; it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> a \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R a k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' a; a \<notin> it; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>); (a, b) \<in> set \<sigma>\<rbrakk> \<Longrightarrow> False
 3. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> k \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' k; k \<notin> it; m k = Some v; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>)\<rbrakk> \<Longrightarrow> sorted_wrt R (map fst \<sigma> @ [k])
[PROOF STEP]
apply (auto simp: restrict_map_def) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>it \<sigma> y a b. \<lbrakk>m a = Some y; it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> a \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R a k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' a; a \<notin> it; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>); (a, b) \<in> set \<sigma>\<rbrakk> \<Longrightarrow> False
 2. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> k \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' k; k \<notin> it; m k = Some v; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>)\<rbrakk> \<Longrightarrow> sorted_wrt R (map fst \<sigma> @ [k])
[PROOF STEP]
apply (metis Some_eq_map_of_iff restrict_map_eq(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k v it \<sigma>. \<lbrakk>it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> k \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' k; k \<notin> it; m k = Some v; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>)\<rbrakk> \<Longrightarrow> sorted_wrt R (map fst \<sigma> @ [k])
[PROOF STEP]
apply (auto simp add: sorted_wrt_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k v it \<sigma> a b. \<lbrakk>it \<subseteq> dom m; \<forall>k'. k' \<in> dom m \<and> k' \<notin> it \<and> k' \<noteq> k \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k k'; \<forall>k'. k' \<in> it \<and> (\<exists>v'. m k' = Some v') \<longrightarrow> R k' k; k \<notin> it; m k = Some v; map_of \<sigma> = m |` it; distinct (map fst \<sigma>); sorted_wrt R (map fst \<sigma>); (a, b) \<in> set \<sigma>\<rbrakk> \<Longrightarrow> R a k
[PROOF STEP]
by (metis (lifting) restrict_map_eq(2) weak_map_of_SomeI)


[STATEMENT]
lemma (in linorder) map_it_to_list_linord_correct:
    assumes A: "map_iterator_linord (it s) m"
    shows "map_of (it_to_list it s) = m
      \<and> distinct (map fst (it_to_list it s))
      \<and> sorted ((map fst (it_to_list it s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted (map fst (it_to_list it s))
[PROOF STEP]
using map_it_to_list_genord_correct[where it=it,
      OF A[unfolded set_iterator_map_linord_def]]
[PROOF STATE]
proof (prove)
using this:
map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted (map fst (it_to_list it s))

goal (1 subgoal):
 1. map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted (map fst (it_to_list it s))
[PROOF STEP]
.


[STATEMENT]
lemma (in linorder) map_it_to_list_rev_linord_correct:
    assumes A: "map_iterator_rev_linord (it s) m"
    shows "map_of (it_to_list it s) = m
      \<and> distinct (map fst (it_to_list it s))
      \<and> sorted (rev (map fst (it_to_list it s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted (rev (map fst (it_to_list it s)))
[PROOF STEP]
using map_it_to_list_genord_correct[where it=it,
      OF A[unfolded set_iterator_map_rev_linord_def]]
[PROOF STATE]
proof (prove)
using this:
map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted_wrt (\<lambda>k k'. k' \<le> k) (map fst (it_to_list it s))

goal (1 subgoal):
 1. map_of (it_to_list it s) = m \<and> distinct (map fst (it_to_list it s)) \<and> sorted (rev (map fst (it_to_list it s)))
[PROOF STEP]
by simp


[STATEMENT]
lemma inj_on[intro]: "inj_on f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f A
[PROOF STEP]
using inj_onI left_inverse
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>x \<in> ?A; y \<in> ?A; ?f x = ?f y\<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> inj_on ?f ?A
?x \<in> A \<Longrightarrow> g (f ?x) = ?x

goal (1 subgoal):
 1. inj_on f A
[PROOF STEP]
by metis


[STATEMENT]
lemma injective_on:
      assumes "x \<in> A" "y \<in> A" "f x = f y"
      shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using assms left_inverse
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
f x = f y
?x \<in> A \<Longrightarrow> g (f ?x) = ?x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by metis


[STATEMENT]
lemma image_superset[intro]: "f ` A \<supseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> f ` A
[PROOF STEP]
using g.wellformed image_iff right_inverse subsetI
[PROOF STATE]
proof (prove)
using this:
?x \<in> B \<Longrightarrow> g ?x \<in> A
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)
?y \<in> B \<Longrightarrow> f (g ?y) = ?y
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B

goal (1 subgoal):
 1. B \<subseteq> f ` A
[PROOF STEP]
by metis


[STATEMENT]
lemma image_eq[simp]: "f ` A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
using image_superset
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> f ` A

goal (1 subgoal):
 1. f ` A = B
[PROOF STEP]
by auto


[STATEMENT]
lemma inj_on_bijection:
    assumes "inj_on f A"
    shows "bijection A (f ` A) f (inv_into A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Functions.bijection A (f ` A) f (inv_into A f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> f x \<in> f ` A
 2. \<And>x. x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A
 3. \<And>x. x \<in> A \<Longrightarrow> inv_into A f (f x) = x
 4. \<And>y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y
[PROOF STEP]
show "\<And> x. x \<in> A \<Longrightarrow> f x \<in> f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> f x \<in> f ` A
[PROOF STEP]
using imageI
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?A \<Longrightarrow> ?f ?x \<in> ?f ` ?A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> f x \<in> f ` A
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> f ?x \<in> f ` A

goal (3 subgoals):
 1. \<And>x. x \<in> f ` A \<Longrightarrow> inv_into A f x \<in> A
 2. \<And>x. x \<in> A \<Longrightarrow> inv_into A f (f x) = x
 3. \<And>y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y
[PROOF STEP]
show "\<And> y. y \<in> f ` A \<Longrightarrow> inv_into A f y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> inv_into A f y \<in> A
[PROOF STEP]
using inv_into_into
[PROOF STATE]
proof (prove)
using this:
?x \<in> ?f ` ?A \<Longrightarrow> inv_into ?A ?f ?x \<in> ?A

goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> inv_into A f y \<in> A
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
?y \<in> f ` A \<Longrightarrow> inv_into A f ?y \<in> A

goal (2 subgoals):
 1. \<And>x. x \<in> A \<Longrightarrow> inv_into A f (f x) = x
 2. \<And>y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y
[PROOF STEP]
show "\<And> x. x \<in> A \<Longrightarrow> inv_into A f (f x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> inv_into A f (f x) = x
[PROOF STEP]
using inv_into_f_f assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inj_on ?f ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> inv_into ?A ?f (?f ?x) = ?x
inj_on f A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> inv_into A f (f x) = x
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
?x \<in> A \<Longrightarrow> inv_into A f (f ?x) = ?x

goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y
[PROOF STEP]
show "\<And> y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y
[PROOF STEP]
using f_inv_into_f
[PROOF STATE]
proof (prove)
using this:
?y \<in> ?f ` ?A \<Longrightarrow> ?f (inv_into ?A ?f ?y) = ?y

goal (1 subgoal):
 1. \<And>y. y \<in> f ` A \<Longrightarrow> f (inv_into A f y) = y
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
?y \<in> f ` A \<Longrightarrow> f (inv_into A f ?y) = ?y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma singletonI:
  assumes "\<And>x. x \<in> A \<Longrightarrow> x = y"
  assumes "y \<in> A"
  shows "A = {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = {y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> ?x = y
y \<in> A

goal (1 subgoal):
 1. A = {y}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma set_mult_inclusion:
  assumes H:"subgroup H G"
  assumes Q:"P \<subseteq> carrier G"
  assumes PQ:"H <#> P \<subseteq> H"
  shows "P \<subseteq> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<subseteq> H
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
from H
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
[PROOF STEP]
have "\<one> \<in> H"
[PROOF STATE]
proof (prove)
using this:
subgroup H G

goal (1 subgoal):
 1. \<one> \<in> H
[PROOF STEP]
by (rule subgroup.one_closed)
[PROOF STATE]
proof (state)
this:
\<one> \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<one> \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
assume x:"x \<in> P"
[PROOF STATE]
proof (state)
this:
x \<in> P

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<one> \<in> H
x \<in> P
[PROOF STEP]
have "\<one> \<otimes> x \<in> H <#> P"
[PROOF STATE]
proof (prove)
using this:
\<one> \<in> H
x \<in> P

goal (1 subgoal):
 1. \<one> \<otimes> x \<in> H <#> P
[PROOF STEP]
unfolding set_mult_def
[PROOF STATE]
proof (prove)
using this:
\<one> \<in> H
x \<in> P

goal (1 subgoal):
 1. \<one> \<otimes> x \<in> (\<Union>h\<in>H. \<Union>k\<in>P. {h \<otimes> k})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<one> \<otimes> x \<in> H <#> P

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
with PQ
[PROOF STATE]
proof (chain)
picking this:
H <#> P \<subseteq> H
\<one> \<otimes> x \<in> H <#> P
[PROOF STEP]
have "\<one> \<otimes> x \<in> H"
[PROOF STATE]
proof (prove)
using this:
H <#> P \<subseteq> H
\<one> \<otimes> x \<in> H <#> P

goal (1 subgoal):
 1. \<one> \<otimes> x \<in> H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<one> \<otimes> x \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> H
[PROOF STEP]
with H Q x
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
P \<subseteq> carrier G
x \<in> P
\<one> \<otimes> x \<in> H
[PROOF STEP]
show  "x \<in> H"
[PROOF STATE]
proof (prove)
using this:
subgroup H G
P \<subseteq> carrier G
x \<in> P
\<one> \<otimes> x \<in> H

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma card_subgrp_dvd:
  assumes "subgroup H G"
  shows "card H dvd order G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H dvd order G
[PROOF STEP]
proof(cases "finite (carrier G)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (carrier G) \<Longrightarrow> card H dvd order G
 2. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite (carrier G)

goal (2 subgoals):
 1. finite (carrier G) \<Longrightarrow> card H dvd order G
 2. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
finite (carrier G)
[PROOF STEP]
have "card (rcosets H) * card H = order G"
[PROOF STATE]
proof (prove)
using this:
subgroup H G
finite (carrier G)

goal (1 subgoal):
 1. card (rcosets H) * card H = order G
[PROOF STEP]
by (metis lagrange)
[PROOF STATE]
proof (state)
this:
card (rcosets H) * card H = order G

goal (2 subgoals):
 1. finite (carrier G) \<Longrightarrow> card H dvd order G
 2. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
card (rcosets H) * card H = order G

goal (1 subgoal):
 1. card H dvd order G
[PROOF STEP]
by (metis dvd_triv_left mult.commute)
[PROOF STATE]
proof (state)
this:
card H dvd order G

goal (1 subgoal):
 1. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite (carrier G)

goal (1 subgoal):
 1. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
hence "order G = 0"
[PROOF STATE]
proof (prove)
using this:
infinite (carrier G)

goal (1 subgoal):
 1. order G = 0
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
infinite (carrier G)

goal (1 subgoal):
 1. card (carrier G) = 0
[PROOF STEP]
by (metis card.infinite)
[PROOF STATE]
proof (state)
this:
order G = 0

goal (1 subgoal):
 1. infinite (carrier G) \<Longrightarrow> card H dvd order G
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
order G = 0

goal (1 subgoal):
 1. card H dvd order G
[PROOF STEP]
by (metis dvd_0_right)
[PROOF STATE]
proof (state)
this:
card H dvd order G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subgroup_finite:
  assumes subgroup:"subgroup H G"
  assumes finite:"finite (carrier G)"
  shows "finite H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite H
[PROOF STEP]
by (metis finite finite_subset subgroup subgroup.subset)


[STATEMENT]
lemma pa_not_zero: "p ^ a \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p ^ a \<noteq> 0
[PROOF STEP]
by (simp add: prime_gt_0_nat prime_p)


[STATEMENT]
lemma sylow_greater_zero:
  shows "card (subgroups_of_size (p ^ a)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
obtain P where PG:"subgroup P G" and cardP:"card P = p ^ a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrakk>subgroup P G; card P = p ^ a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis sylow_thm)
[PROOF STATE]
proof (state)
this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
hence "P \<in> subgroups_of_size (p ^ a)"
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> subgroups_of_size (p ^ a)
[PROOF STEP]
unfolding subgroups_of_size_def
[PROOF STATE]
proof (prove)
using this:
subgroup P G
card P = p ^ a

goal (1 subgoal):
 1. P \<in> {H. subgroup H G \<and> card H = p ^ a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
hence "subgroups_of_size (p ^ a) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
P \<in> subgroups_of_size (p ^ a)

goal (1 subgoal):
 1. subgroups_of_size (p ^ a) \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subgroups_of_size (p ^ a) \<noteq> {}

goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
subgroups_of_size (p ^ a) \<noteq> {}

goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
from finite_G
[PROOF STATE]
proof (chain)
picking this:
finite (carrier G)
[PROOF STEP]
have "finite (subgroups_of_size (p ^ a))"
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. finite (subgroups_of_size (p ^ a))
[PROOF STEP]
unfolding subgroups_of_size_def subgroup_def
[PROOF STATE]
proof (prove)
using this:
finite (carrier G)

goal (1 subgoal):
 1. finite {H. ((H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<longrightarrow> y \<in> H \<longrightarrow> x \<otimes> y \<in> H)) \<and> \<one> \<in> H \<and> (\<forall>x. x \<in> H \<longrightarrow> inv x \<in> H)) \<and> card H = p ^ a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (subgroups_of_size (p ^ a))

goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
subgroups_of_size (p ^ a) \<noteq> {}
finite (subgroups_of_size (p ^ a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subgroups_of_size (p ^ a) \<noteq> {}
finite (subgroups_of_size (p ^ a))

goal (1 subgoal):
 1. 0 < card (subgroups_of_size (p ^ a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < card (subgroups_of_size (p ^ a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_snd_sylow: "snd_sylow G p a m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd_sylow G p a m
[PROOF STEP]
by (rule snd_sylow_axioms)