theory Finalise_R

lemma untyped_mdb_n:
  "untyped_mdb' n" using untyped_mdb apply (simp add: untyped_mdb'_def descendants_of'_def parency) apply clarsimp apply (drule n_cap)+ apply (clarsimp split: if_split_asm) apply (case_tac "p=slot", simp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb' n proof (prove)
using this:
untyped_mdb' m

goal (1 subgoal):
 1. untyped_mdb' n proof (prove)
goal (1 subgoal):
 1. \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p') \<Longrightarrow> \<forall>p p' c. (\<exists>na. n p = Some (CTE c na)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. n p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c na c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); n p = Some (CTE c na); isUntypedCap c; n p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}\<rbrakk> \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then c = capability.NullCap else cap' = c); \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then c' = capability.NullCap else cap' = c')\<rbrakk> \<Longrightarrow> p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' cap' node'. \<lbrakk>m p' = Some (CTE c' node'); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE cap' node')) \<and> c = capability.NullCap; p = slot \<or> (\<exists>node'. m p = Some (CTE cap' node')) \<and> cap' = c\<rbrakk> \<Longrightarrow> p \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' cap' node'. \<lbrakk>m p' = Some (CTE c' node'); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> p'); isUntypedCap c; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE cap' node')) \<and> c = capability.NullCap; p = slot \<or> (\<exists>node'. m p = Some (CTE cap' node')) \<and> cap' = c; p \<noteq> slot\<rbrakk> \<Longrightarrow> p \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p' proof (prove)
goal:
No subgoals!