kings-crown/FVELER_Isabelle huggingface dataset:
theory Fastpath_C

lemma threadSet_st_tcb_at_state:
  "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t
        then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s
        else st_tcb_at' P p s)\<rbrace>
  threadSet f t \<lbrace>\<lambda>_. st_tcb_at' P p\<rbrace>" apply (rule hoare_chain) apply (rule threadSet_obj_at'_really_strongest) prefer 2 apply (simp add: st_tcb_at'_def) apply (clarsimp split: if_splits simp: st_tcb_at'_def o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s)\<rbrace> threadSet f t \<lbrace>\<lambda>_. st_tcb_at' P p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> threadSet f t \<lbrace>?Q\<rbrace>
 2. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> st_tcb_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ?t'4 then ?P4 (f obj) else ?P4 obj) ?t'4 s
 2. \<And>rv s. obj_at' ?P4 ?t'4 s \<Longrightarrow> st_tcb_at' P p s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. obj_at' ?P4 ?t'4 s \<Longrightarrow> st_tcb_at' P p s
 2. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ?t'4 then ?P4 (f obj) else ?P4 obj) ?t'4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<longrightarrow> (if p = t then obj_at' (\<lambda>tcb. P (tcbState (f tcb))) t s else st_tcb_at' P p s) \<Longrightarrow> tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = p then (P \<circ> tcbState) (f obj) else (P \<circ> tcbState) obj) p s proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma recv_ep_queued_st_tcb_at':
  "\<lbrakk> ko_at' (Structures_H.endpoint.RecvEP ts) epptr s ;
     t \<in> set ts;
     sym_refs (state_refs_of' s) \<rbrakk>
   \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s" apply (drule obj_at_ko_at') apply clarsimp apply (drule (1) sym_refs_ko_atD') apply (clarsimp simp: pred_tcb_at'_def obj_at'_real_def refs_of_rev') apply (erule_tac x=t in ballE; clarsimp?) apply (erule ko_wp_at'_weakenE) apply (clarsimp simp: isBlockedOnReceive_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' (Structures_H.endpoint.RecvEP ts) epptr s; t \<in> set ts; sym_refs (state_refs_of' s)\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); \<exists>ko. ko_at' ko epptr s \<and> ko = Structures_H.endpoint.RecvEP ts\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); ko_at' (Structures_H.endpoint.RecvEP ts) epptr s\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = refs_of' (injectKOS (Structures_H.endpoint.RecvEP ts)) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS (Structures_H.endpoint.RecvEP ts)). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> st_tcb_at' isBlockedOnReceive t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = set ts \<times> {EPRecv}; \<forall>x\<in>set ts. ko_wp_at' (\<lambda>ko. \<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive epptr a)) x s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> isBlockedOnReceive (tcbState obj)) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = set ts \<times> {EPRecv}; ko_wp_at' (\<lambda>ko. \<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive epptr a)) t s\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> isBlockedOnReceive (tcbState obj)) t s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>t \<in> set ts; sym_refs (state_refs_of' s); state_refs_of' s epptr = set ts \<times> {EPRecv}; \<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive epptr a)\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj \<and> isBlockedOnReceive (tcbState obj) proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma signed_n_msgRegisters_to_H:
  "(signed n_msgRegisters :: machine_word) = of_nat size_msgRegisters" by (simp add: n_msgRegisters_def size_msgRegisters_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST(32 signed \<rightarrow> 32) n_msgRegisters = word_of_nat size_msgRegisters
theory Fastpath_C

lemma valid_ep_typ_at_lift':
  "\<lbrakk> \<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace> \<rbrakk>
      \<Longrightarrow> \<lbrace>\<lambda>s. valid_ep' ep s\<rbrace> f \<lbrace>\<lambda>rv s. valid_ep' ep s\<rbrace>" apply (cases ep, simp_all add: valid_ep'_def) apply (wp hoare_vcg_const_Ball_lift typ_at_lifts | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>) \<Longrightarrow> \<lbrace>valid_ep' ep\<rbrace> f \<lbrace>\<lambda>rv. valid_ep' ep\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>; ep = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. x1 \<noteq> [] \<and> (\<forall>t\<in>set x1. tcb_at' t s) \<and> distinct x1\<rbrace> f \<lbrace>\<lambda>rv s. x1 \<noteq> [] \<and> (\<forall>t\<in>set x1. tcb_at' t s) \<and> distinct x1\<rbrace>
 2. \<lbrakk>\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>; ep = Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace>
 3. \<And>x3. \<lbrakk>\<And>p. \<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' TCBT p\<rbrace>; ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3\<rbrace> f \<lbrace>\<lambda>rv s. x3 \<noteq> [] \<and> (\<forall>t\<in>set x3. tcb_at' t s) \<and> distinct x3\<rbrace> proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma threadSet_tcbState_valid_objs:
  "\<lbrace>valid_tcb_state' st and valid_objs'\<rbrace>
     threadSet (tcbState_update (\<lambda>_. st)) t
   \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" apply (wp threadSet_valid_objs') apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_tcb_state' st and valid_objs'\<rbrace> threadSet (tcbState_update (\<lambda>_. st)) t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_tcb_state' st and valid_objs') s \<Longrightarrow> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. st) tcb) s)) s proof (prove)
goal:
No subgoals!
theory Fastpath_C

lemma fastpath_reply_cap_check_ccorres:
  "ccorres (\<lambda>rv rv'. \<forall>cap. ccap_relation cap ccap
          \<longrightarrow> rv' = from_bool (isReplyCap cap \<and> \<not> capReplyMaster cap)) ret__int_'
      \<top> ({s. cap_' s = ccap}) []
      (return ()) (Call fastpath_reply_cap_check_'proc)" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: extra_sle_sless_unfolds isMasterReplyCap_fp_conv
                        from_bool_def return_def) apply (simp split: bool.split if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. \<forall>cap. ccap_relation cap ccap \<longrightarrow> rv' = from_bool (isReplyCap cap \<and> \<not> capReplyMaster cap)) ret__int_' (\<lambda>_. True) \<lbrace>\<acute>cap = ccap\<rbrace> [] (return ()) (Call fastpath_reply_cap_check_'proc) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> \<lbrace>\<acute>cap = ccap\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} Call fastpath_reply_cap_check_'proc {s. \<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (\<forall>cap. ccap_relation cap ccap \<longrightarrow> ret__int_' s = from_bool (isReplyCap cap \<and> \<not> capReplyMaster cap))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. True \<and> s \<in> \<lbrace>\<acute>cap = ccap\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. 0 \<le>s 5 \<and> 5 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> (\<exists>(rv, \<sigma>')\<in>fst (return () \<sigma>). (\<sigma>', s\<lparr>ret__int_' := if UCAST(32 \<rightarrow> 32) (cap_C.words_C (cap_' s).[unat 0]) && (1 << unat 5) - 1 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then 1 else 0, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (\<forall>cap. ccap_relation cap ccap \<longrightarrow> (if UCAST(32 \<rightarrow> 32) (cap_C.words_C (cap_' s).[unat 0]) && (1 << unat 5) - 1 = SCAST(32 signed \<rightarrow> 32) cap_reply_cap then 1 else 0) = from_bool (isReplyCap cap \<and> \<not> capReplyMaster cap)))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cap. \<lbrakk>(\<sigma>, x) \<in> rf_sr; ccap = cap_' x; ccap_relation cap (cap_' x)\<rbrakk> \<Longrightarrow> (if isReplyCap cap \<and> \<not> capReplyMaster cap then 1 else 0) = (case isReplyCap cap \<and> \<not> capReplyMaster cap of True \<Rightarrow> word_of_nat 1 | False \<Rightarrow> word_of_nat 0) proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma add_statefn_id1:
  "add_statefn id x = x" by (induct x) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. add_statefn id x = x
theory SimplRewrite

lemma add_statefn_id[simp]:
  "add_statefn id = id" by (rule ext, simp add: add_statefn_id1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. add_statefn id = id
theory SimplRewrite

lemma add_statefn_comp:
  "\<lbrakk> inv (g o f) = inv f o inv g \<rbrakk>
     \<Longrightarrow> add_statefn f (add_statefn g x) = add_statefn (g o f) x" by (induct x, simp_all add: o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inv (g \<circ> f) = inv f \<circ> inv g \<Longrightarrow> add_statefn f (add_statefn g x) = add_statefn (g \<circ> f) x
theory SimplRewrite

lemma isAbr_add_statefn_xstate[simp]:
  "isAbr (add_statefn_xstate f xs) = isAbr xs" by (cases xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isAbr (add_statefn_xstate f xs) = isAbr xs
theory SimplRewrite

lemma add_statefn_xstate_comp:
  "add_statefn_xstate f (add_statefn_xstate g xs) = add_statefn_xstate (f o g) xs" by (cases xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. add_statefn_xstate f (add_statefn_xstate g xs) = add_statefn_xstate (f \<circ> g) xs
theory SimplRewrite

lemma add_statefn_xstate_id[simp]:
  "add_statefn_xstate id = id" by (simp add: add_statefn_xstate_def fun_eq_iff split: xstate.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. add_statefn_xstate id = id
theory SimplRewrite

lemma exec_simulates_refl:
  "exec_simulates S T c c" by (simp add: exec_simulates_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exec_simulates S T c c
theory SimplRewrite

lemma exec_simulatesD:
  "\<lbrakk> \<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t; exec_simulates S T a b; s \<in> S \<rbrakk>
    \<Longrightarrow> \<Gamma> \<turnstile> \<langle>b, Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma> \<turnstile> \<langle>b, Normal s\<rangle> \<Rightarrow> Fault ft)
         \<or> (\<exists>t' \<in> - T. \<Gamma> \<turnstile> \<langle>b, Normal s\<rangle> \<Rightarrow> Normal t')" unfolding exec_simulates_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t; exec_simulates S T a b; s \<in> S\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Normal t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t; \<forall>s\<in>S. \<forall>\<Gamma> t. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Normal t'); s \<in> S\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> Normal t')
theory SimplRewrite

lemma exec_statefn_simulatesD:
  "\<lbrakk> \<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> t; exec_statefn_simulates f S T a b; s \<in> S \<rbrakk>
    \<Longrightarrow> (map_option (add_statefn (inv f)) o \<Gamma>) \<turnstile> \<langle>b, Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t
                  \<or> (\<exists>ft. (map_option (add_statefn (inv f)) o \<Gamma>) \<turnstile> \<langle>b, Normal (f s)\<rangle> \<Rightarrow> Fault ft)
                  \<or> (\<exists>t' \<in> - T. (map_option (add_statefn (inv f)) o \<Gamma>) \<turnstile> \<langle>b, Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))" unfolding exec_statefn_simulates_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t; exec_statefn_simulates f S T a b; s \<in> S\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t; \<forall>s\<in>S. \<forall>\<Gamma> t. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t')); s \<in> S\<rbrakk> \<Longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))
theory SimplRewrite

lemma exec_statefn_simulates_via_statefn:
  "bij f \<Longrightarrow>
   exec_statefn_simulates f S T a b = exec_simulates S T a (add_statefn f b)" apply (simp add: exec_statefn_simulates_def exec_simulates_def) apply (simp add: add_statefn_exec bij_imp_bij_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> exec_statefn_simulates f S T a b = exec_simulates S T a (add_statefn f b) proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> (\<forall>s\<in>S. \<forall>\<Gamma> t. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> add_statefn_xstate f t \<or> (\<exists>ft. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. (map_option (add_statefn (inv f)) \<circ> \<Gamma>)\<turnstile> \<langle>b,Normal (f s)\<rangle> \<Rightarrow> Normal (f t'))) = (\<forall>s\<in>S. \<forall>\<Gamma> t. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile> \<langle>add_statefn f b,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma>\<turnstile> \<langle>add_statefn f b,Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<exists>t'\<in>- T. \<Gamma>\<turnstile> \<langle>add_statefn f b,Normal s\<rangle> \<Rightarrow> Normal t')) proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma spec_statefn_simulates_via_statefn:
  "bij f \<Longrightarrow> spec_statefn_simulates f G G'
      = spec_simulates G (map_option (add_statefn f) o G')" apply (simp add: spec_statefn_simulates_def spec_simulates_def) apply (rule arg_cong[where f=All, OF ext]) apply (rule HOL.conj_cong[OF refl]) apply (safe, simp_all add: exec_statefn_simulates_via_statefn) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> spec_statefn_simulates f G G' = spec_simulates G (map_option (add_statefn f) \<circ> G') proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> (\<forall>x. (G x = None) = (G' x = None) \<and> (\<forall>b b'. G x = Some b \<and> G' x = Some b' \<longrightarrow> exec_statefn_simulates f UNIV UNIV b b')) = (\<forall>x. (G x = None) = (G' x = None) \<and> (\<forall>b b'. G x = Some b \<and> (\<exists>z. G' x = Some z \<and> add_statefn f z = b') \<longrightarrow> exec_simulates UNIV UNIV b b')) proof (prove)
goal (1 subgoal):
 1. \<And>x. bij f \<Longrightarrow> ((G x = None) = (G' x = None) \<and> (\<forall>b b'. G x = Some b \<and> G' x = Some b' \<longrightarrow> exec_statefn_simulates f UNIV UNIV b b')) = ((G x = None) = (G' x = None) \<and> (\<forall>b b'. G x = Some b \<and> (\<exists>z. G' x = Some z \<and> add_statefn f z = b') \<longrightarrow> exec_simulates UNIV UNIV b b')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>bij f; (G x = None) = (G' x = None)\<rbrakk> \<Longrightarrow> (\<forall>b b'. G x = Some b \<and> G' x = Some b' \<longrightarrow> exec_statefn_simulates f UNIV UNIV b b') = (\<forall>b b'. G x = Some b \<and> (\<exists>z. G' x = Some z \<and> add_statefn f z = b') \<longrightarrow> exec_simulates UNIV UNIV b b') proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma com_initial_guards_extra_simps[simp]:
  "com_initial_guards (whileAnno S I V c) = UNIV"
  "com_initial_guards (creturn exn_upd rv_upd rv) = UNIV"
  "com_initial_guards (creturn_void exn_upd) = UNIV"
  "com_initial_guards (call init f ret save) = UNIV"
  "com_initial_guards (cbreak exn_upd) = UNIV"
  "com_initial_guards (ccatchbrk exn) = UNIV" by (simp_all add: whileAnno_def creturn_def creturn_void_def
                    call_def block_def block_exn_def cbreak_def ccatchbrk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (com_initial_guards (whileAnno S I V c) = UNIV &&& com_initial_guards (creturn exn_upd rv_upd rv) = UNIV &&& com_initial_guards (creturn_void exn_upd) = UNIV) &&& com_initial_guards (call init f ret save) = UNIV &&& com_initial_guards (cbreak exn_upd) = UNIV &&& com_initial_guards (ccatchbrk exn) = UNIV
theory SimplRewrite

lemma exec_not_in_initial_guards:
  "\<lbrakk> s \<notin> com_initial_guards c \<rbrakk>
      \<Longrightarrow> \<exists>ft. \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Fault ft" apply (induct c, simp_all) apply clarsimp apply (blast intro: exec.Seq exec.FaultProp) apply (blast intro: exec.GuardFault exec.Guard) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<notin> com_initial_guards c \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (2 subgoals):
 1. \<And>c1 c2. \<lbrakk>\<exists>ft. \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Fault ft; s \<notin> com_initial_guards c2 \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c2,Normal s\<rangle> \<Rightarrow> Fault ft; s \<notin> com_initial_guards c1\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c1;;
c2,Normal s\<rangle> \<Rightarrow> Fault ft
 2. \<And>x1 x2a c. \<lbrakk>s \<notin> com_initial_guards c \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft; s \<in> x2a \<longrightarrow> s \<notin> com_initial_guards c\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard x1 x2a c,Normal s\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (2 subgoals):
 1. \<And>c1 c2 ft. \<lbrakk>s \<notin> com_initial_guards c2 \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c2,Normal s\<rangle> \<Rightarrow> Fault ft; s \<notin> com_initial_guards c1; \<Gamma>\<turnstile> \<langle>c1,Normal s\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c1;;
c2,Normal s\<rangle> \<Rightarrow> Fault ft
 2. \<And>x1 x2a c. \<lbrakk>s \<notin> com_initial_guards c \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft; s \<in> x2a \<longrightarrow> s \<notin> com_initial_guards c\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard x1 x2a c,Normal s\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2a c. \<lbrakk>s \<notin> com_initial_guards c \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft; s \<in> x2a \<longrightarrow> s \<notin> com_initial_guards c\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard x1 x2a c,Normal s\<rangle> \<Rightarrow> Fault ft proof (prove)
goal:
No subgoals!