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