kings-crown/FVELER_Isabelle huggingface dataset:
theory Arch_DR

lemma corres_return_r:
  "corres_underlying st nf nf' dc P P' a (do b; return () od) \<Longrightarrow> corres_underlying st nf nf' dc P P' a b" by (fastforce simp: bind_def dc_def return_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying st nf nf' dc P P' a (do b;
return ()
od) \<Longrightarrow> corres_underlying st nf nf' dc P P' a b
theory Arch_DR

lemma dcorres_assert_assume:
  "\<lbrakk> P' \<Longrightarrow> dcorres rr P Q f (g ()) \<rbrakk> \<Longrightarrow> dcorres rr P Q f (assert P' >>= g)" by (clarsimp simp: assert_def) (rule corres_free_fail)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P' \<Longrightarrow> dcorres rr P Q f (g ())) \<Longrightarrow> dcorres rr P Q f (assert P' >>= g)
theory Tcb_DR

lemma valid_vtable_root_update:
  "\<lbrakk> is_valid_vtable_root (CSpace_A.update_cap_data False x aa)\<rbrakk>
         \<Longrightarrow> CSpace_A.update_cap_data False x aa = aa" apply (clarsimp simp: update_cap_data_def badge_update_def is_valid_vtable_root_def Let_def
                        the_cnode_cap_def is_arch_cap_def arch_update_cap_data_def the_arch_cap_def
                  split: if_split_asm cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_valid_vtable_root (CSpace_A.update_cap_data False x aa) \<Longrightarrow> CSpace_A.update_cap_data False x aa = aa proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma is_cnode_cap_update_cap_data:
  "Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a) \<Longrightarrow> is_cnode_cap a" apply (case_tac a) apply (clarsimp simp:update_cap_data_def arch_update_cap_data_def is_arch_cap_def badge_update_def
      is_cap_simps split:if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a) \<Longrightarrow> Structures_A.is_cnode_cap a proof (prove)
goal (12 subgoals):
 1. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.NullCap\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 2. \<And>x21 x22 x23 x24. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 3. \<And>x31 x32 x33. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 4. \<And>x41 x42 x43. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 5. \<And>x51 x52 x53. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 6. \<And>x61 x62 x63. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 7. \<And>x7. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = ThreadCap x7\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 8. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = cap.DomainCap\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 9. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = IRQControlCap\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
 10. \<And>x10. \<lbrakk>Structures_A.is_cnode_cap (CSpace_A.update_cap_data x w a); a = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> Structures_A.is_cnode_cap a
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma dcorres_idempotent_as_user:
  "\<lbrakk> \<And>a. \<lbrace> \<lambda>s. s = a \<rbrace> x \<lbrace> \<lambda>_ s. s = a \<rbrace> \<rbrakk> \<Longrightarrow>
     dcorres dc \<top> (tcb_at u) (return q) (as_user u x)" apply (clarsimp simp: as_user_def) apply (clarsimp simp: corres_underlying_def bind_def split_def set_object_def get_object_def
                        return_def get_def put_def get_tcb_def gets_the_def gets_def assert_opt_def
                        tcb_at_def select_f_def valid_def
         split: option.split Structures_A.kernel_object.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrace>\<lambda>s. s = a\<rbrace> x \<lbrace>\<lambda>_ s. s = a\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at u) (return q) (as_user u x) proof (prove)
