theory Syscall_C

lemma ccorres_ntfn_cases:
  assumes P: "\<And>p b send d. cap = NotificationCap p b send d \<Longrightarrow> ccorres r xf (P p b send d) (P' p b send d) hs (a cap) (c cap)"
  assumes Q: "\<not>isNotificationCap cap \<Longrightarrow> ccorres r xf (Q cap) (Q' cap) hs (a cap) (c cap)"
  shows
  "ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = NotificationCap p b send d \<longrightarrow> P p b send d s) \<and>
                     (\<not>isNotificationCap cap \<longrightarrow> Q cap s))
               ({s. \<forall>p b send d. cap = NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter>
                {s. \<not>isNotificationCap cap \<longrightarrow> s \<in> Q' cap})
               hs (a cap) (c cap)" apply (cases "isNotificationCap cap") apply (simp add: isCap_simps) apply (elim exE) apply (rule ccorres_guard_imp) apply (erule P) apply simp apply simp apply (rule ccorres_guard_imp) apply (erule Q) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (2 subgoals):
 1. isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap)
 2. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (2 subgoals):
 1. \<exists>v0 v1 v2 v3. cap = capability.NotificationCap v0 v1 v2 v3 \<Longrightarrow> ccorres r xf (\<lambda>s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} hs (a cap) (c cap)
 2. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (2 subgoals):
 1. \<And>v0 v1 v2 v3. cap = capability.NotificationCap v0 v1 v2 v3 \<Longrightarrow> ccorres r xf (\<lambda>s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} hs (a cap) (c cap)
 2. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (4 subgoals):
 1. \<And>v0 v1 v2 v3. cap = capability.NotificationCap v0 v1 v2 v3 \<Longrightarrow> ccorres r xf (?Q13 v0 v1 v2 v3) (?Q'13 v0 v1 v2 v3) hs (a cap) (c cap)
 2. \<And>v0 v1 v2 v3 s. \<lbrakk>cap = capability.NotificationCap v0 v1 v2 v3; \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s\<rbrakk> \<Longrightarrow> ?Q13 v0 v1 v2 v3 s
 3. \<And>v0 v1 v2 v3 s. \<lbrakk>cap = capability.NotificationCap v0 v1 v2 v3; s \<in> {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d}\<rbrakk> \<Longrightarrow> s \<in> ?Q'13 v0 v1 v2 v3
 4. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (3 subgoals):
 1. \<And>v0 v1 v2 v3 s. \<lbrakk>cap = capability.NotificationCap v0 v1 v2 v3; \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s\<rbrakk> \<Longrightarrow> P v0 v1 v2 v3 s
 2. \<And>v0 v1 v2 v3 s. \<lbrakk>cap = capability.NotificationCap v0 v1 v2 v3; s \<in> {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d}\<rbrakk> \<Longrightarrow> s \<in> P' v0 v1 v2 v3
 3. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (2 subgoals):
 1. \<And>v0 v1 v2 v3 s. \<lbrakk>cap = capability.NotificationCap v0 v1 v2 v3; s \<in> {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d}\<rbrakk> \<Longrightarrow> s \<in> P' v0 v1 v2 v3
 2. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (1 subgoal):
 1. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf (\<lambda>s. (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)) ({s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}) hs (a cap) (c cap) proof (prove)
goal (3 subgoals):
 1. \<not> isNotificationCap cap \<Longrightarrow> ccorres r xf ?Q20 ?Q'20 hs (a cap) (c cap)
 2. \<And>s. \<lbrakk>\<not> isNotificationCap cap; (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)\<rbrakk> \<Longrightarrow> ?Q20 s
 3. \<And>s. \<lbrakk>\<not> isNotificationCap cap; s \<in> {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}\<rbrakk> \<Longrightarrow> s \<in> ?Q'20 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> isNotificationCap cap; (\<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> P p b send d s) \<and> (\<not> isNotificationCap cap \<longrightarrow> Q cap s)\<rbrakk> \<Longrightarrow> Q cap s
 2. \<And>s. \<lbrakk>\<not> isNotificationCap cap; s \<in> {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}\<rbrakk> \<Longrightarrow> s \<in> Q' cap proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> isNotificationCap cap; s \<in> {s. \<forall>p b send d. cap = capability.NotificationCap p b send d \<longrightarrow> s \<in> P' p b send d} \<inter> {s. \<not> isNotificationCap cap \<longrightarrow> s \<in> Q' cap}\<rbrakk> \<Longrightarrow> s \<in> Q' cap proof (prove)
goal:
No subgoals!