# 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 }"
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)"
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 }"
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)"