theory CNodeInv_R

lemma spec_corres_symb_exec_r_Ex:
  assumes y: "\<And>s. P' s \<Longrightarrow> \<forall>p \<in> fst (g s). snd p = s"
  assumes z: "\<And>s. P' s \<Longrightarrow> \<exists>p \<in> fst (g s). snd p = s"
  assumes nf: "no_fail P' g"
  assumes x: "\<And>rv. spec_corres s r P (\<lambda>s. \<exists>s'. (rv, s) \<in> fst (g s') \<and> P' s') f (h rv)"
  shows      "spec_corres s r P P' f (do rv \<leftarrow> g; h rv od)" apply (rule spec_corres_guard_imp) apply (rule spec_corres_symb_exec_r_All) prefer 2 apply (rule x) apply (insert nf)[1] apply (clarsimp simp: no_fail_def) apply (frule y) apply (drule(1) bspec) apply fastforce apply assumption apply (frule y) apply (rule conjI) apply clarsimp apply (drule(1) bspec) apply fastforce apply (frule z) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_corres s r P P' f (g >>= h) proof (prove)
goal (3 subgoals):
 1. spec_corres s r ?Q ?Q' f (g >>= h)
 2. P s \<Longrightarrow> ?Q s
 3. \<And>s'. P' s' \<Longrightarrow> ?Q' s' proof (prove)
goal (4 subgoals):
 1. \<And>rv. no_fail (?Q'4 rv) g
 2. \<And>rv. spec_corres s r ?Q (?Q'4 rv) f (h rv)
 3. P s \<Longrightarrow> ?Q s
 4. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> ?Q'4 (fst p) s') \<and> (\<exists>rv. ?Q'4 rv s') proof (prove)
goal (4 subgoals):
 1. \<And>rv. spec_corres s r ?Q (?Q'4 rv) f (h rv)
 2. \<And>rv. no_fail (?Q'4 rv) g
 3. P s \<Longrightarrow> ?Q s
 4. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> ?Q'4 (fst p) s') \<and> (\<exists>rv. ?Q'4 rv s') proof (prove)
goal (3 subgoals):
 1. \<And>rv. no_fail (\<lambda>s. \<exists>s'. (rv, s) \<in> fst (g s') \<and> P' s') g
 2. P s \<Longrightarrow> P s
 3. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (3 subgoals):
 1. \<And>rv. no_fail P' g \<Longrightarrow> no_fail (\<lambda>s. \<exists>s'. (rv, s) \<in> fst (g s') \<and> P' s') g
 2. P s \<Longrightarrow> P s
 3. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (3 subgoals):
 1. \<And>rv s s'. \<lbrakk>\<forall>s. P' s \<longrightarrow> \<not> snd (g s); (rv, s) \<in> fst (g s'); P' s'; snd (g s)\<rbrakk> \<Longrightarrow> False
 2. P s \<Longrightarrow> P s
 3. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (3 subgoals):
 1. \<And>rv s s'. \<lbrakk>\<forall>s. P' s \<longrightarrow> \<not> snd (g s); (rv, s) \<in> fst (g s'); P' s'; snd (g s); \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> False
 2. P s \<Longrightarrow> P s
 3. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (3 subgoals):
 1. \<And>rv s s'. \<lbrakk>\<forall>s. P' s \<longrightarrow> \<not> snd (g s); (rv, s) \<in> fst (g s'); P' s'; snd (g s); snd (rv, s) = s'\<rbrakk> \<Longrightarrow> False
 2. P s \<Longrightarrow> P s
 3. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (2 subgoals):
 1. P s \<Longrightarrow> P s
 2. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s'. P' s' \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> (\<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)) \<and> (\<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> \<forall>p\<in>fst (g s'). snd p = s' \<and> (\<exists>s'a. (fst p, s') \<in> fst (g s'a) \<and> P' s'a)
 2. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> \<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a proof (prove)
goal (2 subgoals):
 1. \<And>s' a b. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'; (a, b) \<in> fst (g s')\<rbrakk> \<Longrightarrow> \<exists>s'a. (a, s') \<in> fst (g s'a) \<and> P' s'a
 2. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> \<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a proof (prove)
goal (2 subgoals):
 1. \<And>s' a b. \<lbrakk>P' s'; (a, b) \<in> fst (g s'); snd (a, b) = s'\<rbrakk> \<Longrightarrow> \<exists>s'a. (a, s') \<in> fst (g s'a) \<and> P' s'a
 2. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> \<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> \<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>P' s'; \<forall>p\<in>fst (g s'). snd p = s'; \<exists>p\<in>fst (g s'). snd p = s'\<rbrakk> \<Longrightarrow> \<exists>rv s'a. (rv, s') \<in> fst (g s'a) \<and> P' s'a proof (prove)
goal:
No subgoals!