(*:maxLineLen=80:*)
(* Vodite racuna kada preuzimate fajl da skinete thy, a ne htm - njega mozete koristiti samo za brz 
pregled zato sto je laksi za online citanje *)

text\<open>\newpage\<close>

section \<open>Klasična logika\<close>
(* section \<open> Classical propositional logic \<close> *)

theory Cas4_vezbe
imports Main "HOL-Library.LaTeXsugar"

begin

(*
 \footnote{Dodati tekst iz: @{url \<open>http://www21.in.tum.de/~ballarin/fomus/part1/part1.pdf\<close>}}
*)

(*subsection \<open>Podsećanje sa predavanja\<close>*)

subsection \<open>Pravilo ccontr - klasična kontradikcija\<close>

text\<open>Početkom 20. veka određen broj matematičara izrazio je svoje kritike klasične matematike.
Naime, u klasičnoj matematici se često postojanje nekog objekta dokazuje svođenjem na kontradikciju,
tako što se dokaže da nije moguće da takav objekat ne postoji, iako se traženi objekat ne konstruiše
efektivno. 

Razmotrimo naredni čuveni primer takvog dokaza. Dokazaćemo da postoje iracionalni brojevi $a$ i $b$
takvi da je $a^b$ racionalan broj. Razmotrimo broj ${\sqrt{2}}^{\sqrt{2}}$. Ako je on racionalan,
tada je dokaz završen, jer možemo uzeti $a = \sqrt{2}$ i $b = \sqrt{2}$, znajući da je $\sqrt{2}$
iracionalan broj. Ako on nije racionalan, tada možemo uzeti da je $a = {\sqrt{2}}^{\sqrt{2}}$ i
$b=\sqrt{2}$. I jedan i drugi broj je iracionalan, dok je $a^b$ =
$({\sqrt{2}}^{\sqrt{2}})^{\sqrt{2}}$ = ${\sqrt{2}}^{(\sqrt{2} \sqrt{2})}$ = ${\sqrt{2}}^2 = 2$
racionalan broj. Time je dokaz završen.

Dakle, dokazali smo tvrđenje o postojanju traženih brojeva, a da i dalje ne umemo eksplicitno da ih
navedemo, jer zapravo ne znamo da li je ${\sqrt{2}}^{\sqrt{2}}$ racionalan ili iracionalan broj.
Predstavnici tzv. \emph{konstruktivističke matematike} odbacuju takve dokaze i zahtevaju da dokazi
postojanja nekih objekata uključuju i mogućnost njihove efektivne konstrukcije. Kao logička osnova
konstruktivističke matematike pojavljuje se \emph{intuicionistička logika}. Intuicionistička logika
odbacuje nekonstruktivne postupke dokazivanja koji su zasnovani na zakonu isključenja trećeg \<open>A \<or> \<not>
A\<close>, kao i na zakonu dvostruke negacije \<open>\<not> \<not> A \<longrightarrow> A\<close>. 

Dokazivanje svođenjem na kontradikciju je dopušteno samo za negativna tvrđenja: moguće je dokazati
tvrđenje \<open>\<not> A\<close> tako što se dokaže da iz pretpostavke \<open>A\<close> sledi kontradikcija, ali nije dopušteno da
se tvrđenje \<open>A\<close> dokaže tako što se iz pretpostavke \<open>\<not> A\<close> dokaže kontradikcija.

Do sada su svi dokazi bili u okviru intuicionističke logike. Dokazi u klasičnoj logici podrazumevaju
uvođenje bar još jednog novog, klasičnog pravila. U sistemu Isabelle/HOL jedna mogućnost je da se
koristi \emph{pravilo klasične kontradikcije} @{text ccontr}: @{thm [mode=Proof] ccontr [no_vars]}.
U udžbenicima matematičke logike, to pravilo se zapisuje ovako:

$$\infer{P}{\infer*{False}{[\neg P]}}$$

Primetimo da smo za rad sa negacijom koristili smo pravilo uvođenja negacije @{text "notI:"} @{thm
[mode=Proof] notI [no_vars]}, koje je slično pravilu klasične kontradikcije. Ključna razlika je ta
što se pravilom uvođenja negacije dokaz kontradikcijom primenjuje samo na negirane formule, što je u
skladu sa intuicionističkom logikom i konstruktivnom matematikom.
Otuda se u intuicionističkoj logici lako dokazuje naredna lema:\<close>

lemma
  shows "A \<longrightarrow> \<not> \<not> A"
  apply (rule impI)
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

text\<open>Međutim, u klasičnoj logici važi pravilo duple negacije:
\begin{exmp}
@{text "\<not> \<not> A \<longrightarrow> A"}
\end{exmp}
\<close>

lemma
  shows "\<not> \<not> A \<longrightarrow> A"
  apply (rule impI)
\<comment> \<open>\<open> 1. \<not> \<not> A \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\emph{Primetimo da ovde ne možemo uspešno primeniti pravilo \<open>notE\<close> (što će 
biti prikazano u narednom dokazu) zato što ono očekuje da iz \<open>\<not> P\<close> i \<open>P\<close> možemo 
da izvedemo bilo šta. \<open>\<not> P\<close> je ovde \<open>\<not> \<not> A\<close>, što znači da je \<open>P\<close> u stvari 
\<open>\<not> A\<close>, i zato ono postaje preostali cilj koji se ne može dokazati.}\<close>
\<comment> \<open>\emph{Primenjujemo pravilo \<open>ccontr\<close>.}\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> \<not> A; \<not> A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Pa sada možemo da primenimo pravilo \<open>notE\<close> i jednostavno završavamo 
dokaz.}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<not> A \<Longrightarrow> \<not> A\<close>\<close>
  apply assumption
\<comment> \<open>\<open>No subgoals!\<close>\<close>
  done

text\<open>Dokaz, naravno, nije moguće izvršiti u intuicionističkoj logici.\<close>

lemma
  shows "\<not> \<not> A \<longrightarrow> A"
\<comment> \<open>\emph{Jedino intuicionističko pravilo koje se može primeniti je \<open>impI\<close>}\<close>
  apply (rule impI)
\<comment> \<open>\<open> 1. \<not> \<not> A \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\emph{Jedino primenjivo pravilo je \<open>notE\<close>}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<not> A\<close>\<close>
\<comment> \<open>\emph{Cilj koj je dobijen je jasno nedokaziv, pa odustajemo od dokaza.}\<close>
  oops

text \<open>Dokažimo i narednu klasičnu teoremu koja ne važi u intuicionističkoj logici:

\begin{exmp}
@{text "(\<not> P \<longrightarrow> P) \<longrightarrow> P"}
\end{exmp}
\<close>

lemma 
  shows "(\<not> P \<longrightarrow> P) \<longrightarrow> P"
  apply (rule impI)
\<comment> \<open>\<open> 1. \<not> P \<longrightarrow> P \<Longrightarrow> P\<close>\<close>
\<comment> \<open>\emph{Ako bismo pokušali da primenimo \<open>impE\<close> dobili bi \<open>\<not> P\<close> kao novi cilj, 
što je nemoguće dokazati.}\<close>
\<comment> \<open>\emph{Pa vidimo da je jedino primenjivo pravilo \<open>ccontr\<close>}\<close>  
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> P \<longrightarrow> P; \<not> P\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Sada pokušavamo sa \<open>impE\<close>}\<close>
  apply (erule impE)
