(**********************************)
(** Wprawki z regularnymi or/and **) 
(**********************************)


Lemma or_commute :  (A,B : Prop)(A\/B) -> (B\/A).

Lemma and_commute: (A,B:Prop) (A\/B) -> (B\/A).

Lemma and_or : (A,B:Prop)(A/\B) -> (A\/B).

(* ktore z ponizszych sa intuicjonistycznie prawdziwe ? *)
Lemma Morgan1  : (A,B:Prop) ~(A\/B) -> ~A/\~B.
Lemma Morgan1' : (A,B:Prop) ~A/\~B -> ~(A\/B).
Lemma Morgan2  : (A,B:Prop) ~(A/\B) -> ~A\/~B.
Lemma Morgan2' : (A,B:Prop) ~A\/~B -> ~(A/\B).

Lemma przyk4 : (A,B,C:Prop)((A->C)/\(B->C)) -> A/\B -> C.

Lemma or_associative1 : (A,B,C:Prop)(A\/B)\/C -> A\/(B\/C).

Lemma or_associative2 : (A,B,C:Prop)(A\/(B\/C)) -> ((A\/B)\/C).

  (********************************************************************)
  (********************************************************************)
  (****   Twierdzenie o punkcie stalym dla funkcji monotonicznej   ****)
  (****   w kracie podzbiorow                                      ****)
  (********************************************************************)
  (********************************************************************)

Parameter U : Type.

Definition SubU := U -> Prop.

  (**************************************)
  (* 1. Definicja porzadku - zawierania *)
  (**************************************)

Definition Incl : SubU -> SubU -> Prop := [S1,S2](u:U)(S1 u) -> (S2 u).

Lemma Incl_refl: (A:SubU) (Incl A A).

Lemma Incl_trans: (A,B,C:SubU) (Incl A B) -> (Incl B C) -> (Incl A C).

Definition Eq1 := [A,B:SubU] ((Incl A B)/\(Incl B A)).

  (*************************)
  (* 2. Dowod, ze to krata *)
  (*************************)

  (* klasa = zbior podzbiorow U *)
Definition CLASS := SubU -> Prop.

Definition Cinter := [K:CLASS] [u:U] (A:SubU) (K A) -> (A u).

Lemma Cinter_Lower_Bound: (A:SubU) (K:CLASS) (K A) -> (Incl (Cinter K) A).

Lemma Cinter_Greatest_Bound: 
  (A:SubU)(K:CLASS) ((B:SubU)(K B) -> (Incl A B)) -> (Incl A (Cinter K)).

Inductive Full_U : SubU := Full_total:(u:U) (Full_U u).

Lemma Full_greatest : (A:SubU)(Incl A Full_U).

  (***************************)
  (* 3. Wlasciwe twierdzenie *)
  (***************************)

Parameter f: SubU -> SubU.
Axiom f_monotone : (A,B:SubU) (Incl A B) -> (Incl (f A) (f B)).

Definition F:CLASS := [A:SubU] (Incl (f A) A).
Definition FI:SubU := (Cinter F).

Lemma FI_Incl: (A:SubU) (F A) -> (Incl FI A).

Lemma fFIf_Incl: (A:SubU) (F A) -> (Incl (f FI) (f A)).

Lemma FIf_Incl: (A:SubU) (F A) -> (Incl (f FI) A).

Lemma fFI_Incl_FI: (Incl (f FI) FI).

Lemma FI_Incl_fFI: (Incl FI (f FI)).

Theorem FI_is_fix: (Eq1 FI (f FI)).

Theorem FI_is_smallest: (A:SubU) (Eq1 A (f A)) -> (Incl FI A).

(****** Sukces !!!!!!! **********)


(* Jakby komus bylo malo :) *)

Definition Eq2 := [A,B:SubU] (u:U) (iff (A u) (B u)).

Lemma Eq1_Eq2: (A,B:SubU) (iff (Eq1 A B) (Eq2 A B)).

Definition union : SubU -> SubU -> SubU := [S1,S2][u:U]((S1 u)\/(S2 u)).

Definition inter : SubU -> SubU -> SubU := [S1,S2][u:U]((S1 u)/\(S2 u)).

Lemma union_Incl: (A,B:SubU) (Incl A (union A B)).

Lemma union_idempotent: (A:SubU) (Eq1 A (union A A)).

Lemma inter_Incl: (A,B:SubU) (Incl (inter A B) A).

Theorem Union_commutative :
  (A,B: SubU) (Eq1 (union A B) (union B A)).

Theorem Union_associative :
  (A, B, C: SubU)
  (Eq1 (union (union A B) C) (union A (union B C))).

Lemma Union_absorbs :
  (A, B: SubU) (Incl B A) -> (Incl (union A B) A).

Theorem Distributivity :
  (A, B, C: SubU)
     (Eq1 (inter A (union B C))
     (union (inter A B) (inter A C))).

Definition compl : SubU -> SubU := [S][u](~(S u)).

Definition is_empty : SubU -> Prop := [S](u:U)(~(S u)).

Definition disjoint : SubU -> SubU -> Prop := [S1,S2] (is_empty (inter S1 S2)).

(* Jak ktos chce wiecej, to niech sobie sam rozwiazuje... *)
(* Empty neutralny dla Union, *)
(* A,B included in (union A B) *)
(* A rozl z C, B rozl z C, to (union A B) i (inter A B) tez *)
(* A rozl z B, to przeciecie dopelnien niepuste *)