[STATEMENT]
lemma nofail_WHILE_eq_rwof:
    assumes NF: "nofail (m0 \<bind> WHILE cond step)"
    shows "m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not>cond s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
from NF WHILE_bounded[of m0 cond step]
[PROOF STATE]
proof (chain)
picking this:
nofail (m0 \<bind> WHILE cond step)
m0 \<bind> WHILE cond step = filter_nb cond (Sup {bounded_WHILE n cond step m0 |n. True})
[PROOF STEP]
have NF':
      "nofail (Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0})"
[PROOF STATE]
proof (prove)
using this:
nofail (m0 \<bind> WHILE cond step)
m0 \<bind> WHILE cond step = filter_nb cond (Sup {bounded_WHILE n cond step m0 |n. True})

goal (1 subgoal):
 1. nofail (Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0})
[PROOF STEP]
by (auto simp: filter_nb_cont)
[PROOF STATE]
proof (state)
this:
nofail (Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0})

goal (1 subgoal):
 1. m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
(*from NF WHILE_bounded[of m0 cond step] obtain X
      where FR:
        "Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0} = RES X"
      by (auto simp: nofail_RES_conv filter_nb_cont)*)
[PROOF STATE]
proof (state)
this:
nofail (Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0})

goal (1 subgoal):
 1. m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
unfolding WHILE_bounded[of m0 cond step] filter_nb_cont
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {filter_nb cond m |m. m \<in> {bounded_WHILE n cond step m0 |n. True}} = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0} = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0} \<le> SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
 2. SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s) \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}
[PROOF STEP]
show "Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}
        \<le> SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0} \<le> SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
using NF' pw_bounded_WHILE_RES_rwof[of _ cond step m0]
[PROOF STATE]
proof (prove)
using this:
nofail (Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0})
\<lbrakk>nofail (bounded_WHILE ?n cond step m0); inres (bounded_WHILE ?n cond step m0) ?x\<rbrakk> \<Longrightarrow> rwof m0 cond step ?x

goal (1 subgoal):
 1. Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0} \<le> SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
[PROOF STEP]
by (fastforce simp: pw_le_iff refine_pw_simps)
[PROOF STATE]
proof (state)
this:
Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0} \<le> SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)

goal (1 subgoal):
 1. SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s) \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s) \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}
[PROOF STEP]
show "SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)
        \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s) \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}
[PROOF STEP]
using NF' pw_rwof_in_bounded_WHILE[of m0 cond step]
[PROOF STATE]
proof (prove)
using this:
nofail (Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0})
rwof m0 cond step ?x \<Longrightarrow> \<exists>n. inres (bounded_WHILE n cond step m0) ?x

goal (1 subgoal):
 1. SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s) \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}
