theory CSpace_R

lemma untyped_mdb_n:
  shows "untyped_mdb' n" using untyped_mdb apply (clarsimp simp add: untyped_mdb'_def descendants split del: if_split) apply (drule n_cap)+ apply (clarsimp split: if_split_asm simp: descendants_of'_def capRange_c' untyped_c') apply (erule_tac x=src in allE) apply (erule_tac x=p' in allE) apply (fastforce simp: src dest: untyped_no_parent) apply (erule_tac x=p in allE) apply (erule_tac x=src in allE) apply (simp add: src) 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. \<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> p' \<in> descendants_of' p m); n p = Some (CTE c na); isUntypedCap c; n p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; p' \<notin> (if src \<in> descendants_of' p m then {dest} else {})\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c'a 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> p' \<in> descendants_of' p m); isUntypedCap c; \<not> isUntypedCap c'a; capRange c'a \<inter> untypedRange c \<noteq> {}; p' \<notin> (if src \<in> descendants_of' p m then {dest} else {}); \<exists>node'. if p = dest then c = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE c node'); \<exists>node'. if p' = dest then c'a = c' \<and> m p' = Some (CTE dest_cap node') else m p' = Some (CTE c'a node')\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p m proof (prove)
goal (2 subgoals):
 1. \<And>p' c' node' node'a. \<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 src_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; m dest = Some (CTE dest_cap node'); p' \<noteq> dest; m p' = Some (CTE c' node'a)\<rbrakk> \<Longrightarrow> False
 2. \<And>p c node' node'a. \<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 src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> dest; m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p' c' node' node'a. \<lbrakk>isUntypedCap src_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; m dest = Some (CTE dest_cap node'); p' \<noteq> dest; m p' = Some (CTE c' node'a); \<forall>p' c. (\<exists>n. m src = 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> src \<rightarrow> p')\<rbrakk> \<Longrightarrow> False
 2. \<And>p c node' node'a. \<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 src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> dest; m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p' c' node' node'a. \<lbrakk>isUntypedCap src_cap; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange src_cap \<noteq> {}; m dest = Some (CTE dest_cap node'); p' \<noteq> dest; m p' = Some (CTE c' node'a); \<forall>c. (\<exists>n. m src = 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> src \<rightarrow> p')\<rbrakk> \<Longrightarrow> False
 2. \<And>p c node' node'a. \<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 src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> dest; m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p c node' node'a. \<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 src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> dest; m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p c node' node'a. \<lbrakk>isUntypedCap c; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> dest; m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a); \<forall>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')\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p c node' node'a. \<lbrakk>isUntypedCap c; \<not> isUntypedCap src_cap; capRange src_cap \<inter> untypedRange c \<noteq> {}; \<not> m \<turnstile> p \<rightarrow> src; p \<noteq> dest; m p = Some (CTE c node'); m dest = Some (CTE dest_cap node'a); \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m src = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> m \<turnstile> p \<rightarrow> src)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!