theory Detype_AI

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m. untyped_inc m (caps_of_state s) \<Longrightarrow> untyped_inc 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>p p' c c'. caps_of_state s p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> caps_of_state s p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p') \<Longrightarrow> \<forall>p p' c c'. (if fst p \<in> untyped_range cap then None else caps_of_state s p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (if fst p' \<in> untyped_range cap then None else caps_of_state s p') = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal (1 subgoal):
 1. \<And>m p p' c c'. caps_of_state s p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> caps_of_state s p' = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p') \<Longrightarrow> (if fst p \<in> untyped_range cap then None else caps_of_state s p) = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (if fst p' \<in> untyped_range cap then None else caps_of_state s p') = Some c' \<longrightarrow> is_untyped_cap c' \<longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> (untyped_range c \<subset> untyped_range c' \<longrightarrow> p \<in> descendants_of p' m \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p m \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p m \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' m \<and> usable_untyped_range c' = {} \<or> p = p') proof (prove)
goal:
No subgoals!