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"
      by (simp add: assms(1) pSum_below_sum)
    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"
      by (simp add: assms(4))
    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 add: atomic_test_test)
  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"
  by (simp add: Test_expression.atom_test zero_atomic_test)

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)
  apply (simp add: zero_test_expression)
  by (simp add: disj_test)

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"
  by (simp add: While_program.atom_prog one_atomic_program)

lemma power_while_program:
  "x ∈ While_program ⟹ x^m ∈ While_program"
  apply (induct m)
  apply (simp add: one_while_program)
  by (simp add: While_program.seq_prog)

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 add: test_expression_test)
  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"
  by (simp add: Pre_expression.test_pre zero_test_expression)

lemma one_pre_expression:
  "1 ∈ Pre_expression"
  by (simp add: Pre_expression.test_pre one_test_expression)

lemma pSum_pre_expression:
  "(∀n . t n ∈ Pre_expression) ⟹ pSum t m ∈ Pre_expression"
  apply (induct m)
  apply (simp add: zero_pre_expression)
  by (simp add: disj_pre)

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)
  apply (simp add: Pre_expression.pre_pre While_program.atom_prog)
  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)))"
  by (simp add: ord.ascending_chain_def t_seq2_ascending)

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"
    by (simp add: assms(1) test_expression_test)
  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"
      by (auto dest: less_imp_Suc_add)
    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 (simp add: derived_hoare_triple.atom_trip)
  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)
  by (simp add: while_complete)

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"
  by (simp add: soundness_completeness valid_hoare_triple_same)

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)
  by (simp add: valid_rule_disj)

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"
  by (simp add: hoare_triple_valid pre_one_increasing)

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
  by (simp add: aL_one pre_below_one)

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"
    by (simp add: test_seq_def)
  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
  by (simp add: aL_def pre_one_one)

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) rule_cons_post_plus sub_mult_closed)
  hence t2: "-p*(--p*-q⊔-p*-r)⦃y⦄-p*-q⊔--p*-r"
    by (smt (z3) tests_dual.sba_dual.less_eq_inf tests_dual.sba_dual.reflexive tests_dual.sba_dual.sub_sup_closed tests_dual.sub_associative tests_dual.sub_sup_closed tests_dual.upper_bound_left tests_dual.wnf_lemma_3)
  have "--p*-q⦃z⦄-p*-q⊔--p*-r"
    by (smt assms(4) tests_dual.inf_commutative rule_cons_post_plus sub_mult_closed)
  hence "--p*(--p*-q⊔-p*-r)⦃z⦄-p*-q⊔--p*-r"
    by (smt (z3) tests_dual.sba_dual.one_def tests_dual.sba_dual.sup_absorb tests_dual.sba_dual.sup_complement_intro tests_dual.sba_dual.sup_right_unit tests_dual.sub_sup_closed tests_dual.sup_complement_intro tests_dual.sup_left_dist_inf tests_dual.sup_right_unit tests_dual.top_double_complement)
  hence "--p*-q⊔-p*-r⦃y⊲-p⊳z⦄-p*-q⊔--p*-r"
    using t2 by (smt tests_dual.inf_closed rule_cond sub_mult_closed)
  hence "-s*(-p*-q⊔--p*-r)⦃x*(y⊲-p⊳z)⦄-p*-q⊔--p*-r"
    using t1 by (smt tests_dual.inf_closed rule_cons_pre_mult rule_seq sub_mult_closed)
  thus ?thesis
    by (smt tests_dual.inf_closed rule_while_pc sub_mult_closed)
qed

end

class hoare_calculus_tc = hoare_calculus + precondition_test_test + precondition_distr_mult +
  assumes while_bnd: "p ∈ Test_expression ∧ q ∈ Pre_expression ∧ x ∈ While_program ⟶ p⋆x«q ≤ Sum (λn . (p*x)^n«bot)"
begin

