kings-crown/FVELER_Isabelle huggingface dataset:
theory SimplRewrite

lemma exec_in_final_guards_induct:
  "\<lbrakk> \<Gamma> \<turnstile> \<langle>c, x\<rangle> \<Rightarrow> y \<rbrakk>
      \<Longrightarrow> \<forall>s t S. x = Normal s \<and> y = Normal t \<and> s \<in> S
            \<longrightarrow> t \<in> com_final_guards S c" apply (induct rule: exec.induct, simp_all) apply (case_tac s', simp_all) apply (auto elim: exec_Normal_elim_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,x\<rangle> \<Rightarrow> y \<Longrightarrow> \<forall>s t S. x = Normal s \<and> y = Normal t \<and> s \<in> S \<longrightarrow> t \<in> com_final_guards S c proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; \<forall>t S. s' = Normal t \<and> s \<in> S \<longrightarrow> t \<in> com_final_guards S c\<^sub>1; \<Gamma>\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; \<forall>s ta S. s' = Normal s \<and> t = Normal ta \<and> s \<in> S \<longrightarrow> ta \<in> com_final_guards S c\<^sub>2\<rbrakk> \<Longrightarrow> \<forall>ta. t = Normal ta \<and> Ex ((\<in>) s) \<longrightarrow> ta \<in> com_final_guards UNIV c\<^sub>2 proof (prove)
goal (3 subgoals):
 1. \<And>c\<^sub>1 s s' c\<^sub>2 t x2. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Abrupt x2; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Abrupt x2\<rangle> \<Rightarrow> t; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<forall>ta. t = Normal ta \<and> Ex ((\<in>) s) \<longrightarrow> ta \<in> com_final_guards UNIV c\<^sub>2
 2. \<And>c\<^sub>1 s s' c\<^sub>2 t x3. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault x3; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Fault x3\<rangle> \<Rightarrow> t; s' = Fault x3\<rbrakk> \<Longrightarrow> \<forall>ta. t = Normal ta \<and> Ex ((\<in>) s) \<longrightarrow> ta \<in> com_final_guards UNIV c\<^sub>2
 3. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Stuck; \<Gamma>\<turnstile> \<langle>c\<^sub>2,Stuck\<rangle> \<Rightarrow> t; s' = Stuck\<rbrakk> \<Longrightarrow> \<forall>ta. t = Normal ta \<and> Ex ((\<in>) s) \<longrightarrow> ta \<in> com_final_guards UNIV c\<^sub>2 proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma exec_in_final_guards:
  "\<lbrakk> \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t \<rbrakk>
      \<Longrightarrow> t \<in> com_final_guards UNIV c" by (drule exec_in_final_guards_induct, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<Longrightarrow> t \<in> com_final_guards UNIV c
theory SimplRewrite

lemma exec_While_not_in_state_lemma:
  "\<lbrakk> \<forall>t'\<in>- T. \<not> \<Gamma> \<turnstile> \<langle>While C' b,Normal s\<rangle> \<Rightarrow> Normal (f t');
     \<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>While C' b,Normal s\<rangle> \<Rightarrow> Fault ft \<rbrakk>
     \<Longrightarrow> (s \<in> com_initial_guards b \<or> s \<notin> f ` (- T))" apply (rule ccontr, clarsimp) apply (drule_tac \<Gamma>=\<Gamma> in exec_not_in_initial_guards) apply (blast intro: exec.WhileTrue exec.WhileFalse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t'\<in>- T. \<not> \<Gamma>\<turnstile> \<langle>While C' b,Normal s\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> \<Gamma>\<turnstile> \<langle>While C' b,Normal s\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> s \<in> com_initial_guards b \<or> s \<notin> f ` (- T) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>t'\<in>- T. \<not> \<Gamma>\<turnstile> \<langle>While C' b,Normal (f x)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> \<Gamma>\<turnstile> \<langle>While C' b,Normal (f x)\<rangle> \<Rightarrow> Fault ft; f x \<notin> com_initial_guards b; s = f x; x \<notin> T\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>t'\<in>- T. \<not> \<Gamma>\<turnstile> \<langle>While C' b,Normal (f x)\<rangle> \<Rightarrow> Normal (f t'); \<forall>ft. \<not> \<Gamma>\<turnstile> \<langle>While C' b,Normal (f x)\<rangle> \<Rightarrow> Fault ft; s = f x; x \<notin> T; \<exists>ft. \<Gamma>\<turnstile> \<langle>b,Normal (f x)\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma exec_statefn_simulates_creturn_void:
  "\<lbrakk> \<And>inn s. s \<in> S \<Longrightarrow> f (exn_upd inn s) = exn_upd' inn (f s) \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates f S T (creturn_void exn_upd)
                (creturn_void exn_upd')" apply (simp add: creturn_void_def) apply (intro exec_statefn_simulates_Seq exec_statefn_simulates_Basic
               exec_statefn_simulates_Skip_Throw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>inn s. s \<in> S \<Longrightarrow> f (exn_upd inn s) = exn_upd' inn (f s)) \<Longrightarrow> exec_statefn_simulates f S T (creturn_void exn_upd) (creturn_void exn_upd') proof (prove)
