kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchInvariants_AI

lemma vs_lookup_trans_ptr_eq':
  "(a, b) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> fst a = fst b \<longrightarrow> snd b = snd a" apply (erule rtrancl_induct) apply simp apply clarsimp apply (cases a) apply clarsimp apply (drule vs_lookup1D) apply clarsimp apply (frule vs_lookup1_trans_is_append) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> fst a = fst b \<longrightarrow> snd b = snd a proof (prove)
goal (2 subgoals):
 1. fst a = fst a \<longrightarrow> snd a = snd a
 2. \<And>y z. \<lbrakk>(a, y) \<in> (vs_lookup1 s)\<^sup>*; (y, z) \<in> vs_lookup1 s; fst a = fst y \<longrightarrow> snd y = snd a\<rbrakk> \<Longrightarrow> fst a = fst z \<longrightarrow> snd z = snd a proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(a, y) \<in> (vs_lookup1 s)\<^sup>*; (y, z) \<in> vs_lookup1 s; fst a = fst y \<longrightarrow> snd y = snd a\<rbrakk> \<Longrightarrow> fst a = fst z \<longrightarrow> snd z = snd a proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba. \<lbrakk>(a, aa, b) \<in> (vs_lookup1 s)\<^sup>*; ((aa, b), fst a, ba) \<in> vs_lookup1 s; fst a = aa \<longrightarrow> b = snd a\<rbrakk> \<Longrightarrow> ba = snd a proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba aaa bb. \<lbrakk>(a, aa, b) \<in> (vs_lookup1 s)\<^sup>*; ((aa, b), fst a, ba) \<in> vs_lookup1 s; fst a = aa \<longrightarrow> b = snd a; a = (aaa, bb)\<rbrakk> \<Longrightarrow> ba = snd a proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba aaa bb. \<lbrakk>((aaa, bb), aa, b) \<in> (vs_lookup1 s)\<^sup>*; ((aa, b), aaa, ba) \<in> vs_lookup1 s; aaa = aa \<longrightarrow> b = bb; a = (aaa, bb)\<rbrakk> \<Longrightarrow> ba = bb proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba aaa bb. \<lbrakk>((aaa, bb), aa, b) \<in> (vs_lookup1 s)\<^sup>*; aaa = aa \<longrightarrow> b = bb; a = (aaa, bb); \<exists>rs r p p' ko. (aa, b) = (rs, p) \<and> (aaa, ba) = (r # rs, p') \<and> ko_at ko p s \<and> (r, p') \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ba = bb proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba bb r ko. \<lbrakk>((r # aa, bb), aa, b) \<in> (vs_lookup1 s)\<^sup>*; a = (r # aa, bb); ko_at ko b s; (r, ba) \<in> vs_refs ko\<rbrakk> \<Longrightarrow> ba = bb proof (prove)
goal (1 subgoal):
 1. \<And>aa b ba bb r ko. \<lbrakk>((r # aa, bb), aa, b) \<in> (vs_lookup1 s)\<^sup>*; a = (r # aa, bb); ko_at ko b s; (r, ba) \<in> vs_refs ko; \<exists>zs. aa = zs @ r # aa\<rbrakk> \<Longrightarrow> ba = bb proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma vs_lookup_trans_ptr_eq:
  "((r,p), (r,p')) \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> p = p'" by (drule vs_lookup_trans_ptr_eq') simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, p), r, p') \<in> (vs_lookup1 s)\<^sup>* \<Longrightarrow> p = p'
theory ArchInvariants_AI

lemma vs_lookup_atE:
  "([VSRef (ucast asid) None] \<rhd> p) s \<Longrightarrow> (arm_asid_table (arch_state s) asid = Some p \<Longrightarrow> P) \<Longrightarrow> P" by (blast dest: vs_lookup_atD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>([VSRef (UCAST(7 \<rightarrow> 32) asid) None] \<rhd> p) s; asid_table s asid = Some p \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory ArchInvariants_AI

lemma vs_lookup_2ConsD:
  "((v # v' # vs) \<rhd> p) s \<Longrightarrow> \<exists>p'. ((v'#vs) \<rhd> p') s \<and> ((v' # vs,p') \<rhd>1 (v # v' # vs, p)) s" apply (clarsimp simp: vs_lookup_def) apply (erule rtranclE) apply (clarsimp simp: vs_asid_refs_def) apply (fastforce simp: vs_lookup1_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v # v' # vs) \<rhd> p) s \<Longrightarrow> \<exists>p'. ((v' # vs) \<rhd> p') s \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((a, b), v # v' # vs, p) \<in> (vs_lookup1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup1 s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); (a, b) = (v # v' # vs, p)\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup1 s
 2. \<And>a b y. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); ((a, b), y) \<in> (vs_lookup1 s)\<^sup>*; (y, v # v' # vs, p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); ((a, b), y) \<in> (vs_lookup1 s)\<^sup>*; (y, v # v' # vs, p) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup1 s proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

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

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

lemma pspace_in_kernel_window_arch_update[simp]:
  "arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s)
     \<Longrightarrow> pspace_in_kernel_window (arch_state_update f s) = pspace_in_kernel_window s" by (simp add: pspace_in_kernel_window_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s) \<Longrightarrow> pspace_in_kernel_window (arch_state_update f s) = pspace_in_kernel_window s
theory ArchInvariants_AI

lemma vs_cap_ref_eq_imp_table_cap_ref_eq:
  "is_pg_cap cap = is_pg_cap cap' \<Longrightarrow> vs_cap_ref cap = vs_cap_ref cap'
   \<Longrightarrow> table_cap_ref cap = table_cap_ref cap'" by (auto simp: is_arch_cap_simps vs_cap_ref_def table_cap_ref_simps
                  arch_cap_fun_lift_def
          split: cap.splits arch_cap.splits vmpage_size.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_pg_cap cap = is_pg_cap cap'; vs_cap_ref cap = vs_cap_ref cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref cap'
theory ArchInvariants_AI

lemma acap_rights_update_id [intro!, simp]:
  "\<lbrakk>wellformed_acap cap\<rbrakk> \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap" unfolding wellformed_acap_def acap_rights_update_def by (auto split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_acap cap \<Longrightarrow> acap_rights_update (acap_rights cap) cap = cap proof (prove)
goal (1 subgoal):
 1. case cap of ASIDPoolCap r as \<Rightarrow> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some x \<Rightarrow> wellformed_mapdata sz x) | PageTableCap r None \<Rightarrow> True | PageTableCap r (Some mapdata) \<Rightarrow> wellformed_mapdata ARMSection mapdata | PageDirectoryCap r None \<Rightarrow> True | PageDirectoryCap r (Some asid) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<Longrightarrow> (case cap of PageCap dev x rs' sz as \<Rightarrow> PageCap dev x (validate_vm_rights (acap_rights cap)) sz as | _ \<Rightarrow> cap) = cap
theory ArchInvariants_AI

lemma in_user_frame_def:
  "in_user_frame p \<equiv> \<lambda>s.
   \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s" apply (rule eq_reflection, rule ext) apply (simp add: in_user_frame_def obj_at_def) apply (rule_tac f=Ex in arg_cong) apply (rule ext, rule iffI) apply (simp add: a_type_simps) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. in_user_frame p \<equiv> \<lambda>s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. in_user_frame p s = (\<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))) = (\<exists>sz ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<lambda>sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))) = (\<lambda>sz. \<exists>ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz)) proof (prove)
goal (2 subgoals):
 1. \<And>s sz. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)) \<Longrightarrow> \<exists>ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz)
 2. \<And>s sz. \<exists>ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) \<Longrightarrow> kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)) proof (prove)
