theory CSpace_R

lemma valid_badges' [simp]:
  "valid_badges n'" using simple src dest apply (clarsimp simp: valid_badges_def) apply (simp add: n_direct_eq') apply (frule_tac p=p in n'_badge) apply (frule_tac p=p' in n'_badge) apply (drule n'_cap)+ apply (clarsimp split: if_split_asm) apply (insert valid_badges) apply (simp add: valid_badges_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges n' proof (prove)
using this:
is_simple_cap' c'
m src = Some (CTE src_cap src_node)
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. valid_badges n' proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some (CTE cap node); n' p' = Some (CTE cap' node'); n' \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some (CTE cap node); n' p' = Some (CTE cap' node'); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some (CTE cap node); n' p' = Some (CTE cap' node'); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<exists>node'. if p = dest then mdbFirstBadged node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' p = Some (CTE cap node); n' p' = Some (CTE cap' node'); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<exists>node'. if p = dest then mdbFirstBadged node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node'; \<exists>node'a. if p' = dest then mdbFirstBadged node' = revokable' src_cap c' \<and> m p' = Some (CTE dest_cap node'a) else m p' = Some (CTE cap' node'a) \<and> mdbFirstBadged node' = mdbFirstBadged node'a\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node'. \<lbrakk>is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; \<exists>node'. if p = dest then mdbFirstBadged node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \<and> mdbFirstBadged node = mdbFirstBadged node'; \<exists>node'a. if p' = dest then mdbFirstBadged node' = revokable' src_cap c' \<and> m p' = Some (CTE dest_cap node'a) else m p' = Some (CTE cap' node'a) \<and> mdbFirstBadged node' = mdbFirstBadged node'a; \<exists>node'. if p = dest then cap = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node'); \<exists>node'. if p' = dest then cap' = c' \<and> m p' = Some (CTE dest_cap node') else m p' = Some (CTE cap' node')\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' node'a node'b. \<lbrakk>m p = Some (CTE cap node'a); m p' = Some (CTE cap' node'b); m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; mdbFirstBadged node = mdbFirstBadged node'a; p' \<noteq> dest; mdbFirstBadged node' = mdbFirstBadged node'b\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'b) \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'b) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' node'a node'b. \<lbrakk>m p = Some (CTE cap node'a); m p' = Some (CTE cap' node'b); m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; mdbFirstBadged node = mdbFirstBadged node'a; p' \<noteq> dest; mdbFirstBadged node' = mdbFirstBadged node'b; valid_badges m\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'b) \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'b) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap node cap' node' node'a node'b. \<lbrakk>m p = Some (CTE cap node'a); m p' = Some (CTE cap' node'b); m \<turnstile> p \<leadsto> p'; global.sameRegionAs cap cap'; is_simple_cap' c'; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); p \<noteq> src; p \<noteq> dest; mdbFirstBadged node = mdbFirstBadged node'a; p' \<noteq> dest; mdbFirstBadged node' = mdbFirstBadged node'b; \<forall>p p' cap. (\<exists>node. m p = Some (CTE cap node)) \<longrightarrow> (\<forall>cap' node'. m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> global.sameRegionAs cap cap' \<longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'))\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'b) \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node'b) proof (prove)
goal:
No subgoals!