\<comment> \<open>\<open> 1. \<not> P \<Longrightarrow> \<not> P\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{I vidimo da je u prvom cilju pretpostavka ista kao zaključak}\<close>
   apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>\<not> P; P\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Primenjujemo \<open>notE\<close>}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. P \<Longrightarrow> P\<close>\<close>
  apply assumption
  done

text \<open> Od četiri smera de Morganovih zakona koji povezuju negaciju, disjunkciju i konjunkciju, tri
važe i mogu se dokazati i u intuicionističkoj logici, dok je za dokaz narednog zakona potrebno
upotrebiti i pravila klasične logike.

\begin{exmp}
@{text "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"}
\end{exmp}

Često se nad disjunkcijom u zaključku primenjuje pravilo @{text ccontr}, što ćemo videti u narednom
dokazu. \<close>

lemma
  shows "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"
  apply (rule impI) 
\<comment> \<open>\<open> 1. \<not> (A \<and> B) \<Longrightarrow> \<not> A \<or> \<not> B\<close>\<close>
\<comment>\<open>\emph{Primena pravila \<open>ccontr\<close> će prebaciti zaključak u negativnom obliku u 
pretpostavke, i zajedno sa preostalim pretpostavkama pokušavamo da dokažemo 
kontradikciju.}\<close>
  apply (rule ccontr) 
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (A \<and> B); \<not> (\<not> A \<or> \<not> B)\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment>\<open>\emph{Sada imamo dve pretpostavke na koje možemo primeniti isto pravilo (u 
ovom slučaju \<open>notE\<close>), možemo da biramo da li ćemo to pravilo primeniti na prvu ili 
drugu pretpostavku. Međutim ovde nam odgovara da izaberemo prvu pretpostavku (i da ne 
upotrebimo naredbu \<open>back\<close>), zato što je u njoj konjunkcija - a ta formula se 
prebacuje u zaključak. Pogodnije je u zaključku raditi sa konjunkcijom nego 
sa disjunkcijom;
Napomena: pogledajte šta se dešava kada stavite back}\<close>
  apply (erule notE) 
\<comment> \<open>\<open> 1. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> A \<and> B\<close>\<close>
  apply (rule conjI)
\<comment> \<open>\emph{Sada prvo primenjujemo pravilo uvođenja konjunkcije i dobijamo dva nova cilja:}\<close>
\<comment> \<open>\<open> 1. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> B\<close>\<close>
\<comment>\<open>\emph{Sada dokazujemo prvi podcilj i ponovo primenjujemo pravilo \<open>ccontr\<close>.}\<close>
   apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<not> A \<or> \<not> B); \<not> A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> B\<close>\<close>
   apply (erule notE) 
\<comment>\<open>\emph{Sada primenjujemo pravilo \<open>notE\<close> na prvu pretpostavku jer nam u ovoj 
situaciji odgovara da imamo disjunkciju u zaključku.}\<close>
\<comment> \<open>\<open> 1. \<not> A \<Longrightarrow> \<not> A \<or> \<not> B\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> B\<close>\<close>
   apply (rule disjI1)
\<comment> \<open>\<open> 1. \<not> A \<Longrightarrow> \<not> A\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> B\<close>\<close>
   apply assumption
\<comment>\<open>\emph{Dokazan je prvi podcilj i sada dokazujemo drugi podcilj.}\<close>
\<comment> \<open>\<open> 1. \<not> (\<not> A \<or> \<not> B) \<Longrightarrow> B\<close>\<close>
\<comment>\<open>\emph{Ponovo primenjujemo pravilo \<open>ccontr\<close> i završavamo dokaz na sličan način 
kao malopre.}\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<not> A \<or> \<not> B); \<not> B\<rbrakk> \<Longrightarrow> False\<close>\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<not> B \<Longrightarrow> \<not> A \<or> \<not> B\<close>\<close>
  apply (rule disjI2)
\<comment> \<open>\<open> 1. \<not> B \<Longrightarrow> \<not> B\<close>\<close>
  apply assumption
\<comment> \<open>\<open>No subgoals!\<close>\<close>
  done


text \<open> 
\begin{exmp}
Pokazati klasični deo de-Morganovog zakona za kvantifikatore:
@{text "(\<not> (\<forall> x. P x)) \<longrightarrow> (\<exists> x. \<not> P x)"}
\end{exmp}

Napomena: Slično kao i u slučaju iskazne logike, ovo je jedino od četiri de-Morganova pravila za
kvantifikatore, koje se dokazuje uz pomoć principa klasične logike.

Intuitivno, ako važi pretpostavka \<open>\<not> (\<forall> x. P x)\<close>, onda \<open>P x\<close> nije tačno za svako \<open>x\<close>, odnosno
postoji neko \<open>a\<close> za koje \<open>P a\<close> nije tačno. Odnosno, za koje važi \<open>\<not> P a\<close>. S obzirom na ovu
činjenicu, možemo da zaključimo da postoji neko \<open>x\<close> za koje je \<open>\<not> P x\<close> tačno, tj. tačno je 
\<open>\<exists> x. \<not> P x\<close>. \<close>

