theory CSpace_AI

lemma dest_None:
  "m dest = None" using valid_mdb dest_null unfolding valid_mdb_def mdb_cte_at_def apply (clarsimp simp: m [symmetric]) apply (cases dest) apply (rule classical) apply (clarsimp simp: cte_wp_at_def) apply fastforce done

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

goal (1 subgoal):
 1. m dest = None 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. m dest = None proof (prove)
goal (1 subgoal):
 1. \<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)\<rbrakk> \<Longrightarrow> m dest = None 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); dest = (a, b)\<rbrakk> \<Longrightarrow> m dest = None 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); dest = (a, b); m dest \<noteq> None\<rbrakk> \<Longrightarrow> m dest = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>fst (get_cap (a, b) 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); dest = (a, b); m (a, b) = Some (aa, ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!