theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wp_sideE':
"\<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>, \<lbrace>E\<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>, \<lbrace>E\<rbrace>" apply (atomize) apply (erule_tac x="(Q \<longrightarrow>* R)" in allE) apply (rule hoare_chainE) 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) (sep_lift s)) and K P'\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>, \<lbrace>E\<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>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<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>, \<lbrace>E\<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>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. \<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>, \<lbrace>E\<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>, \<lbrace>E\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>sep_lift. \<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>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>?P'1 sep_lift\<rbrace> f \<lbrace>?Q'1 sep_lift\<rbrace>, \<lbrace>?E'1 sep_lift\<rbrace>
 2. \<And>sep_lift s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; (P \<and>* (Q \<longrightarrow>* R) and K P') (sep_lift s)\<rbrakk> \<Longrightarrow> ?P'1 sep_lift s
 3. \<And>sep_lift rv s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; ?Q'1 sep_lift rv s\<rbrakk> \<Longrightarrow> R (sep_lift s)
 4. \<And>sep_lift rv s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; ?E'1 sep_lift rv s\<rbrakk> \<Longrightarrow> E rv s proof (prove)
goal (3 subgoals):
 1. \<And>sep_lift s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; (P \<and>* (Q \<longrightarrow>* R) and K P') (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>\<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>, \<lbrace>E\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s)
 3. \<And>sep_lift rv s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; E rv s\<rbrakk> \<Longrightarrow> E rv s proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift rv s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift s)
 2. \<And>sep_lift rv s. \<lbrakk>\<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>, \<lbrace>E\<rbrace>; E rv s\<rbrakk> \<Longrightarrow> E rv s proof (prove)
goal:
No subgoals!