Theory Tests

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

section Tests

theory Tests

imports Subset_Boolean_Algebras.Subset_Boolean_Algebras Base

begin

context subset_boolean_algebra_extended
begin

sublocale sba_dual: subset_boolean_algebra_extended where uminus = uminus and sup = inf and minus = "λx y . -(-x  y)" and inf = sup and bot = top and less_eq = greater_eq and less = greater and top = bot
  apply unfold_locales
  apply (simp add: inf_associative)
  apply (simp add: inf_commutative)
  using inf_cases_2 apply simp
  using inf_closed apply simp
  apply simp
  apply simp
  using sub_sup_closed sub_sup_demorgan apply simp
  apply simp
  apply (simp add: inf_commutative less_eq_inf)
  by (metis inf_commutative inf_idempotent inf_left_dist_sup sub_less_def sup_absorb sup_right_zero top_double_complement)

lemma strict_leq_def:
  "-x < -y  -x  -y  ¬ (-y  -x)"
  by (simp add: sba_dual.sba_dual.sub_less_def sba_dual.sba_dual.sub_less_eq_def)

lemma one_def:
  "top = -bot"
  by simp

end

class tests = times + uminus + one + ord + sup + bot +
  assumes sub_assoc: "-x * (-y * -z) = (-x * -y) * -z"
  assumes sub_comm: "-x * -y = -y * -x"
  assumes sub_compl: "-x = -(--x * -y) * -(--x * --y)"
  assumes sub_mult_closed: "-x * -y = --(-x * -y)"
  assumes the_bot_def: "bot = (THE x . (y . x = -y * --y))" (* define without imposing uniqueness *)
  assumes one_def: "1 = - bot"
  assumes sup_def: "-x  -y = -(--x * --y)"
  assumes leq_def: "-x  -y  -x * -y = -x"
  assumes strict_leq_def: "-x < -y  -x  -y  ¬ (-y  -x)"
begin

sublocale tests_dual: subset_boolean_algebra_extended where uminus = uminus and sup = times and minus = "λx y . -(-x * y)" and inf = sup and bot = 1 and less_eq = greater_eq and less = greater and top = bot
  apply unfold_locales
  apply (simp add: sub_assoc)
  apply (simp add: sub_comm)
  apply (simp add: sub_compl)
  using sub_mult_closed apply simp
  apply (simp add: the_bot_def)
  apply (simp add: one_def the_bot_def)
  apply (simp add: sup_def)
  apply simp
  apply (simp add: leq_def sub_comm)
  by (simp add: leq_def strict_leq_def sub_comm)

sublocale sba: subset_boolean_algebra_extended where uminus = uminus and sup = sup and minus = "λx y . -(-x  y)" and inf = times and bot = bot and less_eq = less_eq and less = less and top = 1 ..

text sets and sequences of tests

definition test_set :: "'a set  bool"
  where "test_set A  xA . x = --x"

lemma mult_left_dist_test_set:
  "test_set A  test_set { -p * x | x . x  A }"
  by (smt mem_Collect_eq sub_mult_closed test_set_def)

lemma mult_right_dist_test_set:
  "test_set A  test_set { x * -p | x . x  A }"
  by (smt mem_Collect_eq sub_mult_closed test_set_def)

lemma sup_left_dist_test_set:
  "test_set A  test_set { -p  x | x . x  A }"
  by (smt mem_Collect_eq tests_dual.sba_dual.sub_sup_closed test_set_def)

lemma sup_right_dist_test_set:
  "test_set A  test_set { x  -p | x . x  A }"
  by (smt mem_Collect_eq tests_dual.sba_dual.sub_sup_closed test_set_def)

lemma test_set_closed:
  "A  B  test_set B  test_set A"
  using test_set_def by auto

definition test_seq :: "(nat  'a)  bool"
  where "test_seq t  n . t n = --t n"

lemma test_seq_test_set:
  "test_seq t  test_set { t n | n::nat . True }"
  using test_seq_def test_set_def by auto

definition nat_test :: "(nat  'a)  'a  bool"
  where "nat_test t s  (n . t n = --t n)  s = --s  (n . t n  s)  (x y . (n . t n * -x  -y)  s * -x  -y)"

lemma nat_test_seq:
  "nat_test t s  test_seq t"
  by (simp add: nat_test_def test_seq_def)

