kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_AI

lemma reply_mdb : "\<And>m. reply_mdb m (caps_of_state s)
                  \<Longrightarrow> reply_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)" by (simp add: reply_mdb_def reply_caps_mdb reply_masters_mdb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m. reply_mdb m (caps_of_state s) \<Longrightarrow> reply_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)
theory Detype_AI

lemma valid_ioports_detype[detype_invs_lemmas]:
  "valid_ioports (detype (untyped_range cap) s)" apply (insert invs, drule invs_valid_ioports) by (clarsimp simp: valid_ioports_detype)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioports (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_ioports s \<Longrightarrow> valid_ioports (detype (untyped_range cap) s)
theory Detype_AI

lemma untype_children_detype[detype_invs_lemmas]: "untyped_children_in_mdb (detype (untyped_range cap) s)" apply (insert child) apply (simp add: untyped_children_in_mdb_def) apply (erule allEI)+ apply (clarsimp simp: detype_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_children_in_mdb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. untyped_children_in_mdb s \<Longrightarrow> untyped_children_in_mdb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>a b aa ba. (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) (aa, ba) s) \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<Longrightarrow> \<forall>a b aa ba. (\<exists>capa. cte_wp_at ((=) capa) (a, b) s \<and> a \<notin> untyped_range cap \<and> is_untyped_cap capa \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range capa \<noteq> {}) (aa, ba) s \<and> aa \<notin> untyped_range cap) \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. (\<exists>cap. cte_wp_at ((=) cap) (a, b) s \<and> is_untyped_cap cap \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range cap \<noteq> {}) (aa, ba) s) \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) \<Longrightarrow> (\<exists>capa. cte_wp_at ((=) capa) (a, b) s \<and> a \<notin> untyped_range cap \<and> is_untyped_cap capa \<and> cte_wp_at (\<lambda>cap'. obj_refs cap' \<inter> untyped_range capa \<noteq> {}) (aa, ba) s \<and> aa \<notin> untyped_range cap) \<longrightarrow> (aa, ba) \<in> descendants_of (a, b) (cdt s) proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma irq_node_detype[simp]: (* duplicated lemma *)
  "\<And>r. interrupt_irq_node (detype r s) = interrupt_irq_node s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>r. interrupt_irq_node (detype r s) = interrupt_irq_node s
theory Detype_AI

