kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_D

lemma dcorres_whenE_throwError_abstract:
  "\<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e);
    \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'\<rbrakk> \<Longrightarrow>
   dcorres rvrel (M and N) (M' and N') m (whenE cond (throwError e) >>=E (\<lambda>_. m'))" apply (unfold whenE_def) apply (case_tac cond) apply (clarsimp) apply (erule corres_guard_imp, simp+) apply (erule corres_guard_imp, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e); \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m (doE _ <- whenE cond (throwError e);
m'
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e); \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m (doE _ <- if cond then throwError e else returnOk ();
m'
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e); \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'; cond\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m (doE _ <- if cond then throwError e else returnOk ();
m'
odE)
 2. \<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e); \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'; \<not> cond\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m (doE _ <- if cond then throwError e else returnOk ();
m'
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dcorres rvrel M M' m (throwError e); cond\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m (throwError e)
 2. \<lbrakk>cond \<Longrightarrow> dcorres rvrel M M' m (throwError e); \<not> cond \<Longrightarrow> dcorres rvrel N N' m m'; \<not> cond\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m (doE _ <- if cond then throwError e else returnOk ();
m'
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres rvrel N N' m m'; \<not> cond\<rbrakk> \<Longrightarrow> dcorres rvrel (M and N) (M' and N') m m' proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_to_wp:
  "dcorres dc \<top> Q (return x) g \<Longrightarrow> \<lbrace>\<lambda>s. Q s \<and> transform s = cs\<rbrace>g\<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (fastforce simp:corres_underlying_def valid_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) Q (return x) g \<Longrightarrow> \<lbrace>\<lambda>s. Q s \<and> transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory Corres_D

lemma wp_to_dcorres:
  "(\<And>cs. \<lbrace>\<lambda>s. Q s \<and> transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>) \<Longrightarrow>  dcorres dc (\<lambda>_. True) Q (return x) g" by (clarsimp simp:corres_underlying_def valid_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cs. \<lbrace>\<lambda>s. Q s \<and> transform s = cs\<rbrace> g \<lbrace>\<lambda>r s. transform s = cs\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) Q (return x) g
theory Corres_D

