1 theory Cas4_vezbe_postavke
   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   sorry
 161 
 162 lemma "(P ⟶ Q) ∧ ¬ Q ⟶ ¬ P"
 163   sorry
 164 
 165 lemma "(P ⟶ (Q ⟶ R)) ⟶ (Q ⟶ (P ⟶ R))"
 166   sorry
 167 
 168 lemma "¬ (P ∧ ¬P)"
 169   sorry
 170 
 171 lemma "A ∧ (B ∨ C) ⟶ (A ∧ B) ∨ (A ∧ C)"
 172   sorry
 173 
 174 lemma "¬ (A ∧ B) ⟶ (A ⟶ ¬B)"
 175   sorry
 176 
 177 lemma "(A ⟶ C) ∧ (B ⟶ ¬ C) ⟶ ¬ (A ∧ B)"
 178   sorry
 179 
 180 lemma "(A ∧ B) ⟶ ((A ⟶ C) ⟶ ¬ (B ⟶ ¬ C))"
 181   sorry
 182 
 183 thm iffE
 184 
 185 lemma "¬ (A ⟷ ¬ A)"
 186   sorry
 187 
 188 lemma "(A ⟷ B) ⟶ (¬ A ⟷ ¬ B)"
 189   sorry
 190 
 191 lemma "A ⟶ ¬ ¬ A"
 192   sorry
 193 
 194 lemma "(Q ⟶ R) ∧ (R ⟶ P ∧ Q) ∧ (P ⟶ Q ∨ R) ⟶ (P ⟷ Q)"
 195   sorry
 196 
 197 lemma "(A ⟶ B) ⟶ (¬ B ⟶ ¬ A)"
 198   sorry
 199 
 200 lemma "¬ A ∨ B ⟶ (A ⟶ B)"
 201   sorry
 202 
 203 end