kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

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

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

lemma vms_ioc_update[iff]:
  "valid_machine_state (is_original_cap_update f s::'z::state_ext state) = valid_machine_state s" by (simp add: valid_machine_state_def)+

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

lemma valid_machine_state_more_update[iff]:
  "valid_machine_state (trans_state f s) = valid_machine_state s" by (simp add: valid_machine_state_def)

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

lemma only_idle_lift_weak:
  assumes "\<And>Q P t. \<lbrace>\<lambda>s. Q (st_tcb_at P t s)\<rbrace> f \<lbrace>\<lambda>_ s. Q (st_tcb_at P t s)\<rbrace>"
  assumes "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>"
  shows "\<lbrace>only_idle\<rbrace> f \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: only_idle_def) apply (rule hoare_vcg_all_lift) apply (rule hoare_lift_Pf [where f="idle_thread"]) apply (rule assms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> f \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>t. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>\<lambda>s. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at idle t s \<longrightarrow> t = idle_thread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t x. \<lbrace>\<lambda>s. st_tcb_at idle t s \<longrightarrow> t = x\<rbrace> f \<lbrace>\<lambda>_ a. st_tcb_at idle t a \<longrightarrow> t = x\<rbrace>
 2. \<And>t 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 cap_rights_update_id [intro!, simp]:
  "wellformed_cap c \<Longrightarrow> cap_rights_update (cap_rights c) c = c" unfolding cap_rights_update_def by (cases c) (auto simp: wellformed_cap_simps split: bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_cap c \<Longrightarrow> cap_rights_update (cap_rights c) c = c proof (prove)
goal (1 subgoal):
 1. wellformed_cap c \<Longrightarrow> (case c of EndpointCap oref badge cr \<Rightarrow> EndpointCap oref badge (cap_rights c) | NotificationCap oref badge cr \<Rightarrow> NotificationCap oref badge (cap_rights c - {AllowGrant, AllowGrantReply}) | ReplyCap t m cr \<Rightarrow> ReplyCap t m (cap_rights c - {AllowRead, AllowGrantReply} \<union> {AllowWrite}) | ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update (cap_rights c) acap) | _ \<Rightarrow> c) = c
theory Invariants_AI

