namespace http://mathhub.info/MitM/core/typedsets ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚

theory TypedSets : base:?Logic =
  include ☞base:?Lists ❙
  include ☞base:?Subtyping ❙
  /T the type operator of sets along with its constructors ❙
  set: type ⟶ type ❘ = [A] A ⟶ prop ❙

  setCons: {A} A ⟶ set A ⟶ set A ❘ = [A] [a,P] [x] P x ∨ x ≐ a❘ # 3 <- 2 ❙
  setList : {A} List A ⟶  set A ❘ # ≪ 2 ≫ ❙
  inSet : {A : type} A ⟶ set A ⟶ prop ❘ = [A][a,P] P a ❘ # 2 ∈ 3 ❙
  bsetst : {A} set A ⟶ (A ⟶ prop) ⟶ set A ❘ = [A][P,Q] [x] P x ∧ Q x ❘ # ⟪ 2 | 3 ⟫ ❙
  fullset : {A} set A ❘ = [A] [x] true ❘ # fullset 1 ❙
  setAsType : {A: type, P: set A} type ❘ = [A,P] ⟨ x : A | ⊦ P x ⟩ ❘ # asType 2 ❙
   // TODO, need a lot of congruence rules that make sure that setcons ACI ❙
❚

theory SetQuantifiers : base:?Logic =
  include ☞base:?NatLiterals ❙
  include ?TypedSets ❙

  forall_sets : {A: type } set A ⟶ (A ⟶ prop) ⟶ prop ❘
    = [A,S,P] ∀[x:A] x ∈ S ⇒ P x ❘ # ∀ ∈ 2 . 3 prec -101 ❙
  exists_sets : {A: type } set A ⟶ (A ⟶ prop) ⟶ prop ❘
    = [A,S,P] ∃[x:A] x ∈ S ∧ P x ❘ # ∃ ∈ 2 . 3 prec -101 ❙
  exists_n_sets : {A:type} ℕ ⟶ set A ⟶ (A ⟶ prop) ⟶ prop ❘ # ∃= 2 ∈ 3 . 4 prec -102 ❙
❚

theory EmptySet : base:?Logic =
	 include ?TypedSets ❙
  emptySet : {A} set A ❘ = [A] [x] false❘# ∅ %I1 ❙
  empty : {A} set A ⟶ prop ❘
         = [A,s] s ≐ ∅  ❘ # empty 2 ❙
  nonEmpty : {A} set A ⟶ prop ❘
         = [A,s] s ≠ ∅  ❙
         
  inhabited : {A} set A ⟶ prop ❘ # inhabited 2 ❙
  axiom_inhabited : {A} ⊦ ∀[S:set A] inhabited S ⇔ (∃ [x] (x ∈ S)) ❙
  axiom_emptySet : {A} ⊦ ¬ (∃ [x:A] (x ∈ ∅)) ❙
❚

theory Singleton : base:?Logic =
   include ?EmptySet ❙
   single : {A} A ⟶ set A ❘ = [A,a] ∅ <- a ❘ # single 2 ❙
   singleton : {A} set A ⟶ prop ❘ = [A,s] ∃[x] s ≐ single x ❘ # singleton 2 ❙
❚

  // consider merge this with singleton ❚
theory Tuples : base:?Logic =
	 include ?EmptySet ❙
	 double : {A} A ⟶ A ⟶ set A ❘ = [A,a,b] ∅ <- a <- b ❘ # double 2 3 ❙
	 triple : {A} A ⟶ A ⟶ A ⟶ set A ❘ = [A,a,b,c] ∅ <- a <- b <- c ❘ # triple 2 3 4 ❙
❚

theory Union : base:?Logic =
   include ?TypedSets ❙
   include ☞base:?DescriptionOperator ❙
   
   axiom_union : {A,a : set A, b : set A} ⊦ ∃! [x: set A] ∀[y : A] y ∈ x ⇔ (y ∈ a ∨ y ∈ b) ❘# axiom_union 1 2 3❙
   union : {A} set A ⟶ set A ⟶ set A ❘ # 2 ∪ 3 ❘ = [A,a,b] 
   		that (set A) ([x: set A] ∀[y : A] y ∈ x ⇔ (y ∈ a ∨ y ∈ b)) (axiom_union A a b) ❙
   		
   munionCollection:  {A,B} set A ⟶ (A ⟶ set B) ⟶ set B ❘ # ⋃ 3 4❙
   unionCollection : {A} set (set A) ⟶ set A ❘ = [A, s] ⋃ s ([e] e) ❘ # UNION 2 ❙
❚
   
theory Intersection : base:?Logic =
   include ?TypedSets ❙
   
   intersection : {A} set A ⟶ set A ⟶ set A ❘ # 2 ∩ 3 ❘ = [A,a,b] ⟪ a | ([x] x ∈ b) ⟫ ❙
   
   mintersectCollection : {A,B} set A ⟶ (A ⟶ set B) ⟶ set B ❘ # ⋂ 3 4 ❙
   intersectCollection : {A} set (set A) ⟶ set A ❘ = [A, s] ⋂ s ([e] e) ❘ # INTERSECT 2 ❙
❚
 
theory SetRelations : base:?Logic =
   include ?Intersection ❙
   include ?EmptySet ❙
   
   subset : {A} set A ⟶ set A ⟶ prop ❘ = [A,S,T] ∀[x] x ∈ S ⇒ x ∈ T ❘ # 2 ⊑ 3 ❙
   properSubset : {A} set A ⟶ set A ⟶ prop ❘= [A,S,T] (S ⊑ T) ∧ ¬ S ≐ T ❘ # 2 ⊂ 3 ❙
   superset : {A} set A ⟶ set A ⟶ prop ❘ = [A,S,T] ∀[x] x ∈ T ⇒ x ∈ S ❘ # 2 ⊒ 3 ❙
   properSuperset : {A} set A ⟶ set A ⟶ prop ❘= [A,S,T] (S ⊒ T) ∧ ¬ S ≐ T ❘ # 2 ⊃ 3 ❙
   disjoint : {A} set A ⟶ set A ⟶ prop ❘= [O,A,B] A ∩ B ≐ ∅ ❘ # disjoint 2 3 ❙
   
   sameSet : {A} set A ⟶ set A ⟶ prop ❘ = [A,S,T] (S ⊑ T) ∧ (T ⊑ S)  ❘ # same_set 2 3 ❙
❚

theory PowerSet : base:?Logic =
	include ?TypedSets ❙
	powerset : {A} set A ⟶ set (set A) ❘# ℘ 2 ❙
	// TODO ❙
❚
   

theory SetDifference : base:?Logic =
	include ?Singleton ❙
	include ?Union ❙
	
	setdiff : {A} set A ⟶ set A ⟶ set A ❘= [O,A,B] ⟪ A | ([x] ¬ x ∈ B) ⟫ ❘ # 2 \ 3 ❙
	symdiff : {A} set A ⟶ set A ⟶ set A ❘= [O,A,B] (A \ B) ∪ (B \ A) ❘ # 2 symdiff 3 ❙
	complement : {A} set A ⟶ set A ❘= [O,A] (fullset O \ A) ❘ # compl 2 ❙
	// take out an element from a set ❙
	subtract : {A} set A ⟶ A ⟶ set A ❘= [O,A,a] A \ (single a) ❘ # 2 - 3 ❙
 ❚
 