lemma de_Morgan: 
  shows "(\<not> (\<forall> x. P x)) \<longrightarrow> (\<exists> x. \<not> P x)"
  apply (rule impI)
\<comment> \<open>\<open> 1. \<not> (\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x\<close>\<close>
\<comment>\<open>\emph{Primenjujemo pravilo \<open>ccontr\<close>, pretpostavljamo suprotno, tj. 
prebacujemo negaciju zaključka na levu stranu sa ciljem da dokažemo 
kontradikciju.}\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<forall>x. P x); \<nexists>x. \<not> P x\<rbrakk> \<Longrightarrow> False\<close>\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<lbrakk>\<nexists>x. \<not> P x\<rbrakk> \<Longrightarrow> \<forall>x. P x\<close>\<close>
\<comment> \<open>\emph{Primenjujemo pravilo \<open>notE\<close> da bismo eliminisali negaciju u prvoj
pretpostavci. Nakon ovog pravila došli smo u situaciju da umesto polazne teoreme
dokazujemo njenu kontrapoziciju (sa eliminisanom dvostrukom negacijom). }\<close>
  apply (rule allI)
\<comment> \<open>\emph{Dokaz nastavljamo na uobičajeni način, uvodeći univerzalni 
kvantifikator (tj. dokazujući tvrđenje za proizvoljno ali fiksirano \<open>x\<close>.}\<close>
\<comment> \<open>\<open>1. \<And>x. \<nexists>x. \<not> P x \<Longrightarrow> P x \<close>\<close>
\<comment> \<open>\emph{U nastavku ponovo kombinacijom pravila \<open>ccontr\<close> i \<open>notE\<close> razmenjujemo
levu i desnu stranu i prelazimo na dokaz kontrapozicije.}\<close>
  apply (rule ccontr)
  apply (erule notE)
\<comment> \<open>\<open>1. \<And>x. \<not> P x \<Longrightarrow> \<exists> x. P x \<close>\<close>
\<comment> \<open>\emph{Dokaz je sada jednostavno završiti, jer je uvedeno proizvoljno \<open>x\<close>, 
svedok za \<open>\<not> P x\<close>.}\<close>
  apply (rule_tac x="x" in exI)
  apply assumption
  done

subsection \<open>Dodatni primeri\<close>

text\<open>U klasičnoj logici, dokazati naredna tvrđenja:\<close>

text \<open> 
\begin{exmp}
@{text "(\<not> B \<longrightarrow> \<not> A) \<longrightarrow> (A \<longrightarrow> B)"}
\end{exmp}
\<close>

lemma
  shows "(\<not> B \<longrightarrow> \<not> A) \<longrightarrow> (A \<longrightarrow> B)"
  apply (rule impI)
\<comment> \<open>\<open> 1. \<not> B \<longrightarrow> \<not> A \<Longrightarrow> A \<longrightarrow> B\<close>\<close>
  apply (rule impI)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> B \<longrightarrow> \<not> A; A\<rbrakk> \<Longrightarrow> B\<close>\<close>
  apply (rule ccontr) 
\<comment> \<open>\<open> 1. \<lbrakk>\<not> B \<longrightarrow> \<not> A; A; \<not> B\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{prebacuje zaključak sa desna na levo i pokušavamo da izvedemo 
kontradikciju}\<close>
  apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>A; \<not> B\<rbrakk> \<Longrightarrow> \<not> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A; \<not> B; \<not> A\<rbrakk> \<Longrightarrow> False\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>A; \<not> B; \<not> A\<rbrakk> \<Longrightarrow> False\<close>\<close>
  apply (erule notE) 
\<comment> \<open>\<open> 1. \<lbrakk>A; \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\emph{eliminacija negacije, ali treba da je primenimo na drugu negaciju, ne 
na \<open>\<not> B\<close>, već na \<open>\<not> A\<close>}\<close>
\<comment> \<open>\<open> 1. \<lbrakk>A; \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
  back
\<comment> \<open>\<open> 1. \<lbrakk>A; \<not> B\<rbrakk> \<Longrightarrow> A\<close>\<close>
  apply assumption
  done

text \<open> 
\begin{exmp}
@{text "(A \<longrightarrow> B) \<longrightarrow> (\<not> A \<or> B)"}
\end{exmp}
\<close>

lemma 
  shows "(A \<longrightarrow> B) \<longrightarrow> (\<not> A \<or> B)"
  apply (rule impI)
\<comment> \<open>\<open> 1. A \<longrightarrow> B \<Longrightarrow> \<not> A \<or> B\<close>\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>A \<longrightarrow> B; \<not> (\<not> A \<or> B)\<rbrakk> \<Longrightarrow> False\<close>\<close>
  apply (erule impE)
\<comment> \<open>\<open> 1. \<not> (\<not> A \<or> B) \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> (\<not> A \<or> B); B\<rbrakk> \<Longrightarrow> False\<close>\<close>
   apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<not> A \<or> B); \<not> A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> (\<not> A \<or> B); B\<rbrakk> \<Longrightarrow> False\<close>\<close>
   apply (erule notE)
\<comment> \<open>\<open> 1. \<not> A \<Longrightarrow> \<not> A \<or> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> (\<not> A \<or> B); B\<rbrakk> \<Longrightarrow> False\<close>\<close>
   apply (rule disjI1)
\<comment> \<open>\<open> 1. \<not> A \<Longrightarrow> \<not> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> (\<not> A \<or> B); B\<rbrakk> \<Longrightarrow> False\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<not> A \<or> B); B\<rbrakk> \<Longrightarrow> False\<close>\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. B \<Longrightarrow> \<not> A \<or> B\<close>\<close>
  apply (rule disjI2)
\<comment> \<open>\<open> 1. B \<Longrightarrow> B\<close>\<close>
  apply assumption
  done

text \<open> 
\begin{exmp}
@{text "(\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"}
\end{exmp}
\<close>

lemma 
  shows "(\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
  apply (rule iffI) 
\<comment>\<open>\emph{Dobijamo dva cilja; sada prvo primenjujemo pravilo uvođenja implikacije u prvom cilju.} \<close>
   apply (rule impI) 
\<comment>\<open>\emph{Sada prebacujemo zaključak na levu stranu i desno dobijamo False. }\<close>
   apply (rule ccontr) 
