chapter \<open>Dokazi u matematičkoj logici\<close>

text\<open>\newpage\<close>

section \<open>Prirodna dedukcija u Isabelle/HOL\<close>
(* section \<open> Intiutionistic propositional logic\<close> *)                          

theory Cas2_vezbe
(*  imports "HOL-Library.LaTeXsugar" "HOL-Library.OptionalSugar"  *)
  imports Main

begin

text\<open> Formalizacija matematike podrazumeva zapis svih tvrđenja na preciznom, formalnom jeziku i
njihovo dokazivanje u okviru određenog formalnog sistema, koji definiše pojam dokaza. Razvijeni su
mnogi formalni sistemi, ali jedan od najpoznatijih i slobodno možemo reći naprirodnijih je
\emph{prirodna dedukcija}, koju je uveo Gerhard Gencen, 1935. godine \cite{}. Dokazi u prirodnoj
dedukciji se izvode korišćenjem malog skupa jasno definisanih pravila (uključujući i jednu aksiomu).
Ova pravila podsećaju na pravila dokazivanja koja se koriste u svakodnevnoj, neformalnoj matematici.
Razlikovaćemo \emph{prirodnu dedukciju za iskaznu logiku} i \emph{prirodnu dedukciju za logiku prvog
reda}. U zavisnosti od toga da li se među pravilima nalaze i pravila koja omogućavaju dokaze
proizvoljnih tvrđenja svođenjem na kontradikciju razlikovaćemo \emph{intuicionističku} i
\emph{klasičnu prirodnu dedukciju} (više reči o ovome biće dato u posebnom poglavlju).

Za klasičnu prirodnu dedukciju za iskaznu logiku važi sledeća teorema potpunosti i saglasnosti:
\emph{Iskazna formula je dokaziva u klasičnoj prirodnoj dedukciji ako i samo ako je tautologija}. Za
klasičnu logiku prvog reda važi sledeća teorema potpunosti i saglasnosti: \emph{Formula logike prvog
reda je dokaziva u klasičnoj prirodnoj dedukciji ako i samo ako je valjana}. Podsetimo se iskazne
tautologije su one iskazne formule koje su tačne u svakoj iskaznoj valuaciji, dok su valjane formule
prvog reda one formule koje su tačne u svakom modelu (pri svakoj valuaciji). Naglasimo da ćemo u
logici prvog reda uvek posmatrati samo \emph{rečenice} tj. formule bez slobodnih promenljivih.
Tačnost iskaznih formula se može utvrditi ispitivanjem svih iskaznih valuacija (semantički) i
automatski dokazivači za iskaznu logiku su češće zasnovani na tom principu nego na korišćenju
prirodne dedukcije. Sa druge strane u logici prvog reda nije moguće ispitati sve moguće domene i
interpretacije date formule (njih najčešće ima beskonačno mnogo) i valjanost formula se stoga po
pravilu ispituje sintaksički (korišćenjem prirodne dedukcije ili nekog srodnog formalizma).

Prirodna dedukcija predstavlja osnovu sistema Isabelle/HOL i svaki dokaz koji se u ovom sistemu
proverava mora da bude sveden na pravila prirodne dedukcije. Međutim, zapis dokaza na nivou
elementarnih pravila prirodne dedukcije može biti veoma komplikovan -- takvi dokazi su veoma dugački
i potrebno je primeniti jako veliki broj pravila da bi se dokazalo i najelementarnije tvrđenje.
Stoga sistem Isabelle/HOL uvodi veliki broj automatskih metoda (npr. @{text "auto"}, @{text
"blast"}, @{text "metis"}, ...) koji korisnicima olakšavaju dokazivanje. Svi ti metodi u krajnjoj
instanci proizvode dokaz u sistemu prirodne dedukcije. Međutim, taj dokaz je skriven od korisnika,
ali je upravo u tom obliku dokaz je vidljiv sistemu i on se "iza scene" proverava.

Još jedan oblik "sakrivanja" pravila prirodne dedukcije od krajnjeg korisnika je korišćenje jezika
za zapis dokaza Isar. Jedan od ciljeva kreiranja tog jezika bio je da formalni dokazi u sistemu
Isabelle/HOL što je više moguće liče na neformalne dokaze iz matematičkih udžbenika. Iako se dokazi
iz udžbenika u nekoj meri zasnivaju na pravilima prirodne dedukcije, primena tih pravila je najčešće
implicitna (retko kada se u udžbeniku iz analize, geometrije, kombinatorike ili neke druge
matematičke oblasti autor direktno poziva na modus ponens ili neko slično pravilo prirodne
dedukcije, iako se ti dokazi suštinski zasnivaju na primeni tih pravila).

Uvođenje jezika Isar i automatskih metoda dokazivanja sa jedne, i prirodne dedukcije sa druge strane
možemo slobodno uporediti sa odnosom programiranja na višim programskim jezicima i programiranjem na
asembleru -- iako se svaki program u krajnjoj instanci prevede i zapiše na asembleru pre svog
izvršavanja, mnogo je udobnije programirati korišćenjem višeg nivoa apstrakcije. Slično, dokaze je
mnogo udobnije pisati u jeziku Isar uz primenu automatskih metoda, međutim, da bi oni mogli da budu
provereni, oni se automatski svode na dokaze zapisane u obliku pravila prirodne dedukcije (za
razliku od programa koji se izvršavaju, dokazi se proveravaju).

Dakle, sve leme koje se javljaju u ovom poglavlju se mogu veoma jednostavno dokazati korišćenjem
automatskih alata (praktično komandom @{text "by auto"}), ali te jednostavne leme će biti dokazane u
sistemu prirodne dedukcije (što se u praksi retko kad koristi), da bi se prikazalo kako se grade
dokazi koji koriste samo osnovna pravila prirodne dedukcije. Poznavanje pravila prirodne dedukcije
može doprineti kasnijem lakšem razumevanju jezika Isar. Dodatno, izučavanje formalnog sistema kakva
je prirodna dedukcija može čitaocu razjasniti koncept formalnog dokaza.\<close>

section\<open>Pravila prirodne dedukcije\<close>

text\<open>Svako od pravila prirodne dedukcije za iskaznu logiku vezano za neki logički veznik, dok kod
logike prvog reda postoje i pravila vezana za kvantifikatore. U intuicionističkoj logici nemamo
drugih pravila, dok u klasičnoj logici postoji bar još jedno dodatno pravilo, koje nije vezano ni za
jedan konkretan logički simbol. Za svaki logički veznik tj. kvantifikator postoje \emph{pravila
uvođenja} i \emph{pravila eliminacije}. Ta pravila ćemo nazivati \emph{intuicionistička pravila}.

Pravila uvođenja nekog veznika tj. kvantifikatora nam govore na koji način možemo da dokažemo
tvrđenja kod kojih se taj veznik tj. kvantifikator javlja kao primarni u zaključku. 

Na primer, da bi se dokazalo tvrđenje čiji je zaključak zapisan kao konjunkcija dva elementarnija
tvrđenja \<open>P \<and> Q\<close>, dovoljno je nezavisno dokazati ta dva elementarnija tvrđenja \<open>P\<close> i \<open>Q\<close>. Videćemo
da se ovaj jednostavan postupak dokazivanja u sistemu prirodne dedukcije formalizuje kroz pravilo
\emph{"uvođenje konjunkcije"}.

Pravila eliminacije nekog veznika tj. kvantifikatora nam govore kako da izmenimo skup pretpostavki
kada se u pretpostavkama tvrđenja koje se dokazuje nalazi neka formula kojoj se taj veznik tj.
kvantifikator javlja kao primarni (drugim rečima, kako da iz postojećih pretpostavki izvedemo neke
nove, koje logički slede iz njih).\<close>

text\<open>Na primer, jedno od osnovnih pravila u neformalnom dokazivanju je pravilo \emph{modus ponens}, koje
nam omogućava da iz dokazanog tvrđenja \<open>P\<close> i dokazanog tvrđenja \<open>P \<rightarrow> Q\<close>, izvedemo tj.
dokažemo tvrđenje \<open>Q\<close>. Ono u formalnom sistemu prirodne dedukcije odgovara pravilu
\emph{"eliminacije implikacije"}.

