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-py«-q = -p*(x«-q)  --p*(y«-q)"
begin

text ‹Theorem 40.2›

lemma ite_pre_then:
  "-p*(x-py«-q) = -p*(x«-q)"
proof -
  have "-p*(x-py«-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-py«-q) = --p*(y«-q)"
proof -
  have "--p*(x-py«-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-py«-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-py«-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-py«-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: "-px«-q = -p*(x«-px«-q)  --p*-q"
  assumes while_post: "-px«-q = -px«--p*-q"
begin

text ‹Theorem 40.4›

lemma while_pre_then:
  "-p*(-px«-q) = -p*(x«-px«-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*(-px«-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:
  "-px«-q  x*(-px)-p1«-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:
  "-px«-q  x-p1«-px«-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  -px«--p"
  by (metis pre_closed tests_dual.sup_idempotent tests_dual.upper_bound_right while_pre_else)

lemma while_pre_compl_one:
  "--p  -px«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  -px«1  -p*-q  -px«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  -px«--p*-q"
proof -
  have 1: "-q*--p  -px«--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  -px«--p*-q"
  proof
    fix n
    show "t n*-p*-q  -px«--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  -px«--p*-q"
      hence "m<n . t m*-p*-q  t m*--p*-q  -px«--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  -px«--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  -px«--p*-q"
        by (smt assms(1) pSum_below_nat pre_closed sub_mult_closed)
      hence "t n*-p*-q*(-px«--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  -px«--p*-q"
        using 2 by (smt (z3) pre_closed tests_dual.sub_sup_closed tests_dual.upper_bound_right)
    qed
  qed
  hence "-q*-p  -px«--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  -px«--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  -px«--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 "-px«--p*?qs  -px«--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  -px«1"
proof -
  have 1: "-r  -px«--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 "-px«--p*s  -px«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  -px«1"
proof -
  have "-px«--p*-q  -px«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  11«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  pq  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  xpy  While_program"
      | while_prog: "p  Test_expression  x  While_program  px  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  pq  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 (px«q) (-p(x«(px«q)*aL)) = --tfun (-p) x (px«q) (-p(x«(px«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 (px«q) (-p(x«(px«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 (px«q) (-p(x«(px«q)*aL)) m = --tseq (-p) x (px«q) (-p(x«(px«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 (px«q) (-p(x«(px«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 (px«q) (-p(x«(px«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 (px«q) (-p(x«(px«q)*aL)) = --tsum (-p) x (px«q) (-p(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) = --tfun2 (-p*q) p x (px«q) (-p*qp*(x«(px«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 (px«q) (-p*qp*(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) m = --tseq2 (-p*q) p x (px«q) (-p*qp*(x«(px«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 (px«q) (-p*qp*(x«(px«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 (px«q) (-p*qp*(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) = --tsum2 (-p*q) p x (px«q) (-p*qp*(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) m  tseq (-p) x (px«q) (-p(x«(px«q)*aL)) m"
proof -
  let ?t2 = "tseq2 (-p*q) p x (px«q) (-p*qp*(x«(px«q)*aL))"
  let ?t = "tseq (-p) x (px«q) (-p(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) m  tsum (-p) x (px«q) (-p(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL))  tsum (-p) x (px«q) (-p(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) m  px«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 (px«q) (-p*qp*(x«(px«q)*aL))  px«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 (px«q) (-p*qp*(x«(px«q)*aL)) = px«q"
proof -
  let ?w = "px«q"
  let ?s = "-p*qp*(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«pxp"
      | seq_trip:   "pxq  qyr  px*yr"
      | cond_trip:  "p  Test_expression  q  Pre_expression  p*qxr  -p*qyr  qxpyr"
      | while_trip: "p  Test_expression  q  Pre_expression  test_seq t  q  Sum t  t 0*p*qxaL*q  (n>0 . t n*p*qxpSum t n*q)  qpx-p*q"
      | cons_trip:  "p  Pre_expression  s  Pre_expression  p  q  qxr  r  s  pxs"

