kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_DP

lemma lookup_slot_wp:
  "\<lbrace>P\<rbrace> lookup_slot cnode_ptr ptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: lookup_slot_def) apply (clarsimp simp: gets_the_resolve_cap[symmetric] split_def) apply (wp get_cap_wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookup_slot cnode_ptr ptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE cspace_root <- liftE (get_cap (cnode_ptr, tcb_cspace_slot));
(slot, uu_) <- resolve_address_bits cspace_root ptr word_bits;
returnOk slot
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE cspace_root <- liftE (get_cap (cnode_ptr, tcb_cspace_slot));
p <- gets_the (resolve_cap cspace_root ptr word_bits);
returnOk (fst p)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> P s proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma always_empty_wp:
  "\<lbrace><ptr  \<mapsto>c - \<and>* R>\<rbrace>
     always_empty_slot ptr
   \<lbrace>\<lambda>_. < ptr  \<mapsto>c NullCap \<and>* R>\<rbrace>" by (clarsimp simp: always_empty_slot_def, wp remove_parent_wp set_cap_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ptr \<mapsto>c - \<and>* R)\<rbrace> always_empty_slot ptr \<lbrace>\<lambda>_. cdl.lift (ptr \<mapsto>c NullCap \<and>* R)\<rbrace>
theory KHeap_DP

lemma fast_finalise_cap_non_ep_wp:
  "\<lbrace><P> and K (\<not> ep_related_cap cap') \<rbrace> fast_finalise cap' final \<lbrace>\<lambda>y. <P>\<rbrace>" by (case_tac cap',simp_all add:ep_related_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift P and K (\<not> ep_related_cap cap')\<rbrace> fast_finalise cap' final \<lbrace>\<lambda>y. cdl.lift P\<rbrace>
theory KHeap_DP

