[STATEMENT]
lemma preservation_of_binary_predicates_and_closures:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  assumes preservation: "rel_preserves_binary_pred Rel Pred"
  shows "rel_preserves_binary_pred (Rel\<^sup>=) Pred"
    and "rel_preserves_binary_pred (Rel\<^sup>+) Pred"
    and "rel_preserves_binary_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_preserves_binary_pred (Rel\<^sup>=) Pred &&& rel_preserves_binary_pred (Rel\<^sup>+) Pred &&& rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_preserves_binary_pred (Rel\<^sup>=) Pred
 2. rel_preserves_binary_pred (Rel\<^sup>+) Pred
 3. rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from preservation
[PROOF STATE]
proof (chain)
picking this:
rel_preserves_binary_pred Rel Pred
[PROOF STEP]
show A: "rel_preserves_binary_pred (Rel\<^sup>=) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_preserves_binary_pred Rel Pred

goal (1 subgoal):
 1. rel_preserves_binary_pred (Rel\<^sup>=) Pred
[PROOF STEP]
by (auto simp add: refl)
[PROOF STATE]
proof (state)
this:
rel_preserves_binary_pred (Rel\<^sup>=) Pred

goal (2 subgoals):
 1. rel_preserves_binary_pred (Rel\<^sup>+) Pred
 2. rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
have B: "\<And>Rel. rel_preserves_binary_pred Rel Pred
           \<Longrightarrow> rel_preserves_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_preserves_binary_pred Rel Pred \<Longrightarrow> rel_preserves_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b x. rel_preserves_binary_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
fix Rel a b x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b x. rel_preserves_binary_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
assume "(a, b) \<in> Rel\<^sup>+" and "rel_preserves_binary_pred Rel Pred" and "Pred a x"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel\<^sup>+
rel_preserves_binary_pred Rel Pred
Pred a x

goal (1 subgoal):
 1. \<And>Rel a b x. rel_preserves_binary_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
thus "Pred b x"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel\<^sup>+
rel_preserves_binary_pred Rel Pred
Pred a x

goal (1 subgoal):
 1. Pred b x
[PROOF STEP]
by (induct, blast+)
[PROOF STATE]
proof (state)
this:
Pred b x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_preserves_binary_pred ?Rel Pred \<Longrightarrow> rel_preserves_binary_pred (?Rel\<^sup>+) Pred

goal (2 subgoals):
 1. rel_preserves_binary_pred (Rel\<^sup>+) Pred
 2. rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