goal (1 subgoal):
 1. (\<And>a. \<lbrace>\<lambda>s. s = a\<rbrace> x \<lbrace>\<lambda>_ s. s = a\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) (tcb_at u) (return q) (do tcb <- gets_the (get_tcb u);
(a, uc') <- select_f (x (arch_tcb_context_get (tcb_arch tcb)));
y <- KHeap_A.set_object u (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od) proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma transform_full_intent_kheap_update_eq:
  "q \<noteq> u' \<Longrightarrow>
   transform_full_intent (machine_state (s\<lparr>kheap := (kheap s)(u' \<mapsto> x')\<rparr>)) q =
   transform_full_intent (machine_state s) q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. q \<noteq> u' \<Longrightarrow> transform_full_intent (machine_state (update_kheap ((kheap s)(u' \<mapsto> x')) s)) q = transform_full_intent (machine_state s) q
theory Tcb_DR

lemma runnable_imply:
  "runnable st
   \<Longrightarrow> (infer_tcb_pending_op obj_id st = RunningCap \<or>
    infer_tcb_pending_op obj_id st = RestartCap)" apply (case_tac st) apply (simp_all add:infer_tcb_pending_op_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. runnable st \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap proof (prove)
goal (8 subgoals):
 1. \<lbrakk>runnable st; st = Running\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 2. \<lbrakk>runnable st; inactive st\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 3. \<lbrakk>runnable st; st = Restart\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 4. \<And>x41 x42. \<lbrakk>runnable st; st = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 5. \<And>x51 x52. \<lbrakk>runnable st; st = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 6. \<lbrakk>runnable st; awaiting_reply st\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 7. \<And>x7. \<lbrakk>runnable st; st = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap
 8. \<lbrakk>runnable st; idle st\<rbrakk> \<Longrightarrow> infer_tcb_pending_op obj_id st = RunningCap \<or> infer_tcb_pending_op obj_id st = RestartCap proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma invoke_tcb_corres_copy_regs_loop:
  "dcorres dc \<top>
     (tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs)
     (corrupt_tcb_intent target_id)
     (mapM_x
        (\<lambda>r. do v \<leftarrow> as_user obj_id' (getRegister r);
                     as_user target_id (setRegister r v)
             od) x)" apply (clarsimp simp: mapM_x_mapM) apply (rule corres_guard_imp) apply (rule corres_dummy_return_l) apply (rule corres_split[OF Intent_DR.set_registers_corres corres_free_return[where P=\<top> and P'= \<top>]]) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs) (corrupt_tcb_intent target_id) (mapM_x (\<lambda>r. do v <- as_user obj_id' (getRegister r);
as_user target_id (setRegister r v)
od) x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs) (corrupt_tcb_intent target_id) (do x <- mapM (\<lambda>r. do v <- as_user obj_id' (getRegister r);
as_user target_id (setRegister r v)
od) x;
return ()
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (corrupt_tcb_intent target_id) (do x <- mapM (\<lambda>r. do v <- as_user obj_id' (getRegister r);
as_user target_id (setRegister r v)
od) x;
return ()
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (corrupt_tcb_intent target_id >>= return) (do x <- mapM (\<lambda>r. do v <- as_user obj_id' (getRegister r);
as_user target_id (setRegister r v)
od) x;
return ()
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs) s \<Longrightarrow> ?Q' s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> corrupt_tcb_intent target_id \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> mapM (\<lambda>r. do v <- as_user obj_id' (getRegister r);
as_user target_id (setRegister r v)
od) x \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 4. \<And>s. (tcb_at target_id and tcb_at obj_id' and valid_idle and not_idle_thread target_id and not_idle_thread obj_id' and valid_etcbs) s \<Longrightarrow> (tcb_at target_id and valid_idle and not_idle_thread target_id and valid_etcbs and ?Q'6) s proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma TPIDRURW_notin_msg_registers[simp]:
 "TPIDRURW \<notin> set msg_registers" apply (auto simp: msgRegisters_def frameRegisters_def gpRegisters_def
                    syscallMessage_def exceptionMessage_def msg_registers_def) apply (rule ccontr) apply clarsimp apply (simp_all add: upto_enum_red image_def) apply (auto simp add: toEnum_eq_to_fromEnum_eq fromEnum_def enum_register maxBound_def
              dest!: toEnum_eq_to_fromEnum_eq[THEN iffD1,rotated,OF sym]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. TPIDRURW \<notin> set msg_registers proof (prove)
goal (1 subgoal):
 1. TPIDRURW \<in> set [R2 .e. R5] \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TPIDRURW \<in> set [R2 .e. R5]; \<not> False\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. TPIDRURW \<in> set [R2 .e. R5] \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. fromEnum R2 \<le> fromEnum R5 \<and> (\<exists>x. (x = fromEnum R5 \<or> fromEnum R2 \<le> x \<and> x < fromEnum R5) \<and> TPIDRURW = toEnum x) \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma transform_full_intent_update_tpidrurw[simp]:
  "transform_full_intent ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>)
   = transform_full_intent ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set s (tcb_arch tcb)\<rparr>)" apply (clarsimp simp: transform_full_intent_def cap_register_def ARM.capRegister_def) by (fastforce simp: get_tcb_message_info_def msg_info_register_def ARM.msgInfoRegister_def
                       get_tcb_mrs_def get_ipc_buffer_words_def Suc_le_eq Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_full_intent ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>) = transform_full_intent ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set s (tcb_arch tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. (let mi = get_tcb_message_info (tcb\<lparr>tcb_arch := arch_tcb_context_set (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>) in \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label mi)) (get_tcb_mrs ms (tcb\<lparr>tcb_arch := arch_tcb_context_set (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>)), cdl_intent_error = guess_error (mi_label mi), cdl_intent_cap = s R0, cdl_intent_extras = get_ipc_buffer_words ms (tcb\<lparr>tcb_arch := arch_tcb_context_set (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)], cdl_intent_recv_slot = case get_ipc_buffer_words ms (tcb\<lparr>tcb_arch := arch_tcb_context_set (s(TPIDRURW := a)) (tcb_arch tcb)\<rparr>) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None\<rparr>) = (let mi = get_tcb_message_info (tcb\<lparr>tcb_arch := arch_tcb_context_set s (tcb_arch tcb)\<rparr>) in \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label mi)) (get_tcb_mrs ms (tcb\<lparr>tcb_arch := arch_tcb_context_set s (tcb_arch tcb)\<rparr>)), cdl_intent_error = guess_error (mi_label mi), cdl_intent_cap = s R0, cdl_intent_extras = get_ipc_buffer_words ms (tcb\<lparr>tcb_arch := arch_tcb_context_set s (tcb_arch tcb)\<rparr>) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)], cdl_intent_recv_slot = case get_ipc_buffer_words ms (tcb\<lparr>tcb_arch := arch_tcb_context_set s (tcb_arch tcb)\<rparr>) [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None\<rparr>)