goal (1 subgoal):
 1. \<And>s sz. \<exists>ko. kheap s (p && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz) \<Longrightarrow> kheap s (p && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz)) proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma in_user_frame_lift:
 assumes typ_at: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>_. typ_at (AArch T) p\<rbrace>"
 shows "\<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>" unfolding in_user_frame_def by (wp hoare_vcg_ex_lift typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace> f \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace>
theory ArchInvariants_AI

lemma wellformed_arch_default:
  "arch_valid_obj (default_arch_object aobject_type dev us) s" unfolding arch_valid_obj_def default_arch_object_def by (cases aobject_type; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_valid_obj (default_arch_object aobject_type dev us) s proof (prove)
goal (1 subgoal):
 1. wellformed_vspace_obj (case aobject_type of SmallPageObj \<Rightarrow> DataPage dev ARMSmallPage | LargePageObj \<Rightarrow> DataPage dev ARMLargePage | SectionObj \<Rightarrow> DataPage dev ARMSection | SuperSectionObj \<Rightarrow> DataPage dev ARMSuperSection | PageTableObj \<Rightarrow> PageTable (\<lambda>x. InvalidPTE) | PageDirectoryObj \<Rightarrow> PageDirectory (\<lambda>x. InvalidPDE) | ASIDPoolObj \<Rightarrow> ASIDPool (\<lambda>_. None))
theory ArchInvariants_AI

lemma valid_vspace_obj_default':
  "valid_vspace_obj (default_arch_object aobject_type dev us) s" unfolding default_arch_object_def by (cases aobject_type; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_obj (default_arch_object aobject_type dev us) s proof (prove)
goal (1 subgoal):
 1. valid_vspace_obj (case aobject_type of SmallPageObj \<Rightarrow> DataPage dev ARMSmallPage | LargePageObj \<Rightarrow> DataPage dev ARMLargePage | SectionObj \<Rightarrow> DataPage dev ARMSection | SuperSectionObj \<Rightarrow> DataPage dev ARMSuperSection | PageTableObj \<Rightarrow> PageTable (\<lambda>x. InvalidPTE) | PageDirectoryObj \<Rightarrow> PageDirectory (\<lambda>x. InvalidPDE) | ASIDPoolObj \<Rightarrow> ASIDPool (\<lambda>_. None)) s
theory ArchInvariants_AI

lemma tcb_hyp_refs_of_simps[simp]:
  "tcb_hyp_refs atcb = {}" by (auto simp: tcb_hyp_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_hyp_refs atcb = {}
theory ArchInvariants_AI

lemma hyp_refs_of_simps[simp]:
  "hyp_refs_of (CNode sz fun) = {}"
  "hyp_refs_of (TCB tcb) = tcb_hyp_refs (tcb_arch tcb)"
  "hyp_refs_of (Endpoint ep) = {}"
  "hyp_refs_of (Notification ntfn) = {}"
  "hyp_refs_of (ArchObj ao) = refs_of_a ao" by (auto simp: hyp_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (hyp_refs_of (CNode sz fun) = {} &&& hyp_refs_of (TCB tcb) = tcb_hyp_refs (tcb_arch tcb)) &&& hyp_refs_of (Endpoint ep) = {} &&& hyp_refs_of (Notification ntfn) = {} &&& hyp_refs_of (ArchObj ao) = refs_of_a ao
theory ArchInvariants_AI

lemma state_hyp_refs_of_elemD:
  "\<lbrakk> ref \<in> state_hyp_refs_of s x \<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. ref \<in> hyp_refs_of obj) x s" by (clarsimp simp add: state_hyp_refs_of_def obj_at_def
                  split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ref \<in> state_hyp_refs_of s x \<Longrightarrow> obj_at (\<lambda>obj. ref \<in> hyp_refs_of obj) x s
theory ArchInvariants_AI

lemma state_hyp_refs_of_eqD:
  "\<lbrakk> state_hyp_refs_of s x = S; S \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. hyp_refs_of obj = S) x s" by (clarsimp simp add: state_hyp_refs_of_def obj_at_def
                  split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>state_hyp_refs_of s x = S; S \<noteq> {}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. hyp_refs_of obj = S) x s
theory ArchInvariants_AI

lemma obj_at_state_hyp_refs_ofD:
  "obj_at P p s \<Longrightarrow> \<exists>ko. P ko \<and> state_hyp_refs_of s p = hyp_refs_of ko" apply (clarsimp simp: obj_at_def state_hyp_refs_of_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P p s \<Longrightarrow> \<exists>ko. P ko \<and> state_hyp_refs_of s p = hyp_refs_of ko proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>kheap s p = Some ko; P ko\<rbrakk> \<Longrightarrow> \<exists>koa. P koa \<and> hyp_refs_of ko = hyp_refs_of koa proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma ko_at_state_hyp_refs_ofD:
  "ko_at ko p s \<Longrightarrow> state_hyp_refs_of s p = hyp_refs_of ko" by (clarsimp dest!: obj_at_state_hyp_refs_ofD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at ko p s \<Longrightarrow> state_hyp_refs_of s p = hyp_refs_of ko
theory ArchInvariants_AI

lemma hyp_sym_refs_obj_atD:
  "\<lbrakk> obj_at P p s; sym_refs (state_hyp_refs_of s) \<rbrakk> \<Longrightarrow>
     \<exists>ko. P ko \<and> state_hyp_refs_of s p = hyp_refs_of ko \<and>
        (\<forall>(x, tp)\<in>hyp_refs_of ko. obj_at (\<lambda>ko. (p, symreftype tp) \<in> hyp_refs_of ko) x s)" apply (drule obj_at_state_hyp_refs_ofD) apply (erule exEI, clarsimp) apply (drule sym, simp) apply (drule(1) sym_refsD) apply (erule state_hyp_refs_of_elemD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; sym_refs (state_hyp_refs_of s)\<rbrakk> \<Longrightarrow> \<exists>ko. P ko \<and> state_hyp_refs_of s p = hyp_refs_of ko \<and> (\<forall>(x, tp)\<in>hyp_refs_of ko. obj_at (\<lambda>ko. (p, symreftype tp) \<in> hyp_refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs (state_hyp_refs_of s); \<exists>ko. P ko \<and> state_hyp_refs_of s p = hyp_refs_of ko\<rbrakk> \<Longrightarrow> \<exists>ko. P ko \<and> state_hyp_refs_of s p = hyp_refs_of ko \<and> (\<forall>(x, tp)\<in>hyp_refs_of ko. obj_at (\<lambda>ko. (p, symreftype tp) \<in> hyp_refs_of ko) x s) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>sym_refs (state_hyp_refs_of s); (a, b) \<in> hyp_refs_of x; P x; state_hyp_refs_of s p = hyp_refs_of x\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (p, symreftype b) \<in> hyp_refs_of ko) a s proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>sym_refs (state_hyp_refs_of s); (a, b) \<in> state_hyp_refs_of s p; P x; hyp_refs_of x = state_hyp_refs_of s p\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (p, symreftype b) \<in> hyp_refs_of ko) a s proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>sym_refs (state_hyp_refs_of s); P x; hyp_refs_of x = state_hyp_refs_of s p; (p, symreftype b) \<in> state_hyp_refs_of s a\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (p, symreftype b) \<in> hyp_refs_of ko) a s proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma state_hyp_refs_of_pspaceI:
  "\<lbrakk> P (state_hyp_refs_of s); kheap s = kheap s' \<rbrakk> \<Longrightarrow> P (state_hyp_refs_of s')" unfolding state_hyp_refs_of_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (state_hyp_refs_of s); kheap s = kheap s'\<rbrakk> \<Longrightarrow> P (state_hyp_refs_of s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (\<lambda>x. case kheap s x of None \<Rightarrow> {} | Some ko \<Rightarrow> hyp_refs_of ko); kheap s = kheap s'\<rbrakk> \<Longrightarrow> P (\<lambda>x. case kheap s' x of None \<Rightarrow> {} | Some ko \<Rightarrow> hyp_refs_of ko)
theory ArchInvariants_AI

lemma state_hyp_refs_update[iff]:
  "kheap (f s) = kheap s \<Longrightarrow> state_hyp_refs_of (f s) = state_hyp_refs_of s" by (clarsimp simp: state_hyp_refs_of_def
                  split: option.splits cong: option.case_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap (f s) = kheap s \<Longrightarrow> state_hyp_refs_of (f s) = state_hyp_refs_of s
theory ArchInvariants_AI

lemma hyp_refs_of_hyp_live:
  "hyp_refs_of ko \<noteq> {} \<Longrightarrow> hyp_live ko" apply (cases ko, simp_all add: hyp_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hyp_refs_of ko \<noteq> {} \<Longrightarrow> hyp_live ko proof (prove)
goal:
No subgoals!
theory ArchInvariants_AI

lemma hyp_refs_of_hyp_live_obj:
  "\<lbrakk> obj_at P p s; \<And>ko. \<lbrakk> P ko; hyp_refs_of ko = {} \<rbrakk> \<Longrightarrow> False \<rbrakk> \<Longrightarrow> obj_at hyp_live p s" by (fastforce simp: obj_at_def hyp_refs_of_hyp_live)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; \<And>ko. \<lbrakk>P ko; hyp_refs_of ko = {}\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> obj_at hyp_live p s
theory ArchInvariants_AI

lemma valid_tcb_arch_ref_lift:
  "tcb_arch_ref t = tcb_arch_ref t' \<Longrightarrow> valid_arch_tcb (tcb_arch t) = valid_arch_tcb (tcb_arch t')" by (simp add: valid_arch_tcb_def tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_arch_ref t = tcb_arch_ref t' \<Longrightarrow> valid_arch_tcb (tcb_arch t) = valid_arch_tcb (tcb_arch t')
theory ArchInvariants_AI

lemma valid_arch_tcb_context_update[simp]:
  "valid_arch_tcb (tcb_context_update f t) = valid_arch_tcb t" unfolding valid_arch_tcb_def obj_at_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_tcb (tcb_context_update f t) = valid_arch_tcb t proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. True) = (\<lambda>_. True)
theory ArchInvariants_AI

lemma valid_arch_arch_tcb_context_set[simp]:
  "valid_arch_tcb (arch_tcb_context_set a t) = valid_arch_tcb t" by (simp add: arch_tcb_context_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_tcb (arch_tcb_context_set a t) = valid_arch_tcb t
theory ArchInvariants_AI

lemma tcb_arch_ref_context_update:
  "tcb_arch_ref (t\<lparr>tcb_arch := (arch_tcb_context_set a (tcb_arch t))\<rparr>) = tcb_arch_ref t" by (simp add: tcb_arch_ref_def arch_tcb_context_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_arch_ref (t\<lparr>tcb_arch := arch_tcb_context_set a (tcb_arch t)\<rparr>) = tcb_arch_ref t
theory ArchInvariants_AI

lemma tcb_arch_ref_set_registers:
  "tcb_arch_ref (tcb\<lparr>tcb_arch := arch_tcb_set_registers regs (tcb_arch tcb)\<rparr>) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_arch_ref (tcb\<lparr>tcb_arch := arch_tcb_set_registers regs (tcb_arch tcb)\<rparr>) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma valid_arch_arch_tcb_set_registers[simp]:
  "valid_arch_tcb (arch_tcb_set_registers a t) = valid_arch_tcb t" by (simp add: arch_tcb_set_registers_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_tcb (arch_tcb_set_registers a t) = valid_arch_tcb t
theory ArchInvariants_AI

lemma tcb_arch_ref_ipc_buffer_update: "\<And>tcb.
       tcb_arch_ref (tcb_ipc_buffer_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_ipc_buffer_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_ctable_update: "\<And>tcb.
       tcb_arch_ref (tcb_ctable_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_ctable_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_vtable_update: "\<And>tcb.
       tcb_arch_ref (tcb_vtable_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_vtable_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_reply_update: "\<And>tcb.
       tcb_arch_ref (tcb_reply_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_reply_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_ipcframe_update: "\<And>tcb.
       tcb_arch_ref (tcb_ipcframe_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_ipcframe_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_state_update: "\<And>tcb.
       tcb_arch_ref (tcb_state_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_state_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_fault_handler_update: "\<And>tcb.
       tcb_arch_ref (tcb_fault_handler_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_fault_handler_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_fault_update: "\<And>tcb.
       tcb_arch_ref (tcb_fault_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_fault_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma tcb_arch_ref_bound_notification_update: "\<And>tcb.
       tcb_arch_ref (tcb_bound_notification_update f tcb) = tcb_arch_ref tcb" by (simp add: tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tcb. tcb_arch_ref (tcb_bound_notification_update f tcb) = tcb_arch_ref tcb
theory ArchInvariants_AI

lemma hyp_live_tcb_def: "hyp_live (TCB tcb) = bound (tcb_arch_ref tcb)" by (clarsimp simp: hyp_live_def tcb_arch_ref_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hyp_live (TCB tcb) = (tcb_arch_ref tcb \<noteq> None)