[STATEMENT]
lemma load_size:
  "(load m n off l = None) = (mem_size m < (off + n + l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (load m n off l = None) = (mem_size m < off + n + l)
[PROOF STEP]
unfolding load_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if n + off + l \<le> mem_size m then Some (read_bytes m (n + off) l) else None) = None) = (mem_size m < off + n + l)
[PROOF STEP]
by (cases "n + off + l \<le> mem_size m") auto


[STATEMENT]
lemma ctxt_comp_n_funas [simp]:
  "(f, v) \<in> funas_ctxt (C^n) \<Longrightarrow> (f, v) \<in> funas_ctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, v) \<in> funas_ctxt (C ^ n) \<Longrightarrow> (f, v) \<in> funas_ctxt C
[PROOF STEP]
by (induct n arbitrary: C) auto


[STATEMENT]
lemma inline_left_gpv_merge_exception_converter:
  "bind_gpv (inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter) (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) =
   bind_gpv (left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv))) (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))
[PROOF STEP]
apply(coinduction arbitrary: gpv rule: gpv.coinduct_strong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva. rel_spmf (rel_generat (=) (=) (rel_fun (=) (\<lambda>gpv gpv'. (\<exists>gpva. gpv = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> gpv' = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))) \<or> gpv = gpv'))) (the_gpv (inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))) (the_gpv (left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))))
[PROOF STEP]
apply(simp add: bind_gpv.sel inline_sel map_bind_spmf bind_map_spmf del: bind_gpv_sel')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva. rel_spmf (rel_generat (=) (=) (rel_fun (=) (\<lambda>gpv gpv'. (\<exists>gpva. gpv = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> gpv' = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))) \<or> gpv = gpv'))) (inline1 run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of (x, conv') \<Rightarrow> case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> case_sum Pure (\<lambda>(out, oracle, rpv). IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline run_converter (rpv x) y))))) (the_gpv gpva \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> map_generat id Inl left_rpv \<circ> map_generat id id (map_fun option_of_exception (map_gpv' id id option_of_exception)) \<circ> map_generat Some id (\<lambda>rpv. case_option (Done None) (\<lambda>input'. gpv_stop (rpv input')))))
[PROOF STEP]
apply(subst inline1_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva. rel_spmf (rel_generat (=) (=) (rel_fun (=) (\<lambda>gpv gpv'. (\<exists>gpva. gpv = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> gpv' = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpva)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))) \<or> gpv = gpv'))) (the_gpv (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpva))) \<bind> case_generat (\<lambda>x. return_spmf (Inl (x, merge_exception_converter))) (\<lambda>out rpv. the_gpv (run_converter merge_exception_converter out) \<bind> case_generat (\<lambda>(x, y). inline1 run_converter (rpv x) y) (\<lambda>out rpv'. return_spmf (Inr (out, rpv', rpv)))) \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of (x, conv') \<Rightarrow> case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> case_sum Pure (\<lambda>(out, oracle, rpv). IO out (\<lambda>input. oracle input \<bind> (\<lambda>(x, y). inline run_converter (rpv x) y))))) (the_gpv gpva \<bind> map_spmf (map_generat id id ((\<circ>) (case_sum id (\<lambda>r. r \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))))) \<circ> (case_generat (\<lambda>x. map_spmf (map_generat id id ((\<circ>) Inl)) (the_gpv (case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)))) (\<lambda>out c. return_spmf (IO out (\<lambda>input. Inr (c input)))) \<circ> map_generat id Inl left_rpv \<circ> map_generat id id (map_fun option_of_exception (map_gpv' id id option_of_exception)) \<circ> map_generat Some id (\<lambda>rpv. case_option (Done None) (\<lambda>input'. gpv_stop (rpv input')))))
[PROOF STEP]
apply(clarsimp simp add: bind_map_spmf intro!: rel_spmf_bind_reflI simp add: generat.map_comp case_map_generat o_def split!: generat.split intro!: rel_funI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>gpva out' c' y. \<lbrakk>IO out' c' \<in> set_spmf (the_gpv gpva); (case case merge_exception y of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c' input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<noteq> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c' input'))) y \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))\<rbrakk> \<Longrightarrow> \<exists>gpv. (case case merge_exception y of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c' input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c' input'))) y \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)) = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))
[PROOF STEP]
subgoal for gpv out c input
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>IO out c \<in> set_spmf (the_gpv gpv); (case case merge_exception input of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<noteq> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c input'))) input \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))\<rbrakk> \<Longrightarrow> \<exists>gpv. (case case merge_exception input of Fault \<Rightarrow> (Fault, const_converter Fault) | OK y' \<Rightarrow> (OK y', merge_exception_converter) of (x, xa) \<Rightarrow> inline run_converter (map_gpv' id id option_of_exception (case x of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (left_rpv c input'))) xa) \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) = inline run_converter (map_gpv' id id option_of_exception (gpv_stop (left_gpv gpv))) merge_exception_converter \<bind> (\<lambda>(x, conv'). case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, conv')) \<and> left_rpv (\<lambda>input'. map_gpv' id id option_of_exception (case input' of Fault \<Rightarrow> Done None | OK input' \<Rightarrow> gpv_stop (c input'))) input \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter)) = left_gpv (map_gpv' id id option_of_exception (gpv_stop gpv)) \<bind> (\<lambda>x. case x of None \<Rightarrow> Fail | Some x' \<Rightarrow> Done (x, merge_exception_converter))
[PROOF STEP]
by(cases input; auto split!: exception.split)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma language_equal_impl_refine[autoref_rules]:
    assumes "SIDE_PRECOND (finite (NBA.nodes A))"
    assumes "SIDE_PRECOND (finite (NBA.nodes B))"
    assumes "SIDE_PRECOND (nba.alphabet A = nba.alphabet B)"
    assumes "(Ai, A) \<in> \<langle>Id, nat_rel\<rangle> nbai_nba_rel"
    assumes "(Bi, B) \<in> \<langle>Id, nat_rel\<rangle> nbai_nba_rel"
    shows "(language_equal_impl Ai Bi, (OP op_language_equal :::
      \<langle>Id, nat_rel\<rangle> nbai_nba_rel \<rightarrow> \<langle>Id, nat_rel\<rangle> nbai_nba_rel \<rightarrow> bool_rel) $ A $ B) \<in> bool_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (language_equal_impl Ai Bi, (OP op_language_equal ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> bool_rel) $ A $ B) \<in> bool_rel
[PROOF STEP]
using language_equal_impl.refine[OF assms[unfolded autoref_tag_defs]]
[PROOF STATE]
proof (prove)
using this:
(language_equal_impl Ai Bi, NBA.language A \<subseteq> NBA.language B \<and> NBA.language B \<subseteq> NBA.language A) \<in> bool_rel

goal (1 subgoal):
 1. (language_equal_impl Ai Bi, (OP op_language_equal ::: \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> \<langle>Id, nat_rel\<rangle>nbai_nba_rel \<rightarrow> bool_rel) $ A $ B) \<in> bool_rel
[PROOF STEP]
by auto


[STATEMENT]
lemma tm_skip_first_arg_len_eq_1_cases:
  fixes s::nat
  assumes "inv_tm_skip_first_arg_len_eq_1 n (s,l,r)"
    and "s=0 \<Longrightarrow> P"
    and "s=1 \<Longrightarrow> P"
    and "s=2 \<Longrightarrow> P"
    and "s=3 \<Longrightarrow> P"
    and "s=4 \<Longrightarrow> P"
    and "s=5 \<Longrightarrow> P"
  shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P
[PROOF STEP]
have "s < 6"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < 6
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> s < 6 \<Longrightarrow> False
[PROOF STEP]
assume "\<not> s < 6"
[PROOF STATE]
proof (state)
this:
\<not> s < 6

goal (1 subgoal):
 1. \<not> s < 6 \<Longrightarrow> False
[PROOF STEP]
with \<open>inv_tm_skip_first_arg_len_eq_1 n (s,l,r)\<close>
[PROOF STATE]
proof (chain)
picking this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
\<not> s < 6
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
\<not> s < 6

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

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

goal (1 subgoal):
 1. P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s < 6
[PROOF STEP]
have "s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3  \<or> s = 4 \<or> s = 5"
[PROOF STATE]
proof (prove)
using this:
s < 6

goal (1 subgoal):
 1. s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5

goal (1 subgoal):
 1. P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
s = 0 \<Longrightarrow> P
s = 1 \<Longrightarrow> P
s = 2 \<Longrightarrow> P
s = 3 \<Longrightarrow> P
s = 4 \<Longrightarrow> P
s = 5 \<Longrightarrow> P
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_tm_skip_first_arg_len_eq_1 n (s, l, r)
s = 0 \<Longrightarrow> P
s = 1 \<Longrightarrow> P
s = 2 \<Longrightarrow> P
s = 3 \<Longrightarrow> P
s = 4 \<Longrightarrow> P
s = 5 \<Longrightarrow> P
s = 0 \<or> s = 1 \<or> s = 2 \<or> s = 3 \<or> s = 4 \<or> s = 5

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma flatten_prec:
  "precise is_flatten_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise is_flatten_list
[PROOF STEP]
apply (intro preciseI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> is_flatten_list a p * F \<and>\<^sub>A is_flatten_list a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
case (1 aa b p F F' lsi' ls' lsi'a ls'a)
[PROOF STATE]
proof (state)
this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'
[PROOF STEP]
have *:
      "\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'"
[PROOF STATE]
proof (prove)
using this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'
[PROOF STEP]
by (smt (z3) assn_aci(10) assn_times_comm)
[PROOF STATE]
proof (state)
this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
have "lsi' = lsi'a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lsi' = lsi'a
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. lsi' = lsi'a
[PROOF STEP]
by (metis outer_list.precise preciseD star_assoc)
[PROOF STATE]
proof (state)
this:
lsi' = lsi'a

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lsi' = lsi'a

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
have "length ls'a = length lsi'a" "length ls' = length lsi'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ls'a = length lsi'a &&& length ls' = length lsi'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F'

goal (1 subgoal):
 1. length ls'a = length lsi'a &&& length ls' = length lsi'
[PROOF STEP]
by (auto simp add: mod_and_dist dest!: mod_starD list_assn_len)
[PROOF STATE]
proof (state)
this:
length ls'a = length lsi'a
length ls' = length lsi'

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lsi' = lsi'a
length ls'a = length lsi'a
length ls' = length lsi'
[PROOF STEP]
have "length ls' = length lsi'" "length lsi' = length lsi'a" "length lsi'a = length ls'a"
[PROOF STATE]
proof (prove)
using this:
lsi' = lsi'a
length ls'a = length lsi'a
length ls' = length lsi'

goal (1 subgoal):
 1. length ls' = length lsi' &&& length lsi' = length lsi'a &&& length lsi'a = length ls'a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a

goal (1 subgoal):
 1. \<And>aa b p F F' lsi' ls' lsi'a ls'a. (aa, b) \<Turnstile> is_outer_list lsi'a p * list_assn is_inner_list ls'a lsi'a * F \<and>\<^sub>A is_outer_list lsi' p * list_assn is_inner_list ls' lsi' * F' \<Longrightarrow> concat ls'a = concat ls'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a

goal (1 subgoal):
 1. concat ls'a = concat ls'
[PROOF STEP]
using * \<open>lsi' = lsi'a\<close>
[PROOF STATE]
proof (prove)
using this:
length ls' = length lsi'
length lsi' = length lsi'a
length lsi'a = length ls'a
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ls'a lsi'a * G \<and>\<^sub>A list_assn is_inner_list ls' lsi' * G'
lsi' = lsi'a

goal (1 subgoal):
 1. concat ls'a = concat ls'
[PROOF STEP]
proof(induction ls' lsi' lsi'a ls'a arbitrary: p rule: list_induct4)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'; [] = []\<rbrakk> \<Longrightarrow> concat [] = concat []
 2. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'
[] = []

goal (2 subgoals):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'; [] = []\<rbrakk> \<Longrightarrow> concat [] = concat []
 2. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'
[] = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list [] [] * G \<and>\<^sub>A list_assn is_inner_list [] [] * G'
[] = []

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

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
case (Cons x xs y ys z zs w ws)
[PROOF STATE]
proof (state)
this:
length xs = length ys
length ys = length zs
length zs = length ws
\<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs = length ys
length ys = length zs
length zs = length ws
\<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs
[PROOF STEP]
have "concat ws = concat xs"
[PROOF STATE]
proof (prove)
using this:
length xs = length ys
length ys = length zs
length zs = length ws
\<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs

goal (1 subgoal):
 1. concat ws = concat xs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ws; length zs = length ws; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs zs * G' \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> is_inner_list w z * list_assn is_inner_list ws zs * G \<and>\<^sub>A is_inner_list x z * list_assn is_inner_list xs zs * G'; y = z \<and> ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs
[PROOF STEP]
by (metis (no_types, opaque_lifting) ab_semigroup_mult_class.mult.left_commute star_assoc)
[PROOF STATE]
proof (state)
this:
concat ws = concat xs

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
concat ws = concat xs

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
have "x = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = w
[PROOF STEP]
using "Cons.prems" preciseD[OF inner_list.precise, where h="(aa,b)"]
[PROOF STATE]
proof (prove)
using this:
\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'
y # ys = z # zs
(aa, b) \<Turnstile> is_inner_list ?a ?p * ?F \<and>\<^sub>A is_inner_list ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'

goal (1 subgoal):
 1. x = w
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> is_inner_list w z * list_assn is_inner_list ws zs * G \<and>\<^sub>A is_inner_list x z * list_assn is_inner_list xs zs * G'; y = z \<and> ys = zs; \<And>a p F a' F'. (aa, b) \<Turnstile> is_inner_list a p * F \<and>\<^sub>A is_inner_list a' p * F' \<Longrightarrow> a = a'\<rbrakk> \<Longrightarrow> x = w
[PROOF STEP]
using assn_times_assoc
[PROOF STATE]
proof (prove)
using this:
?P * ?Q * ?R = ?P * (?Q * ?R)

goal (1 subgoal):
 1. \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> is_inner_list w z * list_assn is_inner_list ws zs * G \<and>\<^sub>A is_inner_list x z * list_assn is_inner_list xs zs * G'; y = z \<and> ys = zs; \<And>a p F a' F'. (aa, b) \<Turnstile> is_inner_list a p * F \<and>\<^sub>A is_inner_list a' p * F' \<Longrightarrow> a = a'\<rbrakk> \<Longrightarrow> x = w
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = w

goal (1 subgoal):
 1. \<And>x xs y ys z zs w ws. \<lbrakk>length xs = length ys; length ys = length zs; length zs = length ws; \<lbrakk>\<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list ws zs * G \<and>\<^sub>A list_assn is_inner_list xs ys * G'; ys = zs\<rbrakk> \<Longrightarrow> concat ws = concat xs; \<exists>G G'. (aa, b) \<Turnstile> list_assn is_inner_list (w # ws) (z # zs) * G \<and>\<^sub>A list_assn is_inner_list (x # xs) (y # ys) * G'; y # ys = z # zs\<rbrakk> \<Longrightarrow> concat (w # ws) = concat (x # xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
concat ws = concat xs
x = w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
concat ws = concat xs
x = w

goal (1 subgoal):
 1. concat (w # ws) = concat (x # xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat (w # ws) = concat (x # xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
concat ls'a = concat ls'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma order_impl_root_order: "\<lbrakk>k > 0; order k t\<rbrakk> \<Longrightarrow> root_order k t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < k; order k t\<rbrakk> \<Longrightarrow> root_order k t
[PROOF STEP]
apply(cases t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < k; order k t; t = Leaf\<rbrakk> \<Longrightarrow> root_order k t
 2. \<And>x21 x22. \<lbrakk>0 < k; order k t; t = Node x21 x22\<rbrakk> \<Longrightarrow> root_order k t
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma new_element_get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a:
  "h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> new_element \<rightarrow>\<^sub>h h' \<Longrightarrow> preserved (get_M ptr getter) h h'
[PROOF STEP]
by(auto simp add: new_element_def get_M_defs preserved_def split: prod.splits option.splits
      elim!: bind_returns_result_E bind_returns_heap_E)


[STATEMENT]
lemma (in is_ntcf) ntcf_is_ntsmcf':
  assumes "\<FF>' = cf_smcf \<FF>"
    and "\<GG>' = cf_smcf \<GG>"
    and "\<AA>' = cat_smc \<AA>"
    and "\<BB>' = cat_smc \<BB>"
  shows "ntcf_ntsmcf \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(1-4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf \<NN> : cf_smcf \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf \<GG> : cat_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<BB>
[PROOF STEP]
by (rule ntcf_is_ntsmcf)


[STATEMENT]
lemma has_locks_lock_lock_conv' [simp]:
  "\<lbrakk> may_lock l t'; t \<noteq> t' \<rbrakk> \<Longrightarrow> has_locks (lock_lock l t') t = has_locks l t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>may_lock l t'; t \<noteq> t'\<rbrakk> \<Longrightarrow> has_locks (lock_lock l t') t = has_locks l t
[PROOF STEP]
by(cases l)(auto elim: may_lock.cases)


[STATEMENT]
lemma not_GCons_self2 [simp]:
  fixes xs::\<Gamma>
  shows "x #\<^sub>\<Gamma> xs \<noteq> xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x #\<^sub>\<Gamma> xs \<noteq> xs
[PROOF STEP]
by (rule not_GCons_self [symmetric])


[STATEMENT]
lemma supp_Alts[simp]: "supp (Alts e1 e2) = supp e1 \<union> supp e2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. supp (Alts e1 e2) = supp e1 \<union> supp e2
[PROOF STEP]
unfolding supp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> Alts e1 e2 \<noteq> Alts e1 e2}} = {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> e1 \<noteq> e1}} \<union> {a. infinite {b. (a \<rightleftharpoons> b) \<bullet> e2 \<noteq> e2}}
[PROOF STEP]
by (auto simp add: Collect_imp_eq Collect_neg_eq)


[STATEMENT]
lemma (in infinite_coin_toss_space) pseudo_proj_False_neq_True:
  shows "pseudo_proj_False n w \<noteq> pseudo_proj_True n w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_proj_False n w \<noteq> pseudo_proj_True n w
[PROOF STEP]
proof (rule diff_streams_if, intro exI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
have "snth (pseudo_proj_False n w) n = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_proj_False n w !! n = False
[PROOF STEP]
unfolding pseudo_proj_False_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((stake n w @ [False]) @- sconst True) !! n = False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pseudo_proj_False n w !! n = False

goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pseudo_proj_False n w !! n = False

goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
have "snth (pseudo_proj_True n w) n = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_proj_True n w !! n = True
[PROOF STEP]
unfolding pseudo_proj_True_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stake n w @- sconst True) !! n = True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pseudo_proj_True n w !! n = True

goal (1 subgoal):
 1. pseudo_proj_False n w !! ?n2 \<noteq> pseudo_proj_True n w !! ?n2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pseudo_proj_False n w !! n = False
pseudo_proj_True n w !! n = True
[PROOF STEP]
show "snth (pseudo_proj_False n w) n \<noteq> snth (pseudo_proj_True n w) n"
[PROOF STATE]
proof (prove)
using this:
pseudo_proj_False n w !! n = False
pseudo_proj_True n w !! n = True

goal (1 subgoal):
 1. pseudo_proj_False n w !! n \<noteq> pseudo_proj_True n w !! n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pseudo_proj_False n w !! n \<noteq> pseudo_proj_True n w !! n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  bernoulli_stream_element_prob_rec':
  fixes x
  assumes "M = bernoulli_stream p"
and "0 \<le> p" and "p \<le> 1"
  shows "\<And> n. measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)} =
    (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
have "ennreal (measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)}) =
    emeasure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x}
[PROOF STEP]
by (metis (no_types, lifting) assms(1) bernoulli_stream_def emeasure_eq_ennreal_measure
        emeasure_space ennreal_top_neq_one neq_top_trans prob_space.emeasure_space_1
        prob_space.prob_space_stream_space prob_space_measure_pmf)
[PROOF STATE]
proof (state)
this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x}

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x}

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
have "... = (emeasure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)
[PROOF STEP]
using bernoulli_stream_element_prob_rec assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?M = bernoulli_stream ?p; 0 \<le> ?p; ?p \<le> 1\<rbrakk> \<Longrightarrow> emeasure ?M {w \<in> space ?M. stake (Suc ?n) w = stake (Suc ?n) ?x} = emeasure ?M {w \<in> space ?M. stake ?n w = stake ?n ?x} * ennreal (prob_component ?p ?x ?n)
M = bernoulli_stream p
0 \<le> p
p \<le> 1

goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake (Suc n) w = stake (Suc n) x} = emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
have "... = (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
have "prob_space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prob_space M
[PROOF STEP]
using assms(1) bernoulli_stream_def prob_space.prob_space_stream_space prob_space_measure_pmf
[PROOF STATE]
proof (prove)
using this:
M = bernoulli_stream p
bernoulli_stream ?p = stream_space (measure_pmf (bernoulli_pmf ?p))
prob_space ?M \<Longrightarrow> prob_space (stream_space ?M)
prob_space (measure_pmf ?p)

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

goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prob_space M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prob_space M

goal (1 subgoal):
 1. emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
by (simp add: ennreal_mult'' finite_measure.emeasure_eq_measure mult.commute prob_space_def)
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emeasure M {w \<in> space M. stake n w = stake n x} * ennreal (prob_component p x n) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
have "ennreal (measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)}) =
    (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
using this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. \<And>n. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
thus "measure M {w\<in> space M. (stake (Suc n) w = stake (Suc n) x)} =
    (measure M {w\<in> space M. (stake n w = stake n x)} * prob_component p x n)"
[PROOF STATE]
proof (prove)
using this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)

goal (1 subgoal):
 1. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
using assms prob_component_def
[PROOF STATE]
proof (prove)
using this:
ennreal \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = ennreal (\<P>(w in M. stake n w = stake n x) * prob_component p x n)
M = bernoulli_stream p
0 \<le> p
p \<le> 1
prob_component ?p ?w ?n = (if ?w !! ?n then ?p else 1 - ?p)

goal (1 subgoal):
 1. \<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<P>(w in M. stake (Suc n) w = stake (Suc n) x) = \<P>(w in M. stake n w = stake n x) * prob_component p x n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma circ_decompose_12:
  "x\<^sup>\<circ> * y\<^sup>\<circ> \<le> (x\<^sup>\<circ> * y)\<^sup>\<circ> * x\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<circ> * y\<^sup>\<circ> \<le> (x\<^sup>\<circ> * y)\<^sup>\<circ> * x\<^sup>\<circ>
[PROOF STEP]
by (metis circ_sup_9 circ_sub_dist_3)


[STATEMENT]
lemma ap_tree_extensional:
  "(\<And>x. f \<diamondop> x = g \<diamondop> x) \<Longrightarrow> f = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f \<diamondop> x = g \<diamondop> x) \<Longrightarrow> f = g
[PROOF STEP]
by(rule ap_tree_strong_extensional) simp


[STATEMENT]
lemma zcf_mult:
  assumes "p \<in> carrier P"
  assumes "q \<in> carrier P"
  shows "zcf(p \<otimes>\<^bsub>P\<^esub> q) = (zcf p) \<otimes> (zcf q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcf (p \<otimes>\<^bsub>P\<^esub> q) = zcf p \<otimes> zcf q
[PROOF STEP]
using zcf_to_fun[of " p \<otimes>\<^bsub>P\<^esub> q" ] zcf_to_fun[of "p" ] zcf_to_fun[of "q" ] to_fun_mult[of q p \<zero>]
[PROOF STATE]
proof (prove)
using this:
p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P \<Longrightarrow> zcf (p \<otimes>\<^bsub>P\<^esub> q) = to_fun (p \<otimes>\<^bsub>P\<^esub> q) \<zero>
p \<in> carrier P \<Longrightarrow> zcf p = to_fun p \<zero>
q \<in> carrier P \<Longrightarrow> zcf q = to_fun q \<zero>
\<lbrakk>q \<in> carrier P; p \<in> carrier P; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> to_fun (p \<otimes>\<^bsub>P\<^esub> q) \<zero> = to_fun p \<zero> \<otimes> to_fun q \<zero>

goal (1 subgoal):
 1. zcf (p \<otimes>\<^bsub>P\<^esub> q) = zcf p \<otimes> zcf q
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma factor_theorem:
  assumes "f \<in> carrier P"
  assumes "a \<in> carrier R"
  assumes "g = UP_root_div f a"
  assumes "to_fun f a = \<zero>"
  shows "f = (X_minus a) \<otimes>\<^bsub>P\<^esub> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
[PROOF STEP]
using remainder_theorem[of f a g _] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier P; a \<in> carrier R; g = UP_root_div f a; ?r = UP_root_rem f a\<rbrakk> \<Longrightarrow> f = ?r \<oplus>\<^bsub>P\<^esub> X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
f \<in> carrier P
a \<in> carrier R
g = UP_root_div f a
to_fun f a = \<zero>

goal (1 subgoal):
 1. f = X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
[PROOF STEP]
unfolding UP_root_rem_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f \<in> carrier P; a \<in> carrier R; g = UP_root_div f a; ?r = monom P (T\<^bsub>a\<^esub> f 0) 0\<rbrakk> \<Longrightarrow> f = ?r \<oplus>\<^bsub>P\<^esub> X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
f \<in> carrier P
a \<in> carrier R
g = UP_root_div f a
to_fun f a = \<zero>

goal (1 subgoal):
 1. f = X_poly_minus R a \<otimes>\<^bsub>P\<^esub> g
[PROOF STEP]
by (simp add: ctrm_zcf taylor_zcf taylor_closed UP_root_div_closed X_minus_closed)


[STATEMENT]
lemma is_pod_ta_eps_empty:
  "is_ta_eps_free (ta R) \<Longrightarrow> is_ta_eps_free (ta L) \<Longrightarrow> is_ta_eps_free (ta (reg_intersect R L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ta_eps_free (ta R); is_ta_eps_free (ta L)\<rbrakk> \<Longrightarrow> is_ta_eps_free (ta (reg_intersect R L))
[PROOF STEP]
by (auto simp: reg_intersect_def prod_ta_def prod_epsRp_def prod_epsLp_def is_ta_eps_free_def)


[STATEMENT]
lemma [param]: "(g, id) \<in> rel \<rightarrow> Id_on (Range rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.g, id) \<in> local.rel \<rightarrow> Id_on (Range local.rel)
[PROOF STEP]
unfolding rel_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.g, id) \<in> br local.g (\<lambda>k. k \<in> local.f ` nodes A) \<rightarrow> Id_on (Range (br local.g (\<lambda>k. k \<in> local.f ` nodes A)))
[PROOF STEP]
by (auto simp: in_br_conv)


