theory CSpace_AI

lemma untyped_inc:
  assumes u: "untyped_inc m cs"
  assumes src: "cs src = Some c"
  assumes al:  "cap_aligned c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  assumes usable:"is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}"
  shows "untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" proof - from d have "untyped_range cap = untyped_range c" by (clarsimp simp: is_derived_def cap_master_cap_def is_cap_simps
                split: cap.split_asm if_split_asm) moreover from d have "is_untyped_cap cap \<longrightarrow> descendants_of src m = {}" by (auto simp: is_derived_def cap_master_cap_def is_cap_simps
             split: if_split_asm cap.splits) moreover from d have "is_untyped_cap cap \<longrightarrow> is_untyped_cap c" by (auto simp: is_derived_def cap_master_cap_def is_cap_simps
             split: if_split_asm cap.splits) ultimately show ?thesis using assms by (auto intro!: untyped_inc_simple) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (state)
goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (chain)
picking this:
is_derived m src cap c proof (prove)
using this:
is_derived m src cap c

goal (1 subgoal):
 1. untyped_range cap = untyped_range c proof (state)
this:
untyped_range cap = untyped_range c

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (state)
this:
untyped_range cap = untyped_range c

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

goal (1 subgoal):
 1. is_untyped_cap cap \<longrightarrow> descendants_of src m = {} proof (state)
this:
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (state)
this:
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}

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

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

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (chain)
picking this:
untyped_range cap = untyped_range c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
is_untyped_cap cap \<longrightarrow> is_untyped_cap c proof (prove)
using this:
untyped_range cap = untyped_range c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
is_untyped_cap cap \<longrightarrow> is_untyped_cap c

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
untyped_range cap = untyped_range c
is_untyped_cap cap \<longrightarrow> descendants_of src m = {}
is_untyped_cap cap \<longrightarrow> is_untyped_cap c
untyped_inc m cs
cs src = Some c
cap_aligned c
cs dest = Some NullCap
is_derived m src cap c
is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}

goal (1 subgoal):
 1. untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (state)
this:
untyped_inc (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))

goal:
No subgoals!