[STATEMENT]
lemma (in Module) mdl_is_module:"submodule R M H \<Longrightarrow> R module (mdl M H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submodule R M H \<Longrightarrow> R module mdl M H
[PROOF STEP]
apply (rule Module.intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. submodule R M H \<Longrightarrow> aGroup (mdl M H)
 2. submodule R M H \<Longrightarrow> Module_axioms (mdl M H) R
[PROOF STEP]
apply (simp add:mdl_is_ag)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. submodule R M H \<Longrightarrow> Module_axioms (mdl M H) R
[PROOF STEP]
apply (rule Module_axioms.intro)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. submodule R M H \<Longrightarrow> Ring R
 2. \<And>a m. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<in> carrier (mdl M H)
 3. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<plusminus>\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m
 4. \<And>a m n. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H); n \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (m \<plusminus>\<^bsub>mdl M H\<^esub> n) = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> n
 5. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 6. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:sc_Ring)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a m. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<in> carrier (mdl M H)
 2. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<plusminus>\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m
 3. \<And>a m n. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H); n \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (m \<plusminus>\<^bsub>mdl M H\<^esub> n) = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> n
 4. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 5. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:mdl_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a m. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> H\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s m \<in> H
 2. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<plusminus>\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m
 3. \<And>a m n. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H); n \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (m \<plusminus>\<^bsub>mdl M H\<^esub> n) = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> n
 4. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 5. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:submodule_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<plusminus>\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m
 2. \<And>a m n. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H); n \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (m \<plusminus>\<^bsub>mdl M H\<^esub> n) = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> n
 3. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 4. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:mdl_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> H\<rbrakk> \<Longrightarrow> (a \<plusminus>\<^bsub>R\<^esub> b) \<cdot>\<^sub>s m = a \<cdot>\<^sub>s m \<plusminus> b \<cdot>\<^sub>s m
 2. \<And>a m n. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H); n \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (m \<plusminus>\<^bsub>mdl M H\<^esub> n) = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> n
 3. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 4. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:submodule_def, (erule conjE)+,
        frule_tac c = m in subsetD[of H "carrier M"], assumption+,
        simp add:sc_l_distr)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a m n. \<lbrakk>submodule R M H; a \<in> carrier R; m \<in> carrier (mdl M H); n \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (m \<plusminus>\<^bsub>mdl M H\<^esub> n) = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m \<plusminus>\<^bsub>mdl M H\<^esub> a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> n
 2. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 3. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:mdl_def submodule_def, (erule conjE)+,
       simp add:asubg_pOp_closed,
       frule_tac c = m in subsetD[of H "carrier M"], assumption+,
       frule_tac c = n in subsetD[of H "carrier M"], assumption+,
       simp add:sc_r_distr)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b m. \<lbrakk>submodule R M H; a \<in> carrier R; b \<in> carrier R; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> (a \<cdot>\<^sub>r\<^bsub>R\<^esub> b) \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = a \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> (b \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m)
 2. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:mdl_def submodule_def, (erule conjE)+,
       frule_tac c = m in subsetD[of H "carrier M"], assumption+,
       simp add:sc_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>submodule R M H; m \<in> carrier (mdl M H)\<rbrakk> \<Longrightarrow> 1\<^sub>r\<^bsub>R\<^esub> \<cdot>\<^sub>s\<^bsub>mdl M H\<^esub> m = m
[PROOF STEP]
apply (simp add:mdl_def submodule_def, (erule conjE)+,
       frule_tac c = m in subsetD[of H "carrier M"], assumption+,
       simp add:sprod_one)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_Basis_list:
  "length Basis_list = card Basis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length Basis_list = DIM('a)
[PROOF STEP]
by (metis Basis_list distinct_Basis_list distinct_card)


[STATEMENT]
lemma eucl_of_list_inner:
  fixes i::"'a::executable_euclidean_space"
  assumes i: "i \<in> Basis"
  assumes l: "length xs = DIM('a)"
  shows "eucl_of_list xs \<bullet> i = xs ! (index Basis_list i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eucl_of_list xs \<bullet> i = xs ! index Basis_list i
[PROOF STEP]
by (simp add: eucl_of_list_nth[OF l] inner_sum_left assms inner_Basis
      nth_eq_iff_index sum.delta if_distrib cong: if_cong)


[STATEMENT]
lemma partitions_finite: "finite X" "finite Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X &&& finite Y
[PROOF STEP]
using partitions_ss finite_subset finV
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> V
Y \<subseteq> V
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite V

goal (1 subgoal):
 1. finite X &&& finite Y
[PROOF STEP]
by auto


[STATEMENT]
lemma complement_involution: "x \<noteq> u \<Longrightarrow> x = \<midarrow>(\<midarrow>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
assume "x \<noteq> u"
[PROOF STATE]
proof (state)
this:
x \<noteq> u

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
have "\<not> P u x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P u x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P u x \<Longrightarrow> False
[PROOF STEP]
assume "P u x"
[PROOF STATE]
proof (state)
this:
P u x

goal (1 subgoal):
 1. P u x \<Longrightarrow> False
[PROOF STEP]
with universe_character
[PROOF STATE]
proof (chain)
picking this:
P ?x u
P u x
[PROOF STEP]
have "x = u"
[PROOF STATE]
proof (prove)
using this:
P ?x u
P u x

goal (1 subgoal):
 1. x = u
[PROOF STEP]
by (rule part_antisymmetry)
[PROOF STATE]
proof (state)
this:
x = u

goal (1 subgoal):
 1. P u x \<Longrightarrow> False
[PROOF STEP]
with \<open>x \<noteq> u\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> u
x = u
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u
x = u

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

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

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "\<exists> v. P v u \<and> \<not> O v x"
[PROOF STATE]
proof (prove)
using this:
\<not> P u x

goal (1 subgoal):
 1. \<exists>v. P v u \<and> \<not> O v x
[PROOF STEP]
by (rule strong_supplementation)
[PROOF STATE]
proof (state)
this:
\<exists>v. P v u \<and> \<not> O v x

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. P v u \<and> \<not> O v x
[PROOF STEP]
obtain v where v: "P v u \<and> \<not> O v x"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. P v u \<and> \<not> O v x

