theory Intent_DR

lemma tcb_cap_casesE:
  assumes cs: "tcb_cap_cases p = Some (gf, sf, restr)"
  and  rules: "\<lbrakk> p = tcb_cnode_index 0; gf = tcb_ctable; sf = tcb_ctable_update; restr = (\<lambda>_ _. \<top>) \<rbrakk> \<Longrightarrow> R"
              "\<lbrakk> p = tcb_cnode_index 1; gf = tcb_vtable; sf = tcb_vtable_update;
                 restr = (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
              "\<lbrakk> p = tcb_cnode_index 2; gf = tcb_reply; sf = tcb_reply_update;
                 restr = (\<lambda>t st c. (is_master_reply_cap c \<and> obj_ref_of c = t
                                        \<and> AllowGrant \<in> cap_rights c)
                                    \<or> (halted st \<and> (c = cap.NullCap))) \<rbrakk> \<Longrightarrow> R"
              "\<lbrakk> p = tcb_cnode_index 3; gf = tcb_caller; sf = tcb_caller_update;
                 restr = (\<lambda>_ st. case st of
                                       Structures_A.BlockedOnReceive e data \<Rightarrow>
                                         ((=) cap.NullCap)
                                     | _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
              "\<lbrakk> p = tcb_cnode_index 4; gf = tcb_ipcframe; sf = tcb_ipcframe_update; restr =
                                     (\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap)) \<rbrakk> \<Longrightarrow> R"
  shows "R" using cs unfolding tcb_cap_cases_def apply (simp split: if_split_asm del: One_nat_def) apply (erule rules, fastforce+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
tcb_cap_cases p = Some (gf, sf, restr)

goal (1 subgoal):
 1. R proof (prove)
using this:
[tcb_cnode_index 0 \<mapsto> (tcb_ctable, tcb_ctable_update, \<lambda>_ _ _. True), tcb_cnode_index 1 \<mapsto> (tcb_vtable, tcb_vtable_update, \<lambda>_ _. is_valid_vtable_root or (=) cap.NullCap), tcb_cnode_index 2 \<mapsto> (tcb_reply, tcb_reply_update, \<lambda>t st c. is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> Structures_A.cap_rights c \<or> halted st \<and> c = cap.NullCap), tcb_cnode_index 3 \<mapsto> (tcb_caller, tcb_caller_update, \<lambda>_ st. case st of BlockedOnReceive e data \<Rightarrow> (=) cap.NullCap | _ \<Rightarrow> is_reply_cap or (=) cap.NullCap), tcb_cnode_index 4 \<mapsto> (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap)] p = Some (gf, sf, restr)

goal (1 subgoal):
 1. R proof (prove)
goal (5 subgoals):
 1. \<lbrakk>p = tcb_cnode_index 4; tcb_ipcframe = gf \<and> tcb_ipcframe_update = sf \<and> (\<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap) = restr\<rbrakk> \<Longrightarrow> R
 2. \<lbrakk>p = tcb_cnode_index 3; tcb_caller = gf \<and> tcb_caller_update = sf \<and> (\<lambda>_. case_thread_state (is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap) (\<lambda>e data. (=) cap.NullCap) (\<lambda>word sender_payload_ext. is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap) (\<lambda>word. is_reply_cap or (=) cap.NullCap) (is_reply_cap or (=) cap.NullCap)) = restr\<rbrakk> \<Longrightarrow> R
 3. \<lbrakk>p = tcb_cnode_index 2; tcb_reply = gf \<and> tcb_reply_update = sf \<and> (\<lambda>t st c. is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> Structures_A.cap_rights c \<or> halted st \<and> c = cap.NullCap) = restr\<rbrakk> \<Longrightarrow> R
 4. \<lbrakk>p = tcb_cnode_index 1; tcb_vtable = gf \<and> tcb_vtable_update = sf \<and> (\<lambda>_ _. is_valid_vtable_root or (=) cap.NullCap) = restr\<rbrakk> \<Longrightarrow> R
 5. \<lbrakk>\<not> iszero (case case case take_bit_num 1 num.One of None \<Rightarrow> None | Some q \<Rightarrow> Some (num.Bit0 q) of None \<Rightarrow> None | Some q \<Rightarrow> Some (num.Bit0 q) of None \<Rightarrow> 0 | Some q \<Rightarrow> numeral q); p = tcb_cnode_index 0; tcb_ctable = gf \<and> tcb_ctable_update = sf \<and> (\<lambda>_ _ _. True) = restr\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!