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> P' \<Longrightarrow>
  \<lbrace>(\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (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. \<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>, \<lbrace>E\<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>, \<lbrace>E\<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>, \<lbrace>E\<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>, \<lbrace>E\<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>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (P \<and>* (Q \<longrightarrow>* R)) (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. \<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>, \<lbrace>E\<rbrace>\<rbrakk> \<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>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>, \<lbrace>E\<rbrace>; (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> ?P'1 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>, \<lbrace>E\<rbrace>; ?Q'1 sep_lift rv s\<rbrakk> \<Longrightarrow> R (sep_lift s)
 4. \<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>, \<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>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>, \<lbrace>E\<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>, \<lbrace>E\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (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>, \<lbrace>E\<rbrace>; E rv s\<rbrakk> \<Longrightarrow> E rv s proof (prove)
goal (2 subgoals):
 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>, \<lbrace>E\<rbrace>; (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> R (sep_lift 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>, \<lbrace>E\<rbrace>; E rv s\<rbrakk> \<Longrightarrow> E rv s proof (prove)
goal:
No subgoals!