kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_AI

lemma subset_splitE:
  "\<lbrakk>A \<subseteq> B \<or> B \<subseteq> A \<or> A \<inter> B = {} ; A \<subset> B \<Longrightarrow>P;B \<subset> A \<Longrightarrow>P ;A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P\<rbrakk> \<Longrightarrow>P" apply (simp add:subset_iff_psubset_eq) apply (elim disjE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B \<or> B \<subseteq> A \<or> A \<inter> B = {}; A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subset> B \<or> A = B \<or> B \<subset> A \<or> B = A \<or> A \<inter> B = {}; A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (5 subgoals):
 1. \<lbrakk>A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P; A \<subset> B\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P; A = B\<rbrakk> \<Longrightarrow> P
 3. \<lbrakk>A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P; B \<subset> A\<rbrakk> \<Longrightarrow> P
 4. \<lbrakk>A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P; B = A\<rbrakk> \<Longrightarrow> P
 5. \<lbrakk>A \<subset> B \<Longrightarrow> P; B \<subset> A \<Longrightarrow> P; A = B \<Longrightarrow> P; A \<inter> B = {} \<Longrightarrow> P; A \<inter> B = {}\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma cap_range_untyped_range_eq[simp]:
  "is_untyped_cap a \<Longrightarrow> cap_range a = untyped_range a" by (clarsimp simp:is_cap_simps cap_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap a \<Longrightarrow> cap_range a = untyped_range a
theory Detype_AI

lemma descendants_range_inD:
  "\<lbrakk>descendants_range_in S p s;p'\<in>descendants_of p (cdt s);caps_of_state s p' = Some cap\<rbrakk>
 \<Longrightarrow> cap_range cap \<inter> S = {}" by (auto simp:descendants_range_in_def cte_wp_at_caps_of_state dest!:bspec)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in S p s; p' \<in> descendants_of p (cdt s); caps_of_state s p' = Some cap\<rbrakk> \<Longrightarrow> cap_range cap \<inter> S = {}
theory Detype_AI

lemma descendants_range_def2:
  "descendants_range cap p = descendants_range_in (cap_range cap) p" by (simp add:descendants_range_in_def descendants_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_range cap p = descendants_range_in (cap_range cap) p
theory Detype_AI

lemma detype_clear_um_independent:
  "detype S (clear_um T s) = clear_um T (detype S s)" by (auto simp add: detype_def clear_um_def ext)

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

lemma valid_mdb_clear_um [iff]:
  "valid_mdb (clear_um S s) = valid_mdb s" by (simp add: clear_um_def)

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

lemma valid_ioc_clear_um[iff]:
  "valid_ioc (clear_um S s) = valid_ioc s" by (simp add: clear_um_def)

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

lemma cur_tcb_clear_um[iff]: "cur_tcb (clear_um S s) = cur_tcb s" by (simp add: clear_um_def cur_tcb_def)

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

lemma untyped_children_in_mdb_clear_um[iff]:
  "untyped_children_in_mdb (clear_um S s) = untyped_children_in_mdb s" by (simp add: untyped_children_in_mdb_def clear_um_def)

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

lemma drange:"descendants_range_in (cap_range cap) ptr (s :: 'a state)" using nodesc by (simp add:descendants_range_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_range_in (cap_range cap) ptr s proof (prove)
using this:
descendants_range cap ptr s

goal (1 subgoal):
 1. descendants_range_in (cap_range cap) ptr s
theory Detype_AI

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

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

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

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

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

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

lemma globals: "valid_global_refs s" using invs by (simp add: invs_def valid_state_def)

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

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

lemma state_refs: "state_refs_of (detype (untyped_range cap) s) = state_refs_of s" apply (rule ext, clarsimp simp add: state_refs_of_detype) apply (rule sym, rule equals0I, drule state_refs_of_elemD) apply (drule live_okE, rule refs_of_live, clarsimp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of (detype (untyped_range cap) s) = state_refs_of s proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> untyped_range cap \<Longrightarrow> {} = state_refs_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> untyped_range cap; obj_at (\<lambda>obj. y \<in> refs_of obj) x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> untyped_range cap; x \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma idle: "idle_thread (detype (untyped_range cap) s) = idle_thread s" by (simp add: detype_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. idle_thread (detype (untyped_range cap) s) = idle_thread s
theory Detype_AI

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

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

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

lemma valid_arch_state: "valid_arch_state s" using invs by clarsimp

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

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

lemma ut_mdb: "untyped_mdb (cdt s) (caps_of_state s)" using invs by (clarsimp dest!: invs_mdb simp add: valid_mdb_def)

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

goal (1 subgoal):
 1. untyped_mdb (cdt s) (caps_of_state s)
theory Detype_AI

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

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

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

lemma valid_global_objs: "valid_global_objs s" using invs by (clarsimp simp: invs_def valid_state_def)

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

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

lemma cap_is_valid: "valid_cap cap s" by (rule cte_wp_valid_cap[OF cap invs_valid_objs[OF invs]])

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

lemma irq_node:
  "interrupt_irq_node (s :: 'a state) irq \<notin> untyped_range cap" using valid_globals_irq_node [OF globals cap] by (simp add: cap_range_def)

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

goal (1 subgoal):
 1. interrupt_irq_node s irq \<notin> untyped_range cap
theory Detype_AI

lemma non_filter_detype:
  "null_filter (caps_of_state s) = null_filter (caps_of_state (detype (untyped_range cap) s))" apply (intro iffI ext) apply (clarsimp simp: null_filter_def split:if_splits)+ apply (rule ccontr) apply (clarsimp dest!:caps_of_state_cteD) apply (frule non_null_present[OF cte_wp_at_weakenE]) apply (clarsimp simp:cte_wp_at_caps_of_state) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_filter (caps_of_state s) = null_filter (caps_of_state (detype (untyped_range cap) s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. null_filter (caps_of_state s) x = null_filter (caps_of_state (detype (untyped_range cap) s)) x proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) \<noteq> Some NullCap; a \<in> untyped_range cap\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = None proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) \<noteq> Some NullCap; a \<in> untyped_range cap; caps_of_state s (a, b) \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>caps_of_state s (a, b) \<noteq> Some NullCap; a \<in> untyped_range cap; cte_wp_at ((=) y) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b y c. \<lbrakk>caps_of_state s (a, b) \<noteq> Some NullCap; a \<in> untyped_range cap; cte_wp_at ((=) y) (a, b) s; y = c\<rbrakk> \<Longrightarrow> NullCap \<noteq> c
 2. \<And>a b y. \<lbrakk>caps_of_state s (a, b) \<noteq> Some NullCap; a \<in> untyped_range cap; cte_wp_at ((=) y) (a, b) s; fst (a, b) \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>caps_of_state s (a, b) \<noteq> Some NullCap; a \<in> untyped_range cap; cte_wp_at ((=) y) (a, b) s; fst (a, b) \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma non_null_caps:
    "\<And>p c. \<lbrakk> caps_of_state s p = Some c; c \<noteq> cap.NullCap \<rbrakk>
     \<Longrightarrow> fst p \<notin> untyped_range cap" by (clarsimp simp: cte_wp_at_caps_of_state non_null_present)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p c. \<lbrakk>caps_of_state s p = Some c; c \<noteq> NullCap\<rbrakk> \<Longrightarrow> fst p \<notin> untyped_range cap
theory Detype_AI

lemma vreply: "valid_reply_caps s" using invs by (simp add: invs_def valid_state_def)

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

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

lemma vmaster: "valid_reply_masters s" using invs by (simp add: invs_def valid_state_def)

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

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

lemma refsym : "sym_refs (state_refs_of s)" using invs by (simp add: invs_def valid_state_def valid_pspace_def)

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

goal (1 subgoal):
 1. sym_refs (state_refs_of s)
theory Detype_AI

lemma hyprefsym : "sym_refs (state_hyp_refs_of s)" using invs by (simp add: invs_def valid_state_def valid_pspace_def)

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

goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of s)
theory Detype_AI

lemma refs_of: "\<And>obj p. \<lbrakk> ko_at obj p s \<rbrakk> \<Longrightarrow> refs_of obj \<subseteq> (UNIV - untyped_range cap \<times> UNIV)" by (fastforce intro: refs_of_live dest!: sym_refs_ko_atD[OF _ refsym] live_okE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>obj p. ko_at obj p s \<Longrightarrow> refs_of obj \<subseteq> UNIV - untyped_range cap \<times> UNIV
theory Detype_AI

lemma refs_of2: "\<And>obj p. kheap s p = Some obj
                     \<Longrightarrow> refs_of obj \<subseteq> (UNIV - untyped_range cap \<times> UNIV)" by (simp add: refs_of obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>obj p. kheap s p = Some obj \<Longrightarrow> refs_of obj \<subseteq> UNIV - untyped_range cap \<times> UNIV
theory Detype_AI

lemma valid_objs_detype[detype_invs_lemmas] : "valid_objs (detype (untyped_range cap) s)" using invs_valid_objs[OF invs] apply (clarsimp simp add: valid_objs_def dom_def) apply (erule allE, erule impE, erule exI) apply (clarsimp elim!: valid_obj) apply (simp add: obj_at_def) done

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

goal (1 subgoal):
 1. valid_objs (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); ptr \<notin> untyped_range cap; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> valid_obj ptr y (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. \<lbrakk>ptr \<notin> untyped_range cap; kheap s ptr = Some y; \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s\<rbrakk> \<Longrightarrow> valid_obj ptr y (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>ptr y. \<lbrakk>ptr \<notin> untyped_range cap; kheap s ptr = Some y\<rbrakk> \<Longrightarrow> ko_at y ptr s proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma pspace_aligned_detype[detype_invs_lemmas] :  "pspace_aligned (detype (untyped_range cap) s)" using invs_psp_aligned[OF invs] apply (clarsimp simp: pspace_aligned_def) apply (drule bspec, erule domI) apply (clarsimp simp: detype_def) done

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

goal (1 subgoal):
 1. pspace_aligned (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); kheap s x = Some y; x \<notin> untyped_range cap\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits (the (kheap (detype (untyped_range cap) s) x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>kheap s x = Some y; x \<notin> untyped_range cap; is_aligned x (obj_bits (the (kheap s x)))\<rbrakk> \<Longrightarrow> is_aligned x (obj_bits (the (kheap (detype (untyped_range cap) s) x))) proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma sym_refs_detype[detype_invs_lemmas] :
  "sym_refs (state_refs_of (detype (untyped_range cap) s))" using refsym by (simp add: state_refs)

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

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

lemma pspace_distinct_detype[detype_invs_lemmas]: "pspace_distinct (detype (untyped_range cap) s)" apply (insert invs, drule invs_distinct) apply (auto simp: pspace_distinct_def) done

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

lemma cut_tcb_detype[detype_invs_lemmas]:
  assumes ct_act: "ct_active s"
  shows "cur_tcb (detype (untyped_range cap) s)"  (* CT_ACT *)
     apply (insert ct_act invs) apply (drule tcb_at_invs) apply (simp add: cur_tcb_def ct_in_state_def) apply (clarsimp simp: detype_def pred_tcb_at_def) apply (fastforce simp: live_def dest: live_okE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_tcb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. cur_tcb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s\<rbrakk> \<Longrightarrow> cur_tcb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_tcb (detype (untyped_range cap) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at active (cur_thread s) s; tcb_at (cur_thread s) s\<rbrakk> \<Longrightarrow> cur_thread (detype (untyped_range cap) s) \<notin> untyped_range cap \<and> tcb_at (cur_thread (detype (untyped_range cap) s)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> active (tcb_state tcb)) (cur_thread s) s; tcb_at (cur_thread s) s; cur_thread s \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma live_okE2: "\<And>obj p. \<lbrakk> kheap s p = Some obj; live obj \<rbrakk>
                      \<Longrightarrow> p \<notin> untyped_range cap" by (simp add: live_okE[where P=live] obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>obj p. \<lbrakk>kheap s p = Some obj; live obj\<rbrakk> \<Longrightarrow> p \<notin> untyped_range cap
theory Detype_AI

lemma untyped_mdb : "\<And>m. untyped_mdb m (caps_of_state s)
                    \<Longrightarrow> untyped_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)" apply (simp only: untyped_mdb_def) apply (elim allEI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m. untyped_mdb m (caps_of_state s) \<Longrightarrow> untyped_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (1 subgoal):
 1. \<And>m. \<forall>ptr ptr' cap cap'. caps_of_state s ptr = Some cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> caps_of_state s ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range cap \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m \<Longrightarrow> \<forall>ptr ptr' capa cap'. (if fst ptr \<in> untyped_range cap then None else caps_of_state s ptr) = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> (if fst ptr' \<in> untyped_range cap then None else caps_of_state s ptr') = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal (1 subgoal):
 1. \<And>m ptr ptr' capa cap'. caps_of_state s ptr = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> caps_of_state s ptr' = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m \<Longrightarrow> (if fst ptr \<in> untyped_range cap then None else caps_of_state s ptr) = Some capa \<longrightarrow> is_untyped_cap capa \<longrightarrow> (if fst ptr' \<in> untyped_range cap then None else caps_of_state s ptr') = Some cap' \<longrightarrow> obj_refs cap' \<inter> untyped_range capa \<noteq> {} \<longrightarrow> ptr' \<in> descendants_of ptr m proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma reply_caps_mdb : "\<And>m. reply_caps_mdb m (caps_of_state s)
                       \<Longrightarrow> reply_caps_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)" apply (simp only: reply_caps_mdb_def) apply (elim allEI) apply (clarsimp elim!: exEI) apply (fastforce dest: non_null_caps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m. reply_caps_mdb m (caps_of_state s) \<Longrightarrow> reply_caps_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (1 subgoal):
 1. \<And>m. \<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> caps_of_state s ptr' = Some (ReplyCap t True rights')) \<Longrightarrow> \<forall>ptr t rights. (if fst ptr \<in> untyped_range cap then None else caps_of_state s ptr) = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> (if fst ptr' \<in> untyped_range cap then None else caps_of_state s ptr') = Some (ReplyCap t True rights')) proof (prove)
goal (1 subgoal):
 1. \<And>m ptr t rights. caps_of_state s ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> caps_of_state s ptr' = Some (ReplyCap t True rights')) \<Longrightarrow> (if fst ptr \<in> untyped_range cap then None else caps_of_state s ptr) = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> (if fst ptr' \<in> untyped_range cap then None else caps_of_state s ptr') = Some (ReplyCap t True rights')) proof (prove)
goal (1 subgoal):
 1. \<And>m a b t rights x ba rights'. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some (ReplyCap t False rights); m (a, b) = Some (x, ba); caps_of_state s (x, ba) = Some (ReplyCap t True rights'); x \<in> untyped_range cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Detype_AI

lemma reply_masters_mdb : "\<And>m. reply_masters_mdb m (caps_of_state s)
                          \<Longrightarrow> reply_masters_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)" apply (simp only: reply_masters_mdb_def) apply (elim allEI) apply clarsimp apply (drule(1) bspec) apply (fastforce dest: non_null_caps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m. reply_masters_mdb m (caps_of_state s) \<Longrightarrow> reply_masters_mdb m (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p) proof (prove)
goal (1 subgoal):
 1. \<And>m. \<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')) \<Longrightarrow> \<forall>ptr t rights. (if fst ptr \<in> untyped_range cap then None else caps_of_state s ptr) = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. (if fst ptr' \<in> untyped_range cap then None else caps_of_state s ptr') = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>m ptr t rights. caps_of_state s ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')) \<Longrightarrow> (if fst ptr \<in> untyped_range cap then None else caps_of_state s ptr) = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. (if fst ptr' \<in> untyped_range cap then None else caps_of_state s ptr') = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>m a b t rights aa ba. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some (ReplyCap t True rights); (aa, ba) \<in> descendants_of (a, b) m; aa \<in> untyped_range cap; m (a, b) = None; \<forall>ptr'\<in>descendants_of (a, b) m. \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>m a b t rights aa ba. \<lbrakk>a \<notin> untyped_range cap; caps_of_state s (a, b) = Some (ReplyCap t True rights); (aa, ba) \<in> descendants_of (a, b) m; aa \<in> untyped_range cap; m (a, b) = None; \<exists>rights'. caps_of_state s (aa, ba) = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!