lemma is_cnode_cap_has_object [simp]:
  "is_cnode_cap cnode_cap \<Longrightarrow> cap_has_object cnode_cap" by (clarsimp simp: cap_type_def cap_has_object_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cnode_cap \<Longrightarrow> cap_has_object cnode_cap
theory KHeap_DP

lemma K_extract:
  "(K P \<and>* Q) s \<Longrightarrow> P" by (auto simp: sep_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (K P \<and>* Q) s \<Longrightarrow> P
theory KHeap_DP

lemma user_pointer_at_cnode_cap':
  "(\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap') s
  \<Longrightarrow> is_cnode_cap cnode_cap" by (clarsimp simp: user_pointer_at_def Let_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap') s \<Longrightarrow> is_cnode_cap cnode_cap
theory KHeap_DP

lemma user_pointer_at_cnode_cap:
  "(\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s
  \<Longrightarrow> is_cnode_cap cnode_cap" by (drule sep_conj_impl, erule user_pointer_at_cnode_cap', assumption+, erule K_extract')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<box> (r, word_bits) : cnode_cap cap_ptr \<mapsto>u cap' \<and>* R) s \<Longrightarrow> is_cnode_cap cnode_cap
theory KHeap_DP

lemma lookup_cap_wp:
  "\<lbrace>P\<rbrace> lookup_cap thread cap_ptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_ .P \<rbrace> " apply (clarsimp simp: lookup_cap_def) apply (wp lookup_slot_wp get_cap_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> lookup_cap thread cap_ptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE slot <- lookup_slot thread cap_ptr;
liftE (get_cap slot)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma update_cap_data:
  "\<lbrace>\<lambda>s. valid_src_cap cap badge \<and> cap_has_type cap
   \<and> ((is_ep_cap cap \<or> is_ntfn_cap cap) \<longrightarrow> \<not> preserve \<and> cap_badge cap = 0)
   \<and> Q (update_cap_data_det badge cap) s \<rbrace>
  update_cap_data preserve badge cap
  \<lbrace>\<lambda>rv s. Q rv s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: Let_def update_cap_data_def update_cap_data_det_def
                        valid_src_cap_def
                        cnode_cap_size_def ep_related_cap_def guard_update_def
                 split: cdl_cap.splits | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_src_cap cap badge \<and> cap_has_type cap \<and> (is_ep_cap cap \<or> is_ntfn_cap cap \<longrightarrow> \<not> preserve \<and> cap_badge cap = 0) \<and> Q (update_cap_data_det badge cap) s\<rbrace> update_cap_data preserve badge cap \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_src_cap cap badge \<and> cap_has_type cap \<and> (is_ep_cap cap \<or> is_ntfn_cap cap \<longrightarrow> \<not> preserve \<and> cap_badge cap = 0) \<and> Q (update_cap_data_det badge cap) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> update_cap_data preserve badge cap \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma cap_object_update_cap_rights:
  "cap_object (update_cap_rights rights src_cap) = cap_object src_cap" apply (simp add: cap_object_def update_cap_rights_def
            split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_object (update_cap_rights rights src_cap) = cap_object src_cap proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma derived_cap_update_cap_data_det_NullCap [simp]:
  "(derived_cap (update_cap_data_det badge cap) = NullCap)
 = (derived_cap cap = NullCap)" by (clarsimp simp: derived_cap_def update_cap_data_det_def
                     badge_update_def update_cap_badge_def guard_update_def
              split: cdl_cap.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (derived_cap (update_cap_data_det badge cap) = NullCap) = (derived_cap cap = NullCap)
theory KHeap_DP

lemma derived_cap_update_cap_rights_NullCap [simp]:
  "(derived_cap (update_cap_rights rights cap) = NullCap)
 = (derived_cap cap = NullCap)" by (clarsimp simp: derived_cap_def update_cap_rights_def
              split: cdl_cap.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (derived_cap (update_cap_rights rights cap) = NullCap) = (derived_cap cap = NullCap)
theory KHeap_DP

lemma derived_cap_reset_cap_asid_NullCap:
  "\<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; derived_cap cap = NullCap\<rbrakk>
  \<Longrightarrow> derived_cap cap' = NullCap" by (clarsimp simp: derived_cap_def reset_cap_asid_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; derived_cap cap = NullCap\<rbrakk> \<Longrightarrow> derived_cap cap' = NullCap
theory KHeap_DP

lemma derived_cap_update_cap_data_det:
  "derived_cap (update_cap_data_det badge cap) =
   update_cap_data_det badge (derived_cap cap)" apply (clarsimp simp: derived_cap_def update_cap_data_det_def) apply (case_tac cap, simp_all add: update_cap_data_det_def badge_update_def
                                     derived_cap_def update_cap_badge_def guard_update_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. derived_cap (update_cap_data_det badge cap) = update_cap_data_det badge (derived_cap cap) proof (prove)
goal (1 subgoal):
 1. (case case cap of EndpointCap x b xa \<Rightarrow> badge_update badge cap | NotificationCap x b xa \<Rightarrow> badge_update badge cap | CNodeCap object g gs x \<Rightarrow> guard_update cap badge | _ \<Rightarrow> cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> case cap of EndpointCap x b xa \<Rightarrow> badge_update badge cap | NotificationCap x b xa \<Rightarrow> badge_update badge cap | CNodeCap object g gs x \<Rightarrow> guard_update cap badge | _ \<Rightarrow> cap) = (case case cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> cap of EndpointCap x b xa \<Rightarrow> badge_update badge (case cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> cap) | NotificationCap x b xa \<Rightarrow> badge_update badge (case cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> cap) | CNodeCap object g gs x \<Rightarrow> guard_update (case cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> cap) badge | _ \<Rightarrow> case cap of ReplyCap x xa \<Rightarrow> NullCap | MasterReplyCap x \<Rightarrow> NullCap | IrqControlCap \<Rightarrow> NullCap | FrameCap d p r sz b x \<Rightarrow> FrameCap d p r sz b None | ZombieCap x \<Rightarrow> NullCap | _ \<Rightarrow> cap) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma cnode_cap_size_upd_cap_rights[simp]:
  "is_cnode_cap src_cap
  \<Longrightarrow> cnode_cap_size (update_cap_rights rights src_cap) = cnode_cap_size src_cap" by (simp add: update_cap_rights_def cnode_cap_size_def
         split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap src_cap \<Longrightarrow> cnode_cap_size (update_cap_rights rights src_cap) = cnode_cap_size src_cap
theory KHeap_DP

lemma cap_has_type_update_rights[simp]:
  "cap_has_type (update_cap_rights rights cap) = cap_has_type cap" by (clarsimp simp: cap_type_def update_cap_rights_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_has_type (update_cap_rights rights cap) = cap_has_type cap
theory KHeap_DP

lemma cap_has_type_asid_cong:
  "reset_cap_asid cap' = reset_cap_asid src_cap
  \<Longrightarrow> cap_has_type cap' = cap_has_type src_cap" by (drule reset_cap_asid_cap_type, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap' = reset_cap_asid src_cap \<Longrightarrow> cap_has_type cap' = cap_has_type src_cap
theory KHeap_DP

lemma ep_related_capI:
  "is_ep_cap cap \<Longrightarrow> ep_related_cap cap"
  "is_ntfn_cap cap \<Longrightarrow> ep_related_cap cap"
  "is_reply_cap cap \<Longrightarrow> ep_related_cap cap" by (cases cap; simp add: ep_related_cap_def cap_type_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (is_ep_cap cap \<Longrightarrow> ep_related_cap cap) &&& (is_ntfn_cap cap \<Longrightarrow> ep_related_cap cap) &&& (is_reply_cap cap \<Longrightarrow> ep_related_cap cap)
theory KHeap_DP

lemma non_cap_cong:
  "reset_cap_asid cap' = reset_cap_asid src_cap
  \<Longrightarrow> (cap' = NullCap) = (src_cap = NullCap)" by (rule iffI,simp_all add:reset_cap_asid_def
    split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap' = reset_cap_asid src_cap \<Longrightarrow> (cap' = NullCap) = (src_cap = NullCap)
theory KHeap_DP

lemma update_cap_data_non:
  "(update_cap_data_det badge cap' = NullCap) = (cap' = NullCap)" by (rule iffI,
      simp_all add: update_cap_data_det_def badge_update_def
                    guard_update_def update_cap_badge_def
             split: cdl_cap.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (update_cap_data_det badge cap' = NullCap) = (cap' = NullCap)
theory KHeap_DP

lemma do_kernel_op_pull_back:
  "\<lbrace>\<lambda>s. P s\<rbrace> oper \<lbrace>\<lambda>r. Q r\<rbrace> \<Longrightarrow>
   \<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do_kernel_op oper \<lbrace>\<lambda>r s. Q r (kernel_state s)\<rbrace>" apply (simp add:do_kernel_op_def) apply (wp|wpc)+ apply (auto simp:valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> oper \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do_kernel_op oper \<lbrace>\<lambda>r s. Q r (kernel_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> oper \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do ms <- gets kernel_state;
(r, ms') <- select_f (oper ms);
y <- modify (kernel_state_update (\<lambda>_. ms'));
return r
od \<lbrace>\<lambda>r s. Q r (kernel_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> oper \<lbrace>Q\<rbrace>; P (kernel_state s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (oper (kernel_state s)). \<forall>xa xb. x = (xa, xb) \<longrightarrow> Q xa (kernel_state (s\<lparr>kernel_state := xb\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma get_thread_inv:
  "\<lbrace> Q \<rbrace> get_thread thread \<lbrace>\<lambda>t s. Q s\<rbrace>" unfolding get_thread_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> get_thread thread \<lbrace>\<lambda>t. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> do t <- get_object thread;
case t of Tcb tcb \<Rightarrow> return tcb | _ \<Rightarrow> fail
od \<lbrace>\<lambda>t. Q\<rbrace>
theory KHeap_DP

lemma get_thread_sep_wp_precise:
  "\<lbrace>\<lambda>s. tcb_at' (\<lambda>tcb. Q tcb s) thread s \<rbrace>
    get_thread thread
   \<lbrace>\<lambda>rv. Q rv\<rbrace>" apply (simp add:get_thread_def | wp | wpc)+ apply (auto simp: object_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at' (\<lambda>tcb. Q tcb s) thread s\<rbrace> get_thread thread \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' (\<lambda>tcb. Q tcb s) thread s \<Longrightarrow> (\<exists>y. cdl_objects s thread = Some y) \<longrightarrow> (the (cdl_objects s thread) = Endpoint \<longrightarrow> ?R32 (ds_id Endpoint) s) \<and> (the (cdl_objects s thread) = Notification \<longrightarrow> ?R33 (ds_id Notification) s) \<and> (\<forall>x. the (cdl_objects s thread) = Tcb x \<longrightarrow> Q x s) \<and> (\<forall>x. the (cdl_objects s thread) = CNode x \<longrightarrow> ?R35 (CNode x) x s) \<and> (\<forall>x. the (cdl_objects s thread) = AsidPool x \<longrightarrow> ?R36 (AsidPool x) x s) \<and> (\<forall>x. the (cdl_objects s thread) = PageTable x \<longrightarrow> ?R37 (PageTable x) x s) \<and> (\<forall>x. the (cdl_objects s thread) = PageDirectory x \<longrightarrow> ?R38 (PageDirectory x) x s) \<and> (\<forall>x. the (cdl_objects s thread) = Frame x \<longrightarrow> ?R39 (Frame x) x s) \<and> (the (cdl_objects s thread) = Untyped \<longrightarrow> ?R40 (ds_id Untyped) s) \<and> (\<forall>x. the (cdl_objects s thread) = IRQNode x \<longrightarrow> ?R41 (IRQNode x) x s) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma has_restart_cap_sep_wp:
  "\<lbrace>\<lambda>s. < (thread,tcb_pending_op_slot) \<mapsto>c cap \<and>* sep_true> s \<and> Q (cap = RestartCap) s\<rbrace>
    has_restart_cap thread
   \<lbrace>\<lambda>rv. Q rv\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: object_at_def) apply (wpsimp simp: object_at_def get_thread_def has_restart_cap_def | intro conjI)+ apply (clarsimp dest!: opt_cap_sep_imp
                   simp: opt_cap_def slots_of_def) apply (clarsimp simp: object_slots_def) apply (erule rsubst) apply (clarsimp simp: reset_cap_asid_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>s. True)) s \<and> Q (cap = RestartCap) s\<rbrace> has_restart_cap thread \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>s. True)) s \<and> Q (cap = RestartCap) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> has_restart_cap thread \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>s. True)) s; Q (cap = RestartCap) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> has_restart_cap thread \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa x. \<lbrakk>cdl.lift ((thread, tcb_pending_op_slot) \<mapsto>c cap \<and>* (\<lambda>s. True)) sa; Q (cap = RestartCap) sa; cdl_objects sa thread = Some (Tcb x)\<rbrakk> \<Longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa x cap'. \<lbrakk>Q (cap = RestartCap) sa; cdl_objects sa thread = Some (Tcb x); object_slots (Tcb x) tcb_pending_op_slot = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cdl_tcb_caps x tcb_pending_op_slot = Some RestartCap) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa x cap'. \<lbrakk>Q (cap = RestartCap) sa; cdl_objects sa thread = Some (Tcb x); cdl_tcb_caps x tcb_pending_op_slot = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cap' = RestartCap) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa x cap'. \<lbrakk>cdl_objects sa thread = Some (Tcb x); cdl_tcb_caps x tcb_pending_op_slot = Some cap'; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> Q (cap = RestartCap) sa = Q (cap' = RestartCap) sa proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma lift_do_kernel_op':
  "\<lbrace>\<lambda>s'. P s'\<rbrace> f \<lbrace>\<lambda>_ s'. Q s'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do_kernel_op f \<lbrace>\<lambda>_ s. Q (kernel_state s)\<rbrace>" apply (simp add: do_kernel_op_def split_def) apply wp apply (simp add: valid_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do_kernel_op f \<lbrace>\<lambda>_ s. Q (kernel_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P (kernel_state s)\<rbrace> do ms <- gets kernel_state;
p <- select_f (f ms);
y <- modify (kernel_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_ s. Q (kernel_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; P (kernel_state s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (kernel_state s)). Q (kernel_state (s\<lparr>kernel_state := snd x\<rparr>)) proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma lift_do_kernel_op:
  "\<lbrace>\<lambda>s. s = s'\<rbrace> f \<lbrace>\<lambda>_ s. s = s'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. (kernel_state s) = s'\<rbrace> do_kernel_op f \<lbrace>\<lambda>_ s. (kernel_state s) = s'\<rbrace>" apply (simp add: do_kernel_op_def split_def) apply wp apply (simp add: valid_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = s'\<rbrace> f \<lbrace>\<lambda>_ s. s = s'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. kernel_state s = s'\<rbrace> do_kernel_op f \<lbrace>\<lambda>_ s. kernel_state s = s'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = s'\<rbrace> f \<lbrace>\<lambda>_ s. s = s'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. kernel_state s = s'\<rbrace> do ms <- gets kernel_state;
p <- select_f (f ms);
y <- modify (kernel_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_ s. kernel_state s = s'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>\<lambda>s. s = s'\<rbrace> f \<lbrace>\<lambda>_ s. s = s'\<rbrace>; kernel_state s = s'\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f (kernel_state s)). kernel_state (s\<lparr>kernel_state := snd x\<rparr>) = s' proof (prove)
goal:
No subgoals!
theory KHeap_DP

lemma switch_to_thread_wp:
  "\<lbrace>\<lambda>s. P (cdl_objects s)\<rbrace>
   switch_to_thread t
   \<lbrace>\<lambda>r s. P (cdl_objects s)\<rbrace>" by (wpsimp simp: switch_to_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_objects s)\<rbrace> switch_to_thread t \<lbrace>\<lambda>r s. P (cdl_objects s)\<rbrace>
theory KHeap_DP

lemma switch_to_thread_current_thread_wp:
  "\<lbrace>\<lambda>s. P t\<rbrace>
   switch_to_thread t
   \<lbrace>\<lambda>r s. P (cdl_current_thread s)\<rbrace>" by (wpsimp simp: switch_to_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P t\<rbrace> switch_to_thread t \<lbrace>\<lambda>r s. P (cdl_current_thread s)\<rbrace>
theory KHeap_DP

lemma schedule_no_choice_wp:
  "\<lbrace>\<lambda>s.  cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<and> P s \<rbrace>
    schedule
  \<lbrace>\<lambda>r s. cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<longrightarrow>  P s\<rbrace>" apply (simp add:schedule_def  switch_to_thread_def change_current_domain_def) apply wp apply (case_tac s,clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<and> P s\<rbrace> schedule \<lbrace>\<lambda>r s. cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<longrightarrow> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<and> P s\<rbrace> do y <- do next_domain <- select UNIV;
modify (cdl_current_domain_update (\<lambda>_. next_domain))
od;
next_domain <- gets cdl_current_domain;
threads <- gets (active_tcbs_in_domain next_domain);
next_thread <- select threads;
modify (cdl_current_thread_update (\<lambda>_. Some next_thread))
od \<sqinter> do y <- do next_domain <- select UNIV;
modify (cdl_current_domain_update (\<lambda>_. next_domain))
od;
modify (cdl_current_thread_update (\<lambda>_. None))
od \<lbrace>\<lambda>r s. cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<longrightarrow> P s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl_current_thread s = Some current_thread \<and> cdl_current_domain s = current_domain \<and> P s \<Longrightarrow> ((\<lambda>s. \<forall>x\<in>UNIV. \<forall>xa\<in>active_tcbs_in_domain (cdl_current_domain (s\<lparr>cdl_current_domain := x\<rparr>)) (s\<lparr>cdl_current_domain := x\<rparr>). cdl_current_thread (s\<lparr>cdl_current_domain := x, cdl_current_thread := Some xa\<rparr>) = Some current_thread \<and> cdl_current_domain (s\<lparr>cdl_current_domain := x, cdl_current_thread := Some xa\<rparr>) = current_domain \<longrightarrow> P (s\<lparr>cdl_current_domain := x, cdl_current_thread := Some xa\<rparr>)) and (\<lambda>s. \<forall>x\<in>UNIV. cdl_current_thread (s\<lparr>cdl_current_domain := x, cdl_current_thread := None\<rparr>) = Some current_thread \<and> cdl_current_domain (s\<lparr>cdl_current_domain := x, cdl_current_thread := None\<rparr>) = current_domain \<longrightarrow> P (s\<lparr>cdl_current_domain := x, cdl_current_thread := None\<rparr>))) s proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Examples

lemma frame_rule:
  "\<And>R. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P \<and>* R\<rbrace> f \<lbrace>\<lambda>_. Q \<and>* R\<rbrace>" oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>R. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P \<and>* R\<rbrace> f \<lbrace>\<lambda>_. Q \<and>* R\<rbrace>