theory Retype_R

lemma untyped_inc_n: "untyped_inc' n" proof - from valid have "untyped_inc' m" .. thus ?thesis apply (clarsimp simp: untyped_inc'_def) apply (simp add: n_Some_eq split: if_split_asm) apply blast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc' n proof (state)
goal (1 subgoal):
 1. untyped_inc' n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. untyped_inc' m proof (state)
this:
untyped_inc' m

goal (1 subgoal):
 1. untyped_inc' n proof (prove)
using this:
untyped_inc' m

goal (1 subgoal):
 1. untyped_inc' 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> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')); n p = Some (CTE c na); isUntypedCap c; n p' = Some (CTE c' n'); isUntypedCap c'\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n'. \<lbrakk>isUntypedCap c'; \<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> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')); \<not> P p; m p = Some (CTE c n); isUntypedCap c; \<not> P p'; m p' = Some (CTE c' n')\<rbrakk> \<Longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> untypedRange c' \<inter> usableUntypedRange c = {}) proof (prove)
goal:
No subgoals! proof (state)
this:
untyped_inc' n

goal:
No subgoals!