theory Tcb_DR

lemma as_user_valid_irq_node[wp]:
  "\<lbrace>valid_irq_node\<rbrace>
    as_user y (set_register a v)
  \<lbrace>\<lambda>rv. valid_irq_node\<rbrace>" apply (simp add: valid_irq_node_def cap_table_at_typ) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift | wps )+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_node\<rbrace> as_user y (set_register a v) \<lbrace>\<lambda>rv. valid_irq_node\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s)\<rbrace> as_user y (set_register a v) \<lbrace>\<lambda>rv s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> as_user y (set_register a v) \<lbrace>\<lambda>rv s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s)\<rbrace>
 2. \<And>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. inj (interrupt_irq_node s) \<and> (\<forall>irq. typ_at (ACapTable 0) (interrupt_irq_node s irq) s) \<Longrightarrow> inj (interrupt_irq_node s) \<and> (\<forall>x. typ_at (ACapTable 0) (interrupt_irq_node s x) s) proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma set_register_TPIDRURW_tcb_abstract_inv[wp]:
  "\<lbrace>\<lambda>cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>
     setRegister TPIDRURW a
   \<lbrace>\<lambda>_ cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>" by (simp add: setRegister_def simpler_modify_def valid_def transform_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace> setRegister TPIDRURW a \<lbrace>\<lambda>_ cxt. P (transform_tcb ms ref (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>) etcb)\<rbrace>
theory Tcb_DR

lemma tcb_fault_fault_handler_upd:
  "tcb_fault (obj'\<lparr>tcb_fault_handler := a\<rparr>) = tcb_fault obj'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_fault (obj'\<lparr>tcb_fault_handler := a\<rparr>) = tcb_fault obj'
theory Tcb_DR

lemma check_cap_at_stable:
  "\<lbrace>P\<rbrace>f\<lbrace>\<lambda>r. P\<rbrace>
   \<Longrightarrow>\<lbrace>P\<rbrace>check_cap_at aa b (check_cap_at aaa bb (f)) \<lbrace>\<lambda>r. P\<rbrace>" apply (clarsimp simp:check_cap_at_def not_idle_thread_def) apply (wp | simp split:if_splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> check_cap_at aa b (check_cap_at aaa bb f) \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> do cap' <- CSpaceAcc_A.get_cap b;
