theory CNodeInv_AI

lemma unique_reply_caps_cap_swap:
  assumes u: "unique_reply_caps cs"
  and     c: "cs p = Some cap"
  and    c': "cs p' = Some cap'"
  and    wd: "weak_derived c cap"
  and   wd': "weak_derived c' cap'"
  and  pneq: "p \<noteq> p'"
  shows "unique_reply_caps (cs (p \<mapsto> c', p' \<mapsto> c))" proof - have new_cap_is_unique[elim]:
    "\<And> p'' t R R'.\<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R);
       c = ReplyCap t False R' \<or> c' = ReplyCap t False R' \<rbrakk>
     \<Longrightarrow> False" using u unfolding unique_reply_caps_def apply (erule_tac disjE) apply simp apply (frule weak_derived_Reply_eq[OF wd]) apply (fastforce simp add:c) apply simp apply (frule weak_derived_Reply_eq[OF wd']) apply (fastforce simp add:c' is_cap_simps) done have old_caps_differ:
    "\<And>t R R'.
     \<lbrakk> cap= ReplyCap t False R; cap' = ReplyCap t False R' \<rbrakk>
     \<Longrightarrow> False" using u c c' is_cap_simps pneq unfolding unique_reply_caps_def by fastforce have new_cap_objs_differ[elim]:
    "\<And>t R R'. \<lbrakk> c= ReplyCap t False R; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False" apply (drule weak_derived_Reply_eq [OF wd]) apply (drule weak_derived_Reply_eq [OF wd']) using old_caps_differ by fastforce show ?thesis using u unfolding unique_reply_caps_def apply (intro allI impI) apply (simp split: if_split_asm del: split_paired_All) apply fastforce+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (state)
goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); c = ReplyCap t False R' \<or> c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
unique_reply_caps cs

goal (1 subgoal):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); c = ReplyCap t False R' \<or> c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'

goal (1 subgoal):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); c = ReplyCap t False R' \<or> c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'; c = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False
 2. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; c = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False
 2. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; c = ReplyCap t False R'; \<exists>R'. cap = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False
 2. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>p'' t R R'. \<lbrakk>p'' \<noteq> p; p'' \<noteq> p'; cs p'' = Some (ReplyCap t False R); \<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; c' = ReplyCap t False R'; \<exists>R'. cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?p'' \<noteq> p; ?p'' \<noteq> p'; cs ?p'' = Some (ReplyCap ?t False ?R); c = ReplyCap ?t False ?R' \<or> c' = ReplyCap ?t False ?R'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>cap = ReplyCap t False R; cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
unique_reply_caps cs
cs p = Some cap
cs p' = Some cap'
is_cnode_cap ?cap = (\<exists>r bits g. ?cap = CNodeCap r bits g)
is_thread_cap ?cap = (\<exists>r. ?cap = ThreadCap r)
is_domain_cap ?cap = (?cap = DomainCap)
is_untyped_cap ?cap = (\<exists>dev r bits f. ?cap = UntypedCap dev r bits f)
is_ep_cap ?cap = (\<exists>r b R. ?cap = EndpointCap r b R)
is_ntfn_cap ?cap = (\<exists>r b R. ?cap = NotificationCap r b R)
is_zombie ?cap = (\<exists>r b n. ?cap = Zombie r b n)
is_arch_cap ?cap = (\<exists>a. ?cap = ArchObjectCap a)
is_reply_cap ?cap = (\<exists>x R. ?cap = ReplyCap x False R)
is_master_reply_cap ?cap = (\<exists>x R. ?cap = ReplyCap x True R)
p \<noteq> p'

goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>cap = ReplyCap t False R; cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'
cs p = Some cap
cs p' = Some cap'
is_cnode_cap ?cap = (\<exists>r bits g. ?cap = CNodeCap r bits g)
is_thread_cap ?cap = (\<exists>r. ?cap = ThreadCap r)
is_domain_cap ?cap = (?cap = DomainCap)
is_untyped_cap ?cap = (\<exists>dev r bits f. ?cap = UntypedCap dev r bits f)
is_ep_cap ?cap = (\<exists>r b R. ?cap = EndpointCap r b R)
is_ntfn_cap ?cap = (\<exists>r b R. ?cap = NotificationCap r b R)
is_zombie ?cap = (\<exists>r b n. ?cap = Zombie r b n)
is_arch_cap ?cap = (\<exists>a. ?cap = ArchObjectCap a)
is_reply_cap ?cap = (\<exists>x R. ?cap = ReplyCap x False R)
is_master_reply_cap ?cap = (\<exists>x R. ?cap = ReplyCap x True R)
p \<noteq> p'

goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>cap = ReplyCap t False R; cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (state)
this:
\<lbrakk>cap = ReplyCap ?t False ?R; cap' = ReplyCap ?t False ?R'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>c = ReplyCap t False R; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>c' = ReplyCap t False R'; \<exists>R'. cap = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>\<exists>R'. cap = ReplyCap t False R'; \<exists>R'. cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<lbrakk>cap = ReplyCap ?t False ?R; cap' = ReplyCap ?t False ?R'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>t R R'. \<lbrakk>\<exists>R'. cap = ReplyCap t False R'; \<exists>R'. cap' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (state)
this:
\<lbrakk>c = ReplyCap ?t False ?R; c' = ReplyCap ?t False ?R'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
using this:
unique_reply_caps cs

goal (1 subgoal):
 1. unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c)) proof (prove)
using this:
\<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'

goal (1 subgoal):
 1. \<forall>ptr ptr' t R R'. (cs(p \<mapsto> c', p' \<mapsto> c)) ptr = Some (ReplyCap t False R) \<longrightarrow> (cs(p \<mapsto> c', p' \<mapsto> c)) ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr' proof (prove)
goal (1 subgoal):
 1. \<And>ptr ptr' t R R'. \<lbrakk>\<forall>ptr ptr' t R R'. cs ptr = Some (ReplyCap t False R) \<longrightarrow> cs ptr' = Some (ReplyCap t False R') \<longrightarrow> ptr = ptr'; (cs(p \<mapsto> c', p' \<mapsto> c)) ptr = Some (ReplyCap t False R); (cs(p \<mapsto> c', p' \<mapsto> c)) ptr' = Some (ReplyCap t False R')\<rbrakk> \<Longrightarrow> ptr = ptr' proof (prove)
goal (6 subgoals):
 1. \<And>ptr ptr' t R R'. \<lbrakk>\<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; ptr = p'; c = ReplyCap t False R; p \<noteq> p'; ptr' = p; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False
 2. \<And>ptr ptr' t R R'. \<lbrakk>\<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; ptr = p'; c = ReplyCap t False R; ptr' \<noteq> p'; ptr' \<noteq> p; cs ptr' = Some (ReplyCap t False R')\<rbrakk> \<Longrightarrow> False
 3. \<And>ptr ptr' t R R'. \<lbrakk>ptr' = p'; c = ReplyCap t False R'; \<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; p \<noteq> p'; ptr = p; c' = ReplyCap t False R\<rbrakk> \<Longrightarrow> False
 4. \<And>ptr ptr' t R R'. \<lbrakk>ptr' = p'; c = ReplyCap t False R'; \<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; ptr \<noteq> p'; ptr \<noteq> p; cs ptr = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> False
 5. \<And>ptr ptr' t R R'. \<lbrakk>\<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; p \<noteq> p'; ptr = p; c' = ReplyCap t False R; ptr' \<noteq> p'; ptr' \<noteq> p; cs ptr' = Some (ReplyCap t False R')\<rbrakk> \<Longrightarrow> False
 6. \<And>ptr ptr' t R R'. \<lbrakk>\<forall>ptr ptr' t. (\<exists>R. cs ptr = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. cs ptr' = Some (ReplyCap t False R')) \<longrightarrow> ptr = ptr'; ptr \<noteq> p'; ptr \<noteq> p; cs ptr = Some (ReplyCap t False R); p \<noteq> p'; ptr' = p; c' = ReplyCap t False R'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
unique_reply_caps (cs(p \<mapsto> c', p' \<mapsto> c))

goal:
No subgoals!