[STATEMENT]
lemma marked_imp_black_or_grey:
  "marked r s \<Longrightarrow> black r s \<or> grey r s"
  "\<not> white r s \<Longrightarrow> \<not> valid_ref r s \<or> black r s \<or> grey r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (marked r s \<Longrightarrow> black r s \<or> grey r s) &&& (\<not> white r s \<Longrightarrow> \<not> obj_at (\<lambda>s. True) r s \<or> black r s \<or> grey r s)
[PROOF STEP]
by (auto simp: black_def grey_def white_def obj_at_def split: option.splits)


[STATEMENT]
lemma p_not_sys:
  "p \<noteq> sys \<longleftrightarrow> p = gc \<or> (\<exists>m. p = mutator m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<noteq> sys) = (p = gc \<or> (\<exists>m. p = mutator m))
[PROOF STEP]
by (cases p) simp_all


[STATEMENT]
lemma (in mut_m') m'm[iff]: "m' \<noteq> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<noteq> m
[PROOF STEP]
using mm'
[PROOF STATE]
proof (prove)
using this:
m \<noteq> m'

goal (1 subgoal):
 1. m' \<noteq> m
[PROOF STEP]
by blast


[STATEMENT]
lemma obj_at_cong[cong]:
  "\<lbrakk>\<And>obj. sys_heap s r = Some obj \<Longrightarrow> P obj = P' obj; r = r'; s = s'\<rbrakk>
   \<Longrightarrow> obj_at P r s \<longleftrightarrow> obj_at P' r' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>obj. sys_heap s r = Some obj \<Longrightarrow> P obj = P' obj; r = r'; s = s'\<rbrakk> \<Longrightarrow> obj_at P r s = obj_at P' r' s'
[PROOF STEP]
unfolding obj_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>obj. sys_heap s r = Some obj \<Longrightarrow> P obj = P' obj; r = r'; s = s'\<rbrakk> \<Longrightarrow> (case sys_heap s r of None \<Rightarrow> False | Some x \<Rightarrow> P x) = (case sys_heap s' r' of None \<Rightarrow> False | Some x \<Rightarrow> P' x)
[PROOF STEP]
by (simp cong: option.case_cong)


[STATEMENT]
lemma obj_at_split:
  "Q (obj_at P r s) = ((sys_heap s r = None \<longrightarrow> Q False) \<and> (\<forall>obj. sys_heap s r = Some obj \<longrightarrow> Q (P obj)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (obj_at P r s) = ((sys_heap s r = None \<longrightarrow> Q False) \<and> (\<forall>obj. sys_heap s r = Some obj \<longrightarrow> Q (P obj)))
[PROOF STEP]
by (simp add: obj_at_def split: option.splits)


[STATEMENT]
lemma obj_at_split_asm:
  "Q (obj_at P r s) = (\<not> ((sys_heap s r = None \<and> \<not>Q False) \<or> (\<exists>obj. sys_heap s r = Some obj \<and> \<not> Q (P obj))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (obj_at P r s) = (\<not> (sys_heap s r = None \<and> \<not> Q False \<or> (\<exists>obj. sys_heap s r = Some obj \<and> \<not> Q (P obj))))
[PROOF STEP]
by (simp add: obj_at_def split: option.splits)


[STATEMENT]
lemma obj_at_eq_imp:
  "eq_imp (\<lambda>(_::unit) s. map_option P (sys_heap s r))
          (obj_at P r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. map_option P (sys_heap s r)) (obj_at P r)
[PROOF STEP]
by (simp add: eq_imp_def obj_at_def split: option.splits)


[STATEMENT]
lemma obj_at_simps:
  "obj_at (\<lambda>obj. P obj \<and> Q obj) r s \<longleftrightarrow> obj_at P r s \<and> obj_at Q r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. P obj \<and> Q obj) r s = (obj_at P r s \<and> obj_at Q r s)
[PROOF STEP]
(*  "obj_at (\<lambda>obj. R) r s \<longleftrightarrow> valid_ref r s \<and> R" looks good but applies to valid_ref *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>obj. P obj \<and> Q obj) r s = (obj_at P r s \<and> obj_at Q r s)
[PROOF STEP]
by (simp_all split: obj_at_splits)


[STATEMENT]
lemma obj_at_field_on_heap_cong[cong]:
  "\<lbrakk>\<And>r' obj. \<lbrakk>sys_heap s r = Some obj; obj_fields obj f = Some r'\<rbrakk>\<Longrightarrow> P r' = P' r'; r = r'; f = f'; s = s'\<rbrakk>
   \<Longrightarrow> obj_at_field_on_heap P r f s \<longleftrightarrow> obj_at_field_on_heap P' r' f' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r' obj. \<lbrakk>sys_heap s r = Some obj; obj_fields obj f = Some r'\<rbrakk> \<Longrightarrow> P r' = P' r'; r = r'; f = f'; s = s'\<rbrakk> \<Longrightarrow> obj_at_field_on_heap P r f s = obj_at_field_on_heap P' r' f' s'
[PROOF STEP]
unfolding obj_at_field_on_heap_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r' obj. \<lbrakk>sys_heap s r = Some obj; obj_fields obj f = Some r'\<rbrakk> \<Longrightarrow> P r' = P' r'; r = r'; f = f'; s = s'\<rbrakk> \<Longrightarrow> (case map_option obj_fields (sys_heap s r) of None \<Rightarrow> False | Some fs \<Rightarrow> case fs f of None \<Rightarrow> True | Some x \<Rightarrow> P x) = (case map_option obj_fields (sys_heap s' r') of None \<Rightarrow> False | Some fs \<Rightarrow> case fs f' of None \<Rightarrow> True | Some x \<Rightarrow> P' x)
[PROOF STEP]
by (simp cong: option.case_cong)


[STATEMENT]
lemma obj_at_field_on_heap_split:
  "Q (obj_at_field_on_heap P r f s) \<longleftrightarrow> ((sys_heap s r = None \<longrightarrow> Q False)
                                 \<and> (\<forall>obj. sys_heap s r = Some obj \<and> obj_fields obj f = None \<longrightarrow> Q True)
                                 \<and> (\<forall>r' obj. sys_heap s r = Some obj \<and> obj_fields obj f = Some r' \<longrightarrow> Q (P r')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (obj_at_field_on_heap P r f s) = ((sys_heap s r = None \<longrightarrow> Q False) \<and> (\<forall>obj. sys_heap s r = Some obj \<and> obj_fields obj f = None \<longrightarrow> Q True) \<and> (\<forall>r' obj. sys_heap s r = Some obj \<and> obj_fields obj f = Some r' \<longrightarrow> Q (P r')))