when (same_object_as aa cap') (do cap' <- CSpaceAcc_A.get_cap bb;
when (same_object_as aaa cap') f
od)
od \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma case_option_wp:
  "(\<And>x. \<lbrace>P x\<rbrace>a\<lbrace>\<lambda>r. Q x\<rbrace>) \<Longrightarrow> \<lbrace>case_option \<top> P z\<rbrace>a\<lbrace>\<lambda>r. case_option \<top> Q z\<rbrace>" by (clarsimp split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> a \<lbrace>\<lambda>r. Q x\<rbrace>) \<Longrightarrow> \<lbrace>case z of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> P x\<rbrace> a \<lbrace>\<lambda>r. case z of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> Q x\<rbrace>
theory Tcb_DR

lemma hoare_case_some:
  "\<lbrace>P\<rbrace>a\<lbrace>\<lambda>r s. Q s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. case x of None \<Rightarrow> True | Some y \<Rightarrow> P s\<rbrace> a
    \<lbrace>\<lambda>rv s. case x of None \<Rightarrow> True | Some y \<Rightarrow> Q s\<rbrace>" apply (case_tac x) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. case x of None \<Rightarrow> True | Some y \<Rightarrow> P s\<rbrace> a \<lbrace>\<lambda>rv s. case x of None \<Rightarrow> True | Some y \<Rightarrow> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. Q\<rbrace>; x = None\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x of None \<Rightarrow> True | Some y \<Rightarrow> P s\<rbrace> a \<lbrace>\<lambda>rv s. case x of None \<Rightarrow> True | Some y \<Rightarrow> Q s\<rbrace>
 2. \<And>aa. \<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>\<lambda>r. Q\<rbrace>; x = Some aa\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. case x of None \<Rightarrow> True | Some y \<Rightarrow> P s\<rbrace> a \<lbrace>\<lambda>rv s. case x of None \<Rightarrow> True | Some y \<Rightarrow> Q s\<rbrace> proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma case_option_wpE:
  "(\<And>x. \<lbrace>P x\<rbrace>a\<lbrace>\<lambda>r. Q x\<rbrace>,-) \<Longrightarrow> \<lbrace>case_option \<top> P z\<rbrace>a\<lbrace>\<lambda>r. case_option \<top> Q z\<rbrace>,-" by (clarsimp split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> a \<lbrace>\<lambda>r. Q x\<rbrace>, -) \<Longrightarrow> \<lbrace>case z of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> P x\<rbrace> a \<lbrace>\<lambda>r. case z of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> Q x\<rbrace>, -
theory Tcb_DR

lemma option_update_thread_not_idle_thread[wp]:
  "\<lbrace>not_idle_thread x and not_idle_thread a\<rbrace>option_update_thread a b c\<lbrace>\<lambda>r. not_idle_thread x\<rbrace>" apply(simp add: option_update_thread_def) apply (rule hoare_pre) apply wpc apply wp apply (clarsimp simp: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp simp: not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread x and not_idle_thread a\<rbrace> option_update_thread a b c \<lbrace>\<lambda>r. not_idle_thread x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread x and not_idle_thread a\<rbrace> case c of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (b v) a \<lbrace>\<lambda>r. not_idle_thread x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case c of None \<Rightarrow> return () | Some v \<Rightarrow> thread_set (b v) a \<lbrace>\<lambda>r. not_idle_thread x\<rbrace>
 2. \<And>s. (not_idle_thread x and not_idle_thread a) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. c = None \<Longrightarrow> \<lbrace>?R11\<rbrace> return () \<lbrace>\<lambda>r. not_idle_thread x\<rbrace>
 2. \<And>x2. c = Some x2 \<Longrightarrow> \<lbrace>?R12 x2\<rbrace> thread_set (b x2) a \<lbrace>\<lambda>r. not_idle_thread x\<rbrace>
 3. \<And>s. (not_idle_thread x and not_idle_thread a) s \<Longrightarrow> (c = None \<longrightarrow> ?R11 s) \<and> (\<forall>x. c = Some x \<longrightarrow> ?R12 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x2. c = Some x2 \<Longrightarrow> \<lbrace>?R12 x2\<rbrace> thread_set (b x2) a \<lbrace>\<lambda>r. not_idle_thread x\<rbrace>
 2. \<And>s. (not_idle_thread x and not_idle_thread a) s \<Longrightarrow> (c = None \<longrightarrow> not_idle_thread x s) \<and> (\<forall>x. c = Some x \<longrightarrow> ?R12 x s) proof (prove)
goal (2 subgoals):
 1. \<And>x2. c = Some x2 \<Longrightarrow> \<lbrace>?R12 x2\<rbrace> do tcb <- gets_the (get_tcb a);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (update_kheap ((kheap s)(a \<mapsto> TCB (b x2 tcb))) s)
od \<lbrace>\<lambda>r. not_idle_thread x\<rbrace>
 2. \<And>s. (not_idle_thread x and not_idle_thread a) s \<Longrightarrow> (c = None \<longrightarrow> not_idle_thread x s) \<and> (\<forall>x. c = Some x \<longrightarrow> ?R12 x s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (not_idle_thread x and not_idle_thread a) s \<Longrightarrow> (c = None \<longrightarrow> not_idle_thread x s) \<and> (\<forall>xa. c = Some xa \<longrightarrow> get_tcb a s \<noteq> None \<longrightarrow> (\<exists>y. kheap s a = Some y) \<longrightarrow> a_type (the (kheap s a)) = ATCB \<longrightarrow> not_idle_thread x (update_kheap ((kheap s)(a \<mapsto> TCB (b xa (the (get_tcb a s))))) s)) proof (prove)
goal:
No subgoals!
theory Tcb_DR

lemma reschedule_required_transform: "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reschedule_required \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (clarsimp simp: reschedule_required_def set_scheduler_action_def etcb_at_def
     | wp tcb_sched_action_transform | wpc | assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> reschedule_required \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory Tcb_DR

lemma possible_switch_to_transform:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> possible_switch_to tptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" unfolding possible_switch_to_def by (wpsimp wp: tcb_sched_action_transform reschedule_required_transform set_scheduler_action_transform_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> possible_switch_to tptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do cur_dom <- gets cur_domain;
target_dom <- ethread_get tcb_domain tptr;
action <- gets scheduler_action;
if target_dom \<noteq> cur_dom then tcb_sched_action tcb_sched_enqueue tptr else if action \<noteq> resume_cur_thread then do reschedule_required;
tcb_sched_action tcb_sched_enqueue tptr
od else set_scheduler_action $ switch_thread tptr
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace>