theory Examples
  imports Main TopologicalSpace
begin


locale topological_space =
  fixes X :: "'a set" and tau :: "'a set set"
  assumes
    (* The empty set and the whole set are in the topology *)
    empty_in_tau: "{} \<in> tau" and
    whole_in_tau: "X \<in> tau" and
    (* The topology is closed under arbitrary unions *)
    arbitrary_union_closed: "\<forall>U. (\<forall>i. U i \<in> tau) \<longrightarrow> (\<Union>i. U i) \<in> tau" and
    (* The topology is closed under finite intersections *)
    finite_intersection_closed: "\<forall>F. finite F \<longrightarrow> (\<forall>A \<in> F. A \<in> tau) \<longrightarrow> (\<Inter>F) \<in> tau"



(* Example 1: Trivial or Indiscrete Topology *)
locale trivial_topology = topological_space
  where X = "{1, 2, 3, 4}" and tau = "{{}, {1, 2, 3, 4}}"

(* Example 2: Another Topology *)
locale another_topology = topological_space
  where X = "{1, 2, 3, 4}" and tau = "{{}, {2}, {1, 2}, {2, 3}, {1, 2, 3}, {1, 2, 3, 4}}"

(* Example 3: Discrete Topology *)
locale discrete_topology = topological_space
  where X = "{1, 2, 3, 4}" and tau = "Pow {1, 2, 3, 4}"


(* Example 4: Non-Topology *)
locale non_topology =
  fixes X :: "int set" and tau :: "int set set"
  defines "X ≡ UNIV :: int set" (* Definition of X as the set of all integers *)
  defines "tau ≡ {A :: int set. finite A} ∪ {UNIV :: int set}" (* Definition of tau *)
  assumes non_topology_axioms: "¬ topological_space X tau"

end

Type unification failed: Clash of types "_ set" and "_ itself"

Type error in application: incompatible operand type

Operator:  topological_space ::
  ??'a itself ⇒ ??'b set ⇒ ??'b set set ⇒ bool
Operand:   X :: int set

interpretation trivial_topology:topological_space "{1, 2, 3, 4}"  "{{}, {1, 2, 3, 4}}"
  sorry

(* OR *)

locale trivial_topology =
  fixes X :: "'a::numeral set" and tau :: "'a set set"
  assumes "X = {1, 2, 3, 4}" and "tau = {{}, {1, 2, 3, 4}}"
begin

sublocale topological_space
  sorry

end