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


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

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

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

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

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

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

Lemma or_associative2 : forall 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 := 
  fun S1 S2 => forall u:U, (S1 u) -> (S2 u).

Lemma Incl_refl: forall A:SubU, Incl A A.

Lemma Incl_trans: forall 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 := fun (K:CLASS) (u:U) => forall A:SubU, K A -> A u.

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

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

Inductive Full_U : SubU := Full_total : forall u:U, Full_U u.

Lemma Full_greatest : forall A:SubU, Incl A Full_U.

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

Variable f: SubU -> SubU.
Hypothesis f_monotone : forall A B:SubU, Incl A B -> Incl (f A) (f B).

Definition F:CLASS := fun A:SubU => Incl (f A) A.
Definition FI:SubU := Cinter F.

Lemma FI_Incl: forall A:SubU, F A -> Incl FI A.

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

Lemma FIf_Incl: forall 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: forall A:SubU, Eq1 A (f A) -> Incl FI A.

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


(* Jakby komus bylo malo :) *)

Definition Eq2 := fun A B:SubU => forall u:U, A u <-> B u.

Lemma Eq1_Eq2: forall A B:SubU, Eq1 A B <-> Eq2 A B.

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

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

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

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

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

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

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

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

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

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

Definition is_empty : SubU -> Prop := fun S => forall u:U, ~(S u).

Definition disjoint : SubU -> SubU -> Prop := fun 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 *)