Dalje, na primer, ako je dokazano tvrđenje koje je zapisano u obliku univerzalno kvantifikovane
rečenice u kojoj se tvrdi da svi objekti imaju neko svojstvo, možemo slobodno smatrati da je
dokazano i tvrđenje koje tvrdi da neki konkretan objekat koji razmatramo ima to svojstvo. Videćemo
da se ovaj postupak dokazivanja formalizuje kroz pravilo \emph{"eliminacije univerzalnog
kvantifikatora"}.\<close>

text\<open>Proizvoljno pravilo prirodne dedukcije možemo zapisati ovako (nazovimo ga pravilo R):
$$\infer{Q}{P_1 & \ldots & P_n}$$ \<close>

text\<open>Pravila prirodne dedukcije možemo čitati i odozgo i odozdo: ako smo dokazali pretpostavke (ono
iznad crte), tada možemo smatrati da smo uspešno dokazali zaključak (ono što se nalazi ispod crte).
Sa druge strane možemo čitati odozdo na gore: da bi smo dokazali traženi zaključak dovoljno je da
dokažemo sve navedene pretpostavke.\<close>

text\<open>Delimo ih na pravila koja se odnose na zaključak tvrđenja - \emph{pravila uvođenja} (koja se u
sistemu Isabelle/HOL koriste uz metod @{text "rule"}) i pravila koja se odnose na pretpostavke
tvrđenja - \emph{pravila eliminacije} (koja se u sistemu Isabelle/HOL koriste uz metod @{text
"erule"}). Pored ova dva metoda, u situaciji kada se zaključak koji se dokazuje već nalazi u
pretpostavkama, koristi se metoda @{text "assumption"}. Ova situacija odgovara primeni aksiome
prirodne dedukcije.

Navedimo jedan kratak dokaz koji koristi tri osnovne metode @{text "rule"}, @{text "erule"} i @{text
"assumption"}. U prvom koraku se primenjuje pravilo uvođenja implikacije u zaključak tvrđenja
(@{text "impI"}), u drugom koraku se primenjuje pravilo eliminacije konjunkcije u pretpostavkama
tvrđenja (@{text "conjE"}), i u trećem koraku se prepoznaje da su pretpostavka i zaključak identični
(@{text "assumption"}). Primetimo da se svaki metod navodi nakon ključne reči @{text "apply"}, dok
se na kraju dokaza navodi ključna reč @{text "done"}.\<close>

lemma "A \<and> B \<longrightarrow> A"
  apply (rule impI) \<comment> \<open>\emph{Cilj postaje: } \<open>A \<and> B \<Longrightarrow> A\<close>.\<close>
  apply (erule conjE) \<comment> \<open>\emph{Cilj postaje: } \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>.\<close>
  apply assumption \<comment> \<open>\emph{Nema više podciljeva.}\<close>
  done \<comment> \<open>\emph{Dokazana teorema.}\<close>     

text\<open>Alternativa je zapisivanje ovakve formule uz pomoć \<open>assumes-shows\<close> bloka. Tada upotreba 
pravila uvođenja implikacije nije potrebna, mora se dodati korak \<open>using assms\<close> i dokaz izgleda 
ovako:\<close>

lemma 
  assumes "A \<and> B"
  shows "A"
  using assms
  apply (rule conjE)
  apply assumption
  done

section\<open>Pravila uvođenja i eliminacije za iskaznu logiku u Isabelle/HOL\<close>

text\<open>Iskazne formule u sistemu Isabelle/HOL se grade pomoću logičkih veznika konjunkcije (\<open>\<and>\<close>),
disjunkcije (\<open>\<or>\<close>), implikacije (\<open>\<longrightarrow>\<close>), ekvivalencije (\<open>\<longleftrightarrow>\<close>) i unarnog simbola negacije (\<open>\<not>\<close>). U nastavku ćemo izložiti pravila
prirodne dedukcije za iskaznu logiku (tj. za ove veznike), a u narednom poglavlju ćemo uvesti i
pravila za kvantifikatore i logiku prvog odnosno višeg reda. Pravila koja se odnose na iskazne
veznike su @{text conjI}, @{text conjE}, @{text disjI1}, @{text disjI2}, @{text disjE}, @{text
impI}, @{text impE}, @{text iffI}, @{text iffE}, @{text notI}, @{text notE}.


\begin{center}
\begin{tabular}{l@ {\qquad}l@ {\qquad}l}
Veznik & Pravilo uvođenja & Pravilo eliminacije \\
\<open>\<and>\<close> & conjI & conjE\\
\<open>\<or>\<close> & disjI1, disjI2 & disjE\\
\<open>\<longrightarrow>\<close> & impI & impE\\
\<open>\<longleftrightarrow>\<close> & iffI & iffE\\
\<open>\<not>\<close> & notI & notE \\
\end{tabular}
\end{center}
\<close>


text\<open>U sistemu Isabelle/HOL naredbom @{text "thm"} dobijamo zapis pravila čije ime navedemo, u
sintaksi meta-logike sistema Isabelle. Naredba @{text "thm"} može biti navedena u bilo kom delu
teorije, čak i u sklopu nekog dokaza, pri čemu ona ne čini deo samog dokaza tj. ne utiče na stanje u
kom se dokazivač nalazi. Zapis svih pravila iskazne logike dat je u nastavku (a objašnjenje jednog
po jednog od ovih pravila će biti navedeno u tekstu koji sledi)\<close>

thm conjI \<comment> \<open>@{text "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}\<close> 
thm disjI1 \<comment> \<open>@{text "?P \<Longrightarrow> ?P \<or> ?Q"}\<close>
thm disjI2 \<comment> \<open>@{text "?Q \<Longrightarrow> ?P \<or> ?Q"}\<close>
thm impI  \<comment> \<open>@{text "(?P \<Longrightarrow> ?Q) \<Longrightarrow> ?P \<longrightarrow> ?Q"}\<close>
thm iffI  \<comment> \<open>@{text "\<lbrakk>?P \<Longrightarrow> ?Q; ?Q \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P = ?Q"}\<close>
thm notI \<comment> \<open>@{text "(?P \<Longrightarrow> False) \<Longrightarrow> \<not> ?P"}\<close>

thm conjE \<comment> \<open>@{text "\<lbrakk>?P \<and> ?Q; \<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}\<close>
thm disjE  \<comment> \<open>@{text "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}\<close>
thm impE \<comment> \<open>@{text "\<lbrakk>?P \<longrightarrow> ?Q; ?P; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}\<close>
thm iffE \<comment> \<open>@{text "\<lbrakk>?P = ?Q; \<lbrakk>?P \<longrightarrow> ?Q; ?Q \<longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}\<close>
thm notE \<comment> \<open>@{text "\<lbrakk>\<not> ?P; ?P\<rbrakk> \<Longrightarrow> ?R"}\<close>

subsection\<open>Pravila uvođenja\<close>

text\<open>Pravila uvođenja nam govore kako se dokazuje tvrđenje čiji zaključak ima određen primarni
veznik. Primenjuju se metodom @{text "rule"}.\<close>

text\<open>\paragraph{Uvođenje konjunkcije:} Kao što je i očekivano, ako pojedinačno možemo da dokažemo
formule \<open>P\<close> i \<open>Q\<close>, onda možemo da dokažemo i formulu \<open>P \<and> Q\<close>. Ovo pravilo se primenjuje kada u
zaključku formule koju pokušavamo da dokažemo imamo konjunkciju kao primarni veznik.

U udžbenicima matematičke logike ovo pravilo se zapisuje na sledeći način:

$$\infer{P \wedge Q}{P & Q}$$

U sistemu Isabelle/HOL ovo pravilo se zove @{text "conjI"} i zapisuje se na sledeći način @{thm
[mode=Proof] conjI [no_vars]}. Šematske promenljive (promenljive obeležene upitnicima) koje se
javljaju u ovom pravilu mogu biti zamenjene proizvoljnim formulama. Pravilo se primenjuje sa desna
na levo. Zaključak tvrđenja koje se dokazuje se unifikuje sa \<open>?P \<and> ?Q\<close>, i to tvrđenje se zamenjuje
sa dva tvrđenja čiji su zaključci redom formule \<open>?P\<close> i \<open>?Q\<close> (instancirane u odnosu na unifikator
zaključka i formulu \<open>?P \<and> ?Q\<close>), dok se pretpostavke prepisuju iz polaznog tvrđenja.

Prikažimo efekat primene ovog pravila na narednom jednostavnom primeru. Formula nije tautologija, pa
dokaz nije moguće završiti i zato je na kraju dokaza upotrebljena ključna reč @{text "oops"}. Izlaz
koji se dobija kada se naredni dokaz pokrene u Isabelle-u biće prikazan u okviru komentara kao deo
samog dokaza.

Kako je glavni veznik u ovoj formuli konjunkcija i kako se ta konjunkcija nalazi u zaključku
tvrđenja koje se dokazuje primenjuje se pravilo @{text "conjI"}. Nakon primene naredbe @{text "apply
(rule conjI)"}, dokazivač identifikuje dva nova cilja \<open>A\<close> i \<open>B\<close> (odnosno u opštem slučaju prvi,
odnosno drugi konjunkt zadat konjunkcijom u zaključku). Nakon toga prvo se dokazuje prvi cilj, i tek
nakon dokazivanja prvog cilja se započinje sa dokazivanjem drugog cilja.\<close>

lemma "A \<and> B"
  apply (rule conjI)
\<comment> \<open>goal (2 subgoals):\<close>
\<comment> \<open>1. A\<close>
\<comment> \<open>2. B\<close>
  oops

text\<open>\paragraph{Uvođenje disjunkcije:} Da bismo dokazali tvrđenje oblika \<open>P \<or> Q\<close> dovoljno je da
dokažemo \<open>P\<close>, odnosno alternativno dovoljno je da dokažemo \<open>Q\<close>. Stoga se u udžbenicima matematičke
logike navode dva pravila uvođenja disjunkcije.

$$\infer{P \vee Q}{P} \qquad \infer{P \vee Q}{Q}$$

U sistemu Isabelle/HOL postoje dva pravila @{text "disjI1:"} @{thm [mode=Proof] disjI1 [no_vars]} i
@{text "disjI2:"} @{thm [mode=Proof] disjI2 [no_vars]}.

Prikažimo efekat primene ovih pravila na narednom primeru (formula nije teorema, pa dokaze nije
moguće završiti). Primena pravila @{text "disjI1"} identifikuje prvi disjunkt \<open>A\<close> kao jedini (novi)
cilj, dok primena pravila @{text "disjI2"} identifikuje drugi disjunkt \<open>B\<close> kao jedini cilj.\<close>

lemma "A \<or> B"
  apply (rule disjI1)
\<comment> \<open>goal (1 subgoal):\<close>
\<comment> \<open>1. A\<close>
  oops

lemma "A \<or> B"
  apply (rule disjI2)
\<comment> \<open>goal (1 subgoal):\<close>
\<comment> \<open>1. B\<close>
  oops

text\<open> Pravila uvođenja disjunkcije se mogu smatrati nebezbednim pravilima. Na primer, moguće je da
dokazujemo teoremu u kojoj iz nekih pretpostavki sledi zaključak \<open>P \<or> Q\<close>. Ako primenimo, na primer,
pravilo @{text "disjI1"}, tada je potrebno da dokažemo tvrđenje u kome iz istih tih pretpostavki
sledi zaključak \<open>P\<close>, međutim, to tvrđenje, za razliku od polaznog, ne mora uopšte više da bude tačno
tj. dokazivo. Pošto se pravila prirodne dedukcije primenjuju tokom rada automatskih metoda, i tada
treba biti obazriv kada se u zaključku nalazi disjunkcija, jer neki automatski metodi pokušavaju da
primene i nebezbedna pravila, poput ovih za eliminaciju disjunkcije, što u nekim slučajevima dovodi
do toga da automatski alat umesto da pojednostavi teoremu koju treba dokazati, svede teoremu na
tvrđenje koje se više ne može dokazati.\<close>


text\<open> \paragraph{Uvođenje implikacije:} Da bismo dokazali \<open>P \<longrightarrow> Q\<close> treba da pretpostavimo 
da \<open>P\<close> važi i pokušamo da dokažemo \<open>Q\<close>. Ako to uspemo, onda smo dokazali 
implikaciju.

U udžbenicima matematičke logike ovo pravilo se zapisuje na sledeći način:

$$\infer{P \rightarrow Q}{\infer*{Q}{[P]}}$$

U sistemu Isabelle/HOL pravilo se zove @{text "impI"} i zapisuje se na sledeći način @{thm
[mode=Proof] impI [no_vars]}. Oba simbola \<open>\<Longrightarrow>\<close> i \<open>\<longrightarrow>\<close> označavaju implikaciju ali 
je prvi simbol deo meta-logike sistema Isabelle i ovde se koristi za zapisivanje pravila izvođenja. 
Sa druge strane veznik \<open>\<longrightarrow>\<close> predstavlja samo jedan od veznika koji se koriste u logici 
višeg reda. Dok se veznik \<open>\<longrightarrow>\<close> koristi za zapisivanje formula logike višeg reda, veznik 
\<open>\<Longrightarrow>\<close> se koristi za odvajanje pretpostavki tvrđenja koje se dokazuje od njegovog zaključka.

Prikažimo efekat primene ovog pravila na narednom primeru (formula nije teorema, pa dokaz nije
moguće završiti). Nakon primene pravila @{text "impI"} vidimo da je formula \<open>A \<Longrightarrow> B\<close> identifikovana
kao novi cilj, odnosno Isabelle je logičku implikaciju zamenio meta-implikacijom i odvojio je
pretpostavke tvrđenja (\<open>A\<close>) od njegovog zaključka (\<open>B\<close>).\<close>

lemma "A \<longrightarrow> B"
  apply (rule impI)
\<comment> \<open>goal (1 subgoal):\<close>
\<comment> \<open>1. \<open>A \<Longrightarrow> B\<close>\<close>
  oops

text\<open> \paragraph{Uvođenje ekvivalencije:} Da bismo dokazali \<open>P \<longleftrightarrow> Q\<close> treba da dokažemo dva
cilja. Prvo da (uz ostale pretpostavke) pretpostavimo da važi \<open>P\<close> i da pokušamo da dokažemo \<open>Q\<close>, i nakon toga, da (uz ostale pretpostavke) pretpostavimo da važi \<open>Q\<close> i da pokušamo da dokažemo \<open>P\<close>. 
U udžbenicima matematičke logike, ovo pravilo se obično ne navodi eksplicitno, već se smatra da je
\<open>P \<longleftrightarrow> Q\<close> samo skraćeni zapis za \<open>P \<longrightarrow> Q \<and> Q \<longrightarrow> P\<close>.

U sistemu Isabelle/HOL pravilo se zove @{text "iffI"} i zapisuje se ovako @{thm [mode=Proof] iffI
[no_vars]}. Dakle, njime se dokaz ekvivalencije efektivno svodi na dokaz dve implikacije.

Prikažimo efekat primene ovog pravila na narednom primeru (formula nije teorema, pa dokaz nije
moguće završiti). Nakon primene pravila @{text "iffI"} logička ekvivalencija u zaključku teoreme se
svodi na dve implikacije \<open>A \<Longrightarrow> B\<close> i \<open>B \<Longrightarrow> A\<close> (primetimo da se primenom ovog pravila u formulama 
odmah dobija veznik meta-implikacije).\<close>

lemma "A \<longleftrightarrow> B"
  apply (rule iffI)
\<comment> \<open>goal (2 subgoals):\<close>
\<comment> \<open>1. \<open>A \<Longrightarrow> B\<close>\<close>
\<comment> \<open>2. \<open>B \<Longrightarrow> A\<close>\<close>
  oops

text\<open> \paragraph{Uvođenje negacije:} Ako iz pretpostavke \<open>P\<close> (i ostalih pretpostavki) možemo da
dokažemo \<open>False\<close>, odnosno ako možemo da izvedemo kontradikciju pod pretpostavkom \<open>P\<close>, onda možemo da
zaključimo da važi \<open>\<not> P\<close>.

U udžbenicima matematičke logike ovo pravilo se zapisuje na sledeći način:

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

U sistemu Isabelle/HOL pravilo se zove @{text "notI"} i zapisuje se na sledeći način 
@{thm [mode=Proof] notI [no_vars]}.

Primetimo da se ovim pravilom dokaz vrši svođenjem na kontradikciju, međutim, jako je važno
naglasiti da se u intuicionističkoj logici na taj način mogu dokazati samo negirana tvrđenja.
Dokazivanje pozitivnih tvrđenja svođenjem na kontradikciju zahteva primenu pravila klasične logike,
o čemu će više reči biti u narednim poglavljima. 

Prikažimo efekat primene ovog pravila na narednom primeru (formula nije teorema, pa dokaz nije
moguće završiti). Nakon primene pravila @{text "notI"} novi cilj postaje formula \<open>A \<Longrightarrow> False\<close>.\<close>

lemma "\<not> A"
  apply (rule notI)
\<comment> \<open>goal (1 subgoal):\<close>
\<comment> \<open>1. \<open>A \<Longrightarrow> False\<close>\<close>
  oops

text\<open>Ovde ćemo navesti nekoliko jednostavnih tvrđenja čiji se dokazi mogu izvesti primenom samo
pravila uvođenja:
\<close>

lemma "A \<longrightarrow> A \<or> B"
  apply (rule impI)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A \<or> B\<close>\<close>
  apply (rule disjI1) \<comment> \<open>\emph{Alternativa @{text "disjI2"} ne uspeva.}\<close>
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
  apply assumption
\<comment> \<open>\<open> No subgoals! \<close>\<close>
  done

lemma "B \<longrightarrow> A \<or> B"
  apply (rule impI)
\<comment> \<open>\<open> 1. B \<Longrightarrow> A \<or> B\<close>\<close>
  apply (rule disjI2)
\<comment> \<open>\<open> 1. B \<Longrightarrow> B\<close>\<close>
  apply assumption
  done

lemma "B \<longrightarrow> (A \<and> A) \<or> B"
  apply (rule impI)
\<comment> \<open>\<open> 1. B \<Longrightarrow> A \<and> A \<or> B\<close>\<close>
  apply (rule disjI2)
\<comment> \<open>\<open> 1. B \<Longrightarrow> B\<close>\<close>
  apply assumption
  done

lemma "A \<longrightarrow> (A \<and> A) \<or> B"
  apply (rule impI)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A \<and> A \<or> B\<close>\<close>
  apply (rule disjI1)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A \<and> A\<close>\<close>
  apply (rule conjI)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. A \<Longrightarrow> A\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
  apply assumption
  done

lemma "A \<longrightarrow> (A \<or> B) \<and> (B \<or> A)"
  apply (rule impI)
\<comment> \<open>\<open> 1. A \<Longrightarrow> (A \<or> B) \<and> (B \<or> A)\<close>\<close>
  apply (rule conjI)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A \<or> B\<close>\<close>
\<comment> \<open>\<open> 2. A \<Longrightarrow> B \<or> A\<close>\<close>
   apply (rule disjI1)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. A \<Longrightarrow> B \<or> A\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. A \<Longrightarrow> B \<or> A\<close>\<close>
  apply (rule disjI2)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
  apply assumption
  done

lemma "A \<longleftrightarrow> A"
  apply (rule iffI)
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
\<comment> \<open>\<open> 2. A \<Longrightarrow> A\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. A \<Longrightarrow> A\<close>\<close>
  apply assumption
  done

subsection\<open>Pravila eliminacije\<close>

text\<open>Pravila eliminacije nam daju nam mogućnost da pretpostavke tvrđenja koje se dokazuje u kojima
se javlja određeni veznik transformišemo na određeni način i tako iskoristimo "znanje" koje je
kodirano tim pretpostavkama. U sistemu Isabelle/HOL se primenjuju metodom @{text erule} koja
pokušava da navedeno pravilo primeni neku od trenutnih pretpostavki. Ako je primena pravila uspešna,
ta pretpostavka se briše i formiraju se novi ciljevi koje je potrebno dokazati (u zavisnosti od
pravila, u njima i pretpostavke i zaključak mogu biti izmenjeni).

Za razliku od zaključka tvrđenja, koji je uvek jedinstven, pretpostavki može biti više. Tako se može
desiti da se jedno pravilo eliminacije može da se primeni na više različitih pretpostavki. U ovakvim
situacijama Isabelle/HOL uvek bira prvu pretpostavku na koju se dato pravilo može primeniti. U
slučaju da je potrebno izabrati neku od narednih pretpostavki, koristi se ključna reč @{text
"back"}, kojom se pronalazi naredna pretpostavka na na koju je moguće primeniti navedeno pravilo
eliminacije i to pravilo se na nju primenjuje. Ako takva pretpostavka ne postoji, prijavljuje se
greška.\<close>

text\<open>\paragraph{Eliminacija konjunkcije:} Kada se eliminiše konjunkcija \<open>P \<and> Q\<close>, u
prirodnoj dedukciji kakva se opisuje u udžbenicima matematičke logike postoje dva pravila u
zavisnosti od toga da li se izvodi prvi ili drugi konjunkt:

$$\infer{P}{P \wedge Q} \qquad \infer{Q}{P \wedge Q}$$

Isabelle/HOL pravilo za eliminaciju konjunkcije malo odstupa od ustaljenih pravila datih u klasičnim
udžbenicima matematičke logike, u kojima postoji posebno pravilo kojim se iz konjunkcije dobija \<open>P\<close>
i posebno pravilo kojim se iz konjunkcije dobija \<open>Q\<close>, i odmah iz konjunkcije daje \<open>P\<close> i \<open>Q\<close>. Pravilo
se zove @{text "conjE"} i zapisuje se na sledeći način @{thm [mode=Proof] conjE [no_vars]}.
Tumačenje ovog pravila je sledeće. Pretpostavimo da je potrebno dokazati neko tvrđenje \<open>?R\<close>, a da se
među pretpostavkama nalazi formula oblika \<open>?P \<and> ?Q\<close>. Tada je dovoljno dokazati tvrđenje \<open>?R\<close> iz
nezavisnih pretpostavki \<open>?P\<close> i \<open>?Q\<close>. Drugim rečima, ako možemo da dokažemo \<open>?P \<and> ?Q\<close> i ako možemo 
da dokažemo da pod pretpostavkama \<open>?P\<close> i \<open>?Q\<close> važi \<open>?R\<close> (tj. \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?R\<close>), tada možemo 
smatrati da smo uspešno dokazali \<open>?R\<close>.

\textbf{Napomena:} Primetimo da su leme u ovom poglavlju formulisane sa meta-implikacijom \<open>\<Longrightarrow>\<close>, naspram do sada korišćene logičke implikacije \<open>\<longrightarrow>\<close>. Razlog za to je što korišćenje meta-implikacije omogućava korisniku da u dokazu ne koristi ni jedno pravilo uvođenja.

Prikažimo efekat primene ovog pravila na narednom primeru. Pravilo eliminacije konjunkcije eliminiše konjunkciju iz pretpostavki i umesto nje dodaje njene pojedinačne konjunkte kojima korisnik dalje može pristupiti po potrebi.\<close>

lemma "A \<and> B \<Longrightarrow> A"
  apply (erule conjE)
\<comment> \<open>\<open> 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>\<close>
  apply assumption
\<comment> \<open>\<open> No subgoals!\<close>\<close>
  done

text\<open> \paragraph{Eliminacija disjunkcije:} Eliminacija disjunkcije odgovara dokazu po slučajevima u
klasičnim matematičkim udžbenicima. 

U udžbenicima matematičke logike, ovo pravilo se zapisuje na sledeći način:

$$\infer{R}{P \vee Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}$$

Dakle, ako nezavisno, iz svakog disjunkta možemo da izvedemo neki zaključak, onda možemo da
eliminišemo disjunkciju i da je zamenimo tim zaključkom. Primetimo da se objektna disjunkcija na
neki način menja konjunkcijom na meta-nivou (potrebno je da dokaz izvršimo nezavisno i za jedan i za
drugi disjunkt).

U sistemu Isabelle/HOL pravilo se zove @{text "disjE"} i zapisuje se na sledeći način @{thm
[mode=Proof] disjE [no_vars]}. Primena ovog pravila rezultira grananjem (jedno tvrđenje se zamenjuje
sa dva) pri čemu prva grana odgovara prvoj pretpostavci a druga grana drugoj pretpostavci. Prvo
pretpostavimo \<open>P\<close>, pa iz toga dokažemo \<open>R\<close>, pa onda nezavisno pretpostavimo \<open>Q\<close>, pa iz toga dokažemo
\<open>R\<close> i onda smatramo da smo dokazali \<open>R\<close>. U toku ovog procesa \<open>R\<close> se dokazuje dva puta, iz različitih
skupova pretpostavki.

\textbf{Napomena:} zadebljane zagrade koje se obično prikazuju u Output prozoru se mogu koristiti i prilikom zapisivanja samog tvrđenja koje se dokazuje.

Prikažimo efekat primene ovog pravila na narednom primeru (formula nije teorema i ne može se dokazati). Eliminacija disjunkcije iz pretpostavke odgovara grananju po slučajevima i generiše dva podcilja: u prvom je jedina pretpostavka tvrđenje \<open>A\<close>, a u drugom tvrđenje \<open>B\<close>.\<close>

lemma "\<lbrakk> A \<or> B \<rbrakk> \<Longrightarrow> C"
  apply (erule disjE)
\<comment> \<open>\<open> 1. A \<Longrightarrow> C\<close>\<close>
\<comment> \<open>\<open> 2. B \<Longrightarrow> C\<close>\<close>
  oops

text\<open> \paragraph{Eliminacija implikacije:} Ako znamo da važi implikacija \<open>P \<longrightarrow> Q\<close>, koristi se
pravilo \emph{modus ponens} za eliminaciju implikacije. U udžbenicima matematičke logike ovo pravilo
se zapisuje na sledeći način:

$$\infer{R}{P & P \rightarrow Q}$$

Da bi se eliminisala implikacija \<open>P \<longrightarrow> Q\<close> neophodno je da se nezavisno (iz ostalih pretpostavki)
dokaže \<open>P\<close>, i da se dokaže da iz ostalih pretpostavki i iz \<open>Q\<close> važi \<open>R\<close>.

U sistemu Isabelle/HOL ovo pravilo se zove @{text "impE"} i zapisuje se na sledeći način @{thm
[mode=Proof] impE [no_vars]}.

Ovo pravilo je još jedno od nebezbednih pravila. Može se desiti da je implikacija (na koju se
primenjuje pravilo) takva da se njena pretpostavka \<open>P\<close> ne može dokazati. Jedan način da se ovo
dogodi je da se eliminacija implikacije greškom primeni na pogrešnu implikaciju u pretpostavkama. U
toj situaciji koristićemo ključnu reč @{text "back"} da bismo naveli dokazivač da pravilo primeni na
narednu drugu pretpostavku.

Prikažimo efekat primene ovog pravila na narednom primeru (tvrđenje se ne može dokazati). Eliminacija implikacije iz pretpostavke generiše dva odvojena cilja. Kako u narednom primeru nema dodatnih pretpostavki, prvi cilj postaje leva strana implikacije (samo formula \<open>A\<close>), a drugi cilj u pretpostavkama zadržava samo desnu stranu implikacije (formula \<open>B\<close>) i u zaključku ostaje originalni cilj.\<close>

lemma "\<lbrakk> A \<longrightarrow> B \<rbrakk> \<Longrightarrow> C"
  apply (erule impE)
\<comment> \<open>\<open> 1. A\<close>\<close>
\<comment> \<open>\<open> 2. B \<Longrightarrow> C\<close>\<close>
  oops

text\<open> \paragraph{Eliminacija ekvivalencije:} Ako znamo da važi implikacija \<open>P \<longleftrightarrow> Q\<close>, koristi se
pravilo za eliminaciju ekvivalencije koje se u sistemu Isabelle/HOL zove @{text "iffE"} i zapisuje
se na sledeći način @{thm [mode=Proof] iffE [no_vars]}. Primena ovog pravila odgovara tumačenju da
je veznik ekvivalencije samo skraćenica za dve implikacije.

Prikažimo efekat primene ovog pravila na narednom primeru (tvrđenje se ne može dokazati). Eliminacija ekvivalencije iz pretpostavke generiše dve nove pretpostavke, implikacija u jednom smeru i implikacija u obrnutom smeru.\<close>

lemma "\<lbrakk> A \<longleftrightarrow> B \<rbrakk> \<Longrightarrow> C"
  apply (erule iffE)
\<comment> \<open>\<open> 1. \<lbrakk>A \<longrightarrow> B; B \<longrightarrow> A\<rbrakk> \<Longrightarrow> C\<close>\<close>
  oops

text\<open> \paragraph{Eliminacija negacije:} Iz kontradiktornih pretpostavki mozemo da zaključimo bilo
šta. U udžbenicima matematičke logike ovo pravilo se primenjuje na sledeći način:

$$\infer{False}{P & \neg P}$$

U sistemu Isabelle/HOL ovo pravilo se zove @{text "notE"} i zapisuje se na sledeći način: @{thm
[mode=Proof] notE [no_vars]}. Primena ovog pravila teče tako što se u pretpostavkama pronađe neka
negirana formula \<open>\<not> P\<close> i onda se iz ostalih pretpostavki pokušava dokazati formula \<open>P\<close>. Primetimo 
da se zaključak polaznog tvrđenja potpuno ignoriše i nakon primene pravila @{text "notE"} on nestaje 
iz transformisanog tvrđenja.

I ovo pravilo je nebezbedno i može se desiti da primena ovog pravila dovede do cilja koji ne možemo
da dokažemo. Do toga može doći i kada u pretpostavkama tvrđenja koje se dokazuje imamo više
negacija, i tada je potrebno voditi računa koju negaciju treba eliminisati. Da bismo precizno
izabrali odgovarajuću negaciju, možemo koristiti naredbu @{text "back"}.

Prikažimo efekat primene ovog pravila na narednom primeru (tvrđenje se ne može dokazati). Eliminacija negacije iz pretpostavke generiše novi cilj koji kao zaključak ima pozitivan oblik formule koja stoji iza veznika \<open>\<not>\<close>. Kako u ovom slučaju nema ostalih pretpostavki, tvrđenje se sastoji samo od tog pozitivnog oblika.\<close>

lemma "\<not> A \<Longrightarrow> B"
  apply (erule notE)
\<comment> \<open>\<open> 1. A\<close>\<close>
  oops

text\<open> \paragraph{Bezbedna i nebezbedna pravila:} Može se primetiti da primena određenih pravila može
narušiti dokazivost tvrđenja. Usled toga razlikujemo \emph{bezbedna} i \emph{nebezbedna} pravila.
\emph{Bezbedna pravila} su @{text "conjI"}, @{text "impI"}, @{text "iffI"}, @{text "notI"}, @{text
"conjE"}, @{text "disjE"} i @{text "iffE"}. \emph{Nebezbedna pravila} su @{text "disjI1"}, @{text
"disjI2"}, @{text "impE"} i @{text "notE"}. U dokazima se preporučuje da se prvo iscrpno primene sva
bezbedna pravila, pa tek onda nebezbedna pravila. Prilikom primene nebezbednih pravila eliminacije
treba voditi računa o tome da li su zaista primenjena na željene pretpostavke.\<close>

section\<open>Primeri dokaza u prirodnoj dedukciji\<close>

text\<open>U nastavku ćemo prikazati primere dokaza prirodnom dedukcijom u sistemu Isabelle/HOL. Svi oni
su dati u obliku niza primena pravila navedenih komandom @{text "apply"}. Takvi dokazi se nazivaju
nestrukturirani dokazi i oni nisu jednostavno čitljivi. Da bismo čitaocu olakšali praćenje navešćemo
dodatna objašnjenja u okviru samih dokaza u vidu komentara (tekst koji se pojavljuje iza dugačke
crtice \<open>(\<comment>)\<close>). Indentacija (uvlačenje) komandi @{text "apply"} u ovim dokazima se javlja kada
primena pravila poveća broj tvrđenja (ciljeva) koje treba pokazati i tada se početak reda pomera za
jedno mesto udesno (jedan razmak) u odnosnu na prethodni red. Kada se podcilj uspešno dokaže,
indentacija se smanjuje za jedno mesto.

Da bi čitalac mogao da prati ove dokaze i u Isabelle/HOL i van njega, u prvih nekoliko primera biće
prikazan prvo kompletan dokaz, pa onda isti taj dokaz detaljno iskomentarisan i dopunjen
odgovarajućim izlazom koji se dobija u Isabelle/HOL. Komentari će biti navedeni za svaku naredbu u
prvih nekoliko primera, a u kasnijim primerima komentarisaćemo samo ključne korake.\<close>

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

text\<open>Dokaz teoreme:\<close>

lemma "A \<and> B \<longrightarrow> B \<and> A"
  apply (rule impI)
  apply (erule conjE) 
  apply (rule conjI)
   apply assumption
  apply assumption
  done

text\<open>Detaljno objašnjen dokaz teoreme: \<close>
(* \footnote{Dodati eventualno par slika ekrana koje prikazuju
promenu ciljeva nakon izvrsavanja pojedinacnih pravila - samo za prvi primer.} *)

lemma "A \<and> B \<longrightarrow> B \<and> A"
\<comment> \<open>Cilj je identifikovan sa: \<open>A \<and> B \<longrightarrow> B \<and> A\<close>, što znači da dokazujemo ovu iskaznu formulu iz
 praznog skupa pretpostavki\<close>
\<comment> \<open>Logičku implikaciju \<open>\<longrightarrow>\<close> u zaključku možemo transformisati je u meta-implikaciju \<open>\<Longrightarrow>\<close>,
korišćenjem pravila impI\<close>
  apply (rule impI)
\<comment> \<open>Sada je cilj postao: \<open>A \<and> B \<Longrightarrow> B \<and> A\<close>, što znači da iz pretpostavke \<open>A \<and> B\<close> dokazujemo zaključak
 \<open>B \<and> A\<close>\<close>
\<comment> \<open>Prvo primenjujemo pravilo za eliminaciju konjunkcije u pretpostavkama, da bismo mogli da koristimo
 pojedinačno pretpostavke \<open>A\<close> i \<open>B\<close>.\<close>
  apply (erule conjE) 
\<comment> \<open>Sada je cilj postao: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B \<and> A\<close>, što znači da iz pretpostavki \<open>A\<close> i \<open>B\<close> dokazujemo
 zaključak \<open>B \<and> A\<close>\<close>
\<comment> \<open>Sada želimo da uvedemo konjunkciju u zaključku i primenjujemo pravilo \<open>conjI\<close> za uvođenje konjunkcije
  (\<open>B \<and> A\<close> dokazujemo tako što nezavisno dokažemo \<open>B\<close> i \<open>A\<close>\<close>
  apply (rule conjI)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>I dokazujemo prvi cilj: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B\<close>. Pošto je sada u pretpostavkama već prisutan trenutni
 zaključak, pozivamo metodu \<open>assumption\<close>\<close>
   apply assumption
\<comment> \<open>Sada nestaje prvi cilj i ostaje samo drugi cilj: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>, za koji opet možemo primeniti
 metodu \<open>assumption\<close> zato što je u pretpostavkama prisutan tekući cilj\<close>
  apply assumption
\<comment> \<open>Nakon ovoga dobijamo izlaz: \<open>No subgoals!\<close> i možemo završiti tekući dokaz naredbom \<open>done\<close>.\<close>
  done
\<comment> \<open>Nakon ove naredbe, teorema je dokazana i evidentirana u Isabelle/HOL.\<close>

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

text\<open>Dokaz teoreme:\<close>

lemma "A \<or> B \<longrightarrow> B \<or> A"
  apply (rule impI)
  apply (erule disjE)
   apply (rule disjI2)
   apply assumption
  apply (rule disjI1)
  apply assumption
  done

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

lemma "A \<or> B \<longrightarrow> B \<or> A"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>A \<or> B \<longrightarrow> B \<or> A\<close>}\<close>
\<comment> \<open>\emph{Logičku implikaciju transformišemo u meta-implikaciju pravilom \<open>impI\<close>}\<close>
  apply (rule impI)
\<comment> \<open>\emph{Cilj je sada: \<open>A \<or> B \<Longrightarrow> B \<or> A\<close>.}\<close>
\<comment> \<open>\emph{U pretpostavci imamo disjunkciju pa je eliminišemo pravilom \<open>disjE\<close>.}\<close>
  apply (erule disjE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. A \<Longrightarrow> B \<or> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. B \<Longrightarrow> B \<or> A\<close>.}\<close>
\<comment> \<open>\emph{Prvo rešavamo prvi cilj: \<open>A \<Longrightarrow> B \<or> A\<close>. Primećujemo da u zaključku prvog cilja imamo 
pretpostavku \<open>A\<close> kao drugi disjunkt pa primenjujemo pravilo \<open>disjI2\<close> da bismo upravo taj disjunkt 
izdvojili.}\<close>
   apply (rule disjI2)
\<comment> \<open>\emph{Tekući cilj sada postaje: \<open>A \<Longrightarrow> A\<close> (dok drugi cilj ostaje nepromenjen i čeka svoj red).}\<close>
\<comment> \<open>\emph{Kada se zaključak nalazi među pretpostavkama primenjujemo naredbu \<open>assumption\<close>, čime se
završava dokaz prvog podcilja.}\<close>
   apply assumption
\<comment> \<open>\emph{Sada rešavamo drugi podcilj: \<open>B \<Longrightarrow> B \<or> A\<close>. Primećujemo da u zaključku imamo pretpostavku \<open>B\<close>
kao prvi disjunkt pa primenjujemo pravilo \<open>disjI1\<close> da bismo upravo taj disjunkt izdvojili.}\<close>
  apply (rule disjI1)
\<comment> \<open>\emph{Tekući cilj sada postaje: \<open>B \<Longrightarrow> B\<close>.}\<close>
\<comment> \<open>\emph{Kada se zaključak nalazi među pretpostavkama primenjujemo naredbu \<open>assumption\<close>, čime se
završava dokaz drugog podcilja.}\<close>
  apply assumption
\<comment> \<open>\emph{Dokazali smo oba cilja i dobijamo izlaz \<open>No subgoals!\<close> i možemo završiti tekući dokaz
naredbom \<open>done\<close>.}\<close>
  done
\<comment> \<open>\emph{Nakon ove naredbe, teorema je dokazana i evidentirana u Isabelle/HOL.}\<close>

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

text\<open>Dokaz teoreme:\<close>

lemma "A \<and> B \<longrightarrow> A \<or> B"
  apply (rule impI)
  apply (erule conjE)
  apply (rule disjI1)
  apply assumption
  done

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

lemma "A \<and> B \<longrightarrow> A \<or> B"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>A \<and> B \<longrightarrow> A \<or> B\<close>}\<close>
\<comment> \<open>\emph{Logičku implikaciju transformišemo u meta-implikaciju pravilom 
\<open>impI\<close>.}\<close>
\<comment> \<open>\emph{Cilj je sada: \<open>A \<and> B \<Longrightarrow> A \<or> B\<close>}.\<close>
  apply (rule impI)
\<comment> \<open>\emph{U pretpostavci se nalazi konjunkcija, eliminišemo je i dobijamo dve nezavisne 
činjenice pravilom \<open>conjE\<close>}.\<close>
  apply (erule conjE) 
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<or> B\<close>.}\<close>
\<comment> \<open>\emph{Sada se u zaključku nalazi takva disjunkcija da je svejedno koji disjunkt 
ćemo ostaviti, pa na primer izdvajamo prvi, pravilom \<open>disjI1\<close>.}\<close>
  apply (rule disjI1)
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{Cilj se nalazi u pretpostavkama pa primenjujemo naredbu \<open>assumption\<close>}.\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza.}\<close>
  done
\<comment> \<open>\emph{Teorema se evidentira u Isabelle/HOL sistemu.}\<close>

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

text\<open>Dokaz teoreme:\<close>

lemma "(A \<and> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
  apply (rule impI)
  apply (rule impI) 
  apply (rule impI) 
  apply (erule impE) 
   apply (rule conjI) 
    apply assumption
   apply assumption
  apply assumption
  done

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

lemma "(A \<and> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>(A \<and> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))\<close>}\<close>
\<comment> \<open>\emph{Pošto sada imamo u zaključku nekoliko vezanih logičkih implikacija, 
transformišemo ih u meta-implikacije uzastopnom primenom pravila \<open>impI\<close>. Svaka 
primena pravila \<open>impI\<close> prebacuje pretpostavku sa desne strane \<open>\<Longrightarrow>\<close> simbola na 
levu stranu.}\<close>
  apply (rule impI)
\<comment> \<open>\emph{Cilj je sada: \<open>A \<and> B \<longrightarrow> C \<Longrightarrow> A \<longrightarrow> B \<longrightarrow> C\<close>}.\<close>
  apply (rule impI) 
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A \<and> B \<longrightarrow> C; A\<rbrakk> \<Longrightarrow> B \<longrightarrow> C\<close>}.\<close>
  apply (rule impI) 
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A \<and> B \<longrightarrow> C; A; B\<rbrakk> \<Longrightarrow> C\<close>}.\<close>
\<comment> \<open>\emph{Sada je potrebno eliminisati implikaciju iz pretpostavki.}\<close>
\<comment>\<open>\emph{Da bi se eliminisala implikacija, treba prvo pokazati da možemo da 
dokažemo da važi njena pretpostavka (u ovom slučaju \<open>A \<and> B\<close>) na osnovu
preostalih pretpostavki; pa onda dokazati da iz preostalih pretpostavki (igrom slučaja 
isto \<open>A \<and> B\<close>) i njenog cilja (\<open>C\<close>) važi globalni cilj (igrom slučaja isto \<open>C\<close>). 
Tako da nakon primene pravila \<open>impE\<close> dobijamo dva podcilja.}\<close>
  apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{Prvo dokazujemo prvi cilj: \<open> \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B\<close> i primenjujemo pravilo 
uvođenja konjunkcije \<open>conjI\<close>.}\<close>
   apply (rule conjI)
\<comment> \<open>\emph{Sada se prvi cilj zamenjuje sa dva nova cilja:}\<close>
\<comment> \<open>\emph{\<open>1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B\<close>.}\<close>
\<comment> \<open>\emph{Pošto se oba cilja već nalaze u pretpostavkama, koristimo dva puta 
naredbu \<open>assumption\<close>.}\<close>
    apply assumption
   apply assumption
\<comment> \<open>\emph{Ovim je rešen prvi cilj, ostaje drugi cilj: \<open> \<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> C\<close> koji 
takođe rešavamo naredbom \<open>assumption\<close>.}\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza.}\<close>
  done

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