\<comment>\<open>\emph{Ovo nam odgovara zato što se sada \<open>\<not> P\<close> dodaje među pretpostavke, a već 
se pojavljuje kao leva strana implikacije. }\<close>
   apply (erule impE)
    apply (assumption)
   apply (erule notE)
   apply assumption 
\<comment>\<open>\emph{Sada smo zatvorili prvi cilj, pa slično sa drugim ciljom.}\<close>
  apply (rule impI)
  apply (rule ccontr) 
\<comment>\<open>\emph{Slično kao u prethodnoj primeni, odgovara nam da \<open>\<not> Q\<close> prebacimo u 
pretpostavke jer se već pojavljuje kao leva strana implikacije.}\<close>
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text \<open> 
\begin{exmp}
@{text "(\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"}
\end{exmp}
\<close>


lemma "(\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
  apply (rule iffI)
   apply (rule impI)
   apply (rule ccontr)
   apply (erule impE)
    apply assumption
   apply (erule notE)
   apply assumption
  apply (rule impI)
  apply (rule ccontr)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text \<open> \begin{exmp} Pirsov zakon. Tipičan ne-intuicionistički primer koji će sigurno zahtevati neki
oblik klasične kontradikcije. \<open>((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P\<close> \end{exmp} \<close>

lemma
  shows "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
  apply (rule impI)
  apply (rule ccontr) 
\<comment>\<open>\emph{Primena klasične kontradikcije, dodajemo negirani zaključak kao novu 
pretpostavku i pokušavamo da izvedemo kontradikciju.}\<close>
  apply (erule impE)
   apply (rule impI)
   apply (erule notE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text \<open>Aladin se nalazi ispred pećine u kojoj su dva kovčega. U svakom od kovčega se nalazi ili
blago ili smrtonosna zamka. Na kovčegu A piše da se bar u jednom od dva kovčega nalazi blago. Na
kovčegu B piše da se u kovčegu A nalazi smrtonosna zamka. Poznato je da su ili oba natpisa tačna ili
da nijedan od njih nije tačan. Odrediti sadržaj kovčega i dokazati odgovor.

Ako nijedan od natpisa ne bi bio tačan, tada nijedan od kovčega ne bi mogao da sadrži blago (jer je
natpis A netačan), dok bi kovčeg A morao da sadrži blago (pošto je natpis B netačan). Ovo je
kontradiktorno, pa je nemoguće da su oba natpisa netačna. Dakle, oba natpisa moraju biti tačna. Tada
kovčeg A sadrži smrtonosnu zamku, dok kovčeg B sadrži blago.

Formalizujmo ova tvrđenja u iskaznoj logici. Neka iskazna promenljiva \<open>bA\<close> označava da kovčeg A
sadrži blago, a iskazna promenljiva \<open>bB\<close> da kovčeg B sadrži blago (tada \<open>\<not> bA\<close> označava da je u
kovčegu A smrtonosna zamka, a \<open>\<not> bB\<close> da je u kovčegu B smrtonosna zamka. Neka promenljiva \<open>nA\<close>
označava da je natpis na kovčegu A tačan, a promenljiva \<open>nB\<close> da je natpis na kovčegu B tačan.

\begin{exmp}
@{text "(nA \<longleftrightarrow> bA \<or> bB) \<and> (nB \<longleftrightarrow> \<not> bA) \<and> ((nA \<and> nB) \<or> (\<not> nA \<and> \<not> nB)) 
\<longrightarrow> \<not> bA \<and> bB"}
\end{exmp}
\<close>

lemma
  shows "(nA \<longleftrightarrow> bA \<or> bB) \<and> (nB \<longleftrightarrow> \<not> bA) \<and> ((nA \<and> nB) \<or> (\<not> nA \<and> \<not> nB)) \<longrightarrow> 
          \<not> bA \<and> bB"
  \<comment>\<open>\emph{Primenjujemo očigledna pravila}\<close>
  apply (rule impI)
  apply (erule conjE)+
  apply (erule iffE)+
\<comment>\<open>\emph{Razmatramo dva slučaja}\<close>
  apply (erule disjE)
\<comment>\<open>\emph{U prvom slučaju su oba natpisa tačna}\<close>
   apply (erule conjE)
\<comment>\<open>\emph{Iz pretpostavki izvodimo da važi \<open>\<not> bA\<close> i da važi \<open>bA \<or> bB\<close>}\<close>
   apply (erule impE)
    apply assumption
   apply (erule impE) back
    apply assumption

\<comment>\<open>\emph{Posebno dokazujemo da važi \<open>\<not> bA\<close> i posebno \<open>bB\<close>}\<close>
   apply (rule conjI)
    apply assumption
\<comment>\<open>\emph{Pošto znamo da važi \<open>bA \<or> bB\<close> analiziramo slučaj da važi \<open>bA\<close> i \<open>bB\<close>}\<close>
   apply (erule disjE)
    apply (erule notE)
    apply assumption
   apply assumption

\<comment>\<open>\emph{U ovom slučaju nijedan od natpisa nije istinit. Dokaćemo da je to 
kontradiktorno}\<close>
  apply (erule conjE)
\<comment>\<open>\emph{Dokazaćemo prvo da iz pretpostavki sledi da blago mora biti bar u 
jednom kovčegu}\<close>
  apply (erule impE) back
\<comment>\<open>\emph{Pretpostavljamo suprotno (da blago nije ni u jednom kovčegu)}\<close>
   apply (rule ccontr)
\<comment>\<open>\emph{Odatle sledi da blago nije u kovčegu A}\<close>
   apply (erule impE) back back
    apply (rule notI)
    apply (erule notE) back back
    apply (rule disjI1)
    apply assumption
\<comment>\<open>\emph{Stoga je natpis B istinit, što je kontradikcija sa tim da nijedan od 
natpisa nije istinit.}\<close>
   apply (erule notE) back
   apply assumption
\<comment>\<open>\emph{Pošto je blago bar u jednom kovčegu, natpis A je istinit, što je 
kontradikcija sa tim da nijedan od natpisa nije istinit.}\<close>
  apply (erule notE)
  apply assumption
  done

subsection \<open> Pravilo classical \<close>

text\<open> Još jedno pravilo klasične logike koje možemo koristiti u sistemu Isabelle/HOL je @{text
"classical: (\<not> ?P \<Longrightarrow> ?P) \<Longrightarrow> ?P"}. Ovo pravilo podrazumeva da u dokazu teoreme uvek možemo
pretpostaviti negaciju zaključka teoreme dok pokušavamo da izvedemo upravo taj zaključak. Pravilo je
slično pravilu svođenja na kontradikciju @{text ccontr}. Jedina razlika je to što se kod pravila
@{text ccontr} iz negacije zaključka izvodi kontradikcija @{text False}, a kod pravila @{text
classical} izvodi zaključak teoreme.\<close>

text \<open> Dokažimo zakon isključenja trećeg korišćenjem pravila @{text classical} (primetimo da njega
ne bismo mogli da dokažemo samo korišćenjem pravila @{text ccontr} i pravilima uvođenja i
eliminacije veznika).

\begin{exmp}
@{text "P \<or> \<not> P"}
\end{exmp}
\<close>

lemma
  shows "P \<or> \<not> P"
\<comment>\<open>\emph{Da bi smo dokazali formulu \<open>A\<close>, dokazaćemo formulu \<open>\<not> A \<Rightarrow> A\<close>, pa 
primenjujemo pravilo \<open>classical\<close>.}\<close>
  apply (rule classical) 
\<comment> \<open>\<open> 1. \<not> (P \<or> \<not> P) \<Longrightarrow> P \<or> \<not> P\<close>\<close>
\<comment> \<open>\emph{Pošto je situacija simetrična, biramo da u cilju zadržimo prvi 
disjunkt, tj. \<open>P\<close>.}\<close>
  apply (rule disjI1) 
\<comment> \<open>\<open> 1. \<not> (P \<or> \<not> P) \<Longrightarrow> P\<close>\<close>
\<comment> \<open>\emph{Dokaz možemo nastaviti običnim svođenjem na kontradikciju, pa 
primenjujemo pravilo \<open>ccontr\<close> (naravno, bilo bi sasvim u redu i da se ponovo 
primeni pravilo \<open>classical\<close>.}\<close>
  apply (rule ccontr) 
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (P \<or> \<not> P); \<not> P\<rbrakk> \<Longrightarrow> False\<close>\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1.  \<not> P \<Longrightarrow> P \<or> \<not> P \<close>\<close>
  apply (rule disjI2)
\<comment> \<open>\<open> 1.  \<not> P \<Longrightarrow> \<not> P \<close>\<close>
  apply assumption
  done

subsection \<open>Razmatranje slučajeva - metod cases\<close>

text\<open>Dokazi po slučajevima se koriste kada je potrebno izvršiti grananje po
nekom uslovu u toku samog dokaza. Za navođenje uslova po kom se grananje vrši
može se koristiti metod \<open>cases\<close>. Iako ovi dokazi izlaze iz striktnog okvira
klasične prirodne dedukcije, oni mogu biti donekle jasniji od dokaza zapisanih
samo pomoću pravila prirodne dedukcije. Prikažimo primer jedne leme koju ćemo
prvo dokazati samo pomoću pravila prirodne dedukcije, a zatim pomoću metoda 
cases.\<close>

text\<open>Na ostrvu na kom se nalaze samo vitezovi i lažovi sreli smo osobu A koja je
rekla da su ona i osoba B iste vrste. Dokazati da je onda osoba B vitez.

Obeležimo sa \<open>A\<close> iskaznu promenljivu koja je tačna ako i samo ako je osoba A 
vitez tj. ako i samo ako osoba A govori istinu. Uvedimo promenljivu \<open>B\<close> istog
značenja i za osobu B. Osoba A govori istinu ako i samo ako su A i B ekvivalentne
promenljive. Zato se teorema može formulisati i dokazati na sledeći način.\<close>

text \<open>DA LI I OVAJ DOKAZ OBJASNITI?\<close>
lemma no_one_admits_knave_apply:
  shows "(A \<longleftrightarrow> (A \<longleftrightarrow> B)) \<longrightarrow> B"
  apply (rule impI)
  apply (erule iffE)
  apply (rule ccontr)
  apply (erule impE)
   apply (rule ccontr)
   apply (erule impE)
    apply (rule iffI)
     apply (erule notE) back
     apply assumption
    apply (erule notE)
    apply assumption
   apply (erule notE) back
   apply assumption
  apply (erule impE)
   apply assumption
  apply (erule iffE)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply (assumption)
  done

text\<open>Pređimo sada na dokaz u kom se koristi metoda \<open>cases\<close>. Prvo će biti naveden
dokaz ove leme bez objašnjenja, a zatim isti dokaz detaljno iskomentarisan sa
stanjima kroz koje prolazi dokazivač u toku dokazivanja. \<close> 
(* \footnote{Sana: Ova lema će kasnije biti dokazana u Isar-u, pa koristimo isto
ime.} *)

lemma no_one_admits_knave_apply_cases:
  shows "(A \<longleftrightarrow> (A \<longleftrightarrow> B)) \<longrightarrow> B"
  apply (rule impI)
  apply (cases A)
\<comment> \<open>\emph{Prva grana: A je tačno}\<close>
   apply (erule iffE)
   apply (erule impE)
    apply assumption
   apply (erule iffE)
   apply (erule impE) back
    apply assumption
   apply assumption
\<comment> \<open>\emph{Druga grana: A je netačno}\<close>
  apply (rule ccontr)
  apply (erule iffE)
  apply (erule impE) back
  apply (rule iffI)
    apply (erule notE) 
    apply assumption
   apply (erule notE) back
   apply assumption
  apply (erule notE) 
  apply assumption
  done

text\<open>Detaljno objašnjen prethodni dokaz teoreme:\<close>

lemma no_one_admits_knave_apply_cases_explained:
  shows "(A \<longleftrightarrow> (A \<longleftrightarrow> B)) \<longrightarrow> B"
  apply (rule impI)
\<comment> \<open>\<open> 1. A = (A = B) \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\emph{Odmah na početku dokaza, granamo ovaj dokaz po slučajevima da li je 
\<open>A\<close> tačno ili netačno. Kada se samo jedan term koristi u okviru metoda \<open>cases\<close> 
nema potrebe koristiti navodnike (inače su neophodni, što ćemo videti u narednom 
primeru).}\<close>
\<comment> \<open>\emph{Ovo će generisati dva nova cilja, u prvom se u skup pretpostavki 
dodaje nova pretpostavka da važi \<open>A\<close>, a u drugom se u skup pretpostavki dodaje 
pretpostavka da važi \<open>\<not> A\<close>.}\<close>
  apply (cases A)
\<comment> \<open>\<open> 1. \<lbrakk>A = (A = B); A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>

\<comment> \<open>\emph{Sada dokazujemo prvi cilj.}\<close>
\<comment> \<open>\emph{U pretpostavkama imamo ekvivalenciju pa primenjujemo pravilo \<open>iffE\<close> koje 
eliminiše ekvivalenciju i dodaje u skup pretpostavki dve implikacije.}\<close>
\<comment> \<open>\emph{Primetimo da zagrade ne stoje oko jednakosti sada, zato što jednakost 
odnosno ekvivalencija ima veći prioritet u odnosu na implikaciju.}\<close>
   apply (erule iffE)
\<comment> \<open>\<open> 1. \<lbrakk>A; A \<longrightarrow> A = B; A = B \<longrightarrow> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\emph{Sada eliminišemo prvu implikaciju (što nam odgovara jer se njena 
pretpostavka \<open>A\<close> već nalazi u spisku pretpostavci tekućeg cilja).}\<close>
   apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>A; A = B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A; A = B \<longrightarrow> A; A = B\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
    apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>A; A = B \<longrightarrow> A; A = B\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\emph{Sada elimišemo ekvivalenciju \<open>A = B\<close> što generiše dve nove implikacije 
koje se dodaju u pretpostavke.}\<close>
   apply (erule iffE)
\<comment> \<open>\<open> 1. \<lbrakk>A; A = B \<longrightarrow> A; A \<longrightarrow> B; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\emph{Sada imamo tri implikacije u pretpostavkama i želimo da eliminišemo drugu 
implikaciju (jer formulu \<open>A\<close> imamo među ostalim pretpostavkama). Pa odmah 
planiramo da pozovemo naredbu \<open>back\<close> nakon ove naredbe.}\<close>
   apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>A; A \<longrightarrow> B; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A = B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A; A \<longrightarrow> B; B \<longrightarrow> A; A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
    back
\<comment> \<open>\<open> 1. \<lbrakk>A; A = B \<longrightarrow> A; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A; A = B \<longrightarrow> A; B \<longrightarrow> A; B\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
    apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>A; A = B \<longrightarrow> A; B \<longrightarrow> A; B\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
   apply assumption
\<comment> \<open>\emph{Dokazali smo prvi cilj, odnosno prvi slučaj kada je \<open>A\<close> tačno.}\<close>

\<comment> \<open>\emph{Sada dokazujemo drugi cilj.}\<close>
\<comment> \<open>\<open> 1. \<lbrakk>A = (A = B); \<not> A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\emph{Sada primenjujemo pravilo \<open>ccontr\<close>, odnosno pretpostavimo suprotno od 
tekućeg cilja i dokažimo da onda dobijamo kontradikciju.}\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>A = (A = B); \<not> A; \<not> B\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Sada prvo eliminišemo ekvivalenciju iz pretpostavki, čime dobijamo dve nove 
implikacije.}\<close>
  apply (erule iffE)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A = B \<longrightarrow> A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Pošto prva implikacija sledi iz \<open>A\<close>, a u pretpostavkama imamo 
da važi \<open>\<not> A\<close>, možemo da zaključimo da nam ne odgovara da eliminišemo prvu 
implikaciju pa pokušavamo sa drugom i odmah planiramo da pozovemo naredbu \<open>back\<close> 
nakon ove naredbe.}\<close>
  apply (erule impE) 
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; \<not> B; A = B \<longrightarrow> A\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
   back
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B\<rbrakk> \<Longrightarrow> A = B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Sada primenjujemo pravilo uvođenja ekvivalencije na \<open>A = B\<close> i dobijamo dva 
nova cilja.}\<close>
   apply (rule iffI)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; B\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Pošto u pretpostavkama imamo \<open>\<not> A\<close> i \<open>A\<close>, odgovara nam da pokušamo da 
eliminišemo prvu negaciju.}\<close>
    apply (erule notE) 
\<comment> \<open>\<open> 1. \<lbrakk>\<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; B\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
    apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; B\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Pošto u pretpostavkama imamo \<open>\<not> B\<close> i \<open>B\<close>, odgovara nam da pokušamo da 
eliminišemo drugu negaciju pa planiramo da pozovemo \<open>back\<close> nakon naredne 
naredbe.}\<close>
   apply (erule notE)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> B; A \<longrightarrow> A = B; B\<rbrakk> \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
   back
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; A \<longrightarrow> A = B; B\<rbrakk> \<Longrightarrow> B\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>\<not> A; \<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Pošto u pretpostavkama imamo \<open>\<not> A\<close> i \<open>A\<close>, odgovara nam da pokušamo da 
eliminišemo prvu negaciju.}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> B; A \<longrightarrow> A = B; A\<rbrakk> \<Longrightarrow> A\<close>\<close>
  apply assumption
