kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_AI

lemma cap_delete_one_deletes[wp]:
  "\<lbrace>\<top>\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) ptr\<rbrace>" apply (simp add: cap_delete_one_def unless_def) apply (wp get_cap_wp) apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do cap <- get_cap ptr;
when (cap \<noteq> NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot ptr NullCap
od)
od \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) ptr s \<longrightarrow> (if cap \<noteq> NullCap then \<lambda>s. True else cte_wp_at (\<lambda>c. c = NullCap) ptr) s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cap_delete_one_reply_st_tcb_at:
  "\<lbrace>pred_tcb_at proj P t and cte_wp_at (is_reply_cap_to t') slot\<rbrace>
    cap_delete_one slot
   \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (rule hoare_seq_ext [OF _ get_cap_sp]) apply (rule hoare_assume_pre) apply (clarsimp simp: cte_wp_at_caps_of_state when_def is_reply_cap_to_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t and cte_wp_at (is_reply_cap_to t') slot\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t and cte_wp_at (is_reply_cap_to t') slot\<rbrace> do cap <- get_cap slot;
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot slot NullCap
od)
od \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrace>pred_tcb_at proj P t and cte_wp_at (is_reply_cap_to t') slot and cte_wp_at (\<lambda>c. c = cap) slot\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot slot NullCap
od) \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap s. (pred_tcb_at proj P t and cte_wp_at (is_reply_cap_to t') slot and cte_wp_at (\<lambda>c. c = cap) slot) s \<Longrightarrow> \<lbrace>pred_tcb_at proj P t and cte_wp_at (is_reply_cap_to t') slot and cte_wp_at (\<lambda>c. c = cap) slot\<rbrace> when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot slot NullCap
od) \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s rights. \<lbrakk>pred_tcb_at proj P t s; caps_of_state s slot = Some (ReplyCap t' False rights)\<rbrakk> \<Longrightarrow> \<lbrace>pred_tcb_at proj P t and cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t' False rights) slot and cte_wp_at (\<lambda>c. c = ReplyCap t' False rights) slot\<rbrace> do final <- gets (is_final_cap' (ReplyCap t' False rights));
empty_slot slot NullCap
od \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma unbind_notification_cte_cap_to[wp]:
"\<lbrace>ex_cte_cap_wp_to P sl\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>" by (wp ex_cte_cap_to_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P sl\<rbrace> unbind_notification t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>
theory Finalise_AI

lemma unbind_maybe_notification_cte_cap_to[wp]:
"\<lbrace>ex_cte_cap_wp_to P sl\<rbrace> unbind_maybe_notification t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>" by (wp ex_cte_cap_to_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P sl\<rbrace> unbind_maybe_notification t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>
theory Finalise_AI

lemma fast_finalise_st_tcb_at:
  "\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace>
     fast_finalise cap fin
   \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (rule hoare_gen_asm) apply (cases cap; wpsimp wp: cancel_all_ipc_st_tcb_at cancel_all_signals_st_tcb_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace> fast_finalise cap fin \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>st. active st \<longrightarrow> P st \<Longrightarrow> \<lbrace>st_tcb_at P t\<rbrace> fast_finalise cap fin \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cap_delete_one_st_tcb_at:
  "\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace>
     cap_delete_one ptr
   \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (simp add: cap_delete_one_def unless_def is_final_cap_def) apply (wpsimp wp: fast_finalise_st_tcb_at get_cap_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st)\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t and (\<lambda>y. \<forall>st. (st = Running \<longrightarrow> P Running) \<and> (st = Restart \<longrightarrow> P Restart))\<rbrace> do cap <- get_cap ptr;
when (cap \<noteq> NullCap) (do final <- gets (is_final_cap' cap);
y <- fast_finalise cap final;
empty_slot ptr NullCap
od)
od \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma can_fast_finalise_Null:
  "can_fast_finalise cap.NullCap" by (simp add: can_fast_finalise_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. can_fast_finalise NullCap
theory Finalise_AI

lemma finalise_cap_fast_Null:
  "\<lbrace>\<lambda>s. can_fast_finalise cap\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv s. rv = (cap.NullCap, NullCap)\<rbrace>" apply (cases cap, simp_all add: can_fast_finalise_def) apply (wp | simp only: o_def simp_thms cases_simp if_cancel fst_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. can_fast_finalise cap\<rbrace> finalise_cap cap final \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap)\<rbrace> proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap)\<rbrace>
 2. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when final (cancel_all_ipc x31)) \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap)\<rbrace>
 3. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap)\<rbrace>
 4. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. rv = (NullCap, NullCap)\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma hoare_pre_disj':
  "\<lbrakk>\<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>;
   \<lbrace>\<lambda>s. Q s \<and> R s\<rbrace> f \<lbrace>T\<rbrace> \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s. (P s \<or> Q s) \<and> R s\<rbrace> f \<lbrace>T\<rbrace>" apply (rule hoare_pre) apply (erule (1) hoare_pre_disj) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>; \<lbrace>\<lambda>s. Q s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P s \<or> Q s) \<and> R s\<rbrace> f \<lbrace>T\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>; \<lbrace>\<lambda>s. Q s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> f \<lbrace>T\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>; \<lbrace>\<lambda>s. Q s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>; (P s \<or> Q s) \<and> R s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>; \<lbrace>\<lambda>s. Q s \<and> R s\<rbrace> f \<lbrace>T\<rbrace>; (P s \<or> Q s) \<and> R s\<rbrakk> \<Longrightarrow> ((\<lambda>s. P s \<and> R s) or (\<lambda>s. Q s \<and> R s)) s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma invs_pspace_alignedI:
  "invs s \<Longrightarrow> pspace_aligned s" apply (simp add: invs_def valid_state_def valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> pspace_aligned s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma cte_wp_at_disj:
  "cte_wp_at (\<lambda>c. P c \<or> P' c) sl s =
   (cte_wp_at (\<lambda>c. P c) sl s \<or> cte_wp_at (\<lambda>c. P' c) sl s)" unfolding cte_wp_at_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. P c \<or> P' c) sl s = (cte_wp_at P sl s \<or> cte_wp_at P' sl s) proof (prove)
goal (1 subgoal):
 1. (\<exists>cap. fst (get_cap sl s) = {(cap, s)} \<and> (P cap \<or> P' cap)) = ((\<exists>cap. fst (get_cap sl s) = {(cap, s)} \<and> P cap) \<or> (\<exists>cap. fst (get_cap sl s) = {(cap, s)} \<and> P' cap))
theory Finalise_AI

lemma cap_not_in_valid_global_refs:
  "\<lbrakk>invs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow>
   obj_refs cap \<inter> global_refs s = {}" apply (drule invs_valid_global_refs) apply (simp add: valid_global_refs_def valid_refs_def) apply (case_tac p, simp) apply (erule_tac x=a in allE, erule_tac x=b in allE) apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s p = Some cap\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_global_refs s\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; p = (a, b)\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; p = (a, b); \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> global_refs s = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some cap; p = (a, b); global_refs s \<inter> (untyped_range cap \<union> obj_refs cap) = {}\<rbrakk> \<Longrightarrow> obj_refs cap \<inter> global_refs s = {} proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma gts_wp:
  "\<lbrace>\<lambda>s. \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> P st s\<rbrace> get_thread_state t \<lbrace>P\<rbrace>" unfolding get_thread_state_def apply (wp thread_get_wp') apply clarsimp apply (drule spec, erule mp) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> P st s\<rbrace> get_thread_state t \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> P st s\<rbrace> thread_get tcb_state t \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> P st s \<Longrightarrow> \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_state tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> P st s; ko_at (TCB tcb) t s\<rbrakk> \<Longrightarrow> P (tcb_state tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. ko_at (TCB tcb) t s \<Longrightarrow> st_tcb_at ((=) (tcb_state tcb)) t s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma gbn_wp:
  "\<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> get_bound_notification t \<lbrace>P\<rbrace>" unfolding get_bound_notification_def apply (wp thread_get_wp') apply (clarsimp) apply (drule spec, erule mp) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> get_bound_notification t \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> thread_get tcb_bound_notification t \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> P ntfn s \<Longrightarrow> \<forall>tcb. ko_at (TCB tcb) t s \<longrightarrow> P (tcb_bound_notification tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>\<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> P ntfn s; ko_at (TCB tcb) t s\<rbrakk> \<Longrightarrow> P (tcb_bound_notification tcb) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. ko_at (TCB tcb) t s \<Longrightarrow> bound_tcb_at ((=) (tcb_bound_notification tcb)) t s proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma valid_irq_node_arch [iff]:
  "valid_irq_node (arch_state_update f s) = valid_irq_node s" by (simp add: valid_irq_node_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node (arch_state_update f s) = valid_irq_node s
theory Finalise_AI

lemma vms_arch_state_update[simp]:
  "valid_machine_state (arch_state_update f s) = valid_machine_state s" by (simp add: valid_machine_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state (arch_state_update f s) = valid_machine_state s
theory Finalise_AI

lemma dmo_bind_return:
  "\<lbrace>P\<rbrace> do_machine_op f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace> do_machine_op (do _ \<leftarrow> f; return x od) \<lbrace>\<lambda>_. Q\<rbrace>" by (simp add: do_machine_op_def bind_def return_def valid_def select_f_def
                     split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do_machine_op f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (do _ <- f;
return x
od) \<lbrace>\<lambda>_. Q\<rbrace>
theory Finalise_AI

lemma st_tcb_at_idle_thread:
  "\<lbrakk> st_tcb_at P (idle_thread s) s; valid_idle s \<rbrakk>
        \<Longrightarrow> P Structures_A.IdleThreadState" by (clarsimp simp: valid_idle_def st_tcb_def2 pred_tcb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P (idle_thread s) s; valid_idle s\<rbrakk> \<Longrightarrow> P IdleThreadState
theory Finalise_AI

lemma tcb_state_merge_tcb_state_default:
  "tcb_state (tcb_registers_caps_merge tcb tcb') = tcb_state tcb"
  "tcb_state default_tcb = Structures_A.Inactive" by (auto simp add: tcb_registers_caps_merge_def default_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_state (tcb_registers_caps_merge tcb tcb') = tcb_state tcb &&& inactive (tcb_state default_tcb)
theory Finalise_AI

lemma tcb_bound_notification_merge_tcb_state_default:
  "tcb_bound_notification (tcb_registers_caps_merge tcb tcb') = tcb_bound_notification tcb"
  "tcb_bound_notification default_tcb = None" by (auto simp add: tcb_registers_caps_merge_def default_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_bound_notification (tcb_registers_caps_merge tcb tcb') = tcb_bound_notification tcb &&& tcb_bound_notification default_tcb = None
theory Finalise_AI

lemma dxo_noop: "do_extended_op f = (return () :: (unit,unit) s_monad)" apply (clarsimp simp add: do_extended_op_def bind_def gets_def get_def return_def
         select_f_def modify_def put_def mk_ef_def wrap_ext_op_unit_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_extended_op f = return () proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. ({((), s\<lparr>exst := ()\<rparr>)}, False)) = (\<lambda>s. ({((), s)}, False)) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma corres_option_split:
  "\<lbrakk>v = v'; corres_underlying sr nf nf' r P P' a c; (\<And>x. v = Some x \<Longrightarrow> corres_underlying sr nf nf' r (Q x) (Q' x) (b x) (d x))\<rbrakk>
  \<Longrightarrow> corres_underlying sr nf nf' r (case_option P Q v) (case_option P' Q' v') (case_option a b v) (case_option c d v')" by (cases v', simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v = v'; corres_underlying sr nf nf' r P P' a c; \<And>x. v = Some x \<Longrightarrow> corres_underlying sr nf nf' r (Q x) (Q' x) (b x) (d x)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (case v of None \<Rightarrow> P | Some x \<Rightarrow> Q x) (case v' of None \<Rightarrow> P' | Some x \<Rightarrow> Q' x) (case v of None \<Rightarrow> a | Some x \<Rightarrow> b x) (case v' of None \<Rightarrow> c | Some x \<Rightarrow> d x)
theory Finalise_AI

lemma hoare_post_case_option_ext:
  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. case_option (P s) (\<lambda>rv'. Q rv' s) rv\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>case_option P Q\<rbrace>" by (erule hoare_post_imp [rotated], simp split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> P s | Some rv' \<Rightarrow> Q rv' s\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>case_option P Q\<rbrace>
theory Finalise_AI

lemma hoare_when_weak_wp:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> when G f \<lbrace>\<lambda>_. P\<rbrace>" by wp simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> when G f \<lbrace>\<lambda>_. P\<rbrace>
theory Finalise_AI

lemma is_cap_tableE:
  "\<lbrakk> is_cap_table sz ko; \<And>cs. \<lbrakk> ko = kernel_object.CNode sz cs; well_formed_cnode_n sz cs\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" unfolding is_cap_table_def by (auto split: Structures_A.kernel_object.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_cap_table sz ko; \<And>cs. \<lbrakk>ko = CNode sz cs; well_formed_cnode_n sz cs\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case ko of CNode sza cs \<Rightarrow> sz = sza \<and> well_formed_cnode_n sz cs | _ \<Rightarrow> False; \<And>cs. \<lbrakk>ko = CNode sz cs; well_formed_cnode_n sz cs\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Finalise_AI

lemma cap_table_at_length:
  "\<lbrakk> cap_table_at bits oref s; valid_objs s \<rbrakk>
     \<Longrightarrow> bits < (word_bits - cte_level_bits)" apply (erule(1) obj_at_valid_objsE) apply (case_tac ko, simp_all add: is_cap_table_def) apply (clarsimp simp: valid_obj_def valid_cs_def
                        valid_cs_size_def well_formed_cnode_n_def
                        length_set_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_table_at bits oref s; valid_objs s\<rbrakk> \<Longrightarrow> bits < word_bits - cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; kheap s oref = Some ko; is_cap_table bits ko; valid_obj oref ko s\<rbrakk> \<Longrightarrow> bits < word_bits - cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ko x12. \<lbrakk>valid_objs s; kheap s oref = Some (CNode bits x12); well_formed_cnode_n bits x12; valid_obj oref (CNode bits x12) s; ko = CNode bits x12\<rbrakk> \<Longrightarrow> bits < word_bits - cte_level_bits proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma emptyable_cte_wp_atD:   "\<lbrakk> cte_wp_at P sl s; valid_objs s;
     \<forall>cap. P cap \<longrightarrow> \<not> is_master_reply_cap cap \<rbrakk>
   \<Longrightarrow> emptyable sl s" apply (clarsimp simp: emptyable_def pred_tcb_at_def obj_at_def
                        is_tcb cte_wp_at_cases) apply (erule(1) pspace_valid_objsE) apply (clarsimp simp: valid_obj_def valid_tcb_def ran_tcb_cap_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P sl s; valid_objs s; \<forall>cap. P cap \<longrightarrow> \<not> is_master_reply_cap cap\<rbrakk> \<Longrightarrow> emptyable sl s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>P (tcb_reply tcb); valid_objs s; \<forall>cap. P cap \<longrightarrow> \<not> is_master_reply_cap cap; snd sl = tcb_cnode_index 2; kheap s (fst sl) = Some (TCB tcb)\<rbrakk> \<Longrightarrow> halted (tcb_state tcb) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>P (tcb_reply tcb); valid_objs s; \<forall>cap. P cap \<longrightarrow> \<not> is_master_reply_cap cap; snd sl = tcb_cnode_index 2; kheap s (fst sl) = Some (TCB tcb); valid_obj (fst sl) (TCB tcb) s\<rbrakk> \<Longrightarrow> halted (tcb_state tcb) proof (prove)
goal:
No subgoals!
theory Finalise_AI

lemma thread_set_emptyable:
  assumes z: "\<And>tcb. tcb_state  (f tcb) = tcb_state  tcb"
  shows      "\<lbrace>emptyable sl\<rbrace> thread_set f t \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" by (wp emptyable_lift thread_set_no_change_tcb_state z)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>emptyable sl\<rbrace> thread_set f t \<lbrace>\<lambda>rv. emptyable sl\<rbrace>
theory ArchFinalise_AI

lemma valid_global_refs_asid_table_udapte [iff]:
  "valid_global_refs (s\<lparr>arch_state := arm_asid_table_update f (arch_state s)\<rparr>) =
  valid_global_refs s" by (simp add: valid_global_refs_def global_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs (s\<lparr>arch_state := arm_asid_table_update f (arch_state s)\<rparr>) = valid_global_refs s
theory ArchFinalise_AI

lemma reachable_pg_cap_is_original_cap_update [simp]:
  "reachable_pg_cap x (is_original_cap_update f s) = reachable_pg_cap x s" by (simp add: reachable_pg_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable_pg_cap x (is_original_cap_update f s) = reachable_pg_cap x s
theory ArchFinalise_AI

lemma reachable_pg_cap_update[simp]:
  "reachable_pg_cap cap' (trans_state f s) = reachable_pg_cap cap' s" by (simp add:reachable_pg_cap_def vs_lookup_pages_def
    vs_lookup_pages1_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable_pg_cap cap' (trans_state f s) = reachable_pg_cap cap' s