kings-crown/FVELER_Isabelle huggingface dataset:
theory BCorres_UL

lemma gets_the_bcorres_underlying[wp]:
  "(\<And>s. f' (t s) = f s) \<Longrightarrow> bcorres_underlying t (gets_the f) (gets_the f')" by (wpsimp simp: gets_the_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. f' (t s) = f s) \<Longrightarrow> bcorres_underlying t (gets_the f) (gets_the f')
theory BCorres_AI

lemma dxo_bcorres[wp]:
  "bcorres (do_extended_op f) (do_extended_op f)" apply (simp add: do_extended_op_def) apply (simp add: bind_def select_f_def modify_def return_def get_def put_def gets_def) apply (simp add: split_def) apply (simp add: bcorres_underlying_def s_bcorres_underlying_def) apply (clarsimp simp: mk_ef_def wrap_ext_op_unit_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (do_extended_op f) (do_extended_op f) proof (prove)
goal (1 subgoal):
 1. bcorres (do ex <- get;
(uu_, es') <- select_f (mk_ef (wrap_ext_op f ex));
modify (exst_update (\<lambda>_. exst es'))
od) (do ex <- get;
(uu_, es') <- select_f (mk_ef (wrap_ext_op f ex));
modify (exst_update (\<lambda>_. ()))
od) proof (prove)
goal (1 subgoal):
 1. bcorres (\<lambda>s. (\<Union>a\<in>fst (mk_ef (wrap_ext_op f s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (uu_, es') \<Rightarrow> \<lambda>s. ({((), s\<lparr>exst := exst es'\<rparr>)}, False)) xa), (\<exists>x\<in>fst (mk_ef (wrap_ext_op f s)). snd ((case x of (uu_, es') \<Rightarrow> \<lambda>s. ({((), s\<lparr>exst := exst es'\<rparr>)}, False)) s)) \<or> snd (mk_ef (wrap_ext_op f s)))) (\<lambda>s. (\<Union>a\<in>fst (mk_ef (wrap_ext_op f s)) \<times> {s}. fst (case a of (x, xa) \<Rightarrow> (case x of (uu_, es') \<Rightarrow> \<lambda>s. ({((), s\<lparr>exst := ()\<rparr>)}, False)) xa), snd (mk_ef (wrap_ext_op f s)))) proof (prove)
goal (1 subgoal):
 1. bcorres (\<lambda>s. (\<Union>x\<in>fst (mk_ef (wrap_ext_op f s)) \<times> {s}. {((), snd x\<lparr>exst := exst (snd (fst x))\<rparr>)}, snd (mk_ef (wrap_ext_op f s)))) (\<lambda>s. (\<Union>x\<in>fst (mk_ef (wrap_ext_op f s)) \<times> {s}. {((), snd x\<lparr>exst := ()\<rparr>)}, snd (mk_ef (wrap_ext_op f s)))) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> ((), truncate_state y)) ` (\<Union>x\<in>fst (mk_ef (wrap_ext_op f s)) \<times> {s}. {((), snd x\<lparr>exst := exst (snd (fst x))\<rparr>)}) \<subseteq> (\<Union>x\<in>fst (mk_ef (wrap_ext_op f (truncate_state s))) \<times> {truncate_state s}. {((), snd x\<lparr>exst := ()\<rparr>)}) proof (prove)
goal:
No subgoals!
theory BCorres_AI

lemma bcorres_select_ext[wp]:
  "bcorres (select_ext a A) (select_ext a A)" by (clarsimp simp: select_ext_def bind_def gets_def return_def select_def assert_def get_def
                     select_switch_unit_def bcorres_underlying_def s_bcorres_underlying_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (select_ext a A) (select_ext a A)
theory BCorres_AI

lemma get_cap_det:
  "(r,s') \<in> fst (get_cap p s) \<Longrightarrow> get_cap p s = ({(r,s)}, False)" apply (cases p) apply (clarsimp simp add: in_monad get_cap_def get_object_def
                     split: kernel_object.split_asm) apply (clarsimp simp add: bind_def return_def assert_opt_def simpler_gets_def) apply (simp add: bind_def simpler_gets_def return_def assert_opt_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> get_cap p s = ({(r, s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(r, s') \<in> fst (get_cap p s); p = (a, b)\<rbrakk> \<Longrightarrow> get_cap p s = ({(r, s)}, False) proof (prove)
goal (2 subgoals):
 1. \<And>a b x11 x12. \<lbrakk>p = (a, b); kheap s a = Some (CNode x11 x12); well_formed_cnode_n x11 x12; s' = s; x12 b = Some r\<rbrakk> \<Longrightarrow> (do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
caps <- case obj of CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail;
assert_opt (caps b)
od) s = ({(r, s)}, False)
 2. \<And>a b x2. \<lbrakk>p = (a, b); kheap s a = Some (TCB x2); s' = s; tcb_cnode_map x2 b = Some r\<rbrakk> \<Longrightarrow> (do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
caps <- case obj of CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail;
assert_opt (caps b)
od) s = ({(r, s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>a b x2. \<lbrakk>p = (a, b); kheap s a = Some (TCB x2); s' = s; tcb_cnode_map x2 b = Some r\<rbrakk> \<Longrightarrow> (do obj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
caps <- case obj of CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return (tcb_cnode_map tcb) | _ \<Rightarrow> fail;
assert_opt (caps b)
od) s = ({(r, s)}, False) proof (prove)
goal:
No subgoals!
theory BCorres_AI

lemma get_object_bcorres_any[wp]:
  "bcorres_underlying (trans_state e) (get_object a) (get_object a)" by (wpsimp simp: get_object_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying (trans_state e) (get_object a) (get_object a)
theory BCorres_AI

lemma get_cap_bcorres_any:
  "bcorres_underlying (trans_state e) (get_cap x) (get_cap x)" by (wpsimp simp: get_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres_underlying (trans_state e) (get_cap x) (get_cap x)
theory BCorres_AI

lemma is_final_cap_bcorres[wp]:
  "bcorres (is_final_cap a) (is_final_cap a)" by (simp add: is_final_cap_def is_final_cap'_def gets_def get_cap_helper | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (is_final_cap a) (is_final_cap a)
theory BCorres_AI

lemma get_tcb_truncate[simp]: "get_tcb a (truncate_state s) = get_tcb a s" by (simp add: get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb a (truncate_state s) = get_tcb a s
theory BCorres_AI

lemma fast_finalise_bcorres[wp]:
  "bcorres (fast_finalise a b) (fast_finalise a b)" by (cases a; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (fast_finalise a b) (fast_finalise a b)
theory BCorres_AI

lemma preemption_point_bcorres[wp]:
  "bcorres preemption_point preemption_point" unfolding preemption_point_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres preemption_point preemption_point proof (prove)
goal (1 subgoal):
 1. bcorres (doE liftE $ do_extended_op update_work_units;
OR_choiceE work_units_limit_reached (doE liftE $ do_extended_op reset_work_units;
irq_opt <- liftE $ do_machine_op (getActiveIRQ True);
case irq_opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> K (throwError $ ()) x
odE) (returnOk ())
odE) (doE liftE $ do_extended_op update_work_units;
OR_choiceE work_units_limit_reached (doE liftE $ do_extended_op reset_work_units;
irq_opt <- liftE $ do_machine_op (getActiveIRQ True);
case irq_opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> K (throwError $ ()) x
odE) (returnOk ())
odE)
theory BCorres_AI

lemma gets_the_get_tcb_bcorres[wp]:
  "bcorres (gets_the (get_tcb a)) (gets_the (get_tcb a)) " by (wpsimp simp: gets_the_def bcorres_underlying_def assert_opt_def split: option.splits|rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bcorres (gets_the (get_tcb a)) (gets_the (get_tcb a))
theory ArchLevityCatch_AI

lemma asid_high_bits_of_shift :
  "asid_high_bits_of (ucast x << asid_low_bits) = x" apply (simp add: asid_high_bits_of_def) apply (rule word_eqI) apply (simp add: word_size nth_ucast nth_shiftr nth_shiftl asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_high_bits_of (UCAST(7 \<rightarrow> 32) x << local.asid_low_bits) = x proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 7) (UCAST(7 \<rightarrow> 32) x << local.asid_low_bits >> local.asid_low_bits) = x proof (prove)
goal (1 subgoal):
 1. \<And>n. n < size (UCAST(32 \<rightarrow> 7) (UCAST(7 \<rightarrow> 32) x << local.asid_low_bits >> local.asid_low_bits)) \<longrightarrow> UCAST(32 \<rightarrow> 7) (UCAST(7 \<rightarrow> 32) x << local.asid_low_bits >> local.asid_low_bits) !! n = x !! n proof (prove)
goal:
No subgoals!
theory ArchLevityCatch_AI

lemma  ptrFormPAddr_addFromPPtr :
  "ptrFromPAddr (Platform.ARM.addrFromPPtr x) = x" by (simp add: ptrFromPAddr_def Platform.ARM.addrFromPPtr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptrFromPAddr (addrFromPPtr x) = x
theory ArchLevityCatch_AI

lemma asid_high_bits_of_add_ucast:
  "is_aligned w asid_low_bits \<Longrightarrow>
  asid_high_bits_of (ucast (x::10 word) + w) = asid_high_bits_of w" apply (rule word_eqI) apply (simp add: word_size asid_high_bits_of_def is_aligned_nth) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply clarsimp apply (drule test_bit_size) apply (simp add: asid_low_bits_def) apply (auto dest: test_bit_size simp: word_size asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned w local.asid_low_bits \<Longrightarrow> asid_high_bits_of (UCAST(10 \<rightarrow> 32) x + w) = asid_high_bits_of w proof (prove)
goal (1 subgoal):
 1. \<And>n. is_aligned w local.asid_low_bits \<Longrightarrow> n < size (asid_high_bits_of (UCAST(10 \<rightarrow> 32) x + w)) \<longrightarrow> asid_high_bits_of (UCAST(10 \<rightarrow> 32) x + w) !! n = asid_high_bits_of w !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> n < 7 \<longrightarrow> (UCAST(10 \<rightarrow> 32) x + w) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> UCAST(10 \<rightarrow> 32) x && w = 0
 2. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> n < 7 \<longrightarrow> (UCAST(10 \<rightarrow> 32) x || w) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> na < size (UCAST(10 \<rightarrow> 32) x && w) \<longrightarrow> (UCAST(10 \<rightarrow> 32) x && w) !! na = 0 !! na
 2. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> n < 7 \<longrightarrow> (UCAST(10 \<rightarrow> 32) x || w) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>n<local.asid_low_bits. \<not> w !! n; na < size (UCAST(10 \<rightarrow> 32) x && w); x !! na; na < 32; w !! na\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> n < 7 \<longrightarrow> (UCAST(10 \<rightarrow> 32) x || w) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>n<local.asid_low_bits. \<not> w !! n; na < size (UCAST(10 \<rightarrow> 32) x && w); na < 32; w !! na; na < size x\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> n < 7 \<longrightarrow> (UCAST(10 \<rightarrow> 32) x || w) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>n<10. \<not> w !! n; na < size (UCAST(10 \<rightarrow> 32) x && w); na < 32; w !! na; na < size x\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<forall>n<local.asid_low_bits. \<not> w !! n \<Longrightarrow> n < 7 \<longrightarrow> (UCAST(10 \<rightarrow> 32) x || w) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal:
No subgoals!
theory ArchLevityCatch_AI

lemma pageBits_less_word_bits [simp]:
  "pageBits < word_bits" by (simp add: pageBits_def word_bits_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBits < word_bits
theory ArchLevityCatch_AI

lemma aobj_ref_arch_cap[simp]:
  "aobj_ref (arch_default_cap aty ptr us dev) = Some ptr" apply (case_tac aty) apply (simp_all add: aobj_ref_def arch_default_cap_def p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aobj_ref (arch_default_cap aty ptr us dev) = Some ptr proof (prove)
goal (7 subgoals):
 1. aty = SmallPageObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr
 2. aty = LargePageObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr
 3. aty = SectionObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr
 4. aty = SuperSectionObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr
 5. aty = PageTableObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr
 6. aty = PageDirectoryObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr
 7. aty = ASIDPoolObj \<Longrightarrow> aobj_ref (arch_default_cap aty ptr us dev) = Some ptr proof (prove)
goal:
No subgoals!
theory LevityCatch_AI

lemma detype_arch_state:
  "arch_state (detype S s) = arch_state s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_state (detype S s) = arch_state s
theory LevityCatch_AI

lemma obj_ref_elemD:
  "r \<in> obj_refs cap \<Longrightarrow> obj_refs cap = {r}" by (cases cap; simp)

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

lemma get_cap_id:
  "(v, s') \<in> fst (get_cap p s) \<Longrightarrow> (s' = s)" by (clarsimp simp: get_cap_def get_object_def in_monad split_def
              split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (v, s') \<in> fst (get_cap p s) \<Longrightarrow> s' = s
theory LevityCatch_AI

lemma None_Some_strg:
  "x = None \<Longrightarrow> x \<noteq> Some y" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = None \<Longrightarrow> x \<noteq> Some y
theory LevityCatch_AI

lemma const_on_failure_wp:
  "\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> const_on_failure n m \<lbrace>Q\<rbrace>" by (wpsimp simp: const_on_failure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv. Q n\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> const_on_failure n m \<lbrace>Q\<rbrace>
theory LevityCatch_AI

lemma select_ext_weak_wp[wp]:
  "\<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select_ext a S \<lbrace>Q\<rbrace>" by (wpsimp simp: select_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select_ext a S \<lbrace>Q\<rbrace>
theory LevityCatch_AI

lemma select_ext_wp[wp]:
  "\<lbrace>\<lambda>s. a s \<in> S \<longrightarrow> Q (a s) s\<rbrace> select_ext a S \<lbrace>Q\<rbrace>" unfolding select_ext_def unwrap_ext_det_ext_ext_def by (wpsimp simp: select_switch_det_ext_ext_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. a s \<in> S \<longrightarrow> Q (a s) s\<rbrace> select_ext a S \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. a s \<in> S \<longrightarrow> Q (a s) s\<rbrace> do s <- get;
x <- if select_switch (exst s) then return (a s) else select S;
assert (x \<in> S);
return x
od \<lbrace>Q\<rbrace>
theory InvariantsPre_AI

lemma obj_at_pspaceI:
  "\<lbrakk> obj_at P ref s; kheap s = kheap s' \<rbrakk> \<Longrightarrow> obj_at P ref s'" by (simp add: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P ref s; kheap s = kheap s'\<rbrakk> \<Longrightarrow> obj_at P ref s'
theory InvariantsPre_AI

lemma obj_atE:
  "\<lbrakk> obj_at P p s; \<And>ko. \<lbrakk> kheap s p = Some ko; P ko \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (auto simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; \<And>ko. \<lbrakk>kheap s p = Some ko; P ko\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory InvariantsPre_AI

lemma obj_at_weakenE:
  "\<lbrakk> obj_at P r s; \<And>ko. P ko \<Longrightarrow> P' ko \<rbrakk> \<Longrightarrow> obj_at P' r s" by (clarsimp simp: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P r s; \<And>ko. P ko \<Longrightarrow> P' ko\<rbrakk> \<Longrightarrow> obj_at P' r s
theory InvariantsPre_AI

lemma ko_at_weakenE:
  "\<lbrakk> ko_at k ptr s; P k \<rbrakk> \<Longrightarrow> obj_at P ptr s" by (erule obj_at_weakenE, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at k ptr s; P k\<rbrakk> \<Longrightarrow> obj_at P ptr s
theory InvariantsPre_AI

lemma [simp]:
  "a_type (Endpoint x) = AEndpoint"
  "a_type (Notification v) = ANTFN" by (simp_all add: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a_type (Endpoint x) = AEndpoint &&& a_type (Notification v) = ANTFN
theory InvariantsPre_AI

lemma a_type_aa_type: "(a_type (ArchObj ako) = AArch T) = (aa_type ako = T)" by (simp add: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a_type (ArchObj ako) = AArch T) = (aa_type ako = T)
theory InvariantsPre_AI

lemma pspace_alignedD [intro?]:
  "\<lbrakk> kheap s p = Some ko; pspace_aligned s \<rbrakk> \<Longrightarrow> is_aligned p (obj_bits ko)" unfolding pspace_aligned_def by (drule bspec, blast, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned p (obj_bits ko) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x)))\<rbrakk> \<Longrightarrow> is_aligned p (obj_bits ko)
theory InvariantsPre_AI

lemma pspace_distinctD:
  "\<lbrakk> kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; pspace_distinct s \<rbrakk>
   \<Longrightarrow> mask_range x (obj_bits ko) \<inter> mask_range y (obj_bits ko') = {}" by (simp add: pspace_distinct_def mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some ko; kheap s y = Some ko'; x \<noteq> y; pspace_distinct s\<rbrakk> \<Longrightarrow> mask_range x (obj_bits ko) \<inter> mask_range y (obj_bits ko') = {}
theory InvariantsPre_AI

lemma symreftype_inverse[simp]:
  "symreftype (symreftype t) = t" by (cases t, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. symreftype (symreftype t) = t
theory InvariantsPre_AI

lemma sym_refsD:
  "\<lbrakk> (y, tp) \<in> st x; sym_refs st \<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> st y" apply (simp add: sym_refs_def) apply (drule spec, drule(1) bspec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, tp) \<in> st x; sym_refs st\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> st y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, tp) \<in> st x; \<forall>x. \<forall>xa\<in>st x. case xa of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> st y\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> st y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(y, tp) \<in> st x; case (y, tp) of (y, tp) \<Rightarrow> (x, symreftype tp) \<in> st y\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> st y proof (prove)
goal:
No subgoals!
theory InvariantsPre_AI

lemma sym_refsE:
  "\<lbrakk> sym_refs st; (y, symreftype tp) \<in> st x \<rbrakk> \<Longrightarrow> (x, tp) \<in> st y" by (drule(1) sym_refsD, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs st; (y, symreftype tp) \<in> st x\<rbrakk> \<Longrightarrow> (x, tp) \<in> st y
theory InvariantsPre_AI

lemma sym_refs_simp:
  "\<lbrakk> sym_refs S \<rbrakk> \<Longrightarrow> ((y, symreftype tp) \<in> S x) = ((x, tp) \<in> S y)" apply safe apply (erule(1) sym_refsE) apply (erule(1) sym_refsD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_refs S \<Longrightarrow> ((y, symreftype tp) \<in> S x) = ((x, tp) \<in> S y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sym_refs S; (y, symreftype tp) \<in> S x\<rbrakk> \<Longrightarrow> (x, tp) \<in> S y
 2. \<lbrakk>sym_refs S; (x, tp) \<in> S y\<rbrakk> \<Longrightarrow> (y, symreftype tp) \<in> S x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs S; (x, tp) \<in> S y\<rbrakk> \<Longrightarrow> (y, symreftype tp) \<in> S x proof (prove)
goal:
No subgoals!
theory InvariantsPre_AI

lemma delta_sym_refs:
  assumes x: "sym_refs rfs'"
      and y: "\<And>x y tp. \<lbrakk> (y, tp) \<in> rfs x; (y, tp) \<notin> rfs' x \<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> rfs y"
      and z: "\<And>x y tp. \<lbrakk> (y, tp) \<in> rfs' x; (y, tp) \<notin> rfs x \<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> rfs y"
  shows      "sym_refs rfs" unfolding sym_refs_def apply clarsimp apply (case_tac "(a, b) \<in> rfs' x") apply (drule sym_refsD [OF _ x]) apply (rule ccontr) apply (frule(1) z) apply simp apply (erule(1) y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_refs rfs proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<forall>(y, tp)\<in>rfs x. (x, symreftype tp) \<in> rfs y proof (prove)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> rfs x \<Longrightarrow> (x, symreftype b) \<in> rfs a proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (a, b) \<in> rfs' x\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a
 2. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (a, b) \<notin> rfs' x\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (x, symreftype b) \<in> rfs' a\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a
 2. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (a, b) \<notin> rfs' x\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (x, symreftype b) \<in> rfs' a; (x, symreftype b) \<notin> rfs a\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (a, b) \<notin> rfs' x\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a proof (prove)
goal (2 subgoals):
 1. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (x, symreftype b) \<in> rfs' a; (x, symreftype b) \<notin> rfs a; (a, symreftype (symreftype b)) \<notin> rfs x\<rbrakk> \<Longrightarrow> False
 2. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (a, b) \<notin> rfs' x\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a proof (prove)
goal (1 subgoal):
 1. \<And>x a b. \<lbrakk>(a, b) \<in> rfs x; (a, b) \<notin> rfs' x\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> rfs a proof (prove)
goal:
No subgoals!
theory InvariantsPre_AI

lemma inj_IRQRef[simp]: "inj IRQRef" by (auto intro!: injI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj IRQRef
theory InvariantsPre_AI

lemma inj_ArchRef[simp]: "inj ArchRef" by (auto intro!: injI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj ArchRef