kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_Cases

lemma "corres_underlying srel nf nf' rrel G G' m ((case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) >>=E g)" apply corres_cases oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel G G' m ((case x of None \<Rightarrow> a | Some y \<Rightarrow> b y) >>=E g) proof (prove)
goal (4 subgoals):
 1. x = None \<Longrightarrow> corres_underlying srel nf nf' rrel ?Q'38 ?Q40 m (a >>=E g)
 2. \<And>x2. x = Some x2 \<Longrightarrow> corres_underlying srel nf nf' rrel (?Q'39 x2) (?Q41 x2) m (b x2 >>=E g)
 3. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q'38 s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q'39 xa s)
 4. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> ?Q40 s') \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?Q41 xa s')
theory Corres_Cases

lemma "corres_underlying srel nf nf' rrel G G' (case x of None \<Rightarrow> a | Some y \<Rightarrow> b)
                                               (case x of None \<Rightarrow> a' | Some y \<Rightarrow> b' y)" 
  (* two cases remain (both None, both Some); eliminated cases have guard \<top> in final implication *)
   apply corres_cases_both oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel G G' (case x of None \<Rightarrow> a | Some y \<Rightarrow> b) (case x of None \<Rightarrow> a' | Some y \<Rightarrow> b' y) proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel G G' (case x of None \<Rightarrow> a | Some y \<Rightarrow> b) (case x of None \<Rightarrow> a' | Some y \<Rightarrow> b' y) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x = None; x = None\<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' rrel ?Q'137 ?Q139 a a'
 2. \<And>x2 x2a. \<lbrakk>x = Some x2; x = Some x2a\<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' rrel (?Q'89 x2 x2a) (?Q91 x2 x2a) b (b' x2a)
 3. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> (x = None \<longrightarrow> ?Q'137 s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> True)) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (x = None \<longrightarrow> True) \<and> (\<forall>xb. x = Some xb \<longrightarrow> ?Q'89 xa xb s))
 4. \<And>s s'. \<lbrakk>G s; G' s'; (s, s') \<in> srel\<rbrakk> \<Longrightarrow> (x = None \<longrightarrow> (x = None \<longrightarrow> ?Q139 s') \<and> (\<forall>xa. x = Some xa \<longrightarrow> True)) \<and> (\<forall>xa. x = Some xa \<longrightarrow> (x = None \<longrightarrow> True) \<and> (\<forall>xb. x = Some xb \<longrightarrow> ?Q91 xa xb s'))
theory Corres_Method

lemma no_fail_triv: "no_fail P f \<Longrightarrow> no_fail P f" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail P f
theory Corres_Method

lemma corres_get_trivial[corres_term]:
  "corres_underlying sr nf nf' (\<lambda>s s'. (s,s') \<in> sr) \<top> \<top> get get" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (\<lambda>s s'. (s, s') \<in> sr) (\<lambda>_. True) (\<lambda>_. True) get get
theory Corres_Method

