[STATEMENT]
lemma lift_preserves_inj:
assumes "inj f"
shows "inj (lift f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (lift f)
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. \<forall>y\<in>UNIV. lift f x = lift f y \<longrightarrow> x = y
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. lift f x = lift f y \<Longrightarrow> x = y
[PROOF STEP]
proof(rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa. lift f x = lift f y \<Longrightarrow> x xa = y xa
[PROOF STEP]
fix inp inp' i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa. lift f x = lift f y \<Longrightarrow> x xa = y xa
[PROOF STEP]
assume *: "lift f inp = lift f inp'"
[PROOF STATE]
proof (state)
this:
lift f inp = lift f inp'

goal (1 subgoal):
 1. \<And>x y xa. lift f x = lift f y \<Longrightarrow> x xa = y xa
[PROOF STEP]
show "inp i = inp' i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inp i = inp' i
[PROOF STEP]
proof(cases "inp i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inp i = None \<Longrightarrow> inp i = inp' i
 2. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
assume inp: "inp i = None"
[PROOF STATE]
proof (state)
this:
inp i = None

goal (2 subgoals):
 1. inp i = None \<Longrightarrow> inp i = inp' i
 2. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
hence "lift f inp i = None"
[PROOF STATE]
proof (prove)
using this:
inp i = None

goal (1 subgoal):
 1. lift f inp i = None
[PROOF STEP]
unfolding lift_def
[PROOF STATE]
proof (prove)
using this:
inp i = None

goal (1 subgoal):
 1. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lift f inp i = None

goal (2 subgoals):
 1. inp i = None \<Longrightarrow> inp i = inp' i
 2. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
hence "lift f inp' i = None"
[PROOF STATE]
proof (prove)
using this:
lift f inp i = None

goal (1 subgoal):
 1. lift f inp' i = None
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
lift f inp i = None
lift f inp = lift f inp'

goal (1 subgoal):
 1. lift f inp' i = None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lift f inp' i = None

goal (2 subgoals):
 1. inp i = None \<Longrightarrow> inp i = inp' i
 2. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
hence "inp' i = None"
[PROOF STATE]
proof (prove)
using this:
lift f inp' i = None

goal (1 subgoal):
 1. inp' i = None
[PROOF STEP]
by(auto simp add: lift_None)
[PROOF STATE]
proof (state)
this:
inp' i = None

goal (2 subgoals):
 1. inp i = None \<Longrightarrow> inp i = inp' i
 2. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
inp' i = None

goal (1 subgoal):
 1. inp i = inp' i
[PROOF STEP]
using inp
[PROOF STATE]
proof (prove)
using this:
inp' i = None
inp i = None

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

goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
assume inp: "inp i = Some v"
[PROOF STATE]
proof (state)
this:
inp i = Some v

goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
hence "lift f inp i = Some (f v)"
[PROOF STATE]
proof (prove)
using this:
inp i = Some v

goal (1 subgoal):
 1. lift f inp i = Some (f v)
[PROOF STEP]
unfolding lift_def
[PROOF STATE]
proof (prove)
using this:
inp i = Some v

goal (1 subgoal):
 1. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = Some (f v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lift f inp i = Some (f v)

goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
hence "lift f inp' i = Some (f v)"
[PROOF STATE]
proof (prove)
using this:
lift f inp i = Some (f v)

goal (1 subgoal):
 1. lift f inp' i = Some (f v)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
lift f inp i = Some (f v)
lift f inp = lift f inp'

goal (1 subgoal):
 1. lift f inp' i = Some (f v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lift f inp' i = Some (f v)

goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lift f inp' i = Some (f v)
[PROOF STEP]
obtain v' where inp': "inp' i = Some v'" and "f v' = f v"
[PROOF STATE]
proof (prove)
using this:
lift f inp' i = Some (f v)

goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>inp' i = Some v'; f v' = f v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lift_def
[PROOF STATE]
proof (prove)
using this:
(case inp' i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = Some (f v)

goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>inp' i = Some v'; f v' = f v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(case_tac "inp' i", auto)
[PROOF STATE]
proof (state)
this:
inp' i = Some v'
f v' = f v

goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
hence "v = v'"
[PROOF STATE]
proof (prove)
using this:
inp' i = Some v'
f v' = f v

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inp' i = Some v'
f v' = f v
inj f

goal (1 subgoal):
 1. v = v'
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
using this:
inp' i = Some v'
f v' = f v
\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. f x = f y \<longrightarrow> x = y

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

goal (1 subgoal):
 1. \<And>a. inp i = Some a \<Longrightarrow> inp i = inp' i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = v'

goal (1 subgoal):
 1. inp i = inp' i
[PROOF STEP]
using inp inp'
[PROOF STATE]
proof (prove)
using this:
v = v'
inp i = Some v
inp' i = Some v'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inp i = inp' i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma liftAll_cong[fundef_cong]:
assumes "\<And> i v. inp i = Some v \<Longrightarrow> phi v = phi' v"
shows "liftAll phi inp = liftAll phi' inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll phi inp = liftAll phi' inp
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v. inp i = Some v \<longrightarrow> phi v) = (\<forall>i v. inp i = Some v \<longrightarrow> phi' v)
[PROOF STEP]
apply((rule iff_allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i v. (inp i = Some v \<longrightarrow> phi v) = (inp i = Some v \<longrightarrow> phi' v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inp ?i = Some ?v \<Longrightarrow> phi ?v = phi' ?v

goal (1 subgoal):
 1. \<And>i v. (inp i = Some v \<longrightarrow> phi v) = (inp i = Some v \<longrightarrow> phi' v)
[PROOF STEP]
by simp


[STATEMENT]
lemma liftAll2_cong[fundef_cong]:
assumes "\<And> i v1 v2. \<lbrakk>inp1 i = Some v1; inp2 i = Some v2\<rbrakk> \<Longrightarrow> phi v1 v2 = phi' v1 v2"
shows "liftAll2 phi inp1 inp2 = liftAll2 phi' inp1 inp2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 phi inp1 inp2 = liftAll2 phi' inp1 inp2
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v1 v2. inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> phi v1 v2) = (\<forall>i v1 v2. inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> phi' v1 v2)
[PROOF STEP]
apply((rule iff_allI)+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i v1 v2. (inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> phi v1 v2) = (inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> phi' v1 v2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inp1 ?i = Some ?v1.0; inp2 ?i = Some ?v2.0\<rbrakk> \<Longrightarrow> phi ?v1.0 ?v2.0 = phi' ?v1.0 ?v2.0

goal (1 subgoal):
 1. \<And>i v1 v2. (inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> phi v1 v2) = (inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> phi' v1 v2)
[PROOF STEP]
by blast


[STATEMENT]
lemma lift_ident: "lift (\<lambda>v. v) inp = inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift (\<lambda>v. v) inp = inp
[PROOF STEP]
by(unfold lift_def, rule ext, case_tac "inp i", auto)


[STATEMENT]
lemma lift_id[simp]:
"lift id inp = inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift id inp = inp
[PROOF STEP]
unfolding lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (id v)) = inp
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. (case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (id v)) = inp i
[PROOF STEP]
by(case_tac "inp i", auto)


[STATEMENT]
lemma lift_comp: "lift g (lift f inp) = lift (g o f) inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift g (lift f inp) = lift (g \<circ> f) inp
[PROOF STEP]
by(unfold lift_def o_def, rule ext, case_tac "inp i", auto)


[STATEMENT]
lemma liftAll_mono:
assumes "\<And> v. phi v \<Longrightarrow> chi v" and "liftAll phi inp"
shows "liftAll chi inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll chi inp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
phi ?v \<Longrightarrow> chi ?v
liftAll phi inp

goal (1 subgoal):
 1. liftAll chi inp
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
phi ?v \<Longrightarrow> chi ?v
\<forall>i v. inp i = Some v \<longrightarrow> phi v

goal (1 subgoal):
 1. \<forall>i v. inp i = Some v \<longrightarrow> chi v
[PROOF STEP]
by blast


[STATEMENT]
lemma liftAll_True: "liftAll (\<lambda>v. True) inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll (\<lambda>v. True) inp
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i v. inp i = Some v \<longrightarrow> True
[PROOF STEP]
by auto


[STATEMENT]
lemma liftAll_lift_comp:  "liftAll phi (lift f inp) = liftAll (phi o f) inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll phi (lift f inp) = liftAll (phi \<circ> f) inp
[PROOF STEP]
unfolding liftAll_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v. lift f inp i = Some v \<longrightarrow> phi v) = (\<forall>i v. inp i = Some v \<longrightarrow> phi (f v))
[PROOF STEP]
by (metis (mono_tags, lifting) lift_Some lift_def option.inject option.simps(5))


[STATEMENT]
lemma liftAll_lift_ext:
"liftAll (\<lambda> x. f x = g x) inp = (lift f inp = lift g inp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll (\<lambda>x. f x = g x) inp = (lift f inp = lift g inp)
[PROOF STEP]
unfolding lift_def liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v. inp i = Some v \<longrightarrow> f v = g v) = ((\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = (\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (g v)))
[PROOF STEP]
by (auto simp: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma liftAll_and:
"liftAll (\<lambda> x. phi x \<and> chi x) inp = (liftAll phi inp \<and> liftAll chi inp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll (\<lambda>x. phi x \<and> chi x) inp = (liftAll phi inp \<and> liftAll chi inp)
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v. inp i = Some v \<longrightarrow> phi v \<and> chi v) = ((\<forall>i v. inp i = Some v \<longrightarrow> phi v) \<and> (\<forall>i v. inp i = Some v \<longrightarrow> chi v))
[PROOF STEP]
by blast


[STATEMENT]
lemma liftAll_mp:
assumes "liftAll (\<lambda> v. phi v \<longrightarrow> chi v) inp" and "liftAll phi inp"
shows "liftAll chi inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll chi inp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>v. phi v \<longrightarrow> chi v) inp
liftAll phi inp

goal (1 subgoal):
 1. liftAll chi inp
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i v. inp i = Some v \<longrightarrow> phi v \<longrightarrow> chi v
\<forall>i v. inp i = Some v \<longrightarrow> phi v

goal (1 subgoal):
 1. \<forall>i v. inp i = Some v \<longrightarrow> chi v
[PROOF STEP]
by auto


[STATEMENT]
lemma sameDom_refl: "sameDom inp inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom inp inp
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (inp i = None) = (inp i = None)
[PROOF STEP]
by auto


[STATEMENT]
lemma sameDom_sym:
"sameDom inp inp' = sameDom inp' inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom inp inp' = sameDom inp' inp
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. (inp i = None) = (inp' i = None)) = (\<forall>i. (inp' i = None) = (inp i = None))
[PROOF STEP]
by auto


[STATEMENT]
lemma sameDom_trans:
"\<lbrakk>sameDom inp inp'; sameDom inp' inp''\<rbrakk> \<Longrightarrow> sameDom inp inp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sameDom inp inp'; sameDom inp' inp''\<rbrakk> \<Longrightarrow> sameDom inp inp''
[PROOF STEP]
unfolding sameDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. (inp i = None) = (inp' i = None); \<forall>i. (inp' i = None) = (inp'' i = None)\<rbrakk> \<Longrightarrow> \<forall>i. (inp i = None) = (inp'' i = None)
[PROOF STEP]
by auto


[STATEMENT]
lemma sameDom_lift1:
"sameDom inp (lift f inp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom inp (lift f inp)
[PROOF STEP]
unfolding sameDom_def lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (inp i = None) = ((case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = None)
[PROOF STEP]
by (auto simp: option.case_eq_if)


[STATEMENT]
lemma sameDom_lift2:
"sameDom (lift f inp) inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom (lift f inp) inp
[PROOF STEP]
unfolding sameDom_def lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. ((case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = None) = (inp i = None)
[PROOF STEP]
by (auto simp: option.case_eq_if)


[STATEMENT]
lemma sameDom_lift_simp1[simp]:
"sameDom inp (lift f inp') = sameDom inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom inp (lift f inp') = sameDom inp inp'
[PROOF STEP]
unfolding sameDom_def lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. (inp i = None) = ((case inp' i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = None)) = (\<forall>i. (inp i = None) = (inp' i = None))
[PROOF STEP]
by (force simp: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma sameDom_lift_simp2[simp]:
"sameDom (lift f inp) inp' = sameDom inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom (lift f inp) inp' = sameDom inp inp'
[PROOF STEP]
unfolding sameDom_def lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i. ((case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = None) = (inp' i = None)) = (\<forall>i. (inp i = None) = (inp' i = None))
[PROOF STEP]
by (force simp: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma lift_preserves_sameDom:
assumes "sameDom inp inp'"
shows "sameDom (lift f inp) (lift g inp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom (lift f inp) (lift g inp')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp inp'

goal (1 subgoal):
 1. sameDom (lift f inp) (lift g inp')
[PROOF STEP]
unfolding sameDom_def lift_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp i = None) = (inp' i = None)

goal (1 subgoal):
 1. \<forall>i. ((case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = None) = ((case inp' i of None \<Rightarrow> None | Some v \<Rightarrow> Some (g v)) = None)
[PROOF STEP]
by (force simp: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma comp2_simp[simp]:
"(h o2 (f,g)) x y = h (f x) (g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h o2 (f,g)) x y = h (f x) (g y)
[PROOF STEP]
unfolding comp2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h (f x) (g y) = h (f x) (g y)
[PROOF STEP]
by simp


[STATEMENT]
lemma comp2_comp:
"((h o2 (f,g)) o2 (f',g')) = (h o2 (f o f', g o g'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h o2 (f,g) o2 (f',g') = h o2 (f \<circ> f',g \<circ> g')
[PROOF STEP]
unfolding comp_def[abs_def] comp2_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. h (f (f' x)) (g (g' y))) = (\<lambda>x y. h (f (f' x)) (g (g' y)))
[PROOF STEP]
by auto


[STATEMENT]
lemma liftAll_imp_liftAll2:
assumes "liftAll (\<lambda>v. \<forall> v'. phi v v') inp"
shows "liftAll2 phi inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 phi inp inp'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
liftAll (\<lambda>v. \<forall>v'. phi v v') inp

goal (1 subgoal):
 1. liftAll2 phi inp inp'
[PROOF STEP]
unfolding liftAll_def liftAll2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i v. inp i = Some v \<longrightarrow> All (phi v)

goal (1 subgoal):
 1. \<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2
[PROOF STEP]
by auto


[STATEMENT]
lemma liftAll2_mono:
assumes "\<And> v v'. phi v v' \<Longrightarrow> chi v v'" and "liftAll2 phi inp inp'"
shows "liftAll2 chi inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 chi inp inp'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
phi ?v ?v' \<Longrightarrow> chi ?v ?v'
liftAll2 phi inp inp'

goal (1 subgoal):
 1. liftAll2 chi inp inp'
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
using this:
phi ?v ?v' \<Longrightarrow> chi ?v ?v'
\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2

goal (1 subgoal):
 1. \<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> chi v1 v2
[PROOF STEP]
by blast


[STATEMENT]
lemma liftAll2_True: "liftAll2 (\<lambda> v v'. True) inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 (\<lambda>v v'. True) inp inp'
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> True
[PROOF STEP]
by auto


[STATEMENT]
lemma liftAll2_lift_comp2:
"liftAll2 phi (lift f1 inp1) (lift f2 inp2) =
 liftAll2 (phi o2 (f1,f2)) inp1 inp2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 phi (lift f1 inp1) (lift f2 inp2) = liftAll2 (phi o2 (f1,f2)) inp1 inp2
[PROOF STEP]
unfolding liftAll2_def lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v1 v2. (case inp1 i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f1 v)) = Some v1 \<and> (case inp2 i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f2 v)) = Some v2 \<longrightarrow> phi v1 v2) = (\<forall>i v1 v2. inp1 i = Some v1 \<and> inp2 i = Some v2 \<longrightarrow> (phi o2 (f1,f2)) v1 v2)
[PROOF STEP]
by (auto simp: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma lift_imp_sameDom:
"lift f inp = lift f inp' \<Longrightarrow> sameDom inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift f inp = lift f inp' \<Longrightarrow> sameDom inp inp'
[PROOF STEP]
unfolding lift_def sameDom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = (\<lambda>i. case inp' i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) \<Longrightarrow> \<forall>i. (inp i = None) = (inp' i = None)
[PROOF STEP]
by (force simp: fun_eq_iff option.case_eq_if split: if_splits)


[STATEMENT]
lemma lift_lift2:
"lift f (lift2 g inp' inp) =
 lift2 (\<lambda> v' v. f (g v' v)) inp' inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift f (lift2 g inp' inp) = lift2 (\<lambda>v' v. f (g v' v)) inp' inp
[PROOF STEP]
unfolding lift_def lift2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. case case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (g v' v) of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = (\<lambda>i. case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f (g v' v)))
[PROOF STEP]
by (force simp: option.case_eq_if split: if_splits)


[STATEMENT]
lemma lift2_left[simp]:
assumes "sameDom inp' inp"
shows "lift2 (\<lambda> v' v. v') inp' inp = inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift2 (\<lambda>v' v. v') inp' inp = inp'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp' inp

goal (1 subgoal):
 1. lift2 (\<lambda>v' v. v') inp' inp = inp'
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp' i = None) = (inp i = None)

goal (1 subgoal):
 1. (\<lambda>i. case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some v') = inp'
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if) metis


[STATEMENT]
lemma lift2_right[simp]:
assumes "sameDom inp' inp"
shows "lift2 (\<lambda> v' v. v) inp' inp = inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lift2 (\<lambda>v' v. v) inp' inp = inp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp' inp

goal (1 subgoal):
 1. lift2 (\<lambda>v' v. v) inp' inp = inp
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp' i = None) = (inp i = None)

goal (1 subgoal):
 1. (\<lambda>i. case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some v) = inp
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma lift2_preserves_sameDom:
assumes "sameDom inp' inp1'" and "sameDom inp inp1"
shows "sameDom (lift2 f inp' inp) (lift2 g inp1' inp1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom (lift2 f inp' inp) (lift2 g inp1' inp1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp' inp1'
sameDom inp inp1

goal (1 subgoal):
 1. sameDom (lift2 f inp' inp) (lift2 g inp1' inp1)
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp' i = None) = (inp1' i = None)
\<forall>i. (inp i = None) = (inp1 i = None)

goal (1 subgoal):
 1. \<forall>i. ((case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None) = ((case (inp1' i, inp1 i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (g v' v)) = None)
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma sameDom_lift2_1:
assumes "sameDom inp' inp"
shows
"sameDom inp' (lift2 f inp' inp) \<and>
 sameDom inp (lift2 f inp' inp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom inp' (lift2 f inp' inp) \<and> sameDom inp (lift2 f inp' inp)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp' inp

goal (1 subgoal):
 1. sameDom inp' (lift2 f inp' inp) \<and> sameDom inp (lift2 f inp' inp)
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp' i = None) = (inp i = None)

goal (1 subgoal):
 1. (\<forall>i. (inp' i = None) = ((case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None)) \<and> (\<forall>i. (inp i = None) = ((case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None))
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma sameDom_lift2_2:
assumes "sameDom inp' inp"
shows
"sameDom (lift2 f inp' inp) inp' \<and>
 sameDom (lift2 f inp' inp) inp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom (lift2 f inp' inp) inp' \<and> sameDom (lift2 f inp' inp) inp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp' inp

goal (1 subgoal):
 1. sameDom (lift2 f inp' inp) inp' \<and> sameDom (lift2 f inp' inp) inp
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp' i = None) = (inp i = None)

goal (1 subgoal):
 1. (\<forall>i. ((case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None) = (inp' i = None)) \<and> (\<forall>i. ((case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None) = (inp i = None))
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma sameDom_lift2_simp1[simp]:
assumes "sameDom inp1' inp1"
shows "sameDom inp (lift2 f inp1' inp1) = sameDom inp inp1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom inp (lift2 f inp1' inp1) = sameDom inp inp1'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp1' inp1

goal (1 subgoal):
 1. sameDom inp (lift2 f inp1' inp1) = sameDom inp inp1'
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp1' i = None) = (inp1 i = None)

goal (1 subgoal):
 1. (\<forall>i. (inp i = None) = ((case (inp1' i, inp1 i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None)) = (\<forall>i. (inp i = None) = (inp1' i = None))
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if) (metis not_Some_eq)


[STATEMENT]
lemma sameDom_lift2_simp2[simp]:
assumes "sameDom inp' inp"
shows "sameDom (lift2 f inp' inp) inp1 = sameDom inp' inp1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sameDom (lift2 f inp' inp) inp1 = sameDom inp' inp1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sameDom inp' inp

goal (1 subgoal):
 1. sameDom (lift2 f inp' inp) inp1 = sameDom inp' inp1
[PROOF STEP]
unfolding sameDom_def lift2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (inp' i = None) = (inp i = None)

goal (1 subgoal):
 1. (\<forall>i. ((case (inp' i, inp i) of (None, b) \<Rightarrow> None | (Some v', None) \<Rightarrow> None | (Some v', Some v) \<Rightarrow> Some (f v' v)) = None) = (inp1 i = None)) = (\<forall>i. (inp' i = None) = (inp1 i = None))
[PROOF STEP]
by (simp add: fun_eq_iff option.case_eq_if) (metis not_Some_eq)


[STATEMENT]
lemma liftAll2_lift_ext:
"(sameDom inp inp' \<and> liftAll2 (\<lambda> v v'. f v = f v') inp inp') =
 (lift f inp = lift f inp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sameDom inp inp' \<and> liftAll2 (\<lambda>v v'. f v = f v') inp inp') = (lift f inp = lift f inp')
[PROOF STEP]
unfolding sameDom_def lift_def liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> f v1 = f v2)) = ((\<lambda>i. case inp i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)) = (\<lambda>i. case inp' i of None \<Rightarrow> None | Some v \<Rightarrow> Some (f v)))
[PROOF STEP]
by (force simp add: fun_eq_iff option.case_eq_if)


[STATEMENT]
lemma liftAll2_and:
"liftAll2 (\<lambda> v v'. phi v v' \<and> chi v v') inp inp' =
(liftAll2 phi inp inp' \<and> liftAll2 chi inp inp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 (\<lambda>v v'. phi v v' \<and> chi v v') inp inp' = (liftAll2 phi inp inp' \<and> liftAll2 chi inp inp')
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2 \<and> chi v1 v2) = ((\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2) \<and> (\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> chi v1 v2))
[PROOF STEP]
by force


[STATEMENT]
lemma liftAll2_mp:
assumes "liftAll2 (\<lambda> v v'. phi v v' \<longrightarrow> chi v v') inp inp'" and "liftAll2 phi inp inp'"
shows "liftAll2 chi inp inp'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftAll2 chi inp inp'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
liftAll2 (\<lambda>v v'. phi v v' \<longrightarrow> chi v v') inp inp'
liftAll2 phi inp inp'

goal (1 subgoal):
 1. liftAll2 chi inp inp'
[PROOF STEP]
unfolding liftAll2_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2 \<longrightarrow> chi v1 v2
\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2

goal (1 subgoal):
 1. \<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> chi v1 v2
[PROOF STEP]
by auto


[STATEMENT]
lemma sameDom_and_liftAll2_iff:
"(sameDom inp inp' \<and> liftAll2 phi inp inp') =
 (\<forall> i. (inp i = None \<and> inp' i = None) \<or>
         (\<exists> v v'. inp i = Some v \<and> inp' i = Some v' \<and> phi v v'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sameDom inp inp' \<and> liftAll2 phi inp inp') = (\<forall>i. inp i = None \<and> inp' i = None \<or> (\<exists>v v'. inp i = Some v \<and> inp' i = Some v' \<and> phi v v'))
[PROOF STEP]
unfolding sameDom_def liftAll2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>i. (inp i = None) = (inp' i = None)) \<and> (\<forall>i v1 v2. inp i = Some v1 \<and> inp' i = Some v2 \<longrightarrow> phi v1 v2)) = (\<forall>i. inp i = None \<and> inp' i = None \<or> (\<exists>v v'. inp i = Some v \<and> inp' i = Some v' \<and> phi v v'))
[PROOF STEP]
apply (auto simp add: fun_eq_iff option.case_eq_if)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>\<forall>i. inp i = None \<and> inp' i = None \<or> (\<exists>v. inp i = Some v \<and> (\<exists>v'. inp' i = Some v' \<and> phi v v')); inp i = Some v1; inp' i = Some v2\<rbrakk> \<Longrightarrow> phi v1 v2
[PROOF STEP]
using option.sel
[PROOF STATE]
proof (prove)
using this:
the (Some ?x2.0) = ?x2.0

goal (1 subgoal):
 1. \<And>i v1 v2. \<lbrakk>\<forall>i. inp i = None \<and> inp' i = None \<or> (\<exists>v. inp i = Some v \<and> (\<exists>v'. inp' i = Some v' \<and> phi v v')); inp i = Some v1; inp' i = Some v2\<rbrakk> \<Longrightarrow> phi v1 v2
[PROOF STEP]
by fastforce


[STATEMENT]
lemma tree_induct:
fixes phi::"('index,'bindex)tree \<Rightarrow> bool" and T::"('index,'bindex)tree"
assumes
  "\<And> inp binp. \<lbrakk>liftAll phi inp; liftAll phi binp\<rbrakk> \<Longrightarrow> phi (Branch inp binp)"
shows "phi T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>liftAll phi ?inp; liftAll phi ?binp\<rbrakk> \<Longrightarrow> phi (Branch ?inp ?binp)

goal (1 subgoal):
 1. phi T
[PROOF STEP]
unfolding liftAll_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>i v. ?inp i = Some v \<longrightarrow> phi v; \<forall>i v. ?binp i = Some v \<longrightarrow> phi v\<rbrakk> \<Longrightarrow> phi (Branch ?inp ?binp)

goal (1 subgoal):
 1. phi T
[PROOF STEP]
by (induct T) (simp, metis rangeI)


[STATEMENT]
lemma treeLess_induct:
fixes phi::"('index,'bindex)tree \<Rightarrow> bool" and
      T::"('index,'bindex)tree"
assumes "\<And> T'. (\<And> T. (T,T') \<in> treeLess \<Longrightarrow> phi T) \<Longrightarrow> phi T'"
shows "phi T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi T
[PROOF STEP]
apply(induct rule: tree_induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>liftAll phi inp; liftAll phi binp\<rbrakk> \<Longrightarrow> phi (Branch inp binp)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<And>T. (T, ?T') \<in> treeLess \<Longrightarrow> phi T) \<Longrightarrow> phi ?T'

goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>liftAll phi inp; liftAll phi binp\<rbrakk> \<Longrightarrow> phi (Branch inp binp)
[PROOF STEP]
unfolding treeLess_def liftAll_def
[PROOF STATE]
proof (prove)
using this:
(\<And>T. (T, ?T') \<in> {(T, T'). \<exists>inp binp i j. T' = Branch inp binp \<and> (inp i = Some T \<or> binp j = Some T)} \<Longrightarrow> phi T) \<Longrightarrow> phi ?T'

goal (1 subgoal):
 1. \<And>inp binp. \<lbrakk>\<forall>i v. inp i = Some v \<longrightarrow> phi v; \<forall>i v. binp i = Some v \<longrightarrow> phi v\<rbrakk> \<Longrightarrow> phi (Branch inp binp)
[PROOF STEP]
by simp (metis tree.inject)


[STATEMENT]
lemma treeLess_wf: "wf treeLess"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf treeLess
[PROOF STEP]
unfolding wf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> treeLess \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> All P
[PROOF STEP]
using treeLess_induct
[PROOF STATE]
proof (prove)
using this:
(\<And>T'. (\<And>T. (T, T') \<in> treeLess \<Longrightarrow> ?phi T) \<Longrightarrow> ?phi T') \<Longrightarrow> ?phi ?T

goal (1 subgoal):
 1. \<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> treeLess \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> All P
[PROOF STEP]
by blast


[STATEMENT]
lemma Least_Max:
assumes phi: "phi (n::nat)" and fin: "finite {n. phi n}"
shows "(LEAST m. \<forall> n. phi n \<longrightarrow> n \<le> m) =
       Max {n. phi n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST m. \<forall>n. phi n \<longrightarrow> n \<le> m) = Max {n. phi n}
[PROOF STEP]
using assms Max_in
[PROOF STATE]
proof (prove)
using this:
phi n
finite {n. phi n}
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A

goal (1 subgoal):
 1. (LEAST m. \<forall>n. phi n \<longrightarrow> n \<le> m) = Max {n. phi n}
[PROOF STEP]
by (intro Least_equality) auto


[STATEMENT]
lemma tri_caseE:
  "\<lbrakk>\<lbrakk>\<not>P;\<not>Q\<rbrakk> \<Longrightarrow> R; P \<Longrightarrow> R; \<lbrakk>\<not>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R; P \<Longrightarrow> R; \<lbrakk>\<not> P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by auto


[STATEMENT]
lemma opt_tagI: "opt_tag x x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opt_tag x x
[PROOF STEP]
unfolding opt_tag_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x
[PROOF STEP]
by simp


[STATEMENT]
lemma opt_tagD: "opt_tag x y \<Longrightarrow> x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. opt_tag x y \<Longrightarrow> x = y
[PROOF STEP]
unfolding opt_tag_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y \<Longrightarrow> x = y
[PROOF STEP]
by simp


[STATEMENT]
lemma wt_sym_gt_0: "wt_sym f > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < wt_sym f
[PROOF STEP]
by (rule less_le_trans[OF \<epsilon>_gt_0 wt_sym_ge_\<epsilon>])


[STATEMENT]
lemma arity_sym_ne_infinity_if_\<delta>_gt_0: "\<delta> > 0 \<Longrightarrow> arity_sym f \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<delta> \<Longrightarrow> arity_sym f \<noteq> \<infinity>
[PROOF STEP]
by (metis arity_hd.simps(2) arity_hd_ne_infinity_if_\<delta>_gt_0)


[STATEMENT]
lemma arity_var_ne_infinity_if_\<delta>_gt_0: "\<delta> > 0 \<Longrightarrow> arity_var x \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<delta> \<Longrightarrow> arity_var x \<noteq> \<infinity>
[PROOF STEP]
by (metis arity_hd.simps(1) arity_hd_ne_infinity_if_\<delta>_gt_0)


[STATEMENT]
lemma arity_ne_infinity_if_\<delta>_gt_0: "\<delta> > 0 \<Longrightarrow> arity s \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<delta> \<Longrightarrow> arity s \<noteq> \<infinity>
[PROOF STEP]
unfolding arity_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<delta> \<Longrightarrow> arity_hd (head s) - enat (num_args s) \<noteq> \<infinity>
[PROOF STEP]
by (induct s rule: tm_induct_apps)
    (metis arity_hd_ne_infinity_if_\<delta>_gt_0 enat.distinct(2) enat.exhaust idiff_enat_enat)


[STATEMENT]
lemma extf_ext: "ext (extf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ext (extf f)
[PROOF STEP]
by (rule ext_irrefl.axioms(1)[OF extf_ext_irrefl])


[STATEMENT]
lemma extf_ext_compat_list: "ext_compat_list (extf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ext_compat_list (extf f)
[PROOF STEP]
using extf_ext_compat_list_strong
[PROOF STATE]
proof (prove)
using this:
ext_compat_list_strong (extf ?f)

goal (1 subgoal):
 1. ext_compat_list (extf f)
[PROOF STEP]
by (simp add: ext_compat_list_axioms_def ext_compat_list_def ext_compat_list_strong.compat_list
    ext_compat_list_strong_def ext_singleton.axioms(1))


[STATEMENT]
lemma extf_ext_wf_bounded: "ext_wf_bounded (extf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ext_wf_bounded (extf f)
[PROOF STEP]
unfolding ext_wf_bounded_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ext_irrefl_before_trans (extf f) \<and> ext_hd_or_tl (extf f)
[PROOF STEP]
using extf_ext_irrefl_before_trans extf_ext_hd_or_tl
[PROOF STATE]
proof (prove)
using this:
ext_irrefl_before_trans (extf ?f)
ext_hd_or_tl (extf ?f)

goal (1 subgoal):
 1. ext_irrefl_before_trans (extf f) \<and> ext_hd_or_tl (extf f)
[PROOF STEP]
by simp


[STATEMENT]
lemma extf_singleton_nil_if_\<delta>_eq_\<epsilon>: "\<delta> = \<epsilon> \<Longrightarrow> extf f gt [s] []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta> = \<epsilon> \<Longrightarrow> extf f gt [s] []
[PROOF STEP]
by (rule extf_snoc_if_\<delta>_eq_\<epsilon>[of _ _ "[]", simplified])


[STATEMENT]
lemma (in subgroup) nat_pow_closed [simp,intro]: "a \<in> H \<Longrightarrow> pow G a (n::nat) \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> H \<Longrightarrow> a [^] n \<in> H
[PROOF STEP]
by (induction n) (auto simp: nat_pow_def)


[STATEMENT]
lemma nat_pow_modify_carrier: "a [^]\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> b = a [^]\<^bsub>G\<^esub> (b::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^]\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> b = a [^]\<^bsub>G\<^esub> b
[PROOF STEP]
by (simp add: nat_pow_def)


[STATEMENT]
lemma (in group) subgroup_card_dvd_group_ord:
  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]
using Coset.group.lagrange[of G H] assms group_axioms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Group.group G; subgroup H G\<rbrakk> \<Longrightarrow> card (rcosets H) * card H = order G
subgroup H G
Group.group G

goal (1 subgoal):
 1. card H dvd order G
[PROOF STEP]
by (metis dvd_triv_right)


[STATEMENT]
lemma (in group) subgroup_card_eq_order:
  assumes "subgroup H G"
  shows "card H = order (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H = order (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H = card (carrier (G\<lparr>carrier := H\<rparr>))
[PROOF STEP]
by simp


[STATEMENT]
lemma (in group) finite_subgroup_card_neq_0:
  assumes "subgroup H G" "finite H"
  shows "card H \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H \<noteq> 0
[PROOF STEP]
using subgroup_nonempty assms
[PROOF STATE]
proof (prove)
using this:
\<not> subgroup {} ?G
subgroup H G
finite H

goal (1 subgoal):
 1. card H \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma (in group) subgroup_order_dvd_group_order:
  assumes "subgroup H G"
  shows "order (G\<lparr>carrier := H\<rparr>) dvd order G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (G\<lparr>carrier := H\<rparr>) dvd order G
[PROOF STEP]
by (metis subgroup_card_dvd_group_ord[of H] assms subgroup_card_eq_order)


[STATEMENT]
lemma (in group) sub_subgroup_dvd_card:
  assumes "subgroup H G" "subgroup J G" "J \<subseteq> H"
  shows "card J dvd card H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card J dvd card H
[PROOF STEP]
by (metis subgroup_incl[of J H] subgroup_card_eq_order[of H]
            group.subgroup_card_dvd_group_ord[of "(G\<lparr>carrier := H\<rparr>)" J] assms
            subgroup.subgroup_is_group[of H G] group_axioms)


[STATEMENT]
lemma (in group) inter_subgroup_dvd_card:
  assumes "subgroup H G" "subgroup J G"
  shows "card (H \<inter> J) dvd card H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (H \<inter> J) dvd card H
[PROOF STEP]
using subgroups_Inter_pair[of H J] assms sub_subgroup_dvd_card[of H "H \<inter> J"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subgroup H G; subgroup J G\<rbrakk> \<Longrightarrow> subgroup (H \<inter> J) G
subgroup H G
subgroup J G
\<lbrakk>subgroup H G; subgroup (H \<inter> J) G; H \<inter> J \<subseteq> H\<rbrakk> \<Longrightarrow> card (H \<inter> J) dvd card H

goal (1 subgoal):
 1. card (H \<inter> J) dvd card H
[PROOF STEP]
by blast


[STATEMENT]
lemma (in group) subgroups_card_coprime_inter_card_one:
  assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
  shows "card (H \<inter> J) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (H \<inter> J) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (H \<inter> J) = 1
[PROOF STEP]
from assms inter_subgroup_dvd_card
[PROOF STATE]
proof (chain)
picking this:
subgroup H G
subgroup J G
coprime (card H) (card J)
\<lbrakk>subgroup ?H G; subgroup ?J G\<rbrakk> \<Longrightarrow> card (?H \<inter> ?J) dvd card ?H
[PROOF STEP]
have "is_unit (card (H \<inter> J))"
[PROOF STATE]
proof (prove)
using this:
subgroup H G
subgroup J G
coprime (card H) (card J)
\<lbrakk>subgroup ?H G; subgroup ?J G\<rbrakk> \<Longrightarrow> card (?H \<inter> ?J) dvd card ?H

goal (1 subgoal):
 1. is_unit (card (H \<inter> J))
[PROOF STEP]
unfolding coprime_def
[PROOF STATE]
proof (prove)
using this:
subgroup H G
subgroup J G
\<forall>c. c dvd card H \<longrightarrow> c dvd card J \<longrightarrow> is_unit c
\<lbrakk>subgroup ?H G; subgroup ?J G\<rbrakk> \<Longrightarrow> card (?H \<inter> ?J) dvd card ?H

goal (1 subgoal):
 1. is_unit (card (H \<inter> J))
[PROOF STEP]
by (metis assms(3) coprime_common_divisor inf_commute)
[PROOF STATE]
proof (state)
this:
is_unit (card (H \<inter> J))

goal (1 subgoal):
 1. card (H \<inter> J) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_unit (card (H \<inter> J))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_unit (card (H \<inter> J))

goal (1 subgoal):
 1. card (H \<inter> J) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (H \<inter> J) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) coset_neq_imp_empty_inter:
  assumes "subgroup H G" "a \<in> carrier G" "b \<in> carrier G"
  shows "H #> a \<noteq> H #> b \<Longrightarrow> (H #> a) \<inter> (H #> b) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H #> a \<noteq> H #> b \<Longrightarrow> (H #> a) \<inter> (H #> b) = {}
[PROOF STEP]
by (metis Int_emptyI assms repr_independence)


[STATEMENT]
lemma (in comm_group) subgroup_is_comm_group:
  assumes "subgroup H G"
  shows "comm_group (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
unfolding comm_group_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>) \<and> Group.group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>)
 2. Group.group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
interpret H: subgroup H G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>)
 2. Group.group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
interpret H: submonoid H G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submonoid H G
[PROOF STEP]
using H.subgroup_is_submonoid
[PROOF STATE]
proof (prove)
using this:
submonoid H G

goal (1 subgoal):
 1. submonoid H G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>)
 2. Group.group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
show "Group.group (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.group (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Group.group (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
show "comm_monoid (G\<lparr>carrier := H\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
using submonoid_is_comm_monoid H.submonoid_axioms
[PROOF STATE]
proof (prove)
using this:
submonoid ?H G \<Longrightarrow> Group.comm_monoid (G\<lparr>carrier := ?H\<rparr>)
submonoid H G

goal (1 subgoal):
 1. Group.comm_monoid (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Group.comm_monoid (G\<lparr>carrier := H\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) pow_int_mod_ord:
  assumes [simp]:"a \<in> carrier G" "ord a \<noteq> 0"
  shows "a [^] (n::int) = a [^] (n mod ord a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q r. \<lbrakk>q = n div int (ord a); r = n mod int (ord a); n = q * int (ord a) + r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mod_div_decomp
[PROOF STATE]
proof (prove)
using this:
(\<And>q r. \<lbrakk>q = ?a div ?b; r = ?a mod ?b; ?a = q * ?b + r\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>q r. \<lbrakk>q = n div int (ord a); r = n mod int (ord a); n = q * int (ord a) + r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q = n div int (ord a)
r = n mod int (ord a)
n = q * int (ord a) + r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
hence "a [^] n = (a [^] int (ord a)) [^] q \<otimes> a [^] r"
[PROOF STATE]
proof (prove)
using this:
q = n div int (ord a)
r = n mod int (ord a)
n = q * int (ord a) + r

goal (1 subgoal):
 1. a [^] n = (a [^] int (ord a)) [^] q \<otimes> a [^] r
[PROOF STEP]
using assms(1) int_pow_mult int_pow_pow
[PROOF STATE]
proof (prove)
using this:
q = n div int (ord a)
r = n mod int (ord a)
n = q * int (ord a) + r
a \<in> carrier G
?x \<in> carrier G \<Longrightarrow> ?x [^] (?i + ?j) = ?x [^] ?i \<otimes> ?x [^] ?j
?x \<in> carrier G \<Longrightarrow> (?x [^] ?n) [^] ?m = ?x [^] (?n * ?m)

goal (1 subgoal):
 1. a [^] n = (a [^] int (ord a)) [^] q \<otimes> a [^] r
[PROOF STEP]
by (metis mult_of_nat_commute)
[PROOF STATE]
proof (state)
this:
a [^] n = (a [^] int (ord a)) [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a [^] n = (a [^] int (ord a)) [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
have "\<dots> = \<one> [^] q \<otimes> a [^] r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a [^] int (ord a)) [^] q \<otimes> a [^] r = \<one> [^] q \<otimes> a [^] r
[PROOF STEP]
by (simp add: int_pow_int)
[PROOF STATE]
proof (state)
this:
(a [^] int (ord a)) [^] q \<otimes> a [^] r = \<one> [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a [^] int (ord a)) [^] q \<otimes> a [^] r = \<one> [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
have "\<dots> = a [^] r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> [^] q \<otimes> a [^] r = a [^] r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one> [^] q \<otimes> a [^] r = a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a [^] n = a [^] r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a [^] n = a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
using d(2)
[PROOF STATE]
proof (prove)
using this:
a [^] n = a [^] r
r = n mod int (ord a)

goal (1 subgoal):
 1. a [^] n = a [^] (n mod int (ord a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a [^] n = a [^] (n mod int (ord a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) pow_nat_mod_ord:
  assumes [simp]:"a \<in> carrier G" "ord a \<noteq> 0"
  shows "a [^] (n::nat) = a [^] (n mod ord a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
obtain q r where d: "q = n div ord a" "r = n mod ord a" "n = q * ord a + r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q r. \<lbrakk>q = n div ord a; r = n mod ord a; n = q * ord a + r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mod_div_decomp
[PROOF STATE]
proof (prove)
using this:
(\<And>q r. \<lbrakk>q = ?a div ?b; r = ?a mod ?b; ?a = q * ?b + r\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>q r. \<lbrakk>q = n div ord a; r = n mod ord a; n = q * ord a + r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
q = n div ord a
r = n mod ord a
n = q * ord a + r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
hence "a [^] n = (a [^] ord a) [^] q \<otimes> a [^] r"
[PROOF STATE]
proof (prove)
using this:
q = n div ord a
r = n mod ord a
n = q * ord a + r

goal (1 subgoal):
 1. a [^] n = (a [^] ord a) [^] q \<otimes> a [^] r
[PROOF STEP]
using assms(1) nat_pow_mult nat_pow_pow
[PROOF STATE]
proof (prove)
using this:
q = n div ord a
r = n mod ord a
n = q * ord a + r
a \<in> carrier G
?x \<in> carrier G \<Longrightarrow> ?x [^] ?n \<otimes> ?x [^] ?m = ?x [^] (?n + ?m)
?x \<in> carrier G \<Longrightarrow> (?x [^] ?n) [^] ?m = ?x [^] (?n * ?m)

goal (1 subgoal):
 1. a [^] n = (a [^] ord a) [^] q \<otimes> a [^] r
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
a [^] n = (a [^] ord a) [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a [^] n = (a [^] ord a) [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
have "\<dots> = \<one> [^] q \<otimes> a [^] r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a [^] ord a) [^] q \<otimes> a [^] r = \<one> [^] q \<otimes> a [^] r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a [^] ord a) [^] q \<otimes> a [^] r = \<one> [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a [^] ord a) [^] q \<otimes> a [^] r = \<one> [^] q \<otimes> a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
have "\<dots> = a [^] r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one> [^] q \<otimes> a [^] r = a [^] r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one> [^] q \<otimes> a [^] r = a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
a [^] n = a [^] r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a [^] n = a [^] r

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
using d(2)
[PROOF STATE]
proof (prove)
using this:
a [^] n = a [^] r
r = n mod ord a

goal (1 subgoal):
 1. a [^] n = a [^] (n mod ord a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a [^] n = a [^] (n mod ord a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) ord_min:
  assumes "m \<ge> 1" "x \<in> carrier G" "x [^] m = \<one>"
  shows   "ord x \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord x \<le> m
[PROOF STEP]
using assms pow_eq_id
[PROOF STATE]
proof (prove)
using this:
1 \<le> m
x \<in> carrier G
x [^] m = \<one>
?x \<in> carrier G \<Longrightarrow> (?x [^] ?n = \<one>) = (ord ?x dvd ?n)

goal (1 subgoal):
 1. ord x \<le> m
[PROOF STEP]
by auto


[STATEMENT]
lemma (in group) bij_betw_mult_left[intro]:
  assumes [simp]: "x \<in> carrier G"
  shows "bij_betw (\<lambda>y. x \<otimes> y) (carrier G) (carrier G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw ((\<otimes>) x) (carrier G) (carrier G)
[PROOF STEP]
by (intro bij_betwI[where ?g = "\<lambda>y. inv x \<otimes> y"])
     (auto simp: m_assoc [symmetric])


[STATEMENT]
lemma (in subgroup) inv_in_iff:
  assumes "x \<in> carrier G" "group G"
  shows   "inv x \<in> H \<longleftrightarrow> x \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv x \<in> H) = (x \<in> H)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inv x \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
assume "inv x \<in> H"
[PROOF STATE]
proof (state)
this:
inv x \<in> H

goal (2 subgoals):
 1. inv x \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
hence "inv (inv x) \<in> H"
[PROOF STATE]
proof (prove)
using this:
inv x \<in> H

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

goal (2 subgoals):
 1. inv x \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv (inv x) \<in> H

goal (2 subgoals):
 1. inv x \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
have "inv (inv x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (inv x) = x
[PROOF STEP]
by (intro group.inv_inv) (use assms in auto)
[PROOF STATE]
proof (state)
this:
inv (inv x) = x

goal (2 subgoals):
 1. inv x \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
[PROOF STEP]
show "x \<in> H"
[PROOF STATE]
proof (prove)
using this:
x \<in> H

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

goal (1 subgoal):
 1. x \<in> H \<Longrightarrow> inv x \<in> H
[PROOF STEP]
qed auto


[STATEMENT]
lemma (in subgroup) mult_in_cancel_left:
  assumes "y \<in> carrier G" "x \<in> H" "group G"
  shows   "x \<otimes> y \<in> H \<longleftrightarrow> y \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<otimes> y \<in> H) = (y \<in> H)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> y \<in> H
 2. y \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
assume "x \<otimes> y \<in> H"
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<in> H

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> y \<in> H
 2. y \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
hence "inv x \<otimes> (x \<otimes> y) \<in> H"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> y \<in> H

goal (1 subgoal):
 1. inv x \<otimes> (x \<otimes> y) \<in> H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<otimes> y \<in> H
y \<in> carrier G
x \<in> H
Group.group G

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

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> y \<in> H
 2. y \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv x \<otimes> (x \<otimes> y) \<in> H

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> y \<in> H
 2. y \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
have "inv x \<otimes> (x \<otimes> y) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv x \<otimes> (x \<otimes> y) = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier G
x \<in> H
Group.group G

goal (1 subgoal):
 1. inv x \<otimes> (x \<otimes> y) = y
[PROOF STEP]
by (simp add: \<open>x \<otimes> y \<in> H\<close> group.inv_solve_left')
[PROOF STATE]
proof (state)
this:
inv x \<otimes> (x \<otimes> y) = y

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> y \<in> H
 2. y \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<in> H
[PROOF STEP]
show "y \<in> H"
[PROOF STATE]
proof (prove)
using this:
y \<in> H

goal (1 subgoal):
 1. y \<in> H
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
y \<in> H

goal (1 subgoal):
 1. y \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma (in subgroup) mult_in_cancel_right:
  assumes "x \<in> carrier G" "y \<in> H" "group G"
  shows   "x \<otimes> y \<in> H \<longleftrightarrow> x \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<otimes> y \<in> H) = (x \<in> H)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
assume "x \<otimes> y \<in> H"
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<in> H

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
hence "(x \<otimes> y) \<otimes> inv y \<in> H"
[PROOF STATE]
proof (prove)
using this:
x \<otimes> y \<in> H

goal (1 subgoal):
 1. x \<otimes> y \<otimes> inv y \<in> H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<otimes> y \<in> H
x \<in> carrier G
y \<in> H
Group.group G

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

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<otimes> inv y \<in> H

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
have "(x \<otimes> y) \<otimes> inv y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> y \<otimes> inv y = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
y \<in> H
Group.group G

goal (1 subgoal):
 1. x \<otimes> y \<otimes> inv y = x
[PROOF STEP]
by (simp add: \<open>x \<otimes> y \<in> H\<close> group.inv_solve_right')
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<otimes> inv y = x

goal (2 subgoals):
 1. x \<otimes> y \<in> H \<Longrightarrow> x \<in> H
 2. x \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<in> H
[PROOF STEP]
show "x \<in> H"
[PROOF STATE]
proof (prove)
using this:
x \<in> H

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

goal (1 subgoal):
 1. x \<in> H \<Longrightarrow> x \<otimes> y \<in> H
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma (in group) (* Manuel Eberl *)
  assumes "x \<in> carrier G" and "x [^] n = \<one>" and "n > 0"
  shows   ord_le: "ord x \<le> n" and ord_pos: "ord x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord x \<le> n &&& 0 < ord x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ord x \<le> n
 2. 0 < ord x
[PROOF STEP]
have "ord x dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord x dvd n
[PROOF STEP]
using pow_eq_id[of x n] assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G \<Longrightarrow> (x [^] n = \<one>) = (ord x dvd n)
x \<in> carrier G
x [^] n = \<one>
0 < n

goal (1 subgoal):
 1. ord x dvd n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ord x dvd n

goal (2 subgoals):
 1. ord x \<le> n
 2. 0 < ord x
[PROOF STEP]
thus "ord x \<le> n" "ord x > 0"
[PROOF STATE]
proof (prove)
using this:
ord x dvd n

goal (1 subgoal):
 1. ord x \<le> n &&& 0 < ord x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ord x dvd n
x \<in> carrier G
x [^] n = \<one>
0 < n

goal (1 subgoal):
 1. ord x \<le> n &&& 0 < ord x
[PROOF STEP]
by (auto intro: dvd_imp_le)
[PROOF STATE]
proof (state)
this:
ord x \<le> n
0 < ord x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) ord_conv_Least: (* Manuel Eberl *)
  assumes "x \<in> carrier G" "\<exists>n::nat > 0. x [^] n = \<one>"
  shows   "ord x = (LEAST n::nat. 0 < n \<and> x [^] n = \<one>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord x = (LEAST n. 0 < n \<and> x [^] n = \<one>)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ord x \<le> (LEAST n. 0 < n \<and> x [^] n = \<one>)
 2. (LEAST n. 0 < n \<and> x [^] n = \<one>) \<le> ord x
[PROOF STEP]
show "ord x \<le> (LEAST n::nat. 0 < n \<and> x [^] n = \<one>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord x \<le> (LEAST n. 0 < n \<and> x [^] n = \<one>)
[PROOF STEP]
using assms LeastI_ex[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
\<exists>n>0. x [^] n = \<one>
0 < (LEAST n. 0 < n \<and> x [^] n = \<one>) \<and> x [^] (LEAST n. 0 < n \<and> x [^] n = \<one>) = \<one>

goal (1 subgoal):
 1. ord x \<le> (LEAST n. 0 < n \<and> x [^] n = \<one>)
[PROOF STEP]
by (intro ord_le) auto
[PROOF STATE]
proof (state)
this:
ord x \<le> (LEAST n. 0 < n \<and> x [^] n = \<one>)

goal (1 subgoal):
 1. (LEAST n. 0 < n \<and> x [^] n = \<one>) \<le> ord x
[PROOF STEP]
show "ord x \<ge> (LEAST n::nat. 0 < n \<and> x [^] n = \<one>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. 0 < n \<and> x [^] n = \<one>) \<le> ord x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier G
\<exists>n>0. x [^] n = \<one>

goal (1 subgoal):
 1. (LEAST n. 0 < n \<and> x [^] n = \<one>) \<le> ord x
[PROOF STEP]
by (intro Least_le) (auto intro: pow_ord_eq_1 ord_pos)
[PROOF STATE]
proof (state)
this:
(LEAST n. 0 < n \<and> x [^] n = \<one>) \<le> ord x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) ord_conv_Gcd: (* Manuel Eberl *)
  assumes "x \<in> carrier G"
  shows   "ord x = Gcd {n. x [^] n = \<one>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord x = Gcd {n. x [^] n = \<one>}
[PROOF STEP]
by (rule sym, rule Gcd_eqI) (use assms in \<open>auto simp: pow_eq_id\<close>)


[STATEMENT]
lemma (in group) subgroup_ord_eq:
  assumes "subgroup H G" "x \<in> H"
  shows "group.ord (G\<lparr>carrier := H\<rparr>) x = ord x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. group.ord (G\<lparr>carrier := H\<rparr>) x = ord x
[PROOF STEP]
using nat_pow_consistent ord_def group.ord_def[of "(G\<lparr>carrier := H\<rparr>)" x]
        subgroup.subgroup_is_group[of H G] assms
[PROOF STATE]
proof (prove)
using this:
?x [^] ?n = ?x [^]\<^bsub>G\<lparr>carrier := ?H\<rparr>\<^esub> ?n
ord ?x \<equiv> SOME d. \<forall>n. (?x [^] n = \<one>) = (d dvd n)
Group.group (G\<lparr>carrier := H\<rparr>) \<Longrightarrow> group.ord (G\<lparr>carrier := H\<rparr>) x \<equiv> SOME d. \<forall>n. (x [^]\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> n = \<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub>) = (d dvd n)
\<lbrakk>subgroup H G; Group.group G\<rbrakk> \<Longrightarrow> Group.group (G\<lparr>carrier := H\<rparr>)
subgroup H G
x \<in> H

goal (1 subgoal):
 1. group.ord (G\<lparr>carrier := H\<rparr>) x = ord x
[PROOF STEP]
by simp


[STATEMENT]
lemma (in group) ord_FactGroup:
  assumes "subgroup P G" "group (G Mod P)"
  shows "order (G Mod P) * card P = order G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (G Mod P) * card P = order G
[PROOF STEP]
using lagrange[of P] FactGroup_def[of G P] assms order_def[of "(G Mod P)"]
[PROOF STATE]
proof (prove)
using this:
subgroup P G \<Longrightarrow> card (rcosets P) * card P = order G
G Mod P = \<lparr>carrier = rcosets P, mult = (<#>), one = P\<rparr>
subgroup P G
Group.group (G Mod P)
order (G Mod P) = card (carrier (G Mod P))

goal (1 subgoal):
 1. order (G Mod P) * card P = order G
[PROOF STEP]
by fastforce


[STATEMENT]
lemma (in group) one_is_same:
  assumes "subgroup H G"
  shows "\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in group) kernel_FactGroup:
  assumes "P \<lhd> G"
  shows "kernel G (G Mod P) (\<lambda>x. P #> x) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel G (G Mod P) ((#>) P) = P
[PROOF STEP]
proof(rule equalityI; rule subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> kernel G (G Mod P) ((#>) P) \<Longrightarrow> x \<in> P
 2. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> kernel G (G Mod P) ((#>) P) \<Longrightarrow> x \<in> P
 2. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
assume "x \<in> kernel G (G Mod P) ((#>) P)"
[PROOF STATE]
proof (state)
this:
x \<in> kernel G (G Mod P) ((#>) P)

goal (2 subgoals):
 1. \<And>x. x \<in> kernel G (G Mod P) ((#>) P) \<Longrightarrow> x \<in> P
 2. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
have "P #> x = \<one>\<^bsub>G Mod P\<^esub>" "x \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
x \<in> kernel G (G Mod P) ((#>) P)

goal (1 subgoal):
 1. P #> x = \<one>\<^bsub>G Mod P\<^esub> &&& x \<in> carrier G
[PROOF STEP]
unfolding kernel_def
[PROOF STATE]
proof (prove)
using this:
x \<in> {x \<in> carrier G. P #> x = \<one>\<^bsub>G Mod P\<^esub>}

goal (1 subgoal):
 1. P #> x = \<one>\<^bsub>G Mod P\<^esub> &&& x \<in> carrier G
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
P #> x = \<one>\<^bsub>G Mod P\<^esub>
x \<in> carrier G

goal (2 subgoals):
 1. \<And>x. x \<in> kernel G (G Mod P) ((#>) P) \<Longrightarrow> x \<in> P
 2. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
with coset_join1[of P x]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>P #> x = P; x \<in> carrier G; subgroup P G\<rbrakk> \<Longrightarrow> x \<in> P
P #> x = \<one>\<^bsub>G Mod P\<^esub>
x \<in> carrier G
[PROOF STEP]
show "x \<in> P"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P #> x = P; x \<in> carrier G; subgroup P G\<rbrakk> \<Longrightarrow> x \<in> P
P #> x = \<one>\<^bsub>G Mod P\<^esub>
x \<in> carrier G

goal (1 subgoal):
 1. x \<in> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P #> x = P; x \<in> carrier G; subgroup P G\<rbrakk> \<Longrightarrow> x \<in> P
P #> x = \<one>\<^bsub>G Mod P\<^esub>
x \<in> carrier G
P \<lhd> G

goal (1 subgoal):
 1. x \<in> P
[PROOF STEP]
unfolding normal_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P #> x = P; x \<in> carrier G; subgroup P G\<rbrakk> \<Longrightarrow> x \<in> P
P #> x = \<one>\<^bsub>G Mod P\<^esub>
x \<in> carrier G
subgroup P G \<and> Group.group G \<and> normal_axioms P G

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

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[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> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> P
[PROOF STEP]
have xc: "x \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
x \<in> P

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
using assms subgroup.subset
[PROOF STATE]
proof (prove)
using this:
x \<in> P
P \<lhd> G
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
unfolding normal_def
[PROOF STATE]
proof (prove)
using this:
x \<in> P
subgroup P G \<and> Group.group G \<and> normal_axioms P G
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. x \<in> carrier G
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> carrier G

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> P
[PROOF STEP]
have "P #> x = P"
[PROOF STATE]
proof (prove)
using this:
x \<in> P

goal (1 subgoal):
 1. P #> x = P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> P
P \<lhd> G

goal (1 subgoal):
 1. P #> x = P
[PROOF STEP]
by (simp add: normal_imp_subgroup subgroup.rcos_const)
[PROOF STATE]
proof (state)
this:
P #> x = P

goal (1 subgoal):
 1. \<And>x. x \<in> P \<Longrightarrow> x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
thus "x \<in> kernel G (G Mod P) ((#>) P)"
[PROOF STATE]
proof (prove)
using this:
P #> x = P

goal (1 subgoal):
 1. x \<in> kernel G (G Mod P) ((#>) P)
[PROOF STEP]
unfolding kernel_def
[PROOF STATE]
proof (prove)
using this:
P #> x = P

goal (1 subgoal):
 1. x \<in> {x \<in> carrier G. P #> x = \<one>\<^bsub>G Mod P\<^esub>}
[PROOF STEP]
using xc
[PROOF STATE]
proof (prove)
using this:
P #> x = P
x \<in> carrier G

goal (1 subgoal):
 1. x \<in> {x \<in> carrier G. P #> x = \<one>\<^bsub>G Mod P\<^esub>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> kernel G (G Mod P) ((#>) P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) sub_subgroup_coprime:
  assumes "subgroup H G" "subgroup J G" "coprime (card H) (card J)"
  and "subgroup sH G" "subgroup sJ G" "sH \<subseteq> H" "sJ \<subseteq> J"
shows "coprime (card sH) (card sJ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (card sH) (card sJ)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgroup H G
subgroup J G
coprime (card H) (card J)
subgroup sH G
subgroup sJ G
sH \<subseteq> H
sJ \<subseteq> J

goal (1 subgoal):
 1. coprime (card sH) (card sJ)
[PROOF STEP]
by (meson coprime_divisors sub_subgroup_dvd_card)


[STATEMENT]
lemma (in group) pow_eq_nat_mod:
  assumes "a \<in> carrier G" "a [^] n = a [^] m"
  shows "n mod (ord a) = m mod (ord a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n mod ord a = m mod ord a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n mod ord a = m mod ord a
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in> carrier G
a [^] n = a [^] m
[PROOF STEP]
have "a [^] (n - m) = \<one>"
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier G
a [^] n = a [^] m

goal (1 subgoal):
 1. a [^] (n - m) = \<one>
[PROOF STEP]
using pow_eq_div2
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier G
a [^] n = a [^] m
\<lbrakk>?x \<in> carrier G; ?x [^] ?m = ?x [^] ?n\<rbrakk> \<Longrightarrow> ?x [^] (?m - ?n) = \<one>

goal (1 subgoal):
 1. a [^] (n - m) = \<one>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a [^] (n - m) = \<one>

goal (1 subgoal):
 1. n mod ord a = m mod ord a
[PROOF STEP]
hence "ord a dvd n - m"
[PROOF STATE]
proof (prove)
using this:
a [^] (n - m) = \<one>

goal (1 subgoal):
 1. ord a dvd n - m
[PROOF STEP]
using assms(1) pow_eq_id
[PROOF STATE]
proof (prove)
using this:
a [^] (n - m) = \<one>
a \<in> carrier G
?x \<in> carrier G \<Longrightarrow> (?x [^] ?n = \<one>) = (ord ?x dvd ?n)

goal (1 subgoal):
 1. ord a dvd n - m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ord a dvd n - m

goal (1 subgoal):
 1. n mod ord a = m mod ord a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ord a dvd n - m

goal (1 subgoal):
 1. n mod ord a = m mod ord a
[PROOF STEP]
by (metis assms mod_eq_dvd_iff_nat nat_le_linear pow_eq_div2 pow_eq_id)
[PROOF STATE]
proof (state)
this:
n mod ord a = m mod ord a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_classes':
  "list_name \<noteq> test_name"
  "list_name \<noteq> Object"
  "list_name \<noteq> ClassCast"
  "list_name \<noteq> OutOfMemory"
  "list_name \<noteq> NullPointer"
  "test_name \<noteq> Object"
  "test_name \<noteq> OutOfMemory"
  "test_name \<noteq> ClassCast"
  "test_name \<noteq> NullPointer"
  "ClassCast \<noteq> NullPointer"
  "ClassCast \<noteq> Object"
  "NullPointer \<noteq> Object"
  "OutOfMemory \<noteq> ClassCast"
  "OutOfMemory \<noteq> NullPointer"
  "OutOfMemory \<noteq> Object"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((list_name \<noteq> test_name &&& list_name \<noteq> Object &&& list_name \<noteq> ClassCast) &&& (list_name \<noteq> OutOfMemory &&& list_name \<noteq> NullPointer) &&& test_name \<noteq> Object &&& test_name \<noteq> OutOfMemory) &&& ((test_name \<noteq> ClassCast &&& test_name \<noteq> NullPointer) &&& ClassCast \<noteq> NullPointer &&& ClassCast \<noteq> Object) &&& (NullPointer \<noteq> Object &&& OutOfMemory \<noteq> ClassCast) &&& OutOfMemory \<noteq> NullPointer &&& OutOfMemory \<noteq> Object
[PROOF STEP]
by (simp_all add: list_name_def test_name_def Object_def NullPointer_def
    OutOfMemory_def ClassCast_def)


[STATEMENT]
lemma distinct_fields:
  "val_name \<noteq> next_name"
  "next_name \<noteq> val_name"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_name \<noteq> next_name &&& next_name \<noteq> val_name
[PROOF STEP]
by (simp_all add: val_name_def next_name_def)


[STATEMENT]
lemma class_Object [simp]:
  "class E Object = Some (undefined, [],[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E Object = \<lfloor>(undefined, [], [])\<rfloor>
[PROOF STEP]
by (simp add: class_def system_defs E_def)


[STATEMENT]
lemma class_NullPointer [simp]:
  "class E NullPointer = Some (Object, [], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E NullPointer = \<lfloor>(Object, [], [])\<rfloor>
[PROOF STEP]
by (simp add: class_def system_defs E_def distinct_classes)


[STATEMENT]
lemma class_OutOfMemory [simp]:
  "class E OutOfMemory = Some (Object, [], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E OutOfMemory = \<lfloor>(Object, [], [])\<rfloor>
[PROOF STEP]
by (simp add: class_def system_defs E_def distinct_classes)


[STATEMENT]
lemma class_ClassCast [simp]:
  "class E ClassCast = Some (Object, [], [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E ClassCast = \<lfloor>(Object, [], [])\<rfloor>
[PROOF STEP]
by (simp add: class_def system_defs E_def distinct_classes)


[STATEMENT]
lemma class_list [simp]:
  "class E list_name = Some list_class"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>list_class\<rfloor>
[PROOF STEP]
by (simp add: class_def system_defs E_def distinct_classes)


[STATEMENT]
lemma class_test [simp]:
  "class E test_name = Some test_class"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E test_name = \<lfloor>test_class\<rfloor>
[PROOF STEP]
by (simp add: class_def system_defs E_def distinct_classes)


[STATEMENT]
lemma E_classes [simp]:
  "{C. is_class E C} = {list_name, test_name, NullPointer,
                        ClassCast, OutOfMemory, Object}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {C. is_class E C} = {list_name, test_name, NullPointer, ClassCast, OutOfMemory, Object}
[PROOF STEP]
by (auto simp add: is_class_def class_def system_defs E_def class_defs)


[STATEMENT]
lemma subcls1:
  "subcls1 E = {(list_name,Object), (test_name,Object), (NullPointer, Object),
                (ClassCast, Object), (OutOfMemory, Object)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls1 E = {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subcls1 E = {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}
[PROOF STEP]
apply (simp add: subcls1_def2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SIGMA C:{list_name, test_name, NullPointer, ClassCast, OutOfMemory, Object}. {D. fst (the (class E C)) = D \<and> C \<noteq> Object}) = {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}
[PROOF STEP]
apply (simp add: class_defs system_defs E_def class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SIGMA C:{list_name, test_name, NullPointer, ClassCast, OutOfMemory, Object}. {D. fst (the (if C = Object then \<lfloor>(undefined, [], [])\<rfloor> else [test_name \<mapsto> (Object, [], [(makelist_name, [], Void, 3, 2, make_list_ins, [])]), list_name \<mapsto> (Object, [(val_name, Integer), (next_name, Class list_name)], [(append_name, [Class list_name], Void, 3, 0, append_ins, [(Suc 0, 2, NullPointer, 7, 0)])]), OutOfMemory \<mapsto> (Object, [], []), ClassCast \<mapsto> (Object, [], []), NullPointer \<mapsto> (Object, [], [])] C)) = D \<and> C \<noteq> Object}) = {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}
[PROOF STEP]
(* FIXME: cannot simply expand class names, since
     inequality proofs on strings are too inefficient *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SIGMA C:{list_name, test_name, NullPointer, ClassCast, OutOfMemory, Object}. {D. fst (the (if C = Object then \<lfloor>(undefined, [], [])\<rfloor> else [test_name \<mapsto> (Object, [], [(makelist_name, [], Void, 3, 2, make_list_ins, [])]), list_name \<mapsto> (Object, [(val_name, Integer), (next_name, Class list_name)], [(append_name, [Class list_name], Void, 3, 0, append_ins, [(Suc 0, 2, NullPointer, 7, 0)])]), OutOfMemory \<mapsto> (Object, [], []), ClassCast \<mapsto> (Object, [], []), NullPointer \<mapsto> (Object, [], [])] C)) = D \<and> C \<noteq> Object}) = {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}
[PROOF STEP]
apply (auto simp: distinct_classes split!: if_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma notin_rtrancl:
  "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r\<^sup>*; a \<noteq> b; \<And>y. (a, y) \<notin> r\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto elim: converse_rtranclE)


[STATEMENT]
lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (subcls1 E)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (subcls1 E)
[PROOF STEP]
apply (rule acyclicI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> (subcls1 E)\<^sup>+
[PROOF STEP]
apply (simp add: subcls1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x, x) \<notin> {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}\<^sup>+
[PROOF STEP]
apply (auto dest!: tranclD)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (Object, list_name) \<in> {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}\<^sup>* \<Longrightarrow> False
 2. (Object, test_name) \<in> {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}\<^sup>* \<Longrightarrow> False
 3. (Object, NullPointer) \<in> {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}\<^sup>* \<Longrightarrow> False
 4. (Object, ClassCast) \<in> {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}\<^sup>* \<Longrightarrow> False
 5. (Object, OutOfMemory) \<in> {(list_name, Object), (test_name, Object), (NullPointer, Object), (ClassCast, Object), (OutOfMemory, Object)}\<^sup>* \<Longrightarrow> False
[PROOF STEP]
apply (auto elim!: notin_rtrancl simp add: distinct_classes)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ((subcls1 E)\<inverse>)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf ((subcls1 E)\<inverse>)
[PROOF STEP]
apply (rule finite_acyclic_wf_converse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite (subcls1 E)
 2. acyclic (subcls1 E)
[PROOF STEP]
apply (simp add: subcls1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. acyclic (subcls1 E)
[PROOF STEP]
apply (rule acyclic_subcls1_E)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma method_append [simp]:
  "method E list_name append_name =
  (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. method E list_name append_name = (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. method E list_name append_name = (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])
[PROOF STEP]
apply (insert class_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>list_class\<rfloor> \<Longrightarrow> method E list_name append_name = (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])
[PROOF STEP]
apply (unfold list_class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>(Object, [(val_name, Integer), (next_name, Class list_name)], [(append_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])])\<rfloor> \<Longrightarrow> method E list_name append_name = (list_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])
[PROOF STEP]
apply (fastforce simp add: Method_def distinct_classes intro: method_def2 Methods.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma method_makelist [simp]:
  "method E test_name makelist_name =
  (test_name, [], Void, 3, 2, make_list_ins, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. method E test_name makelist_name = (test_name, [], Void, 3, 2, make_list_ins, [])
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. method E test_name makelist_name = (test_name, [], Void, 3, 2, make_list_ins, [])
[PROOF STEP]
apply (insert class_test)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E test_name = \<lfloor>test_class\<rfloor> \<Longrightarrow> method E test_name makelist_name = (test_name, [], Void, 3, 2, make_list_ins, [])
[PROOF STEP]
apply (unfold test_class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E test_name = \<lfloor>(Object, [], [(makelist_name, [], Void, 3, 2, make_list_ins, [])])\<rfloor> \<Longrightarrow> method E test_name makelist_name = (test_name, [], Void, 3, 2, make_list_ins, [])
[PROOF STEP]
apply (fastforce simp add: Method_def distinct_classes intro: method_def2 Methods.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma field_val [simp]:
  "field E list_name val_name = (list_name, Integer)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field E list_name val_name = (list_name, Integer)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field E list_name val_name = (list_name, Integer)
[PROOF STEP]
apply (insert class_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>list_class\<rfloor> \<Longrightarrow> field E list_name val_name = (list_name, Integer)
[PROOF STEP]
apply (unfold list_class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>(Object, [(val_name, Integer), (next_name, Class list_name)], [(append_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])])\<rfloor> \<Longrightarrow> field E list_name val_name = (list_name, Integer)
[PROOF STEP]
apply (fastforce simp add: sees_field_def distinct_classes intro: field_def2 Fields.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma field_next [simp]:
  "field E list_name next_name = (list_name, Class list_name)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field E list_name next_name = (list_name, Class list_name)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. field E list_name next_name = (list_name, Class list_name)
[PROOF STEP]
apply (insert class_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>list_class\<rfloor> \<Longrightarrow> field E list_name next_name = (list_name, Class list_name)
[PROOF STEP]
apply (unfold list_class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E list_name = \<lfloor>(Object, [(val_name, Integer), (next_name, Class list_name)], [(append_name, [Class list_name], Void, 3, 0, append_ins, [(1, 2, NullPointer, 7, 0)])])\<rfloor> \<Longrightarrow> field E list_name next_name = (list_name, Class list_name)
[PROOF STEP]
apply (fastforce simp add: distinct_fields sees_field_def distinct_classes intro: field_def2 Fields.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]: "fields E Object = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields E Object = []
[PROOF STEP]
by (fastforce intro: fields_def2 Fields.intros)


[STATEMENT]
lemma [simp]: "fields E NullPointer = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields E NullPointer = []
[PROOF STEP]
by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)


[STATEMENT]
lemma [simp]: "fields E ClassCast = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields E ClassCast = []
[PROOF STEP]
by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)


[STATEMENT]
lemma [simp]: "fields E OutOfMemory = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields E OutOfMemory = []
[PROOF STEP]
by (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)


[STATEMENT]
lemma [simp]: "fields E test_name = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields E test_name = []
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fields E test_name = []
[PROOF STEP]
apply (insert class_test)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E test_name = \<lfloor>test_class\<rfloor> \<Longrightarrow> fields E test_name = []
[PROOF STEP]
apply (unfold test_class_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class E test_name = \<lfloor>(Object, [], [(makelist_name, [], Void, 3, 2, make_list_ins, [])])\<rfloor> \<Longrightarrow> fields E test_name = []
[PROOF STEP]
apply (fastforce simp add: distinct_classes intro: fields_def2 Fields.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wf_struct:
  "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "distinct_fst E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_fst E
[PROOF STEP]
by (simp add: system_defs E_def class_defs distinct_classes)
[PROOF STATE]
proof (state)
this:
distinct_fst E

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct_fst E

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "set SystemClasses \<subseteq> set E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set SystemClasses \<subseteq> set E
[PROOF STEP]
by (simp add: system_defs E_def)
[PROOF STATE]
proof (state)
this:
set SystemClasses \<subseteq> set E

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
hence "wf_syscls E"
[PROOF STATE]
proof (prove)
using this:
set SystemClasses \<subseteq> set E

goal (1 subgoal):
 1. wf_syscls E
[PROOF STEP]
by (rule wf_syscls)
[PROOF STATE]
proof (state)
this:
wf_syscls E

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_syscls E

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "wf_cdecl ?mb E ObjectC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>G C mb. True) E ObjectC
[PROOF STEP]
by (simp add: wf_cdecl_def ObjectC_def)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E ObjectC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E ObjectC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "wf_cdecl ?mb E NullPointerC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>G C mb. True) E NullPointerC
[PROOF STEP]
by (auto elim: notin_rtrancl
            simp add: wf_cdecl_def distinct_classes NullPointerC_def subcls1)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E NullPointerC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E NullPointerC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "wf_cdecl ?mb E ClassCastC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>G C mb. True) E ClassCastC
[PROOF STEP]
by (auto elim: notin_rtrancl
            simp add: wf_cdecl_def distinct_classes ClassCastC_def subcls1)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E ClassCastC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E ClassCastC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "wf_cdecl ?mb E OutOfMemoryC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>G C mb. True) E OutOfMemoryC
[PROOF STEP]
by (auto elim: notin_rtrancl
            simp add: wf_cdecl_def distinct_classes OutOfMemoryC_def subcls1)
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E OutOfMemoryC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E OutOfMemoryC

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "wf_cdecl ?mb E (list_name, list_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>G C mb. True) E (list_name, list_class)
[PROOF STEP]
apply (auto elim!: notin_rtrancl
            simp add: wf_cdecl_def wf_fdecl_def list_class_def
                      wf_mdecl_def subcls1)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. val_name = next_name \<Longrightarrow> False
 2. \<lbrakk>list_name \<noteq> test_name; Object = test_name\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>list_name \<noteq> NullPointer; Object = NullPointer\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>list_name \<noteq> ClassCast; Object = ClassCast\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>list_name \<noteq> OutOfMemory; Object = OutOfMemory\<rbrakk> \<Longrightarrow> False
 6. \<And>D' Ts' T' a aa ab b. \<lbrakk>list_name \<noteq> Object; E \<turnstile> Object sees append_name: Ts'\<rightarrow>T' = (a, aa, ab, b) in D'\<rbrakk> \<Longrightarrow> \<exists>z. Ts' = [z] \<and> subtype E z (Class list_name)
 7. \<And>D' Ts' T' a aa ab b. \<lbrakk>list_name \<noteq> Object; E \<turnstile> Object sees append_name: Ts'\<rightarrow>T' = (a, aa, ab, b) in D'\<rbrakk> \<Longrightarrow> T' = Void
[PROOF STEP]
apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E (list_name, list_class)

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E (list_name, list_class)

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
have "wf_cdecl ?mb E (test_name, test_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_cdecl (\<lambda>G C mb. True) E (test_name, test_class)
[PROOF STEP]
apply (auto elim!: notin_rtrancl
            simp add: wf_cdecl_def wf_fdecl_def test_class_def
                      wf_mdecl_def subcls1)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>test_name \<noteq> list_name; Object = list_name\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>test_name \<noteq> NullPointer; Object = NullPointer\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>test_name \<noteq> ClassCast; Object = ClassCast\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>test_name \<noteq> OutOfMemory; Object = OutOfMemory\<rbrakk> \<Longrightarrow> False
 5. \<And>D' Ts' T' a aa ab b. \<lbrakk>test_name \<noteq> Object; E \<turnstile> Object sees makelist_name: Ts'\<rightarrow>T' = (a, aa, ab, b) in D'\<rbrakk> \<Longrightarrow> Ts' = []
 6. \<And>D' Ts' T' a aa ab b. \<lbrakk>test_name \<noteq> Object; E \<turnstile> Object sees makelist_name: Ts'\<rightarrow>T' = (a, aa, ab, b) in D'\<rbrakk> \<Longrightarrow> T' = Void
[PROOF STEP]
apply (auto simp add: distinct_classes distinct_fields Method_def elim: Methods.cases)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
wf_cdecl (\<lambda>G C mb. True) E (test_name, test_class)

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
distinct_fst E
wf_syscls E
wf_cdecl (\<lambda>G C mb. True) E ObjectC
wf_cdecl (\<lambda>G C mb. True) E NullPointerC
wf_cdecl (\<lambda>G C mb. True) E ClassCastC
wf_cdecl (\<lambda>G C mb. True) E OutOfMemoryC
wf_cdecl (\<lambda>G C mb. True) E (list_name, list_class)
wf_cdecl (\<lambda>G C mb. True) E (test_name, test_class)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct_fst E
wf_syscls E
wf_cdecl (\<lambda>G C mb. True) E ObjectC
wf_cdecl (\<lambda>G C mb. True) E NullPointerC
wf_cdecl (\<lambda>G C mb. True) E ClassCastC
wf_cdecl (\<lambda>G C mb. True) E OutOfMemoryC
wf_cdecl (\<lambda>G C mb. True) E (list_name, list_class)
wf_cdecl (\<lambda>G C mb. True) E (test_name, test_class)

goal (1 subgoal):
 1. wf_prog (\<lambda>G C mb. True) E
[PROOF STEP]
by (simp add: wf_prog_def E_def SystemClasses_def)
[PROOF STATE]
proof (state)
this:
wf_prog (\<lambda>G C mb. True) E

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < n; x \<in> [0, n) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
by (simp add: intervall_def)


[STATEMENT]
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> [n0, n); P n0; x \<in> [Suc n0, n) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> [n0, n); P n0; x \<in> [Suc n0, n) \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (cases "x=n0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> [n0, n); P n0; x \<in> [Suc n0, n) \<Longrightarrow> P x; x = n0\<rbrakk> \<Longrightarrow> P x
 2. \<lbrakk>x \<in> [n0, n); P n0; x \<in> [Suc n0, n) \<Longrightarrow> P x; x \<noteq> n0\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
apply (auto simp add: intervall_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> [n, n) \<Longrightarrow> P x
[PROOF STEP]
by (unfold intervall_def) arith


[STATEMENT]
lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)
[PROOF STEP]
by (auto simp add: check_types_def phi_append_def JVM_states_unfold)