lemma dcorres_symb_exec_rE:
  "\<lbrakk>\<And>rv. dcorres r P (Q' rv) h (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk>
  \<Longrightarrow> dcorres r P P' h (liftE f >>=E g)" apply (simp add: liftE_def lift_def bindE_def) apply (erule (1) dcorres_symb_exec_r) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. dcorres r P (Q' rv) h (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P P' h (liftE f >>=E g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. dcorres r P (Q' rv) h (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> dcorres r P P' h (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>cs. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> f \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!
theory Corres_D

lemma throw_handle:
  "(Monads_D.throw <handle2> (\<lambda>_. m)) = m" by (simp add: handleE'_def throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (throw <handle2> (\<lambda>_. m)) = m
theory Corres_D

lemma dcorres_rhs_noop_below:
  "\<lbrakk> dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g;
     \<lbrace> P \<rbrace> f \<lbrace> \<lambda>_. Q \<rbrace>; \<lbrace> P' \<rbrace> g \<lbrace> \<lambda>_. Q' \<rbrace> \<rbrakk>
   \<Longrightarrow> dcorres anyrel P P' (f :: unit k_monad) (g >>= (\<lambda>_. m))" apply (rule corres_add_noop_lhs2) apply (rule corres_split_forwards') apply (assumption | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> dcorres anyrel P P' f (do _ <- g;
m
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> dcorres anyrel P P' (do _ <- f;
return ()
od) (do _ <- g;
m
od) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> dcorres ?r'2 P P' f g
 2. \<lbrakk>dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>?Q2\<rbrace>
 3. \<lbrakk>dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'2\<rbrace>
 4. \<And>uu_ uua_. \<lbrakk>dcorres anyrel Q Q' (return ()) m; dcorres anyrel P P' f g; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_. Q'\<rbrace>; ?r'2 uu_ uua_\<rbrakk> \<Longrightarrow> dcorres anyrel (?Q2 uu_) (?Q'2 uua_) (return ()) m proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_rhs_noop_above: "\<lbrakk> dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g;
              \<lbrace> P \<rbrace> return () \<lbrace> \<lambda>_. Q \<rbrace>; \<lbrace> P' \<rbrace> m \<lbrace> \<lambda>_. Q' \<rbrace> \<rbrakk>
            \<Longrightarrow> dcorres anyrel' P P' f (m >>= (\<lambda>_. g))" apply (rule corres_add_noop_lhs) apply (rule corres_split_forwards') apply (assumption | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> m \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> dcorres anyrel' P P' f (do _ <- m;
g
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> m \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> dcorres anyrel' P P' (do _ <- return ();
f
od) (do _ <- m;
g
od) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> m \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> dcorres ?r'2 P P' (return ()) m
 2. \<lbrakk>dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> m \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> return () \<lbrace>?Q2\<rbrace>
 3. \<lbrakk>dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> m \<lbrace>\<lambda>_. Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> m \<lbrace>?Q'2\<rbrace>
 4. \<And>uu_ uua_. \<lbrakk>dcorres anyrel P P' (return ()) m; dcorres anyrel' Q Q' f g; \<lbrace>P\<rbrace> return () \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> m \<lbrace>\<lambda>_. Q'\<rbrace>; ?r'2 uu_ uua_\<rbrakk> \<Longrightarrow> dcorres anyrel' (?Q2 uu_) (?Q'2 uua_) f g proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_assert_opt_assume:
  assumes "\<And>x. m = Some x \<Longrightarrow> dcorres R P P' a (c x)"
  shows "dcorres R P P' a (assert_opt m >>= c)" using assms by (auto simp: bind_def assert_opt_def assert_def fail_def return_def
                 corres_underlying_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres R P P' a (assert_opt m >>= c) proof (prove)
using this:
m = Some ?x \<Longrightarrow> dcorres R P P' a (c ?x)

goal (1 subgoal):
 1. dcorres R P P' a (assert_opt m >>= c)
theory Intent_DR

lemma ep_not_idle:
  "\<lbrakk>valid_idle s;obj_at is_ep epptr s\<rbrakk> \<Longrightarrow> not_idle_thread epptr s" by (clarsimp simp:valid_idle_def obj_at_def is_cap_table_def pred_tcb_at_def is_ep_def not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; ep_at epptr s\<rbrakk> \<Longrightarrow> not_idle_thread epptr s
theory Intent_DR

lemma ntfn_not_idle:
  "\<lbrakk>valid_idle s;obj_at is_ntfn epptr s\<rbrakk> \<Longrightarrow> not_idle_thread epptr s" by (clarsimp simp:valid_idle_def obj_at_def is_cap_table_def pred_tcb_at_def is_ntfn_def not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; ntfn_at epptr s\<rbrakk> \<Longrightarrow> not_idle_thread epptr s
theory Intent_DR

lemma cte_wp_at_zombie_not_idle:
  "\<lbrakk>cte_wp_at ((=) (cap.Zombie ptr' zbits n)) ptr s; invs s\<rbrakk> \<Longrightarrow> not_idle_thread (fst ptr) s"
  "\<lbrakk>cte_wp_at ((=) (cap.Zombie ptr' zbits n)) ptr s; invs s\<rbrakk> \<Longrightarrow> not_idle_thread ptr' s" by (auto dest!: zombie_cap_two_nonidles simp: cte_wp_at_caps_of_state not_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>cte_wp_at ((=) (Zombie ptr' zbits n)) ptr s; invs s\<rbrakk> \<Longrightarrow> not_idle_thread (fst ptr) s) &&& (\<lbrakk>cte_wp_at ((=) (Zombie ptr' zbits n)) ptr s; invs s\<rbrakk> \<Longrightarrow> not_idle_thread ptr' s)
theory Intent_DR

lemma tcb_cnode_index_def2:
  "n < 8 \<Longrightarrow> tcb_cnode_index n = bin_to_bl 3 (int n)" unfolding tcb_cnode_index_def to_bl_def by (simp add: uint_nat unat_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 8 \<Longrightarrow> tcb_cnode_index n = bin_to_bl 3 (int n) proof (prove)
goal (1 subgoal):
 1. n < 8 \<Longrightarrow> bin_to_bl LENGTH(3) (uint (word_of_nat n)) = bin_to_bl 3 (int n)
theory Intent_DR

lemma bl_to_bin_tcb_cnode_index:
  "n < 8 \<Longrightarrow> nat (bl_to_bin (tcb_cnode_index n)) = n" unfolding tcb_cnode_index_def by (simp add: unat_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 8 \<Longrightarrow> nat (bl_to_bin (tcb_cnode_index n)) = n proof (prove)
goal (1 subgoal):
 1. n < 8 \<Longrightarrow> nat (bl_to_bin (to_bl (word_of_nat n))) = n
theory Intent_DR

lemma transform_objects_kheap:
  "\<lbrakk> kheap s p = Some ko; p \<noteq> idle_thread s \<rbrakk>
     \<Longrightarrow> transform_objects s p = Some (transform_object (machine_state s) p (ekheap s p) ko)" unfolding transform_objects_def by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; p \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> transform_objects s p = Some (transform_object (machine_state s) p (ekheap s p) ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; p \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))) p = Some (transform_object (machine_state s) p (ekheap s p) ko)
theory Intent_DR

lemma transform_objects_tcb:
  "\<lbrakk> get_tcb ptr s = Some tcb; get_etcb ptr s = Some etcb; ptr \<noteq> idle_thread s\<rbrakk>
    \<Longrightarrow> transform_objects s ptr = Some (transform_tcb (machine_state s) ptr tcb etcb)" by (clarsimp dest!: get_tcb_SomeD simp: get_etcb_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb ptr s = Some tcb; get_etcb ptr s = Some etcb; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> transform_objects s ptr = Some (transform_tcb (machine_state s) ptr tcb etcb)
theory Intent_DR

lemma opt_cap_tcb:
  "\<lbrakk> get_tcb y s = Some tcb; (\<exists>etcb. get_etcb y s = Some etcb); y \<noteq> idle_thread s \<rbrakk> \<Longrightarrow>
  opt_cap (y, sl) (transform s) =
  (if sl \<in> tcb_abstract_slots then (option_map (\<lambda>(getF, _, _). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index sl)))
  else (if sl = tcb_pending_op_slot then (Some (infer_tcb_pending_op y (tcb_state tcb)))
   else (if sl = tcb_boundntfn_slot then (Some  (infer_tcb_bound_notification (tcb_bound_notification tcb))) else None)))" by (fastforce simp add: opt_cap_def KHeap_D.slots_of_def opt_object_tcb object_slots_def transform_tcb_def tcb_slots)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb y s = Some tcb; \<exists>etcb. get_etcb y s = Some etcb; y \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> opt_cap (y, sl) (transform s) = (if sl \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF tcb)) (tcb_cap_cases (tcb_cnode_index sl)) else if sl = tcb_pending_op_slot then Some (infer_tcb_pending_op y (tcb_state tcb)) else if sl = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification tcb)) else None)
theory Intent_DR

lemma cdl_objects_cnode:
  "\<lbrakk> kheap s' y = Some (CNode sz obj'); valid_idle s' ; sz \<noteq> 0\<rbrakk>
    \<Longrightarrow> cdl_objects (transform s') y =
    Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>)" apply (subgoal_tac "y \<noteq> idle_thread s'") apply (auto simp:obj_at_def is_cap_table_def valid_idle_def pred_tcb_at_def
                   transform_def transform_objects_def
             split:nat.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> cdl_objects (transform s') y = Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0; y \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> cdl_objects (transform s') y = Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>)
 2. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s' proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma cdl_objects_irq_node:
  "\<lbrakk> kheap s' y = Some (CNode 0 obj'); valid_idle s' \<rbrakk>
    \<Longrightarrow> cdl_objects (transform s') y =
    Some (cdl_object.IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>)" apply (subgoal_tac "y \<noteq> idle_thread s'") apply (auto simp:obj_at_def is_cap_table_def valid_idle_def pred_tcb_at_def
         transform_def transform_objects_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> cdl_objects (transform s') y = Some (IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'; y \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> cdl_objects (transform s') y = Some (IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>)
 2. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s' proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma transform_objects_cnode:
  "\<lbrakk> kheap s' y = Some (CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> transform_objects s' y =
    Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>)" apply (subgoal_tac "y \<noteq> idle_thread s'") apply (simp add: transform_objects_def) apply (clarsimp simp add: valid_idle_def obj_at_def pred_tcb_at_def split:nat.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> transform_objects s' y = Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0; y \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> transform_objects s' y = Some (cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>)
 2. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; 0 < sz; y \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> (case sz of 0 \<Rightarrow> IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr> | Suc nat \<Rightarrow> cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents (Suc nat) obj', cdl_cnode_size_bits = Suc nat\<rparr>) = cdl_object.CNode \<lparr>cdl_cnode_caps = transform_cnode_contents sz obj', cdl_cnode_size_bits = sz\<rparr>
 2. \<lbrakk>kheap s' y = Some (kernel_object.CNode sz obj'); valid_idle s'; sz \<noteq> 0\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s' proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma transform_objects_irq_node:
  "\<lbrakk> kheap s' y = Some (CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> transform_objects s' y =
    Some (cdl_object.IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>)" apply (subgoal_tac "y \<noteq> idle_thread s'") apply (simp add: transform_objects_def) apply (clarsimp simp add: valid_idle_def obj_at_def pred_tcb_at_def split:nat.split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> transform_objects s' y = Some (IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'; y \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> transform_objects s' y = Some (IRQNode \<lparr>cdl_irq_node_caps = transform_cnode_contents 0 obj'\<rparr>)
 2. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s' y = Some (kernel_object.CNode 0 obj'); valid_idle s'\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s' proof (prove)
goal:
No subgoals!
theory Intent_DR

lemma transform_objects_update_other:
  "\<lbrakk> kh ptr = Some ko; caps_of_object ko = caps_of_object ko'; a_type ko = a_type ko'; ref \<noteq> ptr \<rbrakk>
  \<Longrightarrow> transform_objects (update_kheap (kh(ptr \<mapsto> ko')) s) ref = transform_objects (update_kheap kh s) ref" unfolding transform_objects_def by (cases ref, simp_all add: restrict_map_def caps_of_state_update_same_caps
                               cap_installed_at_irq_def map_add_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh ptr = Some ko; caps_of_object ko = caps_of_object ko'; a_type ko = a_type ko'; ref \<noteq> ptr\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (kh(ptr \<mapsto> ko')) s) ref = transform_objects (update_kheap kh s) ref proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh ptr = Some ko; caps_of_object ko = caps_of_object ko'; a_type ko = a_type ko'; ref \<noteq> ptr\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)}) ++ (\<lambda>ptra. map_option (transform_object (machine_state (update_kheap (kh(ptr \<mapsto> ko')) s)) ptra ((ekheap (update_kheap (kh(ptr \<mapsto> ko')) s) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)})) ptra)) ((kheap (update_kheap (kh(ptr \<mapsto> ko')) s) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)})) ptra))) ref = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap kh s)}) ++ (\<lambda>ptr. map_option (transform_object (machine_state (update_kheap kh s)) ptr ((ekheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) ((kheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr))) ref
theory Intent_DR

lemma caps_of_object_update_state [simp]:
  "(\<lambda>n. map_option (\<lambda>(f, _). f (tcb_state_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_state_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_state_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 caps_of_object_update_boundntfn [simp]:
  "(\<lambda>n. map_option (\<lambda>(f, _). f (tcb_bound_notification_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_bound_notification_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_bound_notification_update stf tcb)) (tcb_cap_cases n) = map_option (\<lambda>(f, uu_). f tcb) (tcb_cap_cases n) proof (prove)
goal:
No subgoals!