kings-crown/FVELER_Isabelle huggingface dataset:
theory Intent_DR

lemma caps_of_object_update_context [simp]:
  "(\<lambda>n. map_option (\<lambda>(f, _). f (tcb_arch_update (tcb_context_update stf) tcb)) (tcb_cap_cases n)) =
   (\<lambda>n. map_option (\<lambda>(f, _). f tcb) (tcb_cap_cases n))" apply (rule ext) apply (simp add: tcb_cap_cases_def split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. map_option (\<lambda>(f, uu_). f (tcb_arch_update (tcb_context_update stf) tcb)) (tcb_cap_cases n)) = (\<lambda>n. map_option (\<lambda>(f, uu_). f tcb) (tcb_cap_cases n)) proof (prove)
goal (1 subgoal):
 1. \<And>n. map_option (\<lambda>(f, uu_). f (tcb_arch_update (tcb_context_update stf) tcb)) (tcb_cap_cases n) = map_option (\<lambda>(f, uu_). f tcb) (tcb_cap_cases n) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma not_generates_pending_is_null:
  "\<not> generates_pending st \<Longrightarrow> (infer_tcb_pending_op ptr st = Types_D.NullCap)" unfolding generates_pending_def infer_tcb_pending_op_def by (simp split: Structures_A.thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> generates_pending st \<Longrightarrow> infer_tcb_pending_op ptr st = cdl_cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<not> (case st of Inactive \<Rightarrow> False | IdleThreadState \<Rightarrow> False | _ \<Rightarrow> True) \<Longrightarrow> (case st of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap ptr True False | BlockedOnNotification ptr \<Rightarrow> PendingNtfnRecvCap ptr | _ \<Rightarrow> cdl_cap.NullCap) = cdl_cap.NullCap
theory Intent_DR

lemma transform_tcb_upd_state_no_pending:
  "\<lbrakk> \<not> generates_pending (tcb_state tcb); \<not> generates_pending (f (tcb_state tcb)) \<rbrakk>
  \<Longrightarrow> transform_tcb ms ptr (tcb_state_update f tcb) etcb = transform_tcb ms ptr tcb etcb" unfolding transform_tcb_def by (simp add: not_generates_pending_is_null cong: transform_full_intent_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> generates_pending (tcb_state tcb); \<not> generates_pending (f (tcb_state tcb))\<rbrakk> \<Longrightarrow> transform_tcb ms ptr (tcb_state_update f tcb) etcb = transform_tcb ms ptr tcb etcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> generates_pending (tcb_state tcb); \<not> generates_pending (f (tcb_state tcb))\<rbrakk> \<Longrightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap $ tcb_ctable (tcb_state_update f tcb), tcb_vspace_slot \<mapsto> transform_cap $ tcb_vtable (tcb_state_update f tcb), tcb_replycap_slot \<mapsto> transform_cap $ tcb_reply (tcb_state_update f tcb), tcb_caller_slot \<mapsto> transform_cap $ tcb_caller (tcb_state_update f tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap $ tcb_ipcframe (tcb_state_update f tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op ptr (tcb_state (tcb_state_update f tcb)), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification (tcb_state_update f tcb))], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler (tcb_state_update f tcb)), cdl_tcb_intent = transform_full_intent ms ptr (tcb_state_update f tcb), cdl_tcb_has_fault = tcb_has_fault (tcb_state_update f tcb), cdl_tcb_domain = tcb_domain etcb\<rparr> = Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap $ tcb_ctable tcb, tcb_vspace_slot \<mapsto> transform_cap $ tcb_vtable tcb, tcb_replycap_slot \<mapsto> transform_cap $ tcb_reply tcb, tcb_caller_slot \<mapsto> transform_cap $ tcb_caller tcb, tcb_ipcbuffer_slot \<mapsto> transform_cap $ tcb_ipcframe tcb, tcb_pending_op_slot \<mapsto> infer_tcb_pending_op ptr (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent ms ptr tcb, cdl_tcb_has_fault = tcb_has_fault tcb, cdl_tcb_domain = tcb_domain etcb\<rparr>
theory Intent_DR

lemma transform_objects_dummy_set_original_cap [simp]:
  "transform_objects (b\<lparr>is_original_cap := x\<rparr>) = transform_objects b" by (clarsimp simp: cap_installed_at_irq_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_objects (b\<lparr>is_original_cap := x\<rparr>) = transform_objects b
theory Intent_DR

lemma transform_objects_dummy_update_cdt [simp]:
  "transform_objects (b\<lparr>cdt := x\<rparr>) = transform_objects b" by (clarsimp simp: cap_installed_at_irq_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_objects (b\<lparr>cdt := x\<rparr>) = transform_objects b
theory Intent_DR

lemma corres_corrupt_tcb_intent_dupl:
  "\<lbrakk> dcorres dc P P' (do corrupt_tcb_intent x; corrupt_tcb_intent x od) g \<rbrakk> \<Longrightarrow>
   dcorres dc P P' (corrupt_tcb_intent x) g" by (subst duplicate_corrupt_tcb_intent[symmetric], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (do corrupt_tcb_intent x;
corrupt_tcb_intent x
od) g \<Longrightarrow> dcorres dc P P' (corrupt_tcb_intent x) g
theory Intent_DR

lemma neq_Nil_conv':
  "(a \<noteq> []) =  (\<exists>h x. a = h@[x])" by (auto | drule append_butlast_last_id)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<noteq> []) = (\<exists>h x. a = h @ [x])
theory Intent_DR

lemma not_idle_thread_as_usr[wp]:
  "\<lbrace>not_idle_thread y\<rbrace> as_user p q \<lbrace>\<lambda>rv. not_idle_thread y\<rbrace>" by (simp add:not_idle_thread_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread y\<rbrace> as_user p q \<lbrace>\<lambda>rv. not_idle_thread y\<rbrace>
theory Intent_DR

lemma corrupt_frame_duplicate: "(do _ \<leftarrow> corrupt_frame bufp; corrupt_frame bufp od) = (corrupt_frame bufp)" apply (rule ext) apply (clarsimp simp:corrupt_frame_def simpler_modify_def bind_assoc) apply (clarsimp simp:bind_def select_def) apply (force simp: corrupt_intents_dup) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- corrupt_frame bufp;
corrupt_frame bufp
od = corrupt_frame bufp proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- corrupt_frame bufp;
corrupt_frame bufp
od) x = corrupt_frame bufp x proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- select UNIV;
_ <- \<lambda>s. ({((), corrupt_intents x bufp s)}, False);
f <- select UNIV;
\<lambda>s. ({((), corrupt_intents f bufp s)}, False)
od) x = (do f <- select UNIV;
\<lambda>s. ({((), corrupt_intents f bufp s)}, False)
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<Union>a\<in>UNIV \<times> {x}. fst (case a of (x, s) \<Rightarrow> (\<Union>a\<in>UNIV \<times> {corrupt_intents x bufp s}. fst (case a of (f, s) \<Rightarrow> ({((), corrupt_intents f bufp s)}, False)), False))) = (\<Union>a\<in>UNIV \<times> {x}. fst (case a of (f, s) \<Rightarrow> ({((), corrupt_intents f bufp s)}, False))) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_return:
  "empty_when_fail (return x)" by (clarsimp simp:return_def empty_when_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_when_fail (return x)
theory Intent_DR

lemma wp_no_fail_spec:
  "\<lbrakk>empty_when_fail f ; no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow>\<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>" apply (case_tac "no_fail ((=) s) f") apply simp apply clarsimp apply (simp add:no_fail_def valid_def empty_when_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail f; no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>empty_when_fail f; no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>; no_fail ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<lbrakk>empty_when_fail f; no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>; \<not> no_fail ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail f; no_fail ((=) s) f \<longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>; \<not> no_fail ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_when_fail f; \<not> no_fail ((=) s) f\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma empty_when_fail_compose:
assumes Q:"\<And>r. empty_when_fail (b r)"
assumes P:"empty_when_fail a"
shows "(\<And>P. weak_det_spec P a) \<Longrightarrow> empty_when_fail (a>>=b)" apply (clarsimp simp:empty_when_fail_def) apply (case_tac "snd (a s)") apply (clarsimp simp:bind_def) using P apply (clarsimp simp:empty_when_fail_def) apply (clarsimp simp:bind_def) apply (clarsimp simp:weak_det_spec_def no_fail_def) apply (drule_tac x = "(=) s" in meta_spec) apply (clarsimp simp:det_spec_def) using Q apply (simp add: empty_when_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. weak_det_spec P a) \<Longrightarrow> empty_when_fail (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. weak_det_spec P a; snd ((a >>= b) s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P. weak_det_spec P a; snd ((a >>= b) s); snd (a s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {}
 2. \<And>s. \<lbrakk>\<And>P. weak_det_spec P a; snd ((a >>= b) s); \<not> snd (a s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s aa ba. \<lbrakk>\<And>P. weak_det_spec P a; snd (a s); (aa, ba) \<in> fst (a s)\<rbrakk> \<Longrightarrow> fst (b aa ba) = {}
 2. \<And>s. \<lbrakk>\<And>P. weak_det_spec P a; snd ((a >>= b) s); \<not> snd (a s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {} proof (prove)
using this:
empty_when_fail a

goal (2 subgoals):
 1. \<And>s aa ba. \<lbrakk>\<And>P. weak_det_spec P a; snd (a s); (aa, ba) \<in> fst (a s)\<rbrakk> \<Longrightarrow> fst (b aa ba) = {}
 2. \<And>s. \<lbrakk>\<And>P. weak_det_spec P a; snd ((a >>= b) s); \<not> snd (a s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. weak_det_spec P a; snd ((a >>= b) s); \<not> snd (a s)\<rbrakk> \<Longrightarrow> fst ((a >>= b) s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba ab bb. \<lbrakk>\<And>P. weak_det_spec P a; \<not> snd (a s); (aa, ba) \<in> fst (a s); snd (b aa ba); (ab, bb) \<in> fst (a s)\<rbrakk> \<Longrightarrow> fst (b ab bb) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba ab bb. \<lbrakk>\<And>P. (\<forall>s. P s \<longrightarrow> \<not> snd (a s)) \<longrightarrow> det_spec P a; \<not> snd (a s); (aa, ba) \<in> fst (a s); snd (b aa ba); (ab, bb) \<in> fst (a s)\<rbrakk> \<Longrightarrow> fst (b ab bb) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba aaa baa. \<lbrakk>\<not> snd (a s); (aa, ba) \<in> fst (a s); snd (b aa ba); (aaa, baa) \<in> fst (a s); (\<forall>sa. s = sa \<longrightarrow> \<not> snd (a sa)) \<longrightarrow> det_spec ((=) s) a\<rbrakk> \<Longrightarrow> fst (b aaa baa) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba. \<lbrakk>snd (b aa ba); a s = ({(aa, ba)}, False)\<rbrakk> \<Longrightarrow> fst (b aa ba) = {} proof (prove)
using this:
empty_when_fail (b ?r)

goal (1 subgoal):
 1. \<And>s aa ba. \<lbrakk>snd (b aa ba); a s = ({(aa, ba)}, False)\<rbrakk> \<Longrightarrow> fst (b aa ba) = {} proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma wp_spec:
assumes "P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>"
shows "\<lbrace>(=) s and P\<rbrace> f \<lbrace>Q\<rbrace>" using assms by (clarsimp simp:valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(=) s and P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
using this:
P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>(=) s and P\<rbrace> f \<lbrace>Q\<rbrace>
theory Intent_DR

lemma det_compose:
  "\<lbrakk>det_spec P a;\<And>r. det_spec (Q r) (b r); \<lbrace>P\<rbrace>a\<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow> det_spec P (a>>=b)" by (fastforce simp: det_spec_def bind_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_spec P a; \<And>r. det_spec (Q r) (b r); \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> det_spec P (a >>= b)
theory Intent_DR

lemma no_fail_compose_imp:
  "\<lbrakk>no_fail P (a>>= b)\<rbrakk> \<Longrightarrow> no_fail P a \<and> (\<exists>Q. (\<lbrace>P\<rbrace>a\<lbrace>Q\<rbrace> \<and> (\<forall>r. no_fail (Q r) (b r))))" apply (clarsimp simp: bind_def no_fail_def) apply (rule_tac x = "\<lambda>rv s. \<exists>s'. P s'\<and> (rv,s) \<in> fst (a s')" in exI) apply (auto simp:valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (a >>= b) \<Longrightarrow> no_fail P a \<and> (\<exists>Q. \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace> \<and> (\<forall>r. no_fail (Q r) (b r))) proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa)) \<and> \<not> snd (a s) \<Longrightarrow> \<exists>Q. \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace> \<and> (\<forall>r s. Q r s \<longrightarrow> \<not> snd (b r s)) proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (a s). \<not> snd (case x of (x, xa) \<Rightarrow> b x xa)) \<and> \<not> snd (a s) \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>\<lambda>rv s. \<exists>s'. P s' \<and> (rv, s) \<in> fst (a s')\<rbrace> \<and> (\<forall>r s. (\<exists>s'. P s' \<and> (r, s) \<in> fst (a s')) \<longrightarrow> \<not> snd (b r s)) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma mapM_load_word_offs_do_machine_op:
  "mapM (load_word_offs ptr) list
     = do_machine_op (mapM loadWord (map (\<lambda>offs. ptr + of_nat (offs * word_size)) list))" apply (subst submonad_mapM[OF submonad_do_machine_op submonad_do_machine_op]) apply (simp add: loadWord_def empty_fail_cond) apply (simp add: load_word_offs_def[abs_def] mapM_map_simp o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM (load_word_offs ptr) list = do_machine_op (mapM loadWord (map (\<lambda>offs. ptr + word_of_nat (offs * word_size)) list)) proof (prove)
goal (2 subgoals):
 1. \<And>x. empty_fail (loadWord x)
 2. mapM (load_word_offs ptr) list = do u <- stateAssert (\<lambda>_. True) [];
mapM (do_machine_op \<circ> loadWord) (map (\<lambda>offs. ptr + word_of_nat (offs * word_size)) list)
od proof (prove)
goal (1 subgoal):
 1. mapM (load_word_offs ptr) list = do u <- stateAssert (\<lambda>_. True) [];
mapM (do_machine_op \<circ> loadWord) (map (\<lambda>offs. ptr + word_of_nat (offs * word_size)) list)
od proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma det_spec_get:
  "det_spec P (get)" by (clarsimp simp:get_def det_spec_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_spec P get
theory Intent_DR

lemma det_spec_put:
  "det_spec P (put t)" by (clarsimp simp:put_def det_spec_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_spec P (put t)
theory Intent_DR

lemma det_spec_modify:
  "det_spec P (modify f)" by (clarsimp simp:simpler_modify_def det_spec_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_spec P (modify f)
theory Intent_DR

lemma det_spec_gets:
  "det_spec P (gets f)" apply (clarsimp simp:gets_def) apply (rule det_compose) apply (rule det_spec_get) apply (rule det_spec_return) apply (fastforce simp:get_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_spec P (gets f) proof (prove)
goal (1 subgoal):
 1. det_spec P (do s <- get;
return (f s)
od) proof (prove)
goal (3 subgoals):
 1. det_spec P get
 2. \<And>r. det_spec (?Q r) (return (f r))
 3. \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r. det_spec (?Q r) (return (f r))
 2. \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get \<lbrace>?Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma det_spec_select_f:
  "\<lbrakk>P a; det_spec P f\<rbrakk> \<Longrightarrow> det_spec Q (select_f (f a))" by (fastforce simp: select_f_def det_spec_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P a; det_spec P f\<rbrakk> \<Longrightarrow> det_spec Q (select_f (f a))
theory Intent_DR

lemma det_imply_weak_det:
  "det_spec P a \<Longrightarrow> weak_det_spec P a" by (simp add:weak_det_spec_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_spec P a \<Longrightarrow> weak_det_spec P a
theory Intent_DR

lemma weak_det_spec_compose:
  assumes Q:"\<And>Q r. weak_det_spec (Q r) (b r)"
  assumes P:"\<And>P. weak_det_spec P a"
  shows "\<And>P. weak_det_spec P (a>>=b)" apply (clarsimp simp:weak_det_spec_def) apply (frule no_fail_compose_imp) apply clarsimp apply (rule det_compose) apply (simp add: P[THEN weak_det_specD]) apply (drule_tac x = r in spec) apply (erule Q[THEN weak_det_specD]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. weak_det_spec P (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<And>P. no_fail P (a >>= b) \<Longrightarrow> det_spec P (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>no_fail P (a >>= b); no_fail P a \<and> (\<exists>Q. \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace> \<and> (\<forall>r. no_fail (Q r) (b r)))\<rbrakk> \<Longrightarrow> det_spec P (a >>= b) proof (prove)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> det_spec P (a >>= b) proof (prove)
goal (3 subgoals):
 1. \<And>P Q. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> det_spec P a
 2. \<And>P Q r. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> det_spec (?Q6 P Q r) (b r)
 3. \<And>P Q. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>?Q6 P Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P Q r. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> det_spec (?Q6 P Q r) (b r)
 2. \<And>P Q. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>?Q6 P Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P Q r. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> det_spec (?Q6 P Q r) (b r)
 2. \<And>P Q. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>?Q6 P Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P Q. \<lbrakk>no_fail P (a >>= b); no_fail P a; \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<forall>r. no_fail (Q r) (b r)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma weak_det_spec_select_f:
  "\<lbrakk>\<And>P. weak_det_spec P f\<rbrakk> \<Longrightarrow> weak_det_spec Q (select_f (f a))" apply (case_tac "\<forall>s. \<not>Q s") apply (simp add:weak_det_spec_def no_fail_def det_spec_def) apply (clarsimp simp:weak_det_spec_def) apply (rule det_spec_select_f[where P = "(=) a"]) apply simp apply (drule_tac x = "(=) a" in meta_spec) apply (clarsimp simp: no_fail_def select_f_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. weak_det_spec P f) \<Longrightarrow> weak_det_spec Q (select_f (f a)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>P. weak_det_spec P f; \<forall>s. \<not> Q s\<rbrakk> \<Longrightarrow> weak_det_spec Q (select_f (f a))
 2. \<lbrakk>\<And>P. weak_det_spec P f; \<not> (\<forall>s. \<not> Q s)\<rbrakk> \<Longrightarrow> weak_det_spec Q (select_f (f a)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. weak_det_spec P f; \<not> (\<forall>s. \<not> Q s)\<rbrakk> \<Longrightarrow> weak_det_spec Q (select_f (f a)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. no_fail P f \<longrightarrow> det_spec P f; Q s; no_fail Q (select_f (f a))\<rbrakk> \<Longrightarrow> det_spec Q (select_f (f a)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>P. no_fail P f \<longrightarrow> det_spec P f; Q s; no_fail Q (select_f (f a))\<rbrakk> \<Longrightarrow> a = a
 2. \<And>s. \<lbrakk>\<And>P. no_fail P f \<longrightarrow> det_spec P f; Q s; no_fail Q (select_f (f a))\<rbrakk> \<Longrightarrow> det_spec ((=) a) f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>P. no_fail P f \<longrightarrow> det_spec P f; Q s; no_fail Q (select_f (f a))\<rbrakk> \<Longrightarrow> det_spec ((=) a) f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q s; no_fail Q (select_f (f a)); no_fail ((=) a) f \<longrightarrow> det_spec ((=) a) f\<rbrakk> \<Longrightarrow> det_spec ((=) a) f proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma weak_det_spec_fail:
  "weak_det_spec P fail" by (auto simp: weak_det_spec_def no_fail_def fail_def det_spec_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P fail
theory Intent_DR

lemma weak_det_spec_assert:
  "weak_det_spec P (assert x)" by (auto simp:weak_det_spec_fail assert_def det_imply_weak_det[OF det_spec_return])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (assert x)
theory Intent_DR

lemma weak_det_spec_assert_opt:
  "weak_det_spec P (assert_opt x)" by (auto simp: weak_det_spec_fail det_imply_weak_det[OF det_spec_return] assert_opt_def split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (assert_opt x)
theory Intent_DR

lemma weak_det_spec_gets_the:
  "weak_det_spec P (gets_the f)" apply (simp add:gets_the_def) apply (rule weak_det_spec_compose[OF weak_det_spec_assert_opt det_imply_weak_det[OF det_spec_gets]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (gets_the f) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (gets f >>= assert_opt) proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma weak_det_spec_loadWord:
  "weak_det_spec P (loadWord x)" apply (clarsimp simp:loadWord_def) apply (rule weak_det_spec_compose)+ apply (rule det_imply_weak_det[OF det_spec_return]) apply (rule weak_det_spec_assert) apply (rule det_imply_weak_det[OF det_spec_gets]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (loadWord x) proof (prove)
goal (1 subgoal):
 1. weak_det_spec P (do m <- gets underlying_memory;
y <- assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od) proof (prove)
goal (3 subgoals):
 1. \<And>Q r Qa ra. weak_det_spec (Qa ra) (return (word_rcat [r (x + 3), r (x + 2), r (x + 1), r x]))
 2. \<And>Q r P. weak_det_spec P (assert (x && mask 2 = 0))
 3. \<And>P. weak_det_spec P (gets underlying_memory) proof (prove)
goal (2 subgoals):
 1. \<And>Q r P. weak_det_spec P (assert (x && mask 2 = 0))
 2. \<And>P. weak_det_spec P (gets underlying_memory) proof (prove)
goal (1 subgoal):
 1. \<And>P. weak_det_spec P (gets underlying_memory) proof (prove)
goal:
No subgoals!