1 theory Cas5_vezbe_postavke 2 imports Main 3 4 begin 5 6 7 section ‹ First order logic › 8 9 subsection ‹ Ponavljanje sa predavanja › 10 11 text‹ pravilo oslobadjanja od univerzalnog kvantifikatora › 12 13 thm allE 14 15 text ‹ Ako znamo da je svaki covek smrtan, i ako je Sokrat covek, pokazati da je onda i Sokrat smrtan › 16 lemma "((∀ x. covek x ⟶ smrtan x) ∧ covek Sokrat) ⟶ smrtan Sokrat" 17 apply (rule impI) 18 apply (erule conjE) 19 (* opsti oblik nam ovde nije koristan 20 apply (erule allE) *) 21 (* pa koristimo odmah instanciranje, ako vazi za svaki onda vazi i za Sokrata 22 promenljiva se zove x u pravilu allE pa i u primeni pravila se zove x *) 23 apply (erule_tac x = "Sokrat" in allE) 24 (* rule_tac i erule_tac --- apply a rule while constraining some of its variables. The 25 typical form is rule_tac v1 = t1 and...and vk = tk in R 26 This method behaves like rule R, while instantiating the variables v1...vk 27 as specified. *) 28 apply (erule impE) (* nakon toga eliminisemo implikaciju *) 29 apply assumption 30 apply assumption 31 done 32 33 text‹ prirodnom dedukcijom dokazati da je ovo teorema logike prvog reda › 34 lemma "(∃ x. P x) ∧ (∀ x. P x ⟶ Q x) ⟶ (∃ x. Q x)" 35 (* razbijamo iskazni skeleton prvo *) 36 apply (rule impI) (* pa konjunkciju sa leve strane *) 37 apply (erule conjE) (* sada prvo eliminisemo egzistencijalni kvantifikator sa leve strane *) 38 apply (erule exE) (* i dobili smo fiksirano ali proizvoljno x, sa kojim mozemo da instanciramo 39 x u allE *) 40 apply (erule_tac x = "x" in allE) 41 apply (erule impE) 42 apply assumption (* sada se oslobadjamo egzistencijalnog kvantifikatora sa desne strane, 43 ali pokusavamo za ovo konkretno x *) 44 apply (rule_tac x = "x" in exI) 45 apply assumption 46 done 47 48 text‹ Kako bismo u Isaru dokazali istu teoremu? 49 Posto koristimo Isar, mozemo koristiti assumes shows zapis:› 50 lemma 51 assumes "∃ x. P x" 52 assumes "∀ x. P x ⟶ Q x" 53 shows "∃ x. Q x" 54 (* posto smo je zapisali sa assumes i shows, nece postojati prva dva koraka iz 55 prethodnog dokaza *) 56 proof - (* - znaci da cemo mi sami da raspisemo dokaz *) 57 (* ovde je bojama napravljena razlika *) 58 (* narandzasto x je ovo dobijeno sa exists *) 59 (* na osnovu pravila eliminacije univerzalnog kvantifikatora primenjenog na narandzasto x *) 60 from `∃ x. P x` obtain x where "P x" by auto (* ili by (rule exE), 61 ali ovde ne zelimo da budemo precizni *) 62 from `∀ x. P x ⟶ Q x` have "P x ⟶ Q x" by auto (* by (rule_tac x = "x" in allE) *) 63 from this `P x` have "Q x" by auto (* by (rule impE) *) 64 from this show "∃ x. Q x" by auto (* by (rule exI) *) 65 qed 66 67 text‹ Malo komplikovanija teorema, moze se zapisati sa jednom promenljivom x, ali citljivije je 68 ako uvedemo razlicite promenljive: c, g i a. 69 Ako je svaki covek smrtan; 70 i ako je svaki grk covek; 71 onda vazi da je svaki grk smrtan. › 72 lemma "(∀ c. covek c ⟶ smrtan c) ∧ (∀ g. grk g ⟶ covek g) ⟶ (∀ a. grk a ⟶ smrtan a)" 73 (* by auto --- prvo testiramo da vidimo da li je dobro formulisana teorema *) 74 apply (rule impI) (* standardno, prvo impI pravilo, pa nakon toga razbijamo konjunkciju sa leve strane *) 75 apply (erule conjE) (* sada uvodimo proizvoljno ali konretno a eliminacijom univerzalnog 76 kvantifikatora sa desne strane *) 77 apply (rule allI) (* sada razbijamo implikaciju sa desne strane *) 78 apply (rule impI) (* sada treba da razbijamo levu stranu i moramo da naglasimo ime promenljive *) 79 (* sada nam je dominantan univerzalni kvantifikator i razbicemo prvi kvantifikator s leva *) 80 apply (erule_tac x = "a" in allE) (* naredni korak rabija preostali kvantifikator *) 81 apply (erule_tac x = "a" in allE) 82 (* sada smo dosli do iskaznog nivoa i mozemo da razbijemo implikaciju *) 83 apply (erule impE) (* pokusamo sa prvom implikacijom... i vidimo da uspeva *) 84 apply (erule impE) 85 apply assumption 86 apply assumption 87 apply assumption 88 done 89 90 text‹ Sada ista lema u isar-u, prvo je zapisemo drugacije. 91 Proverite da je stiklirano Continuous checking sa desne strane › 92 lemma 93 assumes "∀ c. covek c ⟶ smrtan c" 94 assumes "∀ g. grk g ⟶ covek g" 95 shows "∀ a. grk a ⟶ smrtan a" 96 proof (* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali 97 proof (rule allI) *) 98 fix Jorgos 99 show "grk Jorgos ⟶ smrtan Jorgos" 100 proof (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 101 proof (rule impI) *) 102 assume "grk Jorgos" 103 from this and assms(2) have "covek Jorgos" by auto 104 from this and assms(1) show "smrtan Jorgos" by auto 105 qed 106 qed 107 108 text‹ malo duzi, drugacije zapisan dokaz› 109 lemma 110 assumes "∀ c. covek c ⟶ smrtan c" 111 assumes "∀ g. grk g ⟶ covek g" 112 shows "∀ a. grk a ⟶ smrtan a" 113 proof (* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali 114 proof (rule allI) *) 115 fix Jorgos 116 show "grk Jorgos ⟶ smrtan Jorgos" 117 proof (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 118 proof (rule impI) *) 119 assume "grk Jorgos" 120 moreover 121 from assms(2) have "grk Jorgos ⟶ covek Jorgos" by auto 122 ultimately 123 have "covek Jorgos" by auto 124 125 moreover (* novi blok, prethodno ultimately je ispraznilo *) 126 from assms(1) have "covek Jorgos ⟶ smrtan Jorgos" by auto 127 ultimately 128 show "smrtan Jorgos" by auto 129 qed 130 qed 131 132 subsection‹ Primeri za vezbanje › 133 134 text‹Naredne leme dokazati u prirodnoj dedukciji. Pa nakon toga, zapisati uz pomoc 135 assumes i shows i dokazati u Isar-u. › 136 137 (* treba raspisati oba dokaza za sve leme, ali za naredne necu pisati obe formulacije vec to 138 morate uraditi sami za vezbu *) 139 (* resenja zadataka cu okaciti za nekoliko dana *) 140 lemma "(∀ a. P a ⟶ Q a) ∧ (∀ b. P b) ⟶ (∀ x. Q x)" 141 by auto 142 143 lemma 144 assumes "∀ a. P a ⟶ Q a" 145 assumes "∀ b. P b" 146 shows "∀ x. Q x" 147 sorry 148 149 lemma "(∃ x. A x ∨ B x) ⟶ (∃ x. A x) ∨ (∃ x. B x)" 150 by auto 151 152 lemma "(∀ x. A x ⟶ ¬ B x) ⟶ ¬ (∃ x. A x ∧ B x)" 153 by auto 154 155 text ‹Narednih nekoliko primera je opisano recenicama i formulama. Na ispitu ce biti navedena 156 samo formulacija uz pomoc recenica, a zadatak ce biti i zapis uz pomoc formule i 157 raspisani dokaz same formule. Stil dokaza cete najverovatnije moci sami da birate, sem 158 ako nije eksplicitno navedeno koji tip dokaza se ocekuje. Primeticete da su ovi dokazi 159 ponekad laksi ako se koristi prirodna dedukcija nego Isar. › 160 161 text ‹ Formulisati i dokazati naredno tvrdjenje: 162 Ako za svaki broj koji nije paran vazi da je neparan; 163 i ako za svaki neparan broj vazi da nije paran; 164 pokazati da onda za svaki broj vazi da nije istovremeno i paran i neparan › 165 lemma "(∀ x. ¬ paran x ⟶ neparan x) ∧ (∀ x. neparan x ⟶ ¬ paran x) ⟶ (∀ x. ¬ (paran x ∧ neparan x))" 166 by auto 167 168 text ‹ Formulisati i dokazati naredno tvrdjenje: 169 Ako za svaki broj koji nije paran vazi da je neparan; 170 i ako za svaki neparan broj vazi da nije paran; 171 pokazati da onda za svaki broj vazi da je ili paran ili neparan 172 › 173 174 lemma "(∀ x. ¬ paran x ⟶ neparan x) ∧ (∀ x. neparan x ⟶ ¬ paran x) ⟶ (∀ x. paran x ∨ neparan x)" 175 by auto 176 177 text‹ ako svaki konj ima potkovice; 178 i ako ne postoji covek koji ima potkovice; 179 i ako znamo da postoji makar jedan covek; 180 dokazati da postoji covek koji nije konj › 181 182 lemma "(∀ x. konj x ⟶ ima_potkovice x) ∧ ¬ (∃ x. covek x ∧ ima_potkovice x) ∧ (∃ x. covek x) ⟶ 183 (∃ x. covek x ∧ ¬ konj x)" 184 by auto 185 186 text‹ ako je svaki kvadrat romb; 187 i ako je svaki kvadrat pravougaonik; 188 i ako znamo da postoji makar jedan kvadrat; 189 onda postoji makar jedan romb koji je istovremeno i pravougaonik › 190 lemma "(∀ x. kvadrat x ⟶ romb x) ∧ (∀ x. kvadrat x ⟶ pravougaonik x) ∧ (∃ x. kvadrat x) ⟶ 191 (∃ x. romb x ∧ pravougaonik x)" 192 by auto 193 194 end