theory BasicLemmata : base:?Logic =
	include ?SetDifference ❙
	include ?SetRelations ❙
   
	lemma_extensionality: {A} ⊦ ∀[a:set A] ∀[b:set A] same_set a b ⇔ a ≐ b ❙
	lemma_universeMember : {A} ⊦ ∀ [a : A] (a ∈ (fullset A)) ❙
	lemma_subsetTransitive : {A} ⊦ ∀ [s : set A] ∀ [t : set A] ∀ [u : set A] (subset A s t ∧ subset A t u) ⇒ subset A s u ❙
	lemma_subsetReflexive : {A} ⊦ ∀ [s : set A] subset A s s ❙
	lemma_subsetAntisymmetric : {A} ⊦ ∀ [s : set A] ∀ [t : set A] (subset A s t ∧ subset A t s) ⇒ s ≐ t ❙
	lemma_emptyset : {A} ⊦ ∀ [s : set A] subset A ∅ s ❙
	lemma_emptySetSubset : {A} ⊦ ∀ [s : set A] ( subset A s ∅) ⇒ s ≐ ∅ ❙
	lemma_properSubsetTransitive : {A} ⊦ ∀ [s : set A] ∀ [t : set A] ∀ [u : set A] (s ⊂ t ∧ t ⊂ u) ⇒ s ⊂ u ❙
	lemma_properSubsetIrreflexive : {A} ⊦ ∀ [s : set A] ¬ (s ⊂ s) ❙
❚
   
theory FiniteCardinality : base:?Logic =
	include ?TypedSets ❙
	include arithmetics?NaturalNumbers ❙
	
	finite : {A} set A ⟶ prop ❘# 2 finite ❙
	cardinality : {A, a : set A}⊦ a finite ⟶ ℕ ❘# | 2 | %I3 ❙
	infinite : {A} set A ⟶ prop ❘= [A,S] ¬ S finite ❘ # 2 infinite ❙
❚

theory SetStructures : base:?Logic =

	theory setstruct_theory : base:?Logic =
		universe : type ❘ # U❙
	❚
	setstruct = Mod ☞?SetStructures/setstruct_theory ❘ role abbreviation❙
	 
	include ?TypedSets ❙

	dom : setstruct ⟶ type ❘ = [S] (S.universe) ❘ role abbreviation❙
	doms : {S : setstruct}set (dom S) ❘ = [S] fullset (dom S) ❘ role abbreviation ❙
❚

theory IndicatorFunction :  base:?Logic =
	include ?TypedSets ❙
	include ☞arith:?NaturalNumbers ❙
	include ☞base:?DescriptionOperator ❙
	indicatorFunction : {A : type} set A ⟶ A ⟶ ℕ ❘= [A,s,a] if (a ∈ s) then (1 : ℕ) else 0 ❘ ❙
❚


theory AllSets : base:?Logic =
	include ?FiniteCardinality ❙
	include ?PowerSet ❙
	include ?Union ❙
	include ?SetDifference ❙
	include ?SetStructures ❙
	include ?SetRelations ❙

	typeof : {A} set A ⟶ type ❘// = [A,s] ⟨ x : A | ⊦ x ∈ s⟩ ❘ # setastype 2 ❙
	elemof : {A}{s : set A, e : A} ⊦ e ∈ s ⟶ setastype s ❘ # elem 2 3 %I4❙
❚
 
theory SetCollection : base:?Logic =
   include ?AllSets ❙

   collection : type ⟶ type ❘ = [G] set (set G)❙
                                      
   theory setColl_theory : base:?Logic > X : type ❘ =
   	  coll : collection X ❙
   	  colltype = setastype coll ❙
   ❚
   setColl = [X : type] Mod ☞?SetCollection/setColl_theory (X) ❙
   
   emptySetInType : {T, S : setColl T, emptyincoll : ⊦ ∅ ∈ (S.coll) } S.colltype ❘ # ∅t %I1 %I2 %I3 ❙
   fullSetInType : {T, S : setColl T, fullincoll : ⊦ (fullset T) ∈ (S.coll) } S.colltype ❘ # fullt %I1 %I2 %I3 ❙
❚

theory TaggedSetCollection : base:?Logic =
	include ?SetCollection ❙
	include ☞base:?ProductTypes ❙
	
	taggedCollection : type ⟶ type ❘= [G] set (G × set G) ❙

❚