theory Separation_Algebra

lemma sep_conj_assoc:
  "((P ** Q) ** R) = (P ** Q ** R)" (is "?lhs = ?rhs") proof (rule ext, rule iffI) fix h assume a: "?lhs h" then obtain x y z where "P x" and "Q y" and "R z"
                      and "x ## y" and "x ## z" and "y ## z" and "x + y ## z"
                      and "h = x + y + z" by (auto dest!: sep_conjD dest: sep_add_disjD) moreover then have "x ## y + z" by (simp add: sep_disj_add) ultimately show "?rhs h" by (auto simp: sep_add_ac intro!: sep_conjI) next fix h assume a: "?rhs h" then obtain x y z where "P x" and "Q y" and "R z"
                      and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
                      and "h = x + y + z" by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD) thus "?lhs h" by (metis sep_conj_def sep_disj_addI1) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<and>* Q) \<and>* R) = (P \<and>* Q \<and>* R) proof (state)
goal (2 subgoals):
 1. \<And>x. ((P \<and>* Q) \<and>* R) x \<Longrightarrow> (P \<and>* Q \<and>* R) x
 2. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (state)
goal (2 subgoals):
 1. \<And>x. ((P \<and>* Q) \<and>* R) x \<Longrightarrow> (P \<and>* Q \<and>* R) x
 2. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (state)
this:
((P \<and>* Q) \<and>* R) h

goal (2 subgoals):
 1. \<And>x. ((P \<and>* Q) \<and>* R) x \<Longrightarrow> (P \<and>* Q \<and>* R) x
 2. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (chain)
picking this:
((P \<and>* Q) \<and>* R) h proof (prove)
using this:
((P \<and>* Q) \<and>* R) h

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

goal (2 subgoals):
 1. \<And>x. ((P \<and>* Q) \<and>* R) x \<Longrightarrow> (P \<and>* Q \<and>* R) x
 2. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (state)
this:
P x
Q y
R z
x ## y
x ## z
y ## z
x + y ## z
h = x + y + z

goal (2 subgoals):
 1. \<And>x. ((P \<and>* Q) \<and>* R) x \<Longrightarrow> (P \<and>* Q \<and>* R) x
 2. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (chain)
picking this:
P x
Q y
R z
x ## y
x ## z
y ## z
x + y ## z
h = x + y + z proof (prove)
using this:
P x
Q y
R z
x ## y
x ## z
y ## z
x + y ## z
h = x + y + z

goal (1 subgoal):
 1. x ## y + z proof (state)
this:
x ## y + z

goal (2 subgoals):
 1. \<And>x. ((P \<and>* Q) \<and>* R) x \<Longrightarrow> (P \<and>* Q \<and>* R) x
 2. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (chain)
picking this:
P x
Q y
R z
x ## y
x ## z
y ## z
x + y ## z
h = x + y + z
x ## y + z proof (prove)
using this:
P x
Q y
R z
x ## y
x ## z
y ## z
x + y ## z
h = x + y + z
x ## y + z

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

goal (1 subgoal):
 1. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (state)
goal (1 subgoal):
 1. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (state)
goal (1 subgoal):
 1. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (state)
this:
(P \<and>* Q \<and>* R) h

goal (1 subgoal):
 1. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (chain)
picking this:
(P \<and>* Q \<and>* R) h proof (prove)
using this:
(P \<and>* Q \<and>* R) h

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

goal (1 subgoal):
 1. \<And>x. (P \<and>* Q \<and>* R) x \<Longrightarrow> ((P \<and>* Q) \<and>* R) x proof (prove)
using this:
P x
Q y
R z
x ## y
x ## z
y ## z
x ## y + z
h = x + y + z

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

goal:
No subgoals!