[PROOF STEP]
by (simp add: obj_at_field_on_heap_def split: option.splits)


[STATEMENT]
lemma obj_at_field_on_heap_split_asm:
  "Q (obj_at_field_on_heap P r f s) \<longleftrightarrow> (\<not> ((sys_heap s r = None \<and> \<not>Q False)
                                    \<or> (\<exists>obj. sys_heap s r = Some obj \<and> obj_fields obj f = None \<and> \<not> Q True)
                                    \<or> (\<exists>r' obj. sys_heap s r = Some obj \<and> obj_fields obj f = Some r' \<and> \<not> Q (P r'))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q (obj_at_field_on_heap P r f s) = (\<not> (sys_heap s r = None \<and> \<not> Q False \<or> (\<exists>obj. sys_heap s r = Some obj \<and> obj_fields obj f = None \<and> \<not> Q True) \<or> (\<exists>r' obj. sys_heap s r = Some obj \<and> obj_fields obj f = Some r' \<and> \<not> Q (P r'))))
[PROOF STEP]
by (simp add: obj_at_field_on_heap_def split: option.splits)


[STATEMENT]
lemma obj_at_field_on_heap_eq_imp:
  "eq_imp (\<lambda>(_::unit) s. sys_heap s r)
          (obj_at_field_on_heap P r f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. sys_heap s r) (obj_at_field_on_heap P r f)
[PROOF STEP]
by (simp add: eq_imp_def obj_at_field_on_heap_def)


[STATEMENT]
lemma obj_at_field_on_heap_imp_valid_ref[elim]:
  "obj_at_field_on_heap P r f s \<Longrightarrow> valid_ref r s"
  "obj_at_field_on_heap P r f s \<Longrightarrow> valid_null_ref (Some r) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (obj_at_field_on_heap P r f s \<Longrightarrow> obj_at (\<lambda>s. True) r s) &&& (obj_at_field_on_heap P r f s \<Longrightarrow> valid_null_ref (Some r) s)
[PROOF STEP]
by (auto simp: obj_at_field_on_heap_def valid_null_ref_def split: obj_at_splits option.splits)


[STATEMENT]
lemma obj_at_field_on_heapE[elim]:
  "\<lbrakk> obj_at_field_on_heap P r f s; sys_heap s' r = sys_heap s r; \<And>r'. P r' \<Longrightarrow> P' r' \<rbrakk>
       \<Longrightarrow> obj_at_field_on_heap P' r f s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at_field_on_heap P r f s; sys_heap s' r = sys_heap s r; \<And>r'. P r' \<Longrightarrow> P' r'\<rbrakk> \<Longrightarrow> obj_at_field_on_heap P' r f s'
[PROOF STEP]
by (simp add: obj_at_field_on_heap_def split: option.splits)


[STATEMENT]
lemma valid_null_ref_eq_imp:
  "eq_imp (\<lambda>(_::unit) s. Option.bind r (map_option \<langle>True\<rangle> \<circ> sys_heap s))
          (valid_null_ref r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>_ s. Option.bind r (map_option (\<lambda>s. True) \<circ> sys_heap s)) (valid_null_ref r)
[PROOF STEP]
by (simp add: eq_imp_def obj_at_def valid_null_ref_def split: option.splits)


[STATEMENT]
lemma valid_null_ref_simps[simp]:
  "valid_null_ref None s"
  "valid_null_ref (Some r) s \<longleftrightarrow> valid_ref r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_null_ref None s &&& valid_null_ref (Some r) s = obj_at (\<lambda>s. True) r s
[PROOF STEP]
unfolding valid_null_ref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case None of None \<Rightarrow> \<lambda>s. True | Some r' \<Rightarrow> obj_at (\<lambda>s. True) r') s &&& (case Some r of None \<Rightarrow> \<lambda>s. True | Some r' \<Rightarrow> obj_at (\<lambda>s. True) r') s = obj_at (\<lambda>s. True) r s
[PROOF STEP]
by simp_all


[STATEMENT]
lemma do_store_action_prj_simps[simp]:
  "fM (do_store_action w s) = fl \<longleftrightarrow> (fM s = fl \<and> w \<noteq> mw_fM (\<not>fM s)) \<or> w = mw_fM fl"
  "fl = fM (do_store_action w s) \<longleftrightarrow> (fl = fM s \<and> w \<noteq> mw_fM (\<not>fM s)) \<or> w = mw_fM fl"
  "fA (do_store_action w s) = fl \<longleftrightarrow> (fA s = fl \<and> w \<noteq> mw_fA (\<not>fA s)) \<or> w = mw_fA fl"
  "fl = fA (do_store_action w s) \<longleftrightarrow> (fl = fA s \<and> w \<noteq> mw_fA (\<not>fA s)) \<or> w = mw_fA fl"
  "ghost_hs_in_sync (do_store_action w s) = ghost_hs_in_sync s"
  "ghost_hs_phase (do_store_action w s) = ghost_hs_phase s"
  "ghost_honorary_grey (do_store_action w s) = ghost_honorary_grey s"
  "hs_pending (do_store_action w s) = hs_pending s"
  "hs_type (do_store_action w s) = hs_type s"
  "heap (do_store_action w s) r = None \<longleftrightarrow> heap s r = None"
  "mem_lock (do_store_action w s) = mem_lock s"
  "phase (do_store_action w s) = ph \<longleftrightarrow> (phase s = ph \<and> (\<forall>ph'. w \<noteq> mw_Phase ph') \<or> w = mw_Phase ph)"
  "ph = phase (do_store_action w s) \<longleftrightarrow> (ph = phase s \<and> (\<forall>ph'. w \<noteq> mw_Phase ph') \<or> w = mw_Phase ph)"
  "W (do_store_action w s) = W s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((fM (do_store_action w s) = fl) = (fM s = fl \<and> w \<noteq> mw_fM (\<not> fM s) \<or> w = mw_fM fl) &&& (fl = fM (do_store_action w s)) = (fl = fM s \<and> w \<noteq> mw_fM (\<not> fM s) \<or> w = mw_fM fl) &&& (fA (do_store_action w s) = fl) = (fA s = fl \<and> w \<noteq> mw_fA (\<not> fA s) \<or> w = mw_fA fl)) &&& ((fl = fA (do_store_action w s)) = (fl = fA s \<and> w \<noteq> mw_fA (\<not> fA s) \<or> w = mw_fA fl) &&& ghost_hs_in_sync (do_store_action w s) = ghost_hs_in_sync s) &&& ghost_hs_phase (do_store_action w s) = ghost_hs_phase s &&& ghost_honorary_grey (do_store_action w s) = ghost_honorary_grey s) &&& (hs_pending (do_store_action w s) = hs_pending s &&& hs_type (do_store_action w s) = hs_type s &&& (heap (do_store_action w s) r = None) = (heap s r = None)) &&& (mem_lock (do_store_action w s) = mem_lock s &&& (phase (do_store_action w s) = ph) = (phase s = ph \<and> (\<forall>ph'. w \<noteq> mw_Phase ph') \<or> w = mw_Phase ph)) &&& (ph = phase (do_store_action w s)) = (ph = phase s \<and> (\<forall>ph'. w \<noteq> mw_Phase ph') \<or> w = mw_Phase ph) &&& W (do_store_action w s) = W s
