(* Komentarje lahko pisemo tako, da oznacimo zacetek in konec ... *)
\* ... ali pa povemo, da komentar sega vse do konca vrstice

\* Ime datoteke mora biti enako imenu modula
\* V eni datoteki je lahko le en modul.
\* TLC pozenemo z ukazom: java tlc2.TLC MeolicVaja1

---- MODULE MeolicVaja1 ----

\* Predviden cas za to vajo je 90 minut

\* TLC zahteva omejene spremenljivke
\* TRUE, FALSE in BOOLEAN so vgrajene vrednosti
\* Male in velike crke se razlikujejo, zato npr. True ni isto kot TRUE

ASSUME
  \A F,G \in {TRUE, FALSE} : (F => G) <=> (~F \/ G)

ASSUME
  \A F,G \in BOOLEAN : (F => G) <=> (~F \/ G)

\* Kvantifikator \A preberemo "za vsak". Pomeni, da je formula tavtologija.
\* Zvezo ~ \A preberemo "ni res, da za vsak" (ni isto kot "za nobenega").

\* Zveza ~ \A pomeni, da formula ni tavtologija, ni pa nujno protislovje.
\* Ce formula ni tavtologija ni nujno, da njena negacija je tavtologija.

ASSUME
  ~ \A F,G \in BOOLEAN : F \/ G

ASSUME
  ~ \A F,G \in BOOLEAN : ~(F \/ G)

\* Tavtologije v logiki, ki so podobne Huntingtonovim postulatom

ASSUME (* zaprtost *)
  \A F,G \in BOOLEAN : (F \/ G) \in BOOLEAN

ASSUME (* zaprtost *)
  \A F,G \in BOOLEAN : (F /\ G) \in BOOLEAN

ASSUME (* nevtralni element *)
  \A F \in BOOLEAN : (F \/ FALSE) <=> F

ASSUME (* nevtralni element *)
  \A F \in BOOLEAN : (F /\ TRUE) <=> F

ASSUME (* komutativnost *)
  \A F,G \in BOOLEAN : (F \/ G) <=> (G \/ F)

ASSUME (* komutativnost *)
  \A F,G \in BOOLEAN : (F /\ G) <=> (G /\ F)

ASSUME (* distributivnost *)
  \A F,G,H \in BOOLEAN : (F \/ (G /\ H)) <=> (F \/ G) /\ (F \/ H)

ASSUME (* distributivnost *)
  \A F,G,H \in BOOLEAN : (F /\ (G \/ H)) <=> (F /\ G) \/ (F /\ H)

ASSUME (* nasprotni element *)
  \A F \in BOOLEAN : (F \/ ~ F) <=> TRUE

ASSUME (* nasprotni element *)
  \A F \in BOOLEAN : (F /\ ~ F) <=> FALSE

\* Se vec tavtologij

ASSUME (* edinstvenost nasprotnega elementa *)
  \A F,G \in BOOLEAN :
    ~(~F <=> ~G) <=> ~(F <=> G)

ASSUME (* involucija *)
  \A F \in BOOLEAN :
    ~(~F) <=> F

ASSUME (* komplementarnost *)
  \A F \in BOOLEAN :
    /\ (F \/ ~F) <=> TRUE
    /\ (F /\ ~F) <=> FALSE

\* NALOGE 1-6
\* Preverite veljavnost nastetih tavtologij.
\* asociativnost: (A+B)+C = A+(B+C), (A*B)*C = A*(B*C) 
\* identiteta: A+1=1, A*0=0
\* idempotenca: A+A=A, A*A=A
\* absorbcija: A+A*B=A, A*(A+B)=A
\* sosednost: (A*B+A*~B)=A, (A+B)*(A+~B)=A
\* DeMorganov zakon: ~(A+B)=~A*~B, ~(A*B)=~A+~B

\* Pa se nekaj implikacij

ASSUME
  \A F \in BOOLEAN : FALSE => F

\* NALOGE 7-9
\* modus ponens
\* modus tollens
\* hipoteticni silogizem

\* Predikatna logika

\* Zveza \A x pomeni, da formula je tavtologija za vse x.
\* Zveza ~ \A x pomeni, da formula ni tavtologija za vse x.
\* Zveza \E x pomeni, da formula je tavtologija za vsaj en x.
\* Zveza ~ \E x pomeni, da formula ni tavtologija za noben x.

F(x) == (x <=> TRUE)
G(x) == (x <=> FALSE)

ASSUME
  \E x \in BOOLEAN : F(x)

ASSUME
  \E x \in BOOLEAN : ~F(x)

ASSUME
  ~ \A x \in BOOLEAN : F(x)

ASSUME
  ~ \A x \in BOOLEAN : ~F(x)

ASSUME
  (\A x \in BOOLEAN : F(x)) <=> (~ \E x \in BOOLEAN : ~ F(x))

\* Formule s kvantifikatorji so lahko zelo tezko razumljive,
\* se posebej, ce vkljucite negacijo.

ASSUME
  \A x \in BOOLEAN : \E y \in BOOLEAN : F(x) <=> G(y)

ASSUME
  ~ \E x \in BOOLEAN : \A y \in BOOLEAN : F(x) <=> G(y)

ASSUME
  (\A x \in BOOLEAN : (F(x) /\ G(x)))
  <=>
  ((\A x \in BOOLEAN : F(x)) /\ (\A x \in BOOLEAN : G(x)))

ASSUME
  ~(
     (\A x \in BOOLEAN : (F(x) \/ G(x)))
     <=>
     ((\A x \in BOOLEAN : F(x)) \/ (\A x \in BOOLEAN : G(x)))
  )
  
\* Predikate lahko definiramo posebej ali pa kar v formuli

F0(x,y) == ((x \/ y) <=> y)
F1(x,y) == ((x /\ y) <=> y)

ASSUME
  \E x \in BOOLEAN : \A y \in BOOLEAN : F0(x,y)

ASSUME
  \E x \in BOOLEAN : \A y \in BOOLEAN : F1(x,y)

ASSUME
  \E x \in BOOLEAN : \A y \in BOOLEAN : (x \/ y) <=> y

ASSUME
  \E x \in BOOLEAN : \A y \in BOOLEAN : (x /\ y) <=> y

\* Mnozice

ASSUME
  {1, 2, 3} = {3, 1, 2}

ASSUME
  {1, 2, 2, 3, 3, 3} = {3, 1, 1, 2}

ASSUME
  {1, 2} \cup {2, 3, 4} = {5, 4, 3, 2, 1} \cap {1, 2, 3, 4}

ASSUME 
  {1, 3} \subseteq {3, 2, 1}

ASSUME 
  {1, 2, 3} \ {1, 2} = {3}

ASSUME
  {1,2,3} \in SUBSET {1,2,3,4,5}

U == {1,2,3,4,5,6,7,8,9,10}
V == {1,3,5,7,9}

ASSUME 
  U \ V = {2,4,6,8,10}

F2(x,y) == (x \subseteq y)
F3(x,y) == (x = (x \cap y))

ASSUME
  \A x,y \in SUBSET V: F2(x,y) <=> F3(x,y)

\* NALOGA 10
\* Pokazi, da ce iz mnozice stevil 1-20 najprej odvzamemo
\* stevilo 1 ter vse veckratnike stevil 2 in 3, nato pa dodamo
\* stevili 2 in 3, potem dobimo mnozico {2,3,5,7,11,13,17,19},
\* to pa so ravno vsa prastevila manjsa ali enaka 20.

====