theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_side'':
 "\<And>sep_lift.
  (\<And>R. \<lbrace>(\<lambda>s. ((P \<and>* R) and K P')  (sep_lift s))\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>) \<Longrightarrow>
  \<lbrace>(\<lambda>s. ((P \<and>* (Q \<longrightarrow>* R)) and K (P')) (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 (sep_solve) done

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