lemma cap_mask_UNIV [simp]:
  "wellformed_cap c \<Longrightarrow> mask_cap UNIV c = c" by (simp add: mask_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wellformed_cap c \<Longrightarrow> mask_cap UNIV c = c
theory Invariants_AI

lemma wf_empty_bits:
  "well_formed_cnode_n bits (empty_cnode bits)" by (simp add: well_formed_cnode_n_def empty_cnode_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n bits (empty_cnode bits)
theory Invariants_AI

lemma well_formed_cnode_valid_cs_size:
  "valid_cs_size bits s \<Longrightarrow> well_formed_cnode_n bits s" by (clarsimp simp: valid_cs_size_def)

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

lemma empty_cnode_bits:
  "obj_bits (CNode n (empty_cnode n)) = cte_level_bits + n" by (simp add: wf_empty_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_bits (CNode n (empty_cnode n)) = cte_level_bits + n
theory Invariants_AI

lemma irq_revocableD:
  "\<lbrakk> cs p = Some IRQControlCap; irq_revocable (is_original_cap s) cs \<rbrakk> \<Longrightarrow> is_original_cap s p" by (fastforce simp add: irq_revocable_def simp del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some IRQControlCap; irq_revocable (is_original_cap s) cs\<rbrakk> \<Longrightarrow> is_original_cap s p
theory Invariants_AI

lemma invs_valid_stateI [elim!]:
  "invs s \<Longrightarrow> valid_state s" by (simp add: invs_def)

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

lemma tcb_at_invs [elim!]:
  "invs s \<Longrightarrow> tcb_at (cur_thread s) s" by (simp add: invs_def cur_tcb_def)

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

lemma invs_valid_objs [elim!]:
  "invs s \<Longrightarrow> valid_objs s" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma invs_psp_aligned [elim!]:
  "invs s \<Longrightarrow> pspace_aligned s" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma invs_mdb [elim!]:
  "invs s \<Longrightarrow> valid_mdb s" by (simp add: invs_def valid_state_def)

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

lemma invs_mdb_cte [elim!]:
  "invs s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)" by (simp add: invs_def valid_state_def valid_mdb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)
theory Invariants_AI

lemma invs_valid_pspace [elim!]:
  "invs s \<Longrightarrow> valid_pspace s" by (simp add: invs_def valid_state_def)

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

lemma invs_arch_state [elim!]:
  "invs s \<Longrightarrow> valid_arch_state s" by (simp add: invs_def valid_state_def)

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

lemma invs_cur [elim!]:
  "invs s \<Longrightarrow> cur_tcb s" by (simp add: invs_def)

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

lemma invs_distinct [elim!]:
  "invs s \<Longrightarrow> pspace_distinct s" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma invs_iflive [elim!]:
  "invs s \<Longrightarrow> if_live_then_nonz_cap s" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma invs_sym_refs [elim!]:
  "invs s \<Longrightarrow> sym_refs (state_refs_of s)" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma invs_hyp_sym_refs [elim!]: (* ARMHYP move and requalify *)
  "invs s \<Longrightarrow> sym_refs (state_hyp_refs_of s)" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma invs_valid_reply_caps [elim!]:
  "invs s \<Longrightarrow> valid_reply_caps s" by (simp add: invs_def valid_state_def)

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

lemma invs_vobjs_strgs:
  "invs s \<longrightarrow> valid_objs s" by auto

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

lemma invs_valid_global_refs [elim!]:
  "invs s \<Longrightarrow> valid_global_refs s" by (simp add: invs_def valid_state_def)

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

lemma invs_zombies [elim!]:
  "invs s \<Longrightarrow> zombies_final s" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma objs_valid_tcb_ctable:
  "\<lbrakk>valid_objs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable tcb" apply (clarsimp simp: get_tcb_def split: option.splits kernel_object.splits) apply (erule cte_wp_valid_cap[rotated]) apply (rule cte_wp_at_tcbI[where t="(a, b)" for a b, where b3="tcb_cnode_index 0"]) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable tcb proof (prove)
goal (1 subgoal):
 1. kheap s t = Some (TCB tcb) \<Longrightarrow> cte_wp_at ((=) (tcb_ctable tcb)) ?p40 s proof (prove)
goal (3 subgoals):
 1. kheap s t = Some (TCB tcb) \<Longrightarrow> kheap s (fst (?a45, tcb_cnode_index 0)) = Some (TCB ?tcb42)
 2. kheap s t = Some (TCB tcb) \<Longrightarrow> tcb_cap_cases (snd (?a45, tcb_cnode_index 0)) = Some (?getF42, ?setF42)
 3. kheap s t = Some (TCB tcb) \<Longrightarrow> tcb_ctable tcb = ?getF42 ?tcb42 proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma invs_valid_tcb_ctable:
  "\<lbrakk>invs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable tcb" apply (drule invs_valid_stateI) apply (clarsimp simp: valid_state_def valid_pspace_def objs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable tcb proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb t s = Some tcb; valid_state s\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable tcb proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma invs_vspace_objs [elim!]:
  "invs s \<Longrightarrow> valid_vspace_objs s" by (simp add: invs_def valid_state_def)

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

lemma invs_valid_idle[elim!]:
  "invs s \<Longrightarrow> valid_idle s" by (fastforce simp: invs_def valid_state_def)

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

lemma simple_st_tcb_at_state_refs_ofD:
  "st_tcb_at simple t s \<Longrightarrow> bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s" by (fastforce simp: pred_tcb_at_def obj_at_def state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s \<Longrightarrow> bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s
theory Invariants_AI

lemma active_st_tcb_at_state_refs_ofD:
  "st_tcb_at active t s \<Longrightarrow> bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s" by (fastforce simp: pred_tcb_at_def obj_at_def state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at active t s \<Longrightarrow> bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s
theory Invariants_AI

lemma cur_tcb_revokable [iff]:
  "cur_tcb (is_original_cap_update f s) = cur_tcb s" by (simp add: cur_tcb_def)

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

lemma cur_tcb_arch [iff]:
  "cur_tcb (arch_state_update f s) = cur_tcb s" by (simp add: cur_tcb_def)

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

lemma invs_valid_global_objs[elim!]:
  "invs s \<Longrightarrow> valid_global_objs s" by (clarsimp simp: invs_def valid_state_def)

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

lemma get_irq_slot_real_cte:
  "\<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>real_cte_at\<rbrace>" apply (simp add: get_irq_slot_def) apply wp apply (clarsimp simp: invs_def valid_state_def
    valid_irq_node_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>real_cte_at\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>real_cte_at\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> real_cte_at (interrupt_irq_node s irq, []) s proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma all_invs_but_sym_refs_check:
  "(all_invs_but_sym_refs and sym_refs \<circ> state_refs_of and sym_refs o state_hyp_refs_of) = invs" by (simp add: invs_def valid_state_def valid_pspace_def
                o_def pred_conj_def conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and sym_refs \<circ> state_refs_of and sym_refs \<circ> state_hyp_refs_of) = invs
theory Invariants_AI

lemma invs_valid_asid_map[elim!]:
  "invs s \<Longrightarrow> valid_asid_map s" by (simp add: invs_def valid_state_def)

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

lemma invs_valid_ioports[elim!]:
  "invs s \<Longrightarrow> valid_ioports s" by (simp add: invs_def valid_state_def)

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

lemma invs_equal_kernel_mappings[elim!]:
  "invs s \<Longrightarrow> equal_kernel_mappings s" by (simp add:invs_def valid_state_def)

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

lemma invs_valid_irq_node[elim!]:
  "invs s \<Longrightarrow> valid_irq_node s" by (simp add: invs_def valid_state_def)

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

lemma invs_ifunsafe[elim!]:
  "invs s \<Longrightarrow> if_unsafe_then_cap s" by (simp add: invs_def valid_state_def valid_pspace_def)

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

lemma cte_wp_at_cap_aligned:
  "\<lbrakk>cte_wp_at P p s; invs s\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> cap_aligned c" apply (drule (1) cte_wp_at_valid_objs_valid_cap [OF _ invs_valid_objs]) apply (fastforce simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; invs s\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> cap_aligned c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<exists>cap. P cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>c. P c \<and> cap_aligned c proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cte_wp_at_cap_aligned':
  "\<lbrakk>cte_wp_at ((=) cap) p s; invs s\<rbrakk> \<Longrightarrow> cap_aligned cap" apply (drule (1) cte_wp_at_valid_objs_valid_cap [OF _ invs_valid_objs]) apply (fastforce simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) p s; invs s\<rbrakk> \<Longrightarrow> cap_aligned cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<exists>capa. cap = capa \<and> s \<turnstile> capa\<rbrakk> \<Longrightarrow> cap_aligned cap proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma invs_locale_trivial:
  "invs_locale \<top>" by (unfold_locales; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_locale (\<lambda>_. True)
theory Invariants_AI

lemma in_dxo_pspaceD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> kheap s' = kheap s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> kheap s' = kheap s
theory Invariants_AI

lemma in_dxo_revokableD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> is_original_cap s' = is_original_cap s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> is_original_cap s' = is_original_cap s
theory Invariants_AI

lemma in_dxo_cur_threadD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> cur_thread s' = cur_thread s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> cur_thread s' = cur_thread s
theory Invariants_AI

lemma in_dxo_idle_threadD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> idle_thread s' = idle_thread s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> idle_thread s' = idle_thread s
theory Invariants_AI

lemma in_dxo_machine_stateD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> machine_state s' = machine_state s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> machine_state s' = machine_state s
theory Invariants_AI

lemma in_dxo_irq_nodeD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> interrupt_irq_node s' = interrupt_irq_node s
theory Invariants_AI

lemma in_dxo_archD:
  "((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> arch_state s' = arch_state s" by (clarsimp simp: do_extended_op_def select_f_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (do_extended_op f s) \<Longrightarrow> arch_state s' = arch_state s
theory Invariants_AI

lemma max_ipc_length_unfold:
  "max_ipc_length = 128" by (simp add: max_ipc_length_def cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. max_ipc_length = 128
theory Invariants_AI

lemma valid_mask_vm_rights[simp]:
  "mask_vm_rights V R \<in> valid_vm_rights" by (simp add: mask_vm_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask_vm_rights V R \<in> valid_vm_rights
theory Invariants_AI

lemma invs_pspace_in_kernel_window[elim!]:
  "invs s \<Longrightarrow> pspace_in_kernel_window s" by (simp add: invs_def valid_state_def)

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

lemma invs_strengthen:
  "invs s \<Longrightarrow> P s \<longrightarrow> invs s"
  "invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> invs s \<and> Q s"
  "invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> Q s \<and> invs s"
  "invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> (invs and Q) s"
  "invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> (Q and invs) s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((invs s \<Longrightarrow> P s \<longrightarrow> invs s) &&& (invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> invs s \<and> Q s)) &&& (invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> Q s \<and> invs s) &&& (invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> (invs and Q) s) &&& (invs s \<and> (P s \<longrightarrow> Q s) \<Longrightarrow> P s \<longrightarrow> (Q and invs) s)
theory ArchADT_AI

lemma the_arch_cap_simp[simp]: "the_arch_cap (ArchObjectCap x) = x" by (simp add: the_arch_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_arch_cap (ArchObjectCap x) = x
theory ArchADT_AI

lemma get_pd_of_thread_eq:
  "pd_ref \<noteq> arm_global_pd (arch_state s) \<Longrightarrow>
   get_pd_of_thread (kheap s) (arch_state s) tcb_ref = pd_ref \<longleftrightarrow>
   (\<exists>tcb. kheap s tcb_ref = Some (TCB tcb) \<and>
          (\<exists>asid. tcb_vtable tcb =
                  cap.ArchObjectCap (PageDirectoryCap
                                       pd_ref (Some asid)) \<and>
                  (the (vs_cap_ref_arch (the_arch_cap (tcb_vtable tcb))) \<rhd> pd_ref) s))" by (auto simp: get_pd_of_thread_vs_lookup vs_cap_ref_def
          split: option.splits Structures_A.kernel_object.splits
                 cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pd_ref \<noteq> arm_global_pd (arch_state s) \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb_ref = pd_ref) = (\<exists>tcb. kheap s tcb_ref = Some (TCB tcb) \<and> (\<exists>asid. tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd_ref (Some asid)) \<and> (the (vs_cap_ref_arch (the_arch_cap (tcb_vtable tcb))) \<rhd> pd_ref) s))
theory ArchADT_AI

lemma pd_shifting':
 "is_aligned pd pd_bits \<Longrightarrow> (pd + (vptr >> 20 << 2) && ~~ mask pd_bits) = (pd::word32)" unfolding pd_bits_def pageBits_def by (rule pd_shifting_gen; simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. is_aligned pd (12 + 2) \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask (12 + 2) = pd