\<comment> \<open>\<open>No subgoals!\<close>\<close>
  done

text \<open>text\<open>
\begin{exmp}
Paradoks pijanca: postoji osoba za koju važi, ako je on pijanac onda su i svi 
ostali pijanci.
\end{exmp}

Pokazaćemo nekoliko različitih dokaza ovog tvrđenja.\<close>\<close>

 
text\<open>
\begin{exmp}
Paradoks pijanca: postoji osoba za koju važi, ako je on pijanac onda su i svi 
ostali pijanci.
\end{exmp}
\<close>

text\<open>Neformalni dokaz ove teoreme razlikuje slučajeve kada svi piju i kada
postoji neka osoba koja ne pije. Ako svi piju, onda su zaista svi pijanci, a u
suprotnom za tu osobu možemo reći da ako je on pijanac, onda su svi pijanci (to
je tačno jer pretpostavka te implikacije nije tačna). Ovo možemo sprovesti i u
formalnom dokazu tako što koristimo metod \<open>cases\<close> ali sada formulu po kojom
granamo navodimo između dvostrukih navodnika.

Prvo navodimo dokaz bez objašnjenja, pa nakon toga detaljno objašnjen dokaz sa
stanjima kroz koja prolazi dokazivač.\<close>

lemma Drinker's_Principle1_bez_objasnjenja:
  "\<exists> x. (drunk x \<longrightarrow> (\<forall> x. drunk x))"
  apply (cases "\<forall> x. drunk x")
