Theory Complete_Tests

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

section ‹Complete Tests›

theory Complete_Tests

imports Tests

begin

class complete_tests = tests + Sup + Inf +
  assumes sup_test: "test_set A ⟶ Sup A = --Sup A"
  assumes sup_upper: "test_set A ∧ x ∈ A ⟶ x ≤ Sup A"
  assumes sup_least: "test_set A ∧ (∀x∈A . x ≤ -y) ⟶ Sup A ≤ -y"
begin

lemma Sup_isotone:
  "test_set B ⟹ A ⊆ B ⟹ Sup A ≤ Sup B"
  by (metis sup_least sup_test sup_upper test_set_closed subset_eq)

lemma mult_right_dist_sup:
  assumes "test_set A"
    shows "Sup A * -p = Sup { x * -p | x . x ∈ A }"
proof -
  have 1: "test_set { x * -p | x . x ∈ A }"
    by (simp add: assms mult_right_dist_test_set)
  have 2: "Sup { x * -p | x . x ∈ A } ≤ Sup A * -p"
    by (smt (verit, del_insts) assms mem_Collect_eq tests_dual.sub_sup_left_isotone sub_mult_closed sup_test sup_least sup_upper test_set_def)
  have "∀x∈A . x ≤ --(--Sup { x * -p | x . x ∈ A } ⊔ --p)"
  proof
    fix x
    assume 3: "x ∈ A"
    hence "x * -p ⊔ --p ≤ Sup { x * -p | x . x ∈ A } ⊔ --p"
      using 1 by (smt (verit, del_insts) assms mem_Collect_eq tests_dual.sub_inf_left_isotone sub_mult_closed sup_upper test_set_def sup_test)
    thus "x ≤ --(--Sup { x * -p | x . x ∈ A } ⊔ --p)"
      using 1 3 by (smt (z3) assms tests_dual.inf_closed sub_comm test_set_def sup_test sub_mult_closed tests_dual.sba_dual.shunting_right tests_dual.sba_dual.sub_sup_left_isotone tests_dual.inf_absorb tests_dual.inf_less_eq_cases_3)
  qed
  hence "Sup A ≤ --(--Sup { x * -p | x . x ∈ A } ⊔ --p)"
    by (simp add: assms sup_least)
  hence "Sup A * -p ≤ Sup { x * -p | x . x ∈ A }"
    using 1 by (smt (z3) assms sup_test tests_dual.sba_dual.shunting tests_dual.sub_commutative tests_dual.sub_sup_closed tests_dual.sub_sup_demorgan)
  thus ?thesis
    using 1 2 by (smt (z3) assms sup_test tests_dual.sba_dual.sub_sup_closed tests_dual.antisymmetric tests_dual.inf_demorgan tests_dual.inf_idempotent)
qed

lemma mult_left_dist_sup:
  assumes "test_set A"
  shows "-p * Sup A = Sup { -p * x | x . x ∈ A }"
proof -
  have 1: "Sup A * -p = Sup { x * -p | x . x ∈ A }"
    by (simp add: assms mult_right_dist_sup)
  have 2: "-p * Sup A = Sup A * -p"
    by (metis assms sub_comm sup_test)
  have "{ -p * x | x . x ∈ A } = { x * -p | x . x ∈ A }"
    by (metis assms test_set_def tests_dual.sub_commutative)
  thus ?thesis
    using 1 2 by simp
qed

definition Sum :: "(nat ⇒ 'a) ⇒ 'a"
  where "Sum f ≡ Sup { f n | n::nat . True }"

lemma Sum_test:
  "test_seq t ⟹ Sum t = --Sum t"
  using Sum_def sup_test test_seq_test_set by auto

lemma Sum_upper:
  "test_seq t ⟹ t x ≤ Sum t"
  using Sum_def sup_upper test_seq_test_set by auto

lemma Sum_least:
  "test_seq t ⟹ (∀n . t n ≤ -p) ⟹ Sum t ≤ -p"
  using Sum_def sup_least test_seq_test_set by force

lemma mult_right_dist_Sum:
  "test_seq t ⟹ (∀n . t n * -p ≤ -q) ⟹ Sum t * -p ≤ -q"
  by (smt (verit, del_insts) CollectD Sum_def sup_least sup_test test_seq_test_set test_set_def tests_dual.sba_dual.shunting_right tests_dual.sba_dual.sub_sup_closed)

lemma mult_left_dist_Sum:
  "test_seq t ⟹ (∀n . -p * t n ≤ -q) ⟹ -p * Sum t ≤ -q"
  by (smt (verit, del_insts) Sum_def mem_Collect_eq mult_left_dist_sup sub_mult_closed sup_least test_seq_test_set test_set_def)

lemma pSum_below_Sum:
  "test_seq t ⟹ pSum t m ≤ Sum t"
  using Sum_test Sum_upper nat_test_def pSum_below_sum test_seq_def mult_right_dist_Sum by auto

lemma pSum_sup:
  assumes "test_seq t"
    shows "pSum t m = Sup { t i | i . i ∈ {..<m} }"
proof -
  have 1: "test_set { t i | i . i ∈ {..<m} }"
    using assms test_seq_test_set test_set_def by auto
  have "∀y∈{ t i | i . i ∈ {..<m} } . y ≤ --pSum t m"
    using assms pSum_test pSum_upper by force
  hence 2: "Sup { t i | i . i ∈ {..<m} } ≤ --pSum t m"
    using 1 by (simp add: sup_least)
  have "pSum t m ≤ Sup { t i | i . i ∈ {..<m} }"
  proof (induct m)
    case 0
    show ?case
      by (smt (verit, ccfv_SIG) Collect_empty_eq empty_iff lessThan_0 pSum.simps(1) sup_test test_set_def tests_dual.top_greatest)
  next
    case (Suc n)
    have 4: "test_set {t i |i. i ∈ {..<n}}"
      using assms test_seq_def test_set_def by auto
    have 5: "test_set {t i |i. i < Suc n}"
      using assms test_seq_def test_set_def by force
    hence 6: "Sup {t i |i. i < Suc n} = --Sup {t i |i. i < Suc n}"
      using sup_test by auto
    hence "∀x∈{t i |i. i ∈ {..<n}} . x ≤ --Sup {t i |i. i < Suc n}"
      using 5 less_Suc_eq sup_upper by fastforce
    hence 7: "Sup {t i |i. i ∈ {..<n}} ≤ --Sup {t i |i. i < Suc n}"
      using 4 by (simp add: sup_least)
    have "t n ∈ {t i |i. i < Suc n}"
      by auto
    hence "t n ≤ Sup {t i |i. i < Suc n}"
      using 5 by (simp add: sup_upper)
    hence "pSum t n ⊔ t n ≤ Sup {t i |i. i <Suc n}"
      using Suc 4 6 7 by (smt assms tests_dual.greatest_lower_bound test_seq_def pSum_test tests_dual.sba_dual.transitive sup_test)
    thus ?case
      by simp
  qed
  thus ?thesis
    using 1 2 by (smt assms tests_dual.antisymmetric sup_test pSum_test)
qed

definition Prod :: "(nat ⇒ 'a) ⇒ 'a"
  where "Prod f ≡ Inf { f n | n::nat . True }"

lemma Sum_range:
  "Sum f = Sup (range f)"
  by (simp add: Sum_def image_def)

lemma Prod_range:
  "Prod f = Inf (range f)"
  by (simp add: Prod_def image_def)

end

end