kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

lemma valid_global_refs_update [iff]:
  "valid_global_refs (f s) = valid_global_refs s" by (simp add: valid_global_refs_def arch idle)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs (f s) = valid_global_refs s
theory Invariants_AI

lemma valid_asid_map_update [iff]:
  "valid_asid_map (f s) = valid_asid_map s" by (simp add: valid_asid_map_def vspace_at_asid_def arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map (f s) = valid_asid_map s
theory Invariants_AI

lemma valid_arch_state_update [iff]:
  "valid_arch_state (f s) = valid_arch_state s" by (simp add: valid_arch_state_def arch pspace split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state (f s) = valid_arch_state s
theory Invariants_AI

lemma valid_idle_update [iff]:
  "valid_idle (f s) = valid_idle s" by (auto intro: valid_idle_pspaceI simp: pspace idle)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle (f s) = valid_idle s
theory Invariants_AI

lemma valid_kernel_mappings_update [iff]:
  "valid_kernel_mappings (f s) = valid_kernel_mappings s" by (simp add: valid_kernel_mappings_def
                pspace arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings (f s) = valid_kernel_mappings s
theory Invariants_AI

lemma only_idle_update [iff]:
  "only_idle (f s) = only_idle s" by (simp add: only_idle_def idle)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_idle (f s) = only_idle s
theory Invariants_AI

lemma valid_irq_node_update[iff]:
  "valid_irq_node (f s) = valid_irq_node s" by (simp add: valid_irq_node_def irq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node (f s) = valid_irq_node s
theory Invariants_AI

lemma (in irq_states_update_eq) irq_issued_update [iff]:
  "irq_issued irq (f s) = irq_issued irq s" by (simp add: irq_issued_def int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_issued irq (f s) = irq_issued irq s
theory Invariants_AI

lemma (in pspace_int_update_eq) valid_irq_handlers_update [iff]:
  "valid_irq_handlers (f s) = valid_irq_handlers s" by (simp add: valid_irq_handlers_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers (f s) = valid_irq_handlers s
theory Invariants_AI

lemma obj_ref_in_untyped_range:
  "\<lbrakk> is_untyped_cap c; cap_aligned c \<rbrakk> \<Longrightarrow> obj_ref_of c \<in> untyped_range c" apply (clarsimp simp: is_cap_simps cap_aligned_def) apply (erule is_aligned_no_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap c; cap_aligned c\<rbrakk> \<Longrightarrow> obj_ref_of c \<in> untyped_range c proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f. \<lbrakk>c = UntypedCap dev r bits f; is_aligned r bits; bits < word_bits\<rbrakk> \<Longrightarrow> r \<le> r + 2 ^ bits - 1 proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma untyped_range_non_empty:
  "\<lbrakk> is_untyped_cap c; cap_aligned c \<rbrakk> \<Longrightarrow> untyped_range c \<noteq> {}" by (blast dest: obj_ref_in_untyped_range)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap c; cap_aligned c\<rbrakk> \<Longrightarrow> untyped_range c \<noteq> {}
theory Invariants_AI

lemma valid_mdb_cur [iff]:
  "valid_mdb (cur_thread_update f s) = valid_mdb s" by (auto elim!: valid_mdb_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb (cur_thread_update f s) = valid_mdb s
theory Invariants_AI

lemma valid_mdb_machine [iff]:
  "valid_mdb (machine_state_update f s) = valid_mdb s" by (auto elim: valid_mdb_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb (machine_state_update f s) = valid_mdb s
theory Invariants_AI

lemma valid_refs_cte:
  assumes "\<And>P p. cte_wp_at P p s = cte_wp_at P p s'"
  shows "valid_refs R s = valid_refs R s'" by (simp add: valid_refs_def assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_refs R s = valid_refs R s'
theory Invariants_AI

lemma valid_refs_cte_lift:
  assumes ctes: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. valid_refs R s\<rbrace> f \<lbrace>\<lambda>_ s. valid_refs R s\<rbrace>" apply (simp add: valid_refs_def2) apply (rule ctes) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_refs R\<rbrace> f \<lbrace>\<lambda>_. valid_refs R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>c\<in>ran (caps_of_state s). R \<inter> cap_range c = {}\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>c\<in>ran (caps_of_state s). R \<inter> cap_range c = {}\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma valid_global_refs_cte:
  assumes "\<And>P p. cte_wp_at P p s = cte_wp_at P p s'"
  assumes "global_refs s = global_refs s'"
  shows "valid_global_refs s = valid_global_refs s'" apply (simp add: valid_global_refs_def) by (simp add: valid_global_refs_def assms valid_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs s = valid_global_refs s' proof (prove)
goal (1 subgoal):
 1. valid_refs (global_refs s) s = valid_refs (global_refs s') s'
theory Invariants_AI

lemma valid_global_refs_cte_lift:
  assumes ctes: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
  assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>"
  assumes idle: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>"
  assumes irq: "\<And>P. \<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> f \<lbrace>\<lambda>_ s. P (interrupt_irq_node s)\<rbrace>"
  shows "\<lbrace>valid_global_refs\<rbrace> f \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" unfolding valid_global_refs_def valid_refs_def2 apply (rule hoare_lift_Pf [where f="caps_of_state", OF _ ctes]) apply (rule global_refs_lift[OF arch idle irq]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> f \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>c\<in>ran (caps_of_state s). global_refs s \<inter> cap_range c = {}\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>c\<in>ran (caps_of_state s). global_refs s \<inter> cap_range c = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>c\<in>ran x. global_refs s \<inter> cap_range c = {}\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>c\<in>ran x. global_refs a \<inter> cap_range c = {}\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma has_reply_cap_cte_lift:
  assumes ctes: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> f \<lbrace>\<lambda>_ s. P (has_reply_cap t s)\<rbrace>" unfolding has_reply_cap_def by (simp add: cte_wp_at_caps_of_state, rule ctes)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> f \<lbrace>\<lambda>_ s. P (has_reply_cap t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (\<exists>p. cte_wp_at (is_reply_cap_to t) p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (\<exists>p. cte_wp_at (is_reply_cap_to t) p s)\<rbrace>
theory Invariants_AI

lemma valid_reply_masters_cte:
  assumes "\<And>P p. cte_wp_at P p s = cte_wp_at P p s'"
  shows "valid_reply_masters s = valid_reply_masters s'" by (simp add: valid_reply_masters_def assms tcb_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_masters s = valid_reply_masters s'
theory Invariants_AI

lemma pred_tcb_at_disj:
  "(pred_tcb_at proj P t s \<or> pred_tcb_at proj Q t s) = pred_tcb_at proj (\<lambda>a. P a \<or> Q a) t s" by (fastforce simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pred_tcb_at proj P t s \<or> pred_tcb_at proj Q t s) = pred_tcb_at proj (\<lambda>a. P a \<or> Q a) t s
theory Invariants_AI

lemma dom_empty_cnode: "dom (empty_cnode us) = {x. length x = us}" unfolding empty_cnode_def by (simp add: dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (empty_cnode us) = {x. length x = us} proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if length x = us then Some NullCap else None) = {x. length x = us}
theory Invariants_AI

lemma obj_at_default_cap_valid:
  "\<lbrakk>obj_at (\<lambda>ko. ko = default_object ty dev us) x s;
   ty = CapTableObject \<Longrightarrow> 0 < us;
   ty \<noteq> Untyped; ty \<noteq> ArchObject ASIDPoolObj;
   cap_aligned (default_cap ty x us dev)\<rbrakk>
  \<Longrightarrow> s \<turnstile> default_cap ty x us dev" unfolding valid_cap_def by (clarsimp elim!: obj_at_weakenE
      intro!: aobj_at_default_arch_cap_valid
      simp: default_object_def dom_empty_cnode well_formed_cnode_n_def
            is_tcb is_ep is_ntfn is_cap_table
            a_type_def obj_at_def
     split: apiobject_type.splits
            option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>ko. ko = default_object ty dev us) x s; ty = CapTableObject \<Longrightarrow> 0 < us; ty \<noteq> Untyped; ty \<noteq> ArchObject ASIDPoolObj; cap_aligned (default_cap ty x us dev)\<rbrakk> \<Longrightarrow> s \<turnstile> default_cap ty x us dev proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>ko. ko = default_object ty dev us) x s; ty = CapTableObject \<Longrightarrow> 0 < us; ty \<noteq> Untyped; ty \<noteq> ArchObject ASIDPoolObj; cap_aligned (default_cap ty x us dev)\<rbrakk> \<Longrightarrow> cap_aligned (default_cap ty x us dev) \<and> (case default_cap ty x us dev of UntypedCap deva p b f \<Rightarrow> valid_untyped (default_cap ty x us dev) s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True)
theory Invariants_AI

lemma obj_ref_default [simp]:
  "obj_ref_of (default_cap ty x us dev) = x" by (cases ty, auto simp: aobj_ref_default)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_ref_of (default_cap ty x us dev) = x
theory Invariants_AI

lemma valid_pspace_distinct [elim!]:
  "valid_pspace s \<Longrightarrow> pspace_distinct s" by (simp add: valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace s \<Longrightarrow> pspace_distinct s
theory Invariants_AI

lemma ctable_vtable_neq [simp]:
  "get_tcb_ctable_ptr ptr \<noteq> get_tcb_vtable_ptr ptr" unfolding get_tcb_ctable_ptr_def get_tcb_vtable_ptr_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb_ctable_ptr ptr \<noteq> get_tcb_vtable_ptr ptr proof (prove)
goal (1 subgoal):
 1. (ptr, tcb_cnode_index 0) \<noteq> (ptr, tcb_cnode_index 1)
theory Invariants_AI

lemma tcb_at_typ_at:
  "(\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>tcb_at c\<rbrace> f \<lbrace>\<lambda>rv. tcb_at c\<rbrace>" by (simp add: tcb_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>tcb_at c\<rbrace> f \<lbrace>\<lambda>rv. tcb_at c\<rbrace>
theory Invariants_AI

lemma cap_table_at_typ_at:
  "(\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>cap_table_at n c\<rbrace> f \<lbrace>\<lambda>rv. cap_table_at n c\<rbrace>" by (simp add: cap_table_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>T p. \<lbrace>typ_at T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at T p\<rbrace>) \<Longrightarrow> \<lbrace>cap_table_at n c\<rbrace> f \<lbrace>\<lambda>rv. cap_table_at n c\<rbrace>
theory Invariants_AI

lemma valid_idle_lift:
  assumes "\<And>P t. \<lbrace>idle_tcb_at P t\<rbrace> f \<lbrace>\<lambda>_. idle_tcb_at P t\<rbrace>"
  assumes "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>"
  shows "\<lbrace>valid_idle\<rbrace> f \<lbrace>\<lambda>_. valid_idle\<rbrace>" apply (simp add: valid_idle_def) apply (rule hoare_lift_Pf [where f="idle_thread"]) apply (rule hoare_vcg_conj_lift | rule assms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle\<rbrace> f \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr\<rbrace> f \<lbrace>\<lambda>_ s. idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) (idle_thread s) s \<and> idle_thread s = idle_thread_ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. idle_tcb_at (\<lambda>a. case a of (st, ab) \<Rightarrow> idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) x s \<and> x = idle_thread_ptr\<rbrace> f \<lbrace>\<lambda>_ a. idle_tcb_at (\<lambda>a. case a of (st, ab) \<Rightarrow> idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) x a \<and> x = idle_thread_ptr\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma obj_ref_is_tcb:
  "\<lbrakk> r \<in> obj_refs cap; tcb_at r s; s \<turnstile> cap \<rbrakk> \<Longrightarrow>
  is_thread_cap cap \<or> is_zombie cap" by (auto simp: valid_cap_def is_cap_simps obj_at_def is_obj_defs a_type_def
          split: cap.splits
           dest: obj_ref_is_arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> obj_refs cap; tcb_at r s; s \<turnstile> cap\<rbrakk> \<Longrightarrow> is_thread_cap cap \<or> is_zombie cap
theory Invariants_AI

lemma ut_revocableD:
  "\<lbrakk> cs p = Some cap; is_untyped_cap cap; ut_revocable r cs \<rbrakk> \<Longrightarrow> r p" by (auto simp: ut_revocable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some cap; is_untyped_cap cap; ut_revocable r cs\<rbrakk> \<Longrightarrow> r p
theory Invariants_AI

lemma untyped_range_is_untyped_cap [elim!]:
  "untyped_range cap \<noteq> {} \<Longrightarrow> is_untyped_cap cap" by (cases cap) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_range cap \<noteq> {} \<Longrightarrow> is_untyped_cap cap
theory Invariants_AI

lemma not_is_untyped_no_range [elim!]:
  "\<not>is_untyped_cap cap \<Longrightarrow> untyped_range cap = {}" by (cases cap) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_untyped_cap cap \<Longrightarrow> untyped_range cap = {}
theory Invariants_AI

lemma untyped_mdbD:
  "\<lbrakk> cs ptr = Some cap; is_untyped_cap cap; cs ptr' = Some cap';
     obj_refs cap' \<inter> untyped_range cap \<noteq> {}; untyped_mdb m cs \<rbrakk>
  \<Longrightarrow> ptr' \<in> descendants_of ptr m" unfolding untyped_mdb_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs ptr = Some cap; is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; untyped_mdb m cs\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs ptr = Some cap; is_untyped_cap cap; cs ptr' = Some cap'; obj_refs cap' \<inter> untyped_range cap \<noteq> {}; \<forall>ptr ptr' cap cap'. cs ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> cs ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> ptr' \<in> descendants_of ptr m
theory Invariants_AI

lemma cte_wp_at_norm:
  "cte_wp_at P p s \<Longrightarrow> \<exists>c. cte_wp_at ((=) c) p s \<and> P c" by (auto simp add: cte_wp_at_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at P p s \<Longrightarrow> \<exists>c. cte_wp_at ((=) c) p s \<and> P c
theory Invariants_AI

lemma valid_mdb_arch_state [simp]:
  "valid_mdb (arch_state_update f s) = valid_mdb s" by (auto elim!: valid_mdb_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb (arch_state_update f s) = valid_mdb s
theory Invariants_AI

lemma valid_idle_arch_state [simp]:
  "valid_idle (arch_state_update f s) = valid_idle s" by (simp add: valid_idle_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle (arch_state_update f s) = valid_idle s
theory Invariants_AI

lemma if_unsafe_then_cap_arch_state [simp]:
  "if_unsafe_then_cap (arch_state_update f s) = if_unsafe_then_cap s" by (simp add: if_unsafe_then_cap_def ex_cte_cap_wp_to_def)

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

lemma swp_cte_at_arch_update [iff]:
  "swp cte_at (s\<lparr>arch_state := a\<rparr>) = swp cte_at s" by (simp add: cte_wp_at_cases swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp (cte_wp_at (\<lambda>_. True)) (s\<lparr>arch_state := a\<rparr>) = swp (cte_wp_at (\<lambda>_. True)) s
theory Invariants_AI

lemma swp_caps_of_state_arch_update [iff]:
  "caps_of_state (s\<lparr>arch_state := a\<rparr>) = caps_of_state s" apply (rule cte_wp_caps_of_lift) apply (simp add: cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state (s\<lparr>arch_state := a\<rparr>) = caps_of_state s proof (prove)
goal (1 subgoal):
 1. \<And>p P. cte_wp_at P p (s\<lparr>arch_state := a\<rparr>) = cte_wp_at P p s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma is_master_reply_cap_NullCap:
  "is_master_reply_cap NullCap = False" by (simp add: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_master_reply_cap NullCap = False
theory Invariants_AI

lemma valid_reply_mastersD:
  "\<lbrakk> cte_wp_at (is_master_reply_cap_to t) p s; valid_reply_masters s \<rbrakk>
   \<Longrightarrow> p = (t, tcb_cnode_index 2)" by (simp add: valid_reply_masters_def del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (is_master_reply_cap_to t) p s; valid_reply_masters s\<rbrakk> \<Longrightarrow> p = (t, tcb_cnode_index 2)
theory Invariants_AI

lemma valid_reply_mastersD':
  "\<lbrakk> cte_wp_at ((=) (ReplyCap t True R)) p s; valid_reply_masters s \<rbrakk>
   \<Longrightarrow> p = (t, tcb_cnode_index 2)" by (fastforce simp add: valid_reply_masters_def is_master_reply_cap_to_def
                simp del: split_paired_All
                elim: cte_wp_at_lift
                elim!: impE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (ReplyCap t True R)) p s; valid_reply_masters s\<rbrakk> \<Longrightarrow> p = (t, tcb_cnode_index 2)
theory Invariants_AI

lemma valid_cap_aligned:
  "s \<turnstile> cap \<Longrightarrow> cap_aligned cap" by (simp add: valid_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> cap_aligned cap
theory Invariants_AI

lemma valid_pspace_vo [elim!]:
  "valid_pspace s \<Longrightarrow> valid_objs s" by (simp add: valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace s \<Longrightarrow> valid_objs s
theory Invariants_AI

lemma real_cte_at_typ_valid:
  "\<lbrace>typ_at (ACapTable (length (snd p))) (fst p)\<rbrace>
     f
   \<lbrace>\<lambda>rv. typ_at (ACapTable (length (snd p))) (fst p)\<rbrace>
   \<Longrightarrow> \<lbrace>real_cte_at p\<rbrace> f \<lbrace>\<lambda>rv. real_cte_at p\<rbrace>" by (simp add: cap_table_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at (ACapTable (length (snd p))) (fst p)\<rbrace> f \<lbrace>\<lambda>rv. typ_at (ACapTable (length (snd p))) (fst p)\<rbrace> \<Longrightarrow> \<lbrace>real_cte_at p\<rbrace> f \<lbrace>\<lambda>rv. real_cte_at p\<rbrace>
theory Invariants_AI

lemma dmo_aligned[wp]:
  "do_machine_op f \<lbrace>pspace_aligned\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do_machine_op f \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do ms <- gets machine_state;
p <- select_f (f ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cte_wp_at_eqD2:
  "\<lbrakk>cte_wp_at ((=) c) p s; cte_wp_at P p s \<rbrakk> \<Longrightarrow> P c" by (auto elim!: cte_wp_atE split: if_split_asm)

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

lemma only_idle_arch [iff]:
  "only_idle (arch_state_update f s) = only_idle s" by (simp add: only_idle_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_idle (arch_state_update f s) = only_idle s
theory Invariants_AI

lemma (in pspace_update_eq) state_refs_update:
  "state_refs_of (f s) = state_refs_of s" by (simp add: state_refs_of_def pspace cong: option.case_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of (f s) = state_refs_of s
theory Invariants_AI

lemma zombies_final_arch_update [iff]:
  "zombies_final (arch_state_update f s) = zombies_final s" by (simp add: zombies_final_def is_final_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final (arch_state_update f s) = zombies_final s
theory Invariants_AI

lemma zombies_final_more_update [iff]:
  "zombies_final (trans_state f s) = zombies_final s" by (simp add: zombies_final_def is_final_cap'_def)

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

lemma valid_ioc_arch_state_update[iff]:
  "valid_ioc (arch_state_update f s) = valid_ioc s" by (simp add: valid_ioc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc (arch_state_update f s) = valid_ioc s
theory Invariants_AI

lemma valid_ioc_more_update[iff]:
  "valid_ioc (trans_state f s) = valid_ioc s" by (simp add: valid_ioc_def)

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

lemma valid_ioc_interrupt_states_update[iff]:
  "valid_ioc (interrupt_states_update f s) = valid_ioc s" by (simp add: valid_ioc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc (interrupt_states_update f s) = valid_ioc s
theory Invariants_AI

lemma valid_ioc_machine_state_update[iff]:
  "valid_ioc (machine_state_update f s) = valid_ioc s" by (simp add: valid_ioc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc (machine_state_update f s) = valid_ioc s