# Theory Hoare

```(* Title:      Hoare Calculus
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Hoare Calculus›

theory Hoare

imports Complete_Tests Preconditions

begin

class ite =
fixes ite :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("_ ⊲ _ ⊳ _" [58,58,58] 57)

class hoare_triple =
fixes hoare_triple :: "'a ⇒ 'a ⇒ 'a ⇒ bool" ("_ ⦃ _ ⦄ _" [54,54,54] 53)

class ifthenelse = precondition + ite +
assumes ite_pre: "x⊲-p⊳y«-q = -p*(x«-q) ⊔ --p*(y«-q)"
begin

text ‹Theorem 40.2›

lemma ite_pre_then:
"-p*(x⊲-p⊳y«-q) = -p*(x«-q)"
proof -
have "-p*(x⊲-p⊳y«-q) = -p*(x«-q) ⊔ bot*(y«-q)"
by (smt (z3) ite_pre pre_closed tests_dual.sba_dual.sup_right_unit tests_dual.sub_commutative tests_dual.sup_left_zero tests_dual.sup_right_dist_inf tests_dual.top_double_complement tests_dual.wnf_lemma_1)
thus ?thesis
by (metis pre_closed tests_dual.sba_dual.sup_right_unit tests_dual.sub_sup_closed tests_dual.sup_left_zero)
qed

text ‹Theorem 40.3›

lemma ite_pre_else:
"--p*(x⊲-p⊳y«-q) = --p*(y«-q)"
proof -
have "--p*(x⊲-p⊳y«-q) = bot*(x«-q) ⊔ --p*(y«-q)"
by (smt (z3) ite_pre pre_closed tests_dual.sub_commutative tests_dual.sub_inf_left_zero tests_dual.sup_left_zero tests_dual.sup_right_dist_inf tests_dual.top_double_complement tests_dual.wnf_lemma_3)
thus ?thesis
by (metis pre_closed tests_dual.sba_dual.sub_sup_demorgan tests_dual.sub_inf_left_zero tests_dual.sup_left_zero)
qed

lemma ite_import_mult_then:
"-p*-q ≤ x«-r ⟹ -p*-q ≤ x⊲-p⊳y«-r"
by (smt ite_pre_then leq_def pre_closed sub_assoc sub_comm sub_mult_closed)

lemma ite_import_mult_else:
"--p*-q ≤ y«-r ⟹ --p*-q ≤ x⊲-p⊳y«-r"
by (smt ite_pre_else leq_def pre_closed sub_assoc sub_comm sub_mult_closed)

text ‹Theorem 40.1›

lemma ite_import_mult:
"-p*-q ≤ x«-r ⟹ --p*-q ≤ y«-r ⟹ -q ≤ x⊲-p⊳y«-r"
by (smt (verit) ite_import_mult_else ite_import_mult_then pre_closed tests_dual.sba_dual.inf_less_eq_cases)

end

class whiledo = ifthenelse + while +
assumes while_pre: "-p⋆x«-q = -p*(x«-p⋆x«-q) ⊔ --p*-q"
assumes while_post: "-p⋆x«-q = -p⋆x«--p*-q"
begin

text ‹Theorem 40.4›

lemma while_pre_then:
"-p*(-p⋆x«-q) = -p*(x«-p⋆x«-q)"
by (smt pre_closed tests_dual.sub_commutative while_pre tests_dual.wnf_lemma_1)

text ‹Theorem 40.5›

lemma while_pre_else:
"--p*(-p⋆x«-q) = --p*-q"
by (smt pre_closed tests_dual.sub_commutative while_pre tests_dual.wnf_lemma_3)

text ‹Theorem 40.6›

lemma while_pre_sub_1:
"-p⋆x«-q ≤ x*(-p⋆x)⊲-p⊳1«-q"
by (smt (z3) ite_import_mult pre_closed pre_one_increasing pre_seq tests_dual.sba_dual.transitive tests_dual.sub_sup_closed tests_dual.upper_bound_right while_pre_else while_pre_then)

text ‹Theorem 40.7›

lemma while_pre_sub_2:
"-p⋆x«-q ≤ x⊲-p⊳1«-p⋆x«-q"
by (smt (z3) ite_import_mult pre_closed pre_one_increasing tests_dual.sba_dual.transitive tests_dual.sub_sup_closed tests_dual.upper_bound_right while_pre_then)

text ‹Theorem 40.8›

lemma while_pre_compl:
"--p ≤ -p⋆x«--p"
by (metis pre_closed tests_dual.sup_idempotent tests_dual.upper_bound_right while_pre_else)

lemma while_pre_compl_one:
"--p ≤ -p⋆x«1"
by (metis tests_dual.sba_dual.top_double_complement while_post tests_dual.sup_right_unit while_pre_compl)

text ‹Theorem 40.10›

lemma while_export_equiv:
"-q ≤ -p⋆x«1 ⟷ -p*-q ≤ -p⋆x«1"
by (smt pre_closed tests_dual.sba_dual.shunting tests_dual.sba_dual.sub_less_eq_def tests_dual.sba_dual.top_double_complement while_pre_compl_one)

lemma nat_test_pre:
assumes "nat_test t s"
and "-q ≤ s"
and "∀n . t n*-p*-q ≤ x«pSum t n*-q"
shows "-q ≤ -p⋆x«--p*-q"
proof -
have 1: "-q*--p ≤ -p⋆x«--p*-q"
by (metis pre_closed tests_dual.sub_commutative while_post tests_dual.upper_bound_right while_pre_else)
have "∀n . t n*-p*-q ≤ -p⋆x«--p*-q"
proof
fix n
show "t n*-p*-q ≤ -p⋆x«--p*-q"
proof (induct n rule: nat_less_induct)
fix n
have 2: "t n = --(t n)"
using assms(1) nat_test_def by auto
assume "∀m<n . t m*-p*-q ≤ -p⋆x«--p*-q"
hence "∀m<n . t m*-p*-q ⊔ t m*--p*-q ≤ -p⋆x«--p*-q"
using 1 by (smt (verit, del_insts) assms(1) tests_dual.greatest_lower_bound leq_def nat_test_def pre_closed tests_dual.sub_associative tests_dual.sub_commutative sub_mult_closed)
hence "∀m<n . t m*-q ≤ -p⋆x«--p*-q"
by (smt (verit, del_insts) assms(1) tests_dual.sup_right_unit tests_dual.sup_left_dist_inf tests_dual.sup_right_dist_inf nat_test_def tests_dual.inf_complement sub_mult_closed)
hence "pSum t n*-q ≤ -p⋆x«--p*-q"
by (smt assms(1) pSum_below_nat pre_closed sub_mult_closed)
hence "t n*-p*-q*(-p⋆x«--p*-q) = t n*-p*-q"
using 2 by (smt assms(1,3) leq_def pSum_test_nat pre_closed pre_sub_distr sub_assoc sub_comm sub_mult_closed transitive while_pre_then)
thus "t n*-p*-q ≤ -p⋆x«--p*-q"
using 2 by (smt (z3) pre_closed tests_dual.sub_sup_closed tests_dual.upper_bound_right)
qed
qed
hence "-q*-p ≤ -p⋆x«--p*-q"
by (smt (verit, del_insts) assms(1,2) leq_def nat_test_def pre_closed tests_dual.sub_associative tests_dual.sub_commutative sub_mult_closed)
thus ?thesis
using 1 by (smt (z3) pre_closed tests_dual.sba_dual.inf_less_eq_cases tests_dual.sub_commutative tests_dual.sub_sup_closed)
qed

lemma nat_test_pre_1:
assumes "nat_test t s"
and "-r ≤ s"
and "-r ≤ -q"
and "∀n . t n*-p*-q ≤ x«pSum t n*-q"
shows "-r ≤ -p⋆x«--p*-q"
proof -
let ?qs = "-q*s"
have 1: "-r ≤ ?qs"
by (metis assms(1-3) nat_test_def tests_dual.least_upper_bound)
have "∀n . t n*-p*?qs ≤ x«pSum t n*?qs"
proof
fix n
have 2: "pSum t n ≤ s"
have "t n = t n * s"
by (metis assms(1) nat_test_def tests_dual.sba_dual.less_eq_inf)
hence "t n*-p*?qs = t n*-p*-q"
by (smt (verit, ccfv_threshold) assms(1) nat_test_def tests_dual.sub_sup_closed tests_dual.sub_associative tests_dual.sub_commutative)
also have "t n*-p*-q ≤ x«pSum t n*-q"
also have "x«pSum t n*-q = x«pSum t n*?qs"
using 2 by (smt (verit, ccfv_SIG) assms(1) leq_def nat_test_def pSum_test_nat tests_dual.sub_associative tests_dual.sub_commutative)
finally show "t n*-p*?qs ≤ x«pSum t n*?qs"
.
qed
hence 3: "?qs ≤ -p⋆x«--p*?qs"
by (smt (verit, ccfv_threshold) assms(1) tests_dual.upper_bound_left tests_dual.upper_bound_right nat_test_def nat_test_pre pSum_test_nat pre_closed tests_dual.sub_associative sub_mult_closed transitive)
have "-p⋆x«--p*?qs ≤ -p⋆x«--p*-q"
by (metis assms(1) nat_test_def pre_lower_bound_left tests_dual.sub_sup_closed while_post)
thus ?thesis
using 1 3 by (smt (verit, del_insts) leq_def tests_dual.sub_associative assms(1) nat_test_def pre_closed sub_mult_closed)
qed

lemma nat_test_pre_2:
assumes "nat_test t s"
and "-r ≤ s"
and "∀n . t n*-p ≤ x«pSum t n"
shows "-r ≤ -p⋆x«1"
proof -
have 1: "-r ≤ -p⋆x«--p*s"
by (smt (verit, ccfv_threshold) assms leq_def nat_test_def nat_test_pre_1 pSum_below_sum pSum_test_nat tests_dual.sub_associative tests_dual.sub_commutative)
have "-p⋆x«--p*s ≤ -p⋆x«1"
by (metis assms(1) nat_test_def pre_below_pre_one while_post)
thus ?thesis
using 1 by (smt (verit) assms(1) nat_test_def pre_closed tests_dual.sba_dual.top_double_complement while_post tests_dual.transitive)
qed

lemma nat_test_pre_3:
assumes "nat_test t s"
and "-q ≤ s"
and "∀n . t n*-p*-q ≤ x«pSum t n*-q"
shows "-q ≤ -p⋆x«1"
proof -
have "-p⋆x«--p*-q ≤ -p⋆x«1"
by (metis pre_below_pre_one sub_mult_closed)
thus ?thesis
by (smt (verit, ccfv_threshold) assms pre_closed tests_dual.sba_dual.top_double_complement tests_dual.sba_dual.transitive tests_dual.sub_sup_closed nat_test_pre)
qed

definition aL :: "'a"
where "aL ≡ 1⋆1«1"

lemma aL_test:
"aL = --aL"
by (metis aL_def one_def pre_closed)

end

class atoms = tests +
fixes Atomic_program :: "'a set"
fixes Atomic_test :: "'a set"
assumes one_atomic_program: "1 ∈ Atomic_program"
assumes zero_atomic_test: "bot ∈ Atomic_test"
assumes atomic_test_test: "p ∈ Atomic_test ⟶ p = --p"

class while_program = whiledo + atoms + power
begin

inductive_set Test_expression :: "'a set"
where atom_test: "p ∈ Atomic_test ⟹ p ∈ Test_expression"
| neg_test:  "p ∈ Test_expression ⟹ -p ∈ Test_expression"
| conj_test: "p ∈ Test_expression ⟹ q ∈ Test_expression ⟹ p*q ∈ Test_expression"

lemma test_expression_test:
"p ∈ Test_expression ⟹ p = --p"
apply (induct rule: Test_expression.induct)
apply simp
by (metis tests_dual.sub_sup_closed)

lemma disj_test:
"p ∈ Test_expression ⟹ q ∈ Test_expression ⟹ p⊔q ∈ Test_expression"
by (smt conj_test neg_test tests_dual.sub_inf_def test_expression_test)

lemma zero_test_expression:
"bot ∈ Test_expression"

lemma one_test_expression:
"1 ∈ Test_expression"
using Test_expression.simps tests_dual.sba_dual.one_def zero_test_expression by blast

lemma pSum_test_expression:
"(∀n . t n ∈ Test_expression) ⟹ pSum t m ∈ Test_expression"
apply (induct m)

inductive_set While_program :: "'a set"
where atom_prog:  "x ∈ Atomic_program ⟹ x ∈ While_program"
| seq_prog:   "x ∈ While_program ⟹ y ∈ While_program ⟹ x*y ∈ While_program"
| cond_prog:  "p ∈ Test_expression ⟹ x ∈ While_program ⟹ y ∈ While_program ⟹ x⊲p⊳y ∈ While_program"
| while_prog: "p ∈ Test_expression ⟹ x ∈ While_program ⟹ p⋆x ∈ While_program"

lemma one_while_program:
"1 ∈ While_program"

lemma power_while_program:
"x ∈ While_program ⟹ x^m ∈ While_program"
apply (induct m)

inductive_set Pre_expression :: "'a set"
where test_pre: "p ∈ Test_expression ⟹ p ∈ Pre_expression"
| neg_pre:  "p ∈ Pre_expression ⟹ -p ∈ Pre_expression"
| conj_pre: "p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ p*q ∈ Pre_expression"
| pre_pre:  "p ∈ Pre_expression ⟹ x ∈ While_program ⟹ x«p ∈ Pre_expression"

lemma pre_expression_test:
"p ∈ Pre_expression ⟹ p = --p"
apply (induct rule: Pre_expression.induct)
apply simp
apply (metis sub_mult_closed)
by (metis pre_closed)

lemma disj_pre:
"p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ p⊔q ∈ Pre_expression"
by (smt conj_pre neg_pre tests_dual.sub_inf_def pre_expression_test)

lemma zero_pre_expression:
"bot ∈ Pre_expression"

lemma one_pre_expression:
"1 ∈ Pre_expression"

lemma pSum_pre_expression:
"(∀n . t n ∈ Pre_expression) ⟹ pSum t m ∈ Pre_expression"
apply (induct m)

lemma aL_pre_expression:
"aL ∈ Pre_expression"
by (simp add: Pre_expression.pre_pre While_program.while_prog aL_def one_pre_expression one_test_expression one_while_program)

end

class hoare_calculus = while_program + complete_tests
begin

definition tfun :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
where "tfun p x q r ≡ p ⊔ (x«q*r)"

lemma tfun_test:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ tfun p x q r = --tfun p x q r"
by (smt tfun_def sub_mult_closed pre_closed tests_dual.inf_closed)

lemma tfun_pre_expression:
"x ∈ While_program ⟹ p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ r ∈ Pre_expression ⟹ tfun p x q r ∈ Pre_expression"
by (simp add: Pre_expression.conj_pre Pre_expression.pre_pre disj_pre tfun_def)

lemma tfun_iso:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ s = --s ⟹ r ≤ s ⟹ tfun p x q r ≤ tfun p x q s"
by (smt tfun_def tests_dual.sub_sup_right_isotone pre_iso sub_mult_closed tests_dual.sub_inf_right_isotone pre_closed)

definition tseq :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ nat ⇒ 'a"
where "tseq p x q r m ≡ (tfun p x q ^ m) r"

lemma tseq_test:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ tseq p x q r m = --tseq p x q r m"
apply (induct m)
apply (smt tseq_def tfun_test power_zero_id id_def)
by (metis tseq_def tfun_test power_succ_unfold_ext)

lemma tseq_test_seq:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ test_seq (tseq p x q r)"
using test_seq_def tseq_test by auto

lemma tseq_pre_expression:
"x ∈ While_program ⟹ p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ r ∈ Pre_expression ⟹ tseq p x q r m ∈ Pre_expression"
apply (induct m)
apply (smt tseq_def id_def power_zero_id)
by (smt tseq_def power_succ_unfold_ext tfun_pre_expression)

definition tsum :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
where "tsum p x q r ≡ Sum (tseq p x q r)"

lemma tsum_test:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ tsum p x q r = --tsum p x q r"
using Sum_test tseq_test_seq tsum_def by auto

lemma t_fun_test:
"q = --q ⟹ tfun (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) = --tfun (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL))"
by (metis aL_test pre_closed tests_dual.sba_dual.double_negation tfun_def tfun_test)

lemma t_fun_pre_expression:
"x ∈ While_program ⟹ p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ tfun (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) ∈ Pre_expression"
by (simp add: Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre Pre_expression.test_pre While_program.while_prog aL_pre_expression disj_pre tfun_pre_expression)

lemma t_seq_test:
"q = --q ⟹ tseq (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) m = --tseq (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) m"
by (metis aL_test pre_closed tests_dual.sba_dual.double_negation tfun_def tfun_test tseq_test)

lemma t_seq_test_seq:
"q = --q ⟹ test_seq (tseq (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)))"
using test_seq_def t_seq_test by auto

lemma t_seq_pre_expression:
"x ∈ While_program ⟹ p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ tseq (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) m ∈ Pre_expression"
using Pre_expression.pre_pre Pre_expression.test_pre Test_expression.neg_test While_program.while_prog aL_pre_expression tfun_def tfun_pre_expression tseq_pre_expression by auto

lemma t_sum_test:
"q = --q ⟹ tsum (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) = --tsum (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL))"
using Sum_test t_seq_test_seq tsum_def by auto

definition tfun2 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
where "tfun2 p q x r s ≡ p ⊔ q*(x«r*s)"

lemma tfun2_test:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ s = --s ⟹ tfun2 p q x r s = --tfun2 p q x r s"
by (smt tfun2_def sub_mult_closed pre_closed tests_dual.inf_closed)

lemma tfun2_pre_expression:
"x ∈ While_program ⟹ p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ r ∈ Pre_expression ⟹ s ∈ Pre_expression ⟹ tfun2 p q x r s ∈ Pre_expression"
by (simp add: Pre_expression.conj_pre Pre_expression.pre_pre disj_pre tfun2_def)

lemma tfun2_iso:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ s1 = --s1 ⟹ s2 = --s2 ⟹ s1 ≤ s2 ⟹ tfun2 p q x r s1 ≤ tfun2 p q x r s2"
by (smt tfun2_def tests_dual.sub_inf_right_isotone pre_iso sub_mult_closed tests_dual.sub_sup_right_isotone pre_closed)

definition tseq2 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ nat ⇒ 'a"
where "tseq2 p q x r s m ≡ (tfun2 p q x r ^ m) s"

lemma tseq2_test:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ s = --s ⟹ tseq2 p q x r s m = --tseq2 p q x r s m"
apply (induct m)
apply (smt tseq2_def power_zero_id id_def)
by (smt tseq2_def tfun2_test power_succ_unfold_ext)

lemma tseq2_test_seq:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ s = --s ⟹ test_seq (tseq2 p q x r s)"
using test_seq_def tseq2_test by force

lemma tseq2_pre_expression:
"x ∈ While_program ⟹ p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ r ∈ Pre_expression ⟹ s ∈ Pre_expression ⟹ tseq2 p q x r s m ∈ Pre_expression"
apply (induct m)
apply (smt tseq2_def id_def power_zero_id)
by (smt tseq2_def power_succ_unfold_ext tfun2_pre_expression)

definition tsum2 :: "'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ 'a"
where "tsum2 p q x r s ≡ Sum (tseq2 p q x r s)"

lemma tsum2_test:
"p = --p ⟹ q = --q ⟹ r = --r ⟹ s = --s ⟹ tsum2 p q x r s = --tsum2 p q x r s"
using Sum_test tseq2_test_seq tsum2_def by force

lemma t_fun2_test:
"p = --p ⟹ q = --q ⟹ tfun2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) = --tfun2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL))"
by (smt (z3) aL_test pre_closed tests_dual.sub_sup_closed tfun2_def tfun2_test)

lemma t_fun2_pre_expression:
"x ∈ While_program ⟹ p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ tfun2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) ∈ Pre_expression"
by (simp add: Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre Pre_expression.test_pre While_program.while_prog aL_pre_expression disj_pre tfun2_pre_expression)

lemma t_seq2_test:
"p = --p ⟹ q = --q ⟹ tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m = --tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m"
by (smt (z3) aL_test pre_closed tests_dual.sub_sup_closed tfun2_def tfun2_test tseq2_test)

lemma t_seq2_test_seq:
"p = --p ⟹ q = --q ⟹ test_seq (tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)))"
using test_seq_def t_seq2_test by auto

lemma t_seq2_pre_expression:
"x ∈ While_program ⟹ p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m ∈ Pre_expression"
by (simp add: Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre Pre_expression.test_pre While_program.while_prog aL_pre_expression disj_pre tseq2_pre_expression)

lemma t_sum2_test:
"p = --p ⟹ q = --q ⟹ tsum2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) = --tsum2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL))"
using Sum_test t_seq2_test_seq tsum2_def by auto

lemma t_seq2_below_t_seq:
assumes "p ∈ Test_expression"
and "q ∈ Pre_expression"
shows "tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m ≤ tseq (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL)) m"
proof -
let ?t2 = "tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL))"
let ?t = "tseq (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL))"
show "?thesis"
proof (induct m)
case 0
show "?t2 0 ≤ ?t 0"
by (smt assms aL_test id_def tests_dual.upper_bound_left tests_dual.upper_bound_right tests_dual.inf_isotone power_zero_id pre_closed pre_expression_test sub_mult_closed test_pre tseq2_def tseq_def)
next
fix m
assume "?t2 m ≤ ?t m"
hence 1: "?t2 (Suc m) ≤ tfun2 (- p * q) p x (p ⋆ x « q) (?t m)"
by (smt assms power_succ_unfold_ext pre_closed pre_expression_test sub_mult_closed t_seq2_test t_seq_test test_pre tfun2_iso tseq2_def)
have "... ≤ ?t (Suc m)"
by (smt assms tests_dual.upper_bound_left tests_dual.upper_bound_right tests_dual.inf_isotone power_succ_unfold_ext pre_closed pre_expression_test sub_mult_closed t_seq_test test_pre tfun2_def tfun_def tseq_def)
thus "?t2 (Suc m) ≤ ?t (Suc m)"
using 1 by (smt (verit, del_insts) assms pre_closed pre_expression_test test_expression_test tests_dual.sba_dual.transitive tests_dual.sub_sup_closed t_seq2_test t_seq_test tfun2_test)
qed
qed

lemma t_seq2_below_t_sum:
"p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m ≤ tsum (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL))"
by (smt (verit, del_insts) Sum_upper pre_expression_test t_seq2_below_t_seq t_seq2_test t_seq_test t_sum_test test_pre test_seq_def tsum_def leq_def tests_dual.sub_associative)

lemma t_sum2_below_t_sum:
"p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ tsum2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) ≤ tsum (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL))"
by (smt Sum_least pre_expression_test t_seq2_below_t_sum t_seq2_test t_sum_test test_pre test_seq_def tsum2_def)

lemma t_seq2_below_w:
"p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m ≤ p⋆x«q"
apply (cases m)
apply (smt aL_test id_def tests_dual.upper_bound_left tests_dual.sub_sup_right_isotone tests_dual.inf_commutative tests_dual.sub_inf_right_isotone power_zero_id pre_closed pre_expression_test pre_iso sub_mult_closed test_pre tseq2_def while_pre)
by (smt tseq2_def power_succ_unfold_ext tests_dual.upper_bound_left tests_dual.sub_sup_right_isotone tests_dual.inf_commutative tests_dual.sub_inf_right_isotone pre_closed pre_expression_test pre_iso sub_mult_closed t_seq2_test test_pre tseq2_def while_pre tfun2_def)

lemma t_sum2_below_w:
"p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ tsum2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) ≤ p⋆x«q"
by (smt Sum_least pre_closed pre_expression_test t_seq2_below_w t_seq2_test_seq test_pre tsum2_def)

lemma t_sum2_w:
assumes "aL = 1"
and "p ∈ Test_expression"
and "q ∈ Pre_expression"
and "x ∈ While_program"
shows "tsum2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) = p⋆x«q"
proof -
let ?w = "p⋆x«q"
let ?s = "-p*q⊔p*(x«?w*aL)"
have "?w = tseq2 (-p*q) p x ?w ?s 0"
by (smt assms(1-3) tests_dual.sup_right_unit id_def tests_dual.inf_commutative power_zero_id pre_closed pre_expression_test sub_mult_closed test_expression_test tseq2_def while_pre)
hence "?w ≤ tsum2 (-p*q) p x ?w ?s"
by (smt assms(2,3) Sum_upper pre_expression_test t_seq2_test_seq test_pre tsum2_def)
thus ?thesis
by (smt assms(2-4) tests_dual.antisymmetric pre_closed pre_expression_test t_sum2_test t_sum2_below_w test_pre)
qed

inductive derived_hoare_triple :: "'a ⇒ 'a ⇒ 'a ⇒ bool" ("_ ⦇ _ ⦈ _" [54,54,54] 53)
where atom_trip:  "p ∈ Pre_expression ⟹ x ∈ Atomic_program ⟹ x«p⦇x⦈p"
| seq_trip:   "p⦇x⦈q ∧ q⦇y⦈r ⟹ p⦇x*y⦈r"
| cond_trip:  "p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ p*q⦇x⦈r ∧ -p*q⦇y⦈r ⟹ q⦇x⊲p⊳y⦈r"
| while_trip: "p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ test_seq t ∧ q ≤ Sum t ⟹ t 0*p*q⦇x⦈aL*q ⟹ (∀n>0 . t n*p*q⦇x⦈pSum t n*q) ⟹ q⦇p⋆x⦈-p*q"
| cons_trip:  "p ∈ Pre_expression ⟹ s ∈ Pre_expression ⟹ p ≤ q ∧ q⦇x⦈r ⟹ r ≤ s ⟹ p⦇x⦈s"

lemma derived_type:
"p⦇x⦈q ⟹ p ∈ Pre_expression ∧ q ∈ Pre_expression ∧ x ∈ While_program"
apply (induct rule: derived_hoare_triple.induct)
using While_program.seq_prog apply blast
using While_program.cond_prog apply blast
using Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.test_pre While_program.while_prog apply simp
by blast

lemma cons_pre_trip:
"p ∈ Pre_expression ⟹ q⦇y⦈r ⟹ p*q⦇y⦈r"
by (metis cons_trip derived_type Pre_expression.conj_pre pre_expression_test tests_dual.sba_dual.reflexive tests_dual.upper_bound_right)

lemma cons_post_trip:
"q ∈ Pre_expression ⟹ r ∈ Pre_expression ⟹ p⦇y⦈q*r ⟶ p⦇y⦈r"
by (metis cons_trip derived_type pre_expression_test tests_dual.sba_dual.reflexive tests_dual.upper_bound_right)

definition valid_hoare_triple :: "'a ⇒ 'a ⇒ 'a ⇒ bool" ("_ ⟨ _ ⟩ _" [54,54,54] 53)
where "p⟨x⟩q ≡ (p ∈ Pre_expression ∧ q ∈ Pre_expression ∧ x ∈ While_program ∧ p ≤ x«q)"

end

class hoare_calculus_sound = hoare_calculus +
assumes while_soundness: "-p*-q ≤ x«-q ⟶ aL*-q ≤ -p⋆x«-q"
begin

lemma while_soundness_0:
"-p*-q ≤ x«-q ⟹ -q*aL ≤ -p⋆x«--p*-q"
by (smt while_soundness aL_test sub_comm while_post)

lemma while_soundness_1:
assumes "test_seq t"
and "-q ≤ Sum t"
and "t 0*-p*-q ≤ x«aL*-q"
and "∀n>0 . t n*-p*-q ≤ x«pSum t n*-q"
shows "-q ≤ -p⋆x«--p*-q"
proof -
have "∀n . t n*-p*-q ≤ x«-q"
proof
fix n
show "t n*-p*-q ≤ x«-q"
proof (cases n)
case 0
thus ?thesis
by (smt (z3) assms(1) assms(3) aL_test leq_def pre_closed pre_lower_bound_right test_seq_def tests_dual.sub_associative tests_dual.sub_sup_closed)
next
case (Suc m)
hence 1: "t n*-p*-q ≤ x«pSum t n*-q"
using assms(4) by blast
have "x«pSum t n*-q ≤ x«-q"
by (metis assms(1) pSum_test pre_lower_bound_right)
thus ?thesis
using 1 by (smt (verit, del_insts) assms(1) pSum_test pre_closed sub_mult_closed test_seq_def leq_def tests_dual.sub_associative)
qed
qed
hence 2: "-p*-q ≤ x«-q"
by (smt assms(1,2) Sum_test leq_def mult_right_dist_Sum pre_closed sub_assoc sub_comm sub_mult_closed test_seq_def)
have "∀n . t n*-q ≤ -p⋆x«--p*-q ∧ pSum t n*-q ≤ -p⋆x«--p*-q"
proof
fix n
show "t n*-q ≤ -p⋆x«--p*-q ∧ pSum t n*-q ≤ -p⋆x«--p*-q"
proof (induct n rule: nat_less_induct)
fix n
assume 3: "∀m<n . t m*-q ≤ -p⋆x«--p*-q ∧ pSum t m*-q ≤ -p⋆x«--p*-q"
have 4: "pSum t n*-q ≤ -p⋆x«--p*-q"
proof (cases n)
case 0
thus ?thesis
by (metis pSum.simps(1) pre_closed sub_mult_closed tests_dual.top_greatest tests_dual.sba_dual.less_eq_inf tests_dual.top_double_complement)
next
case (Suc m)
hence "pSum t n*-q = (pSum t m ⊔ t m)*-q"
by simp
also have "... = pSum t m*-q ⊔ t m*-q"
by (metis (full_types) assms(1) pSum_test test_seq_def tests_dual.sup_right_dist_inf)
also have "... ≤ -p⋆x«--p*-q"
proof -
have "pSum t m*-q = --(pSum t m*-q) ∧ t m*-q = --(t m*-q) ∧ -p⋆x«--p*-q = --(-p⋆x«--p*-q)"
apply (intro conjI)
apply (metis assms(1) pSum_test tests_dual.sub_sup_closed)
apply (metis assms(1) test_seq_def tests_dual.sub_sup_closed)
by (metis pre_closed tests_dual.sub_sup_closed)
thus ?thesis
using 3 by (smt (z3) lessI Suc tests_dual.greatest_lower_bound sub_mult_closed)
qed
finally show ?thesis
.
qed
hence 5: "x«pSum t n*-q ≤ x«-p⋆x«--p*-q"
by (smt assms pSum_test pre_closed pre_iso sub_mult_closed)
have 6: "-p*(t n*-q) ≤ -p*(-p⋆x«--p*-q)"
proof (cases n)
case 0
thus ?thesis
using 2 by (smt assms(1,3) aL_test leq_def tests_dual.sup_idempotent tests_dual.sub_sup_right_isotone pre_closed pre_lower_bound_left sub_assoc sub_comm sub_mult_closed test_seq_def transitive while_pre_then while_soundness_0)
next
case (Suc m)
hence "-p*(t n*-q) ≤ x«pSum t n*-q"
by (smt assms(1,4) test_seq_def tests_dual.sub_associative tests_dual.sub_commutative zero_less_Suc)
hence "-p*(t n*-q) ≤ x«-p⋆x«--p*-q"
using 5 by (smt assms(1) tests_dual.least_upper_bound pSum_test pre_closed sub_mult_closed test_seq_def leq_def)
hence "-p*(t n*-q) ≤ -p*(x«-p⋆x«--p*-q)"
by (smt assms(1) tests_dual.upper_bound_left pre_closed sub_mult_closed test_seq_def leq_def tests_dual.sub_associative)
thus ?thesis
using while_post while_pre_then by auto
qed
have "--p*(t n*-q) ≤ --p*(-p⋆x«--p*-q)"
by (smt assms(1) leq_def tests_dual.upper_bound_right sub_assoc sub_comm sub_mult_closed test_seq_def while_pre_else)
thus "t n*-q ≤ -p⋆x«--p*-q ∧ pSum t n*-q ≤ -p⋆x«--p*-q"
using 4 6 by (smt assms(1) tests_dual.sup_less_eq_cases_2 pre_closed sub_mult_closed test_seq_def)
qed
qed
thus ?thesis
by (smt assms(1,2) Sum_test leq_def mult_right_dist_Sum pre_closed sub_comm sub_mult_closed)
qed

lemma while_soundness_2:
assumes "test_seq t"
and "-r ≤ Sum t"
and "∀n . t n*-p ≤ x«pSum t n"
shows "-r ≤ -p⋆x«1"
proof -
have 1: "∀n>0 . t n*-p*Sum t ≤ x«pSum t n*Sum t"
by (smt (z3) assms(1,3) Sum_test Sum_upper leq_def pSum_below_Sum pSum_test test_seq_def tests_dual.sub_associative tests_dual.sub_commutative)
have 2: "t 0*-p*Sum t ≤ x«bot"
by (smt assms(1,3) Sum_test Sum_upper leq_def sub_assoc sub_comm test_seq_def pSum.simps(1))
have "x«bot ≤ x«aL*Sum t"
by (smt assms(1) Sum_test aL_test pre_iso sub_mult_closed tests_dual.top_double_complement tests_dual.top_greatest)
hence "t 0*-p*Sum t ≤ x«aL*Sum t"
using 2 by (smt (z3) assms(1) Sum_test aL_test leq_def pSum.simps(1) pSum_test pre_closed test_seq_def tests_dual.sub_associative tests_dual.sub_sup_closed)
hence 3: "Sum t ≤ -p⋆x«--p*Sum t"
using 1 by (smt (verit, del_insts) assms(1) Sum_test tests_dual.sba_dual.one_def tests_dual.sup_right_unit tests_dual.upper_bound_left while_soundness_1)
have "-p⋆x«--p*Sum t ≤ -p⋆x«1"
by (metis assms(1) Sum_test pre_below_pre_one tests_dual.sub_sup_closed)
hence "Sum t ≤ -p⋆x«1"
using 3 by (smt (z3) assms(1) Sum_test pre_closed tests_dual.sba_dual.one_def while_post tests_dual.transitive)
thus ?thesis
by (smt (z3) assms(1,2) Sum_test pre_closed tests_dual.sba_dual.one_def tests_dual.transitive)
qed

theorem soundness:
"p⦇x⦈q ⟹ p⟨x⟩q"
apply (induct rule: derived_hoare_triple.induct)
apply (metis Pre_expression.pre_pre While_program.atom_prog pre_expression_test tests_dual.sba_dual.reflexive valid_hoare_triple_def)
apply (metis valid_hoare_triple_def pre_expression_test pre_compose While_program.seq_prog)
apply (metis valid_hoare_triple_def ite_import_mult pre_expression_test cond_prog test_pre)
apply (smt (verit, del_insts) Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.test_pre While_program.while_prog pre_expression_test valid_hoare_triple_def while_soundness_1)
by (metis pre_expression_test pre_iso pre_pre tests_dual.sba_dual.transitive valid_hoare_triple_def)

end

class hoare_calculus_pre_complete = hoare_calculus +
assumes aL_pre_import: "(x«-q)*aL ≤ x«-q*aL"
assumes pre_right_dist_Sum: "x ∈ While_program ∧ ascending_chain t ∧ test_seq t ⟶ x«Sum t = Sum (λn . x«t n)"
begin

lemma aL_pre_import_equal:
"(x«-q)*aL = (x«-q*aL)*aL"
proof -
have 1: "(x«-q)*aL ≤ (x«-q*aL)*aL"
by (smt (z3) aL_pre_import aL_test pre_closed tests_dual.sub_sup_closed tests_dual.least_upper_bound tests_dual.upper_bound_right)
have "(x«-q*aL)*aL ≤ (x«-q)*aL"
by (smt (verit, ccfv_threshold) aL_test pre_closed pre_lower_bound_left tests_dual.sba_dual.inf_isotone tests_dual.sba_dual.reflexive tests_dual.sub_sup_closed)
thus ?thesis
using 1 by (smt (z3) tests_dual.antisymmetric aL_test pre_closed tests_dual.sub_sup_closed)
qed

lemma aL_pre_below_t_seq2:
assumes "p ∈ Test_expression"
and "q ∈ Pre_expression"
shows "(p⋆x«q)*aL ≤ tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) 0"
proof (unfold tseq2_def power_zero_id id_def while_pre)
have "(p⋆x«q)*aL = (p*(x«p⋆x«q) ⊔ -p*q)*aL"
by (metis assms while_pre test_pre pre_expression_test)
also have "... = p*(x«p⋆x«q)*aL ⊔ -p*q*aL"
by (smt (z3) assms aL_test tests_dual.sup_right_dist_inf pre_closed pre_expression_test sub_mult_closed test_pre)
also have "... = p*((x«p⋆x«q)*aL) ⊔ -p*q*aL"
by (smt assms aL_test pre_closed pre_expression_test test_pre sub_assoc)
also have "... ≤ p*(x«(p⋆x«q)*aL) ⊔ -p*q"
proof -
have 1: "(x«p⋆x«q)*aL ≤ x«(p⋆x«q)*aL"
by (metis assms(2) pre_closed pre_expression_test aL_pre_import)
have "-p*q*aL ≤ -p*q"
by (metis assms(2) aL_test pre_expression_test tests_dual.sub_sup_closed tests_dual.upper_bound_left)
thus ?thesis
using 1 by (smt assms aL_test pre_closed pre_expression_test test_pre tests_dual.sub_sup_closed tests_dual.sub_sup_right_isotone tests_dual.inf_isotone)
qed
also have "... = -p*q ⊔ p*(x«(p⋆x«q)*aL)"
by (smt assms aL_test tests_dual.inf_commutative pre_closed pre_expression_test test_pre tests_dual.sub_sup_closed)
finally show "(p⋆x«q)*aL ≤ -p*q ⊔ p*(x«(p⋆x«q)*aL)"
.
qed

lemma t_seq2_ascending:
assumes "p ∈ Test_expression"
and "q ∈ Pre_expression"
and "x ∈ While_program"
shows "tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) m ≤ tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)) (Suc m)"
proof (induct m)
let ?w = "p⋆x«q"
let ?r = "-p*q⊔p*(x«?w*aL)"
case 0
have 1: "?w*aL = --(?w*aL)"
by (simp add: assms Pre_expression.conj_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression pre_expression_test)
have 2: "?r = --?r"
by (simp add: assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre Pre_expression.test_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test)
have "?w*aL ≤ ?r"
by (metis aL_pre_below_t_seq2 assms(1,2) id_def tseq2_def power_zero_id)
hence "?w*aL ≤ ?w*?r"
using 1 2 by (smt (verit, ccfv_threshold) assms Pre_expression.pre_pre While_program.while_prog aL_test pre_expression_test tests_dual.sub_associative tests_dual.sub_sup_right_isotone tests_dual.sba_dual.less_eq_inf tests_dual.sba_dual.reflexive)
hence "x«?w*aL ≤ x«(?w*?r)"
by (smt (verit, ccfv_threshold) assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test pre_iso test_pre)
hence "p*(x«?w*aL) ≤ p*(x«(?w*?r))"
by (smt (z3) assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test test_pre tests_dual.sub_sup_right_isotone)
hence "?r ≤ -p*q⊔p*(x«(?w*?r))"
by (smt (verit, del_insts) assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test test_pre tests_dual.sba_dual.reflexive tests_dual.inf_isotone)
thus ?case
by (unfold tseq2_def power_zero_id power_succ_unfold_ext id_def tfun2_def)
next
let ?w = "p⋆x«q"
let ?r = "-p*q⊔p*(x«?w*aL)"
let ?t = "tseq2 (-p*q) p x ?w ?r"
case (Suc m)
hence "?w*?t m ≤ ?w*?t (Suc m)"
by (smt (z3) assms(1,2) pre_closed pre_expression_test t_seq2_test test_expression_test tests_dual.sub_sup_right_isotone)
hence "x«?w*?t m ≤ x«?w*?t (Suc m)"
by (smt (z3) assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test pre_iso test_pre tseq2_pre_expression)
hence "p*(x«?w*?t m) ≤ p*(x«?w*?t (Suc m))"
by (smt (z3) assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test test_pre tests_dual.sub_sup_right_isotone tseq2_pre_expression)
hence "-p*q⊔p*(x«?w*?t m) ≤ -p*q⊔p*(x«?w*?t (Suc m))"
by (smt (z3) assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test test_pre tests_dual.sba_dual.reflexive tests_dual.inf_isotone tseq2_pre_expression)
thus ?case
by (smt tseq2_def power_succ_unfold_ext tfun2_def)
qed

lemma t_seq2_ascending_chain:
"p ∈ Test_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ ascending_chain (tseq2 (-p*q) p x (p⋆x«q) (-p*q⊔p*(x«(p⋆x«q)*aL)))"

end

class hoare_calculus_complete = hoare_calculus_pre_complete +
assumes while_completeness: "-p*(x«-q) ≤ -q ⟶ -p⋆x«-q ≤ -q⊔aL"
begin

lemma while_completeness_var:
assumes "-p*(x«-q)⊔-r ≤ -q"
shows "-p⋆x«-r ≤ -q⊔aL"
proof -
have 1: "-p⋆x«-q ≤ -q⊔aL"
by (smt assms pre_closed tests_dual.sub_sup_closed tests_dual.greatest_lower_bound while_completeness)
have "-p⋆x«-r ≤ -p⋆x«-q"
by (smt assms pre_closed tests_dual.sub_sup_closed tests_dual.greatest_lower_bound pre_iso)
thus ?thesis
using 1 by (smt (z3) aL_test pre_closed tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.transitive)
qed

lemma while_completeness_sum:
assumes "p ∈ Test_expression"
and "q ∈ Pre_expression"
and "x ∈ While_program"
shows "p⋆x«q ≤ tsum (-p) x (p⋆x«q) (-p⊔(x«(p⋆x«q)*aL))"
proof -
let ?w = "p⋆x«q"
let ?r = "-p*q⊔p*(x«?w*aL)"
let ?t = "tseq2 (-p*q) p x ?w ?r"
let ?ts = "tsum2 (-p*q) p x ?w ?r"
have 1: "?w = --?w"
by (metis assms(2) pre_expression_test pre_closed)
have 2: "?r = --?r"
by (simp add: assms Pre_expression.conj_pre Pre_expression.neg_pre Pre_expression.pre_pre Pre_expression.test_pre While_program.while_prog aL_pre_expression disj_pre pre_expression_test)
have 3: "?ts = --?ts"
by (meson assms(1) assms(2) pre_expression_test t_sum2_test test_expression_test)
have 4: "test_seq ?t"
by (simp add: assms(1) assms(2) pre_expression_test t_seq2_test_seq test_expression_test)
have "-p*q ≤ ?r"
by (smt (z3) assms(1,2) aL_test pre_closed pre_expression_test sub_mult_closed test_pre tests_dual.lower_bound_left)
hence 5: "-p*q ≤ ?ts"
using 1 2 3 by (smt assms Sum_upper id_def tests_dual.sba_dual.transitive power_zero_id pre_expression_test sub_mult_closed test_pre tseq2_def tseq2_test_seq tsum2_def)
have "∀n . p*(x«?t n) ≤ ?ts"
proof (rule allI, unfold tsum2_def)
fix n
have 6: "p*(x«?t n) ≤ ?t (Suc n)"
using 4 by (smt assms leq_def power_succ_unfold_ext pre_closed pre_expression_test tests_dual.sub_commutative sub_mult_closed t_seq2_below_w test_pre test_seq_def tfun2_def tseq2_def tests_dual.lower_bound_right)
have "?t (Suc n) ≤ Sum ?t"
using 4 Sum_upper by auto
thus "p*(x«?t n) ≤ Sum ?t"
using 3 4 6 by (smt assms(1) pre_closed pre_expression_test sub_mult_closed test_pre test_seq_def tests_dual.transitive tsum2_def)
qed
hence "p*(x«?ts) ≤ ?ts"
using 3 4 by (smt assms mult_left_dist_Sum pre_closed pre_right_dist_Sum t_seq2_ascending_chain test_expression_test test_seq_def tsum2_def)
hence "p*(x«?ts)⊔-p*q ≤ ?ts"
using 3 5 by (smt assms(1,2) tests_dual.greatest_lower_bound pre_closed pre_expression_test sub_mult_closed test_pre)
hence "?w ≤ ?ts⊔aL"
using 1 3 by (smt assms(1,2) pre_expression_test while_post sub_mult_closed t_sum2_below_t_sum t_sum_test test_pre transitive while_completeness_var)
hence "?w = ?w*(?ts⊔aL)"
using 1 3 by (smt aL_test tests_dual.sba_dual.less_eq_inf tests_dual.sba_dual.sub_sup_closed)
also have "... = ?w*?ts⊔?w*aL"
using 1 3 by (smt aL_test tests_dual.sup_left_dist_inf)
also have "... ≤ ?ts⊔?t 0"
using 1 3 4 by (smt (z3) assms(1,2) aL_pre_below_t_seq2 tests_dual.upper_bound_right aL_test test_seq_def tests_dual.sub_sup_closed tests_dual.inf_isotone)
also have "... = ?ts"
using 3 4 by (smt Sum_upper tsum2_def test_seq_def tests_dual.less_eq_inf)
finally have "?w ≤ ?ts"
.
thus ?thesis
using 1 3 by (metis assms t_sum2_below_t_sum t_sum2_below_w tests_dual.antisymmetric)
qed

lemma while_complete:
assumes "p ∈ Test_expression"
and "q ∈ Pre_expression"
and "x ∈ While_program"
and "∀r∈Pre_expression . x«r⦇x⦈r"
shows "p⋆x«q⦇p⋆x⦈q"
proof -
let ?w = "p⋆x«q"
let ?t = "tseq (-p) x ?w (-p⊔(x«?w*aL))"
have 1: "?w ∈ Pre_expression"
by (simp add: assms(1-3) Pre_expression.pre_pre While_program.while_prog)
have 2: "test_seq ?t"
by (simp add: assms(2) pre_expression_test t_seq_test_seq)
hence 3: "?w ≤ Sum ?t"
using assms(1-3) tsum_def while_completeness_sum by auto
have 4: "p = --p"
have "x«?w*aL = --(x«?w*aL)"
using 1 by (simp add: assms(3) Pre_expression.conj_pre Pre_expression.pre_pre aL_pre_expression pre_expression_test)
hence 5: "(-p⊔(x«?w*aL))*p = (x«?w*aL)*p"
using 4 by (metis tests_dual.sba_dual.inf_complement_intro)
have "x«aL*?w⦇x⦈aL*?w"
using 1 by (simp add: assms(4) Pre_expression.conj_pre aL_pre_expression)
hence "x«?w*aL⦇x⦈aL*?w"
using 1 by (metis aL_test pre_expression_test sub_comm)
hence "(x«?w*aL)*p*?w⦇x⦈aL*?w"
using 1 by (smt (z3) assms(1) Pre_expression.conj_pre Pre_expression.test_pre derived_hoare_triple.cons_trip derived_type pre_expression_test sub_assoc tests_dual.sba_dual.reflexive tests_dual.upper_bound_left)
hence "(-p⊔(x«?w*aL))*p*?w⦇x⦈aL*?w"
using 5 by simp
hence 6: "?t 0*p*?w⦇x⦈aL*?w"
by (unfold tseq_def power_zero_id id_def)
have "∀n>0 . ?t n*p*?w⦇x⦈pSum ?t n*?w"
proof (rule allI, rule impI)
fix n
assume "0<(n::nat)"
from this obtain m where 7: "n = Suc m"
hence "?t m*?w ≤ pSum ?t n*?w"
using 1 2 by (smt pSum.simps(2) pSum_test pre_expression_test test_seq_def tests_dual.lower_bound_right tests_dual.sba_dual.inf_isotone tests_dual.sba_dual.reflexive)
thus "?t n*p*?w⦇x⦈pSum ?t n*?w"
using 1 7 by (smt assms conj_pre cons_trip tests_dual.upper_bound_left tests_dual.sba_dual.inf_complement_intro pSum_pre_expression power_succ_unfold_ext pre_closed pre_expression_test sub_assoc sub_comm t_seq_pre_expression test_pre tfun_def tseq_def)
qed
hence "?w⦇p⋆x⦈-p*?w"
using 1 2 3 6 assms while_trip by auto
hence "?w⦇p⋆x⦈-p*q"
using 4 by (metis assms(2) while_pre_else pre_expression_test while_pre_else)
thus ?thesis
using assms(1,2) Pre_expression.neg_pre Pre_expression.test_pre cons_post_trip by blast
qed

lemma pre_completeness:
"x ∈ While_program ⟹ q ∈ Pre_expression ⟹ x«q⦇x⦈q"
apply (induct arbitrary: q rule: While_program.induct)
apply (metis pre_pre pre_seq seq_trip pre_expression_test)
apply (smt cond_prog cond_trip cons_pre_trip ite_pre_else ite_pre_then neg_pre pre_pre pre_expression_test test_pre)

theorem completeness:
"p⟨x⟩q ⟹ p⦇x⦈q"
by (metis valid_hoare_triple_def pre_completeness tests_dual.reflexive pre_expression_test cons_trip)

end

class hoare_calculus_sound_complete = hoare_calculus_sound + hoare_calculus_complete
begin

text ‹Theorem 41›

theorem soundness_completeness:
"p⦇x⦈q ⟷ p⟨x⟩q"
using completeness soundness by blast

end

class hoare_rules = whiledo + complete_tests + hoare_triple +
assumes rule_pre:   "x«-q⦃x⦄-q"
assumes rule_seq:   "-p⦃x⦄-q ∧ -q⦃y⦄-r ⟶ -p⦃x*y⦄-r"
assumes rule_cond:  "-p*-q⦃x⦄-r ∧ --p*-q⦃y⦄-r ⟶ -q⦃x⊲-p⊳y⦄-r"
assumes rule_while: "test_seq t ∧ -q ≤ Sum t ∧ t 0*-p*-q⦃x⦄aL*-q ∧ (∀n>0 . t n*-p*-q⦃x⦄pSum t n*-q) ⟶ -q⦃-p⋆x⦄--p*-q"
assumes rule_cons:  "-p ≤ -q ∧ -q⦃x⦄-r ∧ -r ≤ -s ⟶ -p⦃x⦄-s"
assumes rule_disj:  "-p⦃x⦄-r ∧ -q⦃x⦄-s ⟶ -p⊔-q⦃x⦄-r⊔-s"
begin

lemma rule_cons_pre:
"-p ≤ -q ⟹ -q⦃x⦄-r ⟹ -p⦃x⦄-r"
using rule_cons tests_dual.sba_dual.reflexive by blast

lemma rule_cons_pre_mult:
"-q⦃x⦄-r ⟹ -p*-q⦃x⦄-r"
by (metis tests_dual.sub_sup_closed rule_cons_pre tests_dual.upper_bound_right)

lemma rule_cons_pre_plus:
"-p⊔-q⦃x⦄-r ⟹ -p⦃x⦄-r"
by (metis tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.upper_bound_left rule_cons_pre)

lemma rule_cons_post:
"-q⦃x⦄-r ⟹ -r ≤ -s ⟹ -q⦃x⦄-s"
using rule_cons tests_dual.sba_dual.reflexive by blast

lemma rule_cons_post_mult:
"-q⦃x⦄-r*-s ⟹ -q⦃x⦄-s"
by (metis rule_cons_post tests_dual.upper_bound_left sub_comm sub_mult_closed)

lemma rule_cons_post_plus:
"-q⦃x⦄-r ⟹ -q⦃x⦄-r⊔-s"
by (metis tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.upper_bound_left rule_cons_post)

lemma rule_disj_pre:
"-p⦃x⦄-r ⟹ -q⦃x⦄-r ⟹ -p⊔-q⦃x⦄-r"
by (metis rule_disj tests_dual.sba_dual.sup_idempotent)

end

class hoare_calculus_valid = hoare_calculus_sound_complete + hoare_triple +
assumes hoare_triple_valid: "-p⦃x⦄-q ⟷ -p ≤ x«-q"
begin

lemma valid_hoare_triple_same:
"p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ p⦃x⦄q = p⟨x⟩q"
by (metis valid_hoare_triple_def hoare_triple_valid pre_expression_test)

lemma derived_hoare_triple_same:
"p ∈ Pre_expression ⟹ q ∈ Pre_expression ⟹ x ∈ While_program ⟹ p⦃x⦄q = p⦇x⦈q"

lemma valid_rule_disj:
assumes "-p⦃x⦄-r"
and "-q⦃x⦄-s"
shows "-p⊔-q⦃x⦄-r⊔-s"
proof -
have "x«-r ≤ x«-r⊔-s ∧ x«-s ≤ x«-r⊔-s"
by (metis pre_iso tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.upper_bound_left tests_dual.sba_dual.upper_bound_right)
thus ?thesis
by (smt assms hoare_triple_valid tests_dual.greatest_lower_bound tests_dual.sba_dual.sub_sup_closed pre_closed tests_dual.transitive)
qed

subclass hoare_rules
apply unfold_locales
apply (metis hoare_triple_valid pre_closed tests_dual.sba_dual.reflexive)
apply (meson hoare_triple_valid pre_compose)
apply (smt hoare_triple_valid ite_import_mult sub_mult_closed)
apply (smt (verit, del_insts) hoare_triple_valid aL_test pSum_test sba_dual.sub_sup_closed sub_mult_closed test_seq_def while_soundness_1)
apply (smt hoare_triple_valid pre_iso tests_dual.transitive pre_closed)

lemma nat_test_rule_while:
"nat_test t s ⟹ -q ≤ s ⟹ (∀n . t n*-p*-q⦃x⦄pSum t n*-q) ⟹ -q⦃-p⋆x⦄--p*-q"
by (smt (verit, ccfv_threshold) hoare_triple_valid nat_test_def nat_test_pre pSum_test_nat sub_mult_closed)

lemma test_seq_rule_while:
"test_seq t ⟹ -q ≤ Sum t ⟹ t 0*-p*-q⦃x⦄aL*-q ⟹ (∀n>0 . t n*-p*-q⦃x⦄pSum t n*-q) ⟹ -q⦃-p⋆x⦄--p*-q"
by (smt (verit, del_insts) hoare_triple_valid aL_test pSum_test sub_mult_closed test_seq_def while_soundness_1)

lemma rule_bot:
"bot⦃x⦄-p"
by (metis hoare_triple_valid pre_closed tests_dual.top_double_complement tests_dual.top_greatest)

lemma rule_skip:
"-p⦃1⦄-p"

lemma rule_example_4:
assumes "test_seq t"
and "Sum t = 1"
and "t 0*-p1*-p3 = bot"
and "-p1⦃z1⦄-p1*-p2"
and "∀n>0 . t n*-p1*-p2*-p3⦃z2⦄pSum t n*-p1*-p2"
shows "-p1⦃z1*(-p3⋆z2)⦄-p2*--p3"
proof -
have "t 0*-p3*(-p1*-p2) = bot"
by (smt (verit, ccfv_threshold) assms(1,3) sub_assoc sub_comm sub_mult_closed test_seq_def tests_dual.sup_right_zero)
hence 1: "t 0*-p3*(-p1*-p2)⦃z2⦄aL*(-p1*-p2)"
by (metis aL_test sub_mult_closed rule_bot)
have "∀n>0 . t n*-p3*(-p1*-p2)⦃z2⦄pSum t n*(-p1*-p2)"
by (smt assms(1,5) lower_bound_left pSum_test rule_cons_pre sub_assoc sub_comm sub_mult_closed test_seq_def)
hence "-p1*-p2⦃-p3⋆z2⦄--p3*(-p1*-p2)"
using 1 by (smt (verit, del_insts) assms(1,2) tests_dual.sub_bot_least rule_while sub_mult_closed)
thus ?thesis
by (smt assms(4) tests_dual.upper_bound_left rule_cons_post rule_seq sub_assoc sub_comm sub_mult_closed)
qed

end

class hoare_calculus_pc_2 = hoare_calculus_sound + hoare_calculus_pre_complete +
assumes aL_one: "aL = 1"
begin

subclass hoare_calculus_sound_complete
apply unfold_locales

lemma while_soundness_pc:
assumes "-p*-q ≤ x«-q"
shows "-q ≤ -p⋆x«--p*-q"
proof -
let ?t = "λx . 1"
have 1: "test_seq ?t"
hence 2: "-q ≤ Sum ?t"
by (metis Sum_test Sum_upper tests_dual.sba_dual.one_def tests_dual.antisymmetric tests_dual.sub_bot_least)
have 3: "?t 0*-p*-q ≤ x«aL*-q"
using 1 by (simp add: assms aL_one)
have "∀n>0 . ?t n*-p*-q ≤ x«pSum ?t n*-q"
using 1 by (metis assms pSum_test pSum_upper tests_dual.sba_dual.one_def tests_dual.antisymmetric tests_dual.sub_bot_least tests_dual.sup_left_unit)
thus ?thesis
using 1 2 3 aL_one while_soundness_0 by auto
qed

end

class hoare_calculus_pc = hoare_calculus_sound + hoare_calculus_pre_complete +
assumes pre_one_one: "x«1 = 1"
begin

subclass hoare_calculus_pc_2
apply unfold_locales

end

class hoare_calculus_pc_valid = hoare_calculus_pc + hoare_calculus_valid
begin

lemma rule_while_pc:
"-p*-q⦃x⦄-q ⟹ -q⦃-p⋆x⦄--p*-q"
by (metis hoare_triple_valid sub_mult_closed while_soundness_pc)

lemma rule_alternation:
"-p⦃x⦄-q ⟹ -q⦃y⦄-p ⟹ -p⦃-r⋆x*y⦄--r*-p"
by (meson rule_cons_pre_mult rule_seq rule_while_pc)

lemma rule_alternation_context:
"-p⦃v⦄-p ⟹ -p⦃w⦄-q ⟹ -q⦃x⦄-q ⟹ -q⦃y⦄-p ∧ -p⦃z⦄-p ⟹ -p⦃-r⋆v*w*x*y*z⦄--r*-p"
by (meson rule_cons_pre_mult rule_seq rule_while_pc)

lemma rule_example_3:
assumes "-p*-q⦃x⦄--p*-q"
and "--p*-r⦃x⦄-p*-r"
and "-p*-r⦃y⦄-p*-q"
and "--p*-q⦃z⦄--p*-r"
shows "-p*-q⊔--p*-r⦃-s⋆x*(y⊲-p⊳z)⦄--s*(-p*-q⊔--p*-r)"
proof -
have t1: "-p*-q⊔--p*-r⦃x⦄--p*-q⊔-p*-r"
by (smt assms(1,2) rule_disj sub_mult_closed)
have "-p*-r⦃y⦄-p*-q⊔--p*-r"
by (smt assms(3) ```