1 (*:maxLineLen=80:*) 2 (* Utilities/Buffer Options/Word wrap: soft *) 3 4 section ‹ First order logic › 5 6 subsection ‹ Ponavljanje sa predavanja › 7 8 theory Cas5_vezbe_resenja 9 imports Main 10 11 begin 12 13 text‹U narednim zadacima cemo koristiti pravilo oslobadjanja od univerzalnog 14 kvantifikatora › 15 16 thm allE 17 18 text ‹ Ako znamo da je svaki covek smrtan, i ako je Sokrat covek, pokazati da je 19 onda i Sokrat smrtan › 20 lemma "((∀ x. covek x ⟶ smrtan x) ∧ covek Sokrat) ⟶ smrtan Sokrat" 21 apply (rule impI) 22 apply (erule conjE) 23 (* Opsti oblik nam ovde nije koristan apply (erule allE) pa koristimo odmah 24 instanciranje, ako vazi za svaki onda vazi i za Sokrata. Promenljiva se zove x u 25 pravilu allE pa se i u primeni pravila zove x.*) 26 apply (erule_tac x = "Sokrat" in allE) 27 (* rule_tac i erule_tac --- apply a rule while constraining some of its variables. 28 The typical form is rule_tac v1 = t1 and … and vk = tk in R. This method behaves 29 like rule R, while instantiating the variables v1…vk as specified. *) 30 (* Nakon toga eliminisemo implikaciju i jednostavno zavrsavamo dokaz. *) 31 apply (erule impE) 32 apply assumption 33 apply assumption 34 done 35 36 text‹ Prirodnom dedukcijom dokazati da je naredno tvrdjenje teorema logike prvog 37 reda: › 38 lemma "(∃ x. P x) ∧ (∀ x. P x ⟶ Q x) ⟶ (∃ x. Q x)" 39 (* Prvo razbijamo iskazni skeleton: *) 40 apply (rule impI) (* pa konjunkciju sa leve strane *) 41 apply (erule conjE) (* sada prvo eliminisemo egzistencijalni kvantifikator sa 42 leve strane *) 43 apply (erule exE) (* i dobili smo fiksirano ali proizvoljno x, sa kojim mozemo 44 da instanciramo x u allE *) 45 apply (erule_tac x = "x" in allE) 46 apply (erule impE) 47 apply assumption (* sada se oslobadjamo egzistencijalnog kvantifikatora sa desne 48 strane, ali pokusavamo za ovo konkretno x *) 49 apply (rule_tac x = "x" in exI) 50 apply assumption 51 done 52 53 text‹ Kako bismo u Isaru dokazali istu teoremu? Posto koristimo Isar, mozemo 54 koristiti assumes shows zapis:› 55 lemma 56 assumes "∃ x. P x" 57 assumes "∀ x. P x ⟶ Q x" 58 shows "∃ x. Q x" 59 (* Posto smo je zapisali sa assumes i shows, nece postojati prva dva koraka iz 60 prethodnog dokaza. *) 61 proof - 62 (* - znaci da cemo mi sami da raspisemo dokaz. Obratiti paznju da je ovde 63 bojama napravljena razlika: narandzasto x je ovo dobijeno sa exists. Naredni korak 64 mozemo da citamo: na osnovu pravila eliminacije univerzalnog kvantifikatora 65 primenjenog na narandzasto x *) 66 from `∃ x. P x` obtain x where "P x" by auto (* ili by (rule exE), 67 ali ovde ne zelimo da budemo precizni *) 68 from `∀ x. P x ⟶ Q x` have "P x ⟶ Q x" by auto (* ili by (rule_tac x = "x" in allE) *) 69 from this `P x` have "Q x" by auto (* ili by (rule impE) *) 70 from this show "∃ x. Q x" by auto (* ili by (rule exI) *) 71 qed 72 73 text‹ Malo komplikovanija teorema, moze se zapisati sa jednom promenljivom x, ali 74 citljivije je ako uvedemo razlicite promenljive: c, g i a. 75 76 Ako je svaki covek smrtan; 77 i ako je svaki grk covek; 78 onda vazi da je svaki grk smrtan. › 79 lemma "(∀ c. covek c ⟶ smrtan c) ∧ (∀ g. grk g ⟶ covek g) ⟶ (∀ a. grk a ⟶ smrtan a)" 80 (* by auto --- prvo testiramo da vidimo da li je dobro formulisana teorema *) 81 apply (rule impI) (* standardno, prvo impI pravilo, pa nakon toga razbijamo 82 konjunkciju sa leve strane *) 83 apply (erule conjE) (* sada uvodimo proizvoljno ali konretno a eliminacijom 84 univerzalnog kvantifikatora sa desne strane *) 85 apply (rule allI) (* sada razbijamo implikaciju sa desne strane *) 86 apply (rule impI) (* sada treba da razbijamo levu stranu i moramo da naglasimo 87 ime promenljive *) 88 (* sada nam je dominantan univerzalni kvantifikator i razbicemo prvi kvantifikator 89 s leva *) 90 apply (erule_tac x = "a" in allE) (* naredni korak rabija preostali kvantifikator *) 91 apply (erule_tac x = "a" in allE) 92 (* sada smo dosli do iskaznog nivoa i mozemo da razbijemo implikaciju *) 93 apply (erule impE) (* pokusamo sa prvom implikacijom... i vidimo da uspeva *) 94 apply (erule impE) 95 apply assumption 96 apply assumption 97 apply assumption 98 done 99 100 text‹ Sada ista lema u isar-u, prvo je zapisemo drugacije. Proverite da je stiklirano Continuous checking sa desne strane › 101 lemma 102 assumes "∀ c. covek c ⟶ smrtan c" 103 assumes "∀ g. grk g ⟶ covek g" 104 shows "∀ a. grk a ⟶ smrtan a" 105 proof 106 (* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali 107 proof (rule allI) *) 108 fix Jorgos 109 show "grk Jorgos ⟶ smrtan Jorgos" 110 proof (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 111 proof (rule impI) *) 112 assume "grk Jorgos" 113 from this and assms(2) have "covek Jorgos" by auto 114 from this and assms(1) show "smrtan Jorgos" by auto 115 qed 116 qed 117 118 text‹ malo duzi, drugacije zapisan dokaz› 119 lemma 120 assumes "∀ c. covek c ⟶ smrtan c" 121 assumes "∀ g. grk g ⟶ covek g" 122 shows "∀ a. grk a ⟶ smrtan a" 123 proof 124 (* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali proof (rule allI) *) 125 fix Jorgos 126 show "grk Jorgos ⟶ smrtan Jorgos" 127 proof (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 128 proof (rule impI) *) 129 assume "grk Jorgos" 130 moreover 131 from assms(2) have "grk Jorgos ⟶ covek Jorgos" by auto 132 ultimately 133 have "covek Jorgos" by auto 134 135 moreover (* novi blok, prethodno ultimately je ispraznilo *) 136 from assms(1) have "covek Jorgos ⟶ smrtan Jorgos" by auto 137 ultimately 138 show "smrtan Jorgos" by auto 139 qed 140 qed 141 142 subsection‹ Primeri za vezbanje › 143 144 text‹Naredne leme dokazati u prirodnoj dedukciji. Pa nakon toga, zapisati uz pomoc 145 assumes i shows i dokazati u Isar-u. › 146 147 lemma "(∀ a. P a ⟶ Q a) ∧ (∀ b. P b) ⟶ (∀ x. Q x)" 148 apply (rule impI) 149 apply (erule conjE) 150 apply (rule allI) 151 apply (erule_tac x = "x" in allE) 152 apply (erule_tac x = "x" in allE) 153 apply (erule impE) 154 apply assumption 155 apply assumption 156 done 157 158 lemma 159 assumes "∀ a. P a ⟶ Q a" 160 assumes "∀ b. P b" 161 shows "∀ x. Q x" 162 proof 163 fix x 164 show "Q x" 165 proof - 166 from assms(2) have "P x" by auto 167 from assms(1) have "P x ⟶ Q x" by auto 168 from this `P x` show "Q x" by auto 169 qed 170 qed 171 172 173 lemma "(∃ x. A x ∨ B x) ⟶ (∃ x. A x) ∨ (∃ x. B x)" 174 apply (rule impI) 175 apply (erule exE) (* sada prvo razbijamo pretpostavku na dve odvojene grane *) 176 apply (erule disjE) (* sada kazemo da prvo pokusavamo da dokazemo prvi disjunkt 177 u zakljucku *) 178 apply (rule disjI1) 179 apply (rule_tac x = "x" in exI) 180 apply assumption (* dokazali smo prvi podcilj, sada drugi podcilj pokusavamo 181 da dokazemo kroz drugi disjunkt *) 182 apply (rule disjI2) 183 apply (rule_tac x = "x" in exI) 184 apply assumption 185 done 186 187 text‹Da bi naredna resenja prosla ukljucujemo quick and dirty mode.› 188 declare [[quick_and_dirty=true]] 189 190 text‹Podsecanja radi, ovaj dokaz u isar-u cemo pisati u dve faze: 191 (1) prvo pravimo samo kostur dokaza, nezavrsene dokaze oznacavamo sa sorry: › 192 lemma 193 assumes "∃ x. A x ∨ B x" 194 shows "(∃ x. A x) ∨ (∃ x. B x)" 195 proof - (* ne zelimo bez crtice zato sto onda pokusava da dokaze samo prvi disjunkt, 196 a on ne mora da vazi uvek *) 197 from assms obtain x where "A x ∨ B x" by auto 198 from this show "(∃ x. A x) ∨ (∃ x. B x)" 199 proof (* sada zbog "from this" koje se odnosi na disjunkciju, dobijamo dve grane *) 200 assume "A x" 201 show "(∃ x. A x) ∨ (∃ x. B x)" 202 sorry 203 next 204 assume "B x" 205 show "(∃ x. A x) ∨ (∃ x. B x)" 206 sorry 207 qed 208 qed 209 210 text‹(2) pa sada raspisujemo jednu po jednu granu› 211 lemma 212 assumes "∃ x. A x ∨ B x" 213 shows "(∃ x. A x) ∨ (∃ x. B x)" 214 proof - (* ne zelimo bez crtice zato sto onda pokusava da dokaze samo prvi disjunkt, 215 a on ne mora da vazi uvek *) 216 from assms obtain x where "A x ∨ B x" by auto 217 from this show "(∃ x. A x) ∨ (∃ x. B x)" 218 proof (* sada zbog "from this" koje se odnosi na disjunkciju, dobijamo dve grane *) 219 assume "A x" 220 from this show "(∃ x. A x) ∨ (∃ x. B x)" by auto (* ovo bi bio najkraci dokaz *) 221 next 222 assume "B x" 223 show "(∃ x. A x) ∨ (∃ x. B x)" 224 proof - (* u drugoj grani cemo raspisati dokaz. obavezno stavljamo - posto 225 moramo sami da dodjemo do drugog disjunkta *) 226 from `B x` have "∃ x. B x" by auto 227 from this show "(∃ x. A x) ∨ (∃ x. B x)" by auto 228 qed 229 qed 230 qed 231 232 233 lemma "(∀ x. A x ⟶ ¬ B x) ⟶ ¬ (∃ x. A x ∧ B x)" 234 apply (rule impI) 235 apply (rule notI) 236 apply (erule exE) 237 apply (erule conjE) 238 apply (erule_tac x = "x" in allE) 239 apply (erule impE) 240 apply assumption 241 apply (erule notE) 242 apply assumption 243 done 244 245 text‹ (1) Skoljka automatskog dokaza › 246 lemma 247 assumes "∀ x. A x ⟶ ¬ B x" 248 shows "¬ (∃ x. A x ∧ B x)" 249 proof 250 assume "∃ x. A x ∧ B x" 251 show False 252 sorry 253 qed 254 255 text‹ (2) Raspisani dokaz › 256 lemma 257 assumes "∀ x. A x ⟶ ¬ B x" 258 shows "¬ (∃ x. A x ∧ B x)" 259 proof 260 assume "∃ x. A x ∧ B x" 261 from this obtain x where "A x ∧ B x" by auto 262 from this have "A x" "B x" by auto 263 from this have "¬ B x" using assms by auto 264 from this `B x` show False by auto 265 qed 266 267 268 text ‹Narednih nekoliko primera je opisano recenicama i formulama. Na ispitu ce 269 biti navedena samo formulacija uz pomoc recenica, a zadatak ce biti i zapis uz 270 pomoc formule i raspisani dokaz same formule. Stil dokaza cete najverovatnije 271 moci sami da birate, sem ako nije eksplicitno navedeno koji tip dokaza se ocekuje. 272 Primeticete da su ovi dokazi ponekad laksi ako se koristi prirodna dedukcija nego Isar. › 273 274 text ‹ Formulisati i dokazati naredno tvrdjenje: 275 Ako za svaki broj koji nije paran vazi da je neparan; 276 i ako za svaki neparan broj vazi da nije paran; 277 pokazati da onda za svaki broj vazi da nije istovremeno i paran i neparan › 278 279 lemma "(∀ x. ¬ paran x ⟶ neparan x) ∧ (∀ x. neparan x ⟶ ¬ paran x) 280 ⟶ (∀ x. ¬ (paran x ∧ neparan x))" 281 apply (rule impI) (* sada prvo eliminisemo univerzalni kvantifikator sa desne strane *) 282 apply (rule allI) (* pa razbijamo konjunkciju sa leve strane na dve premise *) 283 apply (erule conjE) (* pa skidamo negaciju sa desne strane tako sto prebacujemo na levu *) 284 apply (rule notI) (* pa opet konjunkciju razbijamo *) 285 apply (erule conjE) (* sada u premisama imamo dve univerzalne kvantifikovane formule, 286 koje posto vaze za svako x vazice i za ovo vec uvedeno fiksirano 287 ali proizvoljno x *) 288 apply (erule_tac x = "x" in allE) 289 apply (erule_tac x = "x" in allE) (* sada posmatranjem skupa pretpostavki vidimo da nam 290 odgovara da razbijemo drugu implikaciju (jer njenu 291 levu stranu vec imamo u pretpostavkama *) 292 apply (erule impE) 293 back 294 apply assumption 295 apply (erule notE) 296 apply assumption 297 done 298 299 text‹ (1) kostur automatskog dokaza › 300 lemma 301 assumes "∀ x. ¬ paran x ⟶ neparan x" 302 assumes "∀ x. neparan x ⟶ ¬ paran x" 303 shows "∀ x. ¬ (paran x ∧ neparan x)" 304 proof 305 fix x 306 show "¬ (paran x ∧ neparan x)" 307 sorry 308 qed 309 310 text‹ (2) naredni korak automatskog dokaza › 311 lemma 312 assumes "∀ x. ¬ paran x ⟶ neparan x" 313 assumes "∀ x. neparan x ⟶ ¬ paran x" 314 shows "∀ x. ¬ (paran x ∧ neparan x)" 315 proof 316 fix x 317 show "¬ (paran x ∧ neparan x)" 318 proof 319 assume "paran x ∧ neparan x" 320 show False 321 sorry 322 qed 323 qed 324 325 text‹ (3) raspisan dokaz › 326 lemma 327 assumes "∀ x. ¬ paran x ⟶ neparan x" 328 assumes "∀ x. neparan x ⟶ ¬ paran x" 329 shows "∀ x. ¬ (paran x ∧ neparan x)" 330 proof 331 fix x 332 show "¬ (paran x ∧ neparan x)" 333 proof 334 assume "paran x ∧ neparan x" 335 from this have "paran x" "neparan x" by auto 336 from this assms(2) have "¬ paran x" by auto 337 from this `paran x` show False by auto 338 qed 339 qed 340 341 342 text ‹ Formulisati i dokazati naredno tvrdjenje: 343 Ako za svaki broj koji nije paran vazi da je neparan; 344 i ako za svaki neparan broj vazi da nije paran; 345 pokazati da onda za svaki broj vazi da je ili paran ili neparan 346 › 347 348 lemma "(∀ x. ¬ paran x ⟶ neparan x) ∧ (∀ x. neparan x ⟶ ¬ paran x) ⟶ (∀ x. paran x ∨ neparan x)" 349 apply (rule impI) 350 apply (erule conjE) (* prvo razbijamo konjunkciju na dve pretpostavke *) 351 apply (rule allI) (* pa dva puta primenjujemo allE na obe pretpostavke *) 352 apply (erule_tac x = "x" in allE) 353 apply (erule_tac x = "x" in allE) 354 apply (rule ccontr) (* sada transformisemo stare pp *) 355 apply (erule impE) 356 apply (rule notI) 357 apply (erule notE) 358 apply (rule disjI1) 359 apply assumption 360 apply (erule impE) 361 apply assumption 362 apply (erule notE) 363 apply (rule disjI2) 364 apply assumption 365 done 366 367 368 text‹ (1) Prvi korak › 369 lemma 370 assumes "∀ x. ¬ paran x ⟶ neparan x" 371 assumes "∀ x. neparan x ⟶ ¬ paran x" 372 shows "∀ x. paran x ∨ neparan x" 373 proof 374 fix x 375 show "paran x ∨ neparan x" 376 sorry 377 qed 378 379 380 text‹ (2) Drugi korak › 381 lemma 382 assumes "∀ x. ¬ paran x ⟶ neparan x" 383 assumes "∀ x. neparan x ⟶ ¬ paran x" 384 shows "∀ x. paran x ∨ neparan x" 385 proof 386 fix x 387 have "paran x ∨ ¬ paran x" by auto (* dodajemo korak da bi napravili grananje 388 po slucajevima *) 389 from this show "paran x ∨ neparan x" (* kada stavimo from this show ... , ako 390 je this disjunkcija dobijamo automatski dve grane *) 391 proof 392 assume "paran x" 393 show "paran x ∨ neparan x" 394 sorry 395 next 396 assume "¬ paran x" 397 show "paran x ∨ neparan x" 398 sorry 399 qed 400 qed 401 402 text‹ (3) Treci korak › 403 lemma 404 assumes "∀ x. ¬ paran x ⟶ neparan x" 405 assumes "∀ x. neparan x ⟶ ¬ paran x" 406 shows "∀ x. paran x ∨ neparan x" 407 proof 408 fix x 409 have "paran x ∨ ¬ paran x" by auto (* dodajemo korak da bi napravili grananje 410 po slucajevima *) 411 from this show "paran x ∨ neparan x" (* kada stavimo from this show ... , ako je 412 this disjunkcija dobijamo automatski dve grane *) 413 proof 414 assume "paran x" 415 from this show "paran x ∨ neparan x" by auto 416 next 417 assume "¬ paran x" 418 from this have "neparan x" using assms(1) by auto 419 from this show "paran x ∨ neparan x" by auto 420 qed 421 qed 422 423 424 text‹ ako svaki konj ima potkovice; 425 i ako ne postoji covek koji ima potkovice; 426 i ako znamo da postoji makar jedan covek; 427 dokazati da postoji covek koji nije konj › 428 429 lemma "(∀ x. konj x ⟶ ima_potkovice x) ∧ ¬ (∃ x. covek x ∧ ima_potkovice x) ∧ (∃ x. covek x) 430 ⟶ (∃ x. covek x ∧ ¬ konj x)" 431 apply (rule impI) (* posto imamo tri konjunkta, konjunkciju razbijamo iz dva puta *) 432 apply (erule conjE) 433 apply (erule conjE) (* sada imamo samo jedan egzistencijalni kvantifikator u premisama, 434 i njega prvog oslobadjamo *) 435 apply (erule exE) (* sada taj novo uvedeni x koristimo u zakljucku *) 436 apply (rule_tac x = "x" in exI) (* sada razbijamo konjunkciju u zakljucku *) 437 apply (rule conjI) (* resavamo prvi podcilj *) 438 apply assumption (* sada resavamo drugi podcilj *) 439 apply (rule notI) (* sada univerzalni kvantifikator u premisama instanciramo vec uvedenim x *) 440 apply (erule_tac x = "x" in allE) (* sada se oslobadjamo implikacije u premisama *) 441 apply (erule impE) 442 apply assumption (* "ne postoji" je primarno negacija, pa moramo da se oslobadjamo nje prvo *) 443 apply (erule notE) (* sada je egzistencijalni kvantifikator presao u zakljucak i instanciramo 444 ga vec uvedenim objektom x *) 445 apply (rule_tac x = "x" in exI) 446 apply (rule conjI) 447 apply assumption 448 apply assumption 449 done 450 451 text‹ (1) kostur dokaza › 452 lemma 453 assumes "∀ x. konj x ⟶ ima_potkovice x" 454 assumes "¬ (∃ x. covek x ∧ ima_potkovice x)" 455 assumes "∃ x. covek x" 456 shows "∃ x. covek x ∧ ¬ konj x" 457 proof - 458 from assms(3) obtain x where "covek x" by auto 459 have "konj x ∨ ¬ konj x" by auto 460 from this have "covek x ∧ ¬ konj x" 461 sorry 462 from this show "∃ x. covek x ∧ ¬ konj x" by auto 463 qed 464 465 text‹ (2) naredni korak raspisan › 466 lemma 467 assumes "∀ x. konj x ⟶ ima_potkovice x" 468 assumes "¬ (∃ x. covek x ∧ ima_potkovice x)" 469 assumes "∃ x. covek x" 470 shows "∃ x. covek x ∧ ¬ konj x" 471 proof - 472 from assms(3) obtain x where "covek x" by auto 473 have "konj x ∨ ¬ konj x" by auto 474 from this have "covek x ∧ ¬ konj x" 475 proof 476 assume "konj x" 477 show "covek x ∧ ¬ konj x" 478 sorry 479 next 480 assume "¬ konj x" 481 show "covek x ∧ ¬ konj x" 482 sorry 483 qed 484 from this show "∃ x. covek x ∧ ¬ konj x" by auto 485 qed 486 487 text‹ (3) kompletan dokaz --- nije bas elegantan, bolje je koristiti prirodnu dedukciju › 488 lemma 489 assumes "∀ x. konj x ⟶ ima_potkovice x" 490 assumes "¬ (∃ x. covek x ∧ ima_potkovice x)" 491 assumes "∃ x. covek x" 492 shows "∃ x. covek x ∧ ¬ konj x" 493 proof - 494 from assms(3) obtain x where "covek x" by auto 495 have "konj x ∨ ¬ konj x" by auto 496 from this have "covek x ∧ ¬ konj x" 497 proof 498 assume "konj x" 499 show "covek x ∧ ¬ konj x" 500 proof 501 from `covek x` show "covek x" by auto 502 next 503 show "¬ konj x" 504 proof 505 assume "konj x" 506 from this assms(1) have "ima_potkovice x" by auto 507 from `covek x` this have "∃ x. covek x ∧ ima_potkovice x" by auto 508 from this assms(2) show False by auto 509 qed 510 qed 511 next 512 assume "¬ konj x" 513 from this and `covek x` 514 show "covek x ∧ ¬ konj x" by auto 515 qed 516 from this show "∃ x. covek x ∧ ¬ konj x" by auto 517 qed 518 519 520 text‹ ako je svaki kvadrat romb; 521 i ako je svaki kvadrat pravougaonik; 522 i ako znamo da postoji makar jedan kvadrat; 523 onda postoji makar jedan romb koji je istovremeno i pravougaonik › 524 lemma "(∀ x. kvadrat x ⟶ romb x) ∧ (∀ x. kvadrat x ⟶ pravougaonik x) ∧ (∃ x. kvadrat x) ⟶ 525 (∃ x. romb x ∧ pravougaonik x)" 526 apply (rule impI) 527 apply (erule conjE) 528 apply (erule conjE) 529 apply (erule exE) (* ovim se uvodi x koji je kvadrat *) 530 apply (erule_tac x = "x" in allE) 531 apply (erule_tac x = "x" in allE) 532 apply (rule_tac x = "x" in exI) 533 apply (rule conjI) 534 apply (erule impE) 535 apply assumption 536 apply assumption 537 apply (erule impE) 538 apply assumption 539 apply (erule impE) 540 apply assumption 541 apply assumption 542 done 543 544 lemma 545 assumes "∀ x. kvadrat x ⟶ romb x" 546 assumes "∀ x. kvadrat x ⟶ pravougaonik x" 547 assumes "∃ x. kvadrat x" 548 shows "∃ x. romb x ∧ pravougaonik x" 549 proof - 550 from assms(3) obtain x where "kvadrat x" by auto 551 from this assms(2) have "pravougaonik x" by auto 552 from `kvadrat x` assms(1) have "romb x" by auto 553 from this `pravougaonik x` show "∃ x. romb x ∧ pravougaonik x" by auto 554 qed 555 556 end