with preservation
[PROOF STATE]
proof (chain)
picking this:
rel_preserves_binary_pred Rel Pred
rel_preserves_binary_pred ?Rel Pred \<Longrightarrow> rel_preserves_binary_pred (?Rel\<^sup>+) Pred
[PROOF STEP]
show "rel_preserves_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_preserves_binary_pred Rel Pred
rel_preserves_binary_pred ?Rel Pred \<Longrightarrow> rel_preserves_binary_pred (?Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_preserves_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_preserves_binary_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from preservation A B[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_preserves_binary_pred Rel Pred
rel_preserves_binary_pred (Rel\<^sup>=) Pred
rel_preserves_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_preserves_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred
[PROOF STEP]
show "rel_preserves_binary_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_preserves_binary_pred Rel Pred
rel_preserves_binary_pred (Rel\<^sup>=) Pred
rel_preserves_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_preserves_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred

goal (1 subgoal):
 1. rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
using trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
rel_preserves_binary_pred Rel Pred
rel_preserves_binary_pred (Rel\<^sup>=) Pred
rel_preserves_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_preserves_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. rel_preserves_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
rel_preserves_binary_pred (Rel\<^sup>*) Pred

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflection_and_closures:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> bool"
  assumes reflection: "rel_reflects_pred Rel Pred"
  shows "rel_reflects_pred (Rel\<^sup>=) Pred"
    and "rel_reflects_pred (Rel\<^sup>+) Pred"
    and "rel_reflects_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_reflects_pred (Rel\<^sup>=) Pred &&& rel_reflects_pred (Rel\<^sup>+) Pred &&& rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_reflects_pred (Rel\<^sup>=) Pred
 2. rel_reflects_pred (Rel\<^sup>+) Pred
 3. rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from reflection
[PROOF STATE]
proof (chain)
picking this:
rel_reflects_pred Rel Pred
[PROOF STEP]
show A: "rel_reflects_pred (Rel\<^sup>=) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_reflects_pred Rel Pred

goal (1 subgoal):
 1. rel_reflects_pred (Rel\<^sup>=) Pred
[PROOF STEP]
by (auto simp add: refl)
[PROOF STATE]
proof (state)
this:
rel_reflects_pred (Rel\<^sup>=) Pred

goal (2 subgoals):
 1. rel_reflects_pred (Rel\<^sup>+) Pred
 2. rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
have B: "\<And>Rel. rel_reflects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_reflects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b. rel_reflects_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
fix Rel a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b. rel_reflects_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
assume "(a, b) \<in> Rel\<^sup>+" and "rel_reflects_pred Rel Pred" and "Pred b"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel\<^sup>+
rel_reflects_pred Rel Pred
Pred b

goal (1 subgoal):
 1. \<And>Rel a b. rel_reflects_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
thus "Pred a"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel\<^sup>+
rel_reflects_pred Rel Pred
Pred b

goal (1 subgoal):
 1. Pred a
[PROOF STEP]
by (induct, blast+)
[PROOF STATE]
proof (state)
this:
Pred a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_reflects_pred ?Rel Pred \<Longrightarrow> rel_reflects_pred (?Rel\<^sup>+) Pred

goal (2 subgoals):
 1. rel_reflects_pred (Rel\<^sup>+) Pred
 2. rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
with reflection
[PROOF STATE]
proof (chain)
picking this:
rel_reflects_pred Rel Pred
rel_reflects_pred ?Rel Pred \<Longrightarrow> rel_reflects_pred (?Rel\<^sup>+) Pred
[PROOF STEP]
show "rel_reflects_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_reflects_pred Rel Pred
rel_reflects_pred ?Rel Pred \<Longrightarrow> rel_reflects_pred (?Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_reflects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_reflects_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from reflection A B[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_reflects_pred Rel Pred
rel_reflects_pred (Rel\<^sup>=) Pred
rel_reflects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_reflects_pred ((Rel\<^sup>=)\<^sup>+) Pred
[PROOF STEP]
show "rel_reflects_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_reflects_pred Rel Pred
rel_reflects_pred (Rel\<^sup>=) Pred
rel_reflects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_reflects_pred ((Rel\<^sup>=)\<^sup>+) Pred

goal (1 subgoal):
 1. rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
using trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
rel_reflects_pred Rel Pred
rel_reflects_pred (Rel\<^sup>=) Pred
rel_reflects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_reflects_pred ((Rel\<^sup>=)\<^sup>+) Pred
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. rel_reflects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
rel_reflects_pred (Rel\<^sup>*) Pred

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reflection_of_binary_predicates_and_closures:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  assumes reflection: "rel_reflects_binary_pred Rel Pred"
  shows "rel_reflects_binary_pred (Rel\<^sup>=) Pred"
    and "rel_reflects_binary_pred (Rel\<^sup>+) Pred"
    and "rel_reflects_binary_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_reflects_binary_pred (Rel\<^sup>=) Pred &&& rel_reflects_binary_pred (Rel\<^sup>+) Pred &&& rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. rel_reflects_binary_pred (Rel\<^sup>=) Pred
 2. rel_reflects_binary_pred (Rel\<^sup>+) Pred
 3. rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from reflection
[PROOF STATE]
proof (chain)
picking this:
rel_reflects_binary_pred Rel Pred
[PROOF STEP]
show A: "rel_reflects_binary_pred (Rel\<^sup>=) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_reflects_binary_pred Rel Pred

goal (1 subgoal):
 1. rel_reflects_binary_pred (Rel\<^sup>=) Pred
[PROOF STEP]
by (auto simp add: refl)
[PROOF STATE]
proof (state)
this:
rel_reflects_binary_pred (Rel\<^sup>=) Pred

goal (2 subgoals):
 1. rel_reflects_binary_pred (Rel\<^sup>+) Pred
 2. rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
have B: "\<And>Rel. rel_reflects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_reflects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b x. rel_reflects_binary_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
fix Rel a b x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel a b x. rel_reflects_binary_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
assume "(a, b) \<in> Rel\<^sup>+" and "rel_reflects_binary_pred Rel Pred" and "Pred b x"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel\<^sup>+
rel_reflects_binary_pred Rel Pred
Pred b x

goal (1 subgoal):
 1. \<And>Rel a b x. rel_reflects_binary_pred Rel Pred \<and> (a, b) \<in> Rel\<^sup>+ \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
thus "Pred a x"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel\<^sup>+
rel_reflects_binary_pred Rel Pred
Pred b x

goal (1 subgoal):
 1. Pred a x
[PROOF STEP]
by (induct, blast+)
[PROOF STATE]
proof (state)
this:
Pred a x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_reflects_binary_pred ?Rel Pred \<Longrightarrow> rel_reflects_binary_pred (?Rel\<^sup>+) Pred

goal (2 subgoals):
 1. rel_reflects_binary_pred (Rel\<^sup>+) Pred
 2. rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
with reflection
[PROOF STATE]
proof (chain)
picking this:
rel_reflects_binary_pred Rel Pred
rel_reflects_binary_pred ?Rel Pred \<Longrightarrow> rel_reflects_binary_pred (?Rel\<^sup>+) Pred
[PROOF STEP]
show "rel_reflects_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_reflects_binary_pred Rel Pred
rel_reflects_binary_pred ?Rel Pred \<Longrightarrow> rel_reflects_binary_pred (?Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_reflects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_reflects_binary_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
from reflection A B[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_reflects_binary_pred Rel Pred
rel_reflects_binary_pred (Rel\<^sup>=) Pred
rel_reflects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_reflects_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred
[PROOF STEP]
show "rel_reflects_binary_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_reflects_binary_pred Rel Pred
rel_reflects_binary_pred (Rel\<^sup>=) Pred
rel_reflects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_reflects_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred

goal (1 subgoal):
 1. rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
using trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
rel_reflects_binary_pred Rel Pred
rel_reflects_binary_pred (Rel\<^sup>=) Pred
rel_reflects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_reflects_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. rel_reflects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
rel_reflects_binary_pred (Rel\<^sup>*) Pred

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma respection_and_closures:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> bool"
  assumes respection: "rel_respects_pred Rel Pred"
  shows "rel_respects_pred (Rel\<^sup>=) Pred"
    and "rel_respects_pred (symcl Rel) Pred"
    and "rel_respects_pred (Rel\<^sup>+) Pred"
    and "rel_respects_pred (symcl (Rel\<^sup>=)) Pred"
    and "rel_respects_pred (Rel\<^sup>*) Pred"
    and "rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_respects_pred (Rel\<^sup>=) Pred &&& rel_respects_pred (symcl Rel) Pred &&& rel_respects_pred (Rel\<^sup>+) Pred) &&& rel_respects_pred (symcl (Rel\<^sup>=)) Pred &&& rel_respects_pred (Rel\<^sup>*) Pred &&& rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. rel_respects_pred (Rel\<^sup>=) Pred
 2. rel_respects_pred (symcl Rel) Pred
 3. rel_respects_pred (Rel\<^sup>+) Pred
 4. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
 5. rel_respects_pred (Rel\<^sup>*) Pred
 6. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from respection
[PROOF STATE]
proof (chain)
picking this:
rel_respects_pred Rel Pred
[PROOF STEP]
show A: "rel_respects_pred (Rel\<^sup>=) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred Rel Pred

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>=) Pred
[PROOF STEP]
using preservation_and_closures(1)[where Rel="Rel" and Pred="Pred"]
            reflection_and_closures(1)[where Rel="Rel" and Pred="Pred"]
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred Rel Pred
rel_preserves_pred Rel Pred \<Longrightarrow> rel_preserves_pred (Rel\<^sup>=) Pred
rel_reflects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (Rel\<^sup>=) Pred

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>=) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_pred (Rel\<^sup>=) Pred

goal (5 subgoals):
 1. rel_respects_pred (symcl Rel) Pred
 2. rel_respects_pred (Rel\<^sup>+) Pred
 3. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
 4. rel_respects_pred (Rel\<^sup>*) Pred
 5. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
have B: "\<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (symcl Rel) Pred
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_preserves_pred (symcl Rel) Pred
 2. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
fix Rel
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_preserves_pred (symcl Rel) Pred
 2. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
assume B1: "rel_respects_pred Rel Pred"
[PROOF STATE]
proof (state)
this:
rel_respects_pred Rel Pred

goal (2 subgoals):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_preserves_pred (symcl Rel) Pred
 2. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
show "rel_preserves_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_preserves_pred (symcl Rel) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
assume "(a, b) \<in> symcl Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
hence "(a, b) \<in> Rel \<or> (b, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<or> (b, a) \<in> Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
assume "Pred a"
[PROOF STATE]
proof (state)
this:
Pred a

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred a \<Longrightarrow> Pred b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred a
[PROOF STEP]
show "Pred b"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred a

goal (1 subgoal):
 1. Pred b
[PROOF STEP]
using B1
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred a
rel_respects_pred Rel Pred

goal (1 subgoal):
 1. Pred b
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Pred b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_preserves_pred (symcl Rel) Pred

goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
fix Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> bool"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
assume B2: "rel_respects_pred Rel Pred"
[PROOF STATE]
proof (state)
this:
rel_respects_pred Rel Pred

goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
show "rel_reflects_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_reflects_pred (symcl Rel) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
assume "(a, b) \<in> symcl Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
hence "(a, b) \<in> Rel \<or> (b, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<or> (b, a) \<in> Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
assume "Pred b"
[PROOF STATE]
proof (state)
this:
Pred b

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> symcl Rel \<and> Pred b \<Longrightarrow> Pred a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred b
[PROOF STEP]
show "Pred a"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred b

goal (1 subgoal):
 1. Pred a
[PROOF STEP]
using B2
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred b
rel_respects_pred Rel Pred

goal (1 subgoal):
 1. Pred a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Pred a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_reflects_pred (symcl Rel) Pred

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_respects_pred ?Rel Pred \<Longrightarrow> rel_respects_pred (symcl ?Rel) Pred

goal (5 subgoals):
 1. rel_respects_pred (symcl Rel) Pred
 2. rel_respects_pred (Rel\<^sup>+) Pred
 3. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
 4. rel_respects_pred (Rel\<^sup>*) Pred
 5. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from respection B[where Rel="Rel"]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_pred Rel Pred
rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (symcl Rel) Pred
[PROOF STEP]
show "rel_respects_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred Rel Pred
rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (symcl Rel) Pred

goal (1 subgoal):
 1. rel_respects_pred (symcl Rel) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_pred (symcl Rel) Pred

goal (4 subgoals):
 1. rel_respects_pred (Rel\<^sup>+) Pred
 2. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
 3. rel_respects_pred (Rel\<^sup>*) Pred
 4. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
have C: "\<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
fix Rel
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
assume "rel_respects_pred Rel Pred"
[PROOF STATE]
proof (state)
this:
rel_respects_pred Rel Pred

goal (1 subgoal):
 1. \<And>Rel. rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
thus "rel_respects_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred Rel Pred

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
using preservation_and_closures(2)[where Rel="Rel" and Pred="Pred"]
              reflection_and_closures(2)[where Rel="Rel" and Pred="Pred"]
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred Rel Pred
rel_preserves_pred Rel Pred \<Longrightarrow> rel_preserves_pred (Rel\<^sup>+) Pred
rel_reflects_pred Rel Pred \<Longrightarrow> rel_reflects_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_pred (Rel\<^sup>+) Pred

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_respects_pred ?Rel Pred \<Longrightarrow> rel_respects_pred (?Rel\<^sup>+) Pred

goal (4 subgoals):
 1. rel_respects_pred (Rel\<^sup>+) Pred
 2. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
 3. rel_respects_pred (Rel\<^sup>*) Pred
 4. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from respection C[where Rel="Rel"]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_pred Rel Pred
rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
show "rel_respects_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred Rel Pred
rel_respects_pred Rel Pred \<Longrightarrow> rel_respects_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_pred (Rel\<^sup>+) Pred

goal (3 subgoals):
 1. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
 2. rel_respects_pred (Rel\<^sup>*) Pred
 3. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from A B[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred (symcl (Rel\<^sup>=)) Pred
[PROOF STEP]
show "rel_respects_pred (symcl (Rel\<^sup>=)) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred (symcl (Rel\<^sup>=)) Pred

goal (1 subgoal):
 1. rel_respects_pred (symcl (Rel\<^sup>=)) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_pred (symcl (Rel\<^sup>=)) Pred

goal (2 subgoals):
 1. rel_respects_pred (Rel\<^sup>*) Pred
 2. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from A C[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred ((Rel\<^sup>=)\<^sup>+) Pred
[PROOF STEP]
show "rel_respects_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred ((Rel\<^sup>=)\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
using trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred ((Rel\<^sup>=)\<^sup>+) Pred
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. rel_respects_pred (Rel\<^sup>*) Pred
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
rel_respects_pred (Rel\<^sup>*) Pred

goal (1 subgoal):
 1. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from A B[where Rel="Rel\<^sup>="] C[where Rel="symcl (Rel\<^sup>=)"]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred (symcl (Rel\<^sup>=)) Pred
rel_respects_pred (symcl (Rel\<^sup>=)) Pred \<Longrightarrow> rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
show "rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_pred (Rel\<^sup>=) Pred
rel_respects_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_pred (symcl (Rel\<^sup>=)) Pred
rel_respects_pred (symcl (Rel\<^sup>=)) Pred \<Longrightarrow> rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma respection_of_binary_predicates_and_closures:
  fixes Rel  :: "('a \<times> 'a) set"
    and Pred :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  assumes respection: "rel_respects_binary_pred Rel Pred"
  shows "rel_respects_binary_pred (Rel\<^sup>=) Pred"
    and "rel_respects_binary_pred (symcl Rel) Pred"
    and "rel_respects_binary_pred (Rel\<^sup>+) Pred"
    and "rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred"
    and "rel_respects_binary_pred (Rel\<^sup>*) Pred"
    and "rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_respects_binary_pred (Rel\<^sup>=) Pred &&& rel_respects_binary_pred (symcl Rel) Pred &&& rel_respects_binary_pred (Rel\<^sup>+) Pred) &&& rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred &&& rel_respects_binary_pred (Rel\<^sup>*) Pred &&& rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. rel_respects_binary_pred (Rel\<^sup>=) Pred
 2. rel_respects_binary_pred (symcl Rel) Pred
 3. rel_respects_binary_pred (Rel\<^sup>+) Pred
 4. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
 5. rel_respects_binary_pred (Rel\<^sup>*) Pred
 6. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from respection
[PROOF STATE]
proof (chain)
picking this:
rel_respects_binary_pred Rel Pred
[PROOF STEP]
show A: "rel_respects_binary_pred (Rel\<^sup>=) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred Rel Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>=) Pred
[PROOF STEP]
using preservation_of_binary_predicates_and_closures(1)[where Rel="Rel" and Pred="Pred"]
            reflection_of_binary_predicates_and_closures(1)[where Rel="Rel" and Pred="Pred"]
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred Rel Pred
rel_preserves_binary_pred Rel Pred \<Longrightarrow> rel_preserves_binary_pred (Rel\<^sup>=) Pred
rel_reflects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (Rel\<^sup>=) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>=) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred (Rel\<^sup>=) Pred

goal (5 subgoals):
 1. rel_respects_binary_pred (symcl Rel) Pred
 2. rel_respects_binary_pred (Rel\<^sup>+) Pred
 3. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
 4. rel_respects_binary_pred (Rel\<^sup>*) Pred
 5. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
have B: "\<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (symcl Rel) Pred
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_preserves_binary_pred (symcl Rel) Pred
 2. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
fix Rel
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_preserves_binary_pred (symcl Rel) Pred
 2. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
assume B1: "rel_respects_binary_pred Rel Pred"
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred Rel Pred

goal (2 subgoals):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_preserves_binary_pred (symcl Rel) Pred
 2. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
show "rel_preserves_binary_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_preserves_binary_pred (symcl Rel) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
fix a b x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
assume "(a, b) \<in> symcl Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
hence "(a, b) \<in> Rel \<or> (b, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<or> (b, a) \<in> Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
assume "Pred a x"
[PROOF STATE]
proof (state)
this:
Pred a x

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred a x \<Longrightarrow> Pred b x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred a x
[PROOF STEP]
show "Pred b x"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred a x

goal (1 subgoal):
 1. Pred b x
[PROOF STEP]
using B1
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred a x
rel_respects_binary_pred Rel Pred

goal (1 subgoal):
 1. Pred b x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Pred b x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_preserves_binary_pred (symcl Rel) Pred

goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
fix Rel
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
assume B2: "rel_respects_binary_pred Rel Pred"
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred Rel Pred

goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
show "rel_reflects_binary_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_reflects_binary_pred (symcl Rel) Pred
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
fix a b x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
assume "(a, b) \<in> symcl Rel"
[PROOF STATE]
proof (state)
this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
hence "(a, b) \<in> Rel \<or> (b, a) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> symcl Rel

goal (1 subgoal):
 1. (a, b) \<in> Rel \<or> (b, a) \<in> Rel
[PROOF STEP]
by (simp add: symcl_def)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
assume "Pred b x"
[PROOF STATE]
proof (state)
this:
Pred b x

goal (1 subgoal):
 1. \<And>a b x. (a, b) \<in> symcl Rel \<and> Pred b x \<Longrightarrow> Pred a x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred b x
[PROOF STEP]
show "Pred a x"
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred b x

goal (1 subgoal):
 1. Pred a x
[PROOF STEP]
using B2
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> Rel \<or> (b, a) \<in> Rel
Pred b x
rel_respects_binary_pred Rel Pred

goal (1 subgoal):
 1. Pred a x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Pred a x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_reflects_binary_pred (symcl Rel) Pred

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred ?Rel Pred \<Longrightarrow> rel_respects_binary_pred (symcl ?Rel) Pred

goal (5 subgoals):
 1. rel_respects_binary_pred (symcl Rel) Pred
 2. rel_respects_binary_pred (Rel\<^sup>+) Pred
 3. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
 4. rel_respects_binary_pred (Rel\<^sup>*) Pred
 5. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from respection B[where Rel="Rel"]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_binary_pred Rel Pred
rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (symcl Rel) Pred
[PROOF STEP]
show "rel_respects_binary_pred (symcl Rel) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred Rel Pred
rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (symcl Rel) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (symcl Rel) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred (symcl Rel) Pred

goal (4 subgoals):
 1. rel_respects_binary_pred (Rel\<^sup>+) Pred
 2. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
 3. rel_respects_binary_pred (Rel\<^sup>*) Pred
 4. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
have C: "\<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
fix Rel
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
assume "rel_respects_binary_pred Rel Pred"
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred Rel Pred

goal (1 subgoal):
 1. \<And>Rel. rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
thus "rel_respects_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred Rel Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
using preservation_of_binary_predicates_and_closures(2)[where Rel="Rel" and Pred="Pred"]
              reflection_of_binary_predicates_and_closures(2)[where Rel="Rel" and Pred="Pred"]
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred Rel Pred
rel_preserves_binary_pred Rel Pred \<Longrightarrow> rel_preserves_binary_pred (Rel\<^sup>+) Pred
rel_reflects_binary_pred Rel Pred \<Longrightarrow> rel_reflects_binary_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred (Rel\<^sup>+) Pred

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred ?Rel Pred \<Longrightarrow> rel_respects_binary_pred (?Rel\<^sup>+) Pred

goal (4 subgoals):
 1. rel_respects_binary_pred (Rel\<^sup>+) Pred
 2. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
 3. rel_respects_binary_pred (Rel\<^sup>*) Pred
 4. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from respection C[where Rel="Rel"]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_binary_pred Rel Pred
rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
show "rel_respects_binary_pred (Rel\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred Rel Pred
rel_respects_binary_pred Rel Pred \<Longrightarrow> rel_respects_binary_pred (Rel\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred (Rel\<^sup>+) Pred

goal (3 subgoals):
 1. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
 2. rel_respects_binary_pred (Rel\<^sup>*) Pred
 3. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from A B[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
[PROOF STEP]
show "rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred

goal (2 subgoals):
 1. rel_respects_binary_pred (Rel\<^sup>*) Pred
 2. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from A C[where Rel="Rel\<^sup>="]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred
[PROOF STEP]
show "rel_respects_binary_pred (Rel\<^sup>*) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
using trancl_reflcl[of Rel]
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred ((Rel\<^sup>=)\<^sup>+) Pred
(Rel\<^sup>=)\<^sup>+ = Rel\<^sup>*

goal (1 subgoal):
 1. rel_respects_binary_pred (Rel\<^sup>*) Pred
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred (Rel\<^sup>*) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
from A B[where Rel="Rel\<^sup>="] C[where Rel="symcl (Rel\<^sup>=)"]
[PROOF STATE]
proof (chain)
picking this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred \<Longrightarrow> rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
show "rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred"
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred (Rel\<^sup>=) Pred
rel_respects_binary_pred (Rel\<^sup>=) Pred \<Longrightarrow> rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred
rel_respects_binary_pred (symcl (Rel\<^sup>=)) Pred \<Longrightarrow> rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred

goal (1 subgoal):
 1. rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rel_respects_binary_pred ((symcl (Rel\<^sup>=))\<^sup>+) Pred

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> x \<Down> t \<Longrightarrow> t = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> x \<Down> t \<Longrightarrow> t = s
[PROOF STEP]
by blast


[STATEMENT]
lemma assumes "(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> x \<Down> t"
shows "t = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = s
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> x \<Down> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(IF b THEN SKIP ELSE SKIP, s) \<Rightarrow> x \<Down> t

goal (1 subgoal):
 1. t = s
[PROOF STEP]
proof cases  \<comment> \<open>inverting assms\<close>
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
 2. \<And>xa. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
case IfTrue
[PROOF STATE]
proof (state)
this:
bval b s
(SKIP, s) \<Rightarrow> x_ \<Down> t
x = x_ + 1

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
 2. \<And>xa. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bval b s
(SKIP, s) \<Rightarrow> x_ \<Down> t
x = x_ + 1

goal (1 subgoal):
 1. t = s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = s

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
case IfFalse
[PROOF STATE]
proof (state)
this:
\<not> bval b s
(SKIP, s) \<Rightarrow> x_ \<Down> t
x = x_ + 1

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<not> bval b s; (SKIP, s) \<Rightarrow> xa \<Down> t; x = xa + 1\<rbrakk> \<Longrightarrow> t = s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> bval b s
(SKIP, s) \<Rightarrow> x_ \<Down> t
x = x_ + 1

goal (1 subgoal):
 1. t = s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t = s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t = s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assign_t_simp:
  "(x ::= a,s) \<Rightarrow> Suc 0 \<Down>  s' \<longleftrightarrow> (s' = s(x := aval a s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ::= a, s) \<Rightarrow> Suc 0 \<Down> s' = (s' = s(x := aval a s))
[PROOF STEP]
by (auto)


[STATEMENT]
lemma Seq_t_assoc:
  "((c1;; c2;; c3, s) \<Rightarrow> p \<Down>  s') \<longleftrightarrow> ((c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s' = (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
assume "(c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'"
[PROOF STATE]
proof (state)
this:
(c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'

goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
obtain s1 s2 p1 p2 p3 where
    c1: "(c1, s) \<Rightarrow> p1 \<Down> s1" and
    c2: "(c2, s1) \<Rightarrow> p2 \<Down> s2" and
    c3: "(c3, s2) \<Rightarrow> p3 \<Down> s'" and
    p: "p = p1 + (p2 + p3)"
[PROOF STATE]
proof (prove)
using this:
(c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'

goal (1 subgoal):
 1. (\<And>p1 s1 p2 s2 p3. \<lbrakk>(c1, s) \<Rightarrow> p1 \<Down> s1; (c2, s1) \<Rightarrow> p2 \<Down> s2; (c3, s2) \<Rightarrow> p3 \<Down> s'; p = p1 + (p2 + p3)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2, s1) \<Rightarrow> p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'
p = p1 + (p2 + p3)

goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
from c2 c3
[PROOF STATE]
proof (chain)
picking this:
(c2, s1) \<Rightarrow> p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'
[PROOF STEP]
have "(c2;; c3, s1) \<Rightarrow> p2 + p3 \<Down>  s'"
[PROOF STATE]
proof (prove)
using this:
(c2, s1) \<Rightarrow> p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'

goal (1 subgoal):
 1. (c2;; c3, s1) \<Rightarrow> p2 + p3 \<Down> s'
[PROOF STEP]
apply (rule Seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2 + p3 = p2 + p3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c2;; c3, s1) \<Rightarrow> p2 + p3 \<Down> s'

goal (2 subgoals):
 1. (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
 2. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
with c1
[PROOF STATE]
proof (chain)
picking this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2;; c3, s1) \<Rightarrow> p2 + p3 \<Down> s'
[PROOF STEP]
show "(c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'"
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2;; c3, s1) \<Rightarrow> p2 + p3 \<Down> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2;; c3, s1) \<Rightarrow> p2 + p3 \<Down> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p1 + (p2 + p3) \<Down> s'
[PROOF STEP]
apply (rule Seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 + (p2 + p3) = p1 + (p2 + p3)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
next
  \<comment> \<open>The other direction is analogous\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
assume "(c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'"
[PROOF STATE]
proof (state)
this:
(c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
obtain s1 s2 p1 p2 p3 where
    c1: "(c1, s) \<Rightarrow> p1 \<Down> s1" and
    c2: "(c2, s1) \<Rightarrow> p2 \<Down> s2" and
    c3: "(c3, s2) \<Rightarrow> p3 \<Down> s'" and
    p: "p = (p1 + p2) + p3"
[PROOF STATE]
proof (prove)
using this:
(c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s'

goal (1 subgoal):
 1. (\<And>p1 s1 p2 s2 p3. \<lbrakk>(c1, s) \<Rightarrow> p1 \<Down> s1; (c2, s1) \<Rightarrow> p2 \<Down> s2; (c3, s2) \<Rightarrow> p3 \<Down> s'; p = p1 + p2 + p3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2, s1) \<Rightarrow> p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'
p = p1 + p2 + p3

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
from c1 c2
[PROOF STATE]
proof (chain)
picking this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2, s1) \<Rightarrow> p2 \<Down> s2
[PROOF STEP]
have "(c1;; c2, s) \<Rightarrow> p1 + p2 \<Down>  s2"
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<Rightarrow> p1 \<Down> s1
(c2, s1) \<Rightarrow> p2 \<Down> s2

goal (1 subgoal):
 1. (c1;; c2, s) \<Rightarrow> p1 + p2 \<Down> s2
[PROOF STEP]
apply (rule Seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 + p2 = p1 + p2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c1;; c2, s) \<Rightarrow> p1 + p2 \<Down> s2

goal (1 subgoal):
 1. (c1;; (c2;; c3), s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
from this c3
[PROOF STATE]
proof (chain)
picking this:
(c1;; c2, s) \<Rightarrow> p1 + p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'
[PROOF STEP]
show "(c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'"
[PROOF STATE]
proof (prove)
using this:
(c1;; c2, s) \<Rightarrow> p1 + p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'

goal (1 subgoal):
 1. (c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
using this:
(c1;; c2, s) \<Rightarrow> p1 + p2 \<Down> s2
(c3, s2) \<Rightarrow> p3 \<Down> s'

goal (1 subgoal):
 1. (c1;; c2;; c3, s) \<Rightarrow> p1 + p2 + p3 \<Down> s'
[PROOF STEP]
apply (rule Seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p1 + p2 + p3 = p1 + p2 + p3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(c1;; c2;; c3, s) \<Rightarrow> p \<Down> s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "(\<exists>p. ((c, s) \<Rightarrow> p \<Down>  s')) = ((c, s) \<Rightarrow> s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>p. (c, s) \<Rightarrow> p \<Down> s') = (c, s) \<Rightarrow> s'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>p. (c, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c, s) \<Rightarrow> s'
 2. (c, s) \<Rightarrow> s' \<Longrightarrow> \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
assume "\<exists>p. (c, s) \<Rightarrow> p \<Down> s'"
[PROOF STATE]
proof (state)
this:
\<exists>p. (c, s) \<Rightarrow> p \<Down> s'

goal (2 subgoals):
 1. \<exists>p. (c, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c, s) \<Rightarrow> s'
 2. (c, s) \<Rightarrow> s' \<Longrightarrow> \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
obtain p where "(c, s) \<Rightarrow> p \<Down> s'"
[PROOF STATE]
proof (prove)
using this:
\<exists>p. (c, s) \<Rightarrow> p \<Down> s'

goal (1 subgoal):
 1. (\<And>p. (c, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c, s) \<Rightarrow> p \<Down> s'

goal (2 subgoals):
 1. \<exists>p. (c, s) \<Rightarrow> p \<Down> s' \<Longrightarrow> (c, s) \<Rightarrow> s'
 2. (c, s) \<Rightarrow> s' \<Longrightarrow> \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
show "((c, s) \<Rightarrow> s')"
[PROOF STATE]
proof (prove)
using this:
(c, s) \<Rightarrow> p \<Down> s'

goal (1 subgoal):
 1. (c, s) \<Rightarrow> s'
[PROOF STEP]
apply(induct c s p s' rule: big_step_t_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s. (SKIP, s) \<Rightarrow> s
 2. \<And>x a s. (x ::= a, s) \<Rightarrow> s(x := aval a s)
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, s1) \<Rightarrow> s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, s2) \<Rightarrow> s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, s1) \<Rightarrow> s3
 4. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, s) \<Rightarrow> t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, s) \<Rightarrow> t
 5. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, s) \<Rightarrow> t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, s) \<Rightarrow> t
 6. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, s1) \<Rightarrow> s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, s2) \<Rightarrow> s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1) \<Rightarrow> s3
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x a s. (x ::= a, s) \<Rightarrow> s(x := aval a s)
 2. \<And>s. (SKIP, s) \<Rightarrow> s
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, s1) \<Rightarrow> s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, s2) \<Rightarrow> s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, s1) \<Rightarrow> s3
 4. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, s) \<Rightarrow> t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, s) \<Rightarrow> t
 5. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, s) \<Rightarrow> t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, s) \<Rightarrow> t
 6. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, s1) \<Rightarrow> s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, s2) \<Rightarrow> s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1) \<Rightarrow> s3
