theory CSpace_AI

lemma (in mdb_insert_abs_sib) reply_masters_mdb_sib:
  assumes r: "reply_masters_mdb m cs"
  assumes src: "cs src = Some c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  shows "reply_masters_mdb n (cs(dest \<mapsto> cap))" unfolding reply_masters_mdb_def using r d apply (intro allI impI) apply (simp add: descendants) apply (simp add: neq desc split: if_split_asm) apply (clarsimp simp: is_derived_def is_cap_simps cap_master_cap_def) apply (unfold reply_masters_mdb_def) apply (intro conjI) apply (erule allE)+ apply (erule(1) impE) apply simp apply (rule impI) apply (erule conjE) apply (drule_tac x=src in bspec, assumption) apply (clarsimp simp: src is_derived_def is_cap_simps) apply (erule allE)+ apply (erule(1) impE) apply (rule impI, simp add: n_def) apply (rule impI, erule conjE) apply (drule_tac x=dest in bspec, assumption) apply (simp add: dst) done

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

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr n. \<exists>rights'. (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src cap c; (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr n. \<exists>rights'. (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src cap c; (if ptr = dest then Some cap else cs ptr) = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src (ReplyCap t True rights) c; ptr = dest; cap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> n dest = None
 2. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); cs (?ptr37 ptr t rights) = Some (ReplyCap (?t39 ptr t rights) True (?rights41 ptr t rights)) \<longrightarrow> m (?ptr37 ptr t rights) = None \<and> (\<forall>ptr'\<in>descendants_of (?ptr37 ptr t rights) m. \<exists>rights'. cs ptr' = Some (ReplyCap (?t39 ptr t rights) False rights'))\<rbrakk> \<Longrightarrow> src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> src \<in> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m; m ptr = None; \<exists>rights'. cs src = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> n ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights'))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); cs (?ptr52 ptr t rights) = Some (ReplyCap (?t54 ptr t rights) True (?rights56 ptr t rights)) \<longrightarrow> m (?ptr52 ptr t rights) = None \<and> (\<forall>ptr'\<in>descendants_of (?ptr52 ptr t rights) m. \<exists>rights'. cs ptr' = Some (ReplyCap (?t54 ptr t rights) False rights'))\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> src \<notin> descendants_of ptr m \<longrightarrow> n ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); src \<notin> descendants_of ptr m\<rbrakk> \<Longrightarrow> dest \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<notin> descendants_of ptr m; dest \<in> descendants_of ptr m; m ptr = None; \<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> \<exists>rights'. cap = ReplyCap t False rights' proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<notin> descendants_of ptr m; dest \<in> descendants_of ptr m; m ptr = None; \<exists>rights'. cs dest = Some (ReplyCap t False rights')\<rbrakk> \<Longrightarrow> \<exists>rights'. cap = ReplyCap t False rights' proof (prove)
goal:
No subgoals!