[STATEMENT]
lemma cat_RK23_is_functor:
  assumes "\<FF> : cat_ordinal (2\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<open>cat_ordinal (2\<^sub>\<nat>)\<close> \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_ordinal (2\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
from ord_of_nat_\<omega>
[PROOF STATE]
proof (chain)
picking this:
?n\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
interpret cat_ordinal_2: finite_category \<alpha> \<open>cat_ordinal (2\<^sub>\<nat>)\<close>
[PROOF STATE]
proof (prove)
using this:
?n\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal (2\<^sub>\<nat>))
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
from ord_of_nat_\<omega>
[PROOF STATE]
proof (chain)
picking this:
?n\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
interpret cat_ordinal_3: finite_category \<alpha> \<open>cat_ordinal (3\<^sub>\<nat>)\<close>
[PROOF STATE]
proof (prove)
using this:
?n\<^sub>\<nat> \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> \<open>cat_ordinal (2\<^sub>\<nat>)\<close> \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_ordinal (2\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_functorI')
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (RK23 \<FF>)
 3. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 4. category \<alpha> \<CC>
 5. vcard (RK23 \<FF>) = 4\<^sub>\<nat>
 6. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 7. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 8. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 9. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
A total of 15 subgoals...
[PROOF STEP]
show "vfsequence (RK23 \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (RK23 \<FF>)
[PROOF STEP]
unfolding RK23_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<lambda>a\<in>\<^sub>\<circ>cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>. if a = []\<^sub>\<circ> \<Rightarrow> \<FF>\<lparr>ObjMap\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> | a = 1\<^sub>\<nat> \<Rightarrow> \<FF>\<lparr>ObjMap\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> | a = 2\<^sub>\<nat> \<Rightarrow> \<FF>\<lparr>ObjMap\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> | otherwise \<Rightarrow> \<FF>\<lparr>HomCod\<rparr>\<lparr>Obj\<rparr>, \<lambda>f\<in>\<^sub>\<circ>cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>. if f = [[]\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ> \<Rightarrow> []\<^sub>\<circ> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> []\<^sub>\<circ> | f = [[]\<^sub>\<circ>, 1\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> []\<^sub>\<circ> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [[]\<^sub>\<circ>, 2\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> []\<^sub>\<circ> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [1\<^sub>\<nat>, 1\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> 1\<^sub>\<nat> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [1\<^sub>\<nat>, 2\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> 1\<^sub>\<nat> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [2\<^sub>\<nat>, 2\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> 1\<^sub>\<nat> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | otherwise \<Rightarrow> \<FF>\<lparr>HomCod\<rparr>\<lparr>Arr\<rparr>, cat_ordinal (3\<^sub>\<nat>), \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequence (RK23 \<FF>)

goal (14 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 3. category \<alpha> \<CC>
 4. vcard (RK23 \<FF>) = 4\<^sub>\<nat>
 5. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 6. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 7. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 8. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A total of 14 subgoals...
[PROOF STEP]
show "vcard (RK23 \<FF>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (RK23 \<FF>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding RK23_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<lambda>a\<in>\<^sub>\<circ>cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>. if a = []\<^sub>\<circ> \<Rightarrow> \<FF>\<lparr>ObjMap\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> | a = 1\<^sub>\<nat> \<Rightarrow> \<FF>\<lparr>ObjMap\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> | a = 2\<^sub>\<nat> \<Rightarrow> \<FF>\<lparr>ObjMap\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> | otherwise \<Rightarrow> \<FF>\<lparr>HomCod\<rparr>\<lparr>Obj\<rparr>, \<lambda>f\<in>\<^sub>\<circ>cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>. if f = [[]\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ> \<Rightarrow> []\<^sub>\<circ> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> []\<^sub>\<circ> | f = [[]\<^sub>\<circ>, 1\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> []\<^sub>\<circ> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [[]\<^sub>\<circ>, 2\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> []\<^sub>\<circ> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [1\<^sub>\<nat>, 1\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> 1\<^sub>\<nat> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [1\<^sub>\<nat>, 2\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> 1\<^sub>\<nat> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | f = [2\<^sub>\<nat>, 2\<^sub>\<nat>]\<^sub>\<circ> \<Rightarrow> 1\<^sub>\<nat> \<otimes>\<^sub>H\<^sub>M\<^sub>.\<^sub>A\<^bsub>\<FF>\<^esub> 1\<^sub>\<nat> | otherwise \<Rightarrow> \<FF>\<lparr>HomCod\<rparr>\<lparr>Arr\<rparr>, cat_ordinal (3\<^sub>\<nat>), \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (RK23 \<FF>) = 4\<^sub>\<nat>

goal (13 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 3. category \<alpha> \<CC>
 4. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 5. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 6. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ArrMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "\<R>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
proof(rule vsv.vsv_vrange_vsubset, unfold cat_Kan_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr> \<Longrightarrow> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr> \<Longrightarrow> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr> \<Longrightarrow> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
[PROOF STEP]
consider \<open>x = 0\<close> | \<open>x = 1\<^sub>\<nat>\<close> | \<open>x = 2\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<lbrakk>x = []\<^sub>\<circ> \<Longrightarrow> thesis; x = 1\<^sub>\<nat> \<Longrightarrow> thesis; x = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding cat_ordinal_cs_simps three
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>, 2\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>x = []\<^sub>\<circ> \<Longrightarrow> thesis; x = 1\<^sub>\<nat> \<Longrightarrow> thesis; x = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>x = []\<^sub>\<circ> \<Longrightarrow> ?thesis; x = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; x = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr> \<Longrightarrow> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x = []\<^sub>\<circ> \<Longrightarrow> ?thesis; x = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; x = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x = []\<^sub>\<circ> \<Longrightarrow> ?thesis; x = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; x = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by cases
          (
            cs_concl
              cs_simp: cat_Kan_cs_simps cat_ordinal_cs_simps omega_of_set
              cs_intro: cat_cs_intros nat_omega_intros
          )+
[PROOF STATE]
proof (state)
this:
RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
qed (cs_concl cs_shallow cs_intro: cat_Kan_cs_intros)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 3. category \<alpha> \<CC>
 4. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 5. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 6. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ArrMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b \<Longrightarrow> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
      if "f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
from 0123 that
[PROOF STATE]
proof (chain)
picking this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat>
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat>
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b

goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (elim cat_ordinal_3_is_arrE; simp only:)
          (
            cs_concl
              cs_simp: cat_Kan_cs_simps
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
[PROOF STATE]
proof (state)
this:
RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> ?b \<Longrightarrow> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> : RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 3. category \<alpha> \<CC>
 4. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 5. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 6. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ArrMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>
 10. \<And>b c g a f. \<lbrakk>g : b \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> c; f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b\<rbrakk> \<Longrightarrow> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g \<circ>\<^sub>A\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> f\<rparr> = RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
A total of 11 subgoals...
[PROOF STEP]
show
      "RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g \<circ>\<^sub>A\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> f\<rparr> =
        RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
      if "g : b \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> c" and "f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b"
      for b c g a f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g \<circ>\<^sub>A\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> f\<rparr> = RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
using 0123 that
[PROOF STATE]
proof (prove)
using this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 2\<^sub>\<nat>
1\<^sub>\<nat> \<in>\<^sub>\<circ> 2\<^sub>\<nat>
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
1\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
2\<^sub>\<nat> \<in>\<^sub>\<circ> 3\<^sub>\<nat>
g : b \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> c
f : a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> b

goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g \<circ>\<^sub>A\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> f\<rparr> = RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>g\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
by (elim cat_ordinal_3_is_arrE; simp only:; (solves\<open>simp\<close>)?) (*slow*)
        (
          cs_concl
            cs_simp:
              cat_ordinal_cs_simps
              cat_Kan_cs_simps
              \<FF>.cf_ArrMap_Comp[symmetric]
            cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
        )+
[PROOF STATE]
proof (state)
this:
\<lbrakk>?g : ?b \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> ?b\<rbrakk> \<Longrightarrow> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>?g \<circ>\<^sub>A\<^bsub>cat_ordinal (3\<^sub>\<nat>)\<^esub> ?f\<rparr> = RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>?g\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 3. category \<alpha> \<CC>
 4. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 5. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 6. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ArrMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>
 10. \<And>c. c \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr> \<Longrightarrow> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
show "RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>"
      if "c \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
c \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
[PROOF STEP]
consider \<open>c = 0\<close> | \<open>c = 1\<^sub>\<nat>\<close> | \<open>c = 2\<^sub>\<nat>\<close>
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<lbrakk>c = []\<^sub>\<circ> \<Longrightarrow> thesis; c = 1\<^sub>\<nat> \<Longrightarrow> thesis; c = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding cat_ordinal_components three
[PROOF STATE]
proof (prove)
using this:
c \<in>\<^sub>\<circ> ZFC_in_HOL.set {[]\<^sub>\<circ>, 1\<^sub>\<nat>, 2\<^sub>\<nat>}

goal (1 subgoal):
 1. \<lbrakk>c = []\<^sub>\<circ> \<Longrightarrow> thesis; c = 1\<^sub>\<nat> \<Longrightarrow> thesis; c = 2\<^sub>\<nat> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>c = []\<^sub>\<circ> \<Longrightarrow> ?thesis; c = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; c = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>c = []\<^sub>\<circ> \<Longrightarrow> ?thesis; c = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; c = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>c = []\<^sub>\<circ> \<Longrightarrow> ?thesis; c = 1\<^sub>\<nat> \<Longrightarrow> ?thesis; c = 2\<^sub>\<nat> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
by (cases, use 0123 in \<open>simp_all only:\<close>)
          (
            cs_concl
              cs_simp:
                cat_ordinal_cs_simps
                cat_Kan_cs_simps
                is_functor.cf_ObjMap_CId[symmetric]
              cs_intro: V_cs_intros cat_cs_intros cat_ordinal_cs_intros
          )+
[PROOF STATE]
proof (state)
this:
RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?c \<in>\<^sub>\<circ> cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr> \<Longrightarrow> RK23 \<FF>\<lparr>ArrMap\<rparr>\<lparr>cat_ordinal (3\<^sub>\<nat>)\<lparr>CId\<rparr>\<lparr>?c\<rparr>\<rparr> = \<CC>\<lparr>CId\<rparr>\<lparr>RK23 \<FF>\<lparr>ObjMap\<rparr>\<lparr>?c\<rparr>\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> (cat_ordinal (3\<^sub>\<nat>))
 3. category \<alpha> \<CC>
 4. RK23 \<FF>\<lparr>HomDom\<rparr> = cat_ordinal (3\<^sub>\<nat>)
 5. RK23 \<FF>\<lparr>HomCod\<rparr> = \<CC>
 6. vsv (RK23 \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (RK23 \<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ObjMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (RK23 \<FF>\<lparr>ArrMap\<rparr>) = cat_ordinal (3\<^sub>\<nat>)\<lparr>Arr\<rparr>
[PROOF STEP]
qed
    (
      cs_concl cs_shallow
        cs_simp: cat_Kan_cs_simps cs_intro: cat_cs_intros cat_Kan_cs_intros
    )+
[PROOF STATE]
proof (state)
this:
RK23 \<FF> : cat_ordinal (3\<^sub>\<nat>) \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "rewrite_iter_slow (X\<^sub>n prop\<^sub>n(''a'') U\<^sub>n (X\<^sub>n nprop\<^sub>n(''a''))) = X\<^sub>n (F\<^sub>n nprop\<^sub>n(''a''))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rewrite_iter_slow (X\<^sub>n prop\<^sub>n(''a'') U\<^sub>n X\<^sub>n nprop\<^sub>n(''a'')) = X\<^sub>n (F\<^sub>n nprop\<^sub>n(''a''))
[PROOF STEP]
by eval


[STATEMENT]
lemma ani_top:
  "ani(top) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ani top = bot
[PROOF STEP]
by (simp add: an_top ani_def)


[STATEMENT]
lemma an_omega_below_an_star:
  "an(x\<^sup>\<omega>) \<le> an(x\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. an (x\<^sup>\<omega>) \<le> an (x\<^sup>\<star>)
[PROOF STEP]
by (simp add: an_n_order n_star_below_n_omega)


[STATEMENT]
lemma op_max_norms_eq_at_diag: "\<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p = \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p = \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p \<le> \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x
 2. \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
have "{\<bar>f i\<bar> |i. i \<in> UNIV} \<subseteq> {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<bar>f i\<bar> |i. i \<in> UNIV} \<subseteq> {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV}
[PROOF STEP]
by (smt Collect_mono diag_mat_vec_nth_simps(1))
[PROOF STATE]
proof (state)
this:
{\<bar>f i\<bar> |i. i \<in> UNIV} \<subseteq> {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV}

goal (2 subgoals):
 1. \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p \<le> \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x
 2. \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
thus "\<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p \<le> \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x"
[PROOF STATE]
proof (prove)
using this:
{\<bar>f i\<bar> |i. i \<in> UNIV} \<subseteq> {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV}

goal (1 subgoal):
 1. \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p \<le> \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x
[PROOF STEP]
unfolding op_norm_diag_mat_eq max_norm_def
[PROOF STATE]
proof (prove)
using this:
{\<bar>f i\<bar> |i. i \<in> UNIV} \<subseteq> {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV}

goal (1 subgoal):
 1. Max {\<bar>f i\<bar> |i. i \<in> UNIV} \<le> Max {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV}
[PROOF STEP]
by (rule Max.subset_imp) (blast, simp only: finite_image_of_finite2)
[PROOF STATE]
proof (state)
this:
\<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p \<le> \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x

goal (1 subgoal):
 1. \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
have "Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
apply(rule cSup_least, blast, clarify, case_tac "i = j", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<bar>f i\<bar> \<le> Sup {uu_. \<exists>i. uu_ = \<bar>f i\<bar>}
 2. \<And>x i j. \<lbrakk>i \<in> UNIV; j \<in> UNIV; i \<noteq> j\<rbrakk> \<Longrightarrow> \<bar>diag_mat f $ i $ j\<bar> \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
by (rule cSup_upper, blast, simp_all) (rule cSup_upper2, auto)
[PROOF STATE]
proof (state)
this:
Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV}

goal (1 subgoal):
 1. \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
thus "\<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p"
[PROOF STATE]
proof (prove)
using this:
Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV}

goal (1 subgoal):
 1. \<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
unfolding op_norm_diag_mat_eq max_norm_def
[PROOF STATE]
proof (prove)
using this:
Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV}

goal (1 subgoal):
 1. Max {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Max {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
apply (subst cSup_eq_Max[symmetric], simp only: finite_image_of_finite2, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Sup {\<bar>f i\<bar> |i. i \<in> UNIV} \<Longrightarrow> Sup {\<bar>diag_mat f $ i $ j\<bar> |i j. i \<in> UNIV \<and> j \<in> UNIV} \<le> Max {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
by (subst cSup_eq_Max[symmetric], simp, blast)
[PROOF STATE]
proof (state)
this:
\<parallel>diag_mat f\<parallel>\<^sub>m\<^sub>a\<^sub>x \<le> \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_distrib_right:
  "sum f A * r = (\<Sum>n\<in>A. f n * r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
proof (cases "finite A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
 2. infinite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite A

goal (2 subgoals):
 1. finite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
 2. infinite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sum f {} * r = (\<Sum>n\<in>{}. f n * r)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum f F * r = (\<Sum>n\<in>F. f n * r)\<rbrakk> \<Longrightarrow> sum f (insert x F) * r = (\<Sum>n\<in>insert x F. f n * r)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. sum f {} * r = (\<Sum>n\<in>{}. f n * r)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum f F * r = (\<Sum>n\<in>F. f n * r)\<rbrakk> \<Longrightarrow> sum f (insert x F) * r = (\<Sum>n\<in>insert x F. f n * r)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {} * r = (\<Sum>n\<in>{}. f n * r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {} * r = (\<Sum>n\<in>{}. f n * r)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum f F * r = (\<Sum>n\<in>F. f n * r)\<rbrakk> \<Longrightarrow> sum f (insert x F) * r = (\<Sum>n\<in>insert x F. f n * r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum f F * r = (\<Sum>n\<in>F. f n * r)\<rbrakk> \<Longrightarrow> sum f (insert x F) * r = (\<Sum>n\<in>insert x F. f n * r)
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
sum f A * r = (\<Sum>n\<in>A. f n * r)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; sum f F * r = (\<Sum>n\<in>F. f n * r)\<rbrakk> \<Longrightarrow> sum f (insert x F) * r = (\<Sum>n\<in>insert x F. f n * r)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
sum f A * r = (\<Sum>n\<in>A. f n * r)

goal (1 subgoal):
 1. sum f (insert x A) * r = (\<Sum>n\<in>insert x A. f n * r)
[PROOF STEP]
by (simp add: distrib_right)
[PROOF STATE]
proof (state)
this:
sum f (insert x A) * r = (\<Sum>n\<in>insert x A. f n * r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum f A * r = (\<Sum>n\<in>A. f n * r)

goal (1 subgoal):
 1. infinite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite A

goal (1 subgoal):
 1. infinite A \<Longrightarrow> sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite A

goal (1 subgoal):
 1. sum f A * r = (\<Sum>n\<in>A. f n * r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f A * r = (\<Sum>n\<in>A. f n * r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_bezout_ext_is_bezout:
  assumes "is_bezout_ext bezout"
  shows "is_bezout (\<lambda>a b. case bezout a b of (x,xa,u,v, gcd') \<Rightarrow> (x,xa,gcd'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_bezout (\<lambda>a b. case bezout a b of (x, xa, u, v, gcd') \<Rightarrow> (x, xa, gcd'))
[PROOF STEP]
unfolding is_bezout_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. let (p, q, gcd_a_b) = case bezout a b of (x, xaa, u, v, gcd') \<Rightarrow> (x, xaa, gcd') in p * a + q * b = gcd_a_b \<and> gcd_a_b dvd a \<and> gcd_a_b dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd gcd_a_b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_bezout_ext bezout

goal (1 subgoal):
 1. \<forall>a b. let (p, q, gcd_a_b) = case bezout a b of (x, xaa, u, v, gcd') \<Rightarrow> (x, xaa, gcd') in p * a + q * b = gcd_a_b \<and> gcd_a_b dvd a \<and> gcd_a_b dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd gcd_a_b)
[PROOF STEP]
unfolding is_bezout_ext_def Let_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a b. case bezout a b of (p, q, u, v, gcd_a_b) \<Rightarrow> p * a + q * b = gcd_a_b \<and> gcd_a_b dvd a \<and> gcd_a_b dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd gcd_a_b) \<and> gcd_a_b * u = - b \<and> gcd_a_b * v = a

goal (1 subgoal):
 1. \<forall>a b. case case bezout a b of (x, xaa, u, v, gcd') \<Rightarrow> (x, xaa, gcd') of (p, q, gcd_a_b) \<Rightarrow> p * a + q * b = gcd_a_b \<and> gcd_a_b dvd a \<and> gcd_a_b dvd b \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd gcd_a_b)
[PROOF STEP]
by (simp add: split_beta)


[STATEMENT]
lemma opartial_net_preserves_subnets:
  assumes "((\<sigma>, SubnetS s t), a, (\<sigma>', st')) \<in> opnet_sos (trans (opnet np p1)) (trans (opnet np p2))"
    shows "\<exists>s' t'. st' = SubnetS s' t'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s' t'. st' = SubnetS s' t'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<sigma>, SubnetS s t), a, \<sigma>', st') \<in> opnet_sos (automaton.trans (opnet np p1)) (automaton.trans (opnet np p2))

goal (1 subgoal):
 1. \<exists>s' t'. st' = SubnetS s' t'
[PROOF STEP]
by cases simp_all


[STATEMENT]
lemma ccomp_ccomp_m [simplified, intro]:
  assumes
    A: "ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>"
      (is "?P \<Turnstile> _\<box>") and
    B: "\<And>cfs. ccomp c\<^sub>1 \<Turnstile> cfs\<box> \<Longrightarrow> mpred (ccomp c\<^sub>1) cfs 0 (length cfs - 1)" and
    C: "\<And>cfs. ccomp c\<^sub>2 \<Turnstile> cfs\<box> \<Longrightarrow> mpred (ccomp c\<^sub>2) cfs 0 (length cfs - 1)"
  shows "mpred ?P cfs 0 (length cfs - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
have "\<exists>k < length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and>
    mpred ([] @ ?P) cfs 0 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k<length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and> mpred ([] @ ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k
[PROOF STEP]
using A and B
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>
ccomp c\<^sub>1 \<Turnstile> ?cfs\<box> \<Longrightarrow> mpred (ccomp c\<^sub>1) ?cfs 0 (length ?cfs - 1)

goal (1 subgoal):
 1. \<exists>k<length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and> mpred ([] @ ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k
[PROOF STEP]
by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
[PROOF STATE]
proof (state)
this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and> mpred ([] @ ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and> mpred ([] @ ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k
[PROOF STEP]
obtain k s s' stk where
   "cfs ! 0 = (0, s, stk) \<and> mpred ?P cfs 0 k \<and> k < length cfs" and
    D: "cfs ! k = (size (ccomp c\<^sub>1), s', stk)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and> mpred ([] @ ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k

goal (1 subgoal):
 1. (\<And>s stk k s'. \<lbrakk>cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs; cfs ! k = (size (ccomp c\<^sub>1), s', stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<exists>k<length cfs. cpred c\<^sub>1 (off [] (cfs ! 0)) (off [] (cfs ! k)) \<and> mpred ([] @ ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. (\<And>s stk k s'. \<lbrakk>cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs; cfs ! k = (size (ccomp c\<^sub>1), s', stk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: cpred_def execl_all_def)
[PROOF STATE]
proof (state)
this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)
[PROOF STEP]
have "\<exists>k' < length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k))
    (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'"
[PROOF STATE]
proof (prove)
using this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)

goal (1 subgoal):
 1. \<exists>k'<length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k)) (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'
[PROOF STEP]
using A and C
[PROOF STATE]
proof (prove)
using this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>
ccomp c\<^sub>2 \<Turnstile> ?cfs\<box> \<Longrightarrow> mpred (ccomp c\<^sub>2) ?cfs 0 (length ?cfs - 1)

goal (1 subgoal):
 1. \<exists>k'<length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k)) (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'
[PROOF STEP]
by (rule_tac execl_all_sub_m, insert execl_all_def, auto)
[PROOF STATE]
proof (state)
this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k)) (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k)) (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'
[PROOF STEP]
obtain k' where
   "fst (cfs ! k') = size ?P \<and> mpred ?P cfs k k' \<and> k' < length cfs"
[PROOF STATE]
proof (prove)
using this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k)) (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'

goal (1 subgoal):
 1. (\<And>k'. fst (cfs ! k') = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs k k' \<and> k' < length cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
\<exists>k'<length cfs. cpred c\<^sub>2 (off (ccomp c\<^sub>1) (cfs ! k)) (off (ccomp c\<^sub>1) (cfs ! k')) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2 @ []) cfs k k'
cfs ! k = (size (ccomp c\<^sub>1), s', stk)

goal (1 subgoal):
 1. (\<And>k'. fst (cfs ! k') = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs k k' \<and> k' < length cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (fastforce simp: cpred_def)
[PROOF STATE]
proof (state)
this:
fst (cfs ! k') = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs k k' \<and> k' < length cfs

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)
fst (cfs ! k') = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs k k' \<and> k' < length cfs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)
fst (cfs ! k') = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs k k' \<and> k' < length cfs

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
cfs ! 0 = (0, s, stk) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 k \<and> k < length cfs
cfs ! k = (size (ccomp c\<^sub>1), s', stk)
fst (cfs ! k') = size (ccomp c\<^sub>1 @ ccomp c\<^sub>2) \<and> mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs k k' \<and> k' < length cfs
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<Turnstile> cfs\<box>

goal (1 subgoal):
 1. mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)
[PROOF STEP]
by (insert execl_last [of ?P cfs k'], simp add: execl_all_def,
     auto intro: mpred_merge)
[PROOF STATE]
proof (state)
this:
mpred (ccomp c\<^sub>1 @ ccomp c\<^sub>2) cfs 0 (length cfs - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finiteUn: "finite (A Un B) = (finite A & finite B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (A \<union> B) = (finite A \<and> finite B)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma set_equality_technical:
  assumes "{x} \<union> (set xs) = {y} \<union> (set ys)"
      and "x \<notin> set xs"
      and "y \<notin> set ys"
      and "y \<in> set xs"
    shows "{x} \<union> (set xs - {y}) = set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x} \<union> (set xs - {y}) = set ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{x} \<union> set xs = {y} \<union> set ys
x \<notin> set xs
y \<notin> set ys
y \<in> set xs

goal (1 subgoal):
 1. {x} \<union> (set xs - {y}) = set ys
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma satL_tL[simp]:
assumes l: "Ik.Ik.wtL l" and \<xi>: "Ik.wtE \<xi>"
shows "TE.satL (eenv \<xi>) (tL l) \<longleftrightarrow> Ik.satL \<xi> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TE.satL (eenv \<xi>) (tL l) = Ik.satL \<xi> l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Ik.wtL l
Ik.wtE \<xi>

goal (1 subgoal):
 1. TE.satL (eenv \<xi>) (tL l) = Ik.satL \<xi> l
[PROOF STEP]
apply(cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>Ik.wtL l; Ik.wtE \<xi>; l = Pos x1\<rbrakk> \<Longrightarrow> TE.satL (eenv \<xi>) (tL l) = Ik.satL \<xi> l
 2. \<And>x2. \<lbrakk>Ik.wtL l; Ik.wtE \<xi>; l = Neg x2\<rbrakk> \<Longrightarrow> TE.satL (eenv \<xi>) (tL l) = Ik.satL \<xi> l
[PROOF STEP]
apply (rename_tac [!] atm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>atm. \<lbrakk>Ik.wtL l; Ik.wtE \<xi>; l = Pos atm\<rbrakk> \<Longrightarrow> TE.satL (eenv \<xi>) (tL l) = Ik.satL \<xi> l
 2. \<And>atm. \<lbrakk>Ik.wtL l; Ik.wtE \<xi>; l = Neg atm\<rbrakk> \<Longrightarrow> TE.satL (eenv \<xi>) (tL l) = Ik.satL \<xi> l
[PROOF STEP]
by (case_tac [!] atm) (auto simp add: intP_def)


[STATEMENT]
lemma ext_border_Cons:
  "Suc i + \<^bold>|u\<^bold>| = \<^bold>|w\<^bold>| \<Longrightarrow> u \<le>b w \<Longrightarrow> (w!i)#u \<le>b (w!i)#w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc i + \<^bold>|u\<^bold>| = \<^bold>|w\<^bold>|; u \<le>b w\<rbrakk> \<Longrightarrow> w ! i # u \<le>b w ! i # w
[PROOF STEP]
unfolding border_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc i + \<^bold>|u\<^bold>| = \<^bold>|w\<^bold>|; u \<le>p w \<and> u \<le>s w \<and> u \<noteq> w \<and> u \<noteq> \<epsilon>\<rbrakk> \<Longrightarrow> w ! i # u \<le>p w ! i # w \<and> w ! i # u \<le>s w ! i # w \<and> w ! i # u \<noteq> w ! i # w \<and> w ! i # u \<noteq> \<epsilon>
[PROOF STEP]
using ext_suf_Cons Cons_prefix_Cons list.discI list.inject
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc ?i + \<^bold>|?u\<^bold>| = \<^bold>|?w\<^bold>|; ?u \<le>s ?w\<rbrakk> \<Longrightarrow> ?w ! ?i # ?u \<le>s ?w ! ?i # ?w
(?x # ?xs \<le>p ?y # ?ys) = (?x = ?y \<and> ?xs \<le>p ?ys)
?list = ?x21.0 # ?x22.0 \<Longrightarrow> ?list \<noteq> \<epsilon>
(?x21.0 # ?x22.0 = ?y21.0 # ?y22.0) = (?x21.0 = ?y21.0 \<and> ?x22.0 = ?y22.0)

goal (1 subgoal):
 1. \<lbrakk>Suc i + \<^bold>|u\<^bold>| = \<^bold>|w\<^bold>|; u \<le>p w \<and> u \<le>s w \<and> u \<noteq> w \<and> u \<noteq> \<epsilon>\<rbrakk> \<Longrightarrow> w ! i # u \<le>p w ! i # w \<and> w ! i # u \<le>s w ! i # w \<and> w ! i # u \<noteq> w ! i # w \<and> w ! i # u \<noteq> \<epsilon>
[PROOF STEP]
by metis


[STATEMENT]
lemma gHomcomp:"\<lbrakk>Group F; Group G; Group H; f \<in> gHom F G; g \<in> gHom G H\<rbrakk>
    \<Longrightarrow> (g \<circ>\<^bsub>F\<^esub> f) \<in> gHom F H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group F; Group G; Group H; f \<in> gHom F G; g \<in> gHom G H\<rbrakk> \<Longrightarrow> g \<circ>\<^bsub>F\<^esub> f \<in> gHom F H
[PROOF STEP]
apply (simp add:gHom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F) \<and> f \<in> carrier F \<rightarrow> carrier G \<and> (\<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y); g \<in> extensional (carrier G) \<and> g \<in> carrier G \<rightarrow> carrier H \<and> (\<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y)\<rbrakk> \<Longrightarrow> g \<circ>\<^bsub>F\<^esub> f \<in> extensional (carrier F) \<and> g \<circ>\<^bsub>F\<^esub> f \<in> carrier F \<rightarrow> carrier H \<and> (\<forall>x\<in>carrier F. \<forall>y\<in>carrier F. (g \<circ>\<^bsub>F\<^esub> f) (x \<cdot>\<^bsub>F\<^esub> y) = (g \<circ>\<^bsub>F\<^esub> f) x \<cdot>\<^bsub>H\<^esub> (g \<circ>\<^bsub>F\<^esub> f) y)
[PROOF STEP]
apply (erule conjE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F); g \<in> extensional (carrier G); f \<in> carrier F \<rightarrow> carrier G; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y; g \<in> carrier G \<rightarrow> carrier H; \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y\<rbrakk> \<Longrightarrow> g \<circ>\<^bsub>F\<^esub> f \<in> extensional (carrier F) \<and> g \<circ>\<^bsub>F\<^esub> f \<in> carrier F \<rightarrow> carrier H \<and> (\<forall>x\<in>carrier F. \<forall>y\<in>carrier F. (g \<circ>\<^bsub>F\<^esub> f) (x \<cdot>\<^bsub>F\<^esub> y) = (g \<circ>\<^bsub>F\<^esub> f) x \<cdot>\<^bsub>H\<^esub> (g \<circ>\<^bsub>F\<^esub> f) y)
[PROOF STEP]
apply (simp add:cmpghom_def composition)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F); g \<in> extensional (carrier G); f \<in> carrier F \<rightarrow> carrier G; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y; g \<in> carrier G \<rightarrow> carrier H; \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y\<rbrakk> \<Longrightarrow> \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. compose (carrier F) g f (x \<cdot>\<^bsub>F\<^esub> y) = compose (carrier F) g f x \<cdot>\<^bsub>H\<^esub> compose (carrier F) g f y
[PROOF STEP]
apply (rule ballI)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F); g \<in> extensional (carrier G); f \<in> carrier F \<rightarrow> carrier G; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y; g \<in> carrier G \<rightarrow> carrier H; \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y; x \<in> carrier F; y \<in> carrier F\<rbrakk> \<Longrightarrow> compose (carrier F) g f (x \<cdot>\<^bsub>F\<^esub> y) = compose (carrier F) g f x \<cdot>\<^bsub>H\<^esub> compose (carrier F) g f y
[PROOF STEP]
apply (simp add:compose_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F); g \<in> extensional (carrier G); f \<in> carrier F \<rightarrow> carrier G; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y; g \<in> carrier G \<rightarrow> carrier H; \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y; x \<in> carrier F; y \<in> carrier F\<rbrakk> \<Longrightarrow> (x \<cdot>\<^bsub>F\<^esub> y \<in> carrier F \<longrightarrow> g (f x \<cdot>\<^bsub>G\<^esub> f y) = g (f x) \<cdot>\<^bsub>H\<^esub> g (f y)) \<and> (x \<cdot>\<^bsub>F\<^esub> y \<notin> carrier F \<longrightarrow> undefined = g (f x) \<cdot>\<^bsub>H\<^esub> g (f y))
[PROOF STEP]
apply (frule_tac x = x in funcset_mem [of "f" "carrier F" "carrier G"],
                                              assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F); g \<in> extensional (carrier G); f \<in> carrier F \<rightarrow> carrier G; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y; g \<in> carrier G \<rightarrow> carrier H; \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y; x \<in> carrier F; y \<in> carrier F; f x \<in> carrier G\<rbrakk> \<Longrightarrow> (x \<cdot>\<^bsub>F\<^esub> y \<in> carrier F \<longrightarrow> g (f x \<cdot>\<^bsub>G\<^esub> f y) = g (f x) \<cdot>\<^bsub>H\<^esub> g (f y)) \<and> (x \<cdot>\<^bsub>F\<^esub> y \<notin> carrier F \<longrightarrow> undefined = g (f x) \<cdot>\<^bsub>H\<^esub> g (f y))
[PROOF STEP]
apply (frule_tac x = y in funcset_mem [of "f" "carrier F" "carrier G"],
                                              assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>Group F; Group G; Group H; f \<in> extensional (carrier F); g \<in> extensional (carrier G); f \<in> carrier F \<rightarrow> carrier G; \<forall>x\<in>carrier F. \<forall>y\<in>carrier F. f (x \<cdot>\<^bsub>F\<^esub> y) = f x \<cdot>\<^bsub>G\<^esub> f y; g \<in> carrier G \<rightarrow> carrier H; \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. g (x \<cdot>\<^bsub>G\<^esub> y) = g x \<cdot>\<^bsub>H\<^esub> g y; x \<in> carrier F; y \<in> carrier F; f x \<in> carrier G; f y \<in> carrier G\<rbrakk> \<Longrightarrow> (x \<cdot>\<^bsub>F\<^esub> y \<in> carrier F \<longrightarrow> g (f x \<cdot>\<^bsub>G\<^esub> f y) = g (f x) \<cdot>\<^bsub>H\<^esub> g (f y)) \<and> (x \<cdot>\<^bsub>F\<^esub> y \<notin> carrier F \<longrightarrow> undefined = g (f x) \<cdot>\<^bsub>H\<^esub> g (f y))
[PROOF STEP]
apply (simp add:Group.mult_closed[of "F"])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gbij_automorph:"\<lbrakk>Group G; gbij\<^bsub>G,G\<^esub> f; gbij\<^bsub>G,G\<^esub> g\<rbrakk>  \<Longrightarrow>
                            gbij\<^bsub>G,G\<^esub> (g \<circ>\<^bsub>G\<^esub> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; gbij\<^bsub>G,G\<^esub> f; gbij\<^bsub>G,G\<^esub> g\<rbrakk> \<Longrightarrow> gbij\<^bsub>G,G\<^esub> (g \<circ>\<^bsub>G\<^esub> f)
[PROOF STEP]
apply (simp add:gbij_comp_bij)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma length_of_twcmpser:"\<lbrakk>Group G; Ugp E; tw_cmpser G (Suc n) f \<rbrakk> \<Longrightarrow>
      length_twcmpser G (Suc n) f =
                     (Suc n) - (card {i. i \<le> n \<and> ((Qw_cmpser G f) i \<cong> E)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; Ugp E; tw_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> length_twcmpser G (Suc n) f = Suc n - card {i. i \<le> n \<and> Qw_cmpser G f i \<cong> E}
[PROOF STEP]
apply (unfold length_twcmpser_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; Ugp E; tw_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> card (f ` {i. i \<le> Suc n}) - Suc 0 = Suc n - card {i. i \<le> n \<and> Qw_cmpser G f i \<cong> E}
[PROOF STEP]
apply (insert length_wcmpser0 [of "G" "E" "n"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; Ugp E; tw_cmpser G (Suc n) f; \<lbrakk>Group G; Ugp E\<rbrakk> \<Longrightarrow> \<forall>f. w_cmpser G (Suc n) f \<longrightarrow> card (f ` {i. i \<le> Suc n}) - 1 = Suc n - card {i. i \<le> n \<and> Qw_cmpser G f i \<cong> E}\<rbrakk> \<Longrightarrow> card (f ` {i. i \<le> Suc n}) - Suc 0 = Suc n - card {i. i \<le> n \<and> Qw_cmpser G f i \<cong> E}
[PROOF STEP]
apply (subgoal_tac "w_cmpser G (Suc n) f", rotate_tac -1,
       simp, simp,
       thin_tac "\<forall>f. w_cmpser G (Suc n) f \<longrightarrow>
           card (f ` {i. i \<le> (Suc n)}) - Suc 0 =
           Suc n - card {i. i \<le> n \<and> Qw_cmpser G f i \<cong> E}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; Ugp E; tw_cmpser G (Suc n) f\<rbrakk> \<Longrightarrow> w_cmpser G (Suc n) f
[PROOF STEP]
apply (simp add:tw_cmpser_def w_cmpser_def, erule conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; Ugp E; td_gchain G (Suc n) f; \<forall>l\<le>n. \<natural>\<^bsub>G\<^esub>f l \<triangleright> f (Suc l)\<rbrakk> \<Longrightarrow> d_gchain G (Suc n) f
[PROOF STEP]
apply (thin_tac "\<forall>i\<le> n. Gp G (f i) \<triangleright> f (Suc i)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Group G; Ugp E; td_gchain G (Suc n) f\<rbrakk> \<Longrightarrow> d_gchain G (Suc n) f
[PROOF STEP]
apply (simp add:td_gchain_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]:
  "(binop_ShiftLeft v1 v2 = Some va) \<longleftrightarrow>
   (\<exists>i1 i2. v1 = Intg i1 \<and> v2 = Intg i2 \<and> va = Inl (Intg (i1 << unat (i2 AND 0x1f))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (binop_ShiftLeft v1 v2 = \<lfloor>va\<rfloor>) = (\<exists>i1 i2. v1 = Intg i1 \<and> v2 = Intg i2 \<and> va = Inl (Intg (i1 << unat (i2 AND 31))))
[PROOF STEP]
by(cases "(v1, v2)" rule: binop_ShiftLeft.cases) auto


[STATEMENT]
lemma res_rc2: "x \<le> y \<Longrightarrow> z \<rightarrow> z \<cdot> x \<le> z \<rightarrow> z \<cdot> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> z \<rightarrow> z \<cdot> x \<le> z \<rightarrow> z \<cdot> y
[PROOF STEP]
by (metis local.res_c2 resr_eq residuated_multr)


[STATEMENT]
lemma horner_eval_eq_setsum:
  fixes x::"'a::linordered_idom"
  shows "horner_eval f x n = (\<Sum>i<n. f i * x^i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
have "horner_eval' f x v n = (\<Sum>i<n. f i * x^i) + v * x^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horner_eval' f x v n = (\<Sum>i<n. f i * x ^ i) + v * x ^ n
[PROOF STEP]
by (induction n arbitrary: v, simp_all add: distrib_left mult.commute)
[PROOF STATE]
proof (state)
this:
horner_eval' f x v n = (\<Sum>i<n. f i * x ^ i) + v * x ^ n

goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
horner_eval' f x ?v2 n = (\<Sum>i<n. f i * x ^ i) + ?v2 * x ^ n

goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
horner_eval' f x ?v2 n = (\<Sum>i<n. f i * x ^ i) + ?v2 * x ^ n

goal (1 subgoal):
 1. horner_eval f x n = (\<Sum>i<n. f i * x ^ i)
[PROOF STEP]
by (simp add: horner_eval_def)
[PROOF STATE]
proof (state)
this:
horner_eval f x n = (\<Sum>i<n. f i * x ^ i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma silent_move_observable_moves:
  "\<lbrakk>S,f \<turnstile> (n'',s'') =as\<Rightarrow> (n',s'); S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (n'',s'')\<rbrakk>
  \<Longrightarrow> S,f \<turnstile> (n,s) =a#as\<Rightarrow> (n',s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,f \<turnstile> (n'',s'') =as\<Rightarrow> (n',s'); S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (n'',s'')\<rbrakk> \<Longrightarrow> S,f \<turnstile> (n,s) =a # as\<Rightarrow> (n',s')
[PROOF STEP]
proof(induct rule:observable_moves.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S f na sa as n' s' aa n'' s''. \<lbrakk>S,f \<turnstile> (na,sa) =as\<Rightarrow>\<^sub>\<tau> (n',s'); S,f \<turnstile> (n',s') -aa\<rightarrow> (n'',s''); S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (na,sa)\<rbrakk> \<Longrightarrow> S,f \<turnstile> (n,s) =a # as @ [aa]\<Rightarrow> (n'',s'')
[PROOF STEP]
case (observable_moves_snoc S f nx sx as n' s' a' n'' s'')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (nx,sx) =as\<Rightarrow>\<^sub>\<tau> (n',s')
S,f \<turnstile> (n',s') -a'\<rightarrow> (n'',s'')
S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (nx,sx)

goal (1 subgoal):
 1. \<And>S f na sa as n' s' aa n'' s''. \<lbrakk>S,f \<turnstile> (na,sa) =as\<Rightarrow>\<^sub>\<tau> (n',s'); S,f \<turnstile> (n',s') -aa\<rightarrow> (n'',s''); S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (na,sa)\<rbrakk> \<Longrightarrow> S,f \<turnstile> (n,s) =a # as @ [aa]\<Rightarrow> (n'',s'')
[PROOF STEP]
from \<open>S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (nx,sx)\<close> \<open>S,f \<turnstile> (nx,sx) =as\<Rightarrow>\<^sub>\<tau> (n',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (nx,sx)
S,f \<turnstile> (nx,sx) =as\<Rightarrow>\<^sub>\<tau> (n',s')
[PROOF STEP]
have "S,f \<turnstile> (n,s) =a#as\<Rightarrow>\<^sub>\<tau> (n',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (nx,sx)
S,f \<turnstile> (nx,sx) =as\<Rightarrow>\<^sub>\<tau> (n',s')

goal (1 subgoal):
 1. S,f \<turnstile> (n,s) =a # as\<Rightarrow>\<^sub>\<tau> (n',s')
[PROOF STEP]
by(rule silent_moves_Cons)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (n,s) =a # as\<Rightarrow>\<^sub>\<tau> (n',s')

goal (1 subgoal):
 1. \<And>S f na sa as n' s' aa n'' s''. \<lbrakk>S,f \<turnstile> (na,sa) =as\<Rightarrow>\<^sub>\<tau> (n',s'); S,f \<turnstile> (n',s') -aa\<rightarrow> (n'',s''); S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (na,sa)\<rbrakk> \<Longrightarrow> S,f \<turnstile> (n,s) =a # as @ [aa]\<Rightarrow> (n'',s'')
[PROOF STEP]
with \<open>S,f \<turnstile> (n',s') -a'\<rightarrow> (n'',s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (n',s') -a'\<rightarrow> (n'',s'')
S,f \<turnstile> (n,s) =a # as\<Rightarrow>\<^sub>\<tau> (n',s')
[PROOF STEP]
have "S,f \<turnstile> (n,s) =(a#as)@[a']\<Rightarrow> (n'',s'')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (n',s') -a'\<rightarrow> (n'',s'')
S,f \<turnstile> (n,s) =a # as\<Rightarrow>\<^sub>\<tau> (n',s')

goal (1 subgoal):
 1. S,f \<turnstile> (n,s) =(a # as) @ [a']\<Rightarrow> (n'',s'')
[PROOF STEP]
by -(rule observable_moves.observable_moves_snoc)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (n,s) =(a # as) @ [a']\<Rightarrow> (n'',s'')

goal (1 subgoal):
 1. \<And>S f na sa as n' s' aa n'' s''. \<lbrakk>S,f \<turnstile> (na,sa) =as\<Rightarrow>\<^sub>\<tau> (n',s'); S,f \<turnstile> (n',s') -aa\<rightarrow> (n'',s''); S,f \<turnstile> (n,s) -a\<rightarrow>\<^sub>\<tau> (na,sa)\<rbrakk> \<Longrightarrow> S,f \<turnstile> (n,s) =a # as @ [aa]\<Rightarrow> (n'',s'')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (n,s) =(a # as) @ [a']\<Rightarrow> (n'',s'')

goal (1 subgoal):
 1. S,f \<turnstile> (n,s) =a # as @ [a']\<Rightarrow> (n'',s'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (n,s) =a # as @ [a']\<Rightarrow> (n'',s'')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prof_max_ge_all_in_pset:
  assumes "j \<in> firms"
  assumes "Y j \<in> profit_maximisation P (production_sets j)"
  shows "\<forall>y \<in> production_sets j. P \<bullet> Y j \<ge> P \<bullet> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>production_sets j. P \<bullet> y \<le> P \<bullet> Y j
[PROOF STEP]
using all_leq assms(2) profit_maximisation_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> arg_max_set ?f ?S \<Longrightarrow> \<forall>y\<in>?S. ?f y \<le> ?f ?x
Y j \<in> profit_maximisation P (production_sets j)
profit_maximisation ?P ?S = arg_max_set ((\<bullet>) ?P) ?S

goal (1 subgoal):
 1. \<forall>y\<in>production_sets j. P \<bullet> y \<le> P \<bullet> Y j
[PROOF STEP]
by fastforce


[STATEMENT]
lemma state_restrict_states[simp]: "states (restrict_states S \<phi>) = states \<phi> \<inter> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. states (restrict_states S \<phi>) = states \<phi> \<inter> S
[PROOF STEP]
by transfer (auto split: if_splits)


[STATEMENT]
lemma special_cosetsI: "T\<in>Pow S \<Longrightarrow> w\<in>W \<Longrightarrow> w +o \<langle>T\<rangle> \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T \<in> Pow S; w \<in> W\<rbrakk> \<Longrightarrow> w +o \<langle>T\<rangle> \<in> \

[PROOF STEP]
using special_cosets_def
[PROOF STATE]
proof (prove)
using this:
\
 \<equiv> \<Union>T\<in>Pow S. \<Union>w\<in>W. {w +o \<langle>T\<rangle>}

goal (1 subgoal):
 1. \<lbrakk>T \<in> Pow S; w \<in> W\<rbrakk> \<Longrightarrow> w +o \<langle>T\<rangle> \<in> \

[PROOF STEP]
by auto


[STATEMENT]
lemma enat_unfold_unique:
  assumes h: "!!x. h x = (if stop x then 0 else eSuc (h (next x)))"
  shows "h x = enat_unfold stop next x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h x = enat_unfold stop next x
[PROOF STEP]
by(coinduction arbitrary: x rule: enat_coinduct)(subst (1 3) h, auto)


[STATEMENT]
lemma foldli_image_aux:
    "foldli l (\<lambda>_. True) (\<lambda>x s. insert (f x) s) s0
    = s0 \<union> f`(set l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l (\<lambda>_. True) (\<lambda>x. insert (f x)) s0 = s0 \<union> f ` set l
[PROOF STEP]
by (induct l arbitrary: s0) auto


[STATEMENT]
lemma transversal_bound_negE:
  assumes transversal: "transversal_segment a b"
  assumes direction: "z \<in> {a -- b}" "f z \<bullet> (rot (a - b)) < 0"
  obtains d B where "d > 0" "0 < B"
    "\<And>x y. x \<in> {a -- b} \<Longrightarrow> dist x y \<le> d \<Longrightarrow> f y \<bullet> (rot (b - a)) \<ge> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {a--b}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {a--b}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from direction
[PROOF STATE]
proof (chain)
picking this:
z \<in> {a--b}
f z \<bullet> rot (a - b) < 0
[PROOF STEP]
have "z \<in> {b -- a}" "f z \<bullet> (rot (b - a)) > 0"
[PROOF STATE]
proof (prove)
using this:
z \<in> {a--b}
f z \<bullet> rot (a - b) < 0

goal (1 subgoal):
 1. z \<in> {b--a} &&& 0 < f z \<bullet> rot (b - a)
[PROOF STEP]
by (auto simp: closed_segment_commute rot_diff_commute[of b a])
[PROOF STATE]
proof (state)
this:
z \<in> {b--a}
0 < f z \<bullet> rot (b - a)

goal (1 subgoal):
 1. (\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {a--b}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from transversal_bound_posE[OF transversal_segment_reverse[OF transversal] this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {b--a}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain d B where "d > 0" "0 < B"
    "\<And>x y. x \<in> {a -- b} \<Longrightarrow> dist x y \<le> d \<Longrightarrow> f y \<bullet> (rot (b - a)) \<ge> B"
[PROOF STATE]
proof (prove)
using this:
(\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {b--a}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {a--b}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: closed_segment_commute)
[PROOF STATE]
proof (state)
this:
0 < d
0 < B
\<lbrakk>?x2 \<in> {a--b}; dist ?x2 ?y2 \<le> d\<rbrakk> \<Longrightarrow> B \<le> f ?y2 \<bullet> rot (b - a)

goal (1 subgoal):
 1. (\<And>d B. \<lbrakk>0 < d; 0 < B; \<And>x y. \<lbrakk>x \<in> {a--b}; dist x y \<le> d\<rbrakk> \<Longrightarrow> B \<le> f y \<bullet> rot (b - a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < d
0 < B
\<lbrakk>?x2 \<in> {a--b}; dist ?x2 ?y2 \<le> d\<rbrakk> \<Longrightarrow> B \<le> f ?y2 \<bullet> rot (b - a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < d
0 < B
\<lbrakk>?x2 \<in> {a--b}; dist ?x2 ?y2 \<le> d\<rbrakk> \<Longrightarrow> B \<le> f ?y2 \<bullet> rot (b - a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Disjoint_Eats_Imp: "{ Disjoint x z, Neg(y IN z) } \<turnstile> Disjoint (Eats x y) z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Disjoint x z, Neg (y IN z)} \<turnstile> Disjoint (Eats x y) z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {Disjoint x z, Neg (y IN z)} \<turnstile> Disjoint (Eats x y) z
[PROOF STEP]
obtain i::name where"atom i \<sharp> (x,y,z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. atom i \<sharp> (x, y, z) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom i \<sharp> (x, y, z)

goal (1 subgoal):
 1. {Disjoint x z, Neg (y IN z)} \<turnstile> Disjoint (Eats x y) z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom i \<sharp> (x, y, z)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atom i \<sharp> (x, y, z)

goal (1 subgoal):
 1. {Disjoint x z, Neg (y IN z)} \<turnstile> Disjoint (Eats x y) z
[PROOF STEP]
by (auto intro: Disjoint_I [of i]  Disjoint_E [THEN rotate3]
                    Mem_cong [OF Assume Refl, THEN Iff_MP_same])
[PROOF STATE]
proof (state)
this:
{Disjoint x z, Neg (y IN z)} \<turnstile> Disjoint (Eats x y) z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trans_strict_pareto: "X \<succ>Pareto Y \<Longrightarrow> Y \<succ>Pareto Z \<Longrightarrow> X \<succ>Pareto Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
assume a1: "X \<succ>Pareto Y"
[PROOF STATE]
proof (state)
this:
X \<succ>Pareto Y

goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
assume "Y \<succ>Pareto Z"
[PROOF STATE]
proof (state)
this:
Y \<succ>Pareto Z

goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Y \<succ>Pareto Z
[PROOF STEP]
have f3: "\<forall>i \<in> agents. U[i] (Z i) \<le> U[i] (X i)"
[PROOF STATE]
proof (prove)
using this:
Y \<succ>Pareto Z

goal (1 subgoal):
 1. \<forall>i\<in>agents. U[i] (Z i) \<le> U[i] (X i)
[PROOF STEP]
by (meson a1 order_trans pareto_dominating_def)
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>agents. U[i] (Z i) \<le> U[i] (X i)

goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>agents. U[i] (Z i) \<le> U[i] (X i)

goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
have "\<exists>i \<in> agents. \<not> U[i] (X i) \<le> U[i] (Y i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i\<in>agents. \<not> U[i] (X i) \<le> U[i] (Y i)
[PROOF STEP]
using a1 pareto_dominating_def
[PROOF STATE]
proof (prove)
using this:
X \<succ>Pareto Y
?X \<succ>Pareto ?Y = ((\<forall>i\<in>agents. U[i] (?Y i) \<le> U[i] (?X i)) \<and> (\<exists>i\<in>agents. U[i] (?Y i) < U[i] (?X i)))

goal (1 subgoal):
 1. \<exists>i\<in>agents. \<not> U[i] (X i) \<le> U[i] (Y i)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>agents. \<not> U[i] (X i) \<le> U[i] (Y i)

goal (1 subgoal):
 1. \<lbrakk>X \<succ>Pareto Y; Y \<succ>Pareto Z\<rbrakk> \<Longrightarrow> X \<succ>Pareto Z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>agents. U[i] (Z i) \<le> U[i] (X i)
\<exists>i\<in>agents. \<not> U[i] (X i) \<le> U[i] (Y i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>agents. U[i] (Z i) \<le> U[i] (X i)
\<exists>i\<in>agents. \<not> U[i] (X i) \<le> U[i] (Y i)

goal (1 subgoal):
 1. X \<succ>Pareto Z
[PROOF STEP]
by (metis \<open>Y \<succ>Pareto Z\<close> less_eq_real_def pareto_dominating_def)
[PROOF STATE]
proof (state)
this:
X \<succ>Pareto Z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "set (flows_stateL (generate_valid_stateful_policy_IFSACS ChairNetwork ChairSecurityRequirements)) =
       set (flows_stateL (generate_valid_stateful_policy_IFSACS_2 ChairNetwork ChairSecurityRequirements))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (flows_stateL (TopoS_Stateful_Policy_impl.generate_valid_stateful_policy_IFSACS ChairNetwork ChairSecurityRequirements)) = set (flows_stateL (TopoS_Stateful_Policy_impl.generate_valid_stateful_policy_IFSACS_2 ChairNetwork ChairSecurityRequirements))
[PROOF STEP]
by eval


[STATEMENT]
lemma ccard_sum:
  fixes n::nat
  assumes "n'\<ge>n''"
    and "n''\<ge>n"
  shows "ccard n n' P = ccard n n'' P + ccard n'' n' P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
have "ccard n n' P = card {i. i>n \<and> i \<le> n' \<and> P i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
have "{i. i>n \<and> i \<le> n' \<and> P i} =
    {i. i>n \<and> i \<le> n'' \<and> P i} \<union> {i. i>n'' \<and> i \<le> n' \<and> P i}" (is "?LHS = ?RHS")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n' \<and> P i} = {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {i. n < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}
 2. {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
show "?LHS \<subseteq> ?RHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. n < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
show "?RHS \<subseteq> ?LHS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
assume "x\<in>?RHS"
[PROOF STATE]
proof (state)
this:
x \<in> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. \<And>x. x \<in> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
hence "x>n \<and> x \<le> n'' \<and> P x \<or> x>n'' \<and> x \<le> n' \<and> P x"
[PROOF STATE]
proof (prove)
using this:
x \<in> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. n < x \<and> x \<le> n'' \<and> P x \<or> n'' < x \<and> x \<le> n' \<and> P x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n < x \<and> x \<le> n'' \<and> P x \<or> n'' < x \<and> x \<le> n' \<and> P x

goal (1 subgoal):
 1. \<And>x. x \<in> {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
thus "x\<in>?LHS"
[PROOF STATE]
proof (prove)
using this:
n < x \<and> x \<le> n'' \<and> P x \<or> n'' < x \<and> x \<le> n' \<and> P x

goal (1 subgoal):
 1. x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n < x \<and> x \<le> n'' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
 2. n'' < x \<and> x \<le> n' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
assume "n < x \<and> x \<le> n'' \<and> P x"
[PROOF STATE]
proof (state)
this:
n < x \<and> x \<le> n'' \<and> P x

goal (2 subgoals):
 1. n < x \<and> x \<le> n'' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
 2. n'' < x \<and> x \<le> n' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
n'' \<le> n'
n \<le> n''
n < x \<and> x \<le> n'' \<and> P x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n'' \<le> n'
n \<le> n''
n < x \<and> x \<le> n'' \<and> P x

goal (1 subgoal):
 1. x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {i. n < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. n'' < x \<and> x \<le> n' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n'' < x \<and> x \<le> n' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
assume "n'' < x \<and> x \<le> n' \<and> P x"
[PROOF STATE]
proof (state)
this:
n'' < x \<and> x \<le> n' \<and> P x

goal (1 subgoal):
 1. n'' < x \<and> x \<le> n' \<and> P x \<Longrightarrow> x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
n'' \<le> n'
n \<le> n''
n'' < x \<and> x \<le> n' \<and> P x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n'' \<le> n'
n \<le> n''
n'' < x \<and> x \<le> n' \<and> P x

goal (1 subgoal):
 1. x \<in> {i. n < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {i. n < i \<and> i \<le> n' \<and> P i}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> {i. n < i \<and> i \<le> n' \<and> P i}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i} \<subseteq> {i. n < i \<and> i \<le> n' \<and> P i}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i. n < i \<and> i \<le> n' \<and> P i} = {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
hence "card ?LHS = card ?RHS"
[PROOF STATE]
proof (prove)
using this:
{i. n < i \<and> i \<le> n' \<and> P i} = {i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n' \<and> P i}
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})
[PROOF STEP]
have "ccard n n' P = card ?RHS"
[PROOF STATE]
proof (prove)
using this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n' \<and> P i}
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
have "card ?RHS = card {i. i>n \<and> i \<le> n'' \<and> P i} + card {i. i>n'' \<and> i \<le> n' \<and> P i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}) = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
proof (rule card_Un_disjoint)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite {i. n < i \<and> i \<le> n'' \<and> P i}
 2. finite {i. n'' < i \<and> i \<le> n' \<and> P i}
 3. {i. n < i \<and> i \<le> n'' \<and> P i} \<inter> {i. n'' < i \<and> i \<le> n' \<and> P i} = {}
[PROOF STEP]
show "finite {i. n < i \<and> i \<le> n'' \<and> P i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. n < i \<and> i \<le> n'' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {i. n < i \<and> i \<le> n'' \<and> P i}

goal (2 subgoals):
 1. finite {i. n'' < i \<and> i \<le> n' \<and> P i}
 2. {i. n < i \<and> i \<le> n'' \<and> P i} \<inter> {i. n'' < i \<and> i \<le> n' \<and> P i} = {}
[PROOF STEP]
show "finite {i. n'' < i \<and> i \<le> n' \<and> P i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n'' \<and> P i} \<inter> {i. n'' < i \<and> i \<le> n' \<and> P i} = {}
[PROOF STEP]
show "{i. n < i \<and> i \<le> n'' \<and> P i} \<inter> {i. n'' < i \<and> i \<le> n' \<and> P i} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. n < i \<and> i \<le> n'' \<and> P i} \<inter> {i. n'' < i \<and> i \<le> n' \<and> P i} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. n < i \<and> i \<le> n'' \<and> P i} \<inter> {i. n'' < i \<and> i \<le> n' \<and> P i} = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}) = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}) = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
have "ccard n n'' P = card {i. i>n \<and> i \<le> n'' \<and> P i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n'' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n'' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n'' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
have "ccard n'' n' P= card {i. i>n'' \<and> i \<le> n' \<and> P i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. n'' < i \<and> i \<le> n' \<and> P i} = card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n'' < i \<and> i \<le> n' \<and> P i} = card {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})
card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}) = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
card {i. n < i \<and> i \<le> n'' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i}
card {i. n'' < i \<and> i \<le> n' \<and> P i} = card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i})
card ({i. n < i \<and> i \<le> n'' \<and> P i} \<union> {i. n'' < i \<and> i \<le> n' \<and> P i}) = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
card {i. n < i \<and> i \<le> n'' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i}
card {i. n'' < i \<and> i \<le> n' \<and> P i} = card {i. n'' < i \<and> i \<le> n' \<and> P i}

goal (1 subgoal):
 1. card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. n < i \<and> i \<le> n' \<and> P i} = card {i. n < i \<and> i \<le> n'' \<and> P i} + card {i. n'' < i \<and> i \<le> n' \<and> P i}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_preserves_iso [simp]:
    assumes "iso f" and "iso g"
    shows "iso (f \<otimes> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso (f \<otimes> g)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
local.iso f
local.iso g

goal (1 subgoal):
 1. local.iso (f \<otimes> g)
[PROOF STEP]
by simp