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 textU 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 textNaredne 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 textDa bi naredna resenja prosla ukljucujemo quick and dirty mode.
 188 declare [[quick_and_dirty=true]]
 189 
 190 textPodsecanja 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