theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_side:
 "\<And>sep_lift.
  (\<And>R. \<lbrace>(\<lambda>s. (P \<and>* R) (sep_lift s)) and K (P')\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow> P' \<Longrightarrow>
  \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) \<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace>" apply (atomize) apply (erule_tac x="(\<lambda>s. (Q \<longrightarrow>* R) s)" in allE) apply (rule hoare_chain) apply (assumption) apply (clarsimp) apply (clarsimp)+ apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<lbrakk>\<And>R. \<lbrace>(\<lambda>s. (P \<and>* R) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>; P'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<lbrakk>\<forall>R. \<lbrace>(\<lambda>s. (P \<and>* R) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>; P'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. R (sep_lift s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sep_lift. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P1 sep_lift\<rbrace> f \<lbrace>?Q1 sep_lift\<rbrace>
 2. \<And>sep_lift s. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?P1 sep_lift s
 3. \<And>sep_lift rv s. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; ?Q1 sep_lift rv s\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ((\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P') s
 2. \<And>sep_lift rv s. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift rv s. \<lbrakk>P'; \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s. \<lbrakk>P'; \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s) proof (prove)
goal:
No subgoals!