theory Hoare_Sep_Tactics

lemma strong_sep_impl_sep_wpE:
"\<And>sep_lift. (\<And>R. \<lbrace>(\<lambda>s. (P \<and>* R) (sep_lift s)) \<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>, \<lbrace>E\<rbrace>) \<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 (simp add: valid_def split_def validE_def) apply (rule allI) apply (rule impI) apply (erule_tac x=s in allE) apply (erule impE) apply (sep_cancel)+ apply (rule ballI) apply (erule_tac x="x" in ballE) apply (clarsimp split: sum.splits) apply (sep_solve) apply (clarsimp split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift. (\<And>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>, \<lbrace>E\<rbrace>) \<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. \<forall>R. \<lbrace>\<lambda>s. (P \<and>* R) (sep_lift s)\<rbrace> f \<lbrace>\<lambda>_ s. (Q \<and>* R) (sep_lift s)\<rbrace>, \<lbrace>E\<rbrace> \<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. \<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>, \<lbrace>E\<rbrace> \<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. \<forall>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<longrightarrow> (\<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x))) \<Longrightarrow> \<forall>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<longrightarrow> (\<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x))) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s. \<forall>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<longrightarrow> (\<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x))) \<Longrightarrow> (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<longrightarrow> (\<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x))) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s. \<lbrakk>\<forall>s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<longrightarrow> (\<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x))); (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<longrightarrow> (\<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x)))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s. (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s) \<Longrightarrow> (P \<and>* (Q \<longrightarrow>* R)) (sep_lift s)
 2. \<And>sep_lift s. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s x. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); \<forall>x\<in>fst (f s). case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x)); x \<in> fst (f s)\<rbrakk> \<Longrightarrow> case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s x. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); x \<in> fst (f s); case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift (snd x))\<rbrakk> \<Longrightarrow> case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x))
 2. \<And>sep_lift s x. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); x \<in> fst (f s); x \<notin> fst (f s)\<rbrakk> \<Longrightarrow> case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (2 subgoals):
 1. \<And>sep_lift s b x2. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); (Inr x2, b) \<in> fst (f s); (Q \<and>* (Q \<longrightarrow>* R)) (sep_lift b)\<rbrakk> \<Longrightarrow> R (sep_lift b)
 2. \<And>sep_lift s x. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); x \<in> fst (f s); x \<notin> fst (f s)\<rbrakk> \<Longrightarrow> case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal (1 subgoal):
 1. \<And>sep_lift s x. \<lbrakk>(P \<and>* (Q \<longrightarrow>* R)) (sep_lift s); x \<in> fst (f s); x \<notin> fst (f s)\<rbrakk> \<Longrightarrow> case fst x of Inl e \<Rightarrow> E e (snd x) | Inr r \<Rightarrow> R (sep_lift (snd x)) proof (prove)
goal:
No subgoals!