text\<open>Prikazaćemo dva načina na koji možemo da dokažemo ovu lemu. Naime, u situaciji kada imamo 
više pretpostavki, korisnik može da bira koju pretpostavku će prvo eliminisati (odnosno
koji veznik će prvo eliminisati). Naredna dva dokaza se razlikuju počevši od trećeg koraka. 
Dokazi su slični ali drugi dokaz je za nijansu kraći (zato što se u njemu samo jednom radi eliminacija konjunkcije).

Prvi način:

Dokaz teoreme:\<close>

lemma "(A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<and> B \<longrightarrow> C)"
  apply (rule impI) 
  apply (rule impI) 
  apply (erule impE) 
   apply (erule conjE) 
   apply assumption
  apply (erule impE)
   apply (erule conjE)
   apply assumption
  apply assumption
  done

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

Isabelle/HOL ne ispisuje zagrade koje se javljaju u izrazima ako taj raspored zagrada odgovara
prioritetu operatora. Tako da u narednom detaljno raspisanom dokazu neće postojati zagrade u
zaključku tvrđenja kao deo Isabelle/HOL interpretacije.\<close>

lemma "(A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<and> B \<longrightarrow> C)"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> A \<and> B \<longrightarrow> C\<close>. Sada 
treba dva puta implikaciju da transformišemo u meta-implikaciju primenom pravila 
\<open>impI\<close>.}\<close>
  apply (rule impI) 
