kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_H

lemma valid_dlist_prevD:
  "\<lbrakk> valid_dlist m; c \<noteq> 0; c' \<noteq> 0 \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'" by (fastforce simp add: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; c \<noteq> 0; c' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'
theory Invariants_H

lemma no_0_simps [simp]:
  assumes "no_0 m"
  shows "((m 0 = Some cte) = False) \<and> ((Some cte = m 0) = False)" using assms by (simp add: no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m (0::'a) = Some cte) = False \<and> (Some cte = m (0::'a)) = False proof (prove)
using this:
no_0 m

goal (1 subgoal):
 1. (m (0::'a) = Some cte) = False \<and> (Some cte = m (0::'a)) = False
theory Invariants_H

lemma vdlist_prevD:
  "\<lbrakk> m \<turnstile> c \<leftarrow> c'; m c = Some cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'" by (fastforce simp: valid_dlist_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leftarrow> c'; m c = Some cte; valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'
theory Invariants_H

lemma vdlist_nextD:
  "\<lbrakk> m \<turnstile> c \<leadsto> c'; m c' = Some cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'" by (fastforce simp: valid_dlist_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; m c' = Some cte; valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'
theory Invariants_H

lemma vdlist_prevD0:
  "\<lbrakk> m \<turnstile> c \<leftarrow> c'; c \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'" by (fastforce simp: valid_dlist_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leftarrow> c'; c \<noteq> 0; valid_dlist m\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'
theory Invariants_H

lemma vdlist_nextD0:
  "\<lbrakk> m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'" by (fastforce simp: valid_dlist_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; valid_dlist m\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'
theory Invariants_H

lemma vdlist_prev_src_unique:
  "\<lbrakk> m \<turnstile> p \<leftarrow> x; m \<turnstile> p \<leftarrow> y; p \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> x = y" by (drule (2) vdlist_prevD0)+ (clarsimp simp: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> p \<leftarrow> x; m \<turnstile> p \<leftarrow> y; p \<noteq> 0; valid_dlist m\<rbrakk> \<Longrightarrow> x = y
theory Invariants_H

lemma vdlist_next_src_unique:
  "\<lbrakk> m \<turnstile> x \<leadsto> p; m \<turnstile> y \<leadsto> p; p \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> x = y" by (drule (2) vdlist_nextD0)+ (clarsimp simp: mdb_prev_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> x \<leadsto> p; m \<turnstile> y \<leadsto> p; p \<noteq> 0; valid_dlist m\<rbrakk> \<Longrightarrow> x = y
theory Invariants_H

lemma cte_at_cte_wp_atD:
  "cte_at' p s \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) p s" by (clarsimp simp add: cte_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) p s
theory Invariants_H

lemma valid_pspace_no_0 [elim]:
  "valid_pspace' s \<Longrightarrow> no_0 (ctes_of s)" by (auto simp: valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace' s \<Longrightarrow> no_0 (ctes_of s)
theory Invariants_H

lemma valid_pspace_dlist [elim]:
  "valid_pspace' s \<Longrightarrow> valid_dlist (ctes_of s)" by (auto simp: valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace' s \<Longrightarrow> valid_dlist (ctes_of s)
theory Invariants_H

lemma next_rtrancl_tranclE [consumes 1, case_names eq trancl]:
  assumes major: "m \<turnstile> x \<leadsto>\<^sup>* y"
  and     r1: "x = y \<Longrightarrow> P"
  and     r2: "\<lbrakk> x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y \<rbrakk> \<Longrightarrow> P"
  shows  "P" using major by (auto dest: rtranclD intro: r1 r2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>* y

goal (1 subgoal):
 1. P
theory Invariants_H

lemma next_single_value:
  "\<lbrakk> m \<turnstile> x \<leadsto> y; m \<turnstile> x \<leadsto> z \<rbrakk> \<Longrightarrow> y = z" unfolding mdb_next_rel_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> x \<leadsto> y; m \<turnstile> x \<leadsto> z\<rbrakk> \<Longrightarrow> y = z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> {(x, y). mdb_next m x = Some y}; (x, z) \<in> {(x, y). mdb_next m x = Some y}\<rbrakk> \<Longrightarrow> y = z
theory Invariants_H

lemma no_0_lhs:
  "\<lbrakk> m \<turnstile> c \<leadsto> y; no_0 m \<rbrakk> \<Longrightarrow> c \<noteq> 0" unfolding no_0_def by (erule contrapos_pn, simp add: mdb_next_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> y; no_0 m\<rbrakk> \<Longrightarrow> c \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> c \<leadsto> y; m 0 = None\<rbrakk> \<Longrightarrow> c \<noteq> 0
theory Invariants_H

lemma mdb_chain_0_no_loops:
  assumes asm: "mdb_chain_0 m"
  and     no0: "no_0 m"
  shows   "no_loops m" proof - { fix c assume mc: "m \<turnstile> c \<leadsto>\<^sup>+ c" with asm have "m \<turnstile> c \<leadsto>\<^sup>+ 0" unfolding mdb_chain_0_def apply - apply (erule bspec, erule tranclE2) apply (auto intro: domI simp: mdb_next_unfold) done with mc have  "m \<turnstile> 0 \<leadsto>\<^sup>+ c" by (rule loop_split) hence False using no0 by (clarsimp dest!:  no_0_lhs_trancl) } thus "no_loops m" unfolding no_loops_def by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_loops m proof (state)
goal (1 subgoal):
 1. no_loops m proof (state)
goal (1 subgoal):
 1. no_loops m proof (state)
goal (1 subgoal):
 1. no_loops m proof (state)
this:
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. no_loops m proof (chain)
picking this:
mdb_chain_0 m
m \<turnstile> c \<leadsto>\<^sup>+ c proof (prove)
using this:
mdb_chain_0 m
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
using this:
\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0
m \<turnstile> c \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0; m \<turnstile> c \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
goal (2 subgoals):
 1. m \<turnstile> c \<leadsto> c \<Longrightarrow> c \<in> dom m
 2. \<And>ca. \<lbrakk>m \<turnstile> c \<leadsto> ca; m \<turnstile> ca \<leadsto>\<^sup>+ c\<rbrakk> \<Longrightarrow> c \<in> dom m proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> c \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. no_loops m proof (chain)
picking this:
m \<turnstile> c \<leadsto>\<^sup>+ c
m \<turnstile> c \<leadsto>\<^sup>+ 0 proof (prove)
using this:
m \<turnstile> c \<leadsto>\<^sup>+ c
m \<turnstile> c \<leadsto>\<^sup>+ 0

goal (1 subgoal):
 1. m \<turnstile> 0 \<leadsto>\<^sup>+ c proof (state)
this:
m \<turnstile> 0 \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. no_loops m proof (prove)
using this:
m \<turnstile> 0 \<leadsto>\<^sup>+ c

goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> 0 \<leadsto>\<^sup>+ c
no_0 m

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. no_loops m proof (state)
this:
m \<turnstile> ?c2 \<leadsto>\<^sup>+ ?c2 \<Longrightarrow> False

goal (1 subgoal):
 1. no_loops m proof (prove)
using this:
m \<turnstile> ?c2 \<leadsto>\<^sup>+ ?c2 \<Longrightarrow> False

goal (1 subgoal):
 1. no_loops m proof (prove)
using this:
m \<turnstile> ?c2 \<leadsto>\<^sup>+ ?c2 \<Longrightarrow> False

goal (1 subgoal):
 1. \<forall>c. (c, c) \<notin> (mdb_next_rel m)\<^sup>+ proof (state)
this:
no_loops m

goal:
No subgoals!
theory Invariants_H

lemma valid_mdb_ctesE [elim]:
  "\<lbrakk>valid_mdb_ctes m;
    \<lbrakk> valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m;
      caps_contained' m; mdb_chunked m; untyped_mdb' m;
      untyped_inc' m; valid_nullcaps m; ut_revocable' m;
      class_links m; distinct_zombies m; irq_control m;
      reply_masters_rvk_fb m \<rbrakk>
          \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" unfolding valid_mdb_ctes_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m \<and> no_0 m \<and> mdb_chain_0 m \<and> valid_badges m \<and> caps_contained' m \<and> mdb_chunked m \<and> untyped_mdb' m \<and> untyped_inc' m \<and> valid_nullcaps m \<and> ut_revocable' m \<and> class_links m \<and> distinct_zombies m \<and> irq_control m \<and> reply_masters_rvk_fb m; \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Invariants_H

lemma valid_mdb_ctesI [intro]:
  "\<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m;
    caps_contained' m; mdb_chunked m; untyped_mdb' m;
    untyped_inc' m; valid_nullcaps m; ut_revocable' m;
    class_links m; distinct_zombies m; irq_control m;
    reply_masters_rvk_fb m \<rbrakk>
  \<Longrightarrow> valid_mdb_ctes m" unfolding valid_mdb_ctes_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m\<rbrakk> \<Longrightarrow> valid_mdb_ctes m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m\<rbrakk> \<Longrightarrow> valid_dlist m \<and> no_0 m \<and> mdb_chain_0 m \<and> valid_badges m \<and> caps_contained' m \<and> mdb_chunked m \<and> untyped_mdb' m \<and> untyped_inc' m \<and> valid_nullcaps m \<and> ut_revocable' m \<and> class_links m \<and> distinct_zombies m \<and> irq_control m \<and> reply_masters_rvk_fb m
theory Invariants_H

lemma state_refs_of'_eq[iff]:
  "state_refs_of' (f s) = state_refs_of' s" by (rule state_refs_of'_pspaceI [OF _ pspace], rule refl)

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

lemma valid_space_update [iff]:
  "valid_pspace' (f s) = valid_pspace' s" by (fastforce simp: valid_pspace' pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace' (f s) = valid_pspace' s
theory Invariants_H

lemma obj_at_update [iff]:
  "obj_at' P p (f s) = obj_at' P p s" by (fastforce intro: obj_at'_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p (f s) = obj_at' P p s
theory Invariants_H

lemma ko_wp_at_update [iff]:
  "ko_wp_at' P p (f s) = ko_wp_at' P p s" by (simp add: pspace ko_wp_at'_def ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p (f s) = ko_wp_at' P p s
theory Invariants_H

lemma cte_wp_at_update [iff]:
  "cte_wp_at' P p (f s) = cte_wp_at' P p s" by (fastforce intro: cte_wp_at'_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' P p (f s) = cte_wp_at' P p s
theory Invariants_H

lemma ex_nonz_cap_to_eq'[iff]:
  "ex_nonz_cap_to' p (f s) = ex_nonz_cap_to' p s" by (simp add: ex_nonz_cap_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to' p (f s) = ex_nonz_cap_to' p s
theory Invariants_H

lemma iflive_update [iff]:
  "if_live_then_nonz_cap' (f s) = if_live_then_nonz_cap' s" by (simp add: if_live_then_nonz_cap'_def ex_nonz_cap_to'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. if_live_then_nonz_cap' (f s) = if_live_then_nonz_cap' s
theory Invariants_H

lemma valid_objs_update [iff]:
  "valid_objs' (f s) = valid_objs' s" apply (simp add: valid_objs'_def pspace) apply (fastforce intro: valid_obj'_pspaceI simp: pspace) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_objs' (f s) = valid_objs' s proof (prove)
goal (1 subgoal):
 1. (\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj (f s)) = (\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma pspace_aligned_update [iff]:
  "pspace_aligned' (f s) = pspace_aligned' s" by (simp add: pspace pspace_aligned'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned' (f s) = pspace_aligned' s
theory Invariants_H

lemma pspace_distinct_update [iff]:
  "pspace_distinct' (f s) = pspace_distinct' s" by (simp add: pspace pspace_distinct'_def ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct' (f s) = pspace_distinct' s
theory Invariants_H

lemma pred_tcb_at_update [iff]:
  "pred_tcb_at' proj P p (f s) = pred_tcb_at' proj P p s" by (simp add: pred_tcb_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at' proj P p (f s) = pred_tcb_at' proj P p s
theory Invariants_H

lemma valid_cap_update [iff]:
  "(f s) \<turnstile>' c = s \<turnstile>' c" by (auto intro: valid_cap'_pspaceI simp: pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' c (f s) = valid_cap' c s
theory Invariants_H

lemma typ_at_update' [iff]:
  "typ_at' T p (f s) = typ_at' T p s" by (simp add: typ_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at' T p (f s) = typ_at' T p s
theory Invariants_H

lemma valid_asid_table_update' [iff]:
  "valid_asid_table' t (f s) = valid_asid_table' t s" by (simp add: valid_asid_table'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_table' t (f s) = valid_asid_table' t s
theory Invariants_H

lemma page_table_at_update' [iff]:
  "page_table_at' p (f s) = page_table_at' p s" by (simp add: page_table_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_table_at' p (f s) = page_table_at' p s
theory Invariants_H

lemma page_directory_at_update' [iff]:
  "page_directory_at' p (f s) = page_directory_at' p s" by (simp add: page_directory_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_directory_at' p (f s) = page_directory_at' p s
theory Invariants_H

lemma valid_global_pts_update' [iff]:
  "valid_global_pts' pts (f s) = valid_global_pts' pts s" by (simp add: valid_global_pts'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_pts' pts (f s) = valid_global_pts' pts s
theory Invariants_H

lemma no_0_obj'_update [iff]:
  "no_0_obj' (f s) = no_0_obj' s" by (simp add: no_0_obj'_def pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0_obj' (f s) = no_0_obj' s
theory Invariants_H

lemma valid_pde_mappings'_update [iff]:
  "valid_pde_mappings' (f s) = valid_pde_mappings' s" by (simp add: valid_pde_mappings'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde_mappings' (f s) = valid_pde_mappings' s
theory Invariants_H

lemma pointerInUserData_update[iff]:
  "pointerInUserData p (f s) = pointerInUserData p s" by (simp add: pointerInUserData_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pointerInUserData p (f s) = pointerInUserData p s
theory Invariants_H

lemma pointerInDeviceData_update[iff]:
  "pointerInDeviceData p (f s) = pointerInDeviceData p s" by (simp add: pointerInDeviceData_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pointerInDeviceData p (f s) = pointerInDeviceData p s
theory Invariants_H

lemma pspace_domain_valid_update [iff]:
  "pspace_domain_valid (f s) = pspace_domain_valid s" by (simp add: pspace_domain_valid_def pspace)

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

lemma global_refs_update' [iff]:
  "global_refs' (f s) = global_refs' s" by (simp add: global_refs'_def arch idle int_nd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global_refs' (f s) = global_refs' s
theory Invariants_H

lemma valid_global_refs_update' [iff]:
  "valid_global_refs' (f s) = valid_global_refs' s" by (simp add: valid_global_refs'_def pspace arch idle maxObj)

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

lemma valid_arch_state_update' [iff]:
  "valid_arch_state' (f s) = valid_arch_state' s" by (simp add: valid_arch_state'_def arch)

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

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

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

lemma ifunsafe_update [iff]:
  "if_unsafe_then_cap' (f s) = if_unsafe_then_cap' s" by (simp add: if_unsafe_then_cap'_def ex_cte_cap_to'_def int_nd)

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

lemma irqs_masked_update [iff]:
  "irqs_masked' (f s) = irqs_masked' s" by (simp add: irqs_masked'_def int)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irqs_masked' (f s) = irqs_masked' s
theory Invariants_H

lemma valid_irq_handlers_update'[iff]:
  "valid_irq_handlers' (f s) = valid_irq_handlers' s" by (simp add: valid_irq_handlers'_def cteCaps_of_def pspace)

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

lemma ko_wp_at_aligned:
  "ko_wp_at' ((=) ko) p s \<Longrightarrow> is_aligned p (objBitsKO ko)" by (simp add: ko_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' ((=) ko) p s \<Longrightarrow> is_aligned p (objBitsKO ko)
theory Invariants_H

lemma ko_wp_at_norm:
  "ko_wp_at' P p s \<Longrightarrow> \<exists>ko. P ko \<and> ko_wp_at' ((=) ko) p s" by (auto simp add: ko_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p s \<Longrightarrow> \<exists>ko. P ko \<and> ko_wp_at' ((=) ko) p s
theory Invariants_H

lemma valid_mdb_machine_state [iff]:
  "valid_mdb' (ksMachineState_update f s) = valid_mdb' s" by (simp add: valid_mdb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb' (ksMachineState_update f s) = valid_mdb' s
theory Invariants_H

lemma cte_wp_at_norm':
  "cte_wp_at' P p s \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) p s \<and> P cte" by (simp add: cte_wp_at'_def)

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

lemma pred_tcb_at' [elim!]:
  "pred_tcb_at' proj P t s \<Longrightarrow> tcb_at' t s" by (auto 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 \<Longrightarrow> tcb_at' t s
theory Invariants_H

lemma valid_pspace_mdb' [elim!]:
  "valid_pspace' s \<Longrightarrow> valid_mdb' s" by (simp add: valid_pspace'_def)

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

lemma page_table_pte_atI':
  "\<lbrakk> page_table_at' p s; x < 2^(ptBits - 2) \<rbrakk> \<Longrightarrow> pte_at' (p + (x << 2)) s" by (simp add: page_table_at'_def pageBits_def ptBits_def pteBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>page_table_at' p s; x < 2 ^ (ptBits - 2)\<rbrakk> \<Longrightarrow> pte_at' (p + (x << 2)) s
theory Invariants_H

lemma no_0_prev:
  "no_0 m \<Longrightarrow> \<not> m \<turnstile> p \<leftarrow> 0" by (simp add: mdb_prev_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 m \<Longrightarrow> \<not> m \<turnstile> p \<leftarrow> 0
theory Invariants_H

lemma nullcapsD':
  "\<lbrakk>m p = Some (CTE NullCap n); valid_nullcaps m \<rbrakk> \<Longrightarrow> n = nullMDBNode" unfolding valid_nullcaps_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.NullCap n); valid_nullcaps m\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.NullCap n); \<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode\<rbrakk> \<Longrightarrow> n = nullMDBNode
theory Invariants_H

lemma class_linksD:
  "\<lbrakk> m p = Some cte; m p' = Some cte'; m \<turnstile> p \<leadsto> p'; class_links m \<rbrakk> \<Longrightarrow>
  capClass (cteCap cte) = capClass (cteCap cte')" using class_links_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; m p' = Some cte'; m \<turnstile> p \<leadsto> p'; class_links m\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
using this:
class_links ?m \<equiv> \<forall>p p' cte cte'. ?m p = Some cte \<longrightarrow> ?m p' = Some cte' \<longrightarrow> ?m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')

goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; m p' = Some cte'; m \<turnstile> p \<leadsto> p'; class_links m\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')
theory Invariants_H

lemma irq_controlD:
  "\<lbrakk> m p = Some (CTE IRQControlCap n); m p' = Some (CTE IRQControlCap n');
    irq_control m \<rbrakk> \<Longrightarrow> p' = p" unfolding irq_control_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); m p' = Some (CTE capability.IRQControlCap n'); irq_control m\<rbrakk> \<Longrightarrow> p' = p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); m p' = Some (CTE capability.IRQControlCap n'); \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p' n'. m p' = Some (CTE capability.IRQControlCap n') \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> p' = p
theory Invariants_H

lemma irq_revocable:
  "\<lbrakk> m p = Some (CTE IRQControlCap n); irq_control m \<rbrakk> \<Longrightarrow> mdbRevocable n" unfolding irq_control_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); irq_control m\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE capability.IRQControlCap n); \<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p' n'. m p' = Some (CTE capability.IRQControlCap n') \<longrightarrow> p' = p)\<rbrakk> \<Longrightarrow> mdbRevocable n