[PROOF STEP]
apply(rule Big_Step.Assign)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s. (SKIP, s) \<Rightarrow> s
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, s1) \<Rightarrow> s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, s2) \<Rightarrow> s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, s1) \<Rightarrow> s3
 3. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, s) \<Rightarrow> t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, s) \<Rightarrow> t
 4. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, s) \<Rightarrow> t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, s) \<Rightarrow> t
 5. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, s) \<Rightarrow> s
 6. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, s1) \<Rightarrow> s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, s2) \<Rightarrow> s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, s1) \<Rightarrow> s3
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(c, s) \<Rightarrow> s'

goal (1 subgoal):
 1. (c, s) \<Rightarrow> s' \<Longrightarrow> \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (c, s) \<Rightarrow> s' \<Longrightarrow> \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
assume "((c, s) \<Rightarrow> s')"
[PROOF STATE]
proof (state)
this:
(c, s) \<Rightarrow> s'

goal (1 subgoal):
 1. (c, s) \<Rightarrow> s' \<Longrightarrow> \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(c, s) \<Rightarrow> s'
[PROOF STEP]
show "(\<exists>p. ((c, s) \<Rightarrow> p \<Down>  s'))"
[PROOF STATE]
proof (prove)
using this:
(c, s) \<Rightarrow> s'