\<comment> \<open>\emph{Cilj je sada: \<open>A \<longrightarrow> B \<longrightarrow> C \<Longrightarrow> A \<and> B \<longrightarrow> C\<close>.}\<close>
  apply (rule impI)
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A \<longrightarrow> B \<longrightarrow> C; A \<and> B\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{U prvoj verziji dokaza ove leme biramo da se prvo oslobodimo 
implikacije u prvoj pretpostavci pravilom \<open>impE\<close>. Prvo treba da pokažemo da njena 
pretpostavka (\<open>A\<close>) može da se dokaže iz preostalih pretpostavki (\<open>A \<and> B\<close>), pa nakon 
toga treba da pokažemo da iz njenog zaključka (\<open>B \<longrightarrow> C\<close>) i preostalih pretpostavki 
može da se izvede finalni cilj.}\<close>
\<comment> \<open>Odnosno: leva strana implikacije postaje zaključak prvog podcilja, desna 
strana implikacije postaje pretpostavka drugog podcilja. \<close>
  apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. A \<and> B \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A \<and> B; B \<longrightarrow> C\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{Sada prvo dokazujemo prvi podcilj: \<open>A \<and> B \<Longrightarrow> A\<close> i eliminišemo 
konjunkciju i izdvajamo konjunkte da bismo mogli da ih koristimo nezavisno.}\<close>
   apply (erule conjE) 
