theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_rv_ex_pre_post:
  "\<And>sep_lift.
   (\<And>R. \<lbrace>\<lambda>s. \<exists>t'. ((P t' \<and>* R) and K(p' t')) (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. \<exists>t'. (( P t' \<and>* (\<lambda>s. (\<forall>x t.  p'' x t \<longrightarrow> (Q x t  \<longrightarrow>* R x t) (s )))) and K(p' t') ) (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 (rule_tac x=t' in exI, simp) 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. \<exists>t'. (P t' \<and>* R and K (p' t')) (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. \<exists>t'. (P t' \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s) and K (p' t')) (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. \<exists>t'. (P t' \<and>* R and K (p' t')) (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'. (P t' \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s) and K (p' t')) (sep_lift s)\<rbrakk> \<Longrightarrow> \<exists>t'. (P t' \<and>* ?R13 sep_lift and K (p' t')) (sep_lift s)
 2. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. \<exists>t'. (P t' \<and>* R and K (p' t')) (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 t'. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. \<exists>t'. (P t' \<and>* R) (sep_lift s) \<and> p' t'\<rbrace> f \<lbrace>\<lambda>x s. \<exists>t. (Q x t \<and>* R) (sep_lift s) \<and> p'' x t\<rbrace>; (P t' \<and>* (\<lambda>s. \<forall>x t. p'' x t \<longrightarrow> (Q x t \<longrightarrow>* R x t) s)) (sep_lift s); p' t'\<rbrakk> \<Longrightarrow> \<exists>t'. (P t' \<and>* ?R13 sep_lift) (sep_lift s) \<and> p' t'
 2. \<And>sep_lift rv s. \<lbrakk>\<And>R. \<lbrace>\<lambda>s. \<exists>t'. (P t' \<and>* R and K (p' t')) (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. \<exists>t'. (P t' \<and>* R and K (p' t')) (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>t'. (\<exists>x y. x ## y \<and> sep_lift s = x + y \<and> P t' x \<and> R y) \<and> p' t'\<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)