goal (1 subgoal):
 1. (\<And>inn s. s \<in> S \<Longrightarrow> f (exn_upd inn s) = exn_upd' inn (f s)) \<Longrightarrow> exec_statefn_simulates f S T (Basic (exn_upd (\<lambda>_. Return));;
THROW) (Basic (exn_upd' (\<lambda>_. Return));;
THROW) proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma exec_statefn_simulates_creturn:
  "\<lbrakk> \<And>inn s. f (exn_upd inn s) = exn_upd' inn (f s);
       \<And>inn s. s \<in> S \<Longrightarrow> f (rv_upd inn s) = rv_upd' inn (f s);
       \<And>inn s. s \<in> S \<Longrightarrow> rv s = rv' (f s) \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates f S T (creturn exn_upd rv_upd rv)
                (creturn exn_upd' rv_upd' rv')" apply (simp add: creturn_def) apply (intro exec_statefn_simulates_Seq exec_statefn_simulates_Basic
               exec_statefn_simulates_Skip_Throw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>inn s. f (exn_upd inn s) = exn_upd' inn (f s); \<And>inn s. s \<in> S \<Longrightarrow> f (rv_upd inn s) = rv_upd' inn (f s); \<And>inn s. s \<in> S \<Longrightarrow> rv s = rv' (f s)\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (creturn exn_upd rv_upd rv) (creturn exn_upd' rv_upd' rv') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>inn s. f (exn_upd inn s) = exn_upd' inn (f s); \<And>inn s. s \<in> S \<Longrightarrow> f (rv_upd inn s) = rv_upd' inn (f s); \<And>s. s \<in> S \<Longrightarrow> rv s = rv' (f s)\<rbrakk> \<Longrightarrow> exec_statefn_simulates f S T (Basic (\<lambda>s. rv_upd (\<lambda>_. rv s) s);;
(Basic (exn_upd (\<lambda>_. Return));;
THROW)) (Basic (\<lambda>s. rv_upd' (\<lambda>_. rv' s) s);;
(Basic (exn_upd' (\<lambda>_. Return));;
THROW)) proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma exec_statefn_simulates_cbreak:
  "\<lbrakk> \<And>inn s. s \<in> S \<Longrightarrow> f (exn_upd inn s) = exn_upd' inn (f s) \<rbrakk>
      \<Longrightarrow> exec_statefn_simulates f S T (cbreak exn_upd)
                (cbreak exn_upd')" apply (simp add: cbreak_def) apply (intro exec_statefn_simulates_Seq exec_statefn_simulates_Basic
               exec_statefn_simulates_Skip_Throw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>inn s. s \<in> S \<Longrightarrow> f (exn_upd inn s) = exn_upd' inn (f s)) \<Longrightarrow> exec_statefn_simulates f S T (cbreak exn_upd) (cbreak exn_upd') proof (prove)