[STATEMENT]
lemma "all_security_requirements_fulfilled I8Requirements I8SSHgraph"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TopoS_Composition_Theory_impl.all_security_requirements_fulfilled I8Requirements I8SSHgraph
[PROOF STEP]
by eval


[STATEMENT]
lemma step_invariant_mono:
  assumes "step_invariant (ws, ps, N) = (ws', ps', N')"
  shows "snd ` set ws \<union> set ps \<subseteq> snd ` set ws' \<union> set ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd ` set ws \<union> set ps \<subseteq> snd ` set ws' \<union> set ps'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step_invariant (ws, ps, N) = (ws', ps', N')

goal (1 subgoal):
 1. snd ` set ws \<union> set ps \<subseteq> snd ` set ws' \<union> set ps'
[PROOF STEP]
proof (intro subsetI, elim UnE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
assume "x \<in> snd `set ws"
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set ws

goal (2 subgoals):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set ws
[PROOF STEP]
show "x \<in> snd ` set ws' \<union> set ps'"
[PROOF STATE]
proof (prove)
using this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set ws

goal (1 subgoal):
 1. x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
proof (cases "x = snd (hd ws)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x \<noteq> snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> snd (hd ws)

goal (2 subgoals):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x \<noteq> snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
with \<open>x \<in> image snd (set ws)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> snd ` set ws
x \<noteq> snd (hd ws)
[PROOF STEP]
have "x \<in> snd ` set (tl ws)"
[PROOF STATE]
proof (prove)
using this:
x \<in> snd ` set ws
x \<noteq> snd (hd ws)

goal (1 subgoal):
 1. x \<in> snd ` set (tl ws)
[PROOF STEP]
by (cases ws) auto
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set (tl ws)

goal (2 subgoals):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
 2. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x \<noteq> snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set (tl ws)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step_invariant (ws, ps, N) = (ws', ps', N')
x \<in> snd ` set (tl ws)

goal (1 subgoal):
 1. x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
by (auto split: prod.splits simp: Let_def)
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set ws' \<union> set ps'

goal (1 subgoal):
 1. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> snd ` set ws; x = snd (hd ws)\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
qed (auto split: prod.splits simp: Let_def)
[PROOF STATE]
proof (state)
this:
x \<in> snd ` set ws' \<union> set ps'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>step_invariant (ws, ps, N) = (ws', ps', N'); step_invariant (ws, ps, N) = (ws', ps', N'); x \<in> set ps\<rbrakk> \<Longrightarrow> x \<in> snd ` set ws' \<union> set ps'
[PROOF STEP]
qed (auto split: prod.splits simp: Let_def)


[STATEMENT]
lemma primes_omega_eq_0_iff: "primes_omega n = 0 \<longleftrightarrow> n = 0 \<or> n = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (primes_omega n = 0) = (n = 0 \<or> n = 1)
[PROOF STEP]
by (auto simp: primes_omega_def prime_factorization_empty_iff)


[STATEMENT]
lemma Eats_Mem_sf:
  assumes "\<And>j::name. Sigma_fm (Var j EQ t)"
      and "\<And>k::name. Sigma_fm (Var k EQ u)"
  shows "Sigma_fm (Eats t u IN Var i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
obtain j::name where j: "atom j \<sharp> (t,u,Var i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. atom j \<sharp> (t, u, Var i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (t, u, Var i)

goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
hence "{} \<turnstile> Eats t u IN Var i IFF
              Ex j (Var j IN Var i AND Var j EQ Eats t u)"
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (t, u, Var i)

goal (1 subgoal):
 1. {} \<turnstile> Eats t u IN Var i IFF SyntaxN.Ex j (Var j IN Var i AND Var j EQ Eats t u)
[PROOF STEP]
apply (auto simp: fresh_Pair intro: Ex_I [where x="Eats t u"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom j \<sharp> t; atom j \<sharp> u; atom j \<sharp> i\<rbrakk> \<Longrightarrow> {Var j IN Var i, Var j EQ Eats t u} \<turnstile> Eats t u IN Var i
[PROOF STEP]
apply (metis Assume Mem_cong [OF _ Refl, THEN Iff_MP_same] rotate2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{} \<turnstile> Eats t u IN Var i IFF SyntaxN.Ex j (Var j IN Var i AND Var j EQ Eats t u)

goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<turnstile> Eats t u IN Var i IFF SyntaxN.Ex j (Var j IN Var i AND Var j EQ Eats t u)

goal (1 subgoal):
 1. Sigma_fm (Eats t u IN Var i)
[PROOF STEP]
by (rule Sigma_fm_Iff) (auto simp: assms supp_conv_fresh Eq_Eats_sf)
[PROOF STATE]
proof (state)
this:
Sigma_fm (Eats t u IN Var i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measure_to_qbs_cong_sets:
  assumes "sets M = sets N"
  shows "measure_to_qbs M = measure_to_qbs N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_to_qbs M = measure_to_qbs N
[PROOF STEP]
by(rule qbs_eqI) (simp add: measurable_cong_sets[OF _ assms])


[STATEMENT]
lemma and_or_s:
assumes "(((get_S w1))::word1) = 0 \<and>
  (AND) w2 (0b00000000000000000000000010000000::word32) = 0"
shows "(((get_S ((OR) ((AND) w1
  (0b11111111000011111111111111111111::word32)) w2)))::word1) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
get_S w1 = 0 \<and> w2 AND 128 = 0
[PROOF STEP]
have "w1 AND 128 = 0"
[PROOF STATE]
proof (prove)
using this:
get_S w1 = 0 \<and> w2 AND 128 = 0

goal (1 subgoal):
 1. w1 AND 128 = 0
[PROOF STEP]
using ucast_s
[PROOF STATE]
proof (prove)
using this:
get_S w1 = 0 \<and> w2 AND 128 = 0
get_S ?w = 0 \<Longrightarrow> ?w AND 128 = 0

goal (1 subgoal):
 1. w1 AND 128 = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w1 AND 128 = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w1 AND 128 = 0
[PROOF STEP]
have "(w1 AND 4279238655 OR w2) AND 128 = 0"
[PROOF STATE]
proof (prove)
using this:
w1 AND 128 = 0

goal (1 subgoal):
 1. (w1 AND 4279238655 OR w2) AND 128 = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
w1 AND 128 = 0
get_S w1 = 0 \<and> w2 AND 128 = 0

goal (1 subgoal):
 1. (w1 AND 4279238655 OR w2) AND 128 = 0
[PROOF STEP]
by (metis word_ao_absorbs(6) word_ao_dist word_bw_comms(2))
[PROOF STATE]
proof (state)
this:
(w1 AND 4279238655 OR w2) AND 128 = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(w1 AND 4279238655 OR w2) AND 128 = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(w1 AND 4279238655 OR w2) AND 128 = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
using ucast_s2
[PROOF STATE]
proof (prove)
using this:
(w1 AND 4279238655 OR w2) AND 128 = 0
?w AND 128 = 0 \<Longrightarrow> get_S ?w = 0

goal (1 subgoal):
 1. get_S (w1 AND 4279238655 OR w2) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_S (w1 AND 4279238655 OR w2) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma memory_write_asi_low_equal:
assumes a1: "low_equal s1 s2 \<and>
Some t1 = memory_write_asi 10 addr bm data s1 \<and>
Some t2 = memory_write_asi 10 addr bm data s2"
shows "low_equal t1 t2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. low_equal t1 t2
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
low_equal s1 s2 \<and> Some t1 = memory_write_asi 10 addr bm data s1 \<and> Some t2 = memory_write_asi 10 addr bm data s2

goal (1 subgoal):
 1. low_equal t1 t2
[PROOF STEP]
apply (simp add: memory_write_asi_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. low_equal s1 s2 \<and> Some t1 = store_word_mem (add_data_cache s1 addr data bm) addr data bm 10 \<and> Some t2 = store_word_mem (add_data_cache s2 addr data bm) addr data bm 10 \<Longrightarrow> low_equal t1 t2
[PROOF STEP]
by (meson add_data_cache_low_equal store_word_mem_low_equal)


[STATEMENT]
lemma non_interference_induct_case_sub2:
assumes a1:
"(user_seq_exe n s1 \<and>
          user_seq_exe n s2 \<longrightarrow>
          (\<exists>t1. Some t1 = SEQ n s1 \<and>
               (\<exists>t2. Some t2 = SEQ n s2 \<and>
                     (((get_S (cpu_reg_val PSR t1)))::word1) = 0 \<and>
    (((get_S (cpu_reg_val PSR t2)))::word1) = 0 \<and> low_equal t1 t2))) \<and>
user_seq_exe (Suc n) s1 \<and>
         user_seq_exe (Suc n) s2"
shows "\<exists>t1. Some t1 = (case SEQ n s1 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and>
              (\<exists>t2. Some t2 = (case SEQ n s2 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and>
                    (((get_S (cpu_reg_val PSR t1)))::word1) = 0 \<and>
    (((get_S (cpu_reg_val PSR t2)))::word1) = 0 \<and> low_equal t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t1. Some t1 = (case SEQ n s1 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> (\<exists>t2. Some t2 = (case SEQ n s2 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> get_S (cpu_reg_val PSR t1) = 0 \<and> get_S (cpu_reg_val PSR t2) = 0 \<and> low_equal t1 t2)
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
(user_seq_exe n s1 \<and> user_seq_exe n s2 \<longrightarrow> (\<exists>t1. Some t1 = SEQ n s1 \<and> (\<exists>t2. Some t2 = SEQ n s2 \<and> get_S (cpu_reg_val PSR t1) = 0 \<and> get_S (cpu_reg_val PSR t2) = 0 \<and> low_equal t1 t2))) \<and> user_seq_exe (Suc n) s1 \<and> user_seq_exe (Suc n) s2

goal (1 subgoal):
 1. \<exists>t1. Some t1 = (case SEQ n s1 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> (\<exists>t2. Some t2 = (case SEQ n s2 of None \<Rightarrow> None | Some x \<Rightarrow> NEXT x) \<and> get_S (cpu_reg_val PSR t1) = 0 \<and> get_S (cpu_reg_val PSR t2) = 0 \<and> low_equal t1 t2)
[PROOF STEP]
by (simp add: non_interference_induct_case user_seq_exe_def)