lemma derived_type:
  "pxq  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  qyr  p*qyr"
  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  pyq*r  pyr"
  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 "pxq  (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  -px«-q"
begin

lemma while_soundness_0:
  "-p*-q  x«-q  -q*aL  -px«--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  -px«--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  -px«--p*-q  pSum t n*-q  -px«--p*-q"
  proof
    fix n
    show "t n*-q  -px«--p*-q  pSum t n*-q  -px«--p*-q"
    proof (induct n rule: nat_less_induct)
      fix n
      assume 3: "m<n . t m*-q  -px«--p*-q  pSum t m*-q  -px«--p*-q"
      have 4: "pSum t n*-q  -px«--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 "...  -px«--p*-q"
        proof -
          have "pSum t m*-q = --(pSum t m*-q)  t m*-q = --(t m*-q)  -px«--p*-q = --(-px«--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«-px«--p*-q"
        by (smt assms pSum_test pre_closed pre_iso sub_mult_closed)
      have 6: "-p*(t n*-q)  -p*(-px«--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«-px«--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«-px«--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*(-px«--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  -px«--p*-q  pSum t n*-q  -px«--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  -px«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  -px«--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 "-px«--p*Sum t  -px«1"
    by (metis assms(1) Sum_test pre_below_pre_one tests_dual.sub_sup_closed)
  hence "Sum t  -px«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:
  "pxq  pxq"
  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 "(px«q)*aL  tseq2 (-p*q) p x (px«q) (-p*qp*(x«(px«q)*aL)) 0"