primrec pSum :: "(nat  'a)  nat  'a"
  where "pSum f 0 = bot"
      | "pSum f (Suc m) = pSum f m  f m"

lemma pSum_test:
  "test_seq t  pSum t m = --(pSum t m)"
  apply (induct m)
  apply simp
  by (smt pSum.simps(2) tests_dual.sba_dual.sub_sup_closed test_seq_def)

lemma pSum_test_nat:
  "nat_test t s  pSum t m = --(pSum t m)"
  by (metis nat_test_seq pSum_test)

lemma pSum_upper:
  "test_seq t  i<m  t i  pSum t m"
proof (induct m)
  show "test_seq t  i<0  t i  pSum t 0"
    by (smt less_zeroE)
next
  fix n
  assume "test_seq t  i<n  t i  pSum t n"
  hence "test_seq t  i<n  t i  pSum t (Suc n)"
    by (smt (z3) pSum.simps(2) pSum_test tests_dual.sba_dual.upper_bound_left tests_dual.transitive test_seq_def)
  thus "test_seq t  i<Suc n  t i  pSum t (Suc n)"
    by (metis less_Suc_eq pSum.simps(2) pSum_test tests_dual.sba_dual.upper_bound_right test_seq_def)
qed

lemma pSum_below:
  "test_seq t  (m<k . t m * -p  -q)  pSum t k * -p  -q"
  apply (induct k)
  apply (simp add: tests_dual.top_greatest)
  by (smt (verit, ccfv_threshold) tests_dual.sup_right_dist_inf pSum.simps(2) pSum_test test_seq_def sub_mult_closed less_Suc_eq tests_dual.sba_dual.sub_associative tests_dual.sba_dual.sub_less_eq_def)

lemma pSum_below_nat:
  "nat_test t s  (m<k . t m * -p  -q)  pSum t k * -p  -q"
  by (simp add: nat_test_seq pSum_below)

lemma pSum_below_sum:
  "nat_test t s  pSum t x  s"
  by (smt (verit, ccfv_threshold) tests_dual.sup_right_unit nat_test_def one_def pSum_below_nat pSum_test_nat)

lemma ascending_chain_sup_left:
  "ascending_chain t  test_seq t  ascending_chain (λn . -p  t n)  test_seq (λn . -p  t n)"
  by (smt (z3) ord.ascending_chain_def tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.sub_sup_right_isotone test_seq_def)

lemma ascending_chain_sup_right:
  "ascending_chain t  test_seq t  ascending_chain (λn . t n  -p)  test_seq (λn . t n  -p)"
  by (smt ascending_chain_def tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.sub_sup_left_isotone test_seq_def)

lemma ascending_chain_mult_left:
  "ascending_chain t  test_seq t  ascending_chain (λn . -p * t n)  test_seq (λn . -p * t n)"
  by (smt (z3) ascending_chain_def sub_mult_closed tests_dual.sba_dual.reflexive tests_dual.sup_isotone test_seq_def)

lemma ascending_chain_mult_right:
  "ascending_chain t  test_seq t  ascending_chain (λn . t n * -p)  test_seq (λn . t n * -p)"
  by (smt (z3) ascending_chain_def sub_mult_closed tests_dual.sba_dual.reflexive tests_dual.sup_isotone test_seq_def)

lemma descending_chain_sup_left:
  "descending_chain t  test_seq t  descending_chain (λn . -p  t n)  test_seq (λn . -p  t n)"
  by (smt descending_chain_def tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.sub_sup_right_isotone test_seq_def)

lemma descending_chain_sup_right:
  "descending_chain t  test_seq t  descending_chain (λn . t n  -p)  test_seq (λn . t n  -p)"
  by (smt descending_chain_def tests_dual.sba_dual.sub_sup_closed tests_dual.sba_dual.sub_sup_left_isotone test_seq_def)

lemma descending_chain_mult_left:
  "descending_chain t  test_seq t  descending_chain (λn . -p * t n)  test_seq (λn . -p * t n)"
  by (smt (z3) descending_chain_def sub_mult_closed tests_dual.sba_dual.reflexive tests_dual.sup_isotone test_seq_def)

lemma descending_chain_mult_right:
  "descending_chain t  test_seq t  descending_chain (λn . t n * -p)  test_seq (λn . t n * -p)"
  by (smt (z3) descending_chain_def sub_mult_closed tests_dual.sba_dual.reflexive tests_dual.sup_isotone test_seq_def)

end

end