kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchInvariants_AI

lemma hyp_live_tcb_simps[simp]:
"\<And>tcb f. hyp_live (TCB (tcb_ipc_buffer_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_mcpriority_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_ctable_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_vtable_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_reply_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_caller_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_ipcframe_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_state_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_fault_handler_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_fault_update f tcb)) = hyp_live (TCB tcb)"
"\<And>tcb f. hyp_live (TCB (tcb_bound_notification_update f tcb)) = hyp_live (TCB tcb)" by (simp_all add: hyp_live_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((\<And>tcb f. hyp_live (TCB (tcb_ipc_buffer_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_mcpriority_update f tcb)) = hyp_live (TCB tcb))) &&& (\<And>tcb f. hyp_live (TCB (tcb_ctable_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_vtable_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_reply_update f tcb)) = hyp_live (TCB tcb))) &&& ((\<And>tcb f. hyp_live (TCB (tcb_caller_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_ipcframe_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_state_update f tcb)) = hyp_live (TCB tcb))) &&& (\<And>tcb f. hyp_live (TCB (tcb_fault_handler_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_fault_update f tcb)) = hyp_live (TCB tcb)) &&& (\<And>tcb f. hyp_live (TCB (tcb_bound_notification_update f tcb)) = hyp_live (TCB tcb))
theory ArchInvariants_AI

lemma valid_arch_tcb_pspaceI:
  "\<lbrakk> valid_arch_tcb t s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> valid_arch_tcb t s'" unfolding valid_arch_tcb_def obj_at_def by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_tcb t s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> valid_arch_tcb t s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True; kheap s = kheap s'\<rbrakk> \<Longrightarrow> True
theory ArchInvariants_AI

