theory Separation_Algebra

lemma precise_distribute:
  "precise P = (\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P)))" proof (rule iffI) assume pp: "precise P" { fix Q R fix h hp hp' s { assume a: "((Q and R) \<and>* P) s" hence "((Q \<and>* P) and (R \<and>* P)) s" by (fastforce dest!: sep_conjD elim: sep_conjI) } moreover { assume qs: "(Q \<and>* P) s" and qr: "(R \<and>* P) s" from qs obtain x y where sxy: "s = x + y" and xy: "x ## y"
                           and x: "Q x" and y: "P y" by (fastforce dest!: sep_conjD) from qr obtain x' y' where sxy': "s = x' + y'" and xy': "x' ## y'"
                           and x': "R x'" and y': "P y'" by (fastforce dest!: sep_conjD) from sxy have ys: "y \<preceq> x + y" using xy by (fastforce simp: sep_substate_disj_add' sep_disj_commute) from sxy' have ys': "y' \<preceq> x' + y'" using xy' by (fastforce simp: sep_substate_disj_add' sep_disj_commute) from pp have yy: "y = y'" using sxy sxy' xy xy' y y' ys ys' by (fastforce simp: precise_def) hence "x = x'" using sxy sxy' xy xy' by (fastforce dest!: sep_add_cancelD) hence "((Q and R) \<and>* P) s" using sxy x x' yy y' xy' by (fastforce intro: sep_conjI) } ultimately have "((Q and R) \<and>* P) s = ((Q \<and>* P) and (R \<and>* P)) s" using pp by blast } thus "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" by blast next assume a: "\<forall>Q R. ((Q and R) \<and>* P) = ((Q \<and>* P) and (R \<and>* P))" thus "precise P" proof (clarsimp simp: precise_def) fix h hp hp' Q R assume hp: "hp \<preceq> h" and hp': "hp' \<preceq> h" and php: "P hp" and php': "P hp'" obtain z where hhp: "h = hp + z" and hpz: "hp ## z" using hp by (clarsimp simp: sep_substate_def) obtain z' where hhp': "h = hp' + z'" and hpz': "hp' ## z'" using hp' by (clarsimp simp: sep_substate_def) have h_eq: "z' + hp' = z + hp" using hhp hhp' hpz hpz' by (fastforce simp: sep_add_ac) from hhp hhp' a hpz hpz' h_eq have "\<forall>Q R. ((Q and R) \<and>* P) (z + hp) = ((Q \<and>* P) and (R \<and>* P)) (z' + hp')" by (fastforce simp: h_eq sep_add_ac sep_conj_commute) hence "(((=) z and (=) z') \<and>* P) (z + hp) =
           (((=) z \<and>* P) and ((=) z' \<and>* P)) (z' + hp')" by blast thus  "hp = hp'" using php php' hpz hpz' h_eq by (fastforce dest!: iffD2 cong: conj_cong
                    simp: sep_add_ac sep_add_cancel sep_conj_def) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. precise P = (\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)) proof (state)
goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
precise P

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
precise P

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (prove)
using this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s

goal (1 subgoal):
 1. (Q \<and>* P) s \<and> (R \<and>* P) s proof (state)
this:
(Q \<and>* P) s \<and> (R \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s \<Longrightarrow> (Q \<and>* P) s \<and> (R \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s \<Longrightarrow> (Q \<and>* P) s \<and> (R \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s \<Longrightarrow> (Q \<and>* P) s \<and> (R \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
(Q \<and>* P) s
(R \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (chain)
picking this:
(Q \<and>* P) s proof (prove)
using this:
(Q \<and>* P) s

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>s = x + y; x ## y; Q x; P y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
s = x + y
x ## y
Q x
P y

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (chain)
picking this:
(R \<and>* P) s proof (prove)
using this:
(R \<and>* P) s

goal (1 subgoal):
 1. (\<And>x' y'. \<lbrakk>s = x' + y'; x' ## y'; R x'; P y'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
s = x' + y'
x' ## y'
R x'
P y'

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (chain)
picking this:
s = x + y proof (prove)
using this:
s = x + y

goal (1 subgoal):
 1. y \<preceq> x + y proof (prove)
using this:
s = x + y
x ## y

goal (1 subgoal):
 1. y \<preceq> x + y proof (state)
this:
y \<preceq> x + y

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (chain)
picking this:
s = x' + y' proof (prove)
using this:
s = x' + y'

goal (1 subgoal):
 1. y' \<preceq> x' + y' proof (prove)
using this:
s = x' + y'
x' ## y'

goal (1 subgoal):
 1. y' \<preceq> x' + y' proof (state)
this:
y' \<preceq> x' + y'

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (chain)
picking this:
precise P proof (prove)
using this:
precise P

goal (1 subgoal):
 1. y = y' proof (prove)
using this:
precise P
s = x + y
s = x' + y'
x ## y
x' ## y'
P y
P y'
y \<preceq> x + y
y' \<preceq> x' + y'

goal (1 subgoal):
 1. y = y' proof (state)
this:
y = y'

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (prove)
using this:
y = y'

goal (1 subgoal):
 1. x = x' proof (prove)
using this:
y = y'
s = x + y
s = x' + y'
x ## y
x' ## y'

goal (1 subgoal):
 1. x = x' proof (state)
this:
x = x'

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (prove)
using this:
x = x'

goal (1 subgoal):
 1. ((\<lambda>s. Q s \<and> R s) \<and>* P) s proof (prove)
using this:
x = x'
s = x + y
Q x
R x'
y = y'
P y'
x' ## y'

goal (1 subgoal):
 1. ((\<lambda>s. Q s \<and> R s) \<and>* P) s proof (state)
this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
\<lbrakk>(Q \<and>* P) s; (R \<and>* P) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. Q s \<and> R s) \<and>* P) s

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (chain)
picking this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s \<Longrightarrow> (Q \<and>* P) s \<and> (R \<and>* P) s
\<lbrakk>(Q \<and>* P) s; (R \<and>* P) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. Q s \<and> R s) \<and>* P) s proof (prove)
using this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s \<Longrightarrow> (Q \<and>* P) s \<and> (R \<and>* P) s
\<lbrakk>(Q \<and>* P) s; (R \<and>* P) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. Q s \<and> R s) \<and>* P) s