lemma zombies_final: "zombies_final s" using invs by (simp add: invs_def valid_state_def valid_pspace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. zombies_final s
theory Detype_AI

lemma valid_refs_detype[detype_invs_lemmas]: "valid_global_refs (detype (untyped_range cap) s)" using globals by (simp add: valid_global_refs_def valid_refs_def glob_det)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs (detype (untyped_range cap) s) proof (prove)
using this:
valid_global_refs s

goal (1 subgoal):
 1. valid_global_refs (detype (untyped_range cap) s)
theory Detype_AI

lemma valid_irq_detype[detype_invs_lemmas]: "valid_irq_node (detype (untyped_range cap) s)" using invs valid_globals_irq_node [OF globals cap] by (simp add: valid_irq_node_def invs_def valid_state_def cap_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_node (detype (untyped_range cap) s) proof (prove)
using this:
invs s
interrupt_irq_node s ?irq \<notin> cap_range cap

goal (1 subgoal):
 1. valid_irq_node (detype (untyped_range cap) s)
theory Detype_AI

lemma valid_reply_masters_detype[detype_invs_lemmas]:
  "valid_reply_masters (detype (untyped_range cap) s)" using vmaster by (clarsimp simp: valid_reply_masters_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_reply_masters (detype (untyped_range cap) s) proof (prove)
using this:
valid_reply_masters s

goal (1 subgoal):
 1. valid_reply_masters (detype (untyped_range cap) s)
theory Detype_AI

lemma valid_irq_handlers_detype[detype_invs_lemmas]:
  "valid_irq_handlers (detype (untyped_range cap) s)" using invs apply (simp add: valid_irq_handlers_def ran_def irq_issued_def
                   invs_def valid_state_def) apply (force simp: detype_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_handlers (detype (untyped_range cap) s) proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_irq_handlers (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_pspace s \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> (\<forall>cap. (\<exists>a b. caps_of_state s (a, b) = Some cap) \<longrightarrow> (\<forall>irq\<in>cap_irqs cap. interrupt_states s irq = IRQSignal)) \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<Longrightarrow> \<forall>capa. (\<exists>a. a \<notin> untyped_range cap \<and> (a \<notin> untyped_range cap \<longrightarrow> (\<exists>b. caps_of_state s (a, b) = Some capa))) \<longrightarrow> (\<forall>irq\<in>cap_irqs capa. interrupt_states (detype (untyped_range cap) s) irq = IRQSignal) proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma only_idle_detype[detype_invs_lemmas]: "only_idle (detype (untyped_range cap) s)" proof - have "only_idle s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (clarsimp simp: only_idle_def) apply (simp add: detype_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_idle (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. only_idle (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. only_idle s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. only_idle s proof (state)
this:
only_idle s

goal (1 subgoal):
 1. only_idle (detype (untyped_range cap) s) proof (prove)
using this:
only_idle s

goal (1 subgoal):
 1. only_idle (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>\<forall>t. st_tcb_at idle t s \<longrightarrow> t = idle_thread s; st_tcb_at idle t s; t \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> t = idle_thread (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals! proof (state)
this:
only_idle (detype (untyped_range cap) s)

goal:
No subgoals!
theory Detype_AI

lemma cap_refs_in_kernel_detype[detype_invs_lemmas]:
  "cap_refs_in_kernel_window (detype (untyped_range cap) s)" proof - have "cap_refs_in_kernel_window s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (simp add: cap_refs_in_kernel_window_def
                     valid_refs_def arch_state_det) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_in_kernel_window (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. cap_refs_in_kernel_window (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. cap_refs_in_kernel_window s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. cap_refs_in_kernel_window s proof (state)
this:
cap_refs_in_kernel_window s

goal (1 subgoal):
 1. cap_refs_in_kernel_window (detype (untyped_range cap) s) proof (prove)
using this:
cap_refs_in_kernel_window s

goal (1 subgoal):
 1. cap_refs_in_kernel_window (detype (untyped_range cap) s) proof (prove)
goal:
No subgoals! proof (state)
this:
cap_refs_in_kernel_window (detype (untyped_range cap) s)

goal:
No subgoals!
theory Detype_AI

lemma valid_ioc_detype[detype_invs_lemmas]: "valid_ioc (detype (untyped_range cap) s)" proof - have "valid_ioc s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply (simp add: valid_ioc_def) apply (clarsimp simp: detype_def neq_commute) apply (drule spec, drule spec, erule impE, assumption) apply (frule_tac p="(a,b)" in non_null_present[simplified neq_commute]) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ioc (detype (untyped_range cap) s) proof (state)
goal (1 subgoal):
 1. valid_ioc (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. valid_ioc s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_ioc s proof (state)
this:
valid_ioc s

goal (1 subgoal):
 1. valid_ioc (detype (untyped_range cap) s) proof (prove)
using this:
valid_ioc s

goal (1 subgoal):
 1. valid_ioc (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s \<Longrightarrow> \<forall>a b. is_original_cap (detype (untyped_range cap) s) (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s \<and> a \<notin> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; is_original_cap s (a, b); a \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_original_cap s (a, b); a \<in> untyped_range cap; cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_original_cap s (a, b); a \<in> untyped_range cap; cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; fst (a, b) \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
valid_ioc (detype (untyped_range cap) s)

goal:
No subgoals!
theory Detype_AI

lemma valid_irq_states_detype[detype_invs_lemmas]: "valid_irq_states
          (clear_um (untyped_range cap) (detype (untyped_range cap) s))" proof - have "valid_irq_states s" using invs by (simp add: invs_def valid_state_def) thus ?thesis apply(clarsimp simp: clear_um_def detype_def valid_irq_states_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_irq_states (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (state)
goal (1 subgoal):
 1. valid_irq_states (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal (1 subgoal):
 1. valid_irq_states s proof (prove)
using this:
invs s

goal (1 subgoal):
 1. valid_irq_states s proof (state)
this:
valid_irq_states s

goal (1 subgoal):
 1. valid_irq_states (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
using this:
valid_irq_states s

goal (1 subgoal):
 1. valid_irq_states (clear_um (untyped_range cap) (detype (untyped_range cap) s)) proof (prove)
goal:
No subgoals! proof (state)
this:
valid_irq_states (clear_um (untyped_range cap) (detype (untyped_range cap) s))

goal:
No subgoals!
theory Detype_AI

lemma invariants:
  assumes ct_act: "ct_active s"
  shows "(invs and untyped_children_in_mdb)
         (detype (untyped_range cap) (clear_um (untyped_range cap) s))" using detype_invs_lemmas detype_invs_assms ct_act by (simp add: invs_def valid_state_def valid_pspace_def
                detype_clear_um_independent clear_um.state_refs_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (invs and untyped_children_in_mdb) (detype (untyped_range cap) (clear_um (untyped_range cap) s)) proof (prove)
using this:
valid_objs (detype (untyped_range cap) s)
pspace_aligned (detype (untyped_range cap) s)
sym_refs (state_refs_of (detype (untyped_range cap) s))
sym_refs (state_hyp_refs_of (detype (untyped_range cap) s))
pspace_distinct (detype (untyped_range cap) s)
ct_active s \<Longrightarrow> cur_tcb (detype (untyped_range cap) s)
valid_mdb (detype (untyped_range cap) s)
valid_ioports (detype (untyped_range cap) s)
untyped_children_in_mdb (detype (untyped_range cap) s)
if_live_then_nonz_cap (detype (untyped_range cap) s)
if_unsafe_then_cap (detype (untyped_range cap) s)
zombies_final (detype (untyped_range cap) s)
valid_global_refs (detype (untyped_range cap) s)
valid_reply_caps (detype (untyped_range cap) s)
valid_irq_node (detype (untyped_range cap) s)
valid_reply_masters (detype (untyped_range cap) s)
valid_irq_handlers (detype (untyped_range cap) s)
only_idle (detype (untyped_range cap) s)
cap_refs_in_kernel_window (detype (untyped_range cap) s)
valid_ioc (detype (untyped_range cap) s)
valid_irq_states (clear_um (untyped_range cap) (detype (untyped_range cap) s))
valid_idle (detype (untyped_range cap) s)
valid_arch_state (detype (untyped_range cap) s)
valid_vspace_objs (detype (untyped_range cap) s)
valid_arch_caps (detype (untyped_range cap) s)
valid_kernel_mappings (detype (untyped_range cap) s)
valid_global_objs (detype (untyped_range cap) s)
valid_asid_map (detype (untyped_range cap) s)
valid_global_vspace_mappings (detype (untyped_range cap) s)
equal_kernel_mappings (detype (untyped_range cap) s)
pspace_in_kernel_window (detype (untyped_range cap) s)
valid_machine_state (clear_um (untyped_range cap) (detype (untyped_range cap) s))
pspace_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))
cap_refs_respects_device_region (clear_um (untyped_range cap) (detype (untyped_range cap) s))
ct_active s

goal (1 subgoal):
 1. (invs and untyped_children_in_mdb) (detype (untyped_range cap) (clear_um (untyped_range cap) s))
theory Detype_AI

lemma gets_modify_comm2:
  "\<forall>s. g (f s) = g s \<Longrightarrow>
   (do x \<leftarrow> modify f; y \<leftarrow> gets g; m x y od) =
   (do y \<leftarrow> gets g; x \<leftarrow> modify f; m x y od)" apply (rule ext) apply (drule spec) by (rule gets_modify_comm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. g (f s) = g s \<Longrightarrow> do x <- modify f;
gets g >>= m x
od = do y <- gets g;
x <- modify f;
m x y
od proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>s. g (f s) = g s \<Longrightarrow> (do x <- modify f;
gets g >>= m x
od) x = (do y <- gets g;
x <- modify f;
m x y
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. g (f (?s2 x)) = g (?s2 x) \<Longrightarrow> (do x <- modify f;
gets g >>= m x
od) x = (do y <- gets g;
x <- modify f;
m x y
od) x
theory Detype_AI

lemma dmo_detype_comm:
  assumes "empty_fail f"
  shows "do_machine_op f >>= (\<lambda>s. modify (detype S)) =
         modify (detype S) >>= (\<lambda>s. do_machine_op f)" proof - have machine_state_detype: "\<forall>s. machine_state (detype S s) = machine_state s" by (simp add: detype_def) have detype_msu_independent:
    "\<And>f. detype S \<circ> machine_state_update f = machine_state_update f \<circ> detype S" by (simp add: detype_def ext) from assms show ?thesis apply (simp add: do_machine_op_def split_def bind_assoc) apply (simp add: gets_modify_comm2[OF machine_state_detype]) apply (rule arg_cong_bind1) apply (simp add: empty_fail_def select_f_walk[OF empty_fail_modify]
                     modify_modify detype_msu_independent) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do s <- do_machine_op f;
modify (detype S)
od = do s <- modify (detype S);
do_machine_op f
od proof (state)
goal (1 subgoal):
 1. do s <- do_machine_op f;
modify (detype S)
od = do s <- modify (detype S);
do_machine_op f
od proof (prove)
goal (1 subgoal):
 1. \<forall>s. machine_state (detype S s) = machine_state s proof (state)
this:
\<forall>s. machine_state (detype S s) = machine_state s

goal (1 subgoal):
 1. do s <- do_machine_op f;
modify (detype S)
od = do s <- modify (detype S);
do_machine_op f
od proof (prove)
goal (1 subgoal):
 1. \<And>f. detype S \<circ> machine_state_update f = machine_state_update f \<circ> detype S proof (state)
this:
detype S \<circ> machine_state_update ?f1 = machine_state_update ?f1 \<circ> detype S

goal (1 subgoal):
 1. do s <- do_machine_op f;
modify (detype S)
od = do s <- modify (detype S);
do_machine_op f
od proof (chain)
picking this:
empty_fail f proof (prove)
using this:
empty_fail f

goal (1 subgoal):
 1. do s <- do_machine_op f;
modify (detype S)
od = do s <- modify (detype S);
do_machine_op f
od proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> do x <- gets machine_state;
x <- select_f (f x);
s <- modify (machine_state_update (\<lambda>_. snd x));
modify (detype S)
od = do s <- modify (detype S);
ms <- gets machine_state;
p <- select_f (f ms);
modify (machine_state_update (\<lambda>_. snd p))
od proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> do x <- gets machine_state;
x <- select_f (f x);
s <- modify (machine_state_update (\<lambda>_. snd x));
modify (detype S)
od = do ms <- gets machine_state;
s <- modify (detype S);
p <- select_f (f ms);
modify (machine_state_update (\<lambda>_. snd p))
od proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail f \<Longrightarrow> do x <- select_f (f x);
s <- modify (machine_state_update (\<lambda>_. snd x));
modify (detype S)
od = do s <- modify (detype S);
p <- select_f (f x);
modify (machine_state_update (\<lambda>_. snd p))
od proof (prove)
goal:
No subgoals! proof (state)
this:
do s <- do_machine_op f;
modify (detype S)
od = do s <- modify (detype S);
do_machine_op f
od

goal:
No subgoals!
theory Detype_AI

lemma (in Detype_AI) delete_objects_def2:
  "delete_objects ptr bits \<equiv>
   do modify (detype {ptr..ptr + 2 ^ bits - 1});
      do_machine_op (freeMemory ptr bits)
   od" by (rule eq_reflection)
     (simp add: delete_objects_def dmo_detype_comm[OF empty_fail_freeMemory])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. delete_objects ptr bits \<equiv> do modify (detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od
theory Detype_AI

lemma modify_modify_bind:
  "(modify f >>= (\<lambda>_. (modify g >>= h))) =
   (modify (g \<circ> f) >>= h)" by (simp add: modify_modify bind_assoc[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- modify f;
modify g >>= h
od = modify (g \<circ> f) >>= h
theory Detype_AI

lemma dmo_untyped_children_in_mdb[wp]:
  "\<lbrace>\<lambda>s. untyped_children_in_mdb s\<rbrace>
   do_machine_op f
   \<lbrace>\<lambda>rv s. untyped_children_in_mdb s\<rbrace>" by (wp | simp add: untyped_mdb_alt[symmetric] do_machine_op_def split_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_children_in_mdb\<rbrace> do_machine_op f \<lbrace>\<lambda>rv. untyped_children_in_mdb\<rbrace>
theory Detype_AI

lemma detype_machine_state_update_comm:
  "detype S (machine_state_update f s) =
   machine_state_update f (detype S s)" by (case_tac s, simp add: detype_def ext)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. detype S (machine_state_update f s) = machine_state_update f (detype S s)
theory Detype_AI

lemma interrupt_irq_node_detype[simp]:
  "interrupt_irq_node (detype S s) = interrupt_irq_node s" by (simp add: detype_def)

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

lemma cte_wp_at_delete_objects[wp]:
  "\<lbrace>\<lambda>s. Q (cte_wp_at (P (interrupt_irq_node s)) p s) \<and>
        fst p \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrace>
   delete_objects ptr bits
   \<lbrace>\<lambda>_ s. Q (cte_wp_at (P (interrupt_irq_node s)) p s)\<rbrace>" apply (simp add: delete_objects_def do_machine_op_def split_def) apply wp apply (simp add: detype_machine_state_update_comm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cte_wp_at (P (interrupt_irq_node s)) p s) \<and> fst p \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>_ s. Q (cte_wp_at (P (interrupt_irq_node s)) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (cte_wp_at (P (interrupt_irq_node s)) p s) \<and> (ptr \<le> fst p \<longrightarrow> \<not> fst p \<le> ptr + 2 ^ bits - 1)\<rbrace> do y <- do ms <- gets machine_state;
p <- select_f (freeMemory ptr bits ms);
modify (machine_state_update (\<lambda>_. snd p))
od;
modify (detype {ptr..ptr + 2 ^ bits - 1})
od \<lbrace>\<lambda>_ s. Q (cte_wp_at (P (interrupt_irq_node s)) p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Q (cte_wp_at (P (interrupt_irq_node s)) p s) \<and> (ptr \<le> fst p \<longrightarrow> \<not> fst p \<le> ptr + 2 ^ bits - 1) \<Longrightarrow> \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). Q (cte_wp_at (P (interrupt_irq_node (detype {ptr..ptr + 2 ^ bits - 1} (s\<lparr>machine_state := snd x\<rparr>)))) p (detype {ptr..ptr + 2 ^ bits - 1} (s\<lparr>machine_state := snd x\<rparr>))) proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma of_nat_le_pow:
  "\<lbrakk>x < 2 ^ n; n \<le> len_of TYPE('a)\<rbrakk> \<Longrightarrow> of_nat x \<le> (mask n :: 'a :: len word)" apply (drule_tac a="2::nat" in power_increasing, simp) apply (frule less_le_trans, assumption) apply (frule of_nat_mono_maybe_le[OF unat_lt2p[of "mask n:: 'a :: len word"],
                                    folded word_bits_def]) apply simp apply (simp add: unat_mask min_def) apply (erule iffD1) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; n \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; 2 ^ n \<le> 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; 2 ^ n \<le> 2 ^ LENGTH('a); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; 2 ^ n \<le> 2 ^ LENGTH('a); x < 2 ^ LENGTH('a); (x \<le> unat (mask n)) = (word_of_nat x \<le> word_of_nat (unat (mask n)))\<rbrakk> \<Longrightarrow> word_of_nat x \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; n \<le> LENGTH('a); x < 2 ^ LENGTH('a); (x \<le> unat (mask n)) = (word_of_nat x \<le> mask n)\<rbrakk> \<Longrightarrow> word_of_nat x \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; n \<le> LENGTH('a); x < 2 ^ LENGTH('a); (x \<le> 2 ^ n - Suc 0) = (word_of_nat x \<le> mask n)\<rbrakk> \<Longrightarrow> word_of_nat x \<le> mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ n; n \<le> LENGTH('a); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x \<le> 2 ^ n - Suc 0 proof (prove)
goal:
No subgoals!