lemma corres_modify_tivial[corres_term]:
  "(\<And>s s'. (s, s') \<in> sr \<Longrightarrow> (f s, g s') \<in> sr) \<Longrightarrow>
   corres_underlying sr nf nf' dc \<top> \<top> (modify f) (modify g)" by (simp add: corres_modify)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. (s, s') \<in> sr \<Longrightarrow> (f s, g s') \<in> sr) \<Longrightarrow> corres_underlying sr nf nf' dc (\<lambda>_. True) (\<lambda>_. True) (modify f) (modify g)
theory LevityCatch

lemma magnitudeCheck_assert:
  "magnitudeCheck x y n = assert (case y of None \<Rightarrow> True | Some z \<Rightarrow> 1 << n \<le> z - x)" apply (simp add: magnitudeCheck_def assert_def when_def
            split: option.split) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. magnitudeCheck x y n = assert (case y of None \<Rightarrow> True | Some z \<Rightarrow> 1 << n \<le> z - x) proof (prove)
goal (1 subgoal):
 1. \<forall>x2. (x2 - x < 2 ^ n \<longrightarrow> y = Some x2 \<longrightarrow> 2 ^ n \<le> x2 - x \<longrightarrow> fail = return ()) \<and> (\<not> x2 - x < 2 ^ n \<longrightarrow> y = Some x2 \<longrightarrow> \<not> 2 ^ n \<le> x2 - x \<longrightarrow> return () = fail) proof (prove)
goal:
No subgoals!
theory LevityCatch

lemma projectKO_inv : "\<lbrace>P\<rbrace> projectKO ko \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: projectKO_def fail_def valid_def return_def
           split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> projectKO ko \<lbrace>\<lambda>rv. P\<rbrace>
theory LevityCatch

lemma alignCheck_assert:
  "alignCheck ptr n = assert (is_aligned ptr n)" by (simp add: is_aligned_mask alignCheck_def assert_def
                alignError_def unless_def when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignCheck ptr n = assert (is_aligned ptr n)
theory LevityCatch

lemma magnitudeCheck_inv:   "\<lbrace>P\<rbrace> magnitudeCheck x y n \<lbrace>\<lambda>rv. P\<rbrace>" apply (clarsimp simp add: magnitudeCheck_def split: option.splits) apply (wp when_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> magnitudeCheck x y n \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. y = Some x2 \<Longrightarrow> \<lbrace>P\<rbrace> when (x2 - x < 2 ^ n) fail \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>y = Some x2; P s\<rbrakk> \<Longrightarrow> (if x2 - x < 2 ^ n then \<lambda>_. True else P) s proof (prove)
goal:
No subgoals!
theory LevityCatch

lemma alignCheck_inv:
  "\<lbrace>P\<rbrace> alignCheck x n \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: alignCheck_def unless_def alignError_def) apply (wp when_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> alignCheck x n \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> when (x && mask n \<noteq> 0) fail \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (if x && mask n \<noteq> 0 then \<lambda>_. True else P) s proof (prove)
goal:
No subgoals!
theory LevityCatch

lemma updateObject_default_inv:
  "\<lbrace>P\<rbrace> updateObject_default obj ko x y n \<lbrace>\<lambda>rv. P\<rbrace>" unfolding updateObject_default_def by (simp, wp magnitudeCheck_inv alignCheck_inv projectKO_inv, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> updateObject_default obj ko x y n \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do assert (x = y);
_ <- projectKO ko;
alignCheck x (objBits obj);
magnitudeCheck x n (objBits obj);
return (injectKO obj)
od \<lbrace>\<lambda>rv. P\<rbrace>
theory LevityCatch

lemma to_from_apiType [simp]: "toAPIType (fromAPIType x) = Some x" by (cases x) (auto simp add: fromAPIType_def ARM_H.fromAPIType_def
    toAPIType_def ARM_H.toAPIType_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. toAPIType (fromAPIType x) = Some x
theory Invariants_H

lemma le_maxDomain_eq_less_numDomains:
  shows "x \<le> unat maxDomain \<longleftrightarrow> x < Kernel_Config.numDomains"
        "y \<le> maxDomain \<longleftrightarrow> unat y < Kernel_Config.numDomains" by (auto simp: Kernel_Config.numDomains_def maxDomain_def word_le_nat_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le> unat maxDomain) = (x < numDomains) &&& (y \<le> maxDomain) = (unat y < numDomains)
theory Invariants_H

lemma [simp]: "itcbState (tcb_to_itcb' tcb) = tcbState tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbState (tcb_to_itcb' tcb) = tcbState tcb
theory Invariants_H

lemma [simp]: "itcbFaultHandler (tcb_to_itcb' tcb) = tcbFaultHandler tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbFaultHandler (tcb_to_itcb' tcb) = tcbFaultHandler tcb
theory Invariants_H

lemma [simp]: "itcbIPCBuffer (tcb_to_itcb' tcb) = tcbIPCBuffer tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbIPCBuffer (tcb_to_itcb' tcb) = tcbIPCBuffer tcb
theory Invariants_H

lemma [simp]: "itcbBoundNotification (tcb_to_itcb' tcb) = tcbBoundNotification tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbBoundNotification (tcb_to_itcb' tcb) = tcbBoundNotification tcb
theory Invariants_H

lemma [simp]: "itcbPriority (tcb_to_itcb' tcb) = tcbPriority tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbPriority (tcb_to_itcb' tcb) = tcbPriority tcb
theory Invariants_H

lemma [simp]: "itcbFault (tcb_to_itcb' tcb) = tcbFault tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbFault (tcb_to_itcb' tcb) = tcbFault tcb
theory Invariants_H

lemma [simp]: "itcbTimeSlice (tcb_to_itcb' tcb) = tcbTimeSlice tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbTimeSlice (tcb_to_itcb' tcb) = tcbTimeSlice tcb
theory Invariants_H

lemma [simp]: "itcbMCP (tcb_to_itcb' tcb) = tcbMCP tcb" by (auto simp: tcb_to_itcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. itcbMCP (tcb_to_itcb' tcb) = tcbMCP tcb
theory Invariants_H

lemma st_tcb_at'_def:
  "st_tcb_at' test \<equiv> obj_at' (test \<circ> tcbState)" by (simp add: pred_tcb_at'_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' test \<equiv> obj_at' (test \<circ> tcbState)
theory Invariants_H

lemma valid_idle'_tcb_at':
  "valid_idle' s \<Longrightarrow> obj_at' idle_tcb' (ksIdleThread s) s" by (clarsimp simp: valid_idle'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle' s \<Longrightarrow> obj_at' idle_tcb' (ksIdleThread s) s
theory Invariants_H

lemma all_invs_but_sym_refs_not_ct_inQ_check':
  "(all_invs_but_sym_refs_ct_not_inQ' and sym_refs \<circ> state_refs_of' and ct_not_inQ) = invs'" by (simp add: pred_conj_def conj_commute conj_left_commute invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues s \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s) and sym_refs \<circ> state_refs_of' and ct_not_inQ) = invs'
theory Invariants_H

lemma all_invs_but_not_ct_inQ_check':
  "(all_invs_but_ct_not_inQ' and ct_not_inQ) = invs'" by (simp add: pred_conj_def conj_commute conj_left_commute invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s) and ct_not_inQ) = invs'
theory Invariants_H

lemma all_invs_but_ct_idle_or_in_cur_domain_check':
  "(all_invs_but_ct_idle_or_in_cur_domain' and ct_idle_or_in_cur_domain') = invs'" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def pred_conj_def
                conj_left_commute conj_commute invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (all_invs_but_ct_idle_or_in_cur_domain' and ct_idle_or_in_cur_domain') = invs'
theory Invariants_H

lemma invs'_to_invs_no_cicd'_def:
  "invs' = (all_invs_but_ct_idle_or_in_cur_domain' and ct_idle_or_in_cur_domain')" by (fastforce simp: invs'_def all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' = (all_invs_but_ct_idle_or_in_cur_domain' and ct_idle_or_in_cur_domain')
theory Invariants_H

lemma ntfn_splits[split]:
  " P (case ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> f1
     | Structures_H.ntfn.ActiveNtfn x \<Rightarrow> f2 x
     | Structures_H.ntfn.WaitingNtfn x \<Rightarrow> f3 x) =
  ((ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> P f1) \<and>
   (\<forall>x2. ntfn = Structures_H.ntfn.ActiveNtfn x2 \<longrightarrow>
         P (f2 x2)) \<and>
   (\<forall>x3. ntfn = Structures_H.ntfn.WaitingNtfn x3 \<longrightarrow>
         P (f3 x3)))"
  "P (case ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> f1
     | Structures_H.ntfn.ActiveNtfn x \<Rightarrow> f2 x
     | Structures_H.ntfn.WaitingNtfn x \<Rightarrow> f3 x) =
  (\<not> (ntfn = Structures_H.ntfn.IdleNtfn \<and> \<not> P f1 \<or>
       (\<exists>x2. ntfn = Structures_H.ntfn.ActiveNtfn x2 \<and>
             \<not> P (f2 x2)) \<or>
       (\<exists>x3. ntfn = Structures_H.ntfn.WaitingNtfn x3 \<and>
             \<not> P (f3 x3))))" by (case_tac ntfn; simp)+
\<comment> \<open>---------------------------------------------------------------------------\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (case ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> f1 | Structures_H.ntfn.ActiveNtfn x \<Rightarrow> f2 x | Structures_H.ntfn.WaitingNtfn x \<Rightarrow> f3 x) = ((ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> P f1) \<and> (\<forall>x2. ntfn = Structures_H.ntfn.ActiveNtfn x2 \<longrightarrow> P (f2 x2)) \<and> (\<forall>x3. ntfn = Structures_H.ntfn.WaitingNtfn x3 \<longrightarrow> P (f3 x3))) &&& P (case ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> f1 | Structures_H.ntfn.ActiveNtfn x \<Rightarrow> f2 x | Structures_H.ntfn.WaitingNtfn x \<Rightarrow> f3 x) = (\<not> (ntfn = Structures_H.ntfn.IdleNtfn \<and> \<not> P f1 \<or> (\<exists>x2. ntfn = Structures_H.ntfn.ActiveNtfn x2 \<and> \<not> P (f2 x2)) \<or> (\<exists>x3. ntfn = Structures_H.ntfn.WaitingNtfn x3 \<and> \<not> P (f3 x3))))
theory Invariants_H

lemma valid_bound_ntfn'_None[simp]:
  "valid_bound_ntfn' None = \<top>" by (auto simp: valid_bound_ntfn'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bound_ntfn' None = (\<lambda>_. True)
theory Invariants_H

lemma valid_bound_ntfn'_Some[simp]:
  "valid_bound_ntfn' (Some x) = ntfn_at' x" by (auto simp: valid_bound_ntfn'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bound_ntfn' (Some x) = ntfn_at' x
theory Invariants_H

lemma valid_bound_tcb'_None[simp]:
  "valid_bound_tcb' None = \<top>" by (auto simp: valid_bound_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bound_tcb' None = (\<lambda>_. True)
theory Invariants_H

lemma valid_bound_tcb'_Some[simp]:
  "valid_bound_tcb' (Some x) = tcb_at' x" by (auto simp: valid_bound_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bound_tcb' (Some x) = tcb_at' x
theory Invariants_H

lemma valid_duplicates'_D:
  "\<lbrakk>vs_valid_duplicates' m; m (p::word32) = Some ko;is_aligned p' 2;
  p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)\<rbrakk>
  \<Longrightarrow> m p' = Some ko " apply (clarsimp simp:vs_valid_duplicates'_def) apply (drule_tac x = p in spec) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vs_valid_duplicates' m; m p = Some ko; is_aligned p' 2; p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)\<rbrakk> \<Longrightarrow> m p' = Some ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x y. case m x of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> m x = m y; m p = Some ko; is_aligned p' 2; p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)\<rbrakk> \<Longrightarrow> m p' = Some ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some ko; is_aligned p' 2; p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko); \<forall>y. case m p of None \<Rightarrow> True | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> p && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> m p = m y\<rbrakk> \<Longrightarrow> m p' = Some ko proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma projectKO_stateI:
  "fst (projectKO e s) = {(obj, s)} \<Longrightarrow> fst (projectKO e s') = {(obj, s')}" unfolding projectKO_def by (auto simp: fail_def return_def valid_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (projectKO e s) = {(obj, s)} \<Longrightarrow> fst (projectKO e s') = {(obj, s')} proof (prove)
goal (1 subgoal):
 1. fst ((case projectKO_opt e of None \<Rightarrow> fail | Some k \<Rightarrow> return k) s) = {(obj, s)} \<Longrightarrow> fst ((case projectKO_opt e of None \<Rightarrow> fail | Some k \<Rightarrow> return k) s') = {(obj, s')}
theory Invariants_H

lemma projectKO_eq:
  "(fst (projectKO ko c) = {(obj, c)}) = (projectKO_opt ko = Some obj)" by (simp add: projectKO_def fail_def return_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (fst (projectKO ko c) = {(obj, c)}) = (projectKO_opt ko = Some obj)
theory Invariants_H

lemma obj_at'_def':
  "obj_at' P p s = (\<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko)
                   \<and> fst (projectKO ko s) = {(obj,s)} \<and> P obj
                   \<and> ps_clear p (objBitsKO ko) s)" apply (simp add: obj_at'_real_def ko_wp_at'_def projectKO_eq
                   True_notin_set_replicate_conv objBits_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p s = (\<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s) proof (prove)
goal (1 subgoal):
 1. (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj) \<and> ps_clear p (objBitsKO ko) s) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj \<and> P obj \<and> ps_clear p (objBitsKO ko) s)) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma obj_at'_def:
  "obj_at' P p s \<equiv> \<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko)
                   \<and> fst (projectKO ko s) = {(obj,s)} \<and> P obj
                   \<and> ps_clear p (objBitsKO ko) s" by (simp add: obj_at'_def')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p s \<equiv> \<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear p (objBitsKO ko) s
theory Invariants_H

lemma obj_atE' [elim?]:
  assumes objat: "obj_at' P ptr s"
  and        rl: "\<And>ko obj.
  \<lbrakk> ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko);
     fst (projectKO ko s) = {(obj,s)}; P obj;
     ps_clear ptr (objBitsKO ko) s \<rbrakk> \<Longrightarrow> R"
  shows "R" using objat unfolding obj_at'_def by (auto intro!: rl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
obj_at' P ptr s

goal (1 subgoal):
 1. R proof (prove)
using this:
\<exists>ko obj. ksPSpace s ptr = Some ko \<and> is_aligned ptr (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear ptr (objBitsKO ko) s

goal (1 subgoal):
 1. R
theory Invariants_H

lemma obj_atI' [intro?]:
  "\<lbrakk> ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko);
       fst (projectKO ko s) = {(obj, s)}; P obj;
       ps_clear ptr (objBitsKO ko) s \<rbrakk>
  \<Longrightarrow> obj_at' P ptr s" unfolding obj_at'_def by (auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> obj_at' P ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; P obj; ps_clear ptr (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>ko obj. ksPSpace s ptr = Some ko \<and> is_aligned ptr (objBitsKO ko) \<and> fst (projectKO ko s) = {(obj, s)} \<and> P obj \<and> ps_clear ptr (objBitsKO ko) s
theory Invariants_H

lemma cte_at'_def:
  "cte_at' p s \<equiv> \<exists>cte::cte. fst (getObject p s) = {(cte,s)}" by (simp add: cte_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) p s \<equiv> \<exists>cte. fst (getObject p s) = {(cte, s)}
theory Invariants_H

lemma tcb_cte_cases_simps[simp]:
  "tcb_cte_cases 0  = Some (tcbCTable, tcbCTable_update)"
  "tcb_cte_cases 16 = Some (tcbVTable, tcbVTable_update)"
  "tcb_cte_cases 32 = Some (tcbReply, tcbReply_update)"
  "tcb_cte_cases 48 = Some (tcbCaller, tcbCaller_update)"
  "tcb_cte_cases 64 = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)" by (simp add: tcb_cte_cases_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tcb_cte_cases 0 = Some (tcbCTable, tcbCTable_update) &&& tcb_cte_cases 0x10 = Some (tcbVTable, tcbVTable_update)) &&& tcb_cte_cases 0x20 = Some (tcbReply, tcbReply_update) &&& tcb_cte_cases 0x30 = Some (tcbCaller, tcbCaller_update) &&& tcb_cte_cases 0x40 = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)
theory Invariants_H

lemma tcb_st_refs_of'_simps[simp]:
 "tcb_st_refs_of' (Running)                  = {}"
 "tcb_st_refs_of' (Inactive)                 = {}"
 "tcb_st_refs_of' (Restart)                  = {}"
 "tcb_st_refs_of' (BlockedOnReceive x'' a')  = {(x'', TCBBlockedRecv)}"
 "tcb_st_refs_of' (BlockedOnSend x a b c d)  = {(x, TCBBlockedSend)}"
 "tcb_st_refs_of' (BlockedOnNotification x') = {(x', TCBSignal)}"
 "tcb_st_refs_of' (BlockedOnReply)           = {}"
 "tcb_st_refs_of' (IdleThreadState)          = {}" by (auto simp: tcb_st_refs_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((tcb_st_refs_of' Structures_H.thread_state.Running = {} &&& tcb_st_refs_of' Structures_H.thread_state.Inactive = {}) &&& tcb_st_refs_of' Structures_H.thread_state.Restart = {} &&& tcb_st_refs_of' (Structures_H.thread_state.BlockedOnReceive x'' a') = {(x'', TCBBlockedRecv)}) &&& (tcb_st_refs_of' (Structures_H.thread_state.BlockedOnSend x a b c d) = {(x, TCBBlockedSend)} &&& tcb_st_refs_of' (Structures_H.thread_state.BlockedOnNotification x') = {(x', TCBSignal)}) &&& tcb_st_refs_of' Structures_H.thread_state.BlockedOnReply = {} &&& tcb_st_refs_of' Structures_H.thread_state.IdleThreadState = {}
theory Invariants_H

lemma ep_q_refs_of'_simps[simp]:
 "ep_q_refs_of'  IdleEP    = {}"
 "ep_q_refs_of' (RecvEP q) = set q \<times> {EPRecv}"
 "ep_q_refs_of' (SendEP q) = set q \<times> {EPSend}" by (auto simp: ep_q_refs_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_q_refs_of' Structures_H.endpoint.IdleEP = {} &&& ep_q_refs_of' (Structures_H.endpoint.RecvEP q) = set q \<times> {EPRecv} &&& ep_q_refs_of' (Structures_H.endpoint.SendEP q) = set q \<times> {EPSend}