\<comment>\<open>prva grana\<close>
   apply (rule exI)
   apply (rule impI)
   apply assumption
\<comment>\<open>druga grana\<close>
  apply (rule ccontr)
  apply (erule notE)
  apply (rule allI)
  apply (rule ccontr)
  apply (erule notE)
  apply (rule_tac x = "x" in exI)
  apply (rule impI)
  apply (erule notE)
  apply assumption
  done

text\<open>Detaljno objašnjen dokaz teoreme:\<close>

lemma Drinker's_Principle1:
  "\<exists> x. (drunk x \<longrightarrow> (\<forall> x. drunk x))"
\<comment> \<open>\emph{Prvo granamo prema tome da li zaključak važi ili ne, primenjujemo 
metod \<open>cases\<close> i dobijamo dve grane, odnosno dva podcilja.}\<close>
  apply (cases "\<forall> x. drunk x")
\<comment> \<open>\<open> 1. \<forall>x. drunk x \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\emph{Sada dokazujemo prvu granu. Moramo primetiti da nam nije bitan svedok 
tako da možemo da primenimo pravilo \<open>exI\<close> bez instanciranja promenljive.}\<close>
   apply (rule exI)
\<comment> \<open>\<open> 1. \<forall>x. drunk x \<Longrightarrow> drunk ?x1 \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\emph{Sada primenjujemo pravilo uvođenja implikacije u zaključak.}\<close>
   apply (rule impI)
