kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpaceInv_AI

lemma if_unsafe_then_cap_more_update[iff]:
  "if_unsafe_then_cap (trans_state f s) = if_unsafe_then_cap s" by (simp add: if_unsafe_then_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_unsafe_then_cap (trans_state f s) = if_unsafe_then_cap s
theory CSpaceInv_AI

lemma set_cdt_caps_of_state:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: set_cdt_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (caps_of_state s) \<Longrightarrow> P (caps_of_state (s\<lparr>cdt := m\<rparr>)) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma ex_cte_cap_to_cnode_always_appropriate_strg:
  "ex_cte_cap_wp_to is_cnode_cap p s
    \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s" by (clarsimp elim!: ex_cte_cap_wp_to_weakenE
                simp: is_cap_simps appropriate_cte_cap_def
               split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to is_cnode_cap p s \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) p s
theory CSpaceInv_AI

lemma update_cdt_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> update_cdt f \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (simp add: update_cdt_def set_cdt_def) apply wp apply (clarsimp elim!: state_refs_of_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> update_cdt f \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := f t\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_refs_of s) \<Longrightarrow> P (state_refs_of (s\<lparr>cdt := f (cdt s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma update_cdt_hyp_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> update_cdt f \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: update_cdt_def set_cdt_def) apply wp apply (clarsimp elim!: state_hyp_refs_of_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> update_cdt f \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := f t\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_hyp_refs_of s) \<Longrightarrow> P (state_hyp_refs_of (s\<lparr>cdt := f (cdt s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma state_refs_of_revokable[simp]:
  "state_refs_of (s \<lparr> is_original_cap := m \<rparr>) = state_refs_of s" by (simp add: state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of (s\<lparr>is_original_cap := m\<rparr>) = state_refs_of s
theory CSpaceInv_AI

lemma is_arch_cap_max_free_index[simp]:
  "is_arch_cap (x\<lparr>free_index:=y\<rparr>) = is_arch_cap x" by (auto simp: is_cap_simps free_index_update_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_arch_cap (free_index_update (\<lambda>_. y) x) = is_arch_cap x
theory CSpaceInv_AI

lemma set_untyped_cap_full_valid_objs:
  "\<lbrace>valid_objs and cte_wp_at ((=) cap) slot\<rbrace>
   set_untyped_cap_as_full cap cap_new slot
   \<lbrace>\<lambda>r. valid_objs\<rbrace>" apply (simp add: set_untyped_cap_as_full_def split del: if_split) apply (wp set_cap_valid_objs) apply (clarsimp simp: tcb_cap_valid_caps_of_stateD cte_wp_at_caps_of_state caps_of_state_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at ((=) cap) slot\<rbrace> set_untyped_cap_as_full cap cap_new slot \<lbrace>\<lambda>r. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at ((=) cap) slot\<rbrace> if is_untyped_cap cap \<and> is_untyped_cap cap_new \<and> obj_ref_of cap = obj_ref_of cap_new \<and> cap_bits_untyped cap = cap_bits_untyped cap_new then set_cap (max_free_index_update cap) slot else return () \<lbrace>\<lambda>r. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and cte_wp_at ((=) cap) slot) s \<Longrightarrow> (is_untyped_cap cap \<and> is_untyped_cap cap_new \<and> obj_ref_of cap = obj_ref_of cap_new \<and> cap_bits_untyped cap = cap_bits_untyped cap_new \<longrightarrow> (valid_objs and valid_cap (max_free_index_update cap) and tcb_cap_valid (max_free_index_update cap) slot) s) \<and> (\<not> (is_untyped_cap cap \<and> is_untyped_cap cap_new \<and> obj_ref_of cap = obj_ref_of cap_new \<and> cap_bits_untyped cap = cap_bits_untyped cap_new) \<longrightarrow> valid_objs s) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma set_untyped_cap_as_full_valid_cap:
  "\<lbrace>valid_cap cap\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>" by (clarsimp simp:set_untyped_cap_as_full_def) (wp set_cap_valid_cap)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap cap\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>
theory CSpaceInv_AI

lemma cap_insert_objs [wp]:
 "\<lbrace>valid_objs and valid_cap cap and tcb_cap_valid cap dest\<rbrace>
  cap_insert cap src dest
  \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (simp add: cap_insert_def set_cdt_def update_cdt_def) apply (wp set_cap_valid_objs set_cap_valid_cap set_untyped_cap_as_full_valid_cap
    set_untyped_cap_full_valid_objs get_cap_wp set_untyped_cap_as_full_tcb_cap_valid
    | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap cap and tcb_cap_valid cap dest\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap cap and tcb_cap_valid cap dest\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- set_untyped_cap_as_full src_cap cap src;
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src)\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma cap_insert_valid_cap[wp]:
  "\<lbrace>valid_cap c\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_cap c\<rbrace>" by (wp valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_cap c\<rbrace>
theory CSpaceInv_AI

lemma cap_rights_update_idem [simp]:
  "cap_rights_update R (cap_rights_update R' cap) = cap_rights_update R cap" by (force simp: cap_rights_update_def split: cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_rights_update R (cap_rights_update R' cap) = cap_rights_update R cap
theory CSpaceInv_AI

lemma cap_master_cap_rights [simp]:
  "cap_master_cap (cap_rights_update R cap) = cap_master_cap cap" by (force simp: cap_master_cap_def cap_rights_update_def split: cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap (cap_rights_update R cap) = cap_master_cap cap
theory CSpaceInv_AI

lemma cap_insert_obj_at_other:
  "\<lbrace>\<lambda>s. P' (obj_at P p s) \<and> p \<noteq> fst src \<and> p \<noteq> fst dest\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_ s. P' (obj_at P p s)\<rbrace>" apply (simp add: cap_insert_def update_cdt_def set_cdt_def set_untyped_cap_as_full_def) apply (rule hoare_pre) apply (wp set_cap_obj_at_other get_cap_wp|simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (obj_at P p s) \<and> p \<noteq> fst src \<and> p \<noteq> fst dest\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>_ s. P' (obj_at P p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P' (obj_at P p s) \<and> p \<noteq> fst src \<and> p \<noteq> fst dest\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src)\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_ s. P' (obj_at P p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- do t <- gets cdt;
s <- get;
put (s\<lparr>cdt := t(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else t src)\<rparr>)
od;
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>_ s. P' (obj_at P p s)\<rbrace>
 2. \<And>s. P' (obj_at P p s) \<and> p \<noteq> fst src \<and> p \<noteq> fst dest \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma only_idle_tcb_update:
  "\<lbrakk>only_idle s; ko_at (TCB t) p s; tcb_state t = tcb_state t' \<or> \<not>idle (tcb_state t') \<rbrakk>
    \<Longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)" by (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>only_idle s; ko_at (TCB t) p s; tcb_state t = tcb_state t' \<or> tcb_state t' \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)
theory ArchCSpaceInv_AI

lemma safe_ioport_insert_triv:
  "\<not>is_arch_cap newcap \<Longrightarrow> safe_ioport_insert newcap oldcap s" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_cap newcap \<Longrightarrow> safe_ioport_insert newcap oldcap s
theory ArchCSpaceInv_AI

lemma set_cap_ioports':
 "\<lbrace>\<lambda>s. valid_ioports s
      \<and> cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) ptr s\<rbrace>
    set_cap cap ptr
  \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_ioports s \<and> cte_wp_at (\<lambda>cap'. safe_ioport_insert cap cap' s) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. valid_ioports\<rbrace>
theory ArchCSpaceInv_AI

lemma unique_table_refs_no_cap_asidE:
  "\<lbrakk>caps_of_state s p = Some cap;
    unique_table_refs (caps_of_state s)\<rbrakk>
   \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s" apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                        cte_wp_at_caps_of_state) apply (unfold unique_table_refs_def) apply (drule_tac x=p in spec, drule_tac x="(a,b)" in spec) apply (drule spec)+ apply (erule impE, assumption)+ apply (clarsimp simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; unique_table_refs (caps_of_state s); (a, b) \<notin> S; obj_refs capa = obj_refs cap; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; \<forall>p p' cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap; (a, b) \<notin> S; obj_refs capa = obj_refs cap; caps_of_state s (a, b) = Some capa\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; (a, b) \<notin> S; obj_refs capa = obj_refs cap; caps_of_state s (a, b) = Some capa; \<forall>cap cap'. caps_of_state s p = Some cap \<longrightarrow> caps_of_state s (a, b) = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; (a, b) \<notin> S; obj_refs capa = obj_refs cap; caps_of_state s (a, b) = Some capa; caps_of_state s p = Some (?cap17 a b capa) \<longrightarrow> caps_of_state s (a, b) = Some (?cap'19 a b capa) \<longrightarrow> obj_refs (?cap'19 a b capa) = obj_refs (?cap17 a b capa) \<longrightarrow> table_cap_ref (?cap'19 a b capa) = table_cap_ref (?cap17 a b capa)\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>caps_of_state s p = Some cap; (a, b) \<notin> S; obj_refs capa = obj_refs cap; caps_of_state s (a, b) = Some capa; table_cap_ref capa = table_cap_ref cap\<rbrakk> \<Longrightarrow> table_cap_ref capa = table_cap_ref cap proof (prove)
goal:
No subgoals!
theory ArchCSpaceInv_AI

lemma is_simple_cap_arch:
  "\<not>is_arch_cap cap \<Longrightarrow> is_simple_cap_arch cap" by (simp add: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_cap cap \<Longrightarrow> is_simple_cap_arch cap
theory ArchCSpaceInv_AI

lemma is_derived_arch_non_arch:
  "\<not>is_arch_cap cap \<Longrightarrow> \<not> is_arch_cap cap' \<Longrightarrow>
      is_derived_arch cap cap'" unfolding is_derived_arch_def is_pg_cap_def is_pt_cap_def is_pd_cap_def
            vs_cap_ref_def is_arch_cap_def by (auto split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_arch_cap cap; \<not> is_arch_cap cap'\<rbrakk> \<Longrightarrow> is_derived_arch cap cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (case cap of ArchObjectCap x \<Rightarrow> True | _ \<Rightarrow> False); \<not> (case cap' of ArchObjectCap x \<Rightarrow> True | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> ((\<exists>p asid. cap = ArchObjectCap (PageTableCap p asid)) \<or> (\<exists>p asid. cap = ArchObjectCap (PageDirectoryCap p asid)) \<longrightarrow> cap_asid cap = cap_asid cap' \<and> cap_asid cap \<noteq> None) \<and> (arch_cap_fun_lift vs_cap_ref_arch None cap = arch_cap_fun_lift vs_cap_ref_arch None cap' \<or> (\<exists>dev p R sz m. cap' = ArchObjectCap (PageCap dev p R sz m)))
theory ArchCSpaceInv_AI

lemma same_master_cap_same_types:
  "cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>
    (is_pt_cap cap = is_pt_cap cap') \<and> (is_pd_cap cap = is_pd_cap cap')" by (clarsimp simp: cap_master_cap_def is_cap_simps
                  split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap cap = cap_master_cap cap' \<Longrightarrow> is_pt_cap cap = is_pt_cap cap' \<and> is_pd_cap cap = is_pd_cap cap'
theory ArchCSpaceInv_AI

lemma is_derived_cap_arch_asid_issues:
  "is_derived_arch cap cap' \<Longrightarrow>
    cap_master_cap cap = cap_master_cap cap'
      \<Longrightarrow> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap \<noteq> None)
             \<and> (is_pg_cap cap \<or> (vs_cap_ref cap = vs_cap_ref cap'))" apply (simp add: is_derived_arch_def) by (auto simp: cap_master_cap_def is_cap_simps
                  cap_asid_def
                  split: cap.splits arch_cap.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_derived_arch cap cap'; cap_master_cap cap = cap_master_cap cap'\<rbrakk> \<Longrightarrow> (is_pt_cap cap \<or> is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(is_pt_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap = cap_asid cap' \<and> (\<exists>y. cap_asid cap = Some y)) \<and> (vs_cap_ref cap = vs_cap_ref cap' \<or> is_pg_cap cap'); cap_master_cap cap = cap_master_cap cap'\<rbrakk> \<Longrightarrow> (is_pt_cap cap \<longrightarrow> (\<exists>y. cap_asid cap' = Some y)) \<and> (is_pd_cap cap \<longrightarrow> (\<exists>y. cap_asid cap' = Some y)) \<and> (is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref cap')
theory ArchCSpaceInv_AI

lemma safe_parent_for_arch_not_arch:
  "\<not>is_arch_cap cap \<Longrightarrow> \<not>safe_parent_for_arch cap p" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_cap cap \<Longrightarrow> \<not> safe_parent_for_arch cap p
theory ArchCSpaceInv_AI

lemma safe_parent_cap_range_arch:
  "safe_parent_for_arch cap pcap \<Longrightarrow> cap_range cap \<subseteq> cap_range pcap" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for_arch cap pcap \<Longrightarrow> cap_range cap \<subseteq> cap_range pcap
theory CSpacePre_AI

lemma fun_upd_Some:
  "ms p = Some k \<Longrightarrow> (ms(a \<mapsto> b)) p = Some (if a = p then b else k)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ms p = Some k \<Longrightarrow> (ms(a \<mapsto> b)) p = Some (if a = p then b else k)
theory CSpacePre_AI

lemma fun_upd_Some_rev:
  "\<lbrakk>ms a = Some k; (ms(a \<mapsto> b)) p = Some cap\<rbrakk>
   \<Longrightarrow> ms p = Some (if a = p then k else cap)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms a = Some k; (ms(a \<mapsto> b)) p = Some cap\<rbrakk> \<Longrightarrow> ms p = Some (if a = p then k else cap)
theory CSpacePre_AI

lemma P_bool_lift':
  "\<lbrakk>\<lbrace>Q and Q'\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>(\<lambda>s. \<not> Q s) and Q'\<rbrace> f \<lbrace>\<lambda>r s. \<not> Q s\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. P (Q s) \<and> Q' s\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>" apply (clarsimp simp:valid_def) apply (elim allE) apply (case_tac "Q s") apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q and Q'\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>; \<lbrace>(\<lambda>s. \<not> Q s) and Q'\<rbrace> f \<lbrace>\<lambda>r s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (Q s) \<and> Q' s\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. Q s \<and> Q' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, x) \<Rightarrow> Q x); \<forall>s. \<not> Q s \<and> Q' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<not> Q s'); (a, b) \<in> fst (f s); P (Q s); Q' s\<rbrakk> \<Longrightarrow> P (Q b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (Q s); Q' s; Q (?s10 s a b) \<and> Q' (?s10 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s10 s a b)). case x of (r, x) \<Rightarrow> Q x); \<not> Q (?s11 s a b) \<and> Q' (?s11 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s11 s a b)). case x of (r, s') \<Rightarrow> \<not> Q s')\<rbrakk> \<Longrightarrow> P (Q b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (Q s); Q' s; Q (?s10 s a b) \<and> Q' (?s10 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s10 s a b)). case x of (r, x) \<Rightarrow> Q x); \<not> Q (?s11 s a b) \<and> Q' (?s11 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s11 s a b)). case x of (r, s') \<Rightarrow> \<not> Q s'); Q s\<rbrakk> \<Longrightarrow> P (Q b)
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (Q s); Q' s; Q (?s10 s a b) \<and> Q' (?s10 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s10 s a b)). case x of (r, x) \<Rightarrow> Q x); \<not> Q (?s11 s a b) \<and> Q' (?s11 s a b) \<longrightarrow> (\<forall>x\<in>fst (f (?s11 s a b)). case x of (r, s') \<Rightarrow> \<not> Q s'); \<not> Q s\<rbrakk> \<Longrightarrow> P (Q b) proof (prove)
goal:
No subgoals!
theory CSpacePre_AI

lemma free_index_update_simps[simp]:
  "free_index_update g (cap.UntypedCap dev ref sz f) = cap.UntypedCap dev ref sz (g f)" by (simp add:free_index_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. free_index_update g (UntypedCap dev ref sz f) = UntypedCap dev ref sz (g f)
theory CSpacePre_AI

lemma is_cap_free_index_update[simp]:
  "is_zombie (src_cap\<lparr>free_index := f \<rparr>) = is_zombie src_cap"
  "is_cnode_cap (src_cap\<lparr>free_index := f \<rparr>) = is_cnode_cap src_cap"
  "is_thread_cap (src_cap\<lparr>free_index := f \<rparr>) = is_thread_cap src_cap"
  "is_domain_cap (src_cap\<lparr>free_index := f \<rparr>) = is_domain_cap src_cap"
  "is_ep_cap (src_cap\<lparr>free_index := f \<rparr>) = is_ep_cap src_cap"
  "is_untyped_cap (src_cap\<lparr>free_index := f \<rparr>) = is_untyped_cap src_cap"
  "is_arch_cap (src_cap\<lparr>free_index := f \<rparr>) = is_arch_cap src_cap"
  "is_zombie (src_cap\<lparr>free_index := f \<rparr>) = is_zombie src_cap"
  "is_ntfn_cap (src_cap\<lparr>free_index := f \<rparr>) = is_ntfn_cap src_cap"
  "is_reply_cap (src_cap\<lparr>free_index := f \<rparr>) = is_reply_cap src_cap"
  "is_master_reply_cap (src_cap\<lparr>free_index := f \<rparr>) = is_master_reply_cap src_cap" by (simp add:is_cap_simps free_index_update_def split:cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_zombie (free_index_update (\<lambda>_. f) src_cap) = is_zombie src_cap &&& is_cnode_cap (free_index_update (\<lambda>_. f) src_cap) = is_cnode_cap src_cap) &&& is_thread_cap (free_index_update (\<lambda>_. f) src_cap) = is_thread_cap src_cap &&& is_domain_cap (free_index_update (\<lambda>_. f) src_cap) = is_domain_cap src_cap &&& is_ep_cap (free_index_update (\<lambda>_. f) src_cap) = is_ep_cap src_cap) &&& (is_untyped_cap (free_index_update (\<lambda>_. f) src_cap) = is_untyped_cap src_cap &&& is_arch_cap (free_index_update (\<lambda>_. f) src_cap) = is_arch_cap src_cap &&& is_zombie (free_index_update (\<lambda>_. f) src_cap) = is_zombie src_cap) &&& is_ntfn_cap (free_index_update (\<lambda>_. f) src_cap) = is_ntfn_cap src_cap &&& is_reply_cap (free_index_update (\<lambda>_. f) src_cap) = is_reply_cap src_cap &&& is_master_reply_cap (free_index_update (\<lambda>_. f) src_cap) = is_master_reply_cap src_cap