\<comment> \<open>\emph{Kako se cilj sada nalazi u pretpostavkama, primenjujemo pravilo 
\<open>assumption\<close>.}\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi podcilj: \<open>\<lbrakk>A \<and> B; B \<longrightarrow> C\<rbrakk> \<Longrightarrow> C\<close>. Prvo ćemo 
eliminisati implikaciju iz druge pretpostavke, što znači da treba iz preostale 
pretpostavke (\<open>A \<and> B\<close>) da dokažemo pretpostavku implikacije (\<open>B\<close>), pa zatim da iz 
preostale pretpostavke i zaključka implikacije (\<open>C\<close>) dokažemo konačni cilj (\<open>C\<close>).}\<close>
  apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. A \<and> B \<Longrightarrow> B\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A \<and> B; C\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{Prvo dokazujemo prvi cilj: \<open>A \<and> B \<Longrightarrow> B\<close> i primenjujemo eliminaciju 
konjunkcije \<open>conjE\<close>.}\<close>
   apply (erule conjE)
\<comment> \<open>\emph{Sada se tekući zaključak nalazi u pretpostavkama i primenjujemo pravilo 
\<open>assumption\<close>.}\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi cilj: \<open>\<lbrakk>A \<and> B; C\<rbrakk> \<Longrightarrow> C\<close> i vidimo da se 
zaključak već nalazi u pretpostavkama i ponovo primenjujemo \<open>assumption\<close>.}\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza.}\<close>
  done

text\<open>Drugi način: \<close>

lemma "(A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<and> B \<longrightarrow> C)"
  apply (rule impI)
  apply (rule impI)
  apply (erule conjE) \<comment> \<open> prvo možemo da eliminišemo konjunkciju \<close>
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply assumption
  done

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

lemma "(A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<and> B \<longrightarrow> C)"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> A \<and> B \<longrightarrow> C\<close>. Sada 
treba dva puta implikaciju da transformišemo u meta-implikaciju primenom pravila 
\<open>impI\<close>.}\<close>
  apply (rule impI) 