\<comment> \<open>\<open> 1. \<lbrakk>\<forall>x. drunk x; drunk ?x1\<rbrakk> \<Longrightarrow> \<forall>x. drunk x\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\emph{I lako dokazujemo prvu granu.}\<close>
   apply assumption

\<comment> \<open>\emph{Sada dokazujemo drugu granu.}\<close>
\<comment> \<open>\<open> 1. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\emph{Prvo primenjujemo klasičnu kontradikciju, odnosno negaciju zaključka 
prebacujemo u pretpostavke i pokušavamo da izvedemo kontradikciju.}\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<forall>x. drunk x); \<nexists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Sada eliminišemo negaciju iz pretpostavki.}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<nexists>x. drunk x \<longrightarrow> (\<forall>x. drunk x) \<Longrightarrow> \<forall>x. drunk x\<close>\<close>
\<comment> \<open>\emph{Pa univerzalni kvantifikator iz zaključka.}\<close>
  apply (rule allI)
\<comment> \<open>\<open> 1. \<And>x. \<nexists>x. drunk x \<longrightarrow> (\<forall>x. drunk x) \<Longrightarrow> drunk x\<close>\<close>
\<comment> \<open>\emph{Ponovo primenjujemo pravilo klasične kontradikcije.}\<close>
  apply (rule ccontr)
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<nexists>x. drunk x \<longrightarrow> (\<forall>x. drunk x); \<not> drunk x\<rbrakk> \<Longrightarrow> False\<close>\<close>
\<comment> \<open>\emph{Eliminišemo negaciju iz pretpostavki.}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<And>x. \<not> drunk x \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\emph{Sada instanciramo egzistencijalni kvantifikator u zaključku 
promenljivom \<open>x\<close> koju smo već uveli.}\<close>
  apply (rule_tac x = "x" in exI)
\<comment> \<open>\<open> 1. \<And>x. \<not> drunk x \<Longrightarrow> drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\emph{Sada primenjujemo pravilo uvođenja implikacije u zaključku.}\<close>
  apply (rule impI)
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<not> drunk x; drunk x\<rbrakk> \<Longrightarrow> \<forall>x. drunk x\<close>\<close>
\<comment> \<open>\emph{Sada eliminišemo negaciju iz pretpostavki.}\<close>
  apply (erule notE)
\<comment> \<open>\<open> 1. \<And>x. drunk x \<Longrightarrow> drunk x\<close>\<close>
  apply assumption
\<comment> \<open>\<open>No subgoals!\<close>\<close>
  done

text\<open>U PREOSTALOJ PRIČI IZ DELA 5 se krije nekoliko nezavisne stvari, koje bi
bilo dobro objasniti sve, ali na jednostavnijim primerima:

\<^item> FRULE - naći neki jednostavniji primer gde se univerzalni kvantifikator mora
koristiti više puta. Npr. 
\<close>

lemma 
  shows "(\<forall> x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f (f a))"
  apply (rule impI)
  apply (erule conjE)
  apply (frule_tac x=a in spec)
  apply (erule impE)
   apply assumption
  apply (erule_tac x="f a" in allE)
  apply (erule impE)
   apply assumption
  apply assumption
  done

text\<open>\footnote{filip: SAMO OVDE OBJASNITI ŠTA JE FRULE I OBJASNITI PRETHODNI PRIMER.}\<close>

text \<open>
\<^item> \verb|SUBGOAL_TAC| - ne smeta mi čak i ako bismo ovo izostavili, a ako ostane treba naći
neki jednostavan primer.
\<close>

text\<open>
\<^item> Primena ranije dokazanih lema.
\<^item> Odnos zapisa u meta-logici i objektnoj logici i \verb|rule_format|.

I jedno i drugo je lepo da se objasni, samo može da se nađe možda neki
jednostavniji primer? \<close>