goal (1 subgoal):
 1. (\<And>v. P v u \<and> \<not> O v x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P v u \<and> \<not> O v x

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "\<not> O v x"
[PROOF STATE]
proof (prove)
using this:
P v u \<and> \<not> O v x

goal (1 subgoal):
 1. \<not> O v x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> O v x

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "\<exists> v. \<not> O v x"
[PROOF STATE]
proof (prove)
using this:
\<not> O v x

goal (1 subgoal):
 1. \<exists>v. \<not> O v x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>v. \<not> O v x

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence notx: "\<forall> w. P w (\<midarrow>x) \<longleftrightarrow> \<not> O w x"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. \<not> O v x

goal (1 subgoal):
 1. \<forall>w. P w (\<midarrow> x) = (\<not> O w x)
[PROOF STEP]
by (rule complement_character)
[PROOF STATE]
proof (state)
this:
\<forall>w. P w (\<midarrow> x) = (\<not> O w x)

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
have "\<midarrow>x \<noteq> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<midarrow> x \<noteq> u
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<midarrow> x = u \<Longrightarrow> False
[PROOF STEP]
assume "\<midarrow>x = u"
[PROOF STATE]
proof (state)
this:
\<midarrow> x = u

goal (1 subgoal):
 1. \<midarrow> x = u \<Longrightarrow> False
[PROOF STEP]
hence "\<forall> w. P w u \<longleftrightarrow> \<not> O w x"
[PROOF STATE]
proof (prove)
using this:
\<midarrow> x = u

goal (1 subgoal):
 1. \<forall>w. P w u = (\<not> O w x)
[PROOF STEP]
using notx
[PROOF STATE]
proof (prove)
using this:
\<midarrow> x = u
\<forall>w. P w (\<midarrow> x) = (\<not> O w x)

goal (1 subgoal):
 1. \<forall>w. P w u = (\<not> O w x)
[PROOF STEP]
by (rule subst)
[PROOF STATE]
proof (state)
this:
\<forall>w. P w u = (\<not> O w x)

goal (1 subgoal):
 1. \<midarrow> x = u \<Longrightarrow> False
[PROOF STEP]
hence "P x u \<longleftrightarrow> \<not> O x x"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. P w u = (\<not> O w x)

goal (1 subgoal):
 1. P x u = (\<not> O x x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P x u = (\<not> O x x)

goal (1 subgoal):
 1. \<midarrow> x = u \<Longrightarrow> False
[PROOF STEP]
hence "\<not> O x x"
[PROOF STATE]
proof (prove)
using this:
P x u = (\<not> O x x)

goal (1 subgoal):
 1. \<not> O x x
[PROOF STEP]
using universe_character
[PROOF STATE]
proof (prove)
using this:
P x u = (\<not> O x x)
P ?x u

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

goal (1 subgoal):
 1. \<midarrow> x = u \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
\<not> O x x

goal (1 subgoal):
 1. False
[PROOF STEP]
using overlap_reflexivity
[PROOF STATE]
proof (prove)
using this:
\<not> O x x
O ?x ?x

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

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

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
have "\<not> P u (\<midarrow>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> P u (\<midarrow> x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P u (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
assume "P u (\<midarrow>x)"
[PROOF STATE]
proof (state)
this:
P u (\<midarrow> x)

goal (1 subgoal):
 1. P u (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
with universe_character
[PROOF STATE]
proof (chain)
picking this:
P ?x u
P u (\<midarrow> x)
[PROOF STEP]
have "\<midarrow>x = u"
[PROOF STATE]
proof (prove)
using this:
P ?x u
P u (\<midarrow> x)

goal (1 subgoal):
 1. \<midarrow> x = u
[PROOF STEP]
by (rule part_antisymmetry)
[PROOF STATE]
proof (state)
this:
\<midarrow> x = u

goal (1 subgoal):
 1. P u (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
with \<open>\<midarrow>x \<noteq> u\<close>
[PROOF STATE]
proof (chain)
picking this:
\<midarrow> x \<noteq> u
\<midarrow> x = u
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<midarrow> x \<noteq> u
\<midarrow> x = u

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> P u (\<midarrow> x)

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "\<exists> v. P v u \<and> \<not> O v (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<not> P u (\<midarrow> x)

goal (1 subgoal):
 1. \<exists>v. P v u \<and> \<not> O v (\<midarrow> x)
[PROOF STEP]
by (rule strong_supplementation)
[PROOF STATE]
proof (state)
this:
\<exists>v. P v u \<and> \<not> O v (\<midarrow> x)

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. P v u \<and> \<not> O v (\<midarrow> x)
[PROOF STEP]
obtain w where w: "P w u \<and> \<not> O w (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. P v u \<and> \<not> O v (\<midarrow> x)

goal (1 subgoal):
 1. (\<And>w. P w u \<and> \<not> O w (\<midarrow> x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P w u \<and> \<not> O w (\<midarrow> x)

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "\<not> O w (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
P w u \<and> \<not> O w (\<midarrow> x)

goal (1 subgoal):
 1. \<not> O w (\<midarrow> x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> O w (\<midarrow> x)

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "\<exists> v. \<not> O v (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<not> O w (\<midarrow> x)

goal (1 subgoal):
 1. \<exists>v. \<not> O v (\<midarrow> x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>v. \<not> O v (\<midarrow> x)

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence notnotx: "\<forall> w. P w (\<midarrow>(\<midarrow>x)) \<longleftrightarrow> \<not> O w (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. \<not> O v (\<midarrow> x)

goal (1 subgoal):
 1. \<forall>w. P w (\<midarrow> (\<midarrow> x)) = (\<not> O w (\<midarrow> x))
[PROOF STEP]
by (rule complement_character)
[PROOF STATE]
proof (state)
this:
\<forall>w. P w (\<midarrow> (\<midarrow> x)) = (\<not> O w (\<midarrow> x))

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
hence "P x (\<midarrow>(\<midarrow>x)) \<longleftrightarrow> \<not> O x (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. P w (\<midarrow> (\<midarrow> x)) = (\<not> O w (\<midarrow> x))

goal (1 subgoal):
 1. P x (\<midarrow> (\<midarrow> x)) = (\<not> O x (\<midarrow> x))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P x (\<midarrow> (\<midarrow> x)) = (\<not> O x (\<midarrow> x))

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P x (\<midarrow> (\<midarrow> x)) = (\<not> O x (\<midarrow> x))

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
have "\<not> O x (\<midarrow>x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> O x (\<midarrow> x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
assume "O x (\<midarrow>x)"
[PROOF STATE]
proof (state)
this:
O x (\<midarrow> x)

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
with overlap_eq
[PROOF STATE]
proof (chain)
picking this:
O ?x ?y = (\<exists>z. P z ?x \<and> P z ?y)
O x (\<midarrow> x)
[PROOF STEP]
have "\<exists> s. P s x \<and> P s (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
O ?x ?y = (\<exists>z. P z ?x \<and> P z ?y)
O x (\<midarrow> x)

goal (1 subgoal):
 1. \<exists>s. P s x \<and> P s (\<midarrow> x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>s. P s x \<and> P s (\<midarrow> x)

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. P s x \<and> P s (\<midarrow> x)
[PROOF STEP]
obtain s where s: "P s x \<and> P s (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>s. P s x \<and> P s (\<midarrow> x)

goal (1 subgoal):
 1. (\<And>s. P s x \<and> P s (\<midarrow> x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P s x \<and> P s (\<midarrow> x)

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
hence "P s x"
[PROOF STATE]
proof (prove)
using this:
P s x \<and> P s (\<midarrow> x)

goal (1 subgoal):
 1. P s x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P s x

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
hence "O s x"
[PROOF STATE]
proof (prove)
using this:
P s x

goal (1 subgoal):
 1. O s x
[PROOF STEP]
by (rule part_implies_overlap)
[PROOF STATE]
proof (state)
this:
O s x

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
from notx
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. P w (\<midarrow> x) = (\<not> O w x)
[PROOF STEP]
have "P s (\<midarrow>x) \<longleftrightarrow> \<not> O s x"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. P w (\<midarrow> x) = (\<not> O w x)

goal (1 subgoal):
 1. P s (\<midarrow> x) = (\<not> O s x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P s (\<midarrow> x) = (\<not> O s x)

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s (\<midarrow> x) = (\<not> O s x)

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
P s x \<and> P s (\<midarrow> x)
[PROOF STEP]
have "P s (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
P s x \<and> P s (\<midarrow> x)

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

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P s (\<midarrow> x) = (\<not> O s x)
P s (\<midarrow> x)
[PROOF STEP]
have "\<not> O s x"
[PROOF STATE]
proof (prove)
using this:
P s (\<midarrow> x) = (\<not> O s x)
P s (\<midarrow> x)

goal (1 subgoal):
 1. \<not> O s x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> O s x

goal (1 subgoal):
 1. O x (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
\<not> O s x

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>O s x\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> O s x
O s x

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

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

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P x (\<midarrow> (\<midarrow> x)) = (\<not> O x (\<midarrow> x))
\<not> O x (\<midarrow> x)
[PROOF STEP]
have "P x (\<midarrow>(\<midarrow>x))"
[PROOF STATE]
proof (prove)
using this:
P x (\<midarrow> (\<midarrow> x)) = (\<not> O x (\<midarrow> x))
\<not> O x (\<midarrow> x)

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

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P x (\<midarrow> (\<midarrow> x))

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
have "P (\<midarrow>(\<midarrow>x)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (\<midarrow> (\<midarrow> x)) x
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
assume "\<not> P (\<midarrow>(\<midarrow>x)) x"
[PROOF STATE]
proof (state)
this:
\<not> P (\<midarrow> (\<midarrow> x)) x

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
hence "\<exists> s. P s (\<midarrow>(\<midarrow>x)) \<and> \<not> O s x"
[PROOF STATE]
proof (prove)
using this:
\<not> P (\<midarrow> (\<midarrow> x)) x

goal (1 subgoal):
 1. \<exists>s. P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x
[PROOF STEP]
by (rule strong_supplementation)
[PROOF STATE]
proof (state)
this:
\<exists>s. P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>s. P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x
[PROOF STEP]
obtain s where s: "P s (\<midarrow>(\<midarrow>x)) \<and> \<not> O s x"
[PROOF STATE]
proof (prove)
using this:
\<exists>s. P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x

goal (1 subgoal):
 1. (\<And>s. P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
hence "\<not> O s x"
[PROOF STATE]
proof (prove)
using this:
P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x

goal (1 subgoal):
 1. \<not> O s x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> O s x

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
from notnotx
[PROOF STATE]
proof (chain)
picking this:
\<forall>w. P w (\<midarrow> (\<midarrow> x)) = (\<not> O w (\<midarrow> x))
[PROOF STEP]
have "P s (\<midarrow>(\<midarrow>x)) \<longleftrightarrow> (\<not> O s (\<midarrow>x))"
[PROOF STATE]
proof (prove)
using this:
\<forall>w. P w (\<midarrow> (\<midarrow> x)) = (\<not> O w (\<midarrow> x))

goal (1 subgoal):
 1. P s (\<midarrow> (\<midarrow> x)) = (\<not> O s (\<midarrow> x))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
P s (\<midarrow> (\<midarrow> x)) = (\<not> O s (\<midarrow> x))

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P s (\<midarrow> (\<midarrow> x)) = (\<not> O s (\<midarrow> x))

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
from s
[PROOF STATE]
proof (chain)
picking this:
P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x
[PROOF STEP]
have "P s (\<midarrow>(\<midarrow>x))"
[PROOF STATE]
proof (prove)
using this:
P s (\<midarrow> (\<midarrow> x)) \<and> \<not> O s x

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

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P s (\<midarrow> (\<midarrow> x)) = (\<not> O s (\<midarrow> x))
P s (\<midarrow> (\<midarrow> x))
[PROOF STEP]
have "\<not> O s (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
P s (\<midarrow> (\<midarrow> x)) = (\<not> O s (\<midarrow> x))
P s (\<midarrow> (\<midarrow> x))

goal (1 subgoal):
 1. \<not> O s (\<midarrow> x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<not> O s (\<midarrow> x)

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
from or_complement_overlap
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. O y ?x \<or> O y (\<midarrow> ?x)
[PROOF STEP]
have "O s x \<or> O s (\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. O y ?x \<or> O y (\<midarrow> ?x)

goal (1 subgoal):
 1. O s x \<or> O s (\<midarrow> x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
O s x \<or> O s (\<midarrow> x)

goal (1 subgoal):
 1. \<not> P (\<midarrow> (\<midarrow> x)) x \<Longrightarrow> False
[PROOF STEP]
thus "False"
[PROOF STATE]
proof (prove)
using this:
O s x \<or> O s (\<midarrow> x)

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. O s x \<Longrightarrow> False
 2. O s (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
assume "O s x"
[PROOF STATE]
proof (state)
this:
O s x

goal (2 subgoals):
 1. O s x \<Longrightarrow> False
 2. O s (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> O s x\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> O s x
O s x
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> O s x
O s x

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

goal (1 subgoal):
 1. O s (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. O s (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
assume "O s (\<midarrow>x)"
[PROOF STATE]
proof (state)
this:
O s (\<midarrow> x)

goal (1 subgoal):
 1. O s (\<midarrow> x) \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> O s (\<midarrow>x )\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> O s (\<midarrow> x)
O s (\<midarrow> x)
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
\<not> O s (\<midarrow> x)
O s (\<midarrow> x)

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

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

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

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P x (\<midarrow> (\<midarrow> x))
P (\<midarrow> (\<midarrow> x)) x
[PROOF STEP]
show "x = \<midarrow>(\<midarrow>x)"
[PROOF STATE]
proof (prove)
using this:
P x (\<midarrow> (\<midarrow> x))
P (\<midarrow> (\<midarrow> x)) x

goal (1 subgoal):
 1. x = \<midarrow> (\<midarrow> x)
[PROOF STEP]
by (rule part_antisymmetry)
[PROOF STATE]
proof (state)
this:
x = \<midarrow> (\<midarrow> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exp_ivp_existence_ivl0:
  "exp_ivp.existence_ivl0 p = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exp_ivp.existence_ivl0 p = UNIV
[PROOF STEP]
by (rule exp_ivp.existence_ivl_eq_domain)
     (auto intro!: exI[where x=1] order_trans[OF norm_Pair_le] order_trans[OF _ norm_snd_le])


[STATEMENT]
lemma v: "(v solves_ode f1) {0..<1} UNIV" and "v 0 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v solves_ode f1) {0..<1} UNIV &&& v 0 = 1
[PROOF STEP]
by (auto intro!: solves_odeI derivative_eq_intros ext
    simp: v_def has_vderiv_on_def f1_def has_vector_derivative_def divide_simps power2_eq_square)


[STATEMENT]
lemma my_induct[consumes 1, case_names base step]:
  fixes P::"nat\<Rightarrow>bool"
assumes less: "i \<le> j"
    and base: "P j"
    and step: "\<And>n. i \<le> n \<Longrightarrow> n < j \<Longrightarrow> (\<forall>n'>n. n'\<le>j \<longrightarrow> P n') \<Longrightarrow> P n"
  shows "P i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P i
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> P i
 2. \<not> ?P \<Longrightarrow> P i
[PROOF STEP]
assume "j=0"
[PROOF STATE]
proof (state)
this:
j = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> P i
 2. \<not> ?P \<Longrightarrow> P i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j = 0

goal (1 subgoal):
 1. P i
[PROOF STEP]
using less base
[PROOF STATE]
proof (prove)
using this:
j = 0
i \<le> j
P j

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

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> P i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> P i
[PROOF STEP]
assume "\<not> j=0"
[PROOF STATE]
proof (state)
this:
j \<noteq> 0

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> P i
[PROOF STEP]
have "j - (j - i) \<ge> i \<longrightarrow> P (j - (j - i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j - (j - i) \<longrightarrow> P (j - (j - i))
[PROOF STEP]
proof (rule less_induct[of "\<lambda>n::nat. j-n \<ge> i \<longrightarrow> P (j-n)" "j-i"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y < x \<Longrightarrow> i \<le> j - y \<longrightarrow> P (j - y)) \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. y < x \<Longrightarrow> i \<le> j - y \<longrightarrow> P (j - y)) \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
assume asmp: "\<And>y. y < x \<Longrightarrow> i \<le> j - y \<longrightarrow> P (j - y)"
[PROOF STATE]
proof (state)
this:
?y < x \<Longrightarrow> i \<le> j - ?y \<longrightarrow> P (j - ?y)

goal (1 subgoal):
 1. \<And>x. (\<And>y. y < x \<Longrightarrow> i \<le> j - y \<longrightarrow> P (j - y)) \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
show "i \<le> j - x \<longrightarrow> P (j - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
 2. \<not> ?P \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
assume "x=0"
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
 2. \<not> ?P \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
with base
[PROOF STATE]
proof (chain)
picking this:
P j
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P j
x = 0

goal (1 subgoal):
 1. i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<le> j - x \<longrightarrow> P (j - x)

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
assume "\<not> x=0"
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
with \<open>j \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
j \<noteq> 0
x \<noteq> 0
[PROOF STEP]
have "j - x < j"
[PROOF STATE]
proof (prove)
using this:
j \<noteq> 0
x \<noteq> 0

goal (1 subgoal):
 1. j - x < j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j - x < j

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> j - x \<longrightarrow> P (j - x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<le> j - x \<Longrightarrow> P (j - x)
[PROOF STEP]
assume "i \<le> j - x"
[PROOF STATE]
proof (state)
this:
i \<le> j - x

goal (1 subgoal):
 1. i \<le> j - x \<Longrightarrow> P (j - x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<le> j - x

goal (1 subgoal):
 1. i \<le> j - x \<Longrightarrow> P (j - x)
[PROOF STEP]
have "\<forall>n'>j-x. n'\<le>j \<longrightarrow> P n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n'>j - x. n' \<le> j \<longrightarrow> P n'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. j - x < n' \<longrightarrow> n' \<le> j \<longrightarrow> P n'
[PROOF STEP]
fix n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n'. j - x < n' \<longrightarrow> n' \<le> j \<longrightarrow> P n'
[PROOF STEP]
show "n'>j-x \<longrightarrow> n'\<le>j \<longrightarrow> P n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j - x < n' \<longrightarrow> n' \<le> j \<longrightarrow> P n'
[PROOF STEP]
proof (rule HOL.impI[OF HOL.impI])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
assume "j - x < n'" and "n' \<le> j"
[PROOF STATE]
proof (state)
this:
j - x < n'
n' \<le> j

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
hence "j - n' < x"
[PROOF STATE]
proof (prove)
using this:
j - x < n'
n' \<le> j

goal (1 subgoal):
 1. j - n' < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j - n' < x

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j - n' < x

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
from \<open>i \<le> j - x\<close> \<open>j - x < n'\<close>
[PROOF STATE]
proof (chain)
picking this:
i \<le> j - x
j - x < n'
[PROOF STEP]
have "i \<le> n'"
[PROOF STATE]
proof (prove)
using this:
i \<le> j - x
j - x < n'

goal (1 subgoal):
 1. i \<le> n'
[PROOF STEP]
using le_less_trans less_imp_le_nat
[PROOF STATE]
proof (prove)
using this:
i \<le> j - x
j - x < n'
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
?m < ?n \<Longrightarrow> ?m \<le> ?n

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

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
with \<open>n' \<le> j\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<le> j
i \<le> n'
[PROOF STEP]
have "i \<le> j - (j - n')"
[PROOF STATE]
proof (prove)
using this:
n' \<le> j
i \<le> n'

goal (1 subgoal):
 1. i \<le> j - (j - n')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i \<le> j - (j - n')

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j - n' < x
i \<le> j - (j - n')
[PROOF STEP]
have  "P (j - (j - n'))"
[PROOF STATE]
proof (prove)
using this:
j - n' < x
i \<le> j - (j - n')

goal (1 subgoal):
 1. P (j - (j - n'))
[PROOF STEP]
using asmp
[PROOF STATE]
proof (prove)
using this:
j - n' < x
i \<le> j - (j - n')
?y < x \<Longrightarrow> i \<le> j - ?y \<longrightarrow> P (j - ?y)

goal (1 subgoal):
 1. P (j - (j - n'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (j - (j - n'))

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P (j - (j - n'))

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
from \<open>n' \<le> j\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<le> j
[PROOF STEP]
have "j - (j - n') = n'"
[PROOF STATE]
proof (prove)
using this:
n' \<le> j

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

goal (1 subgoal):
 1. \<lbrakk>j - x < n'; n' \<le> j\<rbrakk> \<Longrightarrow> P n'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P (j - (j - n'))
j - (j - n') = n'
[PROOF STEP]
show "P n'"
[PROOF STATE]
proof (prove)
using this:
P (j - (j - n'))
j - (j - n') = n'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
j - x < n' \<longrightarrow> n' \<le> j \<longrightarrow> P n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n'>j - x. n' \<le> j \<longrightarrow> P n'

goal (1 subgoal):
 1. i \<le> j - x \<Longrightarrow> P (j - x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<le> j - x
\<forall>n'>j - x. n' \<le> j \<longrightarrow> P n'
[PROOF STEP]
show "P (j - x)"
[PROOF STATE]
proof (prove)
using this:
i \<le> j - x
\<forall>n'>j - x. n' \<le> j \<longrightarrow> P n'

goal (1 subgoal):
 1. P (j - x)
[PROOF STEP]
using \<open>j-x<j\<close> step[of "j-x"]
[PROOF STATE]
proof (prove)
using this:
i \<le> j - x
\<forall>n'>j - x. n' \<le> j \<longrightarrow> P n'
j - x < j
\<lbrakk>i \<le> j - x; j - x < j; \<forall>n'>j - x. n' \<le> j \<longrightarrow> P n'\<rbrakk> \<Longrightarrow> P (j - x)

goal (1 subgoal):
 1. P (j - x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (j - x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<le> j - x \<longrightarrow> P (j - x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<le> j - x \<longrightarrow> P (j - x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i \<le> j - (j - i) \<longrightarrow> P (j - (j - i))

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> P i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<le> j - (j - i) \<longrightarrow> P (j - (j - i))

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> P i
[PROOF STEP]
from less
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
have "j - (j - i) = i"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

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

goal (1 subgoal):
 1. j \<noteq> 0 \<Longrightarrow> P i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<le> j - (j - i) \<longrightarrow> P (j - (j - i))
j - (j - i) = i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<le> j - (j - i) \<longrightarrow> P (j - (j - i))
j - (j - i) = i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bernpoly_1': "bernpoly n 1 = of_real (bernoulli' n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernpoly n (1::'a) = of_real (bernoulli' n)
[PROOF STEP]
using bernpoly_1_1 [where ?'a = 'a]
[PROOF STATE]
proof (prove)
using this:
bernpoly 1 (1::'a) = of_real (1 / 2)

goal (1 subgoal):
 1. bernpoly n (1::'a) = of_real (bernoulli' n)
[PROOF STEP]
by (cases "n = 1") (simp_all add: bernpoly_1 bernoulli'_def)


[STATEMENT]
lemma filter_empty_every_not: "\<And>P l. (filter (\<lambda>x. P x) l = []) = list_all (\<lambda>x. \<not>P x) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P l. (filter P l = []) = list_all (\<lambda>x. \<not> P x) l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P l. (filter P l = []) = list_all (\<lambda>x. \<not> P x) l
[PROOF STEP]
fix P l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P l. (filter P l = []) = list_all (\<lambda>x. \<not> P x) l
[PROOF STEP]
show "(filter (\<lambda>x. P x) l = []) = list_all (\<lambda>x. \<not>P x) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (filter P l = []) = list_all (\<lambda>x. \<not> P x) l
[PROOF STEP]
apply(induction l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (filter P [] = []) = list_all (\<lambda>x. \<not> P x) []
 2. \<And>a l. (filter P l = []) = list_all (\<lambda>x. \<not> P x) l \<Longrightarrow> (filter P (a # l) = []) = list_all (\<lambda>x. \<not> P x) (a # l)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(filter P l = []) = list_all (\<lambda>x. \<not> P x) l

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>NOTE added lemma (listScript.sml:810).\<close>


[STATEMENT]
lemma addr_of_ref_alloc[simp]:
  "addr_of_ref (fst (Ref.alloc x h)) = lim h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_ref (fst (Ref.alloc x h)) = lim h
[PROOF STEP]
unfolding Ref.alloc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_of_ref (fst (let l = lim h; r = Ref l in (r, Ref.set r x (h\<lparr>lim := l + 1\<rparr>)))) = lim h
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma mpoly_to_mpoly_poly_0 [simp]:
  "mpoly_to_mpoly_poly x 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_to_mpoly_poly x 0 = 0
[PROOF STEP]
unfolding mpoly_Const_0 [symmetric] mpoly_to_mpoly_poly_Const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:Const (0::'a):] = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma vD_nsqn_sqn [elim, simp]:
  assumes "ip\<in>vD(rt)"
    shows "nsqn rt ip = sqn rt ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
from \<open>ip\<in>vD(rt)\<close>
[PROOF STATE]
proof (chain)
picking this:
ip \<in> vD rt
[PROOF STEP]
have "ip\<in>kD(rt)"
                      and "the (flag rt ip) = val"
[PROOF STATE]
proof (prove)
using this:
ip \<in> vD rt

goal (1 subgoal):
 1. ip \<in> kD rt &&& the (flag rt ip) = val
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. nsqn rt ip = sqn rt ip
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
nsqn rt ip = sqn rt ip

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma divides_iff_mult_mono:
  assumes "a \<in> carrier G" "b \<in> carrier G"
  assumes "canonical_irreducibles G R"
  assumes "\<And>d. d \<in> R \<Longrightarrow> multiplicity G d a \<le> multiplicity G d b"
  shows "a divides b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a divides b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a divides b
[PROOF STEP]
have "count (factor_mset G a) d \<le> count (factor_mset G b) d" for d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
proof (cases "\<exists>y \<in> carrier G. irreducible G y \<and> d = assocs G y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y
[PROOF STEP]
obtain y where y_def:
      "irreducible G y" "y \<in> carrier G" "d = assocs G y"
[PROOF STATE]
proof (prove)
using this:
\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>irreducible G y; y \<in> carrier G; d = assocs G y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
irreducible G y
y \<in> carrier G
d = assocs G y

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
irreducible G y
y \<in> carrier G
d = assocs G y
[PROOF STEP]
obtain z where z_def: "z \<in> R" "y \<sim> z"
[PROOF STATE]
proof (prove)
using this:
irreducible G y
y \<in> carrier G
d = assocs G y

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> R; y \<sim> z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
irreducible G y
y \<in> carrier G
d = assocs G y
canonical_irreducibles G R

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> R; y \<sim> z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding canonical_irreducibles_def
[PROOF STATE]
proof (prove)
using this:
irreducible G y
y \<in> carrier G
d = assocs G y
R \<subseteq> {a \<in> carrier G. irreducible G a} \<and> (\<forall>x y. x \<in> R \<longrightarrow> y \<in> R \<longrightarrow> x \<sim> y \<longrightarrow> x = y) \<and> (\<forall>x\<in>carrier G. irreducible G x \<longrightarrow> Bex R ((\<sim>) x))

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> R; y \<sim> z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
z \<in> R
y \<sim> z

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have z_more: "irreducible G z" "z \<in> carrier G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible G z &&& z \<in> carrier G
[PROOF STEP]
using z_def(1) assms(3)
[PROOF STATE]
proof (prove)
using this:
z \<in> R
canonical_irreducibles G R

goal (1 subgoal):
 1. irreducible G z &&& z \<in> carrier G
[PROOF STEP]
unfolding canonical_irreducibles_def
[PROOF STATE]
proof (prove)
using this:
z \<in> R
R \<subseteq> {a \<in> carrier G. irreducible G a} \<and> (\<forall>x y. x \<in> R \<longrightarrow> y \<in> R \<longrightarrow> x \<sim> y \<longrightarrow> x = y) \<and> (\<forall>x\<in>carrier G. irreducible G x \<longrightarrow> Bex R ((\<sim>) x))

goal (1 subgoal):
 1. irreducible G z &&& z \<in> carrier G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
irreducible G z
z \<in> carrier G

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have "y \<in> assocs G z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> assocs G z
[PROOF STEP]
using z_def(2) z_more(2) y_def(2)
[PROOF STATE]
proof (prove)
using this:
y \<sim> z
z \<in> carrier G
y \<in> carrier G

goal (1 subgoal):
 1. y \<in> assocs G z
[PROOF STEP]
by (simp add: closure_ofI2)
[PROOF STATE]
proof (state)
this:
y \<in> assocs G z

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
hence d_def: "d = assocs G z"
[PROOF STATE]
proof (prove)
using this:
y \<in> assocs G z

goal (1 subgoal):
 1. d = assocs G z
[PROOF STEP]
using y_def(2,3) z_more(2) assocs_repr_independence
[PROOF STATE]
proof (prove)
using this:
y \<in> assocs G z
y \<in> carrier G
d = assocs G y
z \<in> carrier G
\<lbrakk>?y \<in> assocs G ?x; ?x \<in> carrier G\<rbrakk> \<Longrightarrow> assocs G ?x = assocs G ?y

goal (1 subgoal):
 1. d = assocs G z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d = assocs G z

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have "count (factor_mset G a) d = multiplicity G z a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (factor_mset G a) d = multiplicity G z a
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (factor_mset G a) (assocs G z) = multiplicity G z a
[PROOF STEP]
by (intro factor_mset_count[OF assms(1) z_more(2,1)])
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) d = multiplicity G z a

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) d = multiplicity G z a

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have "... \<le> multiplicity G z b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity G z a \<le> multiplicity G z b
[PROOF STEP]
using assms(4) z_def(1)
[PROOF STATE]
proof (prove)
using this:
?d \<in> R \<Longrightarrow> multiplicity G ?d a \<le> multiplicity G ?d b
z \<in> R

goal (1 subgoal):
 1. multiplicity G z a \<le> multiplicity G z b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
multiplicity G z a \<le> multiplicity G z b

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity G z a \<le> multiplicity G z b

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have "... = count (factor_mset G b) d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity G z b = count (factor_mset G b) d
[PROOF STEP]
unfolding d_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity G z b = count (factor_mset G b) (assocs G z)
[PROOF STEP]
by (intro factor_mset_count[symmetric, OF assms(2) z_more(2,1)])
[PROOF STATE]
proof (state)
this:
multiplicity G z b = count (factor_mset G b) d

goal (2 subgoals):
 1. \<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
 2. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count (factor_mset G a) d \<le> count (factor_mset G b) d

goal (1 subgoal):
 1. count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) d \<le> count (factor_mset G b) d

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y)

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have "count (factor_mset G a) d = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (factor_mset G a) d = 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y)

goal (1 subgoal):
 1. count (factor_mset G a) d = 0
[PROOF STEP]
by (intro factor_mset_count_2[OF assms(1)], simp)
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) d = 0

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) d = 0

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
have "count (factor_mset G b) d = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (factor_mset G b) d = 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y)

goal (1 subgoal):
 1. count (factor_mset G b) d = 0
[PROOF STEP]
by (intro factor_mset_count_2[OF assms(2)], simp)
[PROOF STATE]
proof (state)
this:
count (factor_mset G b) d = 0

goal (1 subgoal):
 1. \<not> (\<exists>y\<in>carrier G. irreducible G y \<and> d = assocs G y) \<Longrightarrow> count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
count (factor_mset G a) d = 0
count (factor_mset G b) d = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count (factor_mset G a) d = 0
count (factor_mset G b) d = 0

goal (1 subgoal):
 1. count (factor_mset G a) d \<le> count (factor_mset G b) d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) d \<le> count (factor_mset G b) d

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
count (factor_mset G a) ?d \<le> count (factor_mset G b) ?d

goal (1 subgoal):
 1. a divides b
[PROOF STEP]
hence "factor_mset G a \<subseteq># factor_mset G b"
[PROOF STATE]
proof (prove)
using this:
count (factor_mset G a) ?d \<le> count (factor_mset G b) ?d

goal (1 subgoal):
 1. factor_mset G a \<subseteq># factor_mset G b
[PROOF STEP]
unfolding subseteq_mset_def
[PROOF STATE]
proof (prove)
using this:
count (factor_mset G a) ?d \<le> count (factor_mset G b) ?d

goal (1 subgoal):
 1. \<forall>aa. count (factor_mset G a) aa \<le> count (factor_mset G b) aa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
factor_mset G a \<subseteq># factor_mset G b

goal (1 subgoal):
 1. a divides b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
factor_mset G a \<subseteq># factor_mset G b

goal (1 subgoal):
 1. a divides b
[PROOF STEP]
using factor_mset_divides assms(1,2)
[PROOF STATE]
proof (prove)
using this:
factor_mset G a \<subseteq># factor_mset G b
\<lbrakk>?a \<in> carrier G; ?b \<in> carrier G\<rbrakk> \<Longrightarrow> ?a divides ?b = (factor_mset G ?a \<subseteq># factor_mset G ?b)
a \<in> carrier G
b \<in> carrier G

goal (1 subgoal):
 1. a divides b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a divides b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma onllD [dest]:
  assumes "onll \<Gamma> P ((\<xi>, p), a, (\<xi>', p'))"
    shows "\<forall>l\<in>labels \<Gamma> p. \<forall>l'\<in>labels \<Gamma> p'. P ((\<xi>, l), a, (\<xi>', l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>l\<in>labels \<Gamma> p. \<forall>l'\<in>labels \<Gamma> p'. P ((\<xi>, l), a, \<xi>', l')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
onll \<Gamma> P ((\<xi>, p), a, \<xi>', p')

goal (1 subgoal):
 1. \<forall>l\<in>labels \<Gamma> p. \<forall>l'\<in>labels \<Gamma> p'. P ((\<xi>, l), a, \<xi>', l')
[PROOF STEP]
unfolding onll_def
[PROOF STATE]
proof (prove)
using this:
case ((\<xi>, p), a, \<xi>', p') of (x, xa) \<Rightarrow> (case x of (\<xi>, p) \<Rightarrow> \<lambda>(a, \<xi>', p'). \<forall>l\<in>labels \<Gamma> p. \<forall>l'\<in>labels \<Gamma> p'. P ((\<xi>, l), a, \<xi>', l')) xa

goal (1 subgoal):
 1. \<forall>l\<in>labels \<Gamma> p. \<forall>l'\<in>labels \<Gamma> p'. P ((\<xi>, l), a, \<xi>', l')
[PROOF STEP]
by simp


[STATEMENT]
lemma (in PolynRg) pol_len_gt_deg:"\<lbrakk>p \<in> carrier R; pol_coeff S c;
       p = polyn_expr R X (fst c) c; deg R S X p < (an j); j \<le> (fst c)\<rbrakk>
       \<Longrightarrow>  (snd c) j = \<zero>\<^bsub>S\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; deg R S X p < an j; j \<le> fst c\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (case_tac "p = \<zero>\<^bsub>R\<^esub>", simp, drule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; pol_coeff S c; deg R S X (polyn_expr R X (fst c) c) < an j; j \<le> fst c; p = polyn_expr R X (fst c) c; polyn_expr R X (fst c) c = \<zero>\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
 2. \<lbrakk>p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; deg R S X p < an j; j \<le> fst c; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:coeff_0_pol_0[THEN sym, of c "fst c"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; deg R S X p < an j; j \<le> fst c; p \<noteq> \<zero>\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:deg_def, simp add:aless_natless)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>polyn_expr R X (fst c) c \<in> carrier R; pol_coeff S c; p = polyn_expr R X (fst c) c; deg_n R S X (polyn_expr R X (fst c) c) < j; j \<le> fst c; polyn_expr R X (fst c) c \<noteq> \<zero>\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (drule sym, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; pol_coeff S c; deg_n R S X p < j; j \<le> fst c; p \<noteq> \<zero>; polyn_expr R X (fst c) c = p\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (frule coeff_max_zeroTr[of c])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> carrier R; pol_coeff S c; deg_n R S X p < j; j \<le> fst c; p \<noteq> \<zero>; polyn_expr R X (fst c) c = p; \<forall>j. j \<le> fst c \<and> c_max S c < j \<longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>\<rbrakk> \<Longrightarrow> snd c j = \<zero>\<^bsub>S\<^esub>
[PROOF STEP]
apply (simp add:pol_deg_eq_c_max)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma walk_middle_edge: "walk (xs @ v # w # ys) \<Longrightarrow> v\<rightarrow>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk (xs @ v # w # ys) \<Longrightarrow> v \<rightarrow> w
[PROOF STEP]
by (induct "xs @ v # w # ys" arbitrary: xs rule: walk.induct, simp, simp)
     (metis list.sel(1,3) self_append_conv2 tl_append2)


[STATEMENT]
lemma nth_least_wellformed[intro?, simp]:
    assumes "enat n < esize A"
    shows "nth_least A n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least A n \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
enat n < esize A

goal (1 subgoal):
 1. nth_least A n \<in> A
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. enat 0 < esize A \<Longrightarrow> nth_least A 0 \<in> A
 2. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
enat 0 < esize A

goal (2 subgoals):
 1. \<And>A. enat 0 < esize A \<Longrightarrow> nth_least A 0 \<in> A
 2. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least A 0 \<in> A
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
enat 0 < esize A

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

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
enat n < esize ?A \<Longrightarrow> nth_least ?A n \<in> ?A
enat (Suc n) < esize A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
have 1: "A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
using Suc(2)
[PROOF STATE]
proof (prove)
using this:
enat (Suc n) < esize A

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

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
have 2: "enat n < esize (A - {least A})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat n < esize (A - {least A})
[PROOF STEP]
using Suc(2) 1
[PROOF STATE]
proof (prove)
using this:
enat (Suc n) < esize A
A \<noteq> {}

goal (1 subgoal):
 1. enat n < esize (A - {least A})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enat n < esize (A - {least A})

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
have 3: "nth_least (A - {least A}) n \<in> A - {least A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least (A - {least A}) n \<in> A - {least A}
[PROOF STEP]
using Suc(1) 2
[PROOF STATE]
proof (prove)
using this:
enat n < esize ?A \<Longrightarrow> nth_least ?A n \<in> ?A
enat n < esize (A - {least A})

goal (1 subgoal):
 1. nth_least (A - {least A}) n \<in> A - {least A}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
nth_least (A - {least A}) n \<in> A - {least A}

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. enat n < esize A \<Longrightarrow> nth_least A n \<in> A; enat (Suc n) < esize A\<rbrakk> \<Longrightarrow> nth_least A (Suc n) \<in> A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_least A (Suc n) \<in> A
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
nth_least (A - {least A}) n \<in> A - {least A}

goal (1 subgoal):
 1. nth_least A (Suc n) \<in> A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_least A (Suc n) \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma point_rep_number_inv: "size {# b \<in># \<B> . x \<notin> b #} = \<b> - (\<B> rep x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (filter_mset ((\<notin>) x) \<B>) = \<b> - \<B> rep x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. size (filter_mset ((\<notin>) x) \<B>) = \<b> - \<B> rep x
[PROOF STEP]
have "\<b> = size {# b \<in># \<B> . x \<notin> b #} + size {# b \<in># \<B> . x \<in> b #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<b> = size (filter_mset ((\<notin>) x) \<B>) + size (filter_mset ((\<in>) x) \<B>)
[PROOF STEP]
using multiset_partition
[PROOF STATE]
proof (prove)
using this:
?M = filter_mset ?P ?M + {#x \<in># ?M. \<not> ?P x#}

goal (1 subgoal):
 1. \<b> = size (filter_mset ((\<notin>) x) \<B>) + size (filter_mset ((\<in>) x) \<B>)
[PROOF STEP]
by (metis add.commute size_union)
[PROOF STATE]
proof (state)
this:
\<b> = size (filter_mset ((\<notin>) x) \<B>) + size (filter_mset ((\<in>) x) \<B>)

goal (1 subgoal):
 1. size (filter_mset ((\<notin>) x) \<B>) = \<b> - \<B> rep x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<b> = size (filter_mset ((\<notin>) x) \<B>) + size (filter_mset ((\<in>) x) \<B>)

goal (1 subgoal):
 1. size (filter_mset ((\<notin>) x) \<B>) = \<b> - \<B> rep x
[PROOF STEP]
by (simp add: point_replication_number_def)
[PROOF STATE]
proof (state)
this:
size (filter_mset ((\<notin>) x) \<B>) = \<b> - \<B> rep x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intersect_num_commute: "b1 |\<inter>| b2 = b2 |\<inter>| b1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b1 |\<inter>| b2 = b2 |\<inter>| b1
[PROOF STEP]
by (simp add: inf_commute intersection_number_def)


[STATEMENT]
lemma init_impl: "(ei, e) \<in> ES \<Longrightarrow>
    c.init_impl ei \<le>\<Down>(\<langle>ES\<rangle>simple_state_rel) (RETURN (a.empty_state e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ei, e) \<in> ES \<Longrightarrow> c.init_impl ei \<le> \<Down> (\<langle>ES\<rangle>simple_state_rel) (RETURN (a.empty_state e))
[PROOF STEP]
unfolding c.init_impl_def a.empty_state_def simple_state_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ei, e) \<in> ES \<Longrightarrow> RETURN \<lparr>ss_stack = [], on_stack = {}, visited = {}, \<dots> = ei\<rparr> \<le> \<Down> {(s, s'). ss_stack s = map (\<lambda>u. (u, pending s' `` {u})) (stack s') \<and> on_stack s = set (stack s') \<and> visited s = dom (discovered s') \<and> dom (finished s') = dom (discovered s') - set (stack s') \<and> set (stack s') \<subseteq> dom (discovered s') \<and> (simple_state.more s, state.more s') \<in> ES} (RETURN \<lparr>counter = 0, discovered = Map.empty, finished = Map.empty, pending = {}, stack = [], tree_edges = {}, back_edges = {}, cross_edges = {}, \<dots> = e\<rparr>)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma tendsto_zero_norm_bound:
  "\<forall>x. \<parallel>G x\<parallel> \<le> \<parallel>F x\<parallel> \<Longrightarrow> (F \<longlongrightarrow> 0) net \<Longrightarrow> (G \<longlongrightarrow> 0) net"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. \<parallel>G x\<parallel> \<le> \<parallel>F x\<parallel>; (F \<longlongrightarrow> (0::'c)) net\<rbrakk> \<Longrightarrow> (G \<longlongrightarrow> (0::'b)) net
[PROOF STEP]
apply(unfold tendsto_iff dist_norm, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e. \<lbrakk>\<forall>x. \<parallel>G x\<parallel> \<le> \<parallel>F x\<parallel>; \<forall>e>0. \<forall>\<^sub>F x in net. \<parallel>F x\<parallel> < e; 0 < e\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in net. \<parallel>G x\<parallel> < e
[PROOF STEP]
apply(rule_tac P="\<lambda>x. \<parallel>F x\<parallel> < e" in eventually_mono, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e x. \<lbrakk>\<forall>x. \<parallel>G x\<parallel> \<le> \<parallel>F x\<parallel>; \<forall>e>0. \<forall>\<^sub>F x in net. \<parallel>F x\<parallel> < e; 0 < e; \<parallel>F x\<parallel> < e\<rbrakk> \<Longrightarrow> \<parallel>G x\<parallel> < e
[PROOF STEP]
by (rename_tac e z) (erule_tac x=z in allE, simp)


[STATEMENT]
lemma vid_on_mono:
  assumes "A \<subseteq>\<^sub>\<circ> B"
  shows "vid_on A \<subseteq>\<^sub>\<circ> vid_on B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vid_on A \<subseteq>\<^sub>\<circ> vid_on B
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq>\<^sub>\<circ> B

goal (1 subgoal):
 1. vid_on A \<subseteq>\<^sub>\<circ> vid_on B
[PROOF STEP]
by auto


[STATEMENT]
lemma eventually_or: "\<diamond> (p \<squnion> q) = (\<diamond> p) \<squnion> (\<diamond> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<diamond> (p \<squnion> q) = \<diamond> p \<squnion> \<diamond> q
[PROOF STEP]
by (simp add: eventually_def SUP_sup_distrib)


[STATEMENT]
lemma mor_case_sum:
  "mor UNIV UNIV s1 s2 UNIV UNIV (case_sum (F1map id Inl Inl o s1) s1') (case_sum (F2map id Inl Inl o s2) s2') Inl Inl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mor UNIV UNIV s1 s2 UNIV UNIV (case_sum (F1map id Inl Inl \<circ> s1) s1') (case_sum (F2map id Inl Inl \<circ> s2) s2') Inl Inl
[PROOF STEP]
apply (tactic \<open>rtac @{context} (@{thm mor_UNIV} RS iffD2) 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F1map id Inl Inl \<circ> s1 = case_sum (F1map id Inl Inl \<circ> s1) s1' \<circ> Inl \<and> F2map id Inl Inl \<circ> s2 = case_sum (F2map id Inl Inl \<circ> s2) s2' \<circ> Inl
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. F1map id Inl Inl \<circ> s1 = case_sum (F1map id Inl Inl \<circ> s1) s1' \<circ> Inl
 2. F2map id Inl Inl \<circ> s2 = case_sum (F2map id Inl Inl \<circ> s2) s2' \<circ> Inl
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. case_sum (F1map id Inl Inl \<circ> s1) s1' \<circ> Inl = F1map id Inl Inl \<circ> s1
 2. F2map id Inl Inl \<circ> s2 = case_sum (F2map id Inl Inl \<circ> s2) s2' \<circ> Inl
[PROOF STEP]
apply (rule case_sum_o_inj(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F2map id Inl Inl \<circ> s2 = case_sum (F2map id Inl Inl \<circ> s2) s2' \<circ> Inl
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case_sum (F2map id Inl Inl \<circ> s2) s2' \<circ> Inl = F2map id Inl Inl \<circ> s2
[PROOF STEP]
apply (rule case_sum_o_inj(1))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hyp_port_strict_prefix:
  assumes "f \<in> hyps_along t is"
  shows "strict_prefix (hyp_port_path_for t is f) is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_prefix (hyp_port_path_for t is f) is
[PROOF STEP]
using hyp_port_prefix[OF assms]
[PROOF STATE]
proof (prove)
using this:
prefix (hyp_port_path_for t is f @ [hyp_port_i_for t is f]) is

goal (1 subgoal):
 1. strict_prefix (hyp_port_path_for t is f) is
[PROOF STEP]
by (simp add: strict_prefixI' prefix_order.dual_order.strict_trans1)


[STATEMENT]
lemma \<nu>_eq_lim: "\<nu> s = lim (\<lambda>n. \<nu>_fin n s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> s = lim (\<lambda>n. \<nu>_fin n s)
[PROOF STEP]
using \<nu>_def
[PROOF STATE]
proof (prove)
using this:
\<nu> ?s = lim (\<lambda>n. \<nu>_fin n ?s)

goal (1 subgoal):
 1. \<nu> s = lim (\<lambda>n. \<nu>_fin n s)
[PROOF STEP]
.


[STATEMENT]
lemma R_abort: "abort \<le> Ref \<lceil>P\<rceil> \<lceil>Q\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abort \<le> Ref \<lceil>P\<rceil> \<lceil>Q\<rceil>
[PROOF STEP]
by (rule R2, simp)

\<comment> \<open> Sequential Composition \<close>


[STATEMENT]
lemma abs_intruder_knowledge_append:
  "\<alpha>\<^sub>i\<^sub>k (A@B) \<I> =
    (ik\<^sub>l\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<cdot>\<^sub>\<alpha>\<^sub>s\<^sub>e\<^sub>t \<alpha>\<^sub>0 (db\<^sub>l\<^sub>s\<^sub>s\<^sub>t (A@B) \<I>) \<union>
    (ik\<^sub>l\<^sub>s\<^sub>s\<^sub>t B \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<cdot>\<^sub>\<alpha>\<^sub>s\<^sub>e\<^sub>t \<alpha>\<^sub>0 (db\<^sub>l\<^sub>s\<^sub>s\<^sub>t (A@B) \<I>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha>\<^sub>i\<^sub>k (A @ B) \<I> = (ik\<^sub>l\<^sub>s\<^sub>s\<^sub>t A \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<cdot>\<^sub>\<alpha>\<^sub>s\<^sub>e\<^sub>t \<alpha>\<^sub>0 (db\<^sub>l\<^sub>s\<^sub>s\<^sub>t (A @ B) \<I>) \<union> (ik\<^sub>l\<^sub>s\<^sub>s\<^sub>t B \<cdot>\<^sub>s\<^sub>e\<^sub>t \<I>) \<cdot>\<^sub>\<alpha>\<^sub>s\<^sub>e\<^sub>t \<alpha>\<^sub>0 (db\<^sub>l\<^sub>s\<^sub>s\<^sub>t (A @ B) \<I>)
[PROOF STEP]
by (metis unlabel_append abs_set_union image_Un ik\<^sub>s\<^sub>s\<^sub>t_append abs_intruder_knowledge_def)


[STATEMENT]
lemma seq_meas_rep_pos:
  assumes "\<forall>E \<in> sets M. \<mu> E < \<infinity>"
  shows "pos_meas_set (\<Union> i. seq_meas_rep i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos_meas_set (\<Union> (range seq_meas_rep))
[PROOF STEP]
proof (rule pos_meas_set_Union)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i. pos_meas_set (seq_meas_rep i)
 2. \<And>i. seq_meas_rep i \<in> sets M
 3. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
show " \<And>i. pos_meas_set (seq_meas_rep i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. pos_meas_set (seq_meas_rep i)
[PROOF STEP]
using seq_meas_rep_ex signed_measure_space.pos_sets_def
      signed_measure_space_axioms
[PROOF STATE]
proof (prove)
using this:
seq_meas_rep ?n \<in> pos_sets \<and> \<mu> (seq_meas_rep ?n) = seq_meas ?n
signed_measure_space ?M ?\<mu> \<Longrightarrow> signed_measure_space.pos_sets ?M ?\<mu> = {A \<in> sets ?M. signed_measure_space.pos_meas_set ?M ?\<mu> A}
signed_measure_space M \<mu>

goal (1 subgoal):
 1. \<And>i. pos_meas_set (seq_meas_rep i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pos_meas_set (seq_meas_rep ?i)

goal (2 subgoals):
 1. \<And>i. seq_meas_rep i \<in> sets M
 2. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pos_meas_set (seq_meas_rep ?i)
[PROOF STEP]
show "\<And>i. seq_meas_rep i \<in> sets M"
[PROOF STATE]
proof (prove)
using this:
pos_meas_set (seq_meas_rep ?i)

goal (1 subgoal):
 1. \<And>i. seq_meas_rep i \<in> sets M
[PROOF STEP]
by (simp add: pos_meas_setD1)
[PROOF STATE]
proof (state)
this:
seq_meas_rep ?i \<in> sets M

goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
show "\<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
have "(\<Union> (range seq_meas_rep)) \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (range seq_meas_rep) \<in> sets M
[PROOF STEP]
proof (rule sigma_algebra.countable_Union)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sigma_algebra ?\<Omega> (sets M)
 2. countable (range seq_meas_rep)
 3. range seq_meas_rep \<subseteq> sets M
[PROOF STEP]
show "sigma_algebra (space M) (sets M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sigma_algebra (space M) (sets M)
[PROOF STEP]
by (simp add: sets.sigma_algebra_axioms)
[PROOF STATE]
proof (state)
this:
sigma_algebra (space M) (sets M)

goal (2 subgoals):
 1. countable (range seq_meas_rep)
 2. range seq_meas_rep \<subseteq> sets M
[PROOF STEP]
show "countable (range seq_meas_rep)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable (range seq_meas_rep)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
countable (range seq_meas_rep)

goal (1 subgoal):
 1. range seq_meas_rep \<subseteq> sets M
[PROOF STEP]
show "range seq_meas_rep \<subseteq> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range seq_meas_rep \<subseteq> sets M
[PROOF STEP]
by (simp add: \<open>\<And>i. seq_meas_rep i \<in> sets M\<close> image_subset_iff)
[PROOF STATE]
proof (state)
this:
range seq_meas_rep \<subseteq> sets M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (range seq_meas_rep) \<in> sets M

goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
hence "\<mu> (\<Union> (range seq_meas_rep)) \<ge> 0 "
[PROOF STATE]
proof (prove)
using this:
\<Union> (range seq_meas_rep) \<in> sets M

goal (1 subgoal):
 1. 0 \<le> \<mu> (\<Union> (range seq_meas_rep))
[PROOF STEP]
using \<open>\<And>i. pos_meas_set (seq_meas_rep i)\<close> \<open>\<And>i. seq_meas_rep i \<in> sets M\<close>
        signed_measure_space.pos_meas_set_pos_lim signed_measure_space_axioms
[PROOF STATE]
proof (prove)
using this:
\<Union> (range seq_meas_rep) \<in> sets M
pos_meas_set (seq_meas_rep ?i)
seq_meas_rep ?i \<in> sets M
\<lbrakk>signed_measure_space ?M ?\<mu>; \<And>i. signed_measure_space.pos_meas_set ?M ?\<mu> (?A i); \<And>i. ?A i \<in> sets ?M\<rbrakk> \<Longrightarrow> 0 \<le> ?\<mu> (\<Union> (range ?A))
signed_measure_space M \<mu>

goal (1 subgoal):
 1. 0 \<le> \<mu> (\<Union> (range seq_meas_rep))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 \<le> \<mu> (\<Union> (range seq_meas_rep))

goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<mu> (\<Union> (range seq_meas_rep))

goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
using assms \<open>\<Union> (range seq_meas_rep) \<in> sets M\<close> abs_ereal_ge0
[PROOF STATE]
proof (prove)
using this:
0 \<le> \<mu> (\<Union> (range seq_meas_rep))
\<forall>E\<in>sets M. \<mu> E < \<infinity>
\<Union> (range seq_meas_rep) \<in> sets M
0 \<le> ?x \<Longrightarrow> \<bar>?x\<bar> = ?x

goal (1 subgoal):
 1. \<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>\<mu> (\<Union> (range seq_meas_rep))\<bar> < \<infinity>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lsc_hull_iff_greatest:
fixes f g :: "'a::metric_space \<Rightarrow> ereal"
shows "(g = lsc_hull f) \<longleftrightarrow>
  lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))"
(is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
assume "?lhs"
[PROOF STATE]
proof (state)
this:
g = lsc_hull f

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
hence "?rhs"
[PROOF STATE]
proof (prove)
using this:
g = lsc_hull f

goal (1 subgoal):
 1. lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))
[PROOF STEP]
using lsc_lsc_hull lsc_hull_le lsc_hull_greatest
[PROOF STATE]
proof (prove)
using this:
g = lsc_hull f
lsc (lsc_hull ?f)
lsc_hull ?f ?x \<le> ?f ?x
\<lbrakk>lsc ?g; \<forall>x. ?g x \<le> ?f x\<rbrakk> \<Longrightarrow> \<forall>x. ?g x \<le> lsc_hull ?f x

goal (1 subgoal):
 1. lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
g = lsc_hull f \<Longrightarrow> lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g = lsc_hull f \<Longrightarrow> lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
g = lsc_hull f \<Longrightarrow> lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
assume "?rhs"
[PROOF STATE]
proof (state)
this:
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
have "(lsc_hull f) x \<le> g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsc_hull f x \<le> g x
[PROOF STEP]
using \<open>?rhs\<close> lsc_lsc_hull lsc_hull_le
[PROOF STATE]
proof (prove)
using this:
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))
lsc (lsc_hull ?f)
lsc_hull ?f ?x \<le> ?f ?x

goal (1 subgoal):
 1. lsc_hull f x \<le> g x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lsc_hull f x \<le> g x

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lsc_hull f x \<le> g x

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
have "(lsc_hull f) x \<ge> g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g x \<le> lsc_hull f x
[PROOF STEP]
using \<open>?rhs\<close> lsc_hull_greatest
[PROOF STATE]
proof (prove)
using this:
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))
\<lbrakk>lsc ?g; \<forall>x. ?g x \<le> ?f x\<rbrakk> \<Longrightarrow> \<forall>x. ?g x \<le> lsc_hull ?f x

goal (1 subgoal):
 1. g x \<le> lsc_hull f x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
g x \<le> lsc_hull f x

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lsc_hull f x \<le> g x
g x \<le> lsc_hull f x
[PROOF STEP]
have "(lsc_hull f) x = g x"
[PROOF STATE]
proof (prove)
using this:
lsc_hull f x \<le> g x
g x \<le> lsc_hull f x

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

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
lsc_hull f ?x2 = g ?x2

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
hence "?lhs"
[PROOF STATE]
proof (prove)
using this:
lsc_hull f ?x2 = g ?x2

goal (1 subgoal):
 1. g = lsc_hull f
[PROOF STEP]
by (simp add: ext)
[PROOF STATE]
proof (state)
this:
g = lsc_hull f

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)) \<Longrightarrow> g = lsc_hull f

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g = lsc_hull f \<Longrightarrow> lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)) \<Longrightarrow> g = lsc_hull f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g = lsc_hull f \<Longrightarrow> lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x))
lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)) \<Longrightarrow> g = lsc_hull f

goal (1 subgoal):
 1. (g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(g = lsc_hull f) = (lsc g \<and> (\<forall>x. g x \<le> f x) \<and> (\<forall>h. lsc h \<and> (\<forall>x. h x \<le> f x) \<longrightarrow> (\<forall>x. h x \<le> g x)))

goal:
No subgoals!
[PROOF STEP]
qed