\<comment> \<open>\emph{Cilj je sada: \<open>A \<longrightarrow> B \<longrightarrow> C \<Longrightarrow> A \<and> B \<longrightarrow> C\<close>.}\<close>
  apply (rule impI)
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A \<longrightarrow> B \<longrightarrow> C; A \<and> B\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{U drugoj verziji dokaza ove leme biramo da se prvo oslobodimo 
konjunkcije u drugoj pretpostavci}.\<close>
  apply (erule conjE) 
\<comment> \<open>\emph{Sada se oslobađamo implikacije u prvoj pretpostavci pravilom \<open>impE\<close>. Prvo 
treba da pokažemo da njena pretpostavka (\<open>A\<close>) može da se dokaže iz preostalih 
pretpostavki (\<open>\<lbrakk>A; B\<rbrakk>\<close>), pa nakon toga treba da pokažemo da iz njenog zaključka 
(\<open>B \<longrightarrow> C\<close>) i preostalih pretpostavki može da se izvede finalni cilj.}\<close>
  apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; B; B \<longrightarrow> C\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{Sada prvo dokazujemo prvi podcilj: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A\<close>. Kako se cilj sada 
nalazi u pretpostavkama, primenjujemo pravilo \<open>assumption\<close>.}\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi cilj: \<open>\<lbrakk>A; B; B \<longrightarrow> C\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{Elimišemo implikaciju iz treće pretpostavke pravilom \<open>impE\<close>. Prvo 
pokazujemo da njena pretpostavka (\<open>B\<close>) može da se dokaže iz preostalih pretpostavki 
(\<open>\<lbrakk>A; B\<rbrakk>\<close>), pa nakon toga da iz preostalih pretpostavki i njenog zaključka (\<open>C\<close>) može 
da se dokaže konačni cilj (\<open>C\<close>).}\<close>
  apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> C\<close>.}\<close>
\<comment> \<open>\emph{Sada prvo dokazujemo prvi podcilj: \<open>\<lbrakk>A; B\<rbrakk> \<Longrightarrow> B\<close>. Kako se cilj sada 
nalazi u pretpostavkama, primenjujemo pravilo \<open>assumption\<close>.}\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi cilj: \<open>\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> C\<close> i vidimo da se zaključak 
već nalazi u pretpostavkama i ponovo primenjujemo \<open>assumption\<close>.}\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza.}\<close>
  done

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

lemma shows "\<not> (A \<or> B) \<longrightarrow> \<not> A \<and> \<not> B"
  apply (rule impI)
  apply (rule conjI)
   apply (rule notI) 
   apply (erule notE)
   apply (rule disjI1)
  apply assumption
  apply (rule notI)
  apply (erule notE)
  apply (rule disjI2)
  apply assumption
  done

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

lemma shows "\<not> (A \<or> B) \<longrightarrow> \<not> A \<and> \<not> B"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>\<not> (A \<or> B) \<longrightarrow> \<not> A \<and> \<not> B\<close>. Prvo implikaciju 
transformišemo u meta-implikaciju primenom pravila \<open>impI\<close>.}\<close>
  apply (rule impI)
\<comment> \<open>\emph{Cilj je sada: \<open>\<not> (A \<or> B) \<Longrightarrow> \<not> A \<and> \<not> B\<close>. Sada primenjujemo pravilo 
uvođenja konjunkcije \<open>conjI\<close>.}\<close>
  apply (rule conjI)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<not> (A \<or> B) \<Longrightarrow> \<not> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<not> (A \<or> B) \<Longrightarrow> \<not> B\<close>.}\<close>
\<comment> \<open>\emph{I prvo dokazujemo prvi cilj: \<open>\<not> (A \<or> B) \<Longrightarrow> \<not> A\<close>. Sada u zaključku 
imamo negaciju pa primenjujemo pravilo \<open>notI\<close> koje izgleda ovako: 
@{thm [mode=Proof] notI [no_vars]}, znači zaključak (bez negacije) prebacujemo u 
pretpostavke i pokušavamo da izvedemo kontradikciju (odnosno \<open>False\<close>).}\<close>
   apply (rule notI) 
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>\<not> (A \<or> B); A\<rbrakk> \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{Sada iz prve pretpostavke treba da eliminišemo negaciju i koristimo pravilo 
\<open>notE\<close> koje izgleda ovako: @{thm [mode=Proof] notE [no_vars]}}.\<close>
\<comment>\<open> Da bismo njega mogli da primenimo, potrebno je da dokažemo pozitivan oblik 
te pretpostavke iz preostalih pretpostavke \<close>
   apply (erule notE)
\<comment> \<open>\emph{Dobijamo sledeći cilj: \<open>A \<Longrightarrow> A \<or> B\<close>. Kako je prvi disjunkt već 
prisutan u pretpostavkama, primenjujemo pravilo \<open>disjI1\<close> koje će izdvojiti upravo 
prvi disjunkt.}\<close>
   apply (rule disjI1)
\<comment> \<open>\emph{Sada se zaključak nalazi u pretpostavkama i primenjujemo pravilo 
\<open>assumption\<close>}.\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi cilj: \<open>\<not> (A \<or> B) \<Longrightarrow> \<not> B\<close>. U zaključku ponovo 
imamo negaciju pa primenjujemo pravilo \<open>notI\<close>: 
@{thm [mode=Proof] notI [no_vars]}, i zaključak (bez negacije) prebacujemo u 
pretpostavke i pokušavamo da izvedemo kontradikciju (odnosno \<open>False\<close>) na osnovu njega 
i ostalih pretpostavki.}\<close>
  apply (rule notI)
\<comment> \<open>\emph{Sada dobijamo cilj: \<open>\<lbrakk>\<not> (A \<or> B); B\<rbrakk> \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{Sada iz prve pretpostavke treba da eliminišemo negaciju i koristimo pravilo 
\<open>notE\<close>: @{thm [mode=Proof] notE [no_vars]}. I pokušavamo da iz ostalih pretpostavki 
dobijemo pozitivan oblik.}\<close>
  apply (erule notE)
\<comment> \<open>Sada dobijamo cilj: \<open>B \<Longrightarrow> A \<or> B\<close>. Kako je drugi disjunkt već prisutan u 
pretpostavkama, primenjujemo pravilo \<open>disjI2\<close> koje će izdvojiti upravo prvi 
disjunkt.\<close>
   apply (rule disjI2)
\<comment> \<open>\emph{Sada se zaključak nalazi u pretpostavkama i primenjujemo pravilo 
\<open>assumption\<close>}.\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza}.\<close>
  done

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

text\<open>I ovu teoremu ćemo dokazati na dva načina. U prvom dokazu ćemo prikazati dokaz dobijen direktno
primenom pravila, a u drugom dokazu ćemo prikazati kako možemo da koristimo naredbu @{text "back"}
da usmerimo primenu pravila na konkretnu pretpostavku.

Prvi način: \<close>

text\<open>Dokaz teoreme:\<close>

lemma shows "\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> B)"
  apply (rule impI)
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE)
   apply assumption 
  apply (erule notE)
  apply (erule notE)
  apply assumption
  done

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

lemma shows "\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> B)"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> B)\<close>. Prvo implikaciju 
transformišemo u meta-implikaciju primenom pravila \<open>impI\<close>.}\<close>
  apply (rule impI)
\<comment> \<open>\emph{Cilj je sada: \<open>\<not> A \<and> \<not> B \<Longrightarrow> \<not> (A \<or> B)\<close>}.\<close>
\<comment> \<open>\emph{U zaključku imamo negaciju pa primenjujemo pravilo \<open>notI\<close> i zaključak 
(bez negacije) prebacujemo u pretpostavke i pokušavamo da izvedemo kontradikciju 
(odnosno \<open>False\<close>).}\<close>
  apply (rule notI)
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>\<not> A \<and> \<not> B; A \<or> B\<rbrakk> \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{Sada prvo eliminišemo konjunkciju sa leve strane, da bi mogli da priđemo 
pojedinačnim konjunktima \<open>\<not> A\<close> i \<open>\<not> B\<close>}.\<close>
  apply (erule conjE)
\<comment> \<open>\emph{Cilj je sada: \<open>\<lbrakk>A \<or> B; \<not> A; \<not> B\<rbrakk> \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{Sada eleminišemo disjunkciju u pretpostavkama pravilom \<open>disjE\<close>}.\<close>
  apply (erule disjE)
\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<lbrakk>\<not> A; \<not> B; A\<rbrakk> \<Longrightarrow> False\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>\<not> A; \<not> B; B\<rbrakk> \<Longrightarrow> False\<close>.}\<close>
\<comment> \<open>\emph{Sada prvo dokazujemo prvi cilj: \<open>\<lbrakk>\<not> A; \<not> B; A\<rbrakk> \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{Pokušavamo da eliminišemo negaciju iz prve pretpostavke pravilom \<open>notE\<close>}.\<close>
   apply (erule notE)
\<comment> \<open>\emph{Sada je prvi cilj: \<open>\<lbrakk>\<not> B; A\<rbrakk> \<Longrightarrow> A\<close>}.\<close>
\<comment> \<open>\emph{Primetimo da je pravilo \<open>notE\<close> primenjeno na pretpostavku \<open>\<not> A\<close> i da je 
pretpostavka \<open>\<not> B\<close> ostala za kasnije}.\<close>
\<comment> \<open>\emph{Kako je sada tekući zaključak već u pretpostavkama, primenjujemo pravilo 
\<open>assumption\<close>}.\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi cilj: \<open>\<lbrakk>\<not> A; \<not> B; B\<rbrakk> \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{Ponovo primenjujemo pravilo \<open>notE\<close> koje se opet primenjuje prvo na 
pretpostavku \<open>\<not> A\<close>}.\<close>
  apply (erule notE)
\<comment> \<open>\emph{Sada je cilj: \<open>\<lbrakk>\<not> B; B\<rbrakk> \<Longrightarrow> A\<close>. Pa ponovo primenjujemo pravilo \<open>notE\<close>, 
ali sada na pretpostavku \<open>\<not> B\<close>.}\<close>
  apply (erule notE)
\<comment> \<open>\emph{Sada je cilj: \<open>B \<Longrightarrow> B\<close> i možemo primeniti pravilo \<open>assumption\<close>}.\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza}.\<close>
  done


text\<open>Drugi način: \<close>

lemma shows "\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> B)"
  apply (rule impI)
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE)
   apply assumption 
  apply (erule notE) 
  back               
  apply assumption
  done

text\<open>Detaljno objašnjen dokaz teoreme, tek od dela koji se razlikuje od prethodnog dokaza:\<close>

lemma shows "\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> B)"
  apply (rule impI)
  apply (rule notI)
  apply (erule conjE)
  apply (erule disjE)
   apply (erule notE)
   apply assumption 
\<comment> \<open>\emph{U trenutku kada je cilj: \<open> \<lbrakk>\<not> A; \<not> B; B\<rbrakk> \<Longrightarrow> False\<close>, svakako moramo 
primeniti pravilo \<open>notE\<close>. Ono se primenjuje na \<open>\<not> A\<close> i prebacuje \<open>A\<close> na desnu 
stranu implikacije.}\<close>
  apply (erule notE) 
