theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_rv_ex_post:
    "\<And>sep_lift.
     (\<And>R. \<lbrace>\<lambda>s. ((P \<and>* R) and K(p')) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. ((Q x t  \<and>* R) and K (p'' x t)) (sep_lift s)\<rbrace>) \<Longrightarrow>
      \<lbrace>\<lambda>s.  (( P \<and>* (\<lambda>s. (\<forall>x t.  p'' x t \<longrightarrow> (Q x t  \<longrightarrow>* R x t) (s )))) and K(p') ) (sep_lift s) \<rbrace> f \<lbrace>\<lambda>rv s . \<exists>t. (R rv t) (sep_lift s) \<rbrace>" apply (rule hoare_chain, assumption)+ apply (clarsimp) apply (sep_cancel) apply (clarsimp simp: sep_conj_def sep_impl_def) by (metis (full_types) sep_add_commute sep_disj_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. (\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R and K (p'' x t)) (sep_lift s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s) and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>t. R rv t (sep_lift s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R and K (p'' x t)) (sep_lift s)\<rbrace>; (P \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s) and K p') (sep_lift s)\<rbrakk> \<Longrightarrow> (P \<and>* ?R13 sep_lift and K p') (sep_lift s)
 2. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R and K (p'' x t)) (sep_lift s)\<rbrace>; \<exists>t. (Q rv t \<and>* ?R13 sep_lift and K (p'' rv t)) (sep_lift s)\<rbrakk> \<Longrightarrow> \<exists>t. R rv t (sep_lift s) proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R) (sep_lift s) \<and> p'' x t\<rbrace>; (P \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s)) (sep_lift s); p'\<rbrakk> \<Longrightarrow> (P \<and>* ?R13 sep_lift) (sep_lift s)
 2. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R and K (p'' x t)) (sep_lift s)\<rbrace>; \<exists>t. (Q rv t \<and>* ?R13 sep_lift and K (p'' rv t)) (sep_lift s)\<rbrakk> \<Longrightarrow> \<exists>t. R rv t (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (P \<and>* R and K p') (sep_lift s)\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R and K (p'' x t)) (sep_lift s)\<rbrace>; \<exists>t. (Q rv t \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s) and K (p'' rv t)) (sep_lift s)\<rbrakk> \<Longrightarrow> \<exists>t. R rv t (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s t x y. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. (\<exists>x y. x ## y \<and> sep_lift s = x + y \<and> P x \<and> R y) \<and> p'\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (\<exists>xa y. xa ## y \<and> sep_lift s = xa + y \<and> Q x t xa \<and> R y) \<and> p'' x t\<rbrace>; p'' rv t; x ## y; sep_lift s = x + y; Q rv t x; \<forall>x t. p'' x t \<longrightarrow> (\<forall>h'. y ## h' \<and> Q x t h' \<longrightarrow> R x t (y + h'))\<rbrakk> \<Longrightarrow> \<exists>t. R rv t (x + y)