theory CSpaceInv_AI

lemma valid_mdb_no_null:
  "\<lbrakk> valid_mdb s; caps_of_state s p = Some cap.NullCap \<rbrakk> \<Longrightarrow>
  \<not> cdt s \<Turnstile> p \<rightarrow> p' \<and> \<not> cdt s \<Turnstile> p' \<rightarrow> p" apply (simp add: valid_mdb_def mdb_cte_at_def cte_wp_at_caps_of_state) apply (cases p, cases p') apply (rule conjI) apply (fastforce dest!: tranclD simp: cdt_parent_defs) apply (fastforce dest!: tranclD2 simp: cdt_parent_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; caps_of_state s p = Some NullCap\<rbrakk> \<Longrightarrow> (p, p') \<notin> (cdt_parent_rel (cdt s))\<^sup>+ \<and> (p', p) \<notin> (cdt_parent_rel (cdt s))\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> NullCap \<noteq> cap)) \<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); caps_of_state s p = Some NullCap\<rbrakk> \<Longrightarrow> (p, p') \<notin> (cdt_parent_rel (cdt s))\<^sup>+ \<and> (p', p) \<notin> (cdt_parent_rel (cdt s))\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> NullCap \<noteq> cap)) \<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); caps_of_state s p = Some NullCap; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (p, p') \<notin> (cdt_parent_rel (cdt s))\<^sup>+ \<and> (p', p) \<notin> (cdt_parent_rel (cdt s))\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> NullCap \<noteq> cap)) \<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); caps_of_state s p = Some NullCap; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (p, p') \<notin> (cdt_parent_rel (cdt s))\<^sup>+
 2. \<And>a b aa ba. \<lbrakk>(\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> NullCap \<noteq> cap)) \<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); caps_of_state s p = Some NullCap; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (p', p) \<notin> (cdt_parent_rel (cdt s))\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(\<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> NullCap \<noteq> cap) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> NullCap \<noteq> cap)) \<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); caps_of_state s p = Some NullCap; p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> (p', p) \<notin> (cdt_parent_rel (cdt s))\<^sup>+ proof (prove)
goal:
No subgoals!