[PROOF STEP]
by (fastforce simp: pw_le_iff refine_pw_simps)
[PROOF STATE]
proof (state)
this:
SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s) \<le> Sup {filter_nb cond m |m. \<exists>n. m = bounded_WHILE n cond step m0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m0 \<bind> WHILE cond step = SPEC (\<lambda>s. rwof m0 cond step s \<and> \<not> cond s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma marked_deletions_sweep_loop_free[simp]:
  notes fun_upd_apply[simp]
  shows
  "\<lbrakk> mut_m.marked_deletions m s; mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s \<rbrakk>
     \<Longrightarrow> mut_m.marked_deletions m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mut_m.marked_deletions m s; mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s\<rbrakk> \<Longrightarrow> mut_m.marked_deletions m (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
unfolding mut_m.marked_deletions_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> marked_deletion x s; mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))) \<longrightarrow> marked_deletion x (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
apply (clarsimp split: mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x21 x22 x23. \<lbrakk>\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (\<forall>x21 x22. (\<forall>x23. x \<noteq> mw_Mutate x21 x22 x23) \<or> obj_at_field_on_heap (\<lambda>r'. marked r' s) x21 x22 s); mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate x21 x22 x23 \<in> set (sys_mem_store_buffers (mutator m) s)\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>r'. marked r' s \<and> r' \<noteq> r) x21 x22 (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
apply (rename_tac ref field option)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref field option. \<lbrakk>\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (\<forall>x21 x22. (\<forall>x23. x \<noteq> mw_Mutate x21 x22 x23) \<or> obj_at_field_on_heap (\<lambda>r'. marked r' s) x21 x22 s); mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s)\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>r'. marked r' s \<and> r' \<noteq> r) ref field (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
apply (drule_tac x="mw_Mutate ref field option" in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref field option. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (\<forall>x21 x22. (\<forall>x23. mw_Mutate ref field option \<noteq> mw_Mutate x21 x22 x23) \<or> obj_at_field_on_heap (\<lambda>r'. marked r' s) x21 x22 s)\<rbrakk> \<Longrightarrow> obj_at_field_on_heap (\<lambda>r'. marked r' s \<and> r' \<noteq> r) ref field (s(sys := s sys\<lparr>heap := (sys_heap s)(r := None)\<rparr>))
[PROOF STEP]
apply (clarsimp simp: obj_at_field_on_heap_def split: option.splits)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> (obj_fields x2a field = None \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r))
 2. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> obj_fields x2a field = None \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r
 2. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 3. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (clarsimp simp: mut_m.reachable_snapshot_inv_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>field option x2a. \<lbrakk>\<forall>x. mut_m.reachable m x s \<longrightarrow> in_snapshot x s; no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2a; obj_fields x2a field = None\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 3. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (drule spec[where x=r], clarsimp simp: in_snapshot_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>field option x2a. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2a; obj_fields x2a field = None; mut_m.reachable m r s \<longrightarrow> black r s \<or> (\<exists>x. (x grey_protects_white r) s)\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 3. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (drule mp, auto simp: mut_m.reachable_def mut_m.tso_store_refs_def split: mem_store_action.splits)[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>field option x2a x. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2a; obj_fields x2a field = None; (x grey_protects_white r) s\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 3. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
(* FIXME rule *)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>field option x2a x. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2a; obj_fields x2a field = None; (x grey_protects_white r) s\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 3. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (drule grey_protects_whiteD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>field option x2a x. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2a; obj_fields x2a field = None; grey x s \<and> (x = r \<or> white r s)\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 3. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (clarsimp simp: no_grey_refs_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ref field option x2 x2a. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = None\<rbrakk> \<Longrightarrow> \<forall>x2b. obj_fields x2a field = Some x2b \<longrightarrow> x2 = x2a \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2b s \<and> x2b \<noteq> r)
 2. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (clarsimp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref field option x2 x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2; obj_fields x2 field = Some x2a; marked x2a s\<rbrakk> \<Longrightarrow> (obj_fields x2b field = None \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r) \<and> (\<forall>x2a. obj_fields x2b field = Some x2a \<longrightarrow> x2 = x2b \<longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> marked x2a s \<and> x2a \<noteq> r))
[PROOF STEP]
apply (rule conjI; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<and> (ref \<noteq> r \<longrightarrow> x2a \<noteq> r)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r
 2. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
apply (clarsimp simp: mut_m.reachable_snapshot_inv_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>field option x2a x2b. \<lbrakk>\<forall>x. mut_m.reachable m x s \<longrightarrow> in_snapshot x s; no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
apply (drule spec[where x=r], clarsimp simp: in_snapshot_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>field option x2a x2b. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2b; marked x2a s; obj_fields x2b field = Some x2a; mut_m.reachable m r s \<longrightarrow> black r s \<or> (\<exists>x. (x grey_protects_white r) s)\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
apply (drule mp, auto simp: mut_m.reachable_def mut_m.tso_store_refs_def split: mem_store_action.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>field option x2a x2b x. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2b; marked x2a s; obj_fields x2b field = Some x2a; (x grey_protects_white r) s\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
(* FIXME rule *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>field option x2a x2b x. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2b; marked x2a s; obj_fields x2b field = Some x2a; (x grey_protects_white r) s\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
apply (drule grey_protects_whiteD)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>field option x2a x2b x. \<lbrakk>no_grey_refs s; white r s; mw_Mutate r field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s r = Some x2b; marked x2a s; obj_fields x2b field = Some x2a; grey x s \<and> (x = r \<or> white r s)\<rbrakk> \<Longrightarrow> False
 2. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
apply (clarsimp simp: no_grey_refs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; white r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
unfolding white_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ref field option x2a x2b. \<lbrakk>mut_m.reachable_snapshot_inv m s; no_grey_refs s; obj_at (\<lambda>obj. obj_mark obj \<noteq> sys_fM s) r s; mw_Mutate ref field option \<in> set (sys_mem_store_buffers (mutator m) s); sys_heap s ref = Some x2b; marked x2a s; obj_fields x2b field = Some x2a\<rbrakk> \<Longrightarrow> ref \<noteq> r \<longrightarrow> x2a \<noteq> r
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma LIMSEQ_squeeze:
  assumes abc: "\<forall>n. a n \<le> b n \<and> b n \<le> c n"
  and alim: "a \<longlonglongrightarrow> (L::real)"
  and clim: "c \<longlonglongrightarrow> L" shows "b \<longlonglongrightarrow> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
assume r0: "(r::real) > 0"
[PROOF STATE]
proof (state)
this:
0 < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < r
[PROOF STEP]
have "\<exists>no. \<forall>n\<ge>no. \<bar>a n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
0 < r

goal (1 subgoal):
 1. \<exists>no. \<forall>n\<ge>no. \<bar>a n - L\<bar> < r
[PROOF STEP]
by (metis LIMSEQ_def alim dist_real_def)
[PROOF STATE]
proof (state)
this:
\<exists>no. \<forall>n\<ge>no. \<bar>a n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>no. \<forall>n\<ge>no. \<bar>a n - L\<bar> < r
[PROOF STEP]
obtain p where 1: "\<forall>n\<ge>p. \<bar>a n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
\<exists>no. \<forall>n\<ge>no. \<bar>a n - L\<bar> < r

goal (1 subgoal):
 1. (\<And>p. \<forall>n\<ge>p. \<bar>a n - L\<bar> < r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>p. \<bar>a n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
have "\<exists>no. \<forall>n\<ge>no. \<bar>c n - L\<bar> < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>no. \<forall>n\<ge>no. \<bar>c n - L\<bar> < r
[PROOF STEP]
by (metis LIMSEQ_def r0 clim dist_real_def)
[PROOF STATE]
proof (state)
this:
\<exists>no. \<forall>n\<ge>no. \<bar>c n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>no. \<forall>n\<ge>no. \<bar>c n - L\<bar> < r
[PROOF STEP]
obtain k where 2: "\<forall>n\<ge>k. \<bar>c n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
\<exists>no. \<forall>n\<ge>no. \<bar>c n - L\<bar> < r

goal (1 subgoal):
 1. (\<And>k. \<forall>n\<ge>k. \<bar>c n - L\<bar> < r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>k. \<bar>c n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
have  "\<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
assume n_max: "max p k \<le> n"
[PROOF STATE]
proof (state)
this:
max p k \<le> n

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max p k \<le> n
[PROOF STEP]
have a_n: "\<bar>a n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
max p k \<le> n

goal (1 subgoal):
 1. \<bar>a n - L\<bar> < r
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
max p k \<le> n
\<forall>n\<ge>p. \<bar>a n - L\<bar> < r

goal (1 subgoal):
 1. \<bar>a n - L\<bar> < r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>a n - L\<bar> < r

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
have c_n: "\<bar>c n - L\<bar> < r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>c n - L\<bar> < r
[PROOF STEP]
using n_max 2
[PROOF STATE]
proof (prove)
using this:
max p k \<le> n
\<forall>n\<ge>k. \<bar>c n - L\<bar> < r

goal (1 subgoal):
 1. \<bar>c n - L\<bar> < r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>c n - L\<bar> < r

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
have "a n \<le> b n \<and> b n \<le> c n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a n \<le> b n \<and> b n \<le> c n
[PROOF STEP]
using abc
[PROOF STATE]
proof (prove)
using this:
\<forall>n. a n \<le> b n \<and> b n \<le> c n

goal (1 subgoal):
 1. a n \<le> b n \<and> b n \<le> c n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a n \<le> b n \<and> b n \<le> c n

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a n \<le> b n \<and> b n \<le> c n
[PROOF STEP]
have "\<bar>b n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
a n \<le> b n \<and> b n \<le> c n

goal (1 subgoal):
 1. \<bar>b n - L\<bar> < r
[PROOF STEP]
using a_n c_n
[PROOF STATE]
proof (prove)
using this:
a n \<le> b n \<and> b n \<le> c n
\<bar>a n - L\<bar> < r
\<bar>c n - L\<bar> < r

goal (1 subgoal):
 1. \<bar>b n - L\<bar> < r
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<bar>b n - L\<bar> < r

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
max p k \<le> ?n2 \<Longrightarrow> \<bar>b ?n2 - L\<bar> < r

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
max p k \<le> ?n2 \<Longrightarrow> \<bar>b ?n2 - L\<bar> < r
[PROOF STEP]
have "\<forall>n\<ge>max p k. \<bar>b n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
max p k \<le> ?n2 \<Longrightarrow> \<bar>b ?n2 - L\<bar> < r

goal (1 subgoal):
 1. \<forall>n\<ge>max p k. \<bar>b n - L\<bar> < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>max p k. \<bar>b n - L\<bar> < r

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<ge>max p k. \<bar>b n - L\<bar> < r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>max p k. \<bar>b n - L\<bar> < r

goal (1 subgoal):
 1. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < ?r2 \<Longrightarrow> \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < ?r2

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < ?r2 \<Longrightarrow> \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < ?r2
[PROOF STEP]
have "\<forall>r>0. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r"
[PROOF STATE]
proof (prove)
using this:
0 < ?r2 \<Longrightarrow> \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < ?r2

goal (1 subgoal):
 1. \<forall>r>0. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>r>0. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>r>0. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>r>0. \<exists>m. \<forall>n\<ge>m. \<bar>b n - L\<bar> < r

goal (1 subgoal):
 1. b \<longlonglongrightarrow> L
[PROOF STEP]
by (simp add: dist_real_def lim_sequentially)
[PROOF STATE]
proof (state)
this:
b \<longlonglongrightarrow> L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma flip_eq:
  fixes x::x and xa::x and s::"'a::fs" and sa::"'a::fs"
  assumes "(\<forall>c. atom c \<sharp> (s, sa) \<longrightarrow> atom c \<sharp> (x, xa, s, sa) \<longrightarrow> (x \<leftrightarrow> c) \<bullet> s = (xa \<leftrightarrow> c) \<bullet> sa)" and "x \<noteq> xa"
  shows "(x \<leftrightarrow> xa) \<bullet> s = sa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<leftrightarrow> xa) \<bullet> s = sa
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (x \<leftrightarrow> xa) \<bullet> s = sa
[PROOF STEP]
have  " ([[atom x]]lst. s = [[atom xa]]lst. sa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[atom x]]lst. s = [[atom xa]]lst. sa
[PROOF STEP]
using assms Abs1_eq_iff_all
[PROOF STATE]
proof (prove)
using this:
\<forall>c. atom c \<sharp> (s, sa) \<longrightarrow> atom c \<sharp> (x, xa, s, sa) \<longrightarrow> (x \<leftrightarrow> c) \<bullet> s = (xa \<leftrightarrow> c) \<bullet> sa
x \<noteq> xa
([{atom ?a}]set. ?x = [{atom ?b}]set. ?y) = (\<forall>c. atom c \<sharp> ?z \<longrightarrow> atom c \<sharp> (?a, ?b, ?x, ?y) \<longrightarrow> (?a \<leftrightarrow> c) \<bullet> ?x = (?b \<leftrightarrow> c) \<bullet> ?y)
([{atom ?a}]res. ?x = [{atom ?b}]res. ?y) = (\<forall>c. atom c \<sharp> ?z \<longrightarrow> atom c \<sharp> (?a, ?b, ?x, ?y) \<longrightarrow> (?a \<leftrightarrow> c) \<bullet> ?x = (?b \<leftrightarrow> c) \<bullet> ?y)
([[atom ?a]]lst. ?x = [[atom ?b]]lst. ?y) = (\<forall>c. atom c \<sharp> ?z \<longrightarrow> atom c \<sharp> (?a, ?b, ?x, ?y) \<longrightarrow> (?a \<leftrightarrow> c) \<bullet> ?x = (?b \<leftrightarrow> c) \<bullet> ?y)

goal (1 subgoal):
 1. [[atom x]]lst. s = [[atom xa]]lst. sa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[[atom x]]lst. s = [[atom xa]]lst. sa

goal (1 subgoal):
 1. (x \<leftrightarrow> xa) \<bullet> s = sa
[PROOF STEP]
hence  "(xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s)"
[PROOF STATE]
proof (prove)
using this:
[[atom x]]lst. s = [[atom xa]]lst. sa

goal (1 subgoal):
 1. xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s
[PROOF STEP]
using assms Abs1_eq_iff[of xa sa x s]
[PROOF STATE]
proof (prove)
using this:
[[atom x]]lst. s = [[atom xa]]lst. sa
\<forall>c. atom c \<sharp> (s, sa) \<longrightarrow> atom c \<sharp> (x, xa, s, sa) \<longrightarrow> (x \<leftrightarrow> c) \<bullet> s = (xa \<leftrightarrow> c) \<bullet> sa
x \<noteq> xa
([{atom xa}]set. sa = [{atom x}]set. s) = (xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s)
([{atom xa}]res. sa = [{atom x}]res. s) = (xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s)
([[atom xa]]lst. sa = [[atom x]]lst. s) = (xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s)

goal (1 subgoal):
 1. xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s

goal (1 subgoal):
 1. (x \<leftrightarrow> xa) \<bullet> s = sa
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s

goal (1 subgoal):
 1. (x \<leftrightarrow> xa) \<bullet> s = sa
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xa = x \<and> sa = s \<or> xa \<noteq> x \<and> sa = (xa \<leftrightarrow> x) \<bullet> s \<and> atom xa \<sharp> s
\<forall>c. atom c \<sharp> (s, sa) \<longrightarrow> atom c \<sharp> (x, xa, s, sa) \<longrightarrow> (x \<leftrightarrow> c) \<bullet> s = (xa \<leftrightarrow> c) \<bullet> sa
x \<noteq> xa

goal (1 subgoal):
 1. (x \<leftrightarrow> xa) \<bullet> s = sa
[PROOF STEP]
by (metis flip_commute)
[PROOF STATE]
proof (state)
this:
(x \<leftrightarrow> xa) \<bullet> s = sa

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dom_supp_g[simp]:
  "atom_dom G \<subseteq> supp G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom_dom G \<subseteq> supp G
[PROOF STEP]
apply(induct G rule: \<Gamma>_induct,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. atom_dom \<Gamma>' \<subseteq> supp \<Gamma>' \<Longrightarrow> atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> supp ((x, b, c) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
using supp_at_base supp_Pair atom_dom.simps supp_GCons
[PROOF STATE]
proof (prove)
using this:
supp ?a = {atom ?a}
supp (?x, ?y) = supp ?x \<union> supp ?y
atom_dom ?\<Gamma> = atom ` Syntax.dom ?\<Gamma>
supp (?x #\<^sub>\<Gamma> ?xs) = supp ?x \<union> supp ?xs

goal (1 subgoal):
 1. \<And>x b c \<Gamma>'. atom_dom \<Gamma>' \<subseteq> supp \<Gamma>' \<Longrightarrow> atom_dom ((x, b, c) #\<^sub>\<Gamma> \<Gamma>') \<subseteq> supp ((x, b, c) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
by fastforce


[STATEMENT]
lemma fresh_dom_free2:
  assumes "atom x \<notin> atom_dom \<Gamma>"
  shows "(x,b,c) \<notin> toSet \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, b, c) \<notin> toSet \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom x \<notin> atom_dom \<Gamma>

goal (1 subgoal):
 1. (x, b, c) \<notin> toSet \<Gamma>
[PROOF STEP]
proof(induct \<Gamma> rule: \<Gamma>_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. atom x \<notin> atom_dom GNil \<Longrightarrow> (x, b, c) \<notin> toSet GNil
 2. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
case GNil
[PROOF STATE]
proof (state)
this:
atom x \<notin> atom_dom GNil

goal (2 subgoals):
 1. atom x \<notin> atom_dom GNil \<Longrightarrow> (x, b, c) \<notin> toSet GNil
 2. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<notin> atom_dom GNil
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<notin> atom_dom GNil

goal (1 subgoal):
 1. (x, b, c) \<notin> toSet GNil
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, b, c) \<notin> toSet GNil

goal (1 subgoal):
 1. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
case (GCons x' b' c' \<Gamma>')
[PROOF STATE]
proof (state)
this:
atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'
atom x \<notin> atom_dom ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')

goal (1 subgoal):
 1. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
hence "x\<noteq>x'"
[PROOF STATE]
proof (prove)
using this:
atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'
atom x \<notin> atom_dom ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')

goal (1 subgoal):
 1. x \<noteq> x'
[PROOF STEP]
using fresh_def fresh_GCons fresh_Pair supp_at_base
[PROOF STATE]
proof (prove)
using this:
atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'
atom x \<notin> atom_dom ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')
?a \<sharp> ?x \<equiv> ?a \<notin> supp ?x
?a \<sharp> ?x #\<^sub>\<Gamma> ?xs = (?a \<sharp> ?x \<and> ?a \<sharp> ?xs)
?a \<sharp> (?x, ?y) = (?a \<sharp> ?x \<and> ?a \<sharp> ?y)
supp ?a = {atom ?a}

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

goal (1 subgoal):
 1. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<noteq> x'

goal (1 subgoal):
 1. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
have "atom x \<notin> atom_dom \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<notin> atom_dom \<Gamma>'
[PROOF STEP]
using fresh_GCons GCons
[PROOF STATE]
proof (prove)
using this:
?a \<sharp> ?x #\<^sub>\<Gamma> ?xs = (?a \<sharp> ?x \<and> ?a \<sharp> ?xs)
atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'
atom x \<notin> atom_dom ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')

goal (1 subgoal):
 1. atom x \<notin> atom_dom \<Gamma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<notin> atom_dom \<Gamma>'

goal (1 subgoal):
 1. \<And>xa ba ca \<Gamma>'. \<lbrakk>atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'; atom x \<notin> atom_dom ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')\<rbrakk> \<Longrightarrow> (x, b, c) \<notin> toSet ((xa, ba, ca) #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> x'
atom x \<notin> atom_dom \<Gamma>'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x'
atom x \<notin> atom_dom \<Gamma>'

goal (1 subgoal):
 1. (x, b, c) \<notin> toSet ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
using toSet.simps GCons
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x'
atom x \<notin> atom_dom \<Gamma>'
toSet GNil = {}
toSet (?xbc #\<^sub>\<Gamma> ?G) = {?xbc} \<union> toSet ?G
atom x \<notin> atom_dom \<Gamma>' \<Longrightarrow> (x, b, c) \<notin> toSet \<Gamma>'
atom x \<notin> atom_dom ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')

goal (1 subgoal):
 1. (x, b, c) \<notin> toSet ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, b, c) \<notin> toSet ((x', b', c') #\<^sub>\<Gamma> \<Gamma>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_Dummy_inj[simp]: "map Dummy l = map Dummy l' \<longleftrightarrow> l = l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map Dummy l = map Dummy l') = (l = l')
[PROOF STEP]
apply (induction l arbitrary: l')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l'. (map Dummy [] = map Dummy l') = ([] = l')
 2. \<And>a l l'. (\<And>l'. (map Dummy l = map Dummy l') = (l = l')) \<Longrightarrow> (map Dummy (a # l) = map Dummy l') = (a # l = l')
[PROOF STEP]
apply (case_tac [!] l')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>l'. l' = [] \<Longrightarrow> (map Dummy [] = map Dummy l') = ([] = l')
 2. \<And>l' a list. l' = a # list \<Longrightarrow> (map Dummy [] = map Dummy l') = ([] = l')
 3. \<And>a l l'. \<lbrakk>\<And>l'. (map Dummy l = map Dummy l') = (l = l'); l' = []\<rbrakk> \<Longrightarrow> (map Dummy (a # l) = map Dummy l') = (a # l = l')
 4. \<And>a l l' aa list. \<lbrakk>\<And>l'. (map Dummy l = map Dummy l') = (l = l'); l' = aa # list\<rbrakk> \<Longrightarrow> (map Dummy (a # l) = map Dummy l') = (a # l = l')
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heap_upds_ok_Nil[simp]: "heap_upds_ok (\<Gamma>, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap_upds_ok (\<Gamma>, [])
[PROOF STEP]
by auto


[STATEMENT]
lemma  adapt_sigma_sets:
assumes "\<And>i. i \<le> n\<Longrightarrow> (X i) \<in> measurable M N"
shows "sigma_algebra (space M) (sigma_sets (space M) (\<Union>i\<in>{m. m \<le> n}. {X i -` A \<inter> space M |A. A \<in> sets N}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sigma_algebra (space M) (sigma_sets (space M) (\<Union>i\<in>{m. m \<le> n}. {X i -` A \<inter> space M |A. A \<in> sets N}))
[PROOF STEP]
proof (rule sigma_algebra_sigma_sets)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Union>i\<in>{m. m \<le> n}. {X i -` A \<inter> space M |A. A \<in> sets N}) \<subseteq> Pow (space M)
[PROOF STEP]
show "(\<Union>i\<in>{m. m \<le> n}. {X i -` A \<inter> space M |A. A \<in> sets N}) \<subseteq> Pow (space M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{m. m \<le> n}. {X i -` A \<inter> space M |A. A \<in> sets N}) \<subseteq> Pow (space M)
[PROOF STEP]
proof (rule UN_subset_iff[THEN iffD2], intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {m. m \<le> n} \<Longrightarrow> {X i -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in> {m. m \<le> n} \<Longrightarrow> {X i -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)
[PROOF STEP]
assume "i \<in> {m. m\<le> n}"
[PROOF STATE]
proof (state)
this:
i \<in> {m. m \<le> n}

goal (1 subgoal):
 1. \<And>i. i \<in> {m. m \<le> n} \<Longrightarrow> {X i -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)
[PROOF STEP]
show "{X i -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {X i -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{X i -` A \<inter> space M |A. A \<in> sets N} \<subseteq> Pow (space M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{m. m \<le> n}. {X i -` A \<inter> space M |A. A \<in> sets N}) \<subseteq> Pow (space M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma circ_simulate_3:
  "y * x\<^sup>\<circ> \<le> x\<^sup>\<circ> \<Longrightarrow> y\<^sup>\<circ> * x\<^sup>\<circ> \<le> x\<^sup>\<circ> * y\<^sup>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * x\<^sup>\<circ> \<le> x\<^sup>\<circ> \<Longrightarrow> y\<^sup>\<circ> * x\<^sup>\<circ> \<le> x\<^sup>\<circ> * y\<^sup>\<circ>
[PROOF STEP]
by (metis sup.bounded_iff circ_reflexive circ_simulate_2 le_iff_sup mult_right_isotone mult_1_right)


[STATEMENT]
lemma set_bit_integer_conv_masks:
  fixes x :: integer shows
  "set_bit x i b = (if b then x OR (push_bit i 1) else x AND NOT (push_bit i 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_bit_class.set_bit x i b = (if b then x OR push_bit i 1 else x AND NOT (push_bit i 1))
[PROOF STEP]
by (transfer; rule bit_eqI) (simp add: bit_simps)


[STATEMENT]
lemma shift_one:
"shift (Suc 0) = poly_shift"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. shift (Suc 0) = poly_shift
[PROOF STEP]
by auto


[STATEMENT]
lemma \<L>_eps_free_parallel_closure_reg:
  assumes "is_ta_eps_free (ta \<A>)"
  shows "\<L> (ftrancl_eps_free_reg (parallel_closure_reg \<F> \<A>)) = \<L> (parallel_closure_reg \<F> \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<L> (ftrancl_eps_free_reg (parallel_closure_reg \<F> \<A>)) = \<L> (parallel_closure_reg \<F> \<A>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<L> (ftrancl_eps_free_reg (parallel_closure_reg \<F> \<A>)) = \<L> (parallel_closure_reg \<F> \<A>)
[PROOF STEP]
have "eps (ta (parallel_closure_reg \<F> \<A>)) |O| eps (ta (parallel_closure_reg \<F> \<A>)) = {||}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eps (ta (parallel_closure_reg \<F> \<A>)) |O| eps (ta (parallel_closure_reg \<F> \<A>)) = {||}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_ta_eps_free (ta \<A>)

goal (1 subgoal):
 1. eps (ta (parallel_closure_reg \<F> \<A>)) |O| eps (ta (parallel_closure_reg \<F> \<A>)) = {||}
[PROOF STEP]
by (auto simp: parallel_closure_reg_def gen_parallel_closure_automaton_def Let_def ta_union_def
      refl_over_states_ta_def fmap_states_reg_def is_ta_eps_free_def fmap_states_ta_def reg_Restr_Q\<^sub>f_def)
[PROOF STATE]
proof (state)
this:
eps (ta (parallel_closure_reg \<F> \<A>)) |O| eps (ta (parallel_closure_reg \<F> \<A>)) = {||}

goal (1 subgoal):
 1. \<L> (ftrancl_eps_free_reg (parallel_closure_reg \<F> \<A>)) = \<L> (parallel_closure_reg \<F> \<A>)
[PROOF STEP]
from frelcomp_empty_ftrancl_simp[OF this]
[PROOF STATE]
proof (chain)
picking this:
(eps (ta (parallel_closure_reg \<F> \<A>)))|\<^sup>+| = eps (ta (parallel_closure_reg \<F> \<A>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(eps (ta (parallel_closure_reg \<F> \<A>)))|\<^sup>+| = eps (ta (parallel_closure_reg \<F> \<A>))

goal (1 subgoal):
 1. \<L> (ftrancl_eps_free_reg (parallel_closure_reg \<F> \<A>)) = \<L> (parallel_closure_reg \<F> \<A>)
[PROOF STEP]
by (intro \<L>_ftrancl_eps_free_closuresI) simp
[PROOF STATE]
proof (state)
this:
\<L> (ftrancl_eps_free_reg (parallel_closure_reg \<F> \<A>)) = \<L> (parallel_closure_reg \<F> \<A>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sqn_update_another [simp]:
    fixes dip ip rt dsn dsk flag hops nhip
  assumes "ip \<noteq> dip"
    shows "sqn (update rt dip (dsn, dsk, flag, hops, nhip)) ip = sqn rt ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqn (update rt dip (dsn, dsk, flag, hops, nhip)) ip = sqn rt ip
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ip \<noteq> dip

goal (1 subgoal):
 1. sqn (update rt dip (dsn, dsk, flag, hops, nhip)) ip = sqn rt ip
[PROOF STEP]
unfolding update_def sqn_def
[PROOF STATE]
proof (prove)
using this:
ip \<noteq> dip

goal (1 subgoal):
 1. (case (case rt dip of None \<Rightarrow> rt(dip \<mapsto> (dsn, dsk, flag, hops, nhip)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip) then rt(dip \<mapsto> (dsn, dsk, flag, hops, nhip)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip) \<and> (\<pi>\<^sub>5 (dsn, dsk, flag, hops, nhip) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(dip \<mapsto> (dsn, dsk, flag, hops, nhip)) else if \<pi>\<^sub>3 (dsn, dsk, flag, hops, nhip) = unk then rt(dip \<mapsto> (\<pi>\<^sub>2 s, snd (dsn, dsk, flag, hops, nhip))) else rt(dip \<mapsto> s)) ip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r) = (case rt ip of None \<Rightarrow> 0 | Some r \<Rightarrow> \<pi>\<^sub>2 r)
[PROOF STEP]
by (clarsimp split: option.splits) auto


[STATEMENT]
lemma sqnf_update_another [simp]:
    fixes dip ip rt dsn dsk flag hops nhip
  assumes "ip \<noteq> dip"
    shows "sqnf (update rt dip (dsn, dsk, flag, hops, nhip)) ip = sqnf rt ip"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqnf (update rt dip (dsn, dsk, flag, hops, nhip)) ip = sqnf rt ip
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ip \<noteq> dip

goal (1 subgoal):
 1. sqnf (update rt dip (dsn, dsk, flag, hops, nhip)) ip = sqnf rt ip
[PROOF STEP]
unfolding update_def sqnf_def
[PROOF STATE]
proof (prove)
using this:
ip \<noteq> dip

goal (1 subgoal):
 1. (case (case rt dip of None \<Rightarrow> rt(dip \<mapsto> (dsn, dsk, flag, hops, nhip)) | Some s \<Rightarrow> if \<pi>\<^sub>2 s < \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip) then rt(dip \<mapsto> (dsn, dsk, flag, hops, nhip)) else if \<pi>\<^sub>2 s = \<pi>\<^sub>2 (dsn, dsk, flag, hops, nhip) \<and> (\<pi>\<^sub>5 (dsn, dsk, flag, hops, nhip) < \<pi>\<^sub>5 s \<or> \<pi>\<^sub>4 s = Aodv_Basic.inv) then rt(dip \<mapsto> (dsn, dsk, flag, hops, nhip)) else if \<pi>\<^sub>3 (dsn, dsk, flag, hops, nhip) = unk then rt(dip \<mapsto> (\<pi>\<^sub>2 s, snd (dsn, dsk, flag, hops, nhip))) else rt(dip \<mapsto> s)) ip of None \<Rightarrow> unk | Some r \<Rightarrow> \<pi>\<^sub>3 r) = (case rt ip of None \<Rightarrow> unk | Some r \<Rightarrow> \<pi>\<^sub>3 r)
[PROOF STEP]
by (clarsimp split: option.splits) auto


[STATEMENT]
lemma [simp]: "a \<notin> scf R12"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> scf R12
[PROOF STEP]
by (rule pareto_efficiency) (simp_all add: eval_pareto R12.eval)


[STATEMENT]
lemma zero_case_rec_exec[simp]:
  "\<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk>
  \<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)
  [ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] =
  0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk> \<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] = 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything
[PROOF STEP]
using list_update_append[of "rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)"
      "0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything" "ft + n - length xs" "rec_exec (gs ! n) xs"]
[PROOF STATE]
proof (prove)
using this:
((rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[ft + n - length xs := rec_exec (gs ! n) xs] = (if ft + n - length xs < length (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)) then (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs))[ft + n - length xs := rec_exec (gs ! n) xs] @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything else (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)) @ (0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[ft + n - length xs - length (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs)) := rec_exec (gs ! n) xs])

goal (1 subgoal):
 1. \<lbrakk>length xs < gf; gf \<le> ft; n < length gs\<rbrakk> \<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[ft + n - length xs := rec_exec (gs ! n) xs, 0 := 0] = 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs < gf; gf \<le> ft; n < length gs; (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[ft + n - length xs := rec_exec (gs ! n) xs] = rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ (0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[0 := rec_exec (gs ! n) xs]; \<not> ft + n - length xs < Suc (ft + n - Suc (length xs))\<rbrakk> \<Longrightarrow> (rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ (0 \<up> (length gs - n) @ 0 # 0 \<up> length xs @ anything)[0 := rec_exec (gs ! n) xs])[0 := 0] = 0 \<up> (ft - length xs) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 # 0 \<up> length xs @ anything
[PROOF STEP]
apply(cases "length gs - n", simp, simp add: list_update.simps replicate_Suc_iff_anywhere Suc_diff_Suc del: replicate_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>length xs < gf; gf \<le> ft; n < length gs; (case ft + n - length xs of 0 \<Rightarrow> rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> Suc nat @ 0 \<up> Suc (length xs) @ anything | Suc j \<Rightarrow> rec_exec (gs ! n) xs # (0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ 0 \<up> Suc nat @ 0 \<up> Suc (length xs) @ anything)[j := rec_exec (gs ! n) xs]) = rec_exec (gs ! n) xs # 0 \<up> (ft - Suc (length xs)) @ map (\<lambda>i. rec_exec i xs) (take n gs) @ (0 \<up> Suc nat @ 0 \<up> Suc (length xs) @ anything)[0 := rec_exec (gs ! n) xs]; length gs - n = Suc nat\<rbrakk> \<Longrightarrow> (0 \<up> Suc nat @ 0 \<up> Suc (length xs) @ anything)[0 := rec_exec (gs ! n) xs] = rec_exec (gs ! n) xs # 0 \<up> (length gs - Suc n) @ 0 \<up> Suc (length xs) @ anything
[PROOF STEP]
apply(simp add: list_update.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma in_hom_char:
    shows "in_hom f a b \<longleftrightarrow> arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_hom f a b = (arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. in_hom f a b \<Longrightarrow> arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b
 2. arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b \<Longrightarrow> in_hom f a b
[PROOF STEP]
show "in_hom f a b \<Longrightarrow> arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_hom f a b \<Longrightarrow> arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b
[PROOF STEP]
using arr_char dom_char cod_char
[PROOF STATE]
proof (prove)
using this:
arr ?f = (?f \<noteq> Null \<and> Dom ?f \<in> Obj \<and> Cod ?f \<in> Obj \<and> Map ?f \<in> Hom (Dom ?f) (Cod ?f))
local.dom ?f = (if arr ?f then MkIde (Dom ?f) else null)
cod ?f = (if arr ?f then MkIde (Cod ?f) else null)

goal (1 subgoal):
 1. in_hom f a b \<Longrightarrow> arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
in_hom f a b \<Longrightarrow> arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b

goal (1 subgoal):
 1. arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b \<Longrightarrow> in_hom f a b
[PROOF STEP]
show "arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b \<Longrightarrow> in_hom f a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b \<Longrightarrow> in_hom f a b
[PROOF STEP]
using arr_char dom_char cod_char ide_char Id_in_Hom MkArr_Map in_homI
[PROOF STATE]
proof (prove)
using this:
arr ?f = (?f \<noteq> Null \<and> Dom ?f \<in> Obj \<and> Cod ?f \<in> Obj \<and> Map ?f \<in> Hom (Dom ?f) (Cod ?f))
local.dom ?f = (if arr ?f then MkIde (Dom ?f) else null)
cod ?f = (if arr ?f then MkIde (Cod ?f) else null)
ide ?a = (arr ?a \<and> local.dom ?a = ?a \<and> cod ?a = ?a)
?A \<in> Obj \<Longrightarrow> Id ?A \<in> Hom ?A ?A
arr ?f \<Longrightarrow> MkArr (Dom ?f) (Cod ?f) (Map ?f) = ?f
\<lbrakk>arr ?f; local.dom ?f = ?a; cod ?f = ?b\<rbrakk> \<Longrightarrow> in_hom ?f ?a ?b

goal (1 subgoal):
 1. arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b \<Longrightarrow> in_hom f a b
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
arr f \<and> ide a \<and> ide b \<and> Dom f = Dom a \<and> Cod f = Dom b \<Longrightarrow> in_hom f a b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma good_context_4 :
"good_context (s::(('a::len) sparc_state)) \<and>
 s'' = delayed_pool_write s \<and>
 fetch_instruction s'' = Inr v1 \<and>
 ((decode_instruction v1)::(Exception list + instruction)) = Inr v2 \<and>
 annul_val s'' = False \<and>
 supported_instruction (fst v2) = True \<and> \<comment> \<open>This line is redundant\<close>
 (fst v2) = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and>
 (((get_S (cpu_reg_val PSR s'')))::word1) = 0
 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False
[PROOF STEP]
assume asm: "good_context (s::(('a::len) sparc_state)) \<and>
  s'' = delayed_pool_write s \<and>
  fetch_instruction s'' = Inr v1 \<and>
  ((decode_instruction v1)::(Exception list + instruction)) = Inr v2 \<and>
  annul_val s'' = False \<and>
  supported_instruction (fst v2) = True \<and> \<comment> \<open>This line is redundant\<close>
  (fst v2) = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and>
  (((get_S (cpu_reg_val PSR s'')))::word1) = 0"
[PROOF STATE]
proof (state)
this:
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0

goal (1 subgoal):
 1. good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0
[PROOF STEP]
have "(fst v2) = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and>
  (((get_S (cpu_reg_val PSR s'')))::word1) = 0 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0

goal (1 subgoal):
 1. fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False
[PROOF STEP]
proof (cases "(get_trap_set s) \<noteq> {} \<and> (reset_trap_val s) = False \<and>
      get_ET (cpu_reg_val PSR s) = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; \<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0

goal (2 subgoals):
 1. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; \<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from this asm
[PROOF STATE]
proof (chain)
picking this:
get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using good_context_1
[PROOF STATE]
proof (prove)
using this:
get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0
good_context ?s \<and> ?s' = ?s \<and> get_trap_set ?s' \<noteq> {} \<and> reset_trap_val ?s' = False \<and> get_ET (cpu_reg_val PSR ?s') = 0 \<Longrightarrow> False

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

goal (1 subgoal):
 1. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; \<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; \<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)

goal (1 subgoal):
 1. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; \<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)
[PROOF STEP]
have fact3: "(get_trap_set s) = {} \<or> (reset_trap_val s) \<noteq> False \<or>
      get_ET (cpu_reg_val PSR s) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)

goal (1 subgoal):
 1. get_trap_set s = {} \<or> reset_trap_val s \<noteq> False \<or> get_ET (cpu_reg_val PSR s) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_trap_set s = {} \<or> reset_trap_val s \<noteq> False \<or> get_ET (cpu_reg_val PSR s) \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0; \<not> (get_trap_set s \<noteq> {} \<and> reset_trap_val s = False \<and> get_ET (cpu_reg_val PSR s) = 0)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
get_trap_set s = {} \<or> reset_trap_val s \<noteq> False \<or> get_ET (cpu_reg_val PSR s) \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
get_trap_set s = {} \<or> reset_trap_val s \<noteq> False \<or> get_ET (cpu_reg_val PSR s) \<noteq> 0
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0 \<Longrightarrow> False
good_context s \<and> s'' = delayed_pool_write s \<and> fetch_instruction s'' = Inr v1 \<and> decode_instruction v1 = Inr v2 \<and> annul_val s'' = False \<and> supported_instruction (fst v2) = True \<and> fst v2 = ctrl_type RETT \<and> get_ET (cpu_reg_val PSR s'') \<noteq> 1 \<and> get_S (cpu_reg_val PSR s'') = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stop_cxt :
  "\<lbrakk> \<turnstile> \<Gamma>,\<S>,P { c } \<Gamma>',\<S>',P' ; c = Stop \<rbrakk> \<Longrightarrow>
  context_equiv \<Gamma> P \<Gamma>' \<and> \<S>' = \<S> \<and> P \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<turnstile> \<Gamma>,\<S>,P {c} \<Gamma>',\<S>',P'; c = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma>' \<and> \<S>' = \<S> \<and> P \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S> P')
[PROOF STEP]
apply (induct rule: has_type.induct)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>\<Gamma> \<S> P. Stop = Stop \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma> \<and> \<S> = \<S> \<and> P \<turnstile> P \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma> \<S> P)
 2. \<And>\<Gamma> \<S> P. Skip = Stop \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma> \<and> \<S> = \<S> \<and> P \<turnstile> P \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma> \<S> P)
 3. \<And>x \<Gamma> e t P P' \<S>. \<lbrakk>x \<in> \<C>; \<Gamma> \<turnstile>\<^sub>a e \<in> t; P \<turnstile> t; \<forall>v\<in>dom \<Gamma>. x \<notin> vars_of_type (the (\<Gamma> v)); P' = assign_post P x e |` {v. local.stable \<S> v}; \<forall>v. x \<in> \<C>_vars v \<and> v \<notin> snd \<S> \<longrightarrow> P \<turnstile> to_total \<Gamma> v \<and> to_total \<Gamma> v \<le>:\<^sub>P' dma_type v; x \<leftarrow> e = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma> \<and> \<S> = \<S> \<and> P \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma> \<S> P')
 4. \<And>x \<Gamma> e t P P' \<S>. \<lbrakk>x \<notin> dom \<Gamma>; x \<notin> \<C>; \<Gamma> \<turnstile>\<^sub>a e \<in> t; t \<le>:\<^sub>P dma_type x; P' = assign_post P x e |` {v. local.stable \<S> v}; x \<leftarrow> e = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma> \<and> \<S> = \<S> \<and> P \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma> \<S> P')
 5. \<And>x \<Gamma> e t \<S> P' P. \<lbrakk>x \<in> dom \<Gamma>; \<Gamma> \<turnstile>\<^sub>a e \<in> t; type_stable \<S> t; P' = assign_post P x e |` {v. local.stable \<S> v}; x \<notin> snd \<S> \<longrightarrow> t \<le>:\<^sub>P' dma_type x; x \<leftarrow> e = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma>(x \<mapsto> t) \<and> \<S> = \<S> \<and> P \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds (\<Gamma>(x \<mapsto> t)) \<S> P')
 6. \<And>\<Gamma> e t P \<S> c\<^sub>1 \<Gamma>' \<S>' P' c\<^sub>2 \<Gamma>'' P'' \<Gamma>''' P'''. \<lbrakk>\<Gamma> \<turnstile>\<^sub>b e \<in> t ; P \<turnstile> t; \<turnstile> \<Gamma>,\<S>,P +\<^sub>\<S> e {c\<^sub>1} \<Gamma>',\<S>',P'; c\<^sub>1 = Stop \<Longrightarrow> \<Gamma> =:\<^sub>P +\<^sub>\<S> e \<Gamma>' \<and> \<S>' = \<S> \<and> P +\<^sub>\<S> e \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P +\<^sub>\<S> e \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S> P'); \<turnstile> \<Gamma>,\<S>,P +\<^sub>\<S> bexp_neg e {c\<^sub>2} \<Gamma>'',\<S>',P''; c\<^sub>2 = Stop \<Longrightarrow> \<Gamma> =:\<^sub>P +\<^sub>\<S> bexp_neg e \<Gamma>'' \<and> \<S>' = \<S> \<and> P +\<^sub>\<S> bexp_neg e \<turnstile> P'' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P +\<^sub>\<S> bexp_neg e \<longrightarrow> tyenv_wellformed mds \<Gamma>'' \<S> P''); \<Gamma>' =:\<^sub>P' \<Gamma>'''; \<Gamma>'' =:\<^sub>P'' \<Gamma>'''; P' \<turnstile> P'''; P'' \<turnstile> P'''; \<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P' \<longrightarrow> tyenv_wellformed mds \<Gamma>''' \<S>' P'''; \<forall>mds. tyenv_wellformed mds \<Gamma>'' \<S>' P'' \<longrightarrow> tyenv_wellformed mds \<Gamma>''' \<S>' P'''; Stmt.If e c\<^sub>1 c\<^sub>2 = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma>''' \<and> \<S>' = \<S> \<and> P \<turnstile> P''' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma>''' \<S> P''')
 7. \<And>\<Gamma> e t P \<S> c. \<lbrakk>\<Gamma> \<turnstile>\<^sub>b e \<in> t ; P \<turnstile> t; \<turnstile> \<Gamma>,\<S>,P +\<^sub>\<S> e {c} \<Gamma>,\<S>,P; c = Stop \<Longrightarrow> \<Gamma> =:\<^sub>P +\<^sub>\<S> e \<Gamma> \<and> \<S> = \<S> \<and> P +\<^sub>\<S> e \<turnstile> P \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P +\<^sub>\<S> e \<longrightarrow> tyenv_wellformed mds \<Gamma> \<S> P); While e c = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma> \<and> \<S> = \<S> \<and> P \<turnstile> P \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma> \<S> P)
 8. \<And>\<Gamma>' \<Gamma> \<S> upd \<S>' P' P c \<Gamma>'' \<S>'' P''. \<lbrakk>\<Gamma>' = \<Gamma> \<oplus>\<^sub>\<S> upd; \<S>' = add_anno_stable \<S> upd; P' = P |` {v. local.stable \<S>' v}; \<turnstile> \<Gamma>',\<S>',P' {c} \<Gamma>'',\<S>'',P''; c = Stop \<Longrightarrow> \<Gamma>' =:\<^sub>P' \<Gamma>'' \<and> \<S>'' = \<S>' \<and> P' \<turnstile> P'' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P' \<longrightarrow> tyenv_wellformed mds \<Gamma>'' \<S>' P''); c \<noteq> Stop; \<And>x. to_total \<Gamma> x \<le>:\<^sub>P' to_total \<Gamma>' x; anno_type_stable \<Gamma> \<S> upd; anno_type_sec \<Gamma> \<S> P upd; c@[upd] = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma>'' \<and> \<S>'' = \<S> \<and> P \<turnstile> P'' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma>'' \<S> P'')
 9. \<And>\<Gamma> \<S> P c\<^sub>1 \<Gamma>' \<S>' P' c\<^sub>2 \<Gamma>'' \<S>'' P''. \<lbrakk>\<turnstile> \<Gamma>,\<S>,P {c\<^sub>1} \<Gamma>',\<S>',P'; c\<^sub>1 = Stop \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma>' \<and> \<S>' = \<S> \<and> P \<turnstile> P' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma>' \<S> P'); \<turnstile> \<Gamma>',\<S>',P' {c\<^sub>2} \<Gamma>'',\<S>'',P''; c\<^sub>2 = Stop \<Longrightarrow> \<Gamma>' =:\<^sub>P' \<Gamma>'' \<and> \<S>'' = \<S>' \<and> P' \<turnstile> P'' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma>' \<S>' P' \<longrightarrow> tyenv_wellformed mds \<Gamma>'' \<S>' P''); c\<^sub>1 ;; c\<^sub>2 = Stop\<rbrakk> \<Longrightarrow> \<Gamma> =:\<^sub>P \<Gamma>'' \<and> \<S>'' = \<S> \<and> P \<turnstile> P'' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma> \<S> P \<longrightarrow> tyenv_wellformed mds \<Gamma>'' \<S> P'')
 10. \<And>\<Gamma>\<^sub>1 \<S> P\<^sub>1 c \<Gamma>\<^sub>1' \<S>' P\<^sub>1' \<Gamma>\<^sub>2 P\<^sub>2 \<Gamma>\<^sub>2' P\<^sub>2'. \<lbrakk>\<turnstile> \<Gamma>\<^sub>1,\<S>,P\<^sub>1 {c} \<Gamma>\<^sub>1',\<S>',P\<^sub>1'; c = Stop \<Longrightarrow> \<Gamma>\<^sub>1 =:\<^sub>P\<^sub>1 \<Gamma>\<^sub>1' \<and> \<S>' = \<S> \<and> P\<^sub>1 \<turnstile> P\<^sub>1' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma>\<^sub>1 \<S> P\<^sub>1 \<longrightarrow> tyenv_wellformed mds \<Gamma>\<^sub>1' \<S> P\<^sub>1'); \<Gamma>\<^sub>2 =:\<^sub>P\<^sub>2 \<Gamma>\<^sub>1; \<forall>mds. tyenv_wellformed mds \<Gamma>\<^sub>2 \<S> P\<^sub>2 \<longrightarrow> tyenv_wellformed mds \<Gamma>\<^sub>1 \<S> P\<^sub>1; \<forall>mds. tyenv_wellformed mds \<Gamma>\<^sub>1' \<S>' P\<^sub>1' \<longrightarrow> tyenv_wellformed mds \<Gamma>\<^sub>2' \<S>' P\<^sub>2'; \<Gamma>\<^sub>1' =:\<^sub>P\<^sub>1' \<Gamma>\<^sub>2'; P\<^sub>2 \<turnstile> P\<^sub>1; P\<^sub>1' \<turnstile> P\<^sub>2'; c = Stop\<rbrakk> \<Longrightarrow> \<Gamma>\<^sub>2 =:\<^sub>P\<^sub>2 \<Gamma>\<^sub>2' \<and> \<S>' = \<S> \<and> P\<^sub>2 \<turnstile> P\<^sub>2' \<and> (\<forall>mds. tyenv_wellformed mds \<Gamma>\<^sub>2 \<S> P\<^sub>2 \<longrightarrow> tyenv_wellformed mds \<Gamma>\<^sub>2' \<S> P\<^sub>2')
A total of 11 subgoals...
[PROOF STEP]
apply (auto intro: context_equiv_trans context_equiv_entailment pred_entailment_trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<omega>_dec_of_Cantor_aux:
  assumes "Cantor_dec (\<alpha>#\<alpha>s)" "length \<alpha>s = length ms"
  shows "\<omega>_dec (\<omega>_of_Cantor (\<alpha>#\<alpha>s) (m#ms))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s)
length \<alpha>s = length ms

goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms))
[PROOF STEP]
proof (induction \<alpha>s arbitrary: ms)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) [\<alpha>]; length [] = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor [\<alpha>] (m # ms))
 2. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<lambda>x y. y < x) [\<alpha>]
length [] = length ms

goal (2 subgoals):
 1. \<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) [\<alpha>]; length [] = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor [\<alpha>] (m # ms))
 2. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sorted_wrt (\<lambda>x y. y < x) [\<alpha>]
length [] = length ms
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<lambda>x y. y < x) [\<alpha>]
length [] = length ms

goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor [\<alpha>] (m # ms))
[PROOF STEP]
using sorted_wrt_iff_nth_less
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<lambda>x y. y < x) [\<alpha>]
length [] = length ms
sorted_wrt ?P ?xs = (\<forall>i j. i < j \<longrightarrow> j < length ?xs \<longrightarrow> ?P (?xs ! i) (?xs ! j))

goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor [\<alpha>] (m # ms))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor [\<alpha>] (m # ms))

goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
case (Cons a \<alpha>s ms)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ?ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ?ms))
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s)
length (a # \<alpha>s) = length ms

goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ?ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ?ms))
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s)
length (a # \<alpha>s) = length ms
[PROOF STEP]
obtain n ns where ns: "ms = n#ns"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ?ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ?ms))
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s)
length (a # \<alpha>s) = length ms

goal (1 subgoal):
 1. (\<And>n ns. ms = n # ns \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis length_Suc_conv)
[PROOF STATE]
proof (state)
this:
ms = n # ns

goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ms = n # ns
[PROOF STEP]
have "a \<le> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
ms = n # ns

goal (1 subgoal):
 1. a \<le> \<alpha>
[PROOF STEP]
using Cons.prems(1) order.strict_implies_order
[PROOF STATE]
proof (prove)
using this:
ms = n # ns
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s)
?a < ?b \<Longrightarrow> ?a \<le> ?b

goal (1 subgoal):
 1. a \<le> \<alpha>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<le> \<alpha>

goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<le> \<alpha>

goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
have "\<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a
[PROOF STEP]
using Cons ns \<open>a \<le> \<alpha>\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ?ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ?ms))
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s)
length (a # \<alpha>s) = length ms
ms = n # ns
a \<le> \<alpha>

goal (1 subgoal):
 1. \<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a
[PROOF STEP]
apply (simp add: \<omega>_dec_replicate)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>ms. length ns = length ms \<Longrightarrow> if m = 0 then sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor \<alpha>s ms) else sorted_wrt (\<lambda>x y. y \<le> x) (\<alpha> # \<omega>_of_Cantor \<alpha>s ms); a < \<alpha> \<and> (\<forall>x\<in>list.set \<alpha>s. x < \<alpha>) \<and> (\<forall>x\<in>list.set \<alpha>s. x < a) \<and> sorted_wrt (\<lambda>x y. y < x) \<alpha>s; length \<alpha>s = length ns; ms = n # ns; a \<le> \<alpha>\<rbrakk> \<Longrightarrow> \<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a
[PROOF STEP]
by (meson \<omega>_of_Cantor_subset order.strict_implies_order subsetD)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a

goal (1 subgoal):
 1. \<And>a \<alpha>s ms. \<lbrakk>\<And>ms. \<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ms)); sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s); length (a # \<alpha>s) = length ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<le> \<alpha>
\<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a \<le> \<alpha>
\<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a

goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
using Cons ns
[PROOF STATE]
proof (prove)
using this:
a \<le> \<alpha>
\<forall>x\<in>list.set (\<omega>_of_Cantor \<alpha>s ns). x \<le> a
\<lbrakk>sorted_wrt (\<lambda>x y. y < x) (\<alpha> # \<alpha>s); length \<alpha>s = length ?ms\<rbrakk> \<Longrightarrow> sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # \<alpha>s) (m # ?ms))
sorted_wrt (\<lambda>x y. y < x) (\<alpha> # a # \<alpha>s)
length (a # \<alpha>s) = length ms
ms = n # ns

goal (1 subgoal):
 1. sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))
[PROOF STEP]
by (force simp: \<omega>_dec_replicate)
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<lambda>x y. y \<le> x) (\<omega>_of_Cantor (\<alpha> # a # \<alpha>s) (m # ms))

goal:
No subgoals!
[PROOF STEP]
qed