1 theory Cas4_vezbe_resenja 2 imports Main 3 4 begin 5 6 (* Prirodna dedukcija *) 7 8 (* Introduction rules - Although we intentionally de-emphasize the basic rules 9 of logic in favour of automatic proof methods that allow you to take bigger 10 steps, these rules are helpful in locating where and why automation fails. *) 11 thm impI (* moves the left-hand side of a HOL implication into the list of assumptions *) 12 thm impE 13 thm conjI (* split the goal into two subgoals *) 14 thm conjE 15 thm disjI1 16 thm disjI2 17 thm disjE 18 thm notI 19 thm notE 20 thm iffI (* split the goal into two subgoals *) 21 thm iffE 22 thm allI (* removes a ∀ by turning the quantified variable into a fixed local 23 variable of the subgoal. *) 24 thm allE 25 26 (* Proof method invocations come in two forms: structured and unstructured. In short, 27 structured form was "by auto". Here we will use only the unstructured form, or command 28 “apply method”, which applies the proof method to the goal without insisting the proof 29 be completed; further apply commands may follow to continue the proof, until it is 30 eventually concluded by the command done (without implicit steps for closing). 31 32 After one or two apply steps, the foreseeable structure of the reasoning is usually lost, 33 and the Isar proof text degenerates into a proof script: understanding it later typically 34 requires stepping through its intermediate goal states. 35 *) 36 37 38 (* ponavljanje sa predavanja *) 39 40 lemma 41 shows "A ∧ B ⟶ B ∧ A" 42 apply (rule impI) 43 apply (erule conjE) 44 apply (rule conjI) 45 apply assumption 46 apply assumption 47 done 48 49 lemma 50 "A ∨ B ⟶ B ∨ A" 51 apply (rule impI) 52 apply (erule disjE) 53 apply (rule disjI2) 54 apply assumption 55 apply (rule disjI1) 56 apply assumption 57 done 58 59 lemma 60 "A ∧ B ⟶ A ∨ B" 61 apply (rule impI) 62 apply (erule conjE) 63 apply (rule disjI1) 64 apply assumption 65 done 66 67 68 lemma "(A ∧ B ⟶ C) ⟶ (A ⟶ (B ⟶ C))" 69 (* alternativa *) 70 (* apply rule *) 71 (* automatically selects the appropriate rule for the current subgoal. --- 72 slicno kao proof bez crtice *) 73 (* mi cemo pisati sva pravila *) 74 apply (rule impI) (* prvo razbijamo desnu stranu koliko mozemo *) 75 apply (rule impI) 76 apply (rule impI) 77 thm impE 78 apply (erule impE) (* da bi se eliminisala slozenija implikacija, treba prvo 79 dokazati da vazi pretpostavka; pa onda dokazati da vazi cilj *) 80 apply (rule conjI) (* razbijamo konjunkciju sa desne strane na dva cilja *) 81 apply assumption 82 apply assumption 83 apply assumption 84 done 85 86 lemma "(A ⟶ (B ⟶ C)) ⟶ (A ∧ B ⟶ C)" 87 apply (rule impI) 88 apply (rule impI) (* prvo razbijamo desnu stranu *) 89 apply (erule impE) (* leva strana implikacije postaje zakljucak prvog podcilja, 90 desna strana implikacije postaje pretpostavka drugog podcilja *) 91 apply (erule conjE) (* sa leve strane se koriste erule *) 92 apply assumption 93 apply (erule impE) 94 apply (erule conjE) 95 apply assumption 96 apply assumption 97 done 98 99 (* drugi nacin *) 100 lemma "(A ⟶ (B ⟶ C)) ⟶ (A ∧ B ⟶ C)" 101 apply (rule impI) 102 apply (rule impI) 103 apply (erule conjE) (* prvo mozemo da razbijemo konjunkciju *) 104 apply (erule impE) 105 apply assumption 106 apply (erule impE) 107 apply assumption 108 apply assumption 109 done 110 111 lemma 112 shows "¬ (A ∨ B) ⟶ ¬ A ∧ ¬ B" 113 apply (rule impI) 114 apply (rule conjI) 115 apply (rule notI) (* prvo razbijamo skroz desnu stranu *) 116 thm notE (* vidimo da treba da dokazemo pozitivan oblik iz preostalih pretpostavki *) 117 apply (erule notE) 118 apply (rule disjI1) 119 apply assumption 120 apply (rule notI) 121 apply (erule notE) 122 apply (erule disjI2) 123 done 124 125 (* prvi nacin *) 126 lemma 127 shows "¬ A ∧ ¬ B ⟶ ¬ (A ∨ B)" 128 apply (rule impI) 129 apply (rule notI) 130 apply (erule conjE) 131 apply (erule disjE) 132 apply (erule notE) 133 apply assumption 134 apply (erule notE) 135 apply (erule notE) 136 apply assumption 137 done 138 139 140 (* drugi nacin *) 141 lemma 142 shows "¬ A ∧ ¬ B ⟶ ¬ (A ∨ B)" 143 apply (rule impI) 144 apply (rule notI) 145 apply (erule conjE) 146 apply (erule disjE) 147 apply (erule notE) 148 apply assumption 149 apply (erule notE) (* prvo prebacuje A na desno, pa posto nam to ne odgovara koristimo back *) 150 back (* back does back-tracking over the result sequence of the latest proof 151 command. Any proof command may return multiple results, and this 152 command explores the possibilities step-by-step. *) 153 apply assumption 154 done 155 156 157 (* materijal za vezbanje: *) 158 159 lemma "(P ⟶ Q) ∧ (Q ⟶ R) ⟶ (P ⟶ Q ∧ R)" 160 apply (rule impI) 161 apply (rule impI) 162 apply (erule conjE) 163 apply (rule conjI) 164 apply (erule impE) 165 apply assumption 166 apply assumption 167 apply (erule impE) 168 apply assumption 169 apply (erule impE) 170 apply assumption 171 apply assumption 172 done 173 174 175 lemma "(P ⟶ Q) ∧ ¬ Q ⟶ ¬ P" 176 apply (rule impI) 177 apply (erule conjE) 178 apply (rule notI) 179 apply (erule impE) 180 apply assumption 181 apply (erule notE) 182 apply assumption 183 done 184 185 lemma "(P ⟶ (Q ⟶ R)) ⟶ (Q ⟶ (P ⟶ R))" 186 apply (rule impI) 187 apply (rule impI) 188 apply (rule impI) 189 apply (erule impE) 190 apply assumption 191 apply (erule impE) 192 apply assumption 193 apply assumption 194 done 195 196 197 lemma "¬ (P ∧ ¬P)" 198 apply (rule notI) 199 apply (erule conjE) 200 apply (erule notE) 201 apply assumption 202 done 203 204 205 lemma "A ∧ (B ∨ C) ⟶ (A ∧ B) ∨ (A ∧ C)" 206 apply (rule impI) 207 apply (erule conjE) 208 apply (erule disjE) 209 apply (rule disjI1) 210 apply (rule conjI) 211 apply assumption 212 apply assumption 213 apply (rule disjI2) 214 apply (rule conjI) 215 apply assumption 216 apply assumption 217 done 218 219 lemma "¬ (A ∧ B) ⟶ (A ⟶ ¬B)" 220 apply (rule impI) 221 apply (rule impI) 222 apply (rule notI) 223 apply (erule notE) 224 apply (rule conjI) 225 apply assumption 226 apply assumption 227 done 228 229 lemma "(A ⟶ C) ∧ (B ⟶ ¬ C) ⟶ ¬ (A ∧ B)" 230 apply (rule impI) 231 apply (rule notI) 232 apply (erule conjE) 233 apply (erule conjE) 234 apply (erule impE) 235 apply assumption 236 apply (erule impE) 237 apply assumption 238 apply (erule notE) 239 apply assumption 240 done 241 242 lemma "(A ∧ B) ⟶ ((A ⟶ C) ⟶ ¬ (B ⟶ ¬ C))" 243 apply (rule impI) 244 apply (rule impI) 245 apply (rule notI) 246 apply (erule conjE) 247 apply (erule impE) 248 apply assumption 249 apply (erule impE) 250 apply assumption 251 apply (erule notE) 252 apply assumption 253 done 254 255 thm iffE 256 257 lemma "¬ (A ⟷ ¬ A)" 258 apply (rule notI) 259 apply (erule iffE) (* sastoji se od dve implikacije : 260 A ⟶ ¬ A; koja se razbija na dva podcilja: 261 dokazi A i iz pp ¬ A dokazi glavni cilj 262 ¬ A ⟶ A; koja se razbija na dva podcilja: 263 dokazi ¬ A i iz pp A dokazi glavni cilj *) 264 apply (erule impE) (* kada prvi put primenimo impE eliminise se prva implikacija *) 265 (* naredni korak bi morao da bude *) 266 (* apply (erule impE) dobijamo cilj koji ne mozemo da dokazemo i moramo da se vratimo! *) 267 back (* naredba back ponistava tu eliminaciju i eliminise drugu implikaciju *) 268 apply (rule notI) (* sada skidamo negaciju sa desne strane *) 269 apply (erule impE) 270 apply assumption 271 apply (erule notE) 272 apply assumption 273 apply (erule impE) 274 apply assumption 275 apply (erule notE) 276 apply assumption 277 done 278 279 lemma "(A ⟷ B) ⟶ (¬ A ⟷ ¬ B)" 280 apply (rule impI) 281 apply (rule iffI) 282 apply (rule notI) 283 apply (erule notE) 284 apply (erule iffE) 285 apply (erule impE) 286 apply (erule impE) 287 apply assumption 288 apply assumption 289 apply (erule impE) 290 apply assumption 291 apply assumption 292 apply (rule notI) 293 apply (erule notE) 294 apply (erule iffE) 295 apply (erule impE) 296 apply assumption 297 apply assumption 298 done 299 300 (* malo kraci dokaz iste teoreme *) 301 lemma "(A ⟷ B) ⟶ (¬ A ⟷ ¬ B)" 302 apply (rule impI) 303 apply (rule iffI) 304 apply (rule notI) 305 apply (erule notE) 306 apply (erule iffE) 307 apply (erule impE) (* ako ovde uradimo back dobijamo kraci dokaz *) 308 back 309 apply assumption 310 apply assumption 311 apply (rule notI) 312 apply (erule notE) 313 apply (erule iffE) 314 apply (erule impE) 315 apply assumption 316 apply assumption 317 done 318 319 320 lemma "A ⟶ ¬ ¬ A" 321 apply (rule impI) 322 apply (rule notI) 323 apply (erule notE) 324 apply assumption 325 done 326 327 328 329 lemma "(Q ⟶ R) ∧ (R ⟶ P ∧ Q) ∧ (P ⟶ Q ∨ R) ⟶ (P ⟷ Q)" 330 apply (rule impI) 331 apply (erule conjE) 332 apply (erule conjE) 333 apply (rule iffI) (* razbijamo na dva cilja, prvi da dokazemo da vazi Q, drugi da dokazemo da vazi P *) 334 (* u premisama imamo P i P ⟶ Q ∨ R pa nam odgovara da razbijemo tu implikaciju *) 335 apply (erule impE) 336 back 337 back 338 apply assumption 339 apply (erule disjE) 340 apply assumption 341 (* u pp imamo P, R i dve implikacije, odgovara nam da razbijemo onu cije pretpostavke vec znamo, 342 odnosno drugu *) 343 apply (erule impE) 344 back 345 apply assumption 346 apply (erule conjE) 347 apply assumption (* tek sada smo dokazali da vazi Q, tj. prvi podcilj *) 348 (* sada dokazujemo drugi podcilj *) 349 (* u pp imamo Q pa nam odgovara da se razbije prva implikacija *) 350 apply (erule impE) 351 apply assumption 352 (* u pp imamo R pa nam odgovara da se razbije prva implikacija *) 353 apply (erule impE) 354 apply assumption 355 apply (erule conjE) 356 apply assumption 357 done 358 359 lemma "(A ⟶ B) ⟶ (¬ B ⟶ ¬ A)" 360 apply (rule impI) 361 apply (rule impI) 362 apply (rule notI) 363 apply (erule notE) 364 apply (erule impE) 365 apply assumption 366 apply assumption 367 done 368 369 lemma "¬ A ∨ B ⟶ (A ⟶ B)" 370 apply (rule impI) 371 apply (rule impI) 372 apply (erule disjE) 373 apply (erule notE) 374 apply assumption 375 apply assumption 376 done 377 378 379 380 end