[STATEMENT]
lemma n_max:"\<lbrakk>A \<subseteq> {i. i \<le> (n::nat)}; A \<noteq> {}\<rbrakk> \<Longrightarrow>
                    (n_max A) \<in> A \<and> (\<forall>x\<in>A. x \<le> (n_max A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> {i. i \<le> n}; A \<noteq> {}\<rbrakk> \<Longrightarrow> n_max A \<in> A \<and> (\<forall>x\<in>A. x \<le> n_max A)
[PROOF STEP]
apply (simp add:n_max_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> {i. i \<le> n}; A \<noteq> {}\<rbrakk> \<Longrightarrow> (THE m. m \<in> A \<and> (\<forall>x\<in>A. x \<le> m)) \<in> A \<and> (\<forall>x\<in>A. x \<le> (THE m. m \<in> A \<and> (\<forall>x\<in>A. x \<le> m)))
[PROOF STEP]
apply (frule ubs_ex_n_max[of "A" "n"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> {i. i \<le> n}; A \<noteq> {}; \<exists>!m. m \<in> A \<and> (\<forall>x\<in>A. x \<le> m)\<rbrakk> \<Longrightarrow> (THE m. m \<in> A \<and> (\<forall>x\<in>A. x \<le> m)) \<in> A \<and> (\<forall>x\<in>A. x \<le> (THE m. m \<in> A \<and> (\<forall>x\<in>A. x \<le> m)))
[PROOF STEP]
apply (rule theI')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> {i. i \<le> n}; A \<noteq> {}; \<exists>!m. m \<in> A \<and> (\<forall>x\<in>A. x \<le> m)\<rbrakk> \<Longrightarrow> \<exists>!x. x \<in> A \<and> (\<forall>xa\<in>A. xa \<le> x)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Order) ord_equiv_reflex:"ord_equiv D D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_equiv D D
[PROOF STEP]
apply (simp add:ord_equiv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. ord_isom D D f
[PROOF STEP]
apply (cut_tac id_ord_isom, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nonequiv_Ssegment:"\<lbrakk>Worder D; a \<in> carrier D\<rbrakk> \<Longrightarrow>
                                   \<not> ord_equiv D (SIod D (Ssegment D a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Worder D; a \<in> carrier D\<rbrakk> \<Longrightarrow> \<not> ord_equiv D (SIod D (Ssegment D a))
[PROOF STEP]
apply (frule Worder.Order[of "D"], frule Worder.Torder[of "D"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D\<rbrakk> \<Longrightarrow> \<not> ord_equiv D (SIod D (Ssegment D a))
[PROOF STEP]
apply (rule contrapos_pp, simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_equiv D (SIod D (Ssegment D a))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:ord_equiv_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; \<exists>f. ord_isom D (SIod D (Ssegment D a)) f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (erule exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cut_tac Ssegment_sub[of "D" "a"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule SIod_Order[of "D" "Ssegment D a"], assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac f = f in Order.ord_isom_func[of "D" "SIod D (Ssegment D a)"],
               assumption+,
 frule_tac f = f and a = a in Order.ord_isom_mem[of "D"
                                       "SIod D (Ssegment D a)"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> carrier (SIod D (Ssegment D a)); f a \<in> carrier (SIod D (Ssegment D a))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac f = f in to_subsetS [of "D" "Ssegment D a"], assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> carrier (SIod D (Ssegment D a)); f a \<in> carrier (SIod D (Ssegment D a)); \<forall>a. a \<in> carrier D \<longrightarrow> a \<preceq>\<^bsub>D\<^esub> f a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (drule_tac a = a in forall_spec, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> carrier (SIod D (Ssegment D a)); f a \<in> carrier (SIod D (Ssegment D a)); a \<preceq>\<^bsub>D\<^esub> f a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
(*
        thin_tac "\<forall>a. a \<in> carrier D \<longrightarrow> a \<preceq>\<^bsub>D\<^esub> f a") *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> carrier (SIod D (Ssegment D a)); f a \<in> carrier (SIod D (Ssegment D a)); a \<preceq>\<^bsub>D\<^esub> f a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:SIod_carrier)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> Ssegment D a; f a \<in> Ssegment D a; a \<preceq>\<^bsub>D\<^esub> f a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (frule_tac c = "f a" in subsetD[of "Ssegment D a" "carrier D"],
        assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> Ssegment D a; f a \<in> Ssegment D a; a \<preceq>\<^bsub>D\<^esub> f a; f a \<in> carrier D\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Ssegment_inc[THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>Worder D; a \<in> carrier D; Order D; Torder D; ord_isom D (SIod D (Ssegment D a)) f; Ssegment D a \<subseteq> carrier D; Order (SIod D (Ssegment D a)); f \<in> carrier D \<rightarrow> Ssegment D a; f a \<prec>\<^bsub>D\<^esub> a; a \<preceq>\<^bsub>D\<^esub> f a; f a \<in> carrier D\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add:Torder.not_le_less[THEN sym, of "D" "a" _])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma left_adjoint_is_ide:
    assumes "is_left_adjoint f"
    shows "ide f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide f
[PROOF STEP]
using assms adjoint_pair_antipar
[PROOF STATE]
proof (prove)
using this:
is_left_adjoint f
adjoint_pair ?f ?g \<Longrightarrow> ide ?f
adjoint_pair ?f ?g \<Longrightarrow> ide ?g
adjoint_pair ?f ?g \<Longrightarrow> src ?f = trg ?g
adjoint_pair ?f ?g \<Longrightarrow> src ?g = trg ?f

goal (1 subgoal):
 1. ide f
[PROOF STEP]
by auto


[STATEMENT]
lemma productF_path_unzip :
  assumes "productF A B FAIL AB"
  and     "path AB (w || tr) q"
  and     "length tr = length w"
shows "path AB (w || (map fst tr || map snd tr)) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path AB (w || map fst tr || map snd tr) q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path AB (w || map fst tr || map snd tr) q
[PROOF STEP]
have "map fst tr || map snd tr = tr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst tr || map snd tr = tr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map fst tr || map snd tr = tr

goal (1 subgoal):
 1. path AB (w || map fst tr || map snd tr) q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map fst tr || map snd tr = tr
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map fst tr || map snd tr = tr

goal (1 subgoal):
 1. path AB (w || map fst tr || map snd tr) q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
map fst tr || map snd tr = tr
productF A B FAIL AB
path AB (w || tr) q
length tr = length w

goal (1 subgoal):
 1. path AB (w || map fst tr || map snd tr) q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path AB (w || map fst tr || map snd tr) q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cxt_inv_assign:
  "\<lbrakk> cxt_to_stmt E c = x \<leftarrow> e \<rbrakk> \<Longrightarrow> c = x \<leftarrow> e \<and> E = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cxt_to_stmt E c = x \<leftarrow> e \<Longrightarrow> c = x \<leftarrow> e \<and> E = []
[PROOF STEP]
by (metis Stmt.simps(11) cxt_inv)


[STATEMENT]
lemma [simp]: "(distinct_names P) = (distinct_names_f P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_names P = distinct_names_f P
[PROOF STEP]
apply(rule)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct_names P \<Longrightarrow> distinct_names_f P
 2. distinct_names_f P \<Longrightarrow> distinct_names P
[PROOF STEP]
apply(erule distinct_names.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Pa cld_dcl_list. \<lbrakk>P = Pa; Pa = map (\<lambda>(cld_XXX, dcl_XXX). cld_XXX) cld_dcl_list; list_all (\<lambda>f. f) (map (\<lambda>(cld_XXX, dcl_XXX). class_name cld_XXX dcl_XXX) cld_dcl_list); distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) cld_dcl_list)\<rbrakk> \<Longrightarrow> distinct_names_f P
 2. distinct_names_f P \<Longrightarrow> distinct_names P
[PROOF STEP]
apply(clarsimp simp add: distinct_names_map)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_names_f P \<Longrightarrow> distinct_names P
[PROOF STEP]
apply(simp add: distinct_names_f_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map class_name_f P) \<Longrightarrow> distinct_names P
[PROOF STEP]
apply(rule_tac cld_dcl_list = "map (\<lambda>cld. (cld, class_name_f cld)) P" in dn_defI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. distinct (map class_name_f P) \<Longrightarrow> P = map (\<lambda>(cld_XXX, dcl_XXX). cld_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P)
 2. distinct (map class_name_f P) \<Longrightarrow> list_all (\<lambda>f. f) (map (\<lambda>(cld_XXX, dcl_XXX). class_name cld_XXX dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
 3. distinct (map class_name_f P) \<Longrightarrow> distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. distinct (map class_name_f P) \<Longrightarrow> P = map ((\<lambda>(cld_XXX, dcl_XXX). cld_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) P
 2. distinct (map class_name_f P) \<Longrightarrow> list_all (\<lambda>f. f) (map (\<lambda>(cld_XXX, dcl_XXX). class_name cld_XXX dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
 3. distinct (map class_name_f P) \<Longrightarrow> distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
[PROOF STEP]
apply(induct P)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. distinct (map class_name_f []) \<Longrightarrow> [] = map ((\<lambda>(cld_XXX, dcl_XXX). cld_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) []
 2. \<And>a P. \<lbrakk>distinct (map class_name_f P) \<Longrightarrow> P = map ((\<lambda>(cld_XXX, dcl_XXX). cld_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) P; distinct (map class_name_f (a # P))\<rbrakk> \<Longrightarrow> a # P = map ((\<lambda>(cld_XXX, dcl_XXX). cld_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) (a # P)
 3. distinct (map class_name_f P) \<Longrightarrow> list_all (\<lambda>f. f) (map (\<lambda>(cld_XXX, dcl_XXX). class_name cld_XXX dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
 4. distinct (map class_name_f P) \<Longrightarrow> distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a P. \<lbrakk>distinct (map class_name_f P) \<Longrightarrow> P = map ((\<lambda>(cld_XXX, dcl_XXX). cld_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) P; distinct (map class_name_f (a # P))\<rbrakk> \<Longrightarrow> a # P = map ((\<lambda>(cld_XXX, dcl_XXX). cld_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) (a # P)
 2. distinct (map class_name_f P) \<Longrightarrow> list_all (\<lambda>f. f) (map (\<lambda>(cld_XXX, dcl_XXX). class_name cld_XXX dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
 3. distinct (map class_name_f P) \<Longrightarrow> distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct (map class_name_f P) \<Longrightarrow> list_all (\<lambda>f. f) (map (\<lambda>(cld_XXX, dcl_XXX). class_name cld_XXX dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
 2. distinct (map class_name_f P) \<Longrightarrow> distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map class_name_f P) \<Longrightarrow> distinct (map (\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) (map (\<lambda>cld. (cld, class_name_f cld)) P))
[PROOF STEP]
apply(clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map class_name_f P) \<Longrightarrow> distinct (map ((\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) P)
[PROOF STEP]
apply(induct P)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. distinct (map class_name_f []) \<Longrightarrow> distinct (map ((\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) [])
 2. \<And>a P. \<lbrakk>distinct (map class_name_f P) \<Longrightarrow> distinct (map ((\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) P); distinct (map class_name_f (a # P))\<rbrakk> \<Longrightarrow> distinct (map ((\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) (a # P))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a P. \<lbrakk>distinct (map class_name_f P) \<Longrightarrow> distinct (map ((\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) P); distinct (map class_name_f (a # P))\<rbrakk> \<Longrightarrow> distinct (map ((\<lambda>(cld_XXX, dcl_XXX). dcl_XXX) \<circ> (\<lambda>cld. (cld, class_name_f cld))) (a # P))
[PROOF STEP]
apply(force)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma crel_vs_lookup:
  "crel_vs
    (\<lambda> v v'. case v' of None \<Rightarrow> True | Some v' \<Rightarrow> v = v' \<and> v = dp param) (dp param) (lookup param)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crel_vs (\<lambda>v v'. case v' of None \<Rightarrow> True | Some v' \<Rightarrow> v = v' \<and> v = dp param) (dp param) (lookup param)
[PROOF STEP]
by (rule
      crel_vsI relcomppI state_dp_consistency.crel_vs_lookup
      rel_state_lookup[unfolded rel_fun_def, rule_format] HOL.refl
     )+


[STATEMENT]
lemma downset_upset_dual: "(`) \<partial> \<circ> \<down> = \<up> \<circ> \<partial>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) \<partial> \<circ> \<down> = \<up> \<circ> \<partial>
[PROOF STEP]
using downset_def upset_def upset_set_to_downset_set
[PROOF STATE]
proof (prove)
using this:
\<down> = \<Down> \<circ> \<eta>
\<up> = \<Up> \<circ> \<eta>
\<Up> = (`) \<partial> \<circ> \<Down> \<circ> (`) \<partial>

goal (1 subgoal):
 1. (`) \<partial> \<circ> \<down> = \<up> \<circ> \<partial>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma csol:
  assumes "t \<in> existence_ivl t0 x0"
  shows "t \<in> T" "{t0--t} \<subseteq> T" "csol t0 x0 t t0 = x0" "(csol t0 x0 t solves_ode f) {t0--t} X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<in> T &&& {t0--t} \<subseteq> T) &&& csol t0 x0 t t0 = x0 &&& (csol t0 x0 t solves_ode f) {t0--t} X
[PROOF STEP]
using csol_mem_csols[OF assms]
[PROOF STATE]
proof (prove)
using this:
(csol t0 x0 t, t) \<in> csols t0 x0

goal (1 subgoal):
 1. (t \<in> T &&& {t0--t} \<subseteq> T) &&& csol t0 x0 t t0 = x0 &&& (csol t0 x0 t solves_ode f) {t0--t} X
[PROOF STEP]
by (auto simp: csols_def)


[STATEMENT]
lemma distinct_upto [intro, simp]:
  "distinct [MkI\<cdot>m..MkI\<cdot>n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
proof (cases "n - m")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>na. n - m = int na \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
 2. \<And>na. n - m = - int (Suc na) \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
case (nonneg i)
[PROOF STATE]
proof (state)
this:
n - m = int i

goal (2 subgoals):
 1. \<And>na. n - m = int na \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
 2. \<And>na. n - m = - int (Suc na) \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n - m = int i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n - m = int i

goal (1 subgoal):
 1. distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
proof (induct i arbitrary: m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. n - m = int 0 \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
 2. \<And>i m. \<lbrakk>\<And>m. n - m = int i \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]; n - m = int (Suc i)\<rbrakk> \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
n - ?m = int i \<Longrightarrow> distinct [MkI\<cdot>?m..MkI\<cdot>n]
n - m = int (Suc i)

goal (2 subgoals):
 1. \<And>m. n - m = int 0 \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
 2. \<And>i m. \<lbrakk>\<And>m. n - m = int i \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]; n - m = int (Suc i)\<rbrakk> \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n - ?m = int i \<Longrightarrow> distinct [MkI\<cdot>?m..MkI\<cdot>n]
n - m = int (Suc i)
[PROOF STEP]
have "n - (m + 1) = int i" and "m \<le> n"
[PROOF STATE]
proof (prove)
using this:
n - ?m = int i \<Longrightarrow> distinct [MkI\<cdot>?m..MkI\<cdot>n]
n - m = int (Suc i)

goal (1 subgoal):
 1. n - (m + 1) = int i &&& m \<le> n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
n - (m + 1) = int i
m \<le> n

goal (2 subgoals):
 1. \<And>m. n - m = int 0 \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
 2. \<And>i m. \<lbrakk>\<And>m. n - m = int i \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]; n - m = int (Suc i)\<rbrakk> \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
with Suc
[PROOF STATE]
proof (chain)
picking this:
n - ?m = int i \<Longrightarrow> distinct [MkI\<cdot>?m..MkI\<cdot>n]
n - m = int (Suc i)
n - (m + 1) = int i
m \<le> n
[PROOF STEP]
have "distinct [MkI\<cdot>(m+1)..MkI\<cdot>n]"
[PROOF STATE]
proof (prove)
using this:
n - ?m = int i \<Longrightarrow> distinct [MkI\<cdot>?m..MkI\<cdot>n]
n - m = int (Suc i)
n - (m + 1) = int i
m \<le> n

goal (1 subgoal):
 1. distinct [MkI\<cdot>(m + 1)..MkI\<cdot>n]
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
distinct [MkI\<cdot>(m + 1)..MkI\<cdot>n]

goal (2 subgoals):
 1. \<And>m. n - m = int 0 \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
 2. \<And>i m. \<lbrakk>\<And>m. n - m = int i \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]; n - m = int (Suc i)\<rbrakk> \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
with \<open>m \<le> n\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<le> n
distinct [MkI\<cdot>(m + 1)..MkI\<cdot>n]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m \<le> n
distinct [MkI\<cdot>(m + 1)..MkI\<cdot>n]

goal (1 subgoal):
 1. distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
by (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
distinct [MkI\<cdot>m..MkI\<cdot>n]

goal (1 subgoal):
 1. \<And>m. n - m = int 0 \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
qed (simp add: one_Integer_def)
[PROOF STATE]
proof (state)
this:
distinct [MkI\<cdot>m..MkI\<cdot>n]

goal (1 subgoal):
 1. \<And>na. n - m = - int (Suc na) \<Longrightarrow> distinct [MkI\<cdot>m..MkI\<cdot>n]
[PROOF STEP]
qed simp


[STATEMENT]
theorem LT4: "\<turnstile> F \<longrightarrow> (F \<leadsto> G) \<longrightarrow> \<diamond>G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> F \<longrightarrow> (F \<leadsto> G) \<longrightarrow> \<diamond>G
[PROOF STEP]
unfolding leadsto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> F \<longrightarrow> \<box>(F \<longrightarrow> \<diamond>G) \<longrightarrow> \<diamond>G
[PROOF STEP]
using ax1[of "TEMP F \<longrightarrow> \<diamond>G"]
[PROOF STATE]
proof (prove)
using this:
\<turnstile> \<box>(F \<longrightarrow> \<diamond>G) \<longrightarrow> F \<longrightarrow> \<diamond>G

goal (1 subgoal):
 1. \<turnstile> F \<longrightarrow> \<box>(F \<longrightarrow> \<diamond>G) \<longrightarrow> \<diamond>G
[PROOF STEP]
by auto


[STATEMENT]
lemma symP_R2P[simp]: "symP (R2P r) \<longleftrightarrow> sym r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symP (R2P r) = sym r
[PROOF STEP]
unfolding symP_def sym_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y. R2P r x y \<longrightarrow> R2P r y x) = (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r)
[PROOF STEP]
by auto


[STATEMENT]
lemma ivl_integral_norm_bound_ivl_integral:
  fixes f :: "real \<Rightarrow> 'a::banach"
  assumes "f integrable_on (closed_segment a b)"
    and "g integrable_on (closed_segment a b)"
    and "\<And>x. x \<in> closed_segment a b \<Longrightarrow> norm (f x) \<le> g x"
  shows "norm (ivl_integral a b f) \<le> abs (ivl_integral a b g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (ivl_integral a b f) \<le> \<bar>ivl_integral a b g\<bar>
[PROOF STEP]
using integral_norm_bound_integral[OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> closed_segment a b \<Longrightarrow> x \<in> closed_segment a b) \<Longrightarrow> norm (integral (closed_segment a b) f) \<le> integral (closed_segment a b) g

goal (1 subgoal):
 1. norm (ivl_integral a b f) \<le> \<bar>ivl_integral a b g\<bar>
[PROOF STEP]
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)


[STATEMENT]
lemma UNIV_bar:
  "(UNIV :: ('a, 'b) bar set) =
  rangeC {\<lambda>_::unit. Bar1} \<union>
  rangeC {Bar2} \<union>
  rangeC (rangeC (rangeC {Bar3})) \<union>
  rangeC (rangeC (rangeC {Bar4}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = rangeC {\<lambda>_. Bar1} \<union> rangeC {Bar2} \<union> rangeC (rangeC (rangeC {Bar3})) \<union> rangeC (rangeC (rangeC {Bar4}))
[PROOF STEP]
apply(rule UNIV_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> rangeC {\<lambda>_. Bar1} \<union> rangeC {Bar2} \<union> rangeC (rangeC (rangeC {Bar3})) \<union> rangeC (rangeC (rangeC {Bar4}))
[PROOF STEP]
apply(case_tac x)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. x = Bar1 \<Longrightarrow> x \<in> rangeC {\<lambda>_. Bar1} \<union> rangeC {Bar2} \<union> rangeC (rangeC (rangeC {Bar3})) \<union> rangeC (rangeC (rangeC {Bar4}))
 2. \<And>x x2. x = Bar2 x2 \<Longrightarrow> x \<in> rangeC {\<lambda>_. Bar1} \<union> rangeC {Bar2} \<union> rangeC (rangeC (rangeC {Bar3})) \<union> rangeC (rangeC (rangeC {Bar4}))
 3. \<And>x x31 x32 x33. x = Bar3 x31 x32 x33 \<Longrightarrow> x \<in> rangeC {\<lambda>_. Bar1} \<union> rangeC {Bar2} \<union> rangeC (rangeC (rangeC {Bar3})) \<union> rangeC (rangeC (rangeC {Bar4}))
 4. \<And>x x41 x42 x43. x = Bar4 x41 x42 x43 \<Longrightarrow> x \<in> rangeC {\<lambda>_. Bar1} \<union> rangeC {Bar2} \<union> rangeC (rangeC (rangeC {Bar3})) \<union> rangeC (rangeC (rangeC {Bar4}))
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_minimal_basisD2:
  assumes "is_minimal_basis B" and "p \<in> B" and "q \<in> B" and "p \<noteq> q"
  shows "\<not> lt p adds\<^sub>t lt q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lt p adds\<^sub>t lt q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_minimal_basis B
p \<in> B
q \<in> B
p \<noteq> q

goal (1 subgoal):
 1. \<not> lt p adds\<^sub>t lt q
[PROOF STEP]
unfolding is_minimal_basis_def
[PROOF STATE]
proof (prove)
using this:
0 \<notin> B \<and> (\<forall>p q. p \<in> B \<longrightarrow> q \<in> B \<longrightarrow> p \<noteq> q \<longrightarrow> \<not> lt p adds\<^sub>t lt q)
p \<in> B
q \<in> B
p \<noteq> q

goal (1 subgoal):
 1. \<not> lt p adds\<^sub>t lt q
[PROOF STEP]
by auto


[STATEMENT]
lemma unfold_llist_eq_LCons [simp]:
  "unfold_llist IS_LNIL LHD LTL b = LCons x xs \<longleftrightarrow>
  \<not> IS_LNIL b \<and> x = LHD b \<and> xs = unfold_llist IS_LNIL LHD LTL (LTL b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (unfold_llist IS_LNIL LHD LTL b = LCons x xs) = (\<not> IS_LNIL b \<and> x = LHD b \<and> xs = unfold_llist IS_LNIL LHD LTL (LTL b))
[PROOF STEP]
by(subst unfold_llist.code) auto


[STATEMENT]
lemma pure_At[simp]: "pure(s \<bullet> t) \<longleftrightarrow> pure s \<and> pure t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pure (s \<bullet> t) = (pure s \<and> pure t)
[PROOF STEP]
by(fastforce elim: pure.cases)


[STATEMENT]
lemma chart_compose_lemma:
  fixes c1 c2
  defines [simp]: "U \<equiv> domain c1"
  defines [simp]: "V \<equiv> domain c2"
  assumes subsets: "U \<inter> V \<subseteq> carrier"
  assumes "\<And>c. c \<in> charts \<Longrightarrow> k-smooth_compat c1 c"
    "\<And>c. c \<in> charts \<Longrightarrow> k-smooth_compat c2 c"
  shows "k-smooth_on (c1 ` (U \<inter> V)) (c2 \<circ> inv_chart c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> V)) (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
proof (rule smooth_on_open_subsetsI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
fix w'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
assume "w' \<in> c1 ` (U \<inter> V)"
[PROOF STATE]
proof (state)
this:
w' \<in> apply_chart c1 ` (U \<inter> V)

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w' \<in> apply_chart c1 ` (U \<inter> V)
[PROOF STEP]
obtain w where w': "w' = c1 w" and "w \<in> U" "w \<in> V"
[PROOF STATE]
proof (prove)
using this:
w' \<in> apply_chart c1 ` (U \<inter> V)

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w' = apply_chart c1 w; w \<in> U; w \<in> V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w' = apply_chart c1 w
w \<in> U
w \<in> V

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w' = apply_chart c1 w
w \<in> U
w \<in> V
[PROOF STEP]
have "w \<in> carrier"
[PROOF STATE]
proof (prove)
using this:
w' = apply_chart c1 w
w \<in> U
w \<in> V

goal (1 subgoal):
 1. w \<in> carrier
[PROOF STEP]
using subsets
[PROOF STATE]
proof (prove)
using this:
w' = apply_chart c1 w
w \<in> U
w \<in> V
U \<inter> V \<subseteq> carrier

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

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> carrier
[PROOF STEP]
obtain c3 where c3: "w \<in> domain c3" "c3 \<in> charts"
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier

goal (1 subgoal):
 1. (\<And>c3. \<lbrakk>w \<in> domain c3; c3 \<in> charts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule carrierE)
[PROOF STATE]
proof (state)
this:
w \<in> domain c3
c3 \<in> charts

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> domain c3
c3 \<in> charts
[PROOF STEP]
have c13: "k-smooth_compat c1 c3" and c23: "k-smooth_compat c2 c3"
[PROOF STATE]
proof (prove)
using this:
w \<in> domain c3
c3 \<in> charts

goal (1 subgoal):
 1. k-smooth_compat c1 c3 &&& k-smooth_compat c2 c3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w \<in> domain c3
c3 \<in> charts
U \<equiv> domain c1
V \<equiv> domain c2
U \<inter> V \<subseteq> carrier
?c \<in> charts \<Longrightarrow> k-smooth_compat c1 ?c
?c \<in> charts \<Longrightarrow> k-smooth_compat c2 ?c

goal (1 subgoal):
 1. k-smooth_compat c1 c3 &&& k-smooth_compat c2 c3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k-smooth_compat c1 c3
k-smooth_compat c2 c3

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
define W where [simp]: "W = domain c3"
[PROOF STATE]
proof (state)
this:
W = domain c3

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
have diff1: "k-smooth_on (c1 ` (U \<inter> W)) (c3 \<circ> inv_chart c1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)
[PROOF STEP]
have 1: "open (c1 ` (U \<inter> W))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (apply_chart c1 ` (U \<inter> W))
[PROOF STEP]
by (rule open_chart_image) auto
[PROOF STATE]
proof (state)
this:
open (apply_chart c1 ` (U \<inter> W))

goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)
[PROOF STEP]
have 2: "w' \<in> c1 ` (U \<inter> W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w' \<in> apply_chart c1 ` (U \<inter> W)
[PROOF STEP]
using \<open>w \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> U

goal (1 subgoal):
 1. w' \<in> apply_chart c1 ` (U \<inter> W)
[PROOF STEP]
by (auto simp: c3 w')
[PROOF STATE]
proof (state)
this:
w' \<in> apply_chart c1 ` (U \<inter> W)

goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)
[PROOF STEP]
from c13
[PROOF STATE]
proof (chain)
picking this:
k-smooth_compat c1 c3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k-smooth_compat c1 c3

goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)
[PROOF STEP]
by (auto simp: smooth_compat_def)
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
define y where "y = (c3 \<circ> inv_chart c1) w'"
[PROOF STATE]
proof (state)
this:
y = (apply_chart c3 \<circ> inv_chart c1) w'

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
have diff2: "k-smooth_on (c3 ` (V \<inter> W)) (c2 \<circ> inv_chart c3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)
[PROOF STEP]
have 1: "open (c3 ` (V \<inter> W))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. open (apply_chart c3 ` (V \<inter> W))
[PROOF STEP]
by (rule open_chart_image) auto
[PROOF STATE]
proof (state)
this:
open (apply_chart c3 ` (V \<inter> W))

goal (1 subgoal):
 1. k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)
[PROOF STEP]
have 2: "y \<in> c3 ` (V \<inter> W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> apply_chart c3 ` (V \<inter> W)
[PROOF STEP]
using \<open>w \<in> U\<close> \<open>w \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> U
w \<in> V

goal (1 subgoal):
 1. y \<in> apply_chart c3 ` (V \<inter> W)
[PROOF STEP]
by (auto simp: y_def c3 w')
[PROOF STATE]
proof (state)
this:
y \<in> apply_chart c3 ` (V \<inter> W)

goal (1 subgoal):
 1. k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)
[PROOF STEP]
from c23
[PROOF STATE]
proof (chain)
picking this:
k-smooth_compat c2 c3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k-smooth_compat c2 c3

goal (1 subgoal):
 1. k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)
[PROOF STEP]
by (auto simp: smooth_compat_def)
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
have "k-smooth_on (c1 ` (U \<inter> V \<inter> W)) ((c2 \<circ> inv_chart c3) o (c3 \<circ> inv_chart c1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3 \<circ> (apply_chart c3 \<circ> inv_chart c1))
[PROOF STEP]
using diff2 diff1
[PROOF STATE]
proof (prove)
using this:
k-smooth_on (apply_chart c3 ` (V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3)
k-smooth_on (apply_chart c1 ` (U \<inter> W)) (apply_chart c3 \<circ> inv_chart c1)

goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3 \<circ> (apply_chart c3 \<circ> inv_chart c1))
[PROOF STEP]
by (rule smooth_on_compose2) auto
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3 \<circ> (apply_chart c3 \<circ> inv_chart c1))

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3 \<circ> (apply_chart c3 \<circ> inv_chart c1))
[PROOF STEP]
have "k-smooth_on (c1 ` (U \<inter> V \<inter> W)) (c2 \<circ> inv_chart c1)"
[PROOF STATE]
proof (prove)
using this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c3 \<circ> (apply_chart c3 \<circ> inv_chart c1))

goal (1 subgoal):
 1. k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
by (rule smooth_on_cong) auto
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c1)

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c1)

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
have "w' \<in> c1 ` (U \<inter> V \<inter> W)" "open (c1 ` (U \<inter> V \<inter> W))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w' \<in> apply_chart c1 ` (U \<inter> V \<inter> W) &&& open (apply_chart c1 ` (U \<inter> V \<inter> W))
[PROOF STEP]
using \<open>w \<in> U\<close> \<open>w \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> U
w \<in> V

goal (1 subgoal):
 1. w' \<in> apply_chart c1 ` (U \<inter> V \<inter> W) &&& open (apply_chart c1 ` (U \<inter> V \<inter> W))
[PROOF STEP]
by (auto simp: w' c3)
[PROOF STATE]
proof (state)
this:
w' \<in> apply_chart c1 ` (U \<inter> V \<inter> W)
open (apply_chart c1 ` (U \<inter> V \<inter> W))

goal (1 subgoal):
 1. \<And>x. x \<in> apply_chart c1 ` (U \<inter> V) \<Longrightarrow> \<exists>T. x \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c1)
w' \<in> apply_chart c1 ` (U \<inter> V \<inter> W)
open (apply_chart c1 ` (U \<inter> V \<inter> W))
[PROOF STEP]
show "\<exists>T. w' \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)"
[PROOF STATE]
proof (prove)
using this:
k-smooth_on (apply_chart c1 ` (U \<inter> V \<inter> W)) (apply_chart c2 \<circ> inv_chart c1)
w' \<in> apply_chart c1 ` (U \<inter> V \<inter> W)
open (apply_chart c1 ` (U \<inter> V \<inter> W))

goal (1 subgoal):
 1. \<exists>T. w' \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)
[PROOF STEP]
by (intro exI[where x="c1 ` (U \<inter> V \<inter> W)"]) simp
[PROOF STATE]
proof (state)
this:
\<exists>T. w' \<in> T \<and> open T \<and> k-smooth_on T (apply_chart c2 \<circ> inv_chart c1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inorder_mkNode[simp]:
  "inorder (mkNode c l a r) = inorder l @ a # inorder r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Tree2.inorder (mkNode c l a r) = Tree2.inorder l @ a # Tree2.inorder r
[PROOF STEP]
by (auto simp: mkNode_def)


[STATEMENT]
lemma member_filter:"\<And>P. List.member (filter P L) x \<Longrightarrow> List.member L x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. List.member (filter P L) x \<Longrightarrow> List.member L x
[PROOF STEP]
apply(induction L, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a L P. \<lbrakk>\<And>P. List.member (filter P L) x \<Longrightarrow> List.member L x; List.member (if P a then a # filter P L else filter P L) x\<rbrakk> \<Longrightarrow> List.member (a # L) x
[PROOF STEP]
by(metis (full_types) member_rec(1))


[STATEMENT]
lemma semantics_tm_id_map [simp]: \<open>map \<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> ts = ts\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map \<lparr>\<^bold>#, \<^bold>\<dagger>\<rparr> ts = ts
[PROOF STEP]
by (auto cong: map_cong)


[STATEMENT]
lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  shows "(P \<oplus> Q) \<oplus> R \<simeq>\<^sup>s P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
have "(P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule Strong_Late_Bisim_Subst_SC.sumAssoc)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> Q) \<oplus> R \<sim>\<^sup>s P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq>\<^sup>s P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule strongEqWeakCong)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<simeq>\<^sup>s P \<oplus> Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filterlim_at'_list:
  "(f \<longlongrightarrow> y) (at' (x::'a llist)) \<Longrightarrow> f \<midarrow>x\<rightarrow> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<longlongrightarrow> y) (at' x) \<Longrightarrow> f \<midarrow>x\<rightarrow> y
[PROOF STEP]
unfolding at'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<longlongrightarrow> y) (if open {x} then principal {x} else at x) \<Longrightarrow> f \<midarrow>x\<rightarrow> y
[PROOF STEP]
by (auto split: if_split_asm simp: open_singleton_iff_lfinite)


[STATEMENT]
lemma lconcat'_lfinite[simp]: "lfinite xs \<Longrightarrow> lconcat' xs = foldr lappend (list_of xs) LNil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite xs \<Longrightarrow> lconcat' xs = foldr lappend (list_of xs) LNil
[PROOF STEP]
by (simp add: lconcat'_def Lim_at'_lfinite)


[STATEMENT]
lemma igb_fr_graphI:
  assumes "igb_graph G"
  assumes "finite ((g_E G)\<^sup>* `` g_V0 G)"
  shows "igb_fr_graph G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb_fr_graph G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. igb_fr_graph G
[PROOF STEP]
interpret igb_graph G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb_graph G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. igb_fr_graph G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb_fr_graph G
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
finite reachable

goal (1 subgoal):
 1. igb_fr_graph G
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
igb_fr_graph G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ListReds2:
  "P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es',s'\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es',s'\<rangle>
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>es',s'\<rangle> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es',s'\<rangle>
[PROOF STEP]
proof(induct rule: rtrancl_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es,s\<rangle>
 2. \<And>a b aa ba. \<lbrakk>P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>a,b\<rangle>; P \<turnstile> \<langle>a,b\<rangle> [\<rightarrow>] \<langle>aa,ba\<rangle>; P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a,b\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # aa,ba\<rangle>
[PROOF STEP]
case refl
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es,s\<rangle>
 2. \<And>a b aa ba. \<lbrakk>P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>a,b\<rangle>; P \<turnstile> \<langle>a,b\<rangle> [\<rightarrow>] \<langle>aa,ba\<rangle>; P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a,b\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # aa,ba\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es,s\<rangle>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # es,s\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>a,b\<rangle>; P \<turnstile> \<langle>a,b\<rangle> [\<rightarrow>] \<langle>aa,ba\<rangle>; P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a,b\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # aa,ba\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>a,b\<rangle>; P \<turnstile> \<langle>a,b\<rangle> [\<rightarrow>] \<langle>aa,ba\<rangle>; P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a,b\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # aa,ba\<rangle>
[PROOF STEP]
case step
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>a___,b___\<rangle>
P \<turnstile> \<langle>a___,b___\<rangle> [\<rightarrow>] \<langle>a_,b_\<rangle>
P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a___,b___\<rangle>

goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>P \<turnstile> \<langle>es,s\<rangle> [\<rightarrow>]* \<langle>a,b\<rangle>; P \<turnstile> \<langle>a,b\<rangle> [\<rightarrow>] \<langle>aa,ba\<rangle>; P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a,b\<rangle>\<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # aa,ba\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a_,b_\<rangle>
[PROOF STEP]
by(rule rtrancl_into_rtrancl[OF step(3) ListRed2[OF step(2)]])
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>Val v # es,s\<rangle> [\<rightarrow>]* \<langle>Val v # a_,b_\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Reds_dom_lcl:
assumes wf: "wwf_J_prog P"
shows "P \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow>* \<langle>e',(h',l')\<rangle> \<Longrightarrow> dom l' \<subseteq> dom l \<union> fv e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow>* \<langle>e',(h', l')\<rangle> \<Longrightarrow> dom l' \<subseteq> dom l \<union> fv e
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow>* \<langle>e',(h', l')\<rangle> \<Longrightarrow> dom l' \<subseteq> dom l \<union> fv e
[PROOF STEP]
proof(induct rule: converse_rtrancl_induct_red)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>e h l. dom l \<subseteq> dom l \<union> fv e
 2. \<And>e\<^sub>0 h\<^sub>0 l\<^sub>0 e\<^sub>1 h\<^sub>1 l\<^sub>1 e' h' l'. \<lbrakk>P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0, l\<^sub>0)\<rangle> \<rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, l\<^sub>1)\<rangle>; dom l' \<subseteq> dom l\<^sub>1 \<union> fv e\<^sub>1\<rbrakk> \<Longrightarrow> dom l' \<subseteq> dom l\<^sub>0 \<union> fv e\<^sub>0
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>e h l. dom l \<subseteq> dom l \<union> fv e
 2. \<And>e\<^sub>0 h\<^sub>0 l\<^sub>0 e\<^sub>1 h\<^sub>1 l\<^sub>1 e' h' l'. \<lbrakk>P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0, l\<^sub>0)\<rangle> \<rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, l\<^sub>1)\<rangle>; dom l' \<subseteq> dom l\<^sub>1 \<union> fv e\<^sub>1\<rbrakk> \<Longrightarrow> dom l' \<subseteq> dom l\<^sub>0 \<union> fv e\<^sub>0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom l_ \<subseteq> dom l_ \<union> fv e_
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dom l_ \<subseteq> dom l_ \<union> fv e_

goal (1 subgoal):
 1. \<And>e\<^sub>0 h\<^sub>0 l\<^sub>0 e\<^sub>1 h\<^sub>1 l\<^sub>1 e' h' l'. \<lbrakk>P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0, l\<^sub>0)\<rangle> \<rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, l\<^sub>1)\<rangle>; dom l' \<subseteq> dom l\<^sub>1 \<union> fv e\<^sub>1\<rbrakk> \<Longrightarrow> dom l' \<subseteq> dom l\<^sub>0 \<union> fv e\<^sub>0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e\<^sub>0 h\<^sub>0 l\<^sub>0 e\<^sub>1 h\<^sub>1 l\<^sub>1 e' h' l'. \<lbrakk>P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0, l\<^sub>0)\<rangle> \<rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, l\<^sub>1)\<rangle>; dom l' \<subseteq> dom l\<^sub>1 \<union> fv e\<^sub>1\<rbrakk> \<Longrightarrow> dom l' \<subseteq> dom l\<^sub>0 \<union> fv e\<^sub>0
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
P \<turnstile> \<langle>e\<^sub>0_,(h\<^sub>0_, l\<^sub>0_)\<rangle> \<rightarrow> \<langle>e\<^sub>1_,(h\<^sub>1_, l\<^sub>1_)\<rangle>
dom l'_ \<subseteq> dom l\<^sub>1_ \<union> fv e\<^sub>1_

goal (1 subgoal):
 1. \<And>e\<^sub>0 h\<^sub>0 l\<^sub>0 e\<^sub>1 h\<^sub>1 l\<^sub>1 e' h' l'. \<lbrakk>P \<turnstile> \<langle>e\<^sub>0,(h\<^sub>0, l\<^sub>0)\<rangle> \<rightarrow> \<langle>e\<^sub>1,(h\<^sub>1, l\<^sub>1)\<rangle>; dom l' \<subseteq> dom l\<^sub>1 \<union> fv e\<^sub>1\<rbrakk> \<Longrightarrow> dom l' \<subseteq> dom l\<^sub>0 \<union> fv e\<^sub>0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> \<langle>e\<^sub>0_,(h\<^sub>0_, l\<^sub>0_)\<rangle> \<rightarrow> \<langle>e\<^sub>1_,(h\<^sub>1_, l\<^sub>1_)\<rangle>
dom l'_ \<subseteq> dom l\<^sub>1_ \<union> fv e\<^sub>1_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e\<^sub>0_,(h\<^sub>0_, l\<^sub>0_)\<rangle> \<rightarrow> \<langle>e\<^sub>1_,(h\<^sub>1_, l\<^sub>1_)\<rangle>
dom l'_ \<subseteq> dom l\<^sub>1_ \<union> fv e\<^sub>1_

goal (1 subgoal):
 1. dom l'_ \<subseteq> dom l\<^sub>0_ \<union> fv e\<^sub>0_
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> \<langle>e\<^sub>0_,(h\<^sub>0_, l\<^sub>0_)\<rangle> \<rightarrow> \<langle>e\<^sub>1_,(h\<^sub>1_, l\<^sub>1_)\<rangle>
dom l'_ \<subseteq> dom l\<^sub>1_ \<union> fv e\<^sub>1_
wwf_J_prog P

goal (1 subgoal):
 1. dom l'_ \<subseteq> dom l\<^sub>0_ \<union> fv e\<^sub>0_
[PROOF STEP]
by(blast dest: Red_fv Red_dom_lcl)
[PROOF STATE]
proof (state)
this:
dom l'_ \<subseteq> dom l\<^sub>0_ \<union> fv e\<^sub>0_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma len_lexext_rev_wf: "wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. len_lexext_rev gt ys xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. len_lexext_rev gt ys xs)
[PROOF STEP]
unfolding len_lexext_rev_iff_len_lexext
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfP (\<lambda>x y. gt y x) \<Longrightarrow> wfP (\<lambda>xs ys. len_lexext gt (rev ys) (rev xs))
[PROOF STEP]
by (rule wfP_app[of "\<lambda>xs ys. len_lexext gt ys xs" rev, simplified]) (rule len_lexext_wf)


[STATEMENT]
lemma PNT5_imp_PNT4:
  assumes "\<psi> \<sim>[at_top] (\<lambda>x. x)"
  shows   "\<theta> \<sim>[at_top] (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
define r where "r = (\<lambda>x. \<theta> x - \<psi> x)"
[PROOF STATE]
proof (state)
this:
r = (\<lambda>x. \<theta> x - \<psi> x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
have "(\<lambda>x. \<psi> x - \<theta> x) \<in> O(\<lambda>x. ln x * sqrt x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<psi> x - \<theta> x) \<in> O(\<lambda>x. ln x * sqrt x)
[PROOF STEP]
by (fact \<psi>_minus_\<theta>_bigo)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<psi> x - \<theta> x) \<in> O(\<lambda>x. ln x * sqrt x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<psi> x - \<theta> x) \<in> O(\<lambda>x. ln x * sqrt x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
have "(\<lambda>x. \<psi> x - \<theta> x) = (\<lambda>x. -r x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<psi> x - \<theta> x) = (\<lambda>x. - r x)
[PROOF STEP]
by (simp add: r_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<psi> x - \<theta> x) = (\<lambda>x. - r x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. - r x) \<in> O(\<lambda>x. ln x * sqrt x)
[PROOF STEP]
have "r \<in> O(\<lambda>x. ln x * sqrt x)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. - r x) \<in> O(\<lambda>x. ln x * sqrt x)

goal (1 subgoal):
 1. r \<in> O(\<lambda>x. ln x * sqrt x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<in> O(\<lambda>x. ln x * sqrt x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
r \<in> O(\<lambda>x. ln x * sqrt x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
have "(\<lambda>x::real. ln x * sqrt x) \<in> o(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. ln x * sqrt x) \<in> o(\<lambda>x. x)
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. ln x * sqrt x) \<in> o(\<lambda>x. x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
r \<in> o(\<lambda>x. x)
[PROOF STEP]
have r: "r \<in> o(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
using this:
r \<in> o(\<lambda>x. x)

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

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
have "(\<lambda>x. \<psi> x + r x) \<sim>[at_top] (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. \<psi> x + r x) \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
using assms r
[PROOF STATE]
proof (prove)
using this:
\<psi> \<sim>[at_top] (\<lambda>x. x)
r \<in> o(\<lambda>x. x)

goal (1 subgoal):
 1. (\<lambda>x. \<psi> x + r x) \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
by (subst asymp_equiv_add_right) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. \<psi> x + r x) \<sim>[at_top] (\<lambda>x. x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. \<psi> x + r x) \<sim>[at_top] (\<lambda>x. x)

goal (1 subgoal):
 1. \<theta> \<sim>[at_top] (\<lambda>x. x)
[PROOF STEP]
by (simp add: r_def)
[PROOF STATE]
proof (state)
this:
\<theta> \<sim>[at_top] (\<lambda>x. x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in module) sum_is_submodule:
  fixes N1 N2
  assumes h1: "submodule R N1 M" and h2: "submodule R N2 M"
  shows "submodule R (submodule_sum N1 N2) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LinearCombinations.submodule R (submodule_sum N1 N2) M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LinearCombinations.submodule R (submodule_sum N1 N2) M
[PROOF STEP]
from h1 h2
[PROOF STATE]
proof (chain)
picking this:
LinearCombinations.submodule R N1 M
LinearCombinations.submodule R N2 M
[PROOF STEP]
interpret l: mod_hom R "(direct_sum (md N1) (md N2))" M "(\<lambda> v. (fst v) \<oplus>\<^bsub>M\<^esub> (snd v))"
[PROOF STATE]
proof (prove)
using this:
LinearCombinations.submodule R N1 M
LinearCombinations.submodule R N2 M

goal (1 subgoal):
 1. mod_hom R (direct_sum (md N1) (md N2)) M (\<lambda>v. fst v \<oplus>\<^bsub>M\<^esub> snd v)
[PROOF STEP]
by (rule sum_map_hom)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. LinearCombinations.submodule R (submodule_sum N1 N2) M
[PROOF STEP]
have 1: "l.im =submodule_sum N1 N2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l.im = submodule_sum N1 N2
[PROOF STEP]
apply (unfold l.im_def submodule_sum_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. fst v \<oplus>\<^bsub>M\<^esub> snd v) ` carrier (direct_sum (md N1) (md N2)) = (\<lambda>(x, y). x \<oplus>\<^bsub>M\<^esub> y) ` {(x, y). x \<in> N1 \<and> y \<in> N2}
[PROOF STEP]
apply (unfold direct_sum_def, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> N1; b \<in> N2\<rbrakk> \<Longrightarrow> a \<oplus>\<^bsub>M\<^esub> b \<in> (\<lambda>x. fst x \<oplus>\<^bsub>M\<^esub> snd x) ` (N1 \<times> N2)
[PROOF STEP]
by (unfold image_def, auto)
[PROOF STATE]
proof (state)
this:
l.im = submodule_sum N1 N2

goal (1 subgoal):
 1. LinearCombinations.submodule R (submodule_sum N1 N2) M
[PROOF STEP]
have 2: "submodule R (l.im) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LinearCombinations.submodule R l.im M
[PROOF STEP]
by (rule l.im_is_submodule)
[PROOF STATE]
proof (state)
this:
LinearCombinations.submodule R l.im M

goal (1 subgoal):
 1. LinearCombinations.submodule R (submodule_sum N1 N2) M
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
l.im = submodule_sum N1 N2
LinearCombinations.submodule R l.im M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l.im = submodule_sum N1 N2
LinearCombinations.submodule R l.im M

goal (1 subgoal):
 1. LinearCombinations.submodule R (submodule_sum N1 N2) M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LinearCombinations.submodule R (submodule_sum N1 N2) M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_gt_trans[trans]: "\<lbrakk>p1 >p p2; p2 >p p3\<rbrakk> \<Longrightarrow> p1 >p p3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p1 >p p2; p2 >p p3\<rbrakk> \<Longrightarrow> p1 >p p3
[PROOF STEP]
unfolding poly_gt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<alpha>. pos_assign \<alpha> \<longrightarrow> eval_poly \<alpha> p1 \<succ> eval_poly \<alpha> p2; \<forall>\<alpha>. pos_assign \<alpha> \<longrightarrow> eval_poly \<alpha> p2 \<succ> eval_poly \<alpha> p3\<rbrakk> \<Longrightarrow> \<forall>\<alpha>. pos_assign \<alpha> \<longrightarrow> eval_poly \<alpha> p1 \<succ> eval_poly \<alpha> p3
[PROOF STEP]
using gt_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<succ> ?y; ?y \<succ> ?z\<rbrakk> \<Longrightarrow> ?x \<succ> ?z

goal (1 subgoal):
 1. \<lbrakk>\<forall>\<alpha>. pos_assign \<alpha> \<longrightarrow> eval_poly \<alpha> p1 \<succ> eval_poly \<alpha> p2; \<forall>\<alpha>. pos_assign \<alpha> \<longrightarrow> eval_poly \<alpha> p2 \<succ> eval_poly \<alpha> p3\<rbrakk> \<Longrightarrow> \<forall>\<alpha>. pos_assign \<alpha> \<longrightarrow> eval_poly \<alpha> p1 \<succ> eval_poly \<alpha> p3
[PROOF STEP]
by blast


[STATEMENT]
lemma e2stack_stack [simp]:
  "e2stack (encode_config (ss, rv)) = list_encode (map encode_frame ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e2stack (encode_config (ss, rv)) = Partial_Recursive.list_encode (map encode_frame ss)
[PROOF STEP]
unfolding e2stack_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pdec1 (encode_config (ss, rv)) = Partial_Recursive.list_encode (map encode_frame ss)
[PROOF STEP]
using encode_config
[PROOF STATE]
proof (prove)
using this:
encode_config (?ss, ?rv) = prod_encode (Partial_Recursive.list_encode (map encode_frame ?ss), encode_option ?rv)

goal (1 subgoal):
 1. pdec1 (encode_config (ss, rv)) = Partial_Recursive.list_encode (map encode_frame ss)
[PROOF STEP]
by simp


[STATEMENT]
lemma (in cf_parallel_2) cf_parallel_2_the_cf_parallel_2_is_tm_functor':
  assumes "\<AA>' = \<up>\<up>\<^sub>C \<aa> \<bb> \<gg> \<ff>" and "\<CC>' = \<CC>"
  shows "\<up>\<up>\<rightarrow>\<up>\<up>\<^sub>C\<^sub>F \<CC> \<aa> \<bb> \<gg> \<ff> \<aa>' \<bb>' \<gg>' \<ff>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>m\<^bsub>\<alpha>\<^esub> \<CC>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>\<up>\<rightarrow>\<up>\<up>\<^sub>C\<^sub>F \<CC> \<aa> \<bb> \<gg> \<ff> \<aa>' \<bb>' \<gg>' \<ff>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>m\<^bsub>\<alpha>\<^esub> \<CC>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>\<up>\<rightarrow>\<up>\<up>\<^sub>C\<^sub>F \<CC> \<aa> \<bb> \<gg> \<ff> \<aa>' \<bb>' \<gg>' \<ff>' : \<up>\<up>\<^sub>C \<aa> \<bb> \<gg> \<ff> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>m\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule cf_parallel_2_the_cf_parallel_2_is_tm_functor)


[STATEMENT]
lemma read_read_nonsync:
" \<lbrakk>\<And>y. c y \<notin> C; \<And>y. d y \<in> C\<rbrakk> \<Longrightarrow>
    ((c `?` x \<rightarrow> (P x)) \<lbrakk>C\<rbrakk> (d `?` x \<rightarrow>(Q x))) = (c `?` x \<rightarrow> ((P x) \<lbrakk>C\<rbrakk> (d `?` x \<rightarrow>(Q x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. c y \<notin> C; \<And>y. d y \<in> C\<rbrakk> \<Longrightarrow> (read c UNIV P \<lbrakk>C\<rbrakk> read d UNIV Q) = (c`?`x \<rightarrow> (P x \<lbrakk>C\<rbrakk> read d UNIV Q))
[PROOF STEP]
apply (auto simp add: read_def o_def, goal_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. c y \<notin> C; \<And>y. d y \<in> C\<rbrakk> \<Longrightarrow> (Mprefix (range c) (\<lambda>x. P (inv c x)) \<lbrakk>C\<rbrakk> Mprefix (range d) (\<lambda>x. Q (inv d x))) = Mprefix (range c) (\<lambda>x. P (inv c x) \<lbrakk>C\<rbrakk> Mprefix (range d) (\<lambda>x. Q (inv d x)))
[PROOF STEP]
apply(insert mprefix_Par_Int_distr[of "range c" C "range d" "\<lambda>x. (Q (inv d x))" "\<lambda>x. (P (inv c x))"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. c y \<notin> C; \<And>y. d y \<in> C; \<lbrakk>range c \<inter> C = {}; range d \<subseteq> C\<rbrakk> \<Longrightarrow> (Mprefix (range d) (\<lambda>x. Q (inv d x)) \<lbrakk>C\<rbrakk> Mprefix (range c) (\<lambda>x. P (inv c x))) = Mprefix (range c) (\<lambda>x. Mprefix (range d) (\<lambda>x. Q (inv d x)) \<lbrakk>C\<rbrakk> P (inv c x))\<rbrakk> \<Longrightarrow> (Mprefix (range c) (\<lambda>x. P (inv c x)) \<lbrakk>C\<rbrakk> Mprefix (range d) (\<lambda>x. Q (inv d x))) = Mprefix (range c) (\<lambda>x. P (inv c x) \<lbrakk>C\<rbrakk> Mprefix (range d) (\<lambda>x. Q (inv d x)))
[PROOF STEP]
apply(subst (1 2) sync_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. c y \<notin> C; \<And>y. d y \<in> C; \<lbrakk>range c \<inter> C = {}; range d \<subseteq> C\<rbrakk> \<Longrightarrow> (Mprefix (range d) (\<lambda>x. Q (inv d x)) \<lbrakk>C\<rbrakk> Mprefix (range c) (\<lambda>x. P (inv c x))) = Mprefix (range c) (\<lambda>x. Mprefix (range d) (\<lambda>x. Q (inv d x)) \<lbrakk>C\<rbrakk> P (inv c x))\<rbrakk> \<Longrightarrow> (Mprefix (range d) (\<lambda>x. Q (inv d x)) \<lbrakk>C\<rbrakk> Mprefix (range c) (\<lambda>x. P (inv c x))) = Mprefix (range c) (\<lambda>x. Mprefix (range d) (\<lambda>x. Q (inv d x)) \<lbrakk>C\<rbrakk> P (inv c x))
[PROOF STEP]
by auto


[STATEMENT]
lemma fds_ln_const [simp]: "fds_ln l (fds_const c) = fds_const l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fds_ln l (fds_const c) = fds_const l
[PROOF STEP]
by (rule fds_eqI) (simp add: fds_ln_def fds_integral_def divide_fds_def)


[STATEMENT]
lemma completely_multiplicative_function_only_pows:
  assumes "completely_multiplicative_function (fds_nth f)"
  shows   "completely_multiplicative_function (fds_nth (fds_primepow_subseries p f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth (fds_primepow_subseries p f))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth (fds_primepow_subseries p f))
[PROOF STEP]
interpret completely_multiplicative_function "fds_nth f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth f)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth (fds_primepow_subseries p f))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. completely_multiplicative_function (fds_nth (fds_primepow_subseries p f))
[PROOF STEP]
by standard (auto simp: fds_nth_subseries prime_factors_product mult)
[PROOF STATE]
proof (state)
this:
completely_multiplicative_function (fds_nth (fds_primepow_subseries p f))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_match_fields_safe_eq2: assumes "all_prerequisites m" shows "OF_match_fields_safe m p \<longleftrightarrow> OF_match_fields m p = Some True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OF_match_fields_safe m p = (OF_match_fields m p = Some True)
[PROOF STEP]
unfolding OF_match_fields_safe_def[abs_def] fun_eq_iff comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (OF_match_fields m p) = (OF_match_fields m p = Some True)
[PROOF STEP]
unfolding of_safe_unsafe_match_eq[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (Some (OF_match_fields_unsafe m p)) = (Some (OF_match_fields_unsafe m p) = Some True)
[PROOF STEP]
unfolding option.sel
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OF_match_fields_unsafe m p = (Some (OF_match_fields_unsafe m p) = Some True)
[PROOF STEP]
by simp


[STATEMENT]
lemma is_openI:
  assumes "U \<subseteq>carrier Q\<^sub>p"
  assumes "\<And>c. c \<in> U \<Longrightarrow> \<exists>n. B\<^bsub>n\<^esub>[c]\<subseteq> U"
  shows "is_open U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_open U
[PROOF STEP]
by (simp add: assms(1) assms(2) is_open_def)


[STATEMENT]
lemma is_max_ball_ofI:
  assumes "U \<subseteq> carrier Q\<^sub>p"
  assumes "(B\<^bsub>m\<^esub>[c]) \<subseteq> U"
  assumes "c \<in> carrier Q\<^sub>p"
  assumes "\<forall>m'. m' < m \<longrightarrow> \<not> B\<^bsub>m'\<^esub>[c] \<subseteq> U"
  shows "is_max_ball_of U (B\<^bsub>m\<^esub>[c])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_max_ball_of U B\<^bsub>m\<^esub>[c]
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_max_ball_of U B\<^bsub>m\<^esub>[c] \<Longrightarrow> False
[PROOF STEP]
assume " \<not> is_max_ball_of U B\<^bsub>m\<^esub>[c]"
[PROOF STATE]
proof (state)
this:
\<not> is_max_ball_of U B\<^bsub>m\<^esub>[c]

goal (1 subgoal):
 1. \<not> is_max_ball_of U B\<^bsub>m\<^esub>[c] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> is_max_ball_of U B\<^bsub>m\<^esub>[c]
[PROOF STEP]
have "\<not> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B'\<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])"
[PROOF STATE]
proof (prove)
using this:
\<not> is_max_ball_of U B\<^bsub>m\<^esub>[c]

goal (1 subgoal):
 1. \<not> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])
[PROOF STEP]
using assms is_max_ball_of_def[of U "B\<^bsub>m\<^esub>[c]" ]
[PROOF STATE]
proof (prove)
using this:
\<not> is_max_ball_of U B\<^bsub>m\<^esub>[c]
U \<subseteq> carrier Q\<^sub>p
B\<^bsub>m\<^esub>[c] \<subseteq> U
c \<in> carrier Q\<^sub>p
\<forall>m'<m. \<not> B\<^bsub>m'\<^esub>[c] \<subseteq> U
is_max_ball_of U B\<^bsub>m\<^esub>[c] \<equiv> is_ball B\<^bsub>m\<^esub>[c] \<and> B\<^bsub>m\<^esub>[c] \<subseteq> U \<and> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])

goal (1 subgoal):
 1. \<not> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])
[PROOF STEP]
unfolding is_ball_def
[PROOF STATE]
proof (prove)
using this:
\<not> is_max_ball_of U B\<^bsub>m\<^esub>[c]
U \<subseteq> carrier Q\<^sub>p
B\<^bsub>m\<^esub>[c] \<subseteq> U
c \<in> carrier Q\<^sub>p
\<forall>m'<m. \<not> B\<^bsub>m'\<^esub>[c] \<subseteq> U
is_max_ball_of U B\<^bsub>m\<^esub>[c] \<equiv> (\<exists>ma. \<exists>ca\<in>carrier Q\<^sub>p. B\<^bsub>m\<^esub>[c] = B\<^bsub>ma\<^esub>[ca]) \<and> B\<^bsub>m\<^esub>[c] \<subseteq> U \<and> (\<forall>B'. (\<exists>m. \<exists>c\<in>carrier Q\<^sub>p. B' = B\<^bsub>m\<^esub>[c]) \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])

goal (1 subgoal):
 1. \<not> (\<forall>B'. (\<exists>m. \<exists>c\<in>carrier Q\<^sub>p. B' = B\<^bsub>m\<^esub>[c]) \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])

goal (1 subgoal):
 1. \<not> is_max_ball_of U B\<^bsub>m\<^esub>[c] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])
[PROOF STEP]
obtain B' where B'_def: "is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<and> \<not> B' \<subseteq> B\<^bsub>m\<^esub>[c]"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<longrightarrow> B' \<subseteq> B\<^bsub>m\<^esub>[c])

goal (1 subgoal):
 1. (\<And>B'. is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<and> \<not> B' \<subseteq> B\<^bsub>m\<^esub>[c] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_ball B' \<and> B' \<subseteq> U \<and> B\<^bsub>m\<^esub>[c] \<subseteq> B' \<and> \<not> B' \<subseteq> B\<^bsub>m\<^esub>[c]

goal (1 subgoal):
 1. \<not> is_max_ball_of U B\<^bsub>m\<^esub>[c] \<Longrightarrow> False
[PROOF STEP]
obtain n where n_def: "B' = B\<^bsub>n\<^esub>[c]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. B' = B\<^bsub>n\<^esub>[c] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson B'_def assms(3) c_ball_center_in is_ball_def radius_of_ball subset_iff)
[PROOF STATE]
proof (state)
this:
B' = B\<^bsub>n\<^esub>[c]

goal (1 subgoal):
 1. \<not> is_max_ball_of U B\<^bsub>m\<^esub>[c] \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
B' = B\<^bsub>n\<^esub>[c]
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
B' = B\<^bsub>n\<^esub>[c]

goal (1 subgoal):
 1. False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
B' = B\<^bsub>n\<^esub>[c]
U \<subseteq> carrier Q\<^sub>p
B\<^bsub>m\<^esub>[c] \<subseteq> U
c \<in> carrier Q\<^sub>p
\<forall>m'<m. \<not> B\<^bsub>m'\<^esub>[c] \<subseteq> U

goal (1 subgoal):
 1. False
[PROOF STEP]
by (smt B'_def Q\<^sub>p_def Zp_def ball_rad_0 padic_integers_axioms)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma space_space': "space' t > space t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space t < space' t
[PROOF STEP]
proof(induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2 x3 t. \<lbrakk>\<And>x3a. x3a \<in> set x3 \<Longrightarrow> space x3a < space' x3a; space t < space' t\<rbrakk> \<Longrightarrow> space (Node x1 x2 x3 t) < space' (Node x1 x2 x3 t)
 2. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
case (Node info deg treeList summary)
[PROOF STATE]
proof (state)
this:
?x3a \<in> set treeList \<Longrightarrow> space ?x3a < space' ?x3a
space summary < space' summary

goal (2 subgoals):
 1. \<And>x1 x2 x3 t. \<lbrakk>\<And>x3a. x3a \<in> set x3 \<Longrightarrow> space x3a < space' x3a; space t < space' t\<rbrakk> \<Longrightarrow> space (Node x1 x2 x3 t) < space' (Node x1 x2 x3 t)
 2. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
hence "\<forall> i < length treeList . (map space treeList)!i < ( map space' treeList)!i"
[PROOF STATE]
proof (prove)
using this:
?x3a \<in> set treeList \<Longrightarrow> space ?x3a < space' ?x3a
space summary < space' summary

goal (1 subgoal):
 1. \<forall>i<length treeList. map space treeList ! i < map space' treeList ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length treeList. map space treeList ! i < map space' treeList ! i

goal (2 subgoals):
 1. \<And>x1 x2 x3 t. \<lbrakk>\<And>x3a. x3a \<in> set x3 \<Longrightarrow> space x3a < space' x3a; space t < space' t\<rbrakk> \<Longrightarrow> space (Node x1 x2 x3 t) < space' (Node x1 x2 x3 t)
 2. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
hence 0:"foldr (+) (map space treeList) 0  + length treeList \<le> foldr (+) (map space' treeList) 0 "
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length treeList. map space treeList ! i < map space' treeList ! i

goal (1 subgoal):
 1. foldr (+) (map space treeList) 0 + length treeList \<le> foldr (+) (map space' treeList) 0
[PROOF STEP]
using foldr_mono[of "(map space treeList)"  "(map space' treeList)" 0 0]
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length treeList. map space treeList ! i < map space' treeList ! i
\<lbrakk>length (map space treeList) = length (map space' treeList); \<forall>i<length (map space treeList). map space treeList ! i < map space' treeList ! i; 0 \<le> 0\<rbrakk> \<Longrightarrow> foldr (+) (map space treeList) 0 + length (map space' treeList) \<le> foldr (+) (map space' treeList) 0

goal (1 subgoal):
 1. foldr (+) (map space treeList) 0 + length treeList \<le> foldr (+) (map space' treeList) 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldr (+) (map space treeList) 0 + length treeList \<le> foldr (+) (map space' treeList) 0

goal (2 subgoals):
 1. \<And>x1 x2 x3 t. \<lbrakk>\<And>x3a. x3a \<in> set x3 \<Longrightarrow> space x3a < space' x3a; space t < space' t\<rbrakk> \<Longrightarrow> space (Node x1 x2 x3 t) < space' (Node x1 x2 x3 t)
 2. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
have 1:"space summary < space' summary"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space summary < space' summary
[PROOF STEP]
using Node
[PROOF STATE]
proof (prove)
using this:
?x3a \<in> set treeList \<Longrightarrow> space ?x3a < space' ?x3a
space summary < space' summary

goal (1 subgoal):
 1. space summary < space' summary
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
space summary < space' summary

goal (2 subgoals):
 1. \<And>x1 x2 x3 t. \<lbrakk>\<And>x3a. x3a \<in> set x3 \<Longrightarrow> space x3a < space' x3a; space t < space' t\<rbrakk> \<Longrightarrow> space (Node x1 x2 x3 t) < space' (Node x1 x2 x3 t)
 2. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
hence "foldr (+) (map space treeList) 0 + length treeList + space summary \<le>
         foldr (+) (map space' treeList) 0 + space' summary"
[PROOF STATE]
proof (prove)
using this:
space summary < space' summary

goal (1 subgoal):
 1. foldr (+) (map space treeList) 0 + length treeList + space summary \<le> foldr (+) (map space' treeList) 0 + space' summary
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
space summary < space' summary
foldr (+) (map space treeList) 0 + length treeList \<le> foldr (+) (map space' treeList) 0

goal (1 subgoal):
 1. foldr (+) (map space treeList) 0 + length treeList + space summary \<le> foldr (+) (map space' treeList) 0 + space' summary
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldr (+) (map space treeList) 0 + length treeList + space summary \<le> foldr (+) (map space' treeList) 0 + space' summary

goal (2 subgoals):
 1. \<And>x1 x2 x3 t. \<lbrakk>\<And>x3a. x3a \<in> set x3 \<Longrightarrow> space x3a < space' x3a; space t < space' t\<rbrakk> \<Longrightarrow> space (Node x1 x2 x3 t) < space' (Node x1 x2 x3 t)
 2. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
foldr (+) (map space treeList) 0 + length treeList + space summary \<le> foldr (+) (map space' treeList) 0 + space' summary
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
foldr (+) (map space treeList) 0 + length treeList + space summary \<le> foldr (+) (map space' treeList) 0 + space' summary

goal (1 subgoal):
 1. space (Node info deg treeList summary) < space' (Node info deg treeList summary)
[PROOF STEP]
using space'.simps(2)[of info deg treeList summary]
       space.simps(2)[of info deg treeList summary]
[PROOF STATE]
proof (prove)
using this:
foldr (+) (map space treeList) 0 + length treeList + space summary \<le> foldr (+) (map space' treeList) 0 + space' summary
space' (Node info deg treeList summary) = 6 + space' summary + foldr (+) (map space' treeList) 0
space (Node info deg treeList summary) = 5 + space summary + length treeList + foldr (+) (map space treeList) 0

goal (1 subgoal):
 1. space (Node info deg treeList summary) < space' (Node info deg treeList summary)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
space (Node info deg treeList summary) < space' (Node info deg treeList summary)

goal (1 subgoal):
 1. \<And>x1 x2. space (Leaf x1 x2) < space' (Leaf x1 x2)
[PROOF STEP]
qed simp


[STATEMENT]
lemma conjugateI1: "residuated f \<Longrightarrow> f(x) \<sqinter> y = \<bottom> \<Longrightarrow> x \<sqinter> conjugate f y = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>residuated f; f x \<sqinter> y = \<bottom>\<rbrakk> \<Longrightarrow> x \<sqinter> conjugate f y = \<bottom>
[PROOF STEP]
by (metis conjugate_iff_def)


[STATEMENT]
lemma while_prot_terms_fun_mono:
  "mono (\<lambda>M'. M \<union> \<Union>(subterms ` M') \<union> \<Union>((set \<circ> fst \<circ> Ana) ` M'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>M'. M \<union> subterms\<^sub>s\<^sub>e\<^sub>t M' \<union> \<Union> ((set \<circ> fst \<circ> Ana) ` M'))
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<subseteq> y \<longrightarrow> M \<union> subterms\<^sub>s\<^sub>e\<^sub>t x \<union> \<Union> ((set \<circ> fst \<circ> Ana) ` x) \<subseteq> M \<union> subterms\<^sub>s\<^sub>e\<^sub>t y \<union> \<Union> ((set \<circ> fst \<circ> Ana) ` y)
[PROOF STEP]
by fast


[STATEMENT]
lemma upper_asymptotic_density_in_01:
  "ereal(upper_asymptotic_density A) = limsup (\<lambda>n. card(A \<inter> {..<n})/n)"
  "upper_asymptotic_density A \<le> 1"
  "upper_asymptotic_density A \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)) &&& upper_asymptotic_density A \<le> 1 &&& 0 \<le> upper_asymptotic_density A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
assume "n>0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
have "card(A \<inter> {..<n}) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (A \<inter> {..<n}) \<le> n
[PROOF STEP]
by (metis card_lessThan Int_lower2 card_mono finite_lessThan)
[PROOF STATE]
proof (state)
this:
card (A \<inter> {..<n}) \<le> n

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (A \<inter> {..<n}) \<le> n
[PROOF STEP]
have "card(A \<inter> {..<n}) / n \<le> ereal 1"
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<n}) \<le> n

goal (1 subgoal):
 1. ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1
[PROOF STEP]
using \<open>n>0\<close>
[PROOF STATE]
proof (prove)
using this:
card (A \<inter> {..<n}) \<le> n
0 < n

goal (1 subgoal):
 1. ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < ?n2 \<Longrightarrow> ereal (real (card (A \<inter> {..<?n2})) / real ?n2) \<le> ereal 1

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?n2 \<Longrightarrow> ereal (real (card (A \<inter> {..<?n2})) / real ?n2) \<le> ereal 1
[PROOF STEP]
have "eventually (\<lambda>n. card(A \<inter> {..<n}) / n \<le> ereal 1) sequentially"
[PROOF STATE]
proof (prove)
using this:
0 < ?n2 \<Longrightarrow> ereal (real (card (A \<inter> {..<?n2})) / real ?n2) \<le> ereal 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1
[PROOF STEP]
by (simp add: eventually_at_top_dense)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1
[PROOF STEP]
have a: "limsup (\<lambda>n. card(A \<inter> {..<n})/n) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. ereal (real (card (A \<inter> {..<n})) / real n) \<le> ereal 1

goal (1 subgoal):
 1. limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)) \<le> 1
[PROOF STEP]
by (simp add: Limsup_const Limsup_bounded)
[PROOF STATE]
proof (state)
this:
limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)) \<le> 1

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
have "card(A \<inter> {..<n}) / n \<ge> ereal 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ereal 0 \<le> ereal (real (card (A \<inter> {..<n})) / real n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ereal 0 \<le> ereal (real (card (A \<inter> {..<?n})) / real ?n)

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ereal 0 \<le> ereal (real (card (A \<inter> {..<?n})) / real ?n)
[PROOF STEP]
have "liminf (\<lambda>n. card(A \<inter> {..<n})/n) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
ereal 0 \<le> ereal (real (card (A \<inter> {..<?n})) / real ?n)

goal (1 subgoal):
 1. 0 \<le> liminf (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
[PROOF STEP]
by (simp add: le_Liminf_iff less_le_trans)
[PROOF STATE]
proof (state)
this:
0 \<le> liminf (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> liminf (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
[PROOF STEP]
have b: "limsup (\<lambda>n. card(A \<inter> {..<n})/n) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> liminf (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))

goal (1 subgoal):
 1. 0 \<le> limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
[PROOF STEP]
by (meson Liminf_le_Limsup order_trans sequentially_bot)
[PROOF STATE]
proof (state)
this:
0 \<le> limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
have "abs(limsup (\<lambda>n. card(A \<inter> {..<n})/n)) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))\<bar> \<noteq> \<infinity>
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)) \<le> 1
0 \<le> limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))

goal (1 subgoal):
 1. \<bar>limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))\<bar> \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))\<bar> \<noteq> \<infinity>

goal (3 subgoals):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
 2. upper_asymptotic_density A \<le> 1
 3. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))\<bar> \<noteq> \<infinity>
[PROOF STEP]
show "ereal(upper_asymptotic_density A) = limsup (\<lambda>n. card(A \<inter> {..<n})/n)"
[PROOF STATE]
proof (prove)
using this:
\<bar>limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))\<bar> \<noteq> \<infinity>

goal (1 subgoal):
 1. ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
[PROOF STEP]
unfolding upper_asymptotic_density_def
[PROOF STATE]
proof (prove)
using this:
\<bar>limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))\<bar> \<noteq> \<infinity>

goal (1 subgoal):
 1. ereal (real_of_ereal (limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)))) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ereal (upper_asymptotic_density A) = limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))

goal (2 subgoals):
 1. upper_asymptotic_density A \<le> 1
 2. 0 \<le> upper_asymptotic_density A
[PROOF STEP]
show "upper_asymptotic_density A \<le> 1" "upper_asymptotic_density A \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_asymptotic_density A \<le> 1 &&& 0 \<le> upper_asymptotic_density A
[PROOF STEP]
unfolding upper_asymptotic_density_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_ereal (limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))) \<le> 1 &&& 0 \<le> real_of_ereal (limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)))
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)) \<le> 1
0 \<le> limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))

goal (1 subgoal):
 1. real_of_ereal (limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x))) \<le> 1 &&& 0 \<le> real_of_ereal (limsup (\<lambda>x. ereal (real (card (A \<inter> {..<x})) / real x)))
[PROOF STEP]
by (auto simp add: real_of_ereal_le_1 real_of_ereal_pos)
[PROOF STATE]
proof (state)
this:
upper_asymptotic_density A \<le> 1
0 \<le> upper_asymptotic_density A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bin_fst_mismatch_all: "\<alpha> \<cdot> [c\<^sub>0] \<le>p f \<zero> \<cdot> f w \<cdot> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> \<cdot> [c\<^sub>0] \<le>p f \<zero> \<cdot> f w \<cdot> \<alpha>
[PROOF STEP]
using pref_prolong[OF bin_fst_mismatch bin_lcp_pref_all[of w]]
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<cdot> [c\<^sub>0] \<le>p f \<zero> \<cdot> f w \<cdot> \<alpha>

goal (1 subgoal):
 1. \<alpha> \<cdot> [c\<^sub>0] \<le>p f \<zero> \<cdot> f w \<cdot> \<alpha>
[PROOF STEP]
.


[STATEMENT]
theorem partialCorrectness:
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes
  "vars F0 \<subseteq> decisionVars" and

  "isInitialState state0 F0" and
  "(state0, state) \<in> transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"

  shows
  "satisfiable F0 = (\<not> getConflictFlag state)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfiable F0 = (\<not> getConflictFlag state)
[PROOF STEP]
(************************************************************************)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. satisfiable F0 = (\<not> getConflictFlag state)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars

goal (1 subgoal):
 1. satisfiable F0 = (\<not> getConflictFlag state)
[PROOF STEP]
using completenessForUNSAT[of "F0" "decisionVars" "state0" "state"]
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
\<lbrakk>vars F0 \<subseteq> decisionVars; \<not> satisfiable F0; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; isFinalState state F0 decisionVars\<rbrakk> \<Longrightarrow> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. satisfiable F0 = (\<not> getConflictFlag state)
[PROOF STEP]
using completenessForSAT[of "F0" "state0" "state" "decisionVars"]
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
\<lbrakk>vars F0 \<subseteq> decisionVars; \<not> satisfiable F0; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; isFinalState state F0 decisionVars\<rbrakk> \<Longrightarrow> getConflictFlag state = True \<and> getC state = []
\<lbrakk>satisfiable F0; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; isFinalState state F0 decisionVars\<rbrakk> \<Longrightarrow> getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))

goal (1 subgoal):
 1. satisfiable F0 = (\<not> getConflictFlag state)
[PROOF STEP]
by auto


[STATEMENT]
lemma gbm_nodes_list_it_unf:
    "it_to_it (gbm_nodes_list_it g)
    \<equiv> map_iterator_dom (it_to_it (m1.list_it g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_it (gbm_nodes_list_it g) \<equiv> map_iterator_dom (it_to_it (m1.list_it g))
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_it (gbm_nodes_list_it g) = map_iterator_dom (it_to_it (m1.list_it g))
[PROOF STEP]
apply (rule it_to_it_fold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (gbm_nodes_list_it g) (map_iterator_dom (it_to_it (m1.list_it g)))
[PROOF STEP]
unfolding gbm_nodes_list_it_def m1.iteratei_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it (map_iterator_dom (it_to_it (m1.list_it g))) (map_iterator_dom (it_to_it (m1.list_it g)))
[PROOF STEP]
by (intro icf_proper_iteratorI)


[STATEMENT]
lemma harry_meas_False_end [simp]: "harry_meas (xs @ [False]) = harry_meas xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. harry_meas (xs @ [False]) = harry_meas xs
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. harry_meas ([] @ [False]) = harry_meas []
 2. \<And>a xs. harry_meas (xs @ [False]) = harry_meas xs \<Longrightarrow> harry_meas ((a # xs) @ [False]) = harry_meas (a # xs)
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
harry_meas (xs @ [False]) = harry_meas xs

goal (2 subgoals):
 1. harry_meas ([] @ [False]) = harry_meas []
 2. \<And>a xs. harry_meas (xs @ [False]) = harry_meas xs \<Longrightarrow> harry_meas ((a # xs) @ [False]) = harry_meas (a # xs)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
harry_meas (xs @ [False]) = harry_meas xs

goal (1 subgoal):
 1. harry_meas ((x # xs) @ [False]) = harry_meas (x # xs)
[PROOF STEP]
by (cases x) (auto simp: harry_meas.simps)
[PROOF STATE]
proof (state)
this:
harry_meas ((x # xs) @ [False]) = harry_meas (x # xs)

goal (1 subgoal):
 1. harry_meas ([] @ [False]) = harry_meas []
[PROOF STEP]
qed (auto simp: harry_meas.simps)


[STATEMENT]
lemma bij_betw_emp[simp]:
"bij_betw f {} {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw f {} {}
[PROOF STEP]
unfolding bij_betw_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f {} \<and> f ` {} = {}
[PROOF STEP]
by auto