(*
text\<open>
\paragraph{Dokaz uz korišćenje pomoćne leme:}

U naredna dva dokaza paradoksa pijanca koristi se klasični deo de-Morganovog 
zakona koji smo već dokazali ali ga navodimo ponovo.\<close>

lemma de_Morgan':
  shows "(\<not> (\<forall> x. P x)) \<longrightarrow> (\<exists> x. \<not> P x)"
  apply (rule impI)
  apply (rule classical)
  apply (erule notE) 
  apply (rule allI)
  apply (rule classical)
  apply (erule notE)
  apply (rule_tac x = "x" in exI)
  apply assumption
  done

text\<open>Prikazaćemo dve verzije dokaza uz pomoć pravila prirodne dedukcije
koje koriste ovu lemu.

\paragraph{Korišćenje pomoćne leme u dokazu:}

Moguće je koristiti i pomoćne leme u apply-skript dokazima, na način koji je
veoma sličan primeni pravila prirodne dedukcije.

- \verb!apply (rule! \<open>theorem\<close>\verb!)! - primenjuje se ako se zaključak teoreme
poklapa sa zaključkom tekućeg cilja.

- \verb!apply (erule! \<open>theorem\<close>\verb!)! - primenjuje se ako se zaključak teoreme
poklapa sa zaključkom tekućeg cilja i prva pretpostavka se poklapa sa pretpostavkom
tekućeg cilja.
 
- \verb!apply (frule! \<open>theorem\<close>\verb!)! - primenjuje se kada se prva pretpostavka
teoreme poklapa sa pretpostavkom tekućeg cilja.

- \verb!apply (drule! \<open>theorem\<close>\verb!)! - slično kao pravilo \<open>frule\<close> s tim što
se pretpostavka koja se koristi briše.

\paragraph{Naredba \<open>[rule_format]\<close>:}

Naredba \<open>rule_format\<close> naglašava Isabelle/HOL da se u tvrđenju leme svako \<open>\<longrightarrow>\<close>
zameni sa \<open>\<Longrightarrow>\<close> pre čuvanja ili primene dokazane leme. Može se koristiti ili
prilikom pozivanja određene leme (u dokazu druge leme - kao što će biti
prikazano u nastavku teksta) ili se može navesti odmah nakon definisanja same
leme (što čitalac može pokušati sam). Ovakva transformacija leme olakšava njenu
primenu u dokazima drugih lema.

\paragraph{Dodavanje među-cilja, metod \<open>subgoal_tac\<close>:}

Metod \<open>subgoal_tac\<close> se koristi da bismo u dokazu dodali novu pretpostavku koju
planiramo da koristimo u dokazu konačnog cilja. Ovo nam omogućava da koristimo
pretpostavku pre nego što je dokažemo, i da se ovaj međukorak (odnosno
pretpostavka koja je korišćena) dokazuje tek nakon dokazivanja konačnog cilja.
Ovaj metod generiše dva cilja: prvi cilj nastaje od polaznog cilja čiji je
spisak pretpostavki proširen novom pretpostavkom, drugi cilj je da se iz prethodnih
pretpostavki dokaže nova pretpostavka.\<close>

(* ovo iskomentarisati negde kasnije --- kod isara ako moze *) 

text\<open>Videćemo i razliku između primene lema @{text de_Morgan} (zapisane sa
@{text "\<longrightarrow>"}) i @{text de_Morgan1} (zapisane sa @{text "\<Longrightarrow>"}).\<close>

(* \footnote{Sana: Ovo može tek sa isar-om, pomeriti tamo ili obrisati.} *)

lemma Drinker's_Principle2:
  "\<exists> x. (drunk x \<longrightarrow> (\<forall> x. drunk x))"
  apply (cases "\<forall> x. drunk x")
\<comment>\<open>\emph{Prva grana se dokazuje na isti način}\<close>
   apply (rule exI)
   apply (rule impI)
   apply assumption
\<comment>\<open>\emph{Druga grana se razlikuje!}\<close>
\<comment>\<open>\emph{Koristimo pravilo \<open>subgoal_tac\<close> i dodajemo novu pretpostavku. Ovo 
generiše dva cilja.}.\<close>
  apply (subgoal_tac "\<exists> x. \<not> drunk x")
\<comment> \<open>\<open> 1. \<lbrakk>\<not> (\<forall>x. drunk x); \<exists>x. \<not> drunk x\<rbrakk> \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
\<comment> \<open>\emph{Sada iz pretpostavki (iz nove pretpostavke) eliminišemo egzistencijalni 
kvantifikator.}\<close>
   apply (erule exE)
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<not> (\<forall>x. drunk x); \<not> drunk x\<rbrakk> \<Longrightarrow> \<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
\<comment> \<open>\emph{Sada pokušavamo sa tim istim \<open>x\<close> primenimo pravilo uvođenja egzistencijalnog 
kvantifikatora u zaključku.}\<close>
   apply (rule_tac x = "x" in exI)
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<not> (\<forall>x. drunk x); \<not> drunk x\<rbrakk> \<Longrightarrow> drunk x \<longrightarrow> (\<forall>x. drunk x)\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
\<comment> \<open>\emph{Sada primenjujemo pravilo uvođenja implikacije u zaključku, čime se pretpostavka iz 
zaključka prebacuje u pretpostavke samog cilja.}\<close>
   apply (rule impI)
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<not> (\<forall>x. drunk x); \<not> drunk x; drunk x\<rbrakk> \<Longrightarrow> \<forall>x. drunk x\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
\<comment>\<open>\emph{Sada u pretpostavkama imamo \<open>\<not> drunk x\<close> i \<open>drunk x\<close>, pa želimo da 
primenimo pravilo \<open>notE\<close> upravo na \<open>\<not> drunk x\<close> (što je druga negacija u 
pretpostavkama). Zbog toga odmah planiramo da nakon primene pravila \<open>notE\<close> pozovemo 
naredbu \<open>back\<close>.} \<close> 
   apply (erule notE) 
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<not> drunk x; drunk x\<rbrakk> \<Longrightarrow> \<forall>x. drunk x\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
   back
\<comment> \<open>\<open> 1. \<And>x. \<lbrakk>\<not> (\<forall>x. drunk x); drunk x\<rbrakk> \<Longrightarrow> drunk x\<close>\<close>
\<comment> \<open>\<open> 2. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<exists>x. \<not> drunk x\<close>\<close>
\<comment>\<open>\emph{Sada je dokazan konačni cilj. Ostaje nam da dokažemo međukorak 
direktnom primenom leme \<open>de_Morgan\<close> nakon što je transformišemo u odgovarajući 
oblik naredbom \<open>[rule_format]\<close>}. Pošto se u zaključku teoreme nalazi upravo 
zaključak leme \<open>de_Morgan\<close> pozivamo je sa metodom \<open>rule\<close>.\<close>
  apply (rule de_Morgan[rule_format]) 
\<comment> \<open>\<open> 1. \<not> (\<forall>x. drunk x) \<Longrightarrow> \<not> (\<forall>x. drunk x)\<close>\<close>
  apply assumption
\<comment> \<open>\<open>No subgoals!\<close>\<close>
  done
*)
end