theory Cas4_vezbe_resenja imports Main begin (* Prirodna dedukcija *) (* Introduction rules - Although we intentionally de-emphasize the basic rules of logic in favour of automatic proof methods that allow you to take bigger steps, these rules are helpful in locating where and why automation fails. *) thm impI (* moves the left-hand side of a HOL implication into the list of assumptions *) thm impE thm conjI (* split the goal into two subgoals *) thm conjE thm disjI1 thm disjI2 thm disjE thm notI thm notE thm iffI (* split the goal into two subgoals *) thm iffE thm allI (* removes a \ by turning the quantified variable into a fixed local variable of the subgoal. *) thm allE (* Proof method invocations come in two forms: structured and unstructured. In short, structured form was "by auto". Here we will use only the unstructured form, or command “apply method”, which applies the proof method to the goal without insisting the proof be completed; further apply commands may follow to continue the proof, until it is eventually concluded by the command done (without implicit steps for closing). After one or two apply steps, the foreseeable structure of the reasoning is usually lost, and the Isar proof text degenerates into a proof script: understanding it later typically requires stepping through its intermediate goal states. *) (* ponavljanje sa predavanja *) lemma shows "A \ B \ B \ A" apply (rule impI) apply (erule conjE) apply (rule conjI) apply assumption apply assumption done lemma "A \ B \ B \ A" apply (rule impI) apply (erule disjE) apply (rule disjI2) apply assumption apply (rule disjI1) apply assumption done lemma "A \ B \ A \ B" apply (rule impI) apply (erule conjE) apply (rule disjI1) apply assumption done lemma "(A \ B \ C) \ (A \ (B \ C))" (* alternativa *) (* apply rule *) (* automatically selects the appropriate rule for the current subgoal. --- slicno kao proof bez crtice *) (* mi cemo pisati sva pravila *) apply (rule impI) (* prvo razbijamo desnu stranu koliko mozemo *) apply (rule impI) apply (rule impI) thm impE apply (erule impE) (* da bi se eliminisala slozenija implikacija, treba prvo dokazati da vazi pretpostavka; pa onda dokazati da vazi cilj *) apply (rule conjI) (* razbijamo konjunkciju sa desne strane na dva cilja *) apply assumption apply assumption apply assumption done lemma "(A \ (B \ C)) \ (A \ B \ C)" apply (rule impI) apply (rule impI) (* prvo razbijamo desnu stranu *) apply (erule impE) (* leva strana implikacije postaje zakljucak prvog podcilja, desna strana implikacije postaje pretpostavka drugog podcilja *) apply (erule conjE) (* sa leve strane se koriste erule *) apply assumption apply (erule impE) apply (erule conjE) apply assumption apply assumption done (* drugi nacin *) lemma "(A \ (B \ C)) \ (A \ B \ C)" apply (rule impI) apply (rule impI) apply (erule conjE) (* prvo mozemo da razbijemo konjunkciju *) apply (erule impE) apply assumption apply (erule impE) apply assumption apply assumption done lemma shows "\ (A \ B) \ \ A \ \ B" apply (rule impI) apply (rule conjI) apply (rule notI) (* prvo razbijamo skroz desnu stranu *) thm notE (* vidimo da treba da dokazemo pozitivan oblik iz preostalih pretpostavki *) apply (erule notE) apply (rule disjI1) apply assumption apply (rule notI) apply (erule notE) apply (erule disjI2) done (* prvi nacin *) lemma shows "\ A \ \ B \ \ (A \ B)" apply (rule impI) apply (rule notI) apply (erule conjE) apply (erule disjE) apply (erule notE) apply assumption apply (erule notE) apply (erule notE) apply assumption done (* drugi nacin *) lemma shows "\ A \ \ B \ \ (A \ B)" apply (rule impI) apply (rule notI) apply (erule conjE) apply (erule disjE) apply (erule notE) apply assumption apply (erule notE) (* prvo prebacuje A na desno, pa posto nam to ne odgovara koristimo back *) back (* back does back-tracking over the result sequence of the latest proof command. Any proof command may return multiple results, and this command explores the possibilities step-by-step. *) apply assumption done (* materijal za vezbanje: *) lemma "(P \ Q) \ (Q \ R) \ (P \ Q \ R)" apply (rule impI) apply (rule impI) apply (erule conjE) apply (rule conjI) apply (erule impE) apply assumption apply assumption apply (erule impE) apply assumption apply (erule impE) apply assumption apply assumption done lemma "(P \ Q) \ \ Q \ \ P" apply (rule impI) apply (erule conjE) apply (rule notI) apply (erule impE) apply assumption apply (erule notE) apply assumption done lemma "(P \ (Q \ R)) \ (Q \ (P \ R))" apply (rule impI) apply (rule impI) apply (rule impI) apply (erule impE) apply assumption apply (erule impE) apply assumption apply assumption done lemma "\ (P \ \P)" apply (rule notI) apply (erule conjE) apply (erule notE) apply assumption done lemma "A \ (B \ C) \ (A \ B) \ (A \ C)" apply (rule impI) apply (erule conjE) apply (erule disjE) apply (rule disjI1) apply (rule conjI) apply assumption apply assumption apply (rule disjI2) apply (rule conjI) apply assumption apply assumption done lemma "\ (A \ B) \ (A \ \B)" apply (rule impI) apply (rule impI) apply (rule notI) apply (erule notE) apply (rule conjI) apply assumption apply assumption done lemma "(A \ C) \ (B \ \ C) \ \ (A \ B)" apply (rule impI) apply (rule notI) apply (erule conjE) apply (erule conjE) apply (erule impE) apply assumption apply (erule impE) apply assumption apply (erule notE) apply assumption done lemma "(A \ B) \ ((A \ C) \ \ (B \ \ C))" apply (rule impI) apply (rule impI) apply (rule notI) apply (erule conjE) apply (erule impE) apply assumption apply (erule impE) apply assumption apply (erule notE) apply assumption done thm iffE lemma "\ (A \ \ A)" apply (rule notI) apply (erule iffE) (* sastoji se od dve implikacije : A \ \ A; koja se razbija na dva podcilja: dokazi A i iz pp \ A dokazi glavni cilj \ A \ A; koja se razbija na dva podcilja: dokazi \ A i iz pp A dokazi glavni cilj *) apply (erule impE) (* kada prvi put primenimo impE eliminise se prva implikacija *) (* naredni korak bi morao da bude *) (* apply (erule impE) dobijamo cilj koji ne mozemo da dokazemo i moramo da se vratimo! *) back (* naredba back ponistava tu eliminaciju i eliminise drugu implikaciju *) apply (rule notI) (* sada skidamo negaciju sa desne strane *) apply (erule impE) apply assumption apply (erule notE) apply assumption apply (erule impE) apply assumption apply (erule notE) apply assumption done lemma "(A \ B) \ (\ A \ \ B)" apply (rule impI) apply (rule iffI) apply (rule notI) apply (erule notE) apply (erule iffE) apply (erule impE) apply (erule impE) apply assumption apply assumption apply (erule impE) apply assumption apply assumption apply (rule notI) apply (erule notE) apply (erule iffE) apply (erule impE) apply assumption apply assumption done (* malo kraci dokaz iste teoreme *) lemma "(A \ B) \ (\ A \ \ B)" apply (rule impI) apply (rule iffI) apply (rule notI) apply (erule notE) apply (erule iffE) apply (erule impE) (* ako ovde uradimo back dobijamo kraci dokaz *) back apply assumption apply assumption apply (rule notI) apply (erule notE) apply (erule iffE) apply (erule impE) apply assumption apply assumption done lemma "A \ \ \ A" apply (rule impI) apply (rule notI) apply (erule notE) apply assumption done lemma "(Q \ R) \ (R \ P \ Q) \ (P \ Q \ R) \ (P \ Q)" apply (rule impI) apply (erule conjE) apply (erule conjE) apply (rule iffI) (* razbijamo na dva cilja, prvi da dokazemo da vazi Q, drugi da dokazemo da vazi P *) (* u premisama imamo P i P \ Q \ R pa nam odgovara da razbijemo tu implikaciju *) apply (erule impE) back back apply assumption apply (erule disjE) apply assumption (* u pp imamo P, R i dve implikacije, odgovara nam da razbijemo onu cije pretpostavke vec znamo, odnosno drugu *) apply (erule impE) back apply assumption apply (erule conjE) apply assumption (* tek sada smo dokazali da vazi Q, tj. prvi podcilj *) (* sada dokazujemo drugi podcilj *) (* u pp imamo Q pa nam odgovara da se razbije prva implikacija *) apply (erule impE) apply assumption (* u pp imamo R pa nam odgovara da se razbije prva implikacija *) apply (erule impE) apply assumption apply (erule conjE) apply assumption done lemma "(A \ B) \ (\ B \ \ A)" apply (rule impI) apply (rule impI) apply (rule notI) apply (erule notE) apply (erule impE) apply assumption apply assumption done lemma "\ A \ B \ (A \ B)" apply (rule impI) apply (rule impI) apply (erule disjE) apply (erule notE) apply assumption apply assumption done end