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 ≡ ∀x∈A . 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