goal (1 subgoal):
 1. (\<And>inn s. s \<in> S \<Longrightarrow> f (exn_upd inn s) = exn_upd' inn (f s)) \<Longrightarrow> exec_statefn_simulates f S T (Basic (exn_upd (\<lambda>_. Break));;
THROW) (Basic (exn_upd' (\<lambda>_. Break));;
THROW) proof (prove)
goal:
No subgoals!
theory SimplRewrite

lemma xstate_inv_set_UNIV:
  "xstate_inv_set UNIV = UNIV" by (simp add: xstate_inv_set_def split: xstate.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xstate_inv_set UNIV = UNIV
theory CToCRefine

lemma spec_statefn_simulates_lookup_tree_Node:
  "\<lbrakk> exec_statefn_simulates g UNIV UNIV v v';
     spec_statefn_simulates g (lookup_tree a f) (lookup_tree c f);
     spec_statefn_simulates g (lookup_tree b f) (lookup_tree d f) \<rbrakk>
    \<Longrightarrow> spec_statefn_simulates g (lookup_tree (Node n v a b) f) (lookup_tree (Node n v' c d) f)" by (simp add: spec_statefn_simulates_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_statefn_simulates g UNIV UNIV v v'; spec_statefn_simulates g (lookup_tree a f) (lookup_tree c f); spec_statefn_simulates g (lookup_tree b f) (lookup_tree d f)\<rbrakk> \<Longrightarrow> spec_statefn_simulates g (lookup_tree (Tree.Node n v a b) f) (lookup_tree (Tree.Node n v' c d) f)
theory CToCRefine

lemma spec_statefn_simulates_lookup_tree_Leaf:
  "spec_statefn_simulates g (lookup_tree Leaf f) (lookup_tree Leaf f')" by (simp add: spec_statefn_simulates_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_statefn_simulates g (lookup_tree Leaf f) (lookup_tree Leaf f')
theory Refine_C

lemma schedule_sch_act_wf:
  "\<lbrace>invs'\<rbrace> schedule \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (rule hoare_post_imp) apply (erule invs_sch_act_wf') apply (rule schedule_invs') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s
 2. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine_C

lemma ucast_not_helper_cheating:
  fixes a:: "10 word"
  assumes a: "ucast a \<noteq> (0xFFFF :: word16)"
  shows "ucast a \<noteq> (0xFFFF::32 signed word)" by (word_bitwise,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32 signed) a \<noteq> 0xFFFF
theory Refine_C

lemma ucast_helper_not_maxword:
  \<open>UCAST(10 \<rightarrow> 32) x \<noteq> 0xFFFF\<close> by transfer (simp add: take_bit_eq_mod)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(10 \<rightarrow> 32) x \<noteq> 0xFFFF
theory Refine_C

lemma ct_active_not_idle'_strengthen:
  "invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<and> ct_active' s \<longrightarrow> ksCurThread s \<noteq> ksIdleThread s
theory Refine_C

lemma ccorres_add_gets:
  "ccorresG rf_sr \<Gamma> rv xf P P' hs (do v \<leftarrow> gets f; m od) c
    \<Longrightarrow> ccorresG rf_sr \<Gamma> rv xf P P' hs m c" by (simp add: gets_bind_ign)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres rv xf P P' hs (do v <- gets f;
m
od) c \<Longrightarrow> ccorres rv xf P P' hs m c
theory Refine_C

lemma callKernel_cur:
  "\<lbrace>all_invs' e\<rbrace> callKernel e \<lbrace>\<lambda>rv s. tcb_at' (ksCurThread s) s\<rbrace>" apply (rule hoare_chain) apply (rule ckernel_invs) apply (clarsimp simp: all_invs'_def sch_act_simple_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs' e\<rbrace> callKernel e \<lbrace>\<lambda>rv s. tcb_at' (ksCurThread s) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P\<rbrace> callKernel e \<lbrace>?Q\<rbrace>
 2. \<And>s. all_invs' e s \<Longrightarrow> ?P s
 3. \<And>rv s. ?Q rv s \<Longrightarrow> tcb_at' (ksCurThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>s. all_invs' e s \<Longrightarrow> (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s
 2. \<And>rv s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle'))) s \<Longrightarrow> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. ((\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle'))) s \<Longrightarrow> tcb_at' (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Refine_C

lemma full_invs_both:
  "ADT_H uop \<Turnstile>
  {s'. \<exists>s. (s,s') \<in> lift_state_relation state_relation \<and>
     s \<in> full_invs \<and> s' \<in> full_invs'}" apply (rule fw_inv_transport) apply (rule akernel_invariant) apply (rule ckernel_invariant) apply (rule fw_sim_A_H) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<Turnstile> {s'. \<exists>s. (s, s') \<in> lift_state_relation state_relation \<and> s \<in> full_invs \<and> s' \<in> full_invs'} proof (prove)
goal (3 subgoals):
 1. ?A \<Turnstile> full_invs
 2. ADT_H uop \<Turnstile> full_invs'
 3. LI ?A (ADT_H uop) (lift_state_relation state_relation) (full_invs \<times> full_invs') proof (prove)
goal (2 subgoals):
 1. ADT_H uop \<Turnstile> full_invs'
 2. LI (ADT_A ?uop4) (ADT_H uop) (lift_state_relation state_relation) (full_invs \<times> full_invs') proof (prove)
goal (1 subgoal):
 1. LI (ADT_A ?uop4) (ADT_H uop) (lift_state_relation state_relation) (full_invs \<times> full_invs') proof (prove)
goal:
No subgoals!
theory Refine_C

lemma mem_dom_split:
 "(dom um \<subseteq> dom (user_mem' s) \<union> dom (device_mem' s))
 \<Longrightarrow> um = restrict_map um (dom (user_mem' s)) ++ restrict_map um (dom (device_mem' s))" apply (rule ext) apply (auto simp: map_add_def restrict_map_def split:if_splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom um \<subseteq> dom (user_mem' s) \<union> dom (device_mem' s) \<Longrightarrow> um = (um|\<^bsub>dom (user_mem' s)\<^esub>) ++ (um|\<^bsub>dom (device_mem' s)\<^esub>) proof (prove)
goal (1 subgoal):
 1. \<And>x. dom um \<subseteq> dom (user_mem' s) \<union> dom (device_mem' s) \<Longrightarrow> um x = ((um|\<^bsub>dom (user_mem' s)\<^esub>) ++ (um|\<^bsub>dom (device_mem' s)\<^esub>)) x proof (prove)
goal:
No subgoals!
theory Refine_C

lemma dom_if_rewrite:
  "dom (\<lambda>x. if P x then Some (f x) else None) = dom (\<lambda>x. if P x then Some () else None)" by (auto split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if P x then Some (f x) else None) = dom (\<lambda>x. if P x then Some () else None)
theory Refine_C

lemma dmo_domain_device_mem'[wp]:
  "\<lbrace>\<lambda>s. P (dom (device_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (device_mem' sa))\<rbrace>" apply (simp add:device_mem'_def pointerInDeviceData_def) apply (rule hoare_pre) apply (subst dom_if_rewrite) apply (wp doMachineOp_typ_at') apply (erule arg_cong[where f = P,THEN iffD1,rotated]) apply (auto split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (dom (device_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (device_mem' sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) s then Some p else None))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) sa then Some p else None))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) sa then Some p else None))\<rbrace>
 2. \<And>s. P (dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) s then Some p else None)) \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (\<lambda>x. if typ_at' UserDataDeviceT (x && ~~ mask pageBits) sa then Some () else None))\<rbrace>
 2. \<And>s. P (dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) s then Some p else None)) \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) s then Some p else None)) \<Longrightarrow> P (dom (\<lambda>x. if typ_at' UserDataDeviceT (x && ~~ mask pageBits) s then Some () else None)) proof (prove)
goal (1 subgoal):
 1. \<And>s. dom (\<lambda>p. if typ_at' UserDataDeviceT (p && ~~ mask pageBits) s then Some p else None) = dom (\<lambda>x. if typ_at' UserDataDeviceT (x && ~~ mask pageBits) s then Some () else None) proof (prove)
goal:
No subgoals!
theory Refine_C

lemma dmo_domain_user_mem'[wp]:
  "\<lbrace>\<lambda>s. P (dom (user_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (user_mem' sa))\<rbrace>" apply (simp add:user_mem'_def pointerInUserData_def) apply (rule hoare_pre) apply (subst dom_if_rewrite) apply (wp doMachineOp_typ_at') apply (erule arg_cong[where f = P,THEN iffD1,rotated]) apply (auto split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (dom (user_mem' s))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (user_mem' sa))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) s then Some (underlying_memory (ksMachineState s) p) else None))\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) sa then Some (underlying_memory (ksMachineState sa) p) else None))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) sa then Some (underlying_memory (ksMachineState sa) p) else None))\<rbrace>
 2. \<And>s. P (dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) s then Some (underlying_memory (ksMachineState s) p) else None)) \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> doMachineOp opfun \<lbrace>\<lambda>rv sa. P (dom (\<lambda>x. if typ_at' UserDataT (x && ~~ mask pageBits) sa then Some () else None))\<rbrace>
 2. \<And>s. P (dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) s then Some (underlying_memory (ksMachineState s) p) else None)) \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) s then Some (underlying_memory (ksMachineState s) p) else None)) \<Longrightarrow> P (dom (\<lambda>x. if typ_at' UserDataT (x && ~~ mask pageBits) s then Some () else None)) proof (prove)
goal (1 subgoal):
 1. \<And>s. dom (\<lambda>p. if typ_at' UserDataT (p && ~~ mask pageBits) s then Some (underlying_memory (ksMachineState s) p) else None) = dom (\<lambda>x. if typ_at' UserDataT (x && ~~ mask pageBits) s then Some () else None) proof (prove)
goal:
No subgoals!
theory Refine_C

theorem refinement2:
  "ADT_C uop \<sqsubseteq> ADT_H uop" unfolding ADT_C_def by (rule refinement2_both)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_C uop \<sqsubseteq> ADT_H uop proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C False)\<rparr> \<sqsubseteq> ADT_H uop
theory Refine_C

theorem fp_refinement:
  "ADT_FP_C uop \<sqsubseteq> ADT_H uop" unfolding ADT_FP_C_def by (rule refinement2_both)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_FP_C uop \<sqsubseteq> ADT_H uop proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C True)\<rparr> \<sqsubseteq> ADT_H uop