\<comment> \<open>\emph{Dobijamo cilj: \<open> \<lbrakk>\<not> B; B\<rbrakk> \<Longrightarrow> A\<close>.}\<close> 
\<comment> \<open>\emph{Međutim to nije najkraći put i možemo da iskoristimo naredbu \<open>back\<close>.}\<close>
\<comment> \<open>\emph{Naredba \<open>back\<close> izvršava backtracking nad rezultatom prethodne 
naredbe u dokazu. Ova komanda će pokušati izvršenje iste naredbe ali nad
sledećom pretpostavkom koja se nalazi u pretpostavkama tekućeg cilja.}\<close>
  back
\<comment> \<open>\emph{Sada dobijamo cilj: \<open> \<lbrakk>\<not> A; B\<rbrakk> \<Longrightarrow> B\<close>. I možemo odmah da primenimo 
naredbu \<open>assumption\<close>}.\<close>
  apply assumption
\<comment> \<open>\emph{Kraj dokaza}.\<close>
  done

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

text\<open>Dokaz teoreme:\<close>

lemma "\<not> (A \<longleftrightarrow> \<not> A)"
  apply (rule notI)
  apply (erule iffE)
  apply (erule impE) 
\<comment> \<open>apply (erule impE) --- ne uspeva\<close>
   back 
\<comment> \<open>apply (erule impE) --- ne uspeva\<close>
   apply (rule notI)
   apply (erule impE)
    apply assumption
   apply (erule notE)
   apply assumption
  apply (erule impE)
  apply assumption
  apply (erule notE)
  apply assumption
  done

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

U ovom dokazu se koristi pravilo za eliminaciju ekvivalencije @{text "iffE"}.\<close>

lemma "\<not> (A \<longleftrightarrow> \<not> A)"
\<comment> \<open>\emph{Cilj je identifikovan sa: \<open>A \<noteq> (\<not> A) \<close>}.\<close>
\<comment> \<open>\emph{Sada imamo situaciju kada je dominantni veznik negacija pa prvo 
primenjujemo pravilo \<open>notI\<close>}.\<close>
  apply (rule notI)                                 
\<comment> \<open>\emph{Sada je cilj: \<open>A = (\<not> A) \<Longrightarrow> False\<close>}.\<close>
\<comment> \<open>\emph{U pretpostavci imamo jednakost, odnosno ekvivalenciju pa moramo da 
primenimo pravilo \<open>iffE\<close> za eliminaciju ekvivalencije}.\<close>
  apply (erule iffE) 
\<comment> \<open>\emph{Sada dobijamo cilj: \<open>\<lbrakk>A \<longrightarrow> \<not> A; \<not> A \<longrightarrow> A\<rbrakk> \<Longrightarrow> False\<close>.}\<close>
\<comment> \<open>\emph{U ovoj situaciji imamo dve implikacije pa imamo mogućnost da se 
oslobodimo prve ili druge implikacije. U svakom slučaju primenjujemo pravilo 
\<open>impE\<close>}.\<close>
  apply (erule impE) 
\<comment>\<open>\emph{Kada prvi put primenimo pravilo \<open>impE\<close> eliminiše se prva implikacija 
\<open>A \<longrightarrow> \<not> A\<close>; i dobijaju se naredna dva podcilja: 
(1) prvo dokaži njenu pretpostavku (\<open>A\<close>) iz preostalih pretpostavki; 
(2) nakon toga iz preostalih pretpostavki zajedno sa njenim zaključkom (\<open>\<not> A\<close>) 
dokaži preostali cilj (\<open>False\<close>)}\<close>

\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. \<not> A \<longrightarrow> A \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>\<not> A \<longrightarrow> A; \<not> A\<rbrakk> \<Longrightarrow> False\<close>.}\<close>

\<comment> \<open>\<open>apply (erule impE)\<close> --- ne uspeva\<close>
\<comment>\<open>\emph{Ako bismo ovako uradili, naredni korak bi morao da bude 
\<open>apply (erule impE)\<close> ali onda dobijamo cilj koji ne možemo da dokažemo (\<open>\<not> A\<close>) 
i moramo da se vratimo! i pozivamo naredbu \<open>back\<close>}.\<close>
   back

\<comment>\<open>\emph{Naredba back poništava tu eliminaciju i eliminiše drugu implikaciju
\<open>\<not> A \<longrightarrow> A\<close>; i dobijamo naredna dva podcilja: 
(1) prvo dokaži njenu pretpostavku \<open>\<not> A\<close> iz preostalih pretpostavki;
(2) nakon toga iz preostalih pretpostavki zajedno sa njenim zaključkom (\<open>A\<close>) dokaži 
cilj}\<close>

\<comment> \<open>\emph{Sada dobijamo dva cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. A \<longrightarrow> \<not> A \<Longrightarrow> \<not> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A \<longrightarrow> \<not> A; A\<rbrakk> \<Longrightarrow> False\<close>.}\<close>

\<comment> \<open>\emph{Sada imamo implikaciju u pretpostavci i negaciju u zaključku. Ako bismo primenili pravilo 
\<open>impE\<close> za eliminaciju iz pretpostavke opet bismo dobili cilj koji ne možemo da dokažemo.}\<close>
\<comment> \<open>\<open>apply (erule impE)\<close> --- ne uspeva\<close>
\<comment> \<open>\emph{Pa primenjujemo pravilo \<open>notI\<close>}.\<close>
   apply (rule notI)  
\<comment> \<open>\emph{Sada dobijamo cilj: \<open>\<lbrakk>A \<longrightarrow> \<not> A; A\<rbrakk> \<Longrightarrow> False\<close>, pa nakon toga ponovo 
eliminišemo implikaciju u pretpostavkama.}\<close>
   apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva nova cilja:.}\<close>
\<comment> \<open>\emph{\<open>1. A \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; \<not> A\<rbrakk> \<Longrightarrow> False\<close>.}\<close>
\<comment> \<open>\emph{Prvi cilj je trivijalan}.\<close>
    apply assumption
\<comment> \<open>\emph{A za drugi cilj primenjujemo pravilo \<open>notE\<close>}.\<close>
   apply (erule notE)
\<comment> \<open>\emph{Čime dobijamo ponovo trivijalan cilj: \<open>A \<Longrightarrow> A\<close>}.\<close>
   apply assumption
\<comment> \<open>\emph{Sada dokazujemo drugi glavni podcilj: \<open>\<lbrakk>A \<longrightarrow> \<not> A; A\<rbrakk> \<Longrightarrow> False\<close> i prvo 
eliminišemo implikaciju iz pretpostavke.}\<close>
  apply (erule impE)
\<comment> \<open>\emph{Sada dobijamo dva nova cilja (ista kao malopre, pa se dokaz izvršava 
na isti način):.}\<close>
\<comment> \<open>\emph{\<open>1. A \<Longrightarrow> A\<close>.}\<close>
\<comment> \<open>\emph{\<open>2. \<lbrakk>A; \<not> A\<rbrakk> \<Longrightarrow> False\<close>.}\<close>
  apply assumption
  apply (erule notE)
  apply assumption
\<comment> \<open>\emph{Kraj dokaza}.\<close>
  done


subsection \<open> Dodatni primeri \<close>

text \<open>Naredne teoreme dokazati uz pomoć pravila prirodne dedukcije. Samo u prva dva dokaza će u
komentarima biti ispisano stanje nakon svakog koraka, zbog lakšeg praćenja, ostali dokazi su
navedeni bez dodatnih objašnjenja.\<close>


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


lemma "(Q \<longrightarrow> R) \<and> (R \<longrightarrow> P \<and> Q) \<and> (P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longleftrightarrow> Q)"
  apply (rule impI)
\<comment> \<open>\<open> 1. (Q \<longrightarrow> R) \<and> (R \<longrightarrow> P \<and> Q) \<and> (P \<longrightarrow> Q \<or> R) \<Longrightarrow> P = Q\<close>\<close>
  apply (erule conjE)
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; (R \<longrightarrow> P \<and> Q) \<and> (P \<longrightarrow> Q \<or> R)\<rbrakk> \<Longrightarrow> P = Q\<close>\<close>
  apply (erule conjE)
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R\<rbrakk> \<Longrightarrow> P = Q\<close>\<close>
\<comment>\<open>\emph{Sada primenjujemo pravilo uvođenja ekvivalencije i dobijamo naredna dva cilja: 
prvo iz prethodnih 
pretpostavki i pretpostavke P dokazujemo da važi Q, pa nakon toga da iz 
prethodnih pretpostavki i pretpostavke Q dokazujemo da važi P. }\<close>
  apply (rule iffI)
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; P\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment> \<open>\emph{Sada dokazujemo prvi cilj.}\<close>
\<comment>\<open>\emph{U pretpostavkama prvog cilja imamo \<open>P\<close> i \<open>P \<longrightarrow> Q \<or> R\<close> pa nam odgovara da 
eliminišemo baš tu implikaciju. Pošto je to treća implikacija u pretpostavkama, moraćemo 
dva puta da pozovemo naredbu \<open>back\<close>.} \<close>
   apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; P\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; P; R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
    back
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; P \<longrightarrow> Q \<or> R; P\<rbrakk> \<Longrightarrow> R\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; P \<longrightarrow> Q \<or> R; P; P \<and> Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
    back
\<comment> \<open>\emph{Sada smo došli do željenog rezultata.}\<close>
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P; Q \<or> R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
    apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P; Q \<or> R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
   apply (erule disjE)
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P; Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P; R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
    apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P; R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment>\<open>\emph{U pretpostavkama imamo P, R i dve implikacije, odgovara nam da 
eliminišemo onu implikaciju čije pretpostavke već znamo, odnosno drugu 
implikaciju, pa ćemo jednom primeniti naredbu \<open>back\<close>.}\<close>
   apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>R \<longrightarrow> P \<and> Q; P; R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>R \<longrightarrow> P \<and> Q; P; R; R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
    back
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; P; R\<rbrakk> \<Longrightarrow> R\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; P; R; P \<and> Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
    apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; P; R; P \<and> Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
   apply (erule conjE)
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; P; R; P; Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
   apply assumption 
\<comment>\<open>\emph{Tek sada smo dokazali da važi Q, tj. prvi podcilj}\<close>
\<comment>\<open>\emph{Sada dokazujemo drugi podcilj}\<close>
\<comment> \<open>\<open> 1. \<lbrakk>Q \<longrightarrow> R; R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment>\<open>\emph{U pretpostavkama imamo Q pa nam odgovara da se eliminiše prva 
implikacija.}\<close>
  apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q; R\<rbrakk> \<Longrightarrow> P\<close>\<close>
   apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>R \<longrightarrow> P \<and> Q; P \<longrightarrow> Q \<or> R; Q; R\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment>\<open>\emph{U pretpostavkama imamo R pa nam odgovara da se eliminiše prva 
implikacija.}\<close>
  apply (erule impE)
\<comment> \<open>\<open> 1. \<lbrakk>P \<longrightarrow> Q \<or> R; Q; R\<rbrakk> \<Longrightarrow> R\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>P \<longrightarrow> Q \<or> R; Q; R; P \<and> Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
  apply assumption
\<comment> \<open>\<open> 1. \<lbrakk>P \<longrightarrow> Q \<or> R; Q; R; P \<and> Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
  apply (erule conjE)
\<comment> \<open>\<open> 1. \<lbrakk>P \<longrightarrow> Q \<or> R; Q; R; P; Q\<rbrakk> \<Longrightarrow> P\<close>\<close>
  apply assumption
