theory CSpace1_R

lemma valid_badges_def2:
  "valid_badges m =
  (\<forall>p p' cap node cap' node'.
   m p = Some (CTE cap node) \<longrightarrow>
   m p' = Some (CTE cap' node') \<longrightarrow>
   m \<turnstile> p \<leadsto> p' \<longrightarrow>
   capMasterCap cap = capMasterCap cap' \<longrightarrow>
   capBadge cap \<noteq> None \<longrightarrow>
   capBadge cap \<noteq> capBadge cap' \<longrightarrow>
   capBadge cap' \<noteq> Some 0 \<longrightarrow>
   mdbFirstBadged node')" apply (simp add: valid_badges_def) apply (intro arg_cong[where f=All] ext imp_cong [OF refl]) apply (case_tac cap, simp_all add: isCap_simps cong: weak_imp_cong) apply (fastforce simp: sameRegionAs_def3 isCap_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges m = (\<forall>p p' cap node cap' node'. m p = Some (CTE cap node) \<longrightarrow> m p' = Some (CTE cap' node') \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capMasterCap cap = capMasterCap cap' \<longrightarrow> capBadge cap \<noteq> None \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. (\<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'))) = (\<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> capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap' node'. \<lbrakk>\<exists>node. m p = Some (CTE cap node); m p' = Some (CTE cap' node'); m \<turnstile> p \<leadsto> p'\<rbrakk> \<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')) = (capMasterCap cap = capMasterCap cap' \<longrightarrow> (\<exists>y. capBadge cap = Some y) \<longrightarrow> capBadge cap \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<And>p p' cap cap' node' x31 x32 x33 x34. \<lbrakk>\<exists>node. m p = Some (CTE (capability.NotificationCap x31 x32 x33 x34) node); m p' = Some (CTE cap' node'); m \<turnstile> p \<leadsto> p'; cap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (global.sameRegionAs (capability.NotificationCap x31 x32 x33 x34) cap' \<longrightarrow> x32 \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') = (capability.NotificationCap x31 0 True True = capMasterCap cap' \<longrightarrow> Some x32 \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node')
 2. \<And>p p' cap cap' node' x51 x52 x53 x54 x55 x56. \<lbrakk>\<exists>node. m p = Some (CTE (capability.EndpointCap x51 x52 x53 x54 x55 x56) node); m p' = Some (CTE cap' node'); m \<turnstile> p \<leadsto> p'; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (global.sameRegionAs (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap' \<longrightarrow> x52 \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') = (capability.EndpointCap x51 0 True True True True = capMasterCap cap' \<longrightarrow> Some x52 \<noteq> capBadge cap' \<longrightarrow> capBadge cap' \<noteq> Some 0 \<longrightarrow> mdbFirstBadged node') proof (prove)
goal:
No subgoals!