goal (1 subgoal):
 1. \<exists>p. (c, s) \<Rightarrow> p \<Down> s'
[PROOF STEP]
apply(induct c s s' rule: big_step_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s. \<exists>p. (SKIP, s) \<Rightarrow> p \<Down> s
 2. \<And>x a s. \<exists>p. (x ::= a, s) \<Rightarrow> p \<Down> s(x := aval a s)
 3. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<exists>p. (c\<^sub>1, s\<^sub>1) \<Rightarrow> p \<Down> s\<^sub>2; (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<exists>p. (c\<^sub>2, s\<^sub>2) \<Rightarrow> p \<Down> s\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>p. (c\<^sub>1;; c\<^sub>2, s\<^sub>1) \<Rightarrow> p \<Down> s\<^sub>3
 4. \<And>b s c\<^sub>1 t c\<^sub>2. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<exists>p. (c\<^sub>1, s) \<Rightarrow> p \<Down> t\<rbrakk> \<Longrightarrow> \<exists>p. (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> p \<Down> t
 5. \<And>b s c\<^sub>2 t c\<^sub>1. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<exists>p. (c\<^sub>2, s) \<Rightarrow> p \<Down> t\<rbrakk> \<Longrightarrow> \<exists>p. (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> p \<Down> t
 6. \<And>b s c. \<not> bval b s \<Longrightarrow> \<exists>p. (WHILE b DO c, s) \<Rightarrow> p \<Down> s
 7. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<exists>p. (c, s\<^sub>1) \<Rightarrow> p \<Down> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<exists>p. (WHILE b DO c, s\<^sub>2) \<Rightarrow> p \<Down> s\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>p. (WHILE b DO c, s\<^sub>1) \<Rightarrow> p \<Down> s\<^sub>3
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
\<exists>p. (c, s) \<Rightarrow> p \<Down> s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem big_step_t_determ: "\<lbrakk> (c,s) \<Rightarrow> p \<Down> t; (c,s) \<Rightarrow> q \<Down> u \<rbrakk> \<Longrightarrow> u = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(c, s) \<Rightarrow> p \<Down> t; (c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t
[PROOF STEP]
apply (induction arbitrary: u q rule: big_step_t.induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s u q. (SKIP, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s
 2. \<And>x a s u q. (x ::= a, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s(x := aval a s)
 3. \<And>c1 s1 x s2 c2 y s3 z u q. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c1, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2; (c2, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (c2, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3; z = x + y; (c1;; c2, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3
 4. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t
 5. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t
 6. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s
 7. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem big_step_t_determ2: "\<lbrakk> (c,s) \<Rightarrow> p \<Down> t; (c,s) \<Rightarrow> q \<Down> u \<rbrakk> \<Longrightarrow> (u = t \<and> p=q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(c, s) \<Rightarrow> p \<Down> t; (c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> p = q
[PROOF STEP]
apply  (induction arbitrary: u q rule: big_step_t_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s u q. (SKIP, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s \<and> Suc 0 = q
 2. \<And>x a s u q. (x ::= a, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s(x := aval a s) \<and> Suc 0 = q
 3. \<And>c1 s1 x s2 c2 y s3 z u q. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c1, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (c2, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (c2, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; z = x + y; (c1;; c2, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
 4. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 5. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 6. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 7. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(elim Skip_tE)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s u q. \<lbrakk>q = Suc 0; u = s\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 2. \<And>x a s u q. (x ::= a, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s(x := aval a s) \<and> Suc 0 = q
 3. \<And>c1 s1 x s2 c2 y s3 z u q. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c1, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (c2, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (c2, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; z = x + y; (c1;; c2, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
 4. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 5. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 6. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 7. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x a s u q. (x ::= a, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s(x := aval a s) \<and> Suc 0 = q
 2. \<And>c1 s1 x s2 c2 y s3 z u q. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c1, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (c2, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (c2, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; z = x + y; (c1;; c2, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
 3. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 4. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 5. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 6. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(elim Assign_tE)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x a s u q. \<lbrakk>q = Suc 0; u = s(x := aval a s)\<rbrakk> \<Longrightarrow> u = s(x := aval a s) \<and> Suc 0 = q
 2. \<And>c1 s1 x s2 c2 y s3 z u q. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c1, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (c2, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (c2, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; z = x + y; (c1;; c2, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
 3. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 4. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 5. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 6. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z u q. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c1, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (c2, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (c2, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; z = x + y; (c1;; c2, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
 2. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 3. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 4. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 5. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c1 x t y c2 u q. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 2. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 3. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 4. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(elim If_tE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>b s c1 x t y c2 u q xa. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; q = Suc xa; bval b s; (c1, s) \<Rightarrow> xa \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 2. \<And>b s c1 x t y c2 u q xa. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; q = Suc xa; \<not> bval b s; (c2, s) \<Rightarrow> xa \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 3. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 4. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 5. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c1 x t y c2 u q xa. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; \<And>u q. (c1, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; q = Suc xa; \<not> bval b s; (c2, s) \<Rightarrow> xa \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 2. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 3. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 4. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c2 x t y c1 u q. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; (IF b THEN c1 ELSE c2, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 2. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 3. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(elim If_tE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c2 x t y c1 u q xa. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; q = Suc xa; bval b s; (c1, s) \<Rightarrow> xa \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 2. \<And>b s c2 x t y c1 u q xa. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; q = Suc xa; \<not> bval b s; (c2, s) \<Rightarrow> xa \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 3. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 4. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c2 x t y c1 u q xa. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; \<And>u q. (c2, s) \<Rightarrow> q \<Down> u \<Longrightarrow> u = t \<and> x = q; y = x + 1; q = Suc xa; \<not> bval b s; (c2, s) \<Rightarrow> xa \<Down> u\<rbrakk> \<Longrightarrow> u = t \<and> y = q
 2. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 3. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s c u q. \<lbrakk>\<not> bval b s; (WHILE b DO c, s) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 2. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(erule While_tE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c u q. \<lbrakk>\<not> bval b s; q = Suc 0; u = s; \<not> bval b s\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 2. \<And>b s c u q x s2 y. \<lbrakk>\<not> bval b s; bval b s; (c, s) \<Rightarrow> x \<Down> s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> u; Suc (x + y) = q\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 3. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s c u q x s2 y. \<lbrakk>\<not> bval b s; bval b s; (c, s) \<Rightarrow> x \<Down> s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> u; Suc (x + y) = q\<rbrakk> \<Longrightarrow> u = s \<and> Suc 0 = q
 2. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
bval b_ s1_
(c_, s1_) \<Rightarrow> x_ \<Down> s2_
(c_, s1_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s2_ \<and> x_ = ?q
(WHILE b_ DO c_, s2_) \<Rightarrow> y_ \<Down> s3_
(WHILE b_ DO c_, s2_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s3_ \<and> y_ = ?q
1 + x_ + y_ = z_
(WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_

goal (1 subgoal):
 1. \<And>b s1 c x s2 y s3 z u q. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; \<And>u q. (c, s1) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s2 \<and> x = q; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; \<And>u q. (WHILE b DO c, s2) \<Rightarrow> q \<Down> u \<Longrightarrow> u = s3 \<and> y = q; 1 + x + y = z; (WHILE b DO c, s1) \<Rightarrow> q \<Down> u\<rbrakk> \<Longrightarrow> u = s3 \<and> z = q
[PROOF STEP]
from 1(7)
[PROOF STATE]
proof (chain)
picking this:
(WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_

goal (1 subgoal):
 1. u_ = s3_ \<and> z_ = q_
[PROOF STEP]
apply(safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> u_ = s3_
 2. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> z_ = q_
[PROOF STEP]
apply(erule While_tE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>q_ = Suc 0; u_ = s1_; \<not> bval b_ s1_\<rbrakk> \<Longrightarrow> u_ = s3_
 2. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> u_ = s3_
 3. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> z_ = q_
[PROOF STEP]
using 1(1-6)
[PROOF STATE]
proof (prove)
using this:
bval b_ s1_
(c_, s1_) \<Rightarrow> x_ \<Down> s2_
(c_, s1_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s2_ \<and> x_ = ?q
(WHILE b_ DO c_, s2_) \<Rightarrow> y_ \<Down> s3_
(WHILE b_ DO c_, s2_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s3_ \<and> y_ = ?q
1 + x_ + y_ = z_

goal (3 subgoals):
 1. \<lbrakk>q_ = Suc 0; u_ = s1_; \<not> bval b_ s1_\<rbrakk> \<Longrightarrow> u_ = s3_
 2. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> u_ = s3_
 3. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> z_ = q_
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> u_ = s3_
 2. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> z_ = q_
[PROOF STEP]
using 1(1-6)
[PROOF STATE]
proof (prove)
using this:
bval b_ s1_
(c_, s1_) \<Rightarrow> x_ \<Down> s2_
(c_, s1_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s2_ \<and> x_ = ?q
(WHILE b_ DO c_, s2_) \<Rightarrow> y_ \<Down> s3_
(WHILE b_ DO c_, s2_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s3_ \<and> y_ = ?q
1 + x_ + y_ = z_

goal (2 subgoals):
 1. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> u_ = s3_
 2. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> z_ = q_
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (WHILE b_ DO c_, s1_) \<Rightarrow> q_ \<Down> u_ \<Longrightarrow> z_ = q_
[PROOF STEP]
apply(erule While_tE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>q_ = Suc 0; u_ = s1_; \<not> bval b_ s1_\<rbrakk> \<Longrightarrow> z_ = q_
 2. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> z_ = q_
[PROOF STEP]
using 1(1-6)
[PROOF STATE]
proof (prove)
using this:
bval b_ s1_
(c_, s1_) \<Rightarrow> x_ \<Down> s2_
(c_, s1_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s2_ \<and> x_ = ?q
(WHILE b_ DO c_, s2_) \<Rightarrow> y_ \<Down> s3_
(WHILE b_ DO c_, s2_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s3_ \<and> y_ = ?q
1 + x_ + y_ = z_

goal (2 subgoals):
 1. \<lbrakk>q_ = Suc 0; u_ = s1_; \<not> bval b_ s1_\<rbrakk> \<Longrightarrow> z_ = q_
 2. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> z_ = q_
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> z_ = q_
[PROOF STEP]
using 1(1-6)
[PROOF STATE]
proof (prove)
using this:
bval b_ s1_
(c_, s1_) \<Rightarrow> x_ \<Down> s2_
(c_, s1_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s2_ \<and> x_ = ?q
(WHILE b_ DO c_, s2_) \<Rightarrow> y_ \<Down> s3_
(WHILE b_ DO c_, s2_) \<Rightarrow> ?q \<Down> ?u \<Longrightarrow> ?u = s3_ \<and> y_ = ?q
1 + x_ + y_ = z_

goal (1 subgoal):
 1. \<And>x s2 y. \<lbrakk>bval b_ s1_; (c_, s1_) \<Rightarrow> x \<Down> s2; (WHILE b_ DO c_, s2) \<Rightarrow> y \<Down> u_; Suc (x + y) = q_\<rbrakk> \<Longrightarrow> z_ = q_
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
u_ = s3_ \<and> z_ = q_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bigstep_det: "(c1, s) \<Rightarrow> p1 \<Down> t1 \<Longrightarrow> (c1, s) \<Rightarrow> p \<Down> t \<Longrightarrow> p1=p \<and> t1=t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(c1, s) \<Rightarrow> p1 \<Down> t1; (c1, s) \<Rightarrow> p \<Down> t\<rbrakk> \<Longrightarrow> p1 = p \<and> t1 = t
[PROOF STEP]
using big_step_t_determ2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?c, ?s) \<Rightarrow> ?p \<Down> ?t; (?c, ?s) \<Rightarrow> ?q \<Down> ?u\<rbrakk> \<Longrightarrow> ?u = ?t \<and> ?p = ?q

goal (1 subgoal):
 1. \<lbrakk>(c1, s) \<Rightarrow> p1 \<Down> t1; (c1, s) \<Rightarrow> p \<Down> t\<rbrakk> \<Longrightarrow> p1 = p \<and> t1 = t
[PROOF STEP]
by simp


[STATEMENT]
lemma bigstep_progress: "(c, s) \<Rightarrow> p \<Down> t \<Longrightarrow> p > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, s) \<Rightarrow> p \<Down> t \<Longrightarrow> 0 < p
[PROOF STEP]
apply(induct rule: big_step_t.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma bigstepT_the_cost: "(c, s) \<Rightarrow> t \<Down> s' \<Longrightarrow> \<down>\<^sub>t(c, s) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, s) \<Rightarrow> t \<Down> s' \<Longrightarrow> \<down>\<^sub>t (c, s) = t
[PROOF STEP]
using bigstep_det
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?c1.0, ?s) \<Rightarrow> ?p1.0 \<Down> ?t1.0; (?c1.0, ?s) \<Rightarrow> ?p \<Down> ?t\<rbrakk> \<Longrightarrow> ?p1.0 = ?p \<and> ?t1.0 = ?t

goal (1 subgoal):
 1. (c, s) \<Rightarrow> t \<Down> s' \<Longrightarrow> \<down>\<^sub>t (c, s) = t
[PROOF STEP]
by blast


[STATEMENT]
lemma bigstepT_the_state: "(c, s) \<Rightarrow> t \<Down> s' \<Longrightarrow> \<down>\<^sub>s(c, s) = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, s) \<Rightarrow> t \<Down> s' \<Longrightarrow> \<down>\<^sub>s (c, s) = s'
[PROOF STEP]
using bigstep_det
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?c1.0, ?s) \<Rightarrow> ?p1.0 \<Down> ?t1.0; (?c1.0, ?s) \<Rightarrow> ?p \<Down> ?t\<rbrakk> \<Longrightarrow> ?p1.0 = ?p \<and> ?t1.0 = ?t

goal (1 subgoal):
 1. (c, s) \<Rightarrow> t \<Down> s' \<Longrightarrow> \<down>\<^sub>s (c, s) = s'
[PROOF STEP]
by blast


[STATEMENT]
lemma SKIPnot: "(\<not> (SKIP, s) \<Rightarrow> p \<Down> t) = (s\<noteq>t \<or> p\<noteq>Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (SKIP, s) \<Rightarrow> p \<Down> t) = (s \<noteq> t \<or> p \<noteq> Suc 0)
[PROOF STEP]
by blast


[STATEMENT]
lemma SKIPp: "\<down>\<^sub>t(SKIP,s) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<down>\<^sub>t (SKIP, s) = Suc 0
[PROOF STEP]
apply(rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>a. (SKIP, s) \<Rightarrow> Suc 0 \<Down> a
 2. \<And>n. \<exists>a. (SKIP, s) \<Rightarrow> n \<Down> a \<Longrightarrow> n = Suc 0
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<exists>a. (SKIP, s) \<Rightarrow> n \<Down> a \<Longrightarrow> n = Suc 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma SKIPt: "\<down>\<^sub>s(SKIP,s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<down>\<^sub>s (SKIP, s) = s
[PROOF STEP]
apply(rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>n. (SKIP, s) \<Rightarrow> n \<Down> s
 2. \<And>a. \<exists>n. (SKIP, s) \<Rightarrow> n \<Down> a \<Longrightarrow> a = s
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. \<exists>n. (SKIP, s) \<Rightarrow> n \<Down> a \<Longrightarrow> a = s
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ASSp: "(THE p. Ex (big_step_t (x ::= e, s) p)) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<down>\<^sub>t (x ::= e, s) = Suc 0
[PROOF STEP]
apply(rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Ex (big_step_t (x ::= e, s) (Suc 0))
 2. \<And>p. Ex (big_step_t (x ::= e, s) p) \<Longrightarrow> p = Suc 0
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. Ex (big_step_t (x ::= e, s) p) \<Longrightarrow> p = Suc 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ASSt: "(THE t. \<exists>p. (x ::= e, s) \<Rightarrow> p \<Down> t) = s(x := aval e s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<down>\<^sub>s (x ::= e, s) = s(x := aval e s)
[PROOF STEP]
apply(rule the_equality)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>p. (x ::= e, s) \<Rightarrow> p \<Down> s(x := aval e s)
 2. \<And>t. \<exists>p. (x ::= e, s) \<Rightarrow> p \<Down> t \<Longrightarrow> t = s(x := aval e s)
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<exists>p. (x ::= e, s) \<Rightarrow> p \<Down> t \<Longrightarrow> t = s(x := aval e s)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ASSnot: "( \<not> (x ::= e, s) \<Rightarrow> p \<Down> t ) = (p\<noteq>Suc 0 \<or> t\<noteq>s(x := aval e s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (x ::= e, s) \<Rightarrow> p \<Down> t) = (p \<noteq> Suc 0 \<or> t \<noteq> s(x := aval e s))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma If_THE_True: "Suc (THE n. \<exists>a. (c1, s) \<Rightarrow> n \<Down> a) =  (THE n. \<exists>a. (IF b THEN c1 ELSE c2, s) \<Rightarrow> n \<Down> a)"
     if T: "bval b s" and c1_t: "terminates (c1,s)" for s l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
from c1_t
[PROOF STATE]
proof (chain)
picking this:
\<down> (c1, s)
[PROOF STEP]
obtain p t where a: "(c1, s) \<Rightarrow> p \<Down> t"
[PROOF STATE]
proof (prove)
using this:
\<down> (c1, s)

goal (1 subgoal):
 1. (\<And>p t. (c1, s) \<Rightarrow> p \<Down> t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(c1, s) \<Rightarrow> p \<Down> t

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
with T
[PROOF STATE]
proof (chain)
picking this:
bval b s
(c1, s) \<Rightarrow> p \<Down> t
[PROOF STEP]
have b: "(IF b THEN c1 ELSE c2, s) \<Rightarrow> p+1 \<Down> t"
[PROOF STATE]
proof (prove)
using this:
bval b s
(c1, s) \<Rightarrow> p \<Down> t

goal (1 subgoal):
 1. (IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
[PROOF STEP]
using IfTrue
[PROOF STATE]
proof (prove)
using this:
bval b s
(c1, s) \<Rightarrow> p \<Down> t
\<lbrakk>bval ?b ?s; (?c1.0, ?s) \<Rightarrow> ?x \<Down> ?t; ?y = ?x + 1\<rbrakk> \<Longrightarrow> (IF ?b THEN ?c1.0 ELSE ?c2.0, ?s) \<Rightarrow> ?y \<Down> ?t

goal (1 subgoal):
 1. (IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
from a bigstepT_the_cost
[PROOF STATE]
proof (chain)
picking this:
(c1, s) \<Rightarrow> p \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t
[PROOF STEP]
have "(THE n. \<exists>a. (c1, s) \<Rightarrow> n \<Down> a) = p"
[PROOF STATE]
proof (prove)
using this:
(c1, s) \<Rightarrow> p \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t

goal (1 subgoal):
 1. \<down>\<^sub>t (c1, s) = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<down>\<^sub>t (c1, s) = p

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<down>\<^sub>t (c1, s) = p

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
from b bigstepT_the_cost
[PROOF STATE]
proof (chain)
picking this:
(IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t
[PROOF STEP]
have "(THE n. \<exists>a. (IF b THEN c1 ELSE c2, s) \<Rightarrow> n \<Down> a) = p+1"
[PROOF STATE]
proof (prove)
using this:
(IF b THEN c1 ELSE c2, s) \<Rightarrow> p + 1 \<Down> t
(?c, ?s) \<Rightarrow> ?t \<Down> ?s' \<Longrightarrow> \<down>\<^sub>t (?c, ?s) = ?t

goal (1 subgoal):
 1. \<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<down>\<^sub>t (c1, s) = p
\<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<down>\<^sub>t (c1, s) = p
\<down>\<^sub>t (IF b THEN c1 ELSE c2, s) = p + 1

goal (1 subgoal):
 1. Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (\<down>\<^sub>t (c1, s)) = \<down>\<^sub>t (IF b THEN c1 ELSE c2, s)

goal:
No subgoals!
[PROOF STEP]
qed