goal (1 subgoal):
 1. ((\<lambda>s. Q s \<and> R s) \<and>* P) s = ((Q \<and>* P) s \<and> (R \<and>* P) s) proof (prove)
using this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s \<Longrightarrow> (Q \<and>* P) s \<and> (R \<and>* P) s
\<lbrakk>(Q \<and>* P) s; (R \<and>* P) s\<rbrakk> \<Longrightarrow> ((\<lambda>s. Q s \<and> R s) \<and>* P) s
precise P

goal (1 subgoal):
 1. ((\<lambda>s. Q s \<and> R s) \<and>* P) s = ((Q \<and>* P) s \<and> (R \<and>* P) s) proof (state)
this:
((\<lambda>s. Q s \<and> R s) \<and>* P) s = ((Q \<and>* P) s \<and> (R \<and>* P) s)

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
((\<lambda>s. ?Q2 s \<and> ?R2 s) \<and>* P) ?s2 = ((?Q2 \<and>* P) ?s2 \<and> (?R2 \<and>* P) ?s2)

goal (2 subgoals):
 1. precise P \<Longrightarrow> \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
 2. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (prove)
using this:
((\<lambda>s. ?Q2 s \<and> ?R2 s) \<and>* P) ?s2 = ((?Q2 \<and>* P) ?s2 \<and> (?R2 \<and>* P) ?s2)

goal (1 subgoal):
 1. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) proof (state)
this:
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)

goal (1 subgoal):
 1. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
goal (1 subgoal):
 1. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (state)
this:
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)

goal (1 subgoal):
 1. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s) \<Longrightarrow> precise P proof (prove)
using this:
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)

goal (1 subgoal):
 1. precise P proof (state)
goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (state)
goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (state)
this:
hp \<preceq> h
hp' \<preceq> h
P hp
P hp'

goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>h = hp + z; hp ## z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
hp \<preceq> h

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>h = hp + z; hp ## z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
h = hp + z
hp ## z

goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>h = hp' + z'; hp' ## z'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
hp' \<preceq> h

goal (1 subgoal):
 1. (\<And>z'. \<lbrakk>h = hp' + z'; hp' ## z'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
h = hp' + z'
hp' ## z'

goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
goal (1 subgoal):
 1. z' + hp' = z + hp proof (prove)
using this:
h = hp + z
h = hp' + z'
hp ## z
hp' ## z'

goal (1 subgoal):
 1. z' + hp' = z + hp proof (state)
this:
z' + hp' = z + hp

goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (chain)
picking this:
h = hp + z
h = hp' + z'
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
hp ## z
hp' ## z'
z' + hp' = z + hp proof (prove)
using this:
h = hp + z
h = hp' + z'
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s)
hp ## z
hp' ## z'
z' + hp' = z + hp

goal (1 subgoal):
 1. \<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) (z + hp) = ((Q \<and>* P) (z' + hp') \<and> (R \<and>* P) (z' + hp')) proof (state)
this:
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) (z + hp) = ((Q \<and>* P) (z' + hp') \<and> (R \<and>* P) (z' + hp'))

goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
using this:
\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) (z + hp) = ((Q \<and>* P) (z' + hp') \<and> (R \<and>* P) (z' + hp'))

goal (1 subgoal):
 1. ((\<lambda>s. z = s \<and> z' = s) \<and>* P) (z + hp) = (((=) z \<and>* P) (z' + hp') \<and> ((=) z' \<and>* P) (z' + hp')) proof (state)
this:
((\<lambda>s. z = s \<and> z' = s) \<and>* P) (z + hp) = (((=) z \<and>* P) (z' + hp') \<and> ((=) z' \<and>* P) (z' + hp'))

goal (1 subgoal):
 1. \<And>h hp hp'. \<lbrakk>\<forall>Q R. ((\<lambda>s. Q s \<and> R s) \<and>* P) = (\<lambda>s. (Q \<and>* P) s \<and> (R \<and>* P) s); hp \<preceq> h; P hp; hp' \<preceq> h; P hp'\<rbrakk> \<Longrightarrow> hp = hp' proof (prove)
using this:
((\<lambda>s. z = s \<and> z' = s) \<and>* P) (z + hp) = (((=) z \<and>* P) (z' + hp') \<and> ((=) z' \<and>* P) (z' + hp'))

goal (1 subgoal):
 1. hp = hp' proof (prove)
using this:
((\<lambda>s. z = s \<and> z' = s) \<and>* P) (z + hp) = (((=) z \<and>* P) (z' + hp') \<and> ((=) z' \<and>* P) (z' + hp'))
P hp
P hp'
hp ## z
hp' ## z'
z' + hp' = z + hp

goal (1 subgoal):
 1. hp = hp' proof (state)
this:
hp = hp'

goal:
No subgoals! proof (state)
this:
precise P

goal:
No subgoals!