proof (unfold tseq2_def power_zero_id id_def while_pre)
  have "(px«q)*aL = (p*(x«px«q)  -p*q)*aL"
    by (metis assms while_pre test_pre pre_expression_test)
  also have "... = p*(x«px«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«px«q)*aL)  -p*q*aL"
    by (smt assms aL_test pre_closed pre_expression_test test_pre sub_assoc)
  also have "...  p*(x«(px«q)*aL)  -p*q"
  proof -
    have 1: "(x«px«q)*aL  x«(px«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«(px«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 "(px«q)*aL  -p*q  p*(x«(px«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 (px«q) (-p*qp*(x«(px«q)*aL)) m  tseq2 (-p*q) p x (px«q) (-p*qp*(x«(px«q)*aL)) (Suc m)"
proof (induct m)
  let ?w = "px«q"
  let ?r = "-p*qp*(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*qp*(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 = "px«q"
  let ?r = "-p*qp*(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*qp*(x«?w*?t m)  -p*qp*(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 (px«q) (-p*qp*(x«(px«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  -px«-q  -qaL"
begin

lemma while_completeness_var:
  assumes "-p*(x«-q)-r  -q"
    shows "-px«-r  -qaL"
proof -
  have 1: "-px«-q  -qaL"
    by (smt assms pre_closed tests_dual.sub_sup_closed tests_dual.greatest_lower_bound while_completeness)
  have "-px«-r  -px«-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 "px«q  tsum (-p) x (px«q) (-p(x«(px«q)*aL))"
proof -
  let ?w = "px«q"
  let ?r = "-p*qp*(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  ?tsaL"
    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*(?tsaL)"
    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 "rPre_expression . x«rxr"
    shows "px«qpxq"
proof -
  let ?w = "px«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*?wxaL*?w"
    using 1 by (simp add: assms(4) Pre_expression.conj_pre aL_pre_expression)
  hence "x«?w*aLxaL*?w"
    using 1 by (metis aL_test pre_expression_test sub_comm)
  hence "(x«?w*aL)*p*?wxaL*?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*?wxaL*?w"
    using 5 by simp
  hence 6: "?t 0*p*?wxaL*?w"
    by (unfold tseq_def power_zero_id id_def)
  have "n>0 . ?t n*p*?wxpSum ?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*?wxpSum ?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 "?wpx-p*?w"
    using 1 2 3 6 assms while_trip by auto
  hence "?wpx-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«qxq"
  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:
  "pxq  pxq"
  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:
  "pxq  pxq"
  using completeness soundness by blast

end

class hoare_rules = whiledo + complete_tests + hoare_triple +
  assumes rule_pre:   "x«-qx-q"
  assumes rule_seq:   "-px-q  -qy-r  -px*y-r"
  assumes rule_cond:  "-p*-qx-r  --p*-qy-r  -qx-py-r"
  assumes rule_while: "test_seq t  -q  Sum t  t 0*-p*-qxaL*-q  (n>0 . t n*-p*-qxpSum t n*-q)  -q-px--p*-q"
  assumes rule_cons:  "-p  -q  -qx-r  -r  -s  -px-s"
  assumes rule_disj:  "-px-r  -qx-s  -p-qx-r-s"
begin

lemma rule_cons_pre:
  "-p  -q  -qx-r  -px-r"
  using rule_cons tests_dual.sba_dual.reflexive by blast

lemma rule_cons_pre_mult:
  "-qx-r  -p*-qx-r"
  by (metis tests_dual.sub_sup_closed rule_cons_pre tests_dual.upper_bound_right)

lemma rule_cons_pre_plus:
  "-p-qx-r  -px-r"
  by (metis tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.upper_bound_left rule_cons_pre)

lemma rule_cons_post:
  "-qx-r  -r  -s  -qx-s"
  using rule_cons tests_dual.sba_dual.reflexive by blast

lemma rule_cons_post_mult:
  "-qx-r*-s  -qx-s"
  by (metis rule_cons_post tests_dual.upper_bound_left sub_comm sub_mult_closed)

lemma rule_cons_post_plus:
  "-qx-r  -qx-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:
 "-px-r  -qx-r  -p-qx-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: "-px-q  -p  x«-q"
begin

lemma valid_hoare_triple_same:
  "p  Pre_expression  q  Pre_expression  x  While_program  pxq = pxq"
  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  pxq = pxq"
  by (simp add: soundness_completeness valid_hoare_triple_same)

lemma valid_rule_disj:
  assumes "-px-r"
      and "-qx-s"
    shows "-p-qx-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*-qxpSum t n*-q)  -q-px--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*-qxaL*-q  (n>0 . t n*-p*-qxpSum t n*-q)  -q-px--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:
  "botx-p"
  by (metis hoare_triple_valid pre_closed tests_dual.top_double_complement tests_dual.top_greatest)

lemma rule_skip:
  "-p1-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 "-p1z1-p1*-p2"
      and "n>0 . t n*-p1*-p2*-p3z2pSum t n*-p1*-p2"
    shows "-p1z1*(-p3z2)-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)z2aL*(-p1*-p2)"
    by (metis aL_test sub_mult_closed rule_bot)
  have "n>0 . t n*-p3*(-p1*-p2)z2pSum 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-p3z2--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  -px«--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*-qx-q  -q-px--p*-q"
  by (metis hoare_triple_valid sub_mult_closed while_soundness_pc)

lemma rule_alternation:
  "-px-q  -qy-p  -p-rx*y--r*-p"
  by (meson rule_cons_pre_mult rule_seq rule_while_pc)

lemma rule_alternation_context:
  "-pv-p  -pw-q  -qx-q  -qy-p  -pz-p  -p-rv*w*x*y*z--r*-p"
  by (meson rule_cons_pre_mult rule_seq rule_while_pc)

lemma rule_example_3:
  assumes "-p*-qx--p*-q"
      and "--p*-rx-p*-r"
      and "-p*-ry-p*-q"
      and "--p*-qz--p*-r"
    shows "-p*-q--p*-r-sx*(y-pz)--s*(-p*-q--p*-r)"
proof -
  have t1: "-p*-q--p*-rx--p*-q-p*-r"
    by (smt assms(1,2) rule_disj sub_mult_closed)
  have "-p*-ry-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*-qz-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*-ry-pz-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-pz)-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  px«q  Sum (λn . (p*x)^n«bot)"
begin

lemma
  assumes "p  Test_expression"
      and "q  Pre_expression"
      and "x  While_program"
    shows "px«q  tsum (-p) x (px«q) (-p(x«(px«q)*aL))"
proof -
  let ?w = "px«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