[PROOF STEP]
by (auto simp: do_store_action_def fun_upd_apply split: mem_store_action.splits obj_at_splits)


[STATEMENT]
lemma reaches_refl[iff]:
  "(r reaches r) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r reaches r) s
[PROOF STEP]
unfolding reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* r r
[PROOF STEP]
by blast


[STATEMENT]
lemma reaches_step[intro]:
  "\<lbrakk>(x reaches y) s; (y points_to z) s\<rbrakk> \<Longrightarrow> (x reaches z) s"
  "\<lbrakk>(y reaches z) s; (x points_to y) s\<rbrakk> \<Longrightarrow> (x reaches z) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(x reaches y) s; (y points_to z) s\<rbrakk> \<Longrightarrow> (x reaches z) s) &&& (\<lbrakk>(y reaches z) s; (x points_to y) s\<rbrakk> \<Longrightarrow> (x reaches z) s)
[PROOF STEP]
unfolding reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y; (y points_to z) s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z) &&& (\<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* y z; (x points_to y) s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z)
[PROOF STEP]
apply (simp add: rtranclp.rtrancl_into_rtrancl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* y z; (x points_to y) s\<rbrakk> \<Longrightarrow> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z
[PROOF STEP]
apply (simp add: converse_rtranclp_into_rtranclp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma reaches_induct[consumes 1, case_names refl step, induct set: reaches]:
  assumes "(x reaches y) s"
  assumes "\<And>x. P x x"
  assumes "\<And>x y z. \<lbrakk>(x reaches y) s; P x y; (y points_to z) s\<rbrakk> \<Longrightarrow> P x z"
  shows "P x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x reaches y) s
P ?x ?x
\<lbrakk>(?x reaches ?y) s; P ?x ?y; (?y points_to ?z) s\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P x y
[PROOF STEP]
unfolding reaches_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x y
P ?x ?x
\<lbrakk>(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* ?x ?y; P ?x ?y; (?y points_to ?z) s\<rbrakk> \<Longrightarrow> P ?x ?z

goal (1 subgoal):
 1. P x y
[PROOF STEP]
by (rule rtranclp.induct)


[STATEMENT]
lemma converse_reachesE[consumes 1, case_names base step]:
  assumes "(x reaches z) s"
  assumes "x = z \<Longrightarrow> P"
  assumes "\<And>y. \<lbrakk>(x points_to y) s; (y reaches z) s\<rbrakk> \<Longrightarrow> P"
  shows P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x reaches z) s
x = z \<Longrightarrow> P
\<lbrakk>(x points_to ?y) s; (?y reaches z) s\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
unfolding reaches_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* x z
x = z \<Longrightarrow> P
\<lbrakk>(x points_to ?y) s; (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* ?y z\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by (blast elim: converse_rtranclpE)


[STATEMENT]
lemma reaches_fields: \<comment> \<open>Complicated condition takes care of \<open>alloc\<close>: collapses no object and object with no fields\<close>
  assumes "(x reaches y) s'"
  assumes "\<forall>r'. \<Union>(ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union>(ran ` obj_fields ` set_option (sys_heap s r'))"
  shows "(x reaches y) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x reaches y) s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x reaches y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))

goal (1 subgoal):
 1. (x reaches y) s
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches x) s
 2. \<And>x y z. \<lbrakk>(x reaches y) s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s; (y points_to z) s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))\<rbrakk> \<Longrightarrow> (x reaches z) s
[PROOF STEP]
case (step x y z)
[PROOF STATE]
proof (state)
this:
(x reaches y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s
(y points_to z) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))

goal (2 subgoals):
 1. \<And>x. \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches x) s
 2. \<And>x y z. \<lbrakk>(x reaches y) s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s; (y points_to z) s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))\<rbrakk> \<Longrightarrow> (x reaches z) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x reaches y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s
(y points_to z) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
[PROOF STEP]
have "(y points_to z) s"
[PROOF STATE]
proof (prove)
using this:
(x reaches y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s
(y points_to z) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))

goal (1 subgoal):
 1. (y points_to z) s
[PROOF STEP]
by (cases "sys_heap s y")
       (auto 10 10 simp: ran_def obj_at_def split: option.splits dest!: spec[where x=y])
[PROOF STATE]
proof (state)
this:
(y points_to z) s

goal (2 subgoals):
 1. \<And>x. \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches x) s
 2. \<And>x y z. \<lbrakk>(x reaches y) s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s; (y points_to z) s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))\<rbrakk> \<Longrightarrow> (x reaches z) s
[PROOF STEP]
with step
[PROOF STATE]
proof (chain)
picking this:
(x reaches y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s
(y points_to z) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
(y points_to z) s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(x reaches y) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches y) s
(y points_to z) s'
\<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))
(y points_to z) s

goal (1 subgoal):
 1. (x reaches z) s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x reaches z) s

goal (1 subgoal):
 1. \<And>x. \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s' r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) \<Longrightarrow> (x reaches x) s
