1 (*:maxLineLen=80:*)
   2 (* Vodite racuna kada preuzimate fajl da skinete thy, a ne htm - njega mozete 
   3 koristiti samo za brz pregled zato sto je laksi za online citanje *)
   4 
   5 section  Classical propositional logic 
   6 
   7 theory Cas6_vezbe_resenja
   8 imports Main
   9 
  10 begin
  11 
  12 subsection Podsećanje sa predavanja
  13 
  14 subsubsection Pravilo ccontr
  15 
  16 textDo sada su svi dokazi bili u okviru intuicionističke logike. Za rad sa 
  17 negacijom koristili smo dva pravila: 
  18 pravilo eliminacije negacije @{text notE}: @{text "⟦¬ P; P⟧ ⟹ R"}, 
  19 i pravilo uvođenja negacije @{text notI}: @{text "(P  False)  ¬ P"}.
  20 
  21 textKada se radi u okvirima klasične logike, imamo mogućnost da koristimo i 
  22 pravilo @{text ccontr}: @{text "(¬ P ⟹ False) ⟹ P"}. Odnosno možemo da 
  23 izvodimo i dokaze uz pomoć kontradikcije, \emph{ccontr} označava 
  24 \emph{classical contradiction}.
  25 
  26 thm notE 
  27 thm notI 
  28 thm ccontr  
  29 
  30 
  31 lemma "¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B"
  32   apply (rule impI) 
  33    primena pravila ccontr će prebaciti zaključak u negativnom obliku u premise, 
  34      i pokušaće da dokaze kontradikciju, odnosno False
  35   apply (rule ccontr) često se nad disjunkcijom u zaključku primenjuje ovo pravilo
  36    kada imamo dve premise na koje možemo primeniti isto pravilo, možemo da biramo 
  37      da li ćemo primeniti na prvu ili drugu pretpostavku, međutim ovde nam odgovara 
  38      da ostavimo ovakvu primenu (bez back), zato što je bolje sa desne strane imati 
  39      konjunkciju nego disjunkciju; 
  40   Napomena: pogledajte šta se dešava kada stavite back
  41   apply (erule notE) 
  42   apply (rule conjI)
  43    sada dokazujemo prvi podcilj
  44    apply (rule ccontr)
  45    apply (erule notE)  ovde nam odgovara da imamo disjunkciju sa desne strane 
  46                          zato što se jednostavno eliminiše
  47    apply (rule disjI1)
  48    apply assumption
  49   sada dokazujemo drugi podcilj
  50   apply (rule ccontr)
  51   apply (erule notE)
  52   apply (rule disjI2)
  53   apply assumption
  54   done
  55 
  56 textDokaz ove iste leme u Isar-u: 
  57 
  58 lemma "¬ (A ∧ B) ⟶ ¬ A ∨ ¬ B"
  59 proof 
  60  isto kao da smo napisali @{text "proof (rule impI)"}, ali ovde će i sam Isabelle 
  61 primeniti pravilo impI pa nije neophodno da stoji i nakon toga ide assume Levo show Desno
  62   assume "¬ (A ∧ B)"
  63   show "¬ A ∨ ¬ B"  ovo je naš cilj C 
  64   proof (rule ccontr)
  65    obratite pažnju: ako ne napišemo ništa (pogledajte šta se dešava ako se samo 
  66   napiše @{text proof}), Isabelle će ovaj cilj transformisati u prvi disjunkt, što 
  67   nije ono što želimo - nije korektno, tako da moramo paziti i eksplicitno navesti 
  68   koje pravilo želimo da bude primenjeno
  69 
  70       da bi dokazali cilj C na osnovu pravila ccontr, dovoljno je da pokažemo da 
  71      @{text "¬ C  False"}, pa nakon toga sledi @{text "assume ¬ C ... show False"} blok 
  72     assume "¬ (¬ A ∨ ¬ B)" 
  73     have "A ∧ B"  među korak koji prvo dokazujemo 
  74     proof
  75         sada nam odgovara da bude samo proof, bez crtice, jer Isabelle sam deli 
  76        ovaj cilj na dva cilja 
  77       show "A"
  78       proof (rule ccontr) 
  79        slično kao gore, da bi dokazali A korišćenjem pravila ccontr, dovoljno je da 
  80          pokažemo @{text "¬ A  False"} odnosno sledi @{text "assume ¬ A ... show False"} blok 
  81         assume "¬ A"
  82         then have "¬ A ∨ ¬ B"
  83           by (rule disjI1)
  84         then show "False"
  85           using ¬ (¬ A  ¬B)  sve do sada uvedene pretpostavke mogu se koristiti, 
  86                                 ali moraju biti navedene svojim vrednostima, između `...` 
  87           by auto
  88       qed
  89     next
  90       show "B"
  91       proof (rule ccontr)
  92         assume "¬ B"
  93         then have "¬ A ∨ ¬ B"
  94           by (rule disjI2)
  95         then show "False"
  96           using ¬ (¬ A  ¬B)
  97           by auto
  98       qed
  99     qed
 100     then show False
 101       using `¬ (A ∧ B)`
 102       by auto
 103   qed
 104 qed
 105 
 106 subsubsection  Pravilo classical 
 107 
 108 text Princip klasične logike se oslikava kroz pravilo 
 109 @{text classical}: @{text "(¬ P ⟹ P) ⟹ P"}. Postoji nekoliko ekvivalentnih 
 110 varijanti ovog pravila ali je ovaj oblik najpogodniji za upotrebu zato što ne menja 
 111 traženi zaključak teoreme. Ovo pravilo podrazumeva da u dokazu teoreme uvek možemo 
 112 pretpostaviti negaciju zaključka teoreme.
 113 
 114 thm classical
 115 
 116 lemma "P ∨ ¬ P"
 117   apply (rule classical) da bi smo dokazali A moramo da prvo dokažemo @{text "¬ A  A"}
 118   apply (rule disjI1) dovoljno je da dokažemo jednu od dve disjunkcije, a kako je sve simetricno, biramo da dokažemo P 
 119   apply (rule classical) na postojeće pretpostavke dodajemo @{text "¬ P"} i pokušavamo da dokažemo P
 120   apply (erule notE) notE znači da treba da dokažemo pozitivan oblik iz preostalih pretpostavki
 121   apply (rule disjI2)
 122   apply assumption
 123   done
 124 
 125 lemma "P ∨ ¬ P"
 126 proof (rule classical)
 127 ovde ne smemo ostaviti bez crtice, zato što Isabelle transformiše disjunkciju
 128 u prvi disjunkt - u ovom trenutku to nam ne odgovara i ne možemo to dokazati 
 129 zato što još uvek nemamo nikakve pretpostavke; 
 130 nećemo ni sa crticom, već ćemo odmah reći koje pravilo želimo da se primeni
 131   assume "¬ (P ∨ ¬ P)"
 132   show "P ∨ ¬ P" 
 133   proof 
 134   sada ćemo ostaviti bez crtice, zato što nam odgovara da primeni podrazumevano pravilo, 
 135 tj. disjI1
 136     show "P"
 137     proof (rule classical)
 138       assume "¬ P"
 139       from this have "P ∨ ¬ P" by auto
 140       from this `¬ (P ∨ ¬ P)` have False by auto
 141       from this show "P" by auto
 142     qed
 143   qed
 144 qed
 145 
 146 subsection Dodatni primeri
 147 
 148 textU klasičnoj logici, dokazati naredna tvrđenja:
 149 
 150 lemma "¬ ¬ A ⟶ A"
 151   apply (rule impI)
 152    apply (erule notE) ne možemo primeniti ovo pravilo zato što ono očekuje da iz 
 153   @{text "¬ P"} i @{text P} možemo da izvedemo bilo šta. @{text "¬ P"} je ovde 
 154   @{text "¬ ¬ A"}, što znači da je @{text P} u stvari @{text "¬ A"}, i zato ono 
 155   postaje preostali cilj
 156   apply (rule ccontr) 
 157   apply (erule notE)
 158   apply assumption
 159   done
 160 
 161 lemma "(¬ B ⟶ ¬ A) ⟶ (A ⟶ B)"
 162   apply (rule impI)
 163   apply (rule impI)
 164   apply (rule ccontr)  prebacuje zaključak sa desna na levo i pokušavamo da 
 165                       izvedemo kontradikciju
 166   apply (erule impE)
 167    apply assumption
 168   apply (erule notE)  eliminacija negacije, ali treba da je primenimo na drugu 
 169                      negaciju, ne na @{text "¬ B"}, već na @{text "¬ A"}
 170   back
 171   apply assumption
 172   done
 173 
 174 lemma "(A ⟶ B) ⟶ (¬ A ∨ B)"
 175   apply (rule impI)
 176   apply (rule ccontr)
 177   apply (erule impE)
 178    apply (rule ccontr)
 179    apply (erule notE)
 180    apply (rule disjI1)
 181    apply assumption
 182   apply (erule notE)
 183   apply (rule disjI2)
 184   apply assumption
 185   done
 186 
 187 lemma "(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)"
 188   apply (rule iffI) dobijamo dva cilja; sada prvo razbijamo implikaciju sa desne 
 189                     strane u prvom cilju 
 190    apply (rule impI) sada prebacujemo zaključak na levu stranu i desno dobijamo False 
 191    apply (rule ccontr) ovo nam odgovara zato što se sada @{text "¬ P"} dodaje među 
 192                        pretpostavke, a već se pojavljuje kao leva strana implikacije 
 193    apply (erule impE)
 194     apply (assumption)
 195    apply (erule notE)
 196    apply assumption sada smo zatvorili prvi cilj, pa slično sa drugim ciljom
 197   apply (rule impI)
 198   apply (rule ccontr) slično kao u prethodnoj primeni, odgovara nam da @{text "¬ Q"} 
 199                       prebacimo u pretpostavke jer se već pojavljuje kao leva strana implikacije
 200   apply (erule impE)
 201    apply assumption
 202   apply (erule notE)
 203   apply assumption
 204   done
 205 
 206 
 207 lemma "(¬ P ⟶ Q) ⟷ (¬ Q ⟶ P)"
 208   apply (rule iffI)
 209    apply (rule impI)
 210    apply (rule ccontr)
 211    apply (erule impE)
 212     apply assumption
 213    apply (erule notE)
 214    apply assumption
 215   apply (rule impI)
 216   apply (rule ccontr)
 217   apply (erule impE)
 218    apply assumption
 219   apply (erule notE)
 220   apply assumption
 221   done
 222 
 223 textPirsov zakon. Tipičan ne-intuicionistički primer koji će sigurno zahtevati 
 224 neki oblik klasične kontradikcije.
 225 
 226 lemma "((P ⟶ Q) ⟶ P) ⟶ P"
 227   apply (rule impI)
 228   apply (rule ccontr) primena klasične kontradikcije, dodajemo negirani zaključak 
 229                       kao novu premisu i pokušavamo da izvedemo kontradikciju
 230   apply (erule impE)
 231    apply (rule impI)
 232    apply (erule notE)
 233    apply assumption
 234   apply (erule notE)
 235   apply assumption
 236   done
 237 
 238 textDokaz u Isar-u:
 239 
 240 lemma 
 241   assumes "(P ⟶ Q) ⟶ P"
 242   shows "P"
 243 proof (rule ccontr) dodajemo negaciju zaključka u premise i pokušavamo da izvedemo 
 244                     kontradikciju
 245   assume "¬ P"
 246   dodajemo međukorak
 247   have "P ⟶ Q" 
 248   proof
 249     assume "P"
 250     from this `¬ P` show "Q" by auto
 251   qed
 252   from this assms have "P" by auto
 253   from this `¬ P` show False by auto
 254 qed
 255 
 256 text Malo komplikovaniji primeri 
 257 
 258 text  
 259 \begin{exmp}
 260 Ako je relacija R simetricna, tranzitivna i ako za svako x postoji y koje je sa njim u 
 261 relaciji, onda je relacija R i refleksivna. 
 262 \end{exmp}
 263 
 264 
 265 textPrvo je potrebno uvesti definicije pojmova koji se javljaju u postavci ovog zadatka:
 266 
 267 definition
 268   "reflexive R ⟷ (∀ x. R x x)"
 269 
 270 definition
 271   "transitive R ⟷ (∀ x y z. R x y ∧ R y z ⟶ R x z)"
 272 
 273 definition
 274   "symmetric R ⟷ (∀ x y. R x y ⟷ R y x)"
 275 
 276 lemma "symmetric R ∧ transitive R ∧ (∀ x. ∃ y. R x y) ⟶ reflexive R"
 277   unfolding symmetric_def transitive_def reflexive_def
 278 prvo primenjujemo unfolding da bismo radili nad samim formulama
 279   apply (rule impI)
 280   apply (erule conjE)
 281   apply (erule conjE)
 282   apply (rule allI) uvodimo fiksirano ali proizvoljno x
 283   sada hoćemo da razbijemo treću premisu, da bismo dosli do exists
 284   apply (erule_tac x = "x" in allE) back back
 285   apply (erule exE) uvodimo fiksirano y
 286   sada skidamo univerzalni kvantifikator za već dobijeno x
 287   apply (erule_tac x = "x" in allE)
 288   apply (erule_tac x = "x" in allE)
 289   sada treba da vodimo računa da nam je primarni kvantifikator po y, i odgovara 
 290   nam da ostane y (naspram x, pogledajte šta bi se dobilo na taj način)
 291   apply (erule_tac x = "y" in allE)
 292   apply (erule_tac x = "y" in allE)
 293   sada biramo sa čim ćemo da zamenimo z, odgovara nam x (pogledajte šta bi se 
 294   dobilo kada biste napisali y)
 295   apply (erule_tac x = "x" in allE)
 296   sada radimo na uobičajeni nacin, nakon što smo sve unifikovali kako treba
 297   apply (erule impE)
 298   apply (rule conjI)
 299     apply assumption
 300    apply (erule iffE)
 301    apply (erule impE)
 302     apply assumption
 303    apply assumption
 304   apply assumption
 305   done
 306 
 307 
 308 lemma 
 309   shows "(nA ⟷ bA ∨ bB) ∧ (nB ⟷ ¬ bA) ∧ ((nA ∧ nB) ∨ (¬ nA ∧ ¬ nB)) ⟶ ¬ bA ∧ bB"
 310   apply (rule impI)  prvo razbijamo što više možemo levu stranu, da ne bismo prvo 
 311                     razbili desnu pa onda dva puta ponavljali isti postupak za obe grane
 312    apply (erule conjE)
 313   apply (erule conjE)
 314   sada razbijamo disjunkciju i dobijamo dva podcilja
 315   apply (erule disjE)
 316    apply (erule conjE) pokušavamo sa prvom ekvivalencijom 
 317    apply (erule iffE) pokušavamo sa prvom ekvivalencijom
 318 napomena: ako se negde zaglavite u dokazu, možete se vratiti na ovakva mesta i sa 
 319 back pokušati sa primenom istog pravila na neku drugu pretpostavku
 320    apply (erule impE)
 321     apply assumption
 322    apply (erule iffE)
 323    apply (erule impE) pokušavamo sa prvom implikacijom
 324     apply assumption
 325    apply (erule impE)
 326     apply assumption
 327    apply (rule conjI)
 328     apply assumption
 329    apply (erule disjE)
 330     apply (erule notE)
 331     apply assumption
 332    apply assumption
 333    sada dokazujemo drugi podcilj
 334   apply (erule conjE)
 335   apply (erule iffE) 
 336   apply (erule iffE) ako pokušamo da razbijemo prvu implikaciju dobijemo da treba 
 337                      da dokažemo @{text nA}, a u pretpostavkama već imamo @{text "¬ nA"}, 
 338                      pa je bolje da razbijemo drugu implikaciju
 339  sada pokušavamo da razbijemo drugu implikaciju
 340   apply (erule impE) back
 341    apply (rule ccontr) sada primenjujemo pravilo ccontr; kada imamo disjunkciju u 
 342                        zaključku, češto je ovo zgodno pravilo
 343    ako probamo da razbijemo prvu implikaciju, dobijamo @{text nA}, slično kao gore to 
 344    nam ne koristi
 345    ako probamo da razbijemo drugu implikaciju, dobijamo @{text nB}, slično kao malopre 
 346    to nam ne koristi jer u premisama imamo @{text "¬ nB"}; 
 347    pa pokušavamo sa trećom 
 348    sada pokušavamo da razbijemo treću implikaciju
 349    apply (erule impE) back back
 350     apply (rule notI) 
 351    sada pokušavamo da razbijemo prvu negaciju i vidimo da nam traži @{text nA} a to 
 352    ne možemo da dokažemo, pa pokušavamo sa drugom negacijom i dodajemo back; 
 353    sada vidimo da treba da dokažemo @{text nB}, što takođe ne možemo da uradimo 
 354    pa dodajemo još jedno back
 355    sada pokušavamo da razbijemo treću negaciju
 356     apply (erule notE) back back ovo je sada lako dokazati
 357     apply (rule disjI1)
 358     apply assumption sada pokušavamo da razbijemo drugu negaciju, da bi izvukli 
 359                      kontradikciju iz @{text "¬ nB"} i @{text nB}
 360    apply (erule notE) back
 361    apply assumption
 362   apply (erule notE)
 363   apply assumption
 364   done
 365 end