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. xT  open T  (yS. yT  yx))"
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›

MLLecker.test_group @{context} () [ud_test_unoverload_definition.test_suite]

end