[PROOF STEP]
qed simp


[STATEMENT]
lemma reaches_eq_imp:
  "eq_imp (\<lambda>r' s. \<Union>(ran ` obj_fields ` set_option (sys_heap s r')))
          (x reaches y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. \<Union> (ran ` obj_fields ` set_option (sys_heap s r'))) (x reaches y)
[PROOF STEP]
unfolding eq_imp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))) \<longrightarrow> (x reaches y) s = (x reaches y) s'
[PROOF STEP]
by (metis reaches_fields)


[STATEMENT]
lemma obj_at_mark_dequeue[simp]:
  "obj_at P r (s(sys := s sys\<lparr> heap := (sys_heap s)(r' := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r')), mem_store_buffers := wb' \<rparr>))
\<longleftrightarrow> obj_at (\<lambda>obj. (P (if r = r' then obj\<lparr> obj_mark := fl \<rparr> else obj))) r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at P r (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r')), mem_store_buffers := wb'\<rparr>)) = obj_at (\<lambda>obj. P (if r = r' then obj\<lparr>obj_mark := fl\<rparr> else obj)) r s
[PROOF STEP]
by (clarsimp simp: fun_upd_apply split: obj_at_splits)


[STATEMENT]
lemma obj_at_field_on_heap_mw_simps[simp]:
  "obj_at_field_on_heap P r0 f0
         (s(sys := (s sys)\<lparr> heap := (sys_heap s)(r := map_option (\<lambda>obj :: ('field, 'payload, 'ref) object. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)),
                            mem_store_buffers := (mem_store_buffers (s Sys))(p := ws) \<rparr>))
\<longleftrightarrow> ( (r \<noteq> r0 \<or> f \<noteq> f0) \<and> obj_at_field_on_heap P r0 f0 s )
   \<or> (r = r0 \<and> f = f0 \<and> valid_ref r s \<and> (case opt_r' of Some r'' \<Rightarrow> P r'' | _ \<Rightarrow> True))"
  "obj_at_field_on_heap P r f (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r')), mem_store_buffers := sb'\<rparr>))
\<longleftrightarrow> obj_at_field_on_heap P r f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. obj_at_field_on_heap P r0 f0 (s(sys := s sys\<lparr>heap := (sys_heap s)(r := map_option (\<lambda>obj. obj\<lparr>obj_fields := (obj_fields obj)(f := opt_r')\<rparr>) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s Sys))(p := ws)\<rparr>)) = ((r \<noteq> r0 \<or> f \<noteq> f0) \<and> obj_at_field_on_heap P r0 f0 s \<or> r = r0 \<and> f = f0 \<and> obj_at (\<lambda>s. True) r s \<and> (case opt_r' of None \<Rightarrow> True | Some r'' \<Rightarrow> P r'')) &&& obj_at_field_on_heap P r f (s(sys := s sys\<lparr>heap := (sys_heap s)(r' := map_option (obj_mark_update (\<lambda>_. fl)) (sys_heap s r')), mem_store_buffers := sb'\<rparr>)) = obj_at_field_on_heap P r f s
[PROOF STEP]
by (auto simp: obj_at_field_on_heap_def fun_upd_apply split: option.splits obj_at_splits)


[STATEMENT]
lemma obj_at_field_on_heap_no_pending_stores:
  "\<lbrakk> sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; \<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); valid_ref r s \<rbrakk>
     \<Longrightarrow> obj_at_field_on_heap (\<lambda>r. opt_r' = Some r) r f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_load (mutator m) (mr_Ref r f) (s sys) = mv_Ref opt_r'; \<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>r. opt_r' = Some r) r f s
[PROOF STEP]
unfolding sys_load_def fold_stores_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(do_load_action (mr_Ref r f) \<circ> (\<lambda>s. fold (\<lambda>w. (\<circ>) (do_store_action w)) (mem_store_buffers s (mutator m)) id s)) (s sys) = mv_Ref opt_r'; \<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>r. opt_r' = Some r) r f s
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f)\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>ra. Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s
[PROOF STEP]
apply (rule fold_invariant[where P="\<lambda>fr. obj_at_field_on_heap (\<lambda>r'. Option.bind (heap (fr (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some r') r f s"
                             and Q="\<lambda>w. w \<in> set (sys_mem_store_buffers (mutator m) s)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); x \<in> set (sys_mem_store_buffers (mutator m) s)\<rbrakk> \<Longrightarrow> x \<in> set (sys_mem_store_buffers (mutator m) s)
 2. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f)\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>ra. Option.bind (heap (id (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s
 3. \<And>x sa. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); x \<in> set (sys_mem_store_buffers (mutator m) s); obj_at_field_on_heap (\<lambda>ra. Option.bind (heap (sa (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>ra. Option.bind (heap ((do_store_action x \<circ> sa) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f)\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>ra. Option.bind (heap (id (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s
 2. \<And>x sa. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); x \<in> set (sys_mem_store_buffers (mutator m) s); obj_at_field_on_heap (\<lambda>ra. Option.bind (heap (sa (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>ra. Option.bind (heap ((do_store_action x \<circ> sa) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s
[PROOF STEP]
apply (fastforce simp: obj_at_field_on_heap_def split: option.splits obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x sa. \<lbrakk>\<forall>opt_r'. mw_Mutate r f opt_r' \<notin> set (sys_mem_store_buffers (mutator m) s); obj_at (\<lambda>s. True) r s; opt_r' = Option.bind (heap (fold (\<lambda>w. (\<circ>) (do_store_action w)) (sys_mem_store_buffers (mutator m) s) id (s sys)) r) (\<lambda>obj. obj_fields obj f); x \<in> set (sys_mem_store_buffers (mutator m) s); obj_at_field_on_heap (\<lambda>ra. Option.bind (heap (sa (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>ra. Option.bind (heap ((do_store_action x \<circ> sa) (s sys)) r) (\<lambda>obj. obj_fields obj f) = Some ra) r f s
[PROOF STEP]
apply (auto simp: do_store_action_def map_option_case fun_upd_apply
           split: obj_at_field_on_heap_splits option.splits obj_at_splits mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inj_upOne: "inj upOne"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj upOne
[PROOF STEP]
by (rule Fun.injI, simp)


[STATEMENT]
lemma surj_upOne: "surj upOne"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj upOne
[PROOF STEP]
proof (unfold Fun.surj_def, rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = upOne x
[PROOF STEP]
fix k::int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = upOne x
[PROOF STEP]
show "\<exists>m. k = upOne m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. k = upOne m
[PROOF STEP]
by (rule exI[of "\<lambda>l. k = upOne l" "k - 1"], simp)
[PROOF STATE]
proof (state)
this:
\<exists>m. k = upOne m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem bij_upOne: "bij upOne"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij upOne
[PROOF STEP]
by (unfold bij_def, rule conjI [OF inj_upOne surj_upOne])


[STATEMENT]
lemma no_fix_upOne: "upOne n \<noteq> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upOne n \<noteq> n
[PROOF STEP]
proof (rule notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. upOne n = n \<Longrightarrow> False
[PROOF STEP]
assume "upOne n = n"
[PROOF STATE]
proof (state)
this:
upOne n = n

goal (1 subgoal):
 1. upOne n = n \<Longrightarrow> False
[PROOF STEP]
with upOne_def
[PROOF STATE]
proof (chain)
picking this:
upOne ?n = ?n + 1
upOne n = n
[PROOF STEP]
have "n+1 = n"
[PROOF STATE]
proof (prove)
using this:
upOne ?n = ?n + 1
upOne n = n

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

goal (1 subgoal):
 1. upOne n = n \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
n + 1 = n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem "Fix upOne = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fix upOne = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Fix upOne = {}
[PROOF STEP]
from Fix_def[of upOne]
[PROOF STATE]
proof (chain)
picking this:
Fix upOne = {n. upOne n = n}
[PROOF STEP]
have "Fix upOne = {n . upOne n = n}"
[PROOF STATE]
proof (prove)
using this:
Fix upOne = {n. upOne n = n}

goal (1 subgoal):
 1. Fix upOne = {n. upOne n = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fix upOne = {n. upOne n = n}

goal (1 subgoal):
 1. Fix upOne = {}
[PROOF STEP]
with no_fix_upOne
[PROOF STATE]
proof (chain)
picking this:
upOne ?n \<noteq> ?n
Fix upOne = {n. upOne n = n}
[PROOF STEP]
have "Fix upOne = {n . False}"
[PROOF STATE]
proof (prove)
using this:
upOne ?n \<noteq> ?n
Fix upOne = {n. upOne n = n}

goal (1 subgoal):
 1. Fix upOne = {n. False}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fix upOne = {n. False}

goal (1 subgoal):
 1. Fix upOne = {}
[PROOF STEP]
with Set.empty_def
[PROOF STATE]
proof (chain)
picking this:
{} = {x. False}
Fix upOne = {n. False}
[PROOF STEP]
show "Fix upOne = {}"
[PROOF STATE]
proof (prove)
using this:
{} = {x. False}
Fix upOne = {n. False}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_upOne_eq: "(inv upOne) (n::int) = n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv upOne n = n - 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv upOne n = n - 1
[PROOF STEP]
fix "n" :: int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv upOne n = n - 1
[PROOF STEP]
have "((inv upOne) \<circ> upOne) (n - 1) = (inv upOne) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv upOne \<circ> upOne) (n - 1) = inv upOne n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(inv upOne \<circ> upOne) (n - 1) = inv upOne n

goal (1 subgoal):
 1. inv upOne n = n - 1
[PROOF STEP]
with inj_upOne and Hilbert_Choice.inv_o_cancel
[PROOF STATE]
proof (chain)
picking this:
inj upOne
inj ?f \<Longrightarrow> inv ?f \<circ> ?f = id
(inv upOne \<circ> upOne) (n - 1) = inv upOne n
[PROOF STEP]
show "(inv upOne) n = n - 1"
[PROOF STATE]
proof (prove)
using this:
inj upOne
inj ?f \<Longrightarrow> inv ?f \<circ> ?f = id
(inv upOne \<circ> upOne) (n - 1) = inv upOne n

goal (1 subgoal):
 1. inv upOne n = n - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv upOne n = n - 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "(inv upOne) n = n - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv upOne n = n - 1
[PROOF STEP]
by (rule Hilbert_Choice.inv_f_eq[of upOne "n - 1" n, OF inj_upOne], simp)


[STATEMENT]
lemma Ex1_Normal_form_part1: "f \<in> Ex1 \<Longrightarrow> \<exists>k. \<forall> n. f(n) = n + k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. f n = n + k
[PROOF STEP]
proof (rule Ex1.induct [of "f"], blast)
    \<comment> \<open>blast takes care of the first goal which is formal noise\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. upOne n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
assume "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. upOne n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
have "\<forall>n. upOne n = n + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. upOne n = n + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n. upOne n = n + 1

goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. upOne n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
with HOL.exI
[PROOF STATE]
proof (chain)
picking this:
?P ?x \<Longrightarrow> \<exists>x. ?P x
\<forall>n. upOne n = n + 1
[PROOF STEP]
show "\<exists>k. \<forall>n. upOne n = n + k"
[PROOF STATE]
proof (prove)
using this:
?P ?x \<Longrightarrow> \<exists>x. ?P x
\<forall>n. upOne n = n + 1

goal (1 subgoal):
 1. \<exists>k. \<forall>n. upOne n = n + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. upOne n = n + k

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
fix fa:: "int => int"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
assume fa_k: "\<exists>k. \<forall>n. fa n = n + k"
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. fa n = n + k

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
thus "\<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>n. fa n = n + k

goal (1 subgoal):
 1. \<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. (upOne \<circ> fa) n = n + k

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
fix fa :: "int \<Rightarrow> int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
assume fa_k: "\<exists>k. \<forall>n. fa n = n + k"
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. fa n = n + k

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
from inv_upOne_eq
[PROOF STATE]
proof (chain)
picking this:
inv upOne ?n = ?n - 1
[PROOF STEP]
have "\<forall>n. (inv upOne) n = n - 1"
[PROOF STATE]
proof (prove)
using this:
inv upOne ?n = ?n - 1

goal (1 subgoal):
 1. \<forall>n. inv upOne n = n - 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. inv upOne n = n - 1

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; \<exists>k. \<forall>n. fa n = n + k\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
with fa_k
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. \<forall>n. fa n = n + k
\<forall>n. inv upOne n = n - 1
[PROOF STEP]
show "\<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>n. fa n = n + k
\<forall>n. inv upOne n = n - 1

goal (1 subgoal):
 1. \<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. (inv upOne \<circ> fa) n = n + k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Ex1_Normal_form_part2:
  "(\<forall>f. ((\<forall>n. f n = n + k) \<longrightarrow> f \<in> Ex1))" (is "?P k")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (\<forall>n. f n = n + k) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof (rule int_induct [of "?P" 1])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<forall>f. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1
 2. \<And>i. \<lbrakk>1 \<le> i; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
 3. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
show "\<forall>f. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
fix f:: "int \<Rightarrow> int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
show "(\<forall>n. f n = n + 1) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n. f n = n + 1 \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume "\<forall>n. f n = n + 1"
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + 1

goal (1 subgoal):
 1. \<forall>n. f n = n + 1 \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
hence "\<forall>n. f n = upOne n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + 1

goal (1 subgoal):
 1. \<forall>n. f n = upOne n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = upOne n

goal (1 subgoal):
 1. \<forall>n. f n = n + 1 \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with fun_eq_iff[of f upOne,THEN sym]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. f x = upOne x) = (f = upOne)
\<forall>n. f n = upOne n
[PROOF STEP]
have "f = upOne"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. f x = upOne x) = (f = upOne)
\<forall>n. f n = upOne n

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

goal (1 subgoal):
 1. \<forall>n. f n = n + 1 \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1.base_func
[PROOF STATE]
proof (chain)
picking this:
upOne \<in> CofGroups.Ex1
f = upOne
[PROOF STEP]
show "f \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
upOne \<in> CofGroups.Ex1
f = upOne

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + 1) \<longrightarrow> f \<in> CofGroups.Ex1

goal (2 subgoals):
 1. \<And>i. \<lbrakk>1 \<le> i; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
 2. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>1 \<le> i; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
 2. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
fix i::int
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>1 \<le> i; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
 2. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume "1 \<le> i"
[PROOF STATE]
proof (state)
this:
1 \<le> i

goal (2 subgoals):
 1. \<And>i. \<lbrakk>1 \<le> i; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
 2. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume induct_hyp: "\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1

goal (2 subgoals):
 1. \<And>i. \<lbrakk>1 \<le> i; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
 2. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
show "\<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
fix f:: "int \<Rightarrow> int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
show "(\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume f_eq: "\<forall>n. f n = n + (i + 1)"
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + (i + 1)

goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
let ?h = "\<lambda>n. n + i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
from induct_hyp
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have h_Ex1: "?h \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. (\<lambda>n. n + i) \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. n + i) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
from  f_eq
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n + (i + 1)
[PROOF STEP]
have "\<forall>n. f n = upOne (?h n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + (i + 1)

goal (1 subgoal):
 1. \<forall>n. f n = upOne (n + i)
[PROOF STEP]
by (unfold upOne_def,auto)
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = upOne (n + i)

goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
hence "\<forall>n. f n = (upOne \<circ> ?h) n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = upOne (n + i)

goal (1 subgoal):
 1. \<forall>n. f n = (upOne \<circ> (\<lambda>n. n + i)) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = (upOne \<circ> (\<lambda>n. n + i)) n

goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with fun_eq_iff[THEN sym, of f "upOne \<circ> ?h"]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. f x = (upOne \<circ> (\<lambda>n. n + i)) x) = (f = upOne \<circ> (\<lambda>n. n + i))
\<forall>n. f n = (upOne \<circ> (\<lambda>n. n + i)) n
[PROOF STEP]
have "f = upOne \<circ> ?h"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. f x = (upOne \<circ> (\<lambda>n. n + i)) x) = (f = upOne \<circ> (\<lambda>n. n + i))
\<forall>n. f n = (upOne \<circ> (\<lambda>n. n + i)) n

goal (1 subgoal):
 1. f = upOne \<circ> (\<lambda>n. n + i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = upOne \<circ> (\<lambda>n. n + i)

goal (1 subgoal):
 1. \<forall>n. f n = n + (i + 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with h_Ex1 and Ex1.comp_func[of ?h]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. n + i) \<in> CofGroups.Ex1
(\<lambda>n. n + i) \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> (\<lambda>n. n + i) \<in> CofGroups.Ex1
f = upOne \<circ> (\<lambda>n. n + i)
[PROOF STEP]
show "f \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. n + i) \<in> CofGroups.Ex1
(\<lambda>n. n + i) \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> (\<lambda>n. n + i) \<in> CofGroups.Ex1
f = upOne \<circ> (\<lambda>n. n + i)

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + (i + 1)) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
fix i::int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume "i \<le> 1"
[PROOF STATE]
proof (state)
this:
i \<le> 1

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume induct_hyp: "\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i \<le> 1; \<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
show "\<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
fix f:: "int \<Rightarrow> int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
show "(\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume f_eq: "\<forall>n. f n = n + (i - 1)"
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + (i - 1)

goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
let ?h = "\<lambda>n. n + i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
from  induct_hyp
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
have h_Ex1: "?h \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (\<forall>n. f n = n + i) \<longrightarrow> f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. (\<lambda>n. n + i) \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. n + i) \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
from inv_upOne_eq and f_eq
[PROOF STATE]
proof (chain)
picking this:
inv upOne ?n = ?n - 1
\<forall>n. f n = n + (i - 1)
[PROOF STEP]
have "\<forall>n. f n = (inv upOne) (?h n)"
[PROOF STATE]
proof (prove)
using this:
inv upOne ?n = ?n - 1
\<forall>n. f n = n + (i - 1)

goal (1 subgoal):
 1. \<forall>n. f n = inv upOne (n + i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = inv upOne (n + i)

goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
hence "\<forall>n. f n = (inv upOne \<circ> ?h) n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = inv upOne (n + i)

goal (1 subgoal):
 1. \<forall>n. f n = (inv upOne \<circ> (\<lambda>n. n + i)) n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = (inv upOne \<circ> (\<lambda>n. n + i)) n

goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with fun_eq_iff[THEN sym, of f "inv upOne \<circ> ?h"]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. f x = (inv upOne \<circ> (\<lambda>n. n + i)) x) = (f = inv upOne \<circ> (\<lambda>n. n + i))
\<forall>n. f n = (inv upOne \<circ> (\<lambda>n. n + i)) n
[PROOF STEP]
have "f = inv upOne \<circ> ?h"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. f x = (inv upOne \<circ> (\<lambda>n. n + i)) x) = (f = inv upOne \<circ> (\<lambda>n. n + i))
\<forall>n. f n = (inv upOne \<circ> (\<lambda>n. n + i)) n

goal (1 subgoal):
 1. f = inv upOne \<circ> (\<lambda>n. n + i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = inv upOne \<circ> (\<lambda>n. n + i)

goal (1 subgoal):
 1. \<forall>n. f n = n + (i - 1) \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with h_Ex1 and Ex1.comp_inv[of ?h]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. n + i) \<in> CofGroups.Ex1
(\<lambda>n. n + i) \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<circ> (\<lambda>n. n + i) \<in> CofGroups.Ex1
f = inv upOne \<circ> (\<lambda>n. n + i)
[PROOF STEP]
show "f \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. n + i) \<in> CofGroups.Ex1
(\<lambda>n. n + i) \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<circ> (\<lambda>n. n + i) \<in> CofGroups.Ex1
f = inv upOne \<circ> (\<lambda>n. n + i)

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. (\<forall>n. f n = n + (i - 1)) \<longrightarrow> f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Ex1_Normal_form: "(f \<in> Ex1) = (\<exists>k. \<forall>n. f(n) = n + k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. f n = n + k)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. f n = n + k
 2. \<exists>k. \<forall>n. f n = n + k \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (2 subgoals):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. f n = n + k
 2. \<exists>k. \<forall>n. f n = n + k \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1_Normal_form_part1 [of f]
[PROOF STATE]
proof (chain)
picking this:
f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. f n = n + k
f \<in> CofGroups.Ex1
[PROOF STEP]
show "(\<exists>k. \<forall>n. f(n) = n + k)"
[PROOF STATE]
proof (prove)
using this:
f \<in> CofGroups.Ex1 \<Longrightarrow> \<exists>k. \<forall>n. f n = n + k
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<exists>k. \<forall>n. f n = n + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. f n = n + k

goal (1 subgoal):
 1. \<exists>k. \<forall>n. f n = n + k \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. \<forall>n. f n = n + k \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
assume "\<exists>k. \<forall>n. f(n) = n + k"
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. f n = n + k

goal (1 subgoal):
 1. \<exists>k. \<forall>n. f n = n + k \<Longrightarrow> f \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1_Normal_form_part2
[PROOF STATE]
proof (chain)
picking this:
\<forall>f. (\<forall>n. f n = n + ?k) \<longrightarrow> f \<in> CofGroups.Ex1
\<exists>k. \<forall>n. f n = n + k
[PROOF STEP]
show "f \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (\<forall>n. f n = n + ?k) \<longrightarrow> f \<in> CofGroups.Ex1
\<exists>k. \<forall>n. f n = n + k

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem all_bij: "f \<in> Ex1 \<Longrightarrow> bij f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> bij f
[PROOF STEP]
proof (unfold bij_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inj f \<and> surj f
[PROOF STEP]
assume "f \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inj f \<and> surj f
[PROOF STEP]
with Ex1_Normal_form
[PROOF STATE]
proof (chain)
picking this:
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)
f \<in> CofGroups.Ex1
[PROOF STEP]
obtain k where f_eq:"\<forall>n. f n = n + k"
[PROOF STATE]
proof (prove)
using this:
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)
f \<in> CofGroups.Ex1

goal (1 subgoal):
 1. (\<And>k. \<forall>n. f n = n + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<Longrightarrow> inj f \<and> surj f
[PROOF STEP]
show "inj f \<and> surj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f \<and> surj f
[PROOF STEP]
proof (rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj f
 2. surj f
[PROOF STEP]
show INJ: "inj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
fix n m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
assume "f n = f m"
[PROOF STATE]
proof (state)
this:
f n = f m

goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
with f_eq
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n + k
f n = f m
[PROOF STEP]
have "n + k = m + k"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + k
f n = f m

goal (1 subgoal):
 1. n + k = m + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n + k = m + k

goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
thus "n = m"
[PROOF STATE]
proof (prove)
using this:
n + k = m + k

goal (1 subgoal):
 1. n = m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. surj f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. surj f
[PROOF STEP]
show SURJ: "surj f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj f
[PROOF STEP]
proof (unfold Fun.surj_def, rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = f x
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>x. y = f x
[PROOF STEP]
from f_eq
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n + k
[PROOF STEP]
have "n = f (n - k)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. n = f (n - k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = f (n - k)

goal (1 subgoal):
 1. \<And>y. \<exists>x. y = f x
[PROOF STEP]
thus "\<exists>m. n = f m"
[PROOF STATE]
proof (prove)
using this:
n = f (n - k)

goal (1 subgoal):
 1. \<exists>m. n = f m
[PROOF STEP]
by (rule exI)
[PROOF STATE]
proof (state)
this:
\<exists>m. n = f m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
surj f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj f \<and> surj f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem no_fixed_pt:
  assumes f_Ex1: "f \<in> Ex1"
  and f_not_id: "f \<noteq> id"
  shows "Fix f = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
proof -
    \<comment> \<open>we start by proving an easy general fact\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
have f_eq_then_id: "(\<forall>n. f(n) = n) \<Longrightarrow> f = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. f n = n \<Longrightarrow> f = id
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>n. f n = n \<Longrightarrow> f = id
[PROOF STEP]
assume f_prop : "\<forall>n. f(n) = n"
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n

goal (1 subgoal):
 1. \<forall>n. f n = n \<Longrightarrow> f = id
[PROOF STEP]
have "(f x = id x) = (f x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x = id x) = (f x = x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f x = id x) = (f x = x)

goal (1 subgoal):
 1. \<forall>n. f n = n \<Longrightarrow> f = id
[PROOF STEP]
hence "(\<forall>x. (f x = id x)) = (\<forall>x. (f x = x))"
[PROOF STATE]
proof (prove)
using this:
(f x = id x) = (f x = x)

goal (1 subgoal):
 1. (\<forall>x. f x = id x) = (\<forall>x. f x = x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<forall>x. f x = id x) = (\<forall>x. f x = x)

goal (1 subgoal):
 1. \<forall>n. f n = n \<Longrightarrow> f = id
[PROOF STEP]
with fun_eq_iff[THEN sym, of f id] and f_prop
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. f x = id x) = (f = id)
\<forall>n. f n = n
(\<forall>x. f x = id x) = (\<forall>x. f x = x)
[PROOF STEP]
show "f = id"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. f x = id x) = (f = id)
\<forall>n. f n = n
(\<forall>x. f x = id x) = (\<forall>x. f x = x)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n \<Longrightarrow> f = id

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
from f_Ex1 and Ex1_Normal_form
[PROOF STATE]
proof (chain)
picking this:
f \<in> CofGroups.Ex1
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)
[PROOF STEP]
have "\<exists>k. \<forall>n. f(n) = n + k"
[PROOF STATE]
proof (prove)
using this:
f \<in> CofGroups.Ex1
(?f \<in> CofGroups.Ex1) = (\<exists>k. \<forall>n. ?f n = n + k)

goal (1 subgoal):
 1. \<exists>k. \<forall>n. f n = n + k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. \<forall>n. f n = n + k

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. \<forall>n. f n = n + k
[PROOF STEP]
obtain k where k_prop: "\<forall>n. f(n) = n + k"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. \<forall>n. f n = n + k

goal (1 subgoal):
 1. (\<And>k. \<forall>n. f n = n + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
hence "k = 0 \<Longrightarrow> \<forall>n. f(n) = n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + k

goal (1 subgoal):
 1. k = 0 \<Longrightarrow> \<forall>n. f n = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = 0 \<Longrightarrow> \<forall>n. f n = n

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with f_eq_then_id and f_not_id
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n \<Longrightarrow> f = id
f \<noteq> id
k = 0 \<Longrightarrow> \<forall>n. f n = n
[PROOF STEP]
have "k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n \<Longrightarrow> f = id
f \<noteq> id
k = 0 \<Longrightarrow> \<forall>n. f n = n

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

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with k_prop
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n = n + k
k \<noteq> 0
[PROOF STEP]
have "\<forall>n. f(n) \<noteq> n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n = n + k
k \<noteq> 0

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

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n. f n \<noteq> n

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
from Fix_def[of f]
[PROOF STATE]
proof (chain)
picking this:
Fix f = {n. f n = n}
[PROOF STEP]
have "Fix f = {n . f(n) = n}"
[PROOF STATE]
proof (prove)
using this:
Fix f = {n. f n = n}

goal (1 subgoal):
 1. Fix f = {n. f n = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fix f = {n. f n = n}

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. f n \<noteq> n
Fix f = {n. f n = n}
[PROOF STEP]
have "Fix f = {n. False}"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. f n \<noteq> n
Fix f = {n. f n = n}

goal (1 subgoal):
 1. Fix f = {n. False}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fix f = {n. False}

goal (1 subgoal):
 1. Fix f = {}
[PROOF STEP]
with Set.empty_def
[PROOF STATE]
proof (chain)
picking this:
{} = {x. False}
Fix f = {n. False}
[PROOF STEP]
show "Fix f = {}"
[PROOF STATE]
proof (prove)
using this:
{} = {x. False}
Fix f = {n. False}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem closed_comp: "f \<in> Ex1 \<and> g \<in> Ex1 \<Longrightarrow> f \<circ> g \<in> Ex1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1 \<Longrightarrow> f \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
proof (rule Ex1.induct [of f], blast)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> g \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
assume "f \<in> Ex1 \<and> g \<in> Ex1"
[PROOF STATE]
proof (state)
this:
f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1

goal (3 subgoals):
 1. f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> g \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
 3. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1.comp_func[of g]
[PROOF STATE]
proof (chain)
picking this:
g \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> g \<in> CofGroups.Ex1
f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1
[PROOF STEP]
show "upOne \<circ> g \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
g \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> g \<in> CofGroups.Ex1
f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. upOne \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upOne \<circ> g \<in> CofGroups.Ex1

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
fix fa
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
assume "fa \<circ> g \<in> Ex1"
[PROOF STATE]
proof (state)
this:
fa \<circ> g \<in> CofGroups.Ex1

goal (2 subgoals):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
 2. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1.comp_func [of "fa \<circ> g"]
    and Fun.o_assoc [of "upOne" "fa" "g"]
[PROOF STATE]
proof (chain)
picking this:
fa \<circ> g \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> (fa \<circ> g) \<in> CofGroups.Ex1
upOne \<circ> (fa \<circ> g) = upOne \<circ> fa \<circ> g
fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
show "upOne \<circ> fa \<circ> g \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
fa \<circ> g \<in> CofGroups.Ex1 \<Longrightarrow> upOne \<circ> (fa \<circ> g) \<in> CofGroups.Ex1
upOne \<circ> (fa \<circ> g) = upOne \<circ> fa \<circ> g
fa \<circ> g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
fix fa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
assume "fa \<circ> g \<in> Ex1"
[PROOF STATE]
proof (state)
this:
fa \<circ> g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. \<And>fa. \<lbrakk>f \<in> CofGroups.Ex1 \<and> g \<in> CofGroups.Ex1; fa \<in> CofGroups.Ex1; fa \<circ> g \<in> CofGroups.Ex1\<rbrakk> \<Longrightarrow> inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
with Ex1.comp_inv [of "fa \<circ> g"]
    and Fun.o_assoc [of "inv upOne" "fa" "g"]
[PROOF STATE]
proof (chain)
picking this:
fa \<circ> g \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<circ> (fa \<circ> g) \<in> CofGroups.Ex1
inv upOne \<circ> (fa \<circ> g) = inv upOne \<circ> fa \<circ> g
fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
show "(inv upOne) \<circ> fa \<circ> g \<in> Ex1"
[PROOF STATE]
proof (prove)
using this:
fa \<circ> g \<in> CofGroups.Ex1 \<Longrightarrow> inv upOne \<circ> (fa \<circ> g) \<in> CofGroups.Ex1
inv upOne \<circ> (fa \<circ> g) = inv upOne \<circ> fa \<circ> g
fa \<circ> g \<in> CofGroups.Ex1

goal (1 subgoal):
 1. inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv upOne \<circ> fa \<circ> g \<in> CofGroups.Ex1

goal:
No subgoals!
[PROOF STEP]
qed