\<comment> \<open>No subgoals!\<close>
  done


text\<open>
\begin{exmp} 
@{text "(P \<longrightarrow> Q) \<and> (Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<and> R)"} 
\end{exmp}
\<close>
lemma "(P \<longrightarrow> Q) \<and> (Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<and> R)"
  apply (rule impI) 
\<comment> \<open>\<open> 1. (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> R) \<Longrightarrow> P \<longrightarrow> Q \<and> R\<close>\<close>
  apply (rule impI) 
\<comment> \<open>\<open> 1. \<lbrakk>(P \<longrightarrow> Q) \<and> (Q \<longrightarrow> R); P\<rbrakk> \<Longrightarrow> Q \<and> R\<close>\<close>
  apply (erule conjE) 
\<comment> \<open>\<open> 1. \<lbrakk>P; P \<longrightarrow> Q; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> Q \<and> R\<close>\<close>
  apply (rule conjI) 
\<comment> \<open>\<open> 1. \<lbrakk>P; P \<longrightarrow> Q; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>P; P \<longrightarrow> Q; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close>\<close>
   apply (erule impE) 
\<comment> \<open>\<open> 1. \<lbrakk>P; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>P; Q \<longrightarrow> R; Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 3. \<lbrakk>P; P \<longrightarrow> Q; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close>\<close>
    apply assumption 
\<comment> \<open>\<open> 1. \<lbrakk>P; Q \<longrightarrow> R; Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>P; P \<longrightarrow> Q; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close>\<close>
   apply assumption 
\<comment> \<open>\<open> 1. \<lbrakk>P; P \<longrightarrow> Q; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> R\<close>\<close>
  apply (erule impE) 
\<comment> \<open>\<open> 1. \<lbrakk>P; Q \<longrightarrow> R\<rbrakk> \<Longrightarrow> P\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>P; Q \<longrightarrow> R; Q\<rbrakk> \<Longrightarrow> R\<close>\<close>
   apply assumption 
\<comment> \<open>\<open> 1. \<lbrakk>P; Q \<longrightarrow> R; Q\<rbrakk> \<Longrightarrow> R\<close>\<close>
  apply (erule impE) 
\<comment> \<open>\<open> 1. \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> Q\<close>\<close>
\<comment> \<open>\<open> 2. \<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> R\<close>\<close>
   apply assumption 
\<comment> \<open>\<open> 1. \<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> R\<close>\<close>
  apply assumption 
\<comment> \<open>No subgoals!\<close>
  done


text\<open>
\begin{exmp} 
@{text "(P \<longrightarrow> Q) \<and> \<not> Q \<longrightarrow> \<not> P"} 
\end{exmp}
\<close>
lemma "(P \<longrightarrow> Q) \<and> \<not> Q \<longrightarrow> \<not> P"
  apply (rule impI)
  apply (erule conjE)
  apply (rule notI)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> (Q \<longrightarrow> (P \<longrightarrow> R))"} 
\end{exmp}
\<close>
lemma "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> (Q \<longrightarrow> (P \<longrightarrow> R))"
  apply (rule impI)
  apply (rule impI)
  apply (rule impI)
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "\<not> (P \<and> \<not>P)"} 
\end{exmp}
\<close>
lemma "\<not> (P \<and> \<not>P)"
  apply (rule notI)
  apply (erule conjE)
  apply (erule notE)
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "A \<and> (B \<or> C) \<longrightarrow> (A \<and> B) \<or> (A \<and> C)"} 
\end{exmp}
\<close>
lemma "A \<and> (B \<or> C) \<longrightarrow> (A \<and> B) \<or> (A \<and> C)"
  apply (rule impI)
  apply (erule conjE)
  apply (erule disjE)
   apply (rule disjI1)
   apply (rule conjI)
    apply assumption
   apply assumption
  apply (rule disjI2)
  apply (rule conjI)
   apply assumption
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "\<not> (A \<and> B) \<longrightarrow> (A \<longrightarrow> \<not>B)"} 
\end{exmp}
\<close>
lemma "\<not> (A \<and> B) \<longrightarrow> (A \<longrightarrow> \<not>B)"
  apply (rule impI)
  apply (rule impI)
  apply (rule notI)
  apply (erule notE)
  apply (rule conjI)
   apply assumption
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "(A \<longrightarrow> C) \<and> (B \<longrightarrow> \<not> C) \<longrightarrow> \<not> (A \<and> B)"} 
\end{exmp}
\<close>
lemma "(A \<longrightarrow> C) \<and> (B \<longrightarrow> \<not> C) \<longrightarrow> \<not> (A \<and> B)"
  apply (rule impI)
  apply (rule notI)
  apply (erule conjE)
  apply (erule conjE)
  apply (erule impE)
  apply assumption
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "(A \<and> B) \<longrightarrow> ((A \<longrightarrow> C) \<longrightarrow> \<not> (B \<longrightarrow> \<not> C))"} 
\end{exmp}
\<close>
lemma "(A \<and> B) \<longrightarrow> ((A \<longrightarrow> C) \<longrightarrow> \<not> (B \<longrightarrow> \<not> C))"
  apply (rule impI)
  apply (rule impI)
  apply (rule notI)
  apply (erule conjE)
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "(A \<longleftrightarrow> B) \<longrightarrow> (\<not> A \<longleftrightarrow> \<not> B)"} 
\end{exmp}
\<close>
lemma "(A \<longleftrightarrow> B) \<longrightarrow> (\<not> A \<longleftrightarrow> \<not> B)"
  apply (rule impI)
  apply (rule iffI)
   apply (rule notI)
  apply (erule notE)
   apply (erule iffE)
   apply (erule impE)
    apply (erule impE)
     apply assumption
    apply assumption
   apply (erule impE)
  apply assumption
   apply assumption
  apply (rule notI)
  apply (erule notE)
  apply (erule iffE)
  apply (erule impE)
   apply assumption
  apply assumption
  done

text\<open>Malo kraći dokaz iste teoreme uz korišćenje naredbe @{text "back"}. \<close>

lemma "(A \<longleftrightarrow> B) \<longrightarrow> (\<not> A \<longleftrightarrow> \<not> B)"
  apply (rule impI)
  apply (rule iffI)
   apply (rule notI)
  apply (erule notE)
   apply (erule iffE)
   apply (erule impE) 
\<comment>\<open>\emph{Ako ovde upotrebimo \<open>back\<close> dobijamo kraći dokaz.} \<close>
    back
    apply assumption
   apply assumption
  apply (rule notI)
  apply (erule notE)
  apply (erule iffE)
  apply (erule impE)
  apply assumption
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "A \<longrightarrow> \<not> \<not> A"} 
\end{exmp}
\<close>
lemma "A \<longrightarrow> \<not> \<not> A"
  apply (rule impI)
  apply (rule notI)
  apply (erule notE)
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "\<not> (A \<longleftrightarrow> \<not> A)"} 
\end{exmp}
\<close>
lemma "\<not> (A \<longleftrightarrow> \<not> A)"
  apply (rule notI)
  apply (erule iffE)
  apply (erule impE)
   back
   apply (rule notI)
   apply (erule impE)
    apply assumption
   apply (erule notE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "(A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> \<not> A)"} 
\end{exmp}
\<close>
lemma "(A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> \<not> A)"
  apply (rule impI)
  apply (rule impI)
  apply (rule notI)
  apply (erule notE)
  apply (erule impE)
   apply assumption
  apply assumption
  done

text\<open>
\begin{exmp} 
@{text "\<not> A \<or> B \<longrightarrow> (A \<longrightarrow> B)"} 
\end{exmp}
\<close>
lemma "\<not> A \<or> B \<longrightarrow> (A \<longrightarrow> B)"
  apply (rule impI)
  apply (rule impI)
  apply (erule disjE)
   apply (erule notE)
   apply assumption                                                                    
  apply assumption
  done

(* Filip: TODO: Da bi tekst u nastavku bio razumljiv, neophodno je proširiti ga primerima} *)


section\<open>Opis mehanizma primene pravila\<close>

text\<open>Primena pravila prirodne dedukcije, se pokreće ključnom rečju @{text "apply"}, najčešće sa
metodima @{text "rule"} i @{text "erule"}. Pored njih, moguće je primenjivati i metode @{text
"drule"} i @{text "frule"}. Umesto višestrukog navođenja istog pravila više puta za redom, može se navesti simbol \verb|+| nakon samog pravila.
U nastavku je detaljno objašnjen mehanizam primene ovih metoda u
kombinaciji sa pravilima uvođenja i eliminacije.

\begin{itemize}

\item Metod @{text "rule R"} unifikuje $Q$ sa tekućim podciljem, izbacuje taj podcilj i umesto njega
uvodi $n$ novih podciljeva $P_1, \ldots, P_n$. Pravilo @{text "rule"} se koristi za primenu pravila
uvođenja.

\item Metod @{text "erule R"} unifikuje $Q$ sa tekućim podciljem i istovremeno unifikuje $P_1$ sa
nekom pretpostavkom koja se trenutno koristi za dokazivanje tekućeg podcilja. $P_1$ se smatra
glavnom pretpostavkom kada se primenjuje sa metodom @{text "erule"} i metodom @{text "drule"} (koji
će biti opisan u narednom pasusu). Podcilj se izbacuje i umesto njega se uvodi $n-1$ novih
podciljeva $P_2, \ldots, P_n$ (koji među svojim pretpostavkama nemaju pretpostavku $P_1$ koja je
korišćena prilikom primene pravila).

U slučaju da ne želimo da se data pretpostavka obriše, može se alternativno koristiti metod
@{text "(rule R, assumption)"}.

\item Metod @{text "drule R"} unifikuje $P_1$ sa nekom od pretpostavki (nakon te unifikacije
odgovarajuća pretpostavka se briše). Podcilj se zamenjuje sa $n-1$ novih podciljeva $P_2, \ldots,
P_n$. $n$-ti podcilj će izgledati isto kao polazni podcilj, sa dodatom pretpostavkom $Q$. Ovaj metod
se koristi za primenu destruktivnih pravila.

\item Metod @{text "frule R"} je isti kao @{text "drule R"}, s tim što se pretpostavka koja je
korišćena prilikom primene pravila ne briše.

\item Alternativa je (za svako od ovih pravila) je da se pravilo primeni sa instanciranjem nekih od
njegovih promenljivih, na primer:

\verb|rule_tac| $v_1 = t_1$ \verb|and ... and| $v_k = t_k$ \verb|in R|

\item Dodatno pored instanciranja, ako dokaz ima nekoliko nedokazanih podciljeva, korisnik može
izabrati redni broj podcilja na koji želi da se fokusira i da na njega bude primenjeno odabrano
pravilo:

@{text "rule_tac [i] R"}

\item Pravilo @{text "assumption"}: koristi se ako se negde u pretpostavkama nalazi P, tada smatramo
da je taj podcilj dokazan.

\item Komanda @{text "apply rule"}: koristi se kada želimo da dokazivač sam odabere pravilo prirodne
dedukcije na osnovu trenutno aktuelnog cilja.

\item Komanda @{text "done"}: koristi se kao poslednja naredba u dokazu. Primenjuje se kada više
nema nedokazanih ciljeva i njome se evidentira nova teorema u Isabelle/HOL sistemu. 

\end{itemize}\<close>

end