1 (*:maxLineLen=80:*)
   2 (* 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 *)
   3 
   4 section ‹ Classical propositional logic ›
   5 
   6 theory Cas6_vezbe_postavke
   7 imports Main
   8 
   9 begin
  10 
  11 subsection ‹Podsećanje sa predavanja›
  12 
  13 subsubsection ‹Pravilo ccontr›
  14 
  15 text‹Do sada su svi dokazi bili u okviru intuicionističke logike. Za rad sa 
  16 negacijom koristili smo dva pravila: 
  17 pravilo eliminacije negacije @{text notE}: @{text "⟦¬ P; P⟧ ⟹ R"}, 
  18 i pravilo uvođenja negacije @{text notI}: @{text "(P ⟹ False) ⟹ ¬ P"}.›
  19 
  20 text‹Kada se radi u okvirima klasične logike, imamo mogućnost da koristimo i 
  21 pravilo @{text ccontr}: @{text "(¬ P ⟹ False) ⟹ P"}. Odnosno možemo da 
  22 izvodimo i dokaze uz pomoć kontradikcije, \emph{ccontr} označava 
  23 \emph{classical contradiction}.›
  24 
  25 thm notE 
  26 thm notI 
  27 thm ccontr  
  28 
  29 
  30 lemma "¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B"
  31   apply (rule impI) 
  32   ― ‹primena pravila ccontr će prebaciti zaključak u negativnom obliku u premise, 
  33      i pokušaće da dokaze kontradikciju, odnosno False›
  34   apply (rule ccontr) ―‹često se nad disjunkcijom u zaključku primenjuje ovo pravilo›
  35   ― ‹kada imamo dve premise na koje možemo primeniti isto pravilo, možemo da biramo 
  36      da li ćemo primeniti na prvu ili drugu pretpostavku, međutim ovde nam odgovara 
  37      da ostavimo ovakvu primenu (bez back), zato što je bolje sa desne strane imati 
  38      konjunkciju nego disjunkciju; 
  39   Napomena: pogledajte šta se dešava kada stavite back›
  40   apply (erule notE) 
  41   apply (rule conjI)
  42    ―‹sada dokazujemo prvi podcilj›
  43    apply (rule ccontr)
  44    apply (erule notE) ― ‹ovde nam odgovara da imamo disjunkciju sa desne strane 
  45                          zato što se jednostavno eliminiše›
  46    apply (rule disjI1)
  47    apply assumption
  48   ―‹sada dokazujemo drugi podcilj›
  49   apply (rule ccontr)
  50   apply (erule notE)
  51   apply (rule disjI2)
  52   apply assumption
  53   done
  54 
  55 text‹Dokaz ove iste leme u Isar-u: ›
  56 
  57 lemma "¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B"
  58 proof 
  59 ― ‹isto kao da smo napisali @{text "proof (rule impI)"}, ali ovde će i sam Isabelle 
  60 primeniti pravilo impI pa nije neophodno da stoji i nakon toga ide assume Levo show Desno›
  61   assume "¬ (A ∧ B)"
  62   show "¬ A ∨ ¬ B" ― ‹ovo je naš cilj C ›
  63   proof (rule ccontr)
  64   ― ‹obratite pažnju: ako ne napišemo ništa (pogledajte šta se dešava ako se samo 
  65   napiše @{text proof}), Isabelle će ovaj cilj transformisati u prvi disjunkt, što 
  66   nije ono što želimo - nije korektno, tako da moramo paziti i eksplicitno navesti 
  67   koje pravilo želimo da bude primenjeno›
  68 
  69      ― ‹da bi dokazali cilj C na osnovu pravila ccontr, dovoljno je da pokažemo da 
  70      @{text "¬ C ⟹ False"}, pa nakon toga sledi @{text "assume ¬ C ... show False"} blok ›
  71     assume "¬ (¬ A ∨ ¬ B)" 
  72     have "A ∧ B" ― ‹među korak koji prvo dokazujemo ›
  73     proof
  74        ― ‹sada nam odgovara da bude samo proof, bez crtice, jer Isabelle sam deli 
  75        ovaj cilj na dva cilja ›
  76       show "A"
  77       proof (rule ccontr) 
  78       ― ‹slično kao gore, da bi dokazali A korišćenjem pravila ccontr, dovoljno je da 
  79          pokažemo @{text "¬ A ⟹ False"} odnosno sledi @{text "assume ¬ A ... show False"} blok ›
  80         assume "¬ A"
  81         then have "¬ A ∨ ¬ B"
  82           by (rule disjI1)
  83         then show "False"
  84           using ‹¬ (¬ A ∨ ¬B)› ― ‹sve do sada uvedene pretpostavke mogu se koristiti, 
  85                                 ali moraju biti navedene svojim vrednostima, između `...` ›
  86           by auto
  87       qed
  88     next
  89       show "B"
  90       proof (rule ccontr)
  91         assume "¬ B"
  92         then have "¬ A ∨ ¬ B"
  93           by (rule disjI2)
  94         then show "False"
  95           using ‹¬ (¬ A ∨ ¬B)›
  96           by auto
  97       qed
  98     qed
  99     then show False
 100       using `¬ (A ∧ B)`
 101       by auto
 102   qed
 103 qed
 104 
 105 subsubsection ‹ Pravilo classical ›
 106 
 107 text‹ Princip klasične logike se oslikava kroz pravilo 
 108 @{text classical}: @{text "(¬ P ⟹ P) ⟹ P"}. Postoji nekoliko ekvivalentnih 
 109 varijanti ovog pravila ali je ovaj oblik najpogodniji za upotrebu zato što ne menja 
 110 traženi zaključak teoreme. Ovo pravilo podrazumeva da u dokazu teoreme uvek možemo 
 111 pretpostaviti negaciju zaključka teoreme.›
 112 
 113 thm classical
 114 
 115 lemma "P ∨ ¬ P"
 116   apply (rule classical) ―‹da bi smo dokazali A moramo da prvo dokažemo @{text "¬ A ⇒ A"}›
 117   apply (rule disjI1) ―‹dovoljno je da dokažemo jednu od dve disjunkcije, a kako je sve simetricno, biramo da dokažemo P ›
 118   apply (rule classical) ―‹na postojeće pretpostavke dodajemo @{text "¬ P"} i pokušavamo da dokažemo P›
 119   apply (erule notE) ―‹notE znači da treba da dokažemo pozitivan oblik iz preostalih pretpostavki›
 120   apply (rule disjI2)
 121   apply assumption
 122   done
 123 
 124 lemma "P ∨ ¬ P"
 125 proof (rule classical)
 126 ―‹ovde ne smemo ostaviti bez crtice, zato što Isabelle transformiše disjunkciju
 127 u prvi disjunkt - u ovom trenutku to nam ne odgovara i ne možemo to dokazati 
 128 zato što još uvek nemamo nikakve pretpostavke; 
 129 nećemo ni sa crticom, već ćemo odmah reći koje pravilo želimo da se primeni›
 130   assume "¬ (P ∨ ¬ P)"
 131   show "P ∨ ¬ P" 
 132   proof 
 133   ―‹sada ćemo ostaviti bez crtice, zato što nam odgovara da primeni podrazumevano pravilo, 
 134 tj. disjI1›
 135     show "P"
 136     proof (rule classical)
 137       assume "¬ P"
 138       from this have "P ∨ ¬ P" by auto
 139       from this `¬ (P ∨ ¬ P)` have False by auto
 140       from this show "P" by auto
 141     qed
 142   qed
 143 qed
 144 
 145 subsection ‹Dodatni primeri›
 146 
 147 text‹U klasičnoj logici, dokazati naredna tvrđenja:›
 148 
 149 lemma "¬ ¬ A ⟶ A"
 150   by auto
 151 
 152 lemma "(¬ B ⟶ ¬ A) ⟶ (A ⟶ B)"
 153   by auto
 154 
 155 lemma "(A ⟶ B) ⟶ (¬ A ∨ B)"
 156   by auto
 157 
 158 lemma "(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)"
 159   by auto
 160 
 161 lemma "(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)"
 162   by auto
 163 
 164 text‹Pirsov zakon. Tipičan ne-intuicionistički primer koji će sigurno zahtevati 
 165 neki oblik klasične kontradikcije.›
 166 
 167 lemma "((P ⟶ Q) ⟶ P) ⟶ P"
 168   by auto
 169 
 170 text‹Dokazati ovu istu teoremu i u Isar-u.›
 171 
 172 lemma 
 173   assumes "(P ⟶ Q) ⟶ P"
 174   shows "P"
 175   sorry
 176 
 177 text ‹Malo komplikovaniji primeri ›
 178 
 179 text ‹ 
 180 \begin{exmp}
 181 Ako je relacija R simetricna, tranzitivna i ako za svako x postoji y koje je sa njim u 
 182 relaciji, onda je relacija R i refleksivna. 
 183 \end{exmp}
 184 ›
 185 
 186 text‹Prvo je potrebno uvesti definicije pojmova koji se javljaju u postavci ovog zadatka:›
 187 
 188 definition
 189   "reflexive R ⟷ (∀ x. R x x)"
 190 
 191 definition
 192   "transitive R ⟷ (∀ x y z. R x y ∧ R y z ⟶ R x z)"
 193 
 194 definition
 195   "symmetric R ⟷ (∀ x y. R x y ⟷ R y x)"
 196 
 197 lemma "symmetric R ∧ transitive R ∧ (∀ x. ∃ y. R x y) ⟶ reflexive R"
 198   unfolding symmetric_def transitive_def reflexive_def
 199   by blast
 200 
 201 lemma 
 202   shows "(nA ⟷ bA ∨ bB) ∧ (nB ⟷ ¬ bA) ∧ ((nA ∧ nB) ∨ (¬ nA ∧ ¬ nB)) ⟶ ¬ bA ∧ bB"
 203   by auto
 204 
 205 end