lemma
  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 ?s = "-p⊔(x«?w*aL)"
  let ?t = "tseq (-p) x ?w ?s"
  let ?b = "λn . (p*x)^n«bot"
  have 2: "test_seq ?t"
    by (simp add: assms(2) pre_expression_test t_seq_test_seq)
  have 3: "test_seq ?b"
    using pre_closed test_seq_def tests_dual.sba_dual.complement_top by blast
  have 4: "?w = --?w"
    by (metis assms(2) pre_expression_test pre_closed)
  have "?w ≤ Sum ?b"
    using assms while_bnd by blast
  hence 5: "?w = Sum ?b*?w"
    using 3 4 by (smt Sum_test leq_def sub_comm)
  have "∀n . ?b n*?w ≤ ?t n"
  proof
    fix n
    show "?b n*?w ≤ ?t n"
    proof (induct n)
      show "?b 0*?w ≤ ?t 0"
        using 2 4 by (metis power.power_0 pre_one test_seq_def tests_dual.sup_left_zero tests_dual.top_double_complement tests_dual.top_greatest)
    next
      fix n
      assume 6: "?b n*?w ≤ ?t n"
      have "-p ≤ ?t (Suc n)"
        apply (unfold tseq_def power_succ_unfold_ext)
        by (smt assms(2) pre_expression_test t_seq_test pre_closed sub_mult_closed tfun_def tseq_def tests_dual.lower_bound_left)
      hence 7: "-p*?b (Suc n)*?w ≤ ?t (Suc n)"
        using 2 3 4 by (smt tests_dual.upper_bound_left sub_mult_closed test_seq_def tests_dual.transitive)
      have 8: "p*?b (Suc n)*?w ≤ x«?w*(?b n*?w)"
        by (smt assms(1,2) tests_dual.upper_bound_right tests_dual.sup_idempotent power_Suc pre_closed pre_distr_mult pre_expression_test pre_import_composition sub_assoc sub_comm sub_mult_closed test_expression_test while_pre_then tests_dual.top_double_complement)
      have 9: "... ≤ x«?w*?t n"
        using 2 3 4 6 by (smt tests_dual.sub_sup_right_isotone pre_iso sub_mult_closed test_seq_def)
      have "... ≤ ?t (Suc n)"
        using 2 4 by (smt power_succ_unfold_ext pre_closed sub_mult_closed test_seq_def tfun_def tseq_def tests_dual.lower_bound_right)
      hence "p*?b (Suc n)*?w ≤ ?t (Suc n)"
        using 2 3 4 8 9 by (smt assms(1) pre_closed sub_mult_closed test_expression_test test_seq_def tests_dual.transitive)
      thus "?b (Suc n)*?w ≤ ?t (Suc n)"
        using 2 3 4 7 by (smt assms(1) tests_dual.sup_less_eq_cases sub_assoc sub_mult_closed test_expression_test test_seq_def)
    qed
  qed
  hence "Sum ?b*?w ≤ tsum (-p) x ?w ?s"
    using 3 4 by (smt assms(2) Sum_upper mult_right_dist_Sum pre_expression_test sub_mult_closed t_seq_test t_sum_test test_seq_def tests_dual.transitive tsum_def)
  thus ?thesis
    using 5 by auto
qed

end

class complete_pre = complete_tests + precondition + power
begin

definition bnd :: "'a ⇒ 'a"
  where "bnd x ≡ Sup { x^n«bot | n::nat . True }"

lemma bnd_test_set:
  "test_set { x^n«bot | n::nat . True }"
  by (smt (verit, del_insts) CollectD pre_closed test_set_def tests_dual.top_double_complement)

lemma bnd_test:
  "bnd x = --bnd x"
  using bnd_def bnd_test_set sup_test by auto

lemma bnd_upper:
  "x^m«bot ≤ bnd x"
proof -
  have "x^m«bot ∈ { x^m«bot | m::nat . True }"
    by auto
  thus ?thesis
    using bnd_def bnd_test_set sup_upper by auto
qed

lemma bnd_least:
  assumes "∀n . x^n«bot ≤ -p"
    shows "bnd x ≤ -p"
proof -
  have "∀y∈{ x^n«bot | n::nat . True } . y ≤ -p"
    using assms by blast
  thus ?thesis
    using bnd_def bnd_test_set sup_least by auto
qed

lemma mult_right_dist_bnd:
  assumes "∀n . (x^n«bot)*-p ≤ -q"
    shows "bnd x*-p ≤ -q"
proof -
  have "Sup { y*-p | y . y ∈ { x^n«bot | n::nat . True } } ≤ -q"
    by (smt assms mem_Collect_eq tests_dual.complement_bot pre_closed sub_mult_closed sup_least test_set_def)
  thus ?thesis
    using bnd_test_set bnd_def mult_right_dist_sup by simp
qed

lemma tests_complete:
  "nat_test (λn . (-p*x)^n«bot) (bnd(-p*x))"
  using bnd_test bnd_upper mult_right_dist_bnd nat_test_def tests_dual.complement_bot pre_closed by blast

end

end