theory Trace_More_VCG

lemma other_hoare_in_monad_post:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<forall>(v, s) \<in> mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace>" proof - have P: "\<And>v s. (F v = v) \<and> (v, s) \<in> mres (fn s) \<Longrightarrow> (F v, s) \<in> mres (fn s)" by simp show ?thesis apply (rule hoare_post_imp [OF P], assumption) apply (rule hoare_pre_imp) defer apply (rule hoare_vcg_conj_lift) apply (rule univ_get_wp [OF x]) apply (rule hoare_in_monad_post [OF x]) apply clarsimp apply (drule bspec, assumption, simp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(v, s)\<in>mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(v, s)\<in>mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>v s. F v = v \<and> (v, s) \<in> mres (fn s) \<Longrightarrow> (F v, s) \<in> mres (fn s) proof (state)
this:
F ?v = ?v \<and> (?v, ?s) \<in> mres (fn ?s) \<Longrightarrow> (F ?v, ?s) \<in> mres (fn ?s)

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(v, s)\<in>mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(v, s)\<in>mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(v, s)\<in>mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. F v = v \<and> (v, s') \<in> mres (fn s')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<forall>(v, s)\<in>mres (fn s). F v = v \<Longrightarrow> ?Q4 s
 2. \<lbrace>?Q4\<rbrace> fn \<lbrace>\<lambda>v s'. F v = v \<and> (v, s') \<in> mres (fn s')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> fn \<lbrace>\<lambda>v s'. F v = v \<and> (v, s') \<in> mres (fn s')\<rbrace>
 2. \<And>s. \<forall>(v, s)\<in>mres (fn s). F v = v \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P7\<rbrace> fn \<lbrace>\<lambda>rv s. F rv = rv\<rbrace>
 2. \<lbrace>?P'7\<rbrace> fn \<lbrace>\<lambda>rv s. (rv, s) \<in> mres (fn s)\<rbrace>
 3. \<And>s. \<forall>(v, s)\<in>mres (fn s). F v = v \<Longrightarrow> ?P7 s \<and> ?P'7 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'7\<rbrace> fn \<lbrace>\<lambda>rv s. (rv, s) \<in> mres (fn s)\<rbrace>
 2. \<And>s. \<forall>(v, s)\<in>mres (fn s). F v = v \<Longrightarrow> (\<forall>(rv, s')\<in>mres (fn s). s = s' \<longrightarrow> F rv = rv) \<and> ?P'7 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>(v, s)\<in>mres (fn s). F v = v \<Longrightarrow> (\<forall>(rv, s')\<in>mres (fn s). s = s' \<longrightarrow> F rv = rv) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>mres (fn b). case x of (v, s) \<Rightarrow> F v = v; (a, b) \<in> mres (fn b)\<rbrakk> \<Longrightarrow> F a = a proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. \<forall>(v, s)\<in>mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace>

goal:
No subgoals!