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