theory CSpace_AI

lemma dest_desc:
  "descendants_of dest m = {}" using valid_mdb dest_null unfolding valid_mdb_def mdb_cte_at_def apply (clarsimp simp add: descendants_of_def m[symmetric]) apply (drule tranclD) apply (clarsimp simp: cdt_parent_of_def) apply (cases dest) apply (clarsimp simp: cte_wp_at_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of dest m = {} proof (prove)
using this:
valid_mdb s
cte_wp_at ((=) NullCap) dest s

goal (1 subgoal):
 1. descendants_of dest m = {} proof (prove)
using this:
(\<forall>p c. cdt s c = Some p \<longrightarrow> swp (cte_wp_at ((\<noteq>) NullCap)) s p \<and> swp (cte_wp_at ((\<noteq>) NullCap)) s c) \<and> untyped_mdb (cdt s) (caps_of_state s) \<and> descendants_inc (cdt s) (caps_of_state s) \<and> no_mloop (cdt s) \<and> untyped_inc (cdt s) (caps_of_state s) \<and> ut_revocable (is_original_cap s) (caps_of_state s) \<and> irq_revocable (is_original_cap s) (caps_of_state s) \<and> reply_master_revocable (is_original_cap s) (caps_of_state s) \<and> reply_mdb (cdt s) (caps_of_state s) \<and> valid_arch_mdb (is_original_cap s) (caps_of_state s)
cte_wp_at ((=) NullCap) dest s

goal (1 subgoal):
 1. descendants_of dest m = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) NullCap) dest s; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb m (caps_of_state s); descendants_inc m (caps_of_state s); no_mloop m; untyped_inc m (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb m (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); m \<Turnstile> dest \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) NullCap) dest s; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb m (caps_of_state s); descendants_inc m (caps_of_state s); no_mloop m; untyped_inc m (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb m (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); \<exists>z. m \<Turnstile> dest \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cte_wp_at ((=) NullCap) dest s; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb m (caps_of_state s); descendants_inc m (caps_of_state s); no_mloop m; untyped_inc m (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb m (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); m (aa, ba) = Some dest; m \<Turnstile> (aa, ba) \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>cte_wp_at ((=) NullCap) dest s; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> cte_wp_at ((\<noteq>) NullCap) (a, b) s \<and> cte_wp_at ((\<noteq>) NullCap) (aa, ba) s; untyped_mdb m (caps_of_state s); descendants_inc m (caps_of_state s); no_mloop m; untyped_inc m (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb m (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); m (aa, ba) = Some dest; m \<Turnstile> (aa, ba) \<rightarrow>* (a, b); dest = (ab, bb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>fst (get_cap (ab, bb) s) = {(NullCap, s)}; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> NullCap \<noteq> cap) \<and> (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)} \<and> NullCap \<noteq> cap); untyped_mdb m (caps_of_state s); descendants_inc m (caps_of_state s); no_mloop m; untyped_inc m (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb m (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); m (aa, ba) = Some (ab, bb); m \<Turnstile> (aa, ba) \<rightarrow>* (a, b); dest = (ab, bb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!