lemma valid_arch_tcb_typ_at:
  "\<lbrakk> valid_arch_tcb t s; \<And>T p. typ_at T p s \<Longrightarrow> typ_at T p s' \<rbrakk> \<Longrightarrow> valid_arch_tcb t s'" by (simp add: valid_arch_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_tcb t s; \<And>T p. typ_at T p s \<Longrightarrow> typ_at T p s'\<rbrakk> \<Longrightarrow> valid_arch_tcb t s'
theory ArchInvariants_AI

lemma valid_arch_tcb_lift:
  "(\<And>T p. f \<lbrace>typ_at T p\<rbrace>) \<Longrightarrow> f \<lbrace>valid_arch_tcb t\<rbrace>" unfolding valid_arch_tcb_def by (wp hoare_vcg_all_lift hoare_vcg_imp_lift; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>_. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>valid_arch_tcb t\<rbrace> f \<lbrace>\<lambda>_. valid_arch_tcb t\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>_. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>
theory ArchInvariants_AI

lemma arch_gen_obj_refs_inD:
  "x \<in> arch_gen_obj_refs cap \<Longrightarrow> arch_gen_obj_refs cap = {x}" by (simp add: arch_gen_obj_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> arch_gen_obj_refs cap \<Longrightarrow> arch_gen_obj_refs cap = {x}
theory ArchInvariants_AI

lemma obj_ref_not_arch_gen_ref:
  "x \<in> obj_refs cap \<Longrightarrow> arch_gen_refs cap = {}" by (cases cap; simp add: arch_gen_obj_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> obj_refs cap \<Longrightarrow> arch_gen_refs cap = {}
theory ArchInvariants_AI

lemma arch_gen_obj_refs_simps[simp]:
  "arch_gen_obj_refs (ASIDPoolCap a b) = {}"
  "arch_gen_obj_refs (PageTableCap c d) = {}"
  "arch_gen_obj_refs (PageDirectoryCap e f) = {}"
  "arch_gen_obj_refs (ASIDControlCap) = {}"
  "arch_gen_obj_refs (PageCap x1 x2 x3 x4 x5) = {}" by (simp add: arch_gen_obj_refs_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (arch_gen_obj_refs (ASIDPoolCap a b) = {} &&& arch_gen_obj_refs (PageTableCap c d) = {}) &&& arch_gen_obj_refs (PageDirectoryCap e f) = {} &&& arch_gen_obj_refs ASIDControlCap = {} &&& arch_gen_obj_refs (PageCap x1 x2 x3 x4 x5) = {}
theory ArchInvariants_AI

lemma same_aobject_same_arch_gen_refs:
  "same_aobject_as ac ac' \<Longrightarrow> arch_gen_obj_refs ac = arch_gen_obj_refs ac'" by (clarsimp simp: arch_gen_obj_refs_def split: arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_aobject_as ac ac' \<Longrightarrow> arch_gen_obj_refs ac = arch_gen_obj_refs ac'
theory ArchInvariants_AI

lemma arch_tcb_context_get_set[simp]:
  "arch_tcb_context_get (arch_tcb_context_set uc a_tcb) = uc" by (simp add: arch_tcb_context_get_def arch_tcb_context_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_tcb_context_get (arch_tcb_context_set uc a_tcb) = uc
theory ArchInvariants_AI

lemma vs_lookup_trans_sub2:
  assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
  shows "vs_lookup_trans s \<subseteq> vs_lookup_trans s'" proof - have "vs_lookup1 s \<subseteq> vs_lookup1 s'" by (fastforce dest: ko elim: vs_lookup1_stateI2) thus ?thesis by (rule rtrancl_mono) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (state)
goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (prove)
goal (1 subgoal):
 1. vs_lookup1 s \<subseteq> vs_lookup1 s' proof (state)
this:
vs_lookup1 s \<subseteq> vs_lookup1 s'

goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (prove)
using this:
vs_lookup1 s \<subseteq> vs_lookup1 s'

goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>* proof (state)
this:
(vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>*

goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_pages_trans_sub2:
  assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs_pages ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
  shows "vs_lookup_pages_trans s \<subseteq> vs_lookup_pages_trans s'" proof - have "vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'" by (fastforce dest: ko elim: vs_lookup_pages1_stateI2) thus ?thesis by (rule rtrancl_mono) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (state)
goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s' proof (state)
this:
vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'

goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (prove)
using this:
vs_lookup_pages1 s \<subseteq> vs_lookup_pages1 s'

goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>* proof (state)
this:
(vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>*

goal:
No subgoals!
theory ArchInvariants_AI

lemma pte_ref_pagesD:
  "pte_ref_pages (pt y) = Some x \<Longrightarrow>
   (VSRef (ucast y) (Some APageTable), x) \<in> vs_refs_pages (ArchObj (PageTable pt))" by (auto simp: pte_ref_pages_def vs_refs_pages_def graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pte_ref_pages (pt y) = Some x \<Longrightarrow> (VSRef (UCAST(8 \<rightarrow> 32) y) (Some APageTable), x) \<in> vs_refs_pages (ArchObj (PageTable pt))
theory ArchInvariants_AI

lemma valid_asid_table_ran:
  "valid_asid_table asid_tbl s \<Longrightarrow> \<forall>p\<in>ran asid_tbl. asid_pool_at p s" by (simp add: valid_arch_state_def valid_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_table asid_tbl s \<Longrightarrow> \<forall>p\<in>ran asid_tbl. typ_at (AArch AASIDPool) p s
theory ArchInvariants_AI

lemma vs_refs_add_one'':
  "p \<in> kernel_mapping_slots \<Longrightarrow>
   vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = vs_refs (ArchObj (PageDirectory pd))" by (auto simp: vs_refs_def graph_of_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<in> kernel_mapping_slots \<Longrightarrow> vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = vs_refs (ArchObj (PageDirectory pd))
theory ArchInvariants_AI

lemma vs_refs_pages_subset: "vs_refs ko \<subseteq> vs_refs_pages ko" apply (clarsimp simp: vs_refs_pages_def vs_refs_def graph_of_def pde_ref_def pde_ref_pages_def
                  split: kernel_object.splits arch_kernel_obj.splits pde.splits) subgoal for "fun" a b using
    imageI[where A="{(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (fun x)) = Some y}"
             and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"] by (clarsimp simp: pde_ref_def pde_ref_pages_def split: if_splits pde.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_refs ko \<subseteq> vs_refs_pages ko proof (prove)
goal (1 subgoal):
 1. \<And>x3 aa ba. \<lbrakk>ko = ArchObj (PageDirectory x3); (if aa \<in> kernel_mapping_slots then None else pde_ref (x3 aa)) = Some ba\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) aa) (Some APageDirectory), ba) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (x3 x)) = Some y} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = ArchObj (PageDirectory fun); (if a \<in> kernel_mapping_slots then None else pde_ref (fun a)) = Some b\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (fun x)) = Some y} proof (prove)
using this:
(a, b) \<in> {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (fun x)) = Some y} \<Longrightarrow> (case (a, b) of (r, y) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) \<in> (\<lambda>(r, y). (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), y)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (fun x)) = Some y}

goal (1 subgoal):
 1. \<lbrakk>ko = ArchObj (PageDirectory fun); (if a \<in> kernel_mapping_slots then None else pde_ref (fun a)) = Some b\<rbrakk> \<Longrightarrow> (VSRef (UCAST(12 \<rightarrow> 32) a) (Some APageDirectory), b) \<in> (\<lambda>x. case x of (r, x) \<Rightarrow> (VSRef (UCAST(12 \<rightarrow> 32) r) (Some APageDirectory), x)) ` {(x, y). (if x \<in> kernel_mapping_slots then None else pde_ref_pages (fun x)) = Some y} proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vas_valid_asid_table:
  "valid_arch_state s \<Longrightarrow> valid_asid_table (asid_table s) s" by (simp add: valid_arch_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<Longrightarrow> valid_asid_table (asid_table s) s
theory ArchInvariants_AI

lemma physBase_aligned[simplified pageBitsForSize_simps]:
  "is_aligned physBase (pageBitsForSize ARMSuperSection)" by simp (rule physBase_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned physBase (pageBitsForSize ARMSuperSection)
theory ArchInvariants_AI

lemma pptrBase_aligned[simplified pageBitsForSize_simps]:
  "is_aligned pptrBase (pageBitsForSize ARMSuperSection)" by (simp add: is_aligned_def pptrBase_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pptrBase (pageBitsForSize ARMSuperSection)
theory ArchInvariants_AI

lemma pptrBaseOffset_aligned[simplified pageBitsForSize_simps]:
  "is_aligned pptrBaseOffset (pageBitsForSize ARMSuperSection)" by (auto simp: pptrBaseOffset_def physBase_aligned pptrBase_aligned
           elim: is_aligned_weaken intro: aligned_sub_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pptrBaseOffset (pageBitsForSize ARMSuperSection)
theory ArchInvariants_AI

lemma pageBitsForSize_limit[simplified pageBitsForSize_simps, simp]:
  "pageBitsForSize sz \<le> pageBitsForSize ARMSuperSection" by (cases sz; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBitsForSize sz \<le> pageBitsForSize ARMSuperSection
theory ArchInvariants_AI

lemma is_aligned_pptrBaseOffset[simplified pageBitsForSize_simps]:
  "is_aligned pptrBaseOffset (pageBitsForSize sz)" by (cases sz; clarsimp intro!: is_aligned_weaken[OF pptrBaseOffset_aligned])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pptrBaseOffset (pageBitsForSize sz)
theory ArchInvariants_AI

lemma is_aligned_addrFromPPtr_n[simplified pageBitsForSize_simps]:
  "\<lbrakk> is_aligned p n; n \<le> (pageBitsForSize ARMSuperSection) \<rbrakk>
   \<Longrightarrow> is_aligned (Platform.ARM.addrFromPPtr p) n" by (auto simp: addrFromPPtr_def
           elim!: aligned_sub_aligned
           intro: is_aligned_weaken pptrBaseOffset_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n \<le> pageBitsForSize ARMSuperSection\<rbrakk> \<Longrightarrow> is_aligned (addrFromPPtr p) n
theory ArchInvariants_AI

lemma is_aligned_addrFromPPtr:
  "is_aligned p pageBits \<Longrightarrow> is_aligned (Platform.ARM.addrFromPPtr p) pageBits" by (simp add: is_aligned_addrFromPPtr_n pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p pageBits \<Longrightarrow> is_aligned (addrFromPPtr p) pageBits
theory ArchInvariants_AI

lemma is_aligned_ptrFromPAddr_n[simplified pageBitsForSize_simps]:
  "\<lbrakk> is_aligned p n; n \<le> (pageBitsForSize ARMSuperSection)\<rbrakk>
   \<Longrightarrow> is_aligned (ptrFromPAddr p) n" by (auto simp: ptrFromPAddr_def
           elim!: aligned_add_aligned
           intro: is_aligned_weaken pptrBaseOffset_aligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; n \<le> pageBitsForSize ARMSuperSection\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr p) n
theory ArchInvariants_AI

lemma is_aligned_ptrFromPAddr:
  "is_aligned p pageBits \<Longrightarrow> is_aligned (ptrFromPAddr p) pageBits" by (simp add: is_aligned_ptrFromPAddr_n pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p pageBits \<Longrightarrow> is_aligned (ptrFromPAddr p) pageBits
theory ArchInvariants_AI

lemma is_aligned_ptrFromPAddrD[simplified pageBitsForSize_simps]:
  "\<lbrakk> is_aligned (ptrFromPAddr b) a; a \<le> (pageBitsForSize ARMSuperSection)\<rbrakk>
   \<Longrightarrow> is_aligned b a" by (simp add: ptrFromPAddr_def)
     (erule is_aligned_addD2, erule is_aligned_weaken[OF pptrBaseOffset_aligned])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned (ptrFromPAddr b) a; a \<le> pageBitsForSize ARMSuperSection\<rbrakk> \<Longrightarrow> is_aligned b a
theory Invariants_AI

lemma tcb_to_itcb_simps[simp]:
  "itcb_state (tcb_to_itcb tcb) = tcb_state tcb"
  "itcb_fault_handler (tcb_to_itcb tcb) = tcb_fault_handler tcb"
  "itcb_ipc_buffer (tcb_to_itcb tcb) = tcb_ipc_buffer tcb"
  "itcb_fault (tcb_to_itcb tcb) = tcb_fault tcb"
  "itcb_bound_notification (tcb_to_itcb tcb) = tcb_bound_notification tcb"
  "itcb_mcpriority (tcb_to_itcb tcb) = tcb_mcpriority tcb"
  "itcb_arch (tcb_to_itcb tcb) = tcb_iarch tcb" by (auto simp: tcb_to_itcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (itcb_state (tcb_to_itcb tcb) = tcb_state tcb &&& itcb_fault_handler (tcb_to_itcb tcb) = tcb_fault_handler tcb &&& itcb_ipc_buffer (tcb_to_itcb tcb) = tcb_ipc_buffer tcb) &&& (itcb_fault (tcb_to_itcb tcb) = tcb_fault tcb &&& itcb_bound_notification (tcb_to_itcb tcb) = tcb_bound_notification tcb) &&& itcb_mcpriority (tcb_to_itcb tcb) = tcb_mcpriority tcb &&& itcb_arch (tcb_to_itcb tcb) = tcb_iarch tcb
theory Invariants_AI

lemma st_tcb_at_def: "st_tcb_at test \<equiv> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> test (tcb_state tcb))" by (simp add: pred_tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at test \<equiv> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> test (tcb_state tcb))
theory Invariants_AI

lemma cte_wp_at_lift:
  "\<lbrakk>cte_wp_at P p s ; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> cte_wp_at Q p s" by (fastforce simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> cte_wp_at Q p s
theory Invariants_AI

lemma obj_at_eq_helper:
  "\<lbrakk> \<And>obj. P obj = P' obj \<rbrakk> \<Longrightarrow> obj_at P = obj_at P'" apply (rule ext)+ apply (simp add: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>obj. P obj = P' obj) \<Longrightarrow> obj_at P = obj_at P' proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<And>obj. P obj = P' obj) \<Longrightarrow> obj_at P x xa = obj_at P' x xa proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma is_ep_def2: "(is_ep ko) = bound (partial_inv Endpoint ko)" by (auto simp: is_ep_def split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_ep ko = (partial_inv Endpoint ko \<noteq> None)
theory Invariants_AI

lemma ep_at_def2: "ep_at = (obj_at (\<lambda>ko. bound (partial_inv Endpoint ko)))" by (rule obj_at_eq_helper, simp add: is_ep_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at = obj_at (\<lambda>ko. partial_inv Endpoint ko \<noteq> None)
theory Invariants_AI

lemma is_ntfn_def2: "(is_ntfn ko) = bound (partial_inv Notification ko)" by (auto simp: is_ntfn_def split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_ntfn ko = (partial_inv Notification ko \<noteq> None)
theory Invariants_AI

lemma ntfn_at_def2: "ntfn_at = (obj_at (\<lambda>ko. bound (partial_inv Notification ko)))" by (rule obj_at_eq_helper, simp add: is_ntfn_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_at = obj_at (\<lambda>ko. partial_inv Notification ko \<noteq> None)
theory Invariants_AI

lemma valid_obj_imp_valid_simple: "valid_obj p ko s \<Longrightarrow> valid_simple_obj ko s" by (clarsimp simp: valid_obj_def valid_simple_obj_def split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj p ko s \<Longrightarrow> valid_simple_obj ko s
theory Invariants_AI

lemma valid_ep_def2: "valid_ep = (\<lambda>x s. valid_simple_obj (Endpoint x) s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ep = (\<lambda>x. valid_simple_obj (Endpoint x))
theory Invariants_AI

lemma valid_ntfn_def2: "valid_ntfn = (\<lambda>x s. valid_simple_obj (Notification x) s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ntfn = (\<lambda>x. valid_simple_obj (Notification x))
theory Invariants_AI

lemma valid_simple_kheap:"\<lbrakk>kheap s p = Some v ;
                 a_type v \<in> {AEndpoint, ANTFN} \<rbrakk>\<Longrightarrow> valid_obj p v s = valid_simple_obj v s" by (auto simp: valid_obj_imp_valid_simple valid_obj_def a_type_def
           split: kernel_object.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some v; is_simple_type v\<rbrakk> \<Longrightarrow> valid_obj p v s = valid_simple_obj v s
theory Invariants_AI

lemma a_type_arch_live:
  "a_type ko = AArch tp \<Longrightarrow> \<not> live0 ko" by (simp add: a_type_def
         split: Structures_A.kernel_object.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a_type ko = AArch tp \<Longrightarrow> \<not> live0 ko
theory Invariants_AI

lemma reply_caps_mdbE:
  assumes hyp:"reply_caps_mdb m cs"
  assumes side_hyp: "cs slot = Some (ReplyCap t False R)"
  obtains ptr R' where "m slot = Some ptr" and "cs ptr = Some (ReplyCap t True R')" using side_hyp hyp by (fastforce simp:reply_caps_mdb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>ptr R'. \<lbrakk>m slot = Some ptr; cs ptr = Some (ReplyCap t True R')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
cs slot = Some (ReplyCap t False R)
reply_caps_mdb m cs

goal (1 subgoal):
 1. (\<And>ptr R'. \<lbrakk>m slot = Some ptr; cs ptr = Some (ReplyCap t True R')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory Invariants_AI

lemma reply_cap_get_tcb_simp[simp]: "reply_cap_get_tcb (ReplyCap t m R) = t" by (simp add: reply_cap_get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_cap_get_tcb (ReplyCap t m R) = t
theory Invariants_AI

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_AI

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_AI

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_AI

lemma is_ep:
  "is_ep ko = (\<exists>ep. ko = Endpoint ep)" unfolding is_ep_def by (cases ko) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_ep ko = (\<exists>ep. ko = Endpoint ep) proof (prove)
goal (1 subgoal):
 1. (case ko of Endpoint p \<Rightarrow> True | _ \<Rightarrow> False) = (\<exists>ep. ko = Endpoint ep)
theory Invariants_AI

lemma is_ntfn:
  "is_ntfn ko = (\<exists>ep. ko = Notification ep)" unfolding is_ntfn_def by (cases ko) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_ntfn ko = (\<exists>ep. ko = Notification ep) proof (prove)
goal (1 subgoal):
 1. (case ko of Notification p \<Rightarrow> True | _ \<Rightarrow> False) = (\<exists>ep. ko = Notification ep)
theory Invariants_AI

lemma is_tcb:
  "is_tcb ko = (\<exists>tcb. ko = TCB tcb)" unfolding is_tcb_def by (cases ko) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb ko = (\<exists>tcb. ko = TCB tcb) proof (prove)
goal (1 subgoal):
 1. (case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False) = (\<exists>tcb. ko = TCB tcb)
theory Invariants_AI

lemma is_cap_table:
  "is_cap_table bits ko =
  (\<exists>cs. ko = CNode bits cs \<and> well_formed_cnode_n bits cs)" unfolding is_cap_table_def by (cases ko) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cap_table bits ko = (\<exists>cs. ko = CNode bits cs \<and> well_formed_cnode_n bits cs) proof (prove)
goal (1 subgoal):
 1. (case ko of CNode sz cs \<Rightarrow> bits = sz \<and> well_formed_cnode_n bits cs | _ \<Rightarrow> False) = (\<exists>cs. ko = CNode bits cs \<and> well_formed_cnode_n bits cs)
theory Invariants_AI

lemma obj_at_get_object:
  "obj_at P ref s \<Longrightarrow> fst (get_object ref s) \<noteq> {}" by (auto simp: obj_at_def get_object_def gets_def get_def
                 return_def assert_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P ref s \<Longrightarrow> fst (get_object ref s) \<noteq> {}