1 theory Cas5_vezbe_postavke
   2 imports Main
   3 
   4 begin
   5 
   6 
   7 section  First order logic 
   8 
   9 subsection  Ponavljanje sa predavanja 
  10 
  11 text pravilo oslobadjanja od univerzalnog kvantifikatora 
  12 
  13 thm allE
  14 
  15 text  Ako znamo da je svaki covek smrtan, i ako je Sokrat covek, pokazati da je onda i Sokrat smrtan 
  16 lemma "((∀ x. covek x ⟶ smrtan x) ∧ covek Sokrat) ⟶ smrtan Sokrat"
  17   apply (rule impI)
  18   apply (erule conjE)
  19 (* opsti oblik nam ovde nije koristan 
  20   apply (erule allE) *)
  21 (*  pa koristimo odmah instanciranje, ako vazi za svaki onda vazi i za Sokrata 
  22     promenljiva se zove x u pravilu allE pa i u primeni pravila se zove x *)
  23   apply (erule_tac x = "Sokrat" in allE)
  24 (* rule_tac i erule_tac --- apply a rule while constraining some of its variables. The
  25 typical form is rule_tac v1 = t1 and...and vk = tk in R
  26 This method behaves like rule R, while instantiating the variables v1...vk
  27 as specified. *)
  28   apply (erule impE) (* nakon toga eliminisemo implikaciju *)
  29    apply assumption
  30   apply assumption
  31   done
  32 
  33 text prirodnom dedukcijom dokazati da je ovo teorema logike prvog reda 
  34 lemma "(∃ x. P x) ∧ (∀ x. P x ⟶ Q x) ⟶ (∃ x. Q x)"
  35 (* razbijamo iskazni skeleton prvo *)
  36   apply (rule impI) (* pa konjunkciju sa leve strane *)
  37   apply (erule conjE) (* sada prvo eliminisemo egzistencijalni kvantifikator sa leve strane *)
  38   apply (erule exE) (* i dobili smo fiksirano ali proizvoljno x, sa kojim mozemo da instanciramo 
  39                        x u allE *)
  40   apply (erule_tac x = "x" in allE) 
  41   apply (erule impE)
  42   apply assumption (* sada se oslobadjamo egzistencijalnog kvantifikatora sa desne strane, 
  43                       ali pokusavamo za ovo konkretno x *)
  44   apply (rule_tac x = "x" in exI)
  45   apply assumption
  46   done
  47 
  48 text Kako bismo u Isaru dokazali istu teoremu?
  49    Posto koristimo Isar, mozemo koristiti assumes shows zapis:
  50 lemma 
  51   assumes "∃ x. P x"
  52   assumes "∀ x. P x ⟶ Q x"
  53   shows "∃ x. Q x"
  54 (* posto smo je zapisali sa assumes i shows, nece postojati prva dva koraka iz 
  55    prethodnog dokaza *)
  56 proof - (* - znaci da cemo mi sami da raspisemo dokaz *)
  57   (* ovde je bojama napravljena razlika *)
  58   (* narandzasto x je ovo dobijeno sa exists *)
  59   (* na osnovu pravila eliminacije univerzalnog kvantifikatora primenjenog na narandzasto x *)
  60   from `∃ x. P x` obtain x where "P x" by auto (* ili by (rule exE), 
  61                                                   ali ovde ne zelimo da budemo precizni *)
  62   from `∀ x. P x ⟶ Q x` have "P x ⟶ Q x" by auto (* by (rule_tac x = "x" in allE) *)
  63   from this `P x` have "Q x" by auto (* by (rule impE) *)
  64   from this show "∃ x. Q x" by auto (* by (rule exI) *)
  65 qed
  66 
  67 text Malo komplikovanija teorema, moze se zapisati sa jednom promenljivom x, ali citljivije je 
  68    ako uvedemo razlicite promenljive: c, g i a.
  69    Ako je svaki covek smrtan; 
  70    i ako je svaki grk covek; 
  71    onda vazi da je svaki grk smrtan. 
  72 lemma "(∀ c. covek c ⟶ smrtan c) ∧ (∀ g. grk g ⟶ covek g) ⟶ (∀ a. grk a ⟶ smrtan a)"
  73 (* by auto --- prvo testiramo da vidimo da li je dobro formulisana teorema *)
  74   apply (rule impI) (* standardno, prvo impI pravilo, pa nakon toga razbijamo konjunkciju sa leve strane *)
  75   apply (erule conjE) (* sada uvodimo proizvoljno ali konretno a eliminacijom univerzalnog 
  76                          kvantifikatora sa desne strane *) 
  77   apply (rule allI) (* sada razbijamo implikaciju sa desne strane *)
  78   apply (rule impI) (* sada treba da razbijamo levu stranu i moramo da naglasimo ime promenljive *)
  79   (* sada nam je dominantan univerzalni kvantifikator i razbicemo prvi kvantifikator s leva *)
  80   apply (erule_tac x = "a" in allE) (* naredni korak rabija preostali kvantifikator *)
  81   apply (erule_tac x = "a" in allE) 
  82   (* sada smo dosli do iskaznog nivoa i mozemo da razbijemo implikaciju *)
  83   apply (erule impE) (* pokusamo sa prvom implikacijom... i vidimo da uspeva *)
  84    apply (erule impE)
  85     apply assumption
  86    apply assumption 
  87    apply assumption
  88   done
  89 
  90 text Sada ista lema u isar-u, prvo je zapisemo drugacije. 
  91 Proverite da je stiklirano Continuous checking sa desne strane 
  92 lemma
  93   assumes "∀ c. covek c ⟶ smrtan c"
  94   assumes "∀ g. grk g ⟶ covek g"
  95   shows "∀ a. grk a ⟶ smrtan a"
  96 proof (* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali 
  97          proof (rule allI) *)
  98   fix Jorgos
  99   show "grk Jorgos ⟶ smrtan Jorgos"
 100   proof  (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 
 101             proof (rule impI) *)
 102     assume "grk Jorgos" 
 103     from this and assms(2) have "covek Jorgos" by auto
 104     from this and assms(1) show "smrtan Jorgos" by auto
 105   qed
 106 qed
 107 
 108 text malo duzi, drugacije zapisan dokaz
 109 lemma 
 110   assumes "∀ c. covek c ⟶ smrtan c"
 111   assumes "∀ g. grk g ⟶ covek g"
 112   shows "∀ a. grk a ⟶ smrtan a"
 113 proof (* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali 
 114          proof (rule allI) *)
 115   fix Jorgos
 116   show "grk Jorgos ⟶ smrtan Jorgos"
 117   proof  (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 
 118             proof (rule impI) *)
 119     assume "grk Jorgos" 
 120     moreover
 121     from assms(2) have "grk Jorgos ⟶ covek Jorgos" by auto
 122     ultimately 
 123     have "covek Jorgos" by auto
 124 
 125     moreover (* novi blok, prethodno ultimately je ispraznilo *)
 126     from assms(1) have "covek Jorgos ⟶ smrtan Jorgos" by auto
 127     ultimately 
 128     show "smrtan Jorgos" by auto
 129   qed
 130 qed
 131 
 132 subsection Primeri za vezbanje 
 133 
 134 textNaredne leme dokazati u prirodnoj dedukciji. Pa nakon toga, zapisati uz pomoc 
 135 assumes i shows i dokazati u Isar-u. 
 136 
 137 (* treba raspisati oba dokaza za sve leme, ali za naredne necu pisati obe formulacije vec to 
 138    morate uraditi sami za vezbu *)
 139 (* resenja zadataka cu okaciti za nekoliko dana *)
 140 lemma "(∀ a. P a ⟶ Q a) ∧ (∀ b. P b) ⟶ (∀ x. Q x)"
 141   by auto
 142 
 143 lemma 
 144   assumes "∀ a. P a ⟶ Q a"
 145   assumes "∀ b. P b"
 146   shows "∀ x. Q x"
 147   sorry
 148 
 149 lemma "(∃ x. A x ∨ B x) ⟶ (∃ x. A x) ∨ (∃ x. B x)"
 150   by auto
 151 
 152 lemma "(∀ x. A x ⟶ ¬ B x) ⟶ ¬ (∃ x. A x ∧ B x)"
 153   by auto
 154 
 155 text Narednih nekoliko primera je opisano recenicama i formulama. Na ispitu ce biti navedena 
 156       samo formulacija uz pomoc recenica, a zadatak ce biti i zapis uz pomoc formule i 
 157       raspisani dokaz same formule. Stil dokaza cete najverovatnije moci sami da birate, sem 
 158       ako nije eksplicitno navedeno koji tip dokaza se ocekuje. Primeticete da su ovi dokazi 
 159       ponekad laksi ako se koristi prirodna dedukcija nego Isar. 
 160 
 161 text  Formulisati i dokazati naredno tvrdjenje:
 162    Ako za svaki broj koji nije paran vazi da je neparan; 
 163    i ako za svaki neparan broj vazi da nije paran; 
 164    pokazati da onda za svaki broj vazi da nije istovremeno i paran i neparan 
 165 lemma "(∀ x. ¬ paran x ⟶ neparan x) ∧ (∀ x. neparan x ⟶ ¬ paran x) ⟶ (∀ x. ¬ (paran x ∧ neparan x))"
 166   by auto
 167 
 168 text  Formulisati i dokazati naredno tvrdjenje:
 169    Ako za svaki broj koji nije paran vazi da je neparan; 
 170    i ako za svaki neparan broj vazi da nije paran; 
 171    pokazati da onda za svaki broj vazi da je ili paran ili neparan
 172 
 173 
 174 lemma "(∀ x. ¬ paran x ⟶ neparan x) ∧ (∀ x. neparan x ⟶ ¬ paran x) ⟶ (∀ x. paran x ∨ neparan x)"
 175   by auto
 176 
 177 text ako svaki konj ima potkovice; 
 178    i ako ne postoji covek koji ima potkovice; 
 179    i ako znamo da postoji  makar jedan covek; 
 180    dokazati da postoji covek koji nije konj 
 181 
 182 lemma "(∀ x. konj x ⟶ ima_potkovice x) ∧ ¬ (∃ x. covek x ∧ ima_potkovice x) ∧ (∃ x. covek x) ⟶ 
 183 (∃ x. covek x ∧ ¬ konj x)" 
 184   by auto
 185 
 186 text ako je svaki kvadrat romb; 
 187    i ako je svaki kvadrat pravougaonik; 
 188    i ako znamo da postoji makar jedan kvadrat;
 189    onda postoji makar jedan romb koji je istovremeno i pravougaonik 
 190 lemma "(∀ x. kvadrat x ⟶ romb x) ∧ (∀ x. kvadrat x ⟶ pravougaonik x) ∧ (∃ x. kvadrat x) ⟶ 
 191        (∃ x. romb x ∧ pravougaonik x)" 
 192   by auto
 193 
 194 end