theory Refine_C

theorem seL4_refinement:
  "ADT_C uop \<sqsubseteq> ADT_A uop" by (blast intro: refinement refinement2 refinement_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_C uop \<sqsubseteq> ADT_A uop
theory Refine_C

lemma exec_C_Basic:
  "exec_C Gamma (Basic f) = (modify f)" apply (rule ext) apply (simp add: exec_C_def simpler_modify_def) apply (auto elim: exec.cases intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exec_C Gamma (Basic f) = modify f proof (prove)
goal (1 subgoal):
 1. \<And>x. exec_C Gamma (Basic f) x = modify f x proof (prove)
goal (1 subgoal):
 1. \<And>x. {()} \<times> {s'. Gamma\<turnstile> \<langle>Basic f,Normal x\<rangle> \<Rightarrow> Normal s'} = {((), f x)} \<and> (\<forall>xs. xs \<in> range Normal \<or> \<not> Gamma\<turnstile> \<langle>Basic f,Normal x\<rangle> \<Rightarrow> xs) proof (prove)
goal:
No subgoals!
theory Refine_C

lemma in_monad_imp_rewriteE:
  "\<lbrakk> (a, b) \<in> fst (f' s); monadic_rewrite F False \<top> f f'; F \<longrightarrow> \<not> snd (f s) \<rbrakk>
     \<Longrightarrow> (a, b) \<in> fst (f s)" by (auto simp add: monadic_rewrite_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> fst (f' s); monadic_rewrite F False (\<lambda>_. True) f f'; F \<longrightarrow> \<not> snd (f s)\<rbrakk> \<Longrightarrow> (a, b) \<in> fst (f s)
theory Refine_C

lemma ccorres_underlying_Fault:
  "\<lbrakk> ccorres_underlying srel Gamma rrefl xf arrel axf G G' hs m c;
           \<exists>s. (s, s') \<in> srel \<and> G s \<and> s' \<in> G' \<and> \<not> snd (m s) \<rbrakk>
      \<Longrightarrow> \<not> Gamma \<turnstile> \<langle>c, Normal s'\<rangle> \<Rightarrow> Fault ft" apply clarsimp apply (erule(4) ccorresE) apply (erule exec_handlers.EHOther) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel Gamma rrefl xf arrel axf G G' hs m c; \<exists>s. (s, s') \<in> srel \<and> G s \<and> s' \<in> G' \<and> \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> Gamma\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ccorres_underlying srel Gamma rrefl xf arrel axf G G' hs m c; (s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); Gamma\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); Gamma\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> Gamma\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n5 s, ?x5 s)
 2. \<And>s t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); Gamma\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Fault ft; ?x5 s = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n5 s = length hs) rrefl xf arrel axf r t'; ?n5 s \<le> length hs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> isAbr (Fault ft)
 2. \<And>s t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); Gamma\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Fault ft; Fault ft = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (length hs = length hs) rrefl xf arrel axf r t'; length hs \<le> length hs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s); Gamma\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> Fault ft; Fault ft = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (length hs = length hs) rrefl xf arrel axf r t'; length hs \<le> length hs\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!