theory Extended_Separation_Algebra

lemma rewrite_sp:
  "(\<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s))  \<longleftrightarrow> (\<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) )" apply (rule iffI) apply (clarsimp) apply (erule_tac x="P -* R" in allE) apply (erule_tac x=s in allE) apply (drule mp) apply (erule (1) sep_snake_septraction) apply (assumption) apply (clarsimp) apply (erule_tac x="P \<leadsto>* R" in allE) apply (erule_tac x=s in allE) apply (clarsimp) apply (sep_cancel) apply (erule (1) sep_septraction_snake) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s)) = (\<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s)) proof (prove)
goal (2 subgoals):
 1. \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) \<Longrightarrow> \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s)
 2. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (2 subgoals):
 1. \<And>R s. \<lbrakk>\<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s); R s\<rbrakk> \<Longrightarrow> (Q \<and>* (P -* R)) (f s)
 2. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (2 subgoals):
 1. \<And>R s. \<lbrakk>R s; \<forall>s. (P \<leadsto>* P -* R) s \<longrightarrow> (Q \<and>* (P -* R)) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* (P -* R)) (f s)
 2. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (2 subgoals):
 1. \<And>R s. \<lbrakk>R s; (P \<leadsto>* P -* R) s \<longrightarrow> (Q \<and>* (P -* R)) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* (P -* R)) (f s)
 2. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (3 subgoals):
 1. \<And>R s. R s \<Longrightarrow> (P \<leadsto>* P -* R) s
 2. \<And>R s. \<lbrakk>R s; (Q \<and>* (P -* R)) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* (P -* R)) (f s)
 3. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (2 subgoals):
 1. \<And>R s. \<lbrakk>R s; (Q \<and>* (P -* R)) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* (P -* R)) (f s)
 2. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (1 subgoal):
 1. \<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s) \<Longrightarrow> \<forall>R s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (1 subgoal):
 1. \<And>R s. \<lbrakk>\<forall>R s. R s \<longrightarrow> (Q \<and>* (P -* R)) (f s); (P \<leadsto>* R) s\<rbrakk> \<Longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (1 subgoal):
 1. \<And>R s. \<lbrakk>(P \<leadsto>* R) s; \<forall>s. (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* (P -* (P \<leadsto>* R))) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (1 subgoal):
 1. \<And>R s. \<lbrakk>(P \<leadsto>* R) s; (P \<leadsto>* R) s \<longrightarrow> (Q \<and>* (P -* (P \<leadsto>* R))) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (1 subgoal):
 1. \<And>R s. \<lbrakk>(P \<leadsto>* R) s; (Q \<and>* (P -* (P \<leadsto>* R))) (f s)\<rbrakk> \<Longrightarrow> (Q \<and>* R) (f s) proof (prove)
goal (1 subgoal):
 1. \<And>R s sa. \<lbrakk>(P \<leadsto>* R) s; (P -* (P \<leadsto>* R)) sa\<rbrakk> \<Longrightarrow> R sa proof (prove)
goal:
No subgoals!