theory CSpace_AI

lemma untyped_inc:
  assumes u: "untyped_inc m cs"
  assumes d: "is_derived m src cap c"
  assumes p: "\<not>should_be_parent_of c r cap f" "cap_aligned cap"
  assumes r: "is_untyped_cap c \<longrightarrow> r"
  shows "untyped_inc n (cs(dest \<mapsto> cap))" proof - from p d r have u1: "\<not>is_untyped_cap c" by - (rule not_parent_not_untyped) moreover with d have u2: "\<not>is_untyped_cap cap" by (auto simp: is_derived_def cap_master_cap_def is_cap_simps
             split: if_split_asm cap.splits) ultimately show ?thesis using u desc unfolding untyped_inc_def by (auto simp: descendants split: if_split_asm) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (state)
goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (chain)
picking this:
\<not> should_be_parent_of c r cap f
cap_aligned cap
is_derived m src cap c
is_untyped_cap c \<longrightarrow> r proof (prove)
using this:
\<not> should_be_parent_of c r cap f
cap_aligned cap
is_derived m src cap c
is_untyped_cap c \<longrightarrow> r

goal (1 subgoal):
 1. \<not> is_untyped_cap c proof (state)
this:
\<not> is_untyped_cap c

goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (state)
this:
\<not> is_untyped_cap c

goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (chain)
picking this:
is_derived m src cap c
\<not> is_untyped_cap c proof (prove)
using this:
is_derived m src cap c
\<not> is_untyped_cap c

goal (1 subgoal):
 1. \<not> is_untyped_cap cap proof (state)
this:
\<not> is_untyped_cap cap

goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (chain)
picking this:
\<not> is_untyped_cap c
\<not> is_untyped_cap cap proof (prove)
using this:
\<not> is_untyped_cap c
\<not> is_untyped_cap cap

goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (prove)
using this:
\<not> is_untyped_cap c
\<not> is_untyped_cap cap
untyped_inc m cs
descendants_of dest m = {}

goal (1 subgoal):
 1. untyped_inc n (cs(dest \<mapsto> cap)) proof (prove)
using this:
\<not> is_untyped_cap c
\<not> is_untyped_cap cap
\<forall>p p' c c'. cs p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> cs 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')
descendants_of dest m = {}

goal (1 subgoal):
 1. \<forall>p p' c c'. (cs(dest \<mapsto> cap)) p = Some c \<longrightarrow> is_untyped_cap c \<longrightarrow> (cs(dest \<mapsto> cap)) 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' n \<and> untyped_range c \<inter> usable_untyped_range c' = {}) \<and> (untyped_range c' \<subset> untyped_range c \<longrightarrow> p' \<in> descendants_of p n \<and> untyped_range c' \<inter> usable_untyped_range c = {}) \<and> (untyped_range c = untyped_range c' \<longrightarrow> p' \<in> descendants_of p n \<and> usable_untyped_range c = {} \<or> p \<in> descendants_of p' n \<and> usable_untyped_range c' = {} \<or> p = p') proof (state)
this:
untyped_inc n (cs(dest \<mapsto> cap))

goal:
No subgoals!