Theory UD_Tests

(* Title: UD/Tests/UD_Tests.thy
   Author: Mihails Milehins
   Copyright 2021 (C) Mihails Milehins

A test suite for the framework UD.
*)

section‹Test suite for UD›
theory UD_Tests
  imports
    "../UD"
    "../../IML_UT/IML_UT"
    Complex_Main
begin



subsection‹Background›

(* 
The following two definitions were copied from 
HOL-Analysis.Elementary_Topology with minor amendments
to avoid unnecessary dependencies
*)
definition (in topological_space) islimpt:: "'a ⇒ 'a set ⇒ bool"
  where "islimpt x S ⟷ (∀T. x∈T ⟶ open T ⟶ (∃y∈S. y∈T ∧ y≠x))"
definition closure :: "('a::topological_space) set ⇒ 'a set" 
  where "closure S = S ∪ {x. islimpt x S}"

ud ‹topological_space.closed›
ud ‹islimpt›

lemma closed_with: "closed ≡ closed.with open"
  unfolding closed_def closed.with_def .

definition closure_with :: "('a set ⇒ bool) ⇒ 'a set ⇒ 'a set"
  where "closure_with τ ≡ λS. S ∪ {x. islimpt.with τ x S}"

lemma closure_with: "closure ≡ closure_with open"
  unfolding closure_def islimpt.with closure_with_def .



subsection‹Tests›

ML_file‹UD_TEST_UNOVERLOAD_DEFINITION.ML›

ML‹
Lecker.test_group @{context} () [ud_test_unoverload_definition.test_suite]
›

end