theory CSpace_AI

lemma (in mdb_insert_abs_sib) reply_caps_mdb_sib:
  assumes r: "reply_caps_mdb m cs"
  assumes p: "\<not>should_be_parent_of c r cap f"
  assumes rev: "is_master_reply_cap c \<longrightarrow> r"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  shows "reply_caps_mdb n (cs(dest \<mapsto> cap))" unfolding reply_caps_mdb_def using r p d apply (intro allI impI) apply (simp add: desc neq split: if_split_asm del: split_paired_Ex) apply (clarsimp simp: should_be_parent_of_def is_derived_def is_cap_simps
                         cap_master_cap_def rev) apply (unfold reply_caps_mdb_def)[1] apply (erule allE)+ apply (erule(1) impE) apply (erule exEI) apply (simp add: n_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_caps_mdb n (cs(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. n ptr = Some ptr' \<and> (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t True rights')) proof (prove)
using this:
reply_caps_mdb m cs
\<not> should_be_parent_of c r cap f
is_derived m src cap c

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. n ptr = Some ptr' \<and> (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t True rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; \<not> should_be_parent_of c r cap f; is_derived m src cap c; (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr' rights'. n ptr = Some ptr' \<and> (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t True rights') proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; \<not> should_be_parent_of c r (ReplyCap t False rights) f; is_derived m src (ReplyCap t False rights) c; ptr = dest; cap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> n dest = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights')))
 2. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; \<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> n ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; \<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> n ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. m ptr = Some ptr' \<and> cs ptr' = Some (ReplyCap t True rights')); \<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> n ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights); cs (?ptr40 ptr t rights) = Some (ReplyCap (?t42 ptr t rights) False (?rights44 ptr t rights)) \<longrightarrow> (\<exists>ptr' rights'. m (?ptr40 ptr t rights) = Some ptr' \<and> cs ptr' = Some (ReplyCap (?t42 ptr t rights) True rights'))\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> n ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights); \<exists>ptr' rights'. m ptr = Some ptr' \<and> cs ptr' = Some (ReplyCap t True rights')\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> n ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights x. \<lbrakk>\<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights); \<exists>rights'. m ptr = Some x \<and> cs x = Some (ReplyCap t True rights')\<rbrakk> \<Longrightarrow> x \<noteq> dest \<and> (x \<noteq> dest \<longrightarrow> n ptr = Some x \<and> (\<exists>rights'. cs x = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights x. \<lbrakk>\<not> should_be_parent_of c r cap f; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights); m ptr = Some x \<and> (\<exists>rights'. cs x = Some (ReplyCap t True rights'))\<rbrakk> \<Longrightarrow> x \<noteq> dest proof (prove)
goal:
No subgoals!