(*:maxLineLen=80:*)
(* Utilities/Buffer Options/Word wrap: soft *)

section \<open> First order logic \<close>

subsection \<open> Ponavljanje sa predavanja \<close>

theory Cas5_vezbe_resenja
imports Main

begin

text\<open>U narednim zadacima cemo koristiti pravilo oslobadjanja od univerzalnog
kvantifikatora \<close>

thm allE

text \<open> Ako znamo da je svaki covek smrtan, i ako je Sokrat covek, pokazati da je 
onda i Sokrat smrtan \<close>
lemma "((\<forall> x. covek x \<longrightarrow> smrtan x) \<and> covek Sokrat) \<longrightarrow> smrtan Sokrat"
  apply (rule impI)
  apply (erule conjE)
(* Opsti oblik nam ovde nije koristan apply (erule allE) pa koristimo odmah 
instanciranje, ako vazi za svaki onda vazi i za Sokrata. Promenljiva se zove x u 
pravilu allE pa se i u primeni pravila zove x.*)
  apply (erule_tac x = "Sokrat" in allE)
(* rule_tac i  erule_tac --- apply a rule while constraining some of its variables. 
The typical form is rule_tac v1 = t1 and \<dots> and vk = tk in R. This method behaves 
like rule R, while instantiating the variables v1\<dots>vk as specified. *)
(* Nakon toga eliminisemo implikaciju i jednostavno zavrsavamo dokaz. *)
  apply (erule impE) 
   apply assumption
  apply assumption
  done

text\<open> Prirodnom dedukcijom dokazati da je naredno tvrdjenje teorema logike prvog 
reda: \<close>
lemma "(\<exists> x. P x) \<and> (\<forall> x. P x \<longrightarrow> Q x) \<longrightarrow> (\<exists> x. Q x)"
(* Prvo razbijamo iskazni skeleton: *)
  apply (rule impI) (* pa konjunkciju sa leve strane *)
  apply (erule conjE) (* sada prvo eliminisemo egzistencijalni kvantifikator sa 
                         leve strane *)
  apply (erule exE) (* i dobili smo fiksirano ali proizvoljno x, sa kojim mozemo 
                       da instanciramo x u allE *)
  apply (erule_tac x = "x" in allE) 
  apply (erule impE)
   apply assumption (* sada se oslobadjamo egzistencijalnog kvantifikatora sa desne 
                       strane, ali pokusavamo za ovo konkretno x *)
  apply (rule_tac x = "x" in exI)
  apply assumption
  done

text\<open> Kako bismo u Isaru dokazali istu teoremu? Posto koristimo Isar, mozemo 
koristiti assumes shows zapis:\<close>
lemma 
  assumes "\<exists> x. P x"
  assumes "\<forall> x. P x \<longrightarrow> Q x"
  shows "\<exists> x. Q x"
(* Posto smo je zapisali sa assumes i shows, nece postojati prva dva koraka iz 
prethodnog dokaza. *)
proof - 
(* - znaci da cemo mi sami da raspisemo dokaz. Obratiti paznju da je ovde 
bojama napravljena razlika: narandzasto x je ovo dobijeno sa exists. Naredni korak 
mozemo da citamo: na osnovu pravila eliminacije univerzalnog kvantifikatora 
primenjenog na narandzasto x *)
  from `\<exists> x. P x` obtain x where "P x" by auto (* ili by (rule exE), 
                                                  ali ovde ne zelimo da budemo precizni *)
  from `\<forall> x. P x \<longrightarrow> Q x` have "P x \<longrightarrow> Q x" by auto (* ili by (rule_tac x = "x" in allE) *)
  from this `P x` have "Q x" by auto (* ili by (rule impE) *)
  from this show "\<exists> x. Q x" by auto (* ili by (rule exI) *)
qed

text\<open> Malo komplikovanija teorema, moze se zapisati sa jednom promenljivom x, ali 
citljivije je ako uvedemo razlicite promenljive: c, g i a.

   Ako je svaki covek smrtan; 
   i ako je svaki grk covek; 
   onda vazi da je svaki grk smrtan. \<close>
lemma "(\<forall> c. covek c \<longrightarrow> smrtan c) \<and> (\<forall> g. grk g \<longrightarrow> covek g) \<longrightarrow> (\<forall> a. grk a \<longrightarrow> smrtan a)"
(* by auto --- prvo testiramo da vidimo da li je dobro formulisana teorema *)
  apply (rule impI) (* standardno, prvo impI pravilo, pa nakon toga razbijamo 
                       konjunkciju sa leve strane *)
  apply (erule conjE) (* sada uvodimo proizvoljno ali konretno a eliminacijom 
                         univerzalnog kvantifikatora sa desne strane *)
  apply (rule allI) (* sada razbijamo implikaciju sa desne strane *)
  apply (rule impI) (* sada treba da razbijamo levu stranu i moramo da naglasimo 
                       ime promenljive *)
  (* sada nam je dominantan univerzalni kvantifikator i razbicemo prvi kvantifikator 
     s leva *)
  apply (erule_tac x = "a" in allE) (* naredni korak rabija preostali kvantifikator *)
  apply (erule_tac x = "a" in allE) 
  (* sada smo dosli do iskaznog nivoa i mozemo da razbijemo implikaciju *)
  apply (erule impE) (* pokusamo sa prvom implikacijom... i vidimo da uspeva *)
   apply (erule impE)
    apply assumption
   apply assumption 
   apply assumption
  done

text\<open> Sada ista lema u isar-u, prvo je zapisemo drugacije. Proverite da je stiklirano Continuous checking sa desne strane \<close>
lemma
  assumes "\<forall> c. covek c \<longrightarrow> smrtan c"
  assumes "\<forall> g. grk g \<longrightarrow> covek g"
  shows "\<forall> a. grk a \<longrightarrow> smrtan a"
proof 
(* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali 
   proof (rule allI) *)
  fix Jorgos
  show "grk Jorgos \<longrightarrow> smrtan Jorgos"
  proof  (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 
            proof (rule impI) *)
    assume "grk Jorgos" 
    from this and assms(2) have "covek Jorgos" by auto
    from this and assms(1) show "smrtan Jorgos" by auto
  qed
qed

text\<open> malo duzi, drugacije zapisan dokaz\<close>
lemma 
  assumes "\<forall> c. covek c \<longrightarrow> smrtan c"
  assumes "\<forall> g. grk g \<longrightarrow> covek g"
  shows "\<forall> a. grk a \<longrightarrow> smrtan a"
proof 
(* sam isabelle sugerise uvodjenje proizvoljnog a, isto kao da smo napisali proof (rule allI) *)
  fix Jorgos
  show "grk Jorgos \<longrightarrow> smrtan Jorgos"
  proof  (* opet isabelle sugerise i nadje impI --- isto kao da smo napisali 
            proof (rule impI) *)
    assume "grk Jorgos" 
    moreover
    from assms(2) have "grk Jorgos \<longrightarrow> covek Jorgos" by auto
    ultimately 
    have "covek Jorgos" by auto

    moreover (* novi blok, prethodno ultimately je ispraznilo *)
    from assms(1) have "covek Jorgos \<longrightarrow> smrtan Jorgos" by auto
    ultimately 
    show "smrtan Jorgos" by auto
  qed
qed

subsection\<open> Primeri za vezbanje \<close>

text\<open>Naredne leme dokazati u prirodnoj dedukciji. Pa nakon toga, zapisati uz pomoc 
assumes i shows i dokazati u Isar-u. \<close>

lemma "(\<forall> a. P a \<longrightarrow> Q a) \<and> (\<forall> b. P b) \<longrightarrow> (\<forall> x. Q x)"
  apply (rule impI)
  apply (erule conjE)
  apply (rule allI)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "x" in allE)
  apply (erule impE)
   apply assumption
  apply assumption
  done

lemma 
  assumes "\<forall> a. P a \<longrightarrow> Q a"
  assumes "\<forall> b. P b"
  shows "\<forall> x. Q x"
proof
  fix x
  show "Q x"
  proof - 
    from assms(2) have "P x" by auto
    from assms(1) have "P x \<longrightarrow> Q x" by auto
    from this `P x` show "Q x" by auto
  qed
qed


lemma "(\<exists> x. A x \<or> B x) \<longrightarrow> (\<exists> x. A x) \<or> (\<exists> x. B x)"
  apply (rule impI)
  apply (erule exE) (* sada prvo razbijamo pretpostavku na dve odvojene grane *)
  apply (erule disjE) (* sada kazemo da prvo pokusavamo da dokazemo prvi disjunkt 
                         u zakljucku *)
   apply (rule disjI1)
   apply (rule_tac x = "x" in exI)
   apply assumption (* dokazali smo prvi podcilj, sada drugi podcilj pokusavamo 
                       da dokazemo kroz drugi disjunkt *)
  apply (rule disjI2) 
  apply (rule_tac x = "x" in exI)
  apply assumption
  done

text\<open>Da bi naredna resenja prosla ukljucujemo quick and dirty mode.\<close>
declare [[quick_and_dirty=true]]

text\<open>Podsecanja radi, ovaj dokaz u isar-u cemo pisati u dve faze:
(1) prvo pravimo samo kostur dokaza, nezavrsene dokaze oznacavamo sa sorry: \<close>
lemma
  assumes "\<exists> x. A x \<or> B x"
  shows "(\<exists> x. A x) \<or> (\<exists> x. B x)"
proof - (* ne zelimo bez crtice zato sto onda pokusava da dokaze samo prvi disjunkt, 
           a on ne mora da vazi uvek *)
  from assms obtain x where "A x \<or> B x" by auto
  from this show "(\<exists> x. A x) \<or> (\<exists> x. B x)" 
  proof (* sada zbog "from this" koje se odnosi na disjunkciju, dobijamo dve grane *)
    assume "A x" 
    show "(\<exists> x. A x) \<or> (\<exists> x. B x)"
      sorry
  next
    assume "B x"
    show "(\<exists> x. A x) \<or> (\<exists> x. B x)"
      sorry
  qed
qed

text\<open>(2) pa sada raspisujemo jednu po jednu granu\<close>
lemma
  assumes "\<exists> x. A x \<or> B x"
  shows "(\<exists> x. A x) \<or> (\<exists> x. B x)"
proof - (* ne zelimo bez crtice zato sto onda pokusava da dokaze samo prvi disjunkt, 
           a on ne mora da vazi uvek *)
  from assms obtain x where "A x \<or> B x" by auto
  from this show "(\<exists> x. A x) \<or> (\<exists> x. B x)" 
  proof (* sada zbog "from this" koje se odnosi na disjunkciju, dobijamo dve grane *)
    assume "A x" 
    from this show "(\<exists> x. A x) \<or> (\<exists> x. B x)" by auto (* ovo bi bio najkraci dokaz *)
  next
    assume "B x"
    show "(\<exists> x. A x) \<or> (\<exists> x. B x)"
    proof - (* u drugoj grani cemo raspisati dokaz. obavezno stavljamo - posto 
               moramo sami da dodjemo do drugog disjunkta *)
      from `B x` have "\<exists> x. B x" by auto
      from this show "(\<exists> x. A x) \<or> (\<exists> x. B x)" by auto
    qed
  qed
qed


lemma "(\<forall> x. A x \<longrightarrow> \<not> B x) \<longrightarrow> \<not> (\<exists> x. A x \<and> B x)"
  apply (rule impI)
  apply (rule notI)
  apply (erule exE)
  apply (erule conjE)
  apply (erule_tac x = "x" in allE)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text\<open> (1) Skoljka automatskog dokaza \<close>
lemma 
  assumes "\<forall> x. A x \<longrightarrow> \<not> B x"
  shows "\<not> (\<exists> x. A x \<and> B x)"
proof 
  assume "\<exists> x. A x \<and> B x"
  show False
    sorry
qed

text\<open> (2) Raspisani dokaz \<close>
lemma 
  assumes "\<forall> x. A x \<longrightarrow> \<not> B x"
  shows "\<not> (\<exists> x. A x \<and> B x)"
proof 
  assume "\<exists> x. A x \<and> B x"
  from this obtain x where "A x \<and> B x" by auto
  from this have "A x" "B x" by auto
  from this have "\<not> B x" using assms by auto
  from this `B x` show False by auto
qed


text \<open>Narednih nekoliko primera je opisano recenicama i formulama. Na ispitu ce 
biti navedena samo formulacija uz pomoc recenica, a zadatak ce biti i zapis uz 
pomoc formule i raspisani dokaz same formule. Stil dokaza cete najverovatnije 
moci sami da birate, sem ako nije eksplicitno navedeno koji tip dokaza se ocekuje. 
Primeticete da su ovi dokazi ponekad laksi ako se koristi prirodna dedukcija nego Isar. \<close>

text \<open> Formulisati i dokazati naredno tvrdjenje:
   Ako za svaki broj koji nije paran vazi da je neparan; 
   i ako za svaki neparan broj vazi da nije paran; 
   pokazati da onda za svaki broj vazi da nije istovremeno i paran i neparan \<close>

lemma "(\<forall> x. \<not> paran x \<longrightarrow> neparan x) \<and> (\<forall> x. neparan x \<longrightarrow> \<not> paran x)
        \<longrightarrow> (\<forall> x. \<not> (paran x \<and> neparan x))"
  apply (rule impI) (* sada prvo eliminisemo univerzalni kvantifikator sa desne strane *)
  apply (rule allI) (* pa razbijamo konjunkciju sa leve strane na dve premise *)
  apply (erule conjE) (* pa skidamo negaciju sa desne strane tako sto prebacujemo na levu *)
  apply (rule notI) (* pa opet konjunkciju razbijamo *)
  apply (erule conjE) (* sada u premisama imamo dve univerzalne kvantifikovane formule, 
                         koje posto vaze za svako x vazice i za ovo vec uvedeno fiksirano 
                         ali proizvoljno x *)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "x" in allE) (* sada posmatranjem skupa pretpostavki vidimo da nam 
                                       odgovara da razbijemo drugu implikaciju (jer njenu 
                                       levu stranu vec imamo u pretpostavkama *)
  apply (erule impE)
   back
   apply assumption
  apply (erule notE)
  apply assumption
  done

text\<open> (1) kostur automatskog dokaza \<close>
lemma 
  assumes "\<forall> x. \<not> paran x \<longrightarrow> neparan x"
  assumes "\<forall> x. neparan x \<longrightarrow> \<not> paran x"
  shows "\<forall> x. \<not> (paran x \<and> neparan x)"
proof 
  fix x
  show "\<not> (paran x \<and> neparan x)"
    sorry
qed

text\<open> (2) naredni korak automatskog dokaza \<close>
lemma 
  assumes "\<forall> x. \<not> paran x \<longrightarrow> neparan x"
  assumes "\<forall> x. neparan x \<longrightarrow> \<not> paran x"
  shows "\<forall> x. \<not> (paran x \<and> neparan x)"
proof 
  fix x
  show "\<not> (paran x \<and> neparan x)"
  proof
    assume "paran x \<and> neparan x"
    show False 
      sorry
  qed
qed

text\<open> (3) raspisan dokaz \<close>
lemma 
  assumes "\<forall> x. \<not> paran x \<longrightarrow> neparan x"
  assumes "\<forall> x. neparan x \<longrightarrow> \<not> paran x"
  shows "\<forall> x. \<not> (paran x \<and> neparan x)"
proof 
  fix x
  show "\<not> (paran x \<and> neparan x)"
  proof
    assume "paran x \<and> neparan x"
    from this have "paran x" "neparan x" by auto
    from this assms(2) have "\<not> paran x" by auto
    from this `paran x` show False by auto
  qed
qed


text \<open> Formulisati i dokazati naredno tvrdjenje: 
   Ako za svaki broj koji nije paran vazi da je neparan; 
   i ako za svaki neparan broj vazi da nije paran; 
   pokazati da onda za svaki broj vazi da je ili paran ili neparan
\<close>

lemma "(\<forall> x. \<not> paran x \<longrightarrow> neparan x) \<and> (\<forall> x. neparan x \<longrightarrow> \<not> paran x) \<longrightarrow> (\<forall> x. paran x \<or> neparan x)"
  apply (rule impI) 
  apply (erule conjE) (* prvo razbijamo konjunkciju na dve pretpostavke *)
  apply (rule allI) (* pa dva puta primenjujemo allE na obe pretpostavke *)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "x" in allE)
  apply (rule ccontr) (* sada transformisemo stare pp *)
  apply (erule impE)
   apply (rule notI)
   apply (erule notE)
   apply (rule disjI1)
   apply assumption
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply (rule disjI2)
  apply assumption
  done


text\<open> (1) Prvi korak \<close>
lemma 
  assumes "\<forall> x. \<not> paran x \<longrightarrow> neparan x"
  assumes "\<forall> x. neparan x \<longrightarrow> \<not> paran x"
  shows "\<forall> x. paran x \<or> neparan x"
proof
  fix x
  show "paran x \<or> neparan x" 
    sorry
qed


text\<open> (2) Drugi korak \<close>
lemma 
  assumes "\<forall> x. \<not> paran x \<longrightarrow> neparan x"
  assumes "\<forall> x. neparan x \<longrightarrow> \<not> paran x"
  shows "\<forall> x. paran x \<or> neparan x"
proof
  fix x
  have "paran x \<or> \<not> paran x" by auto (* dodajemo korak da bi napravili grananje 
                                        po slucajevima *)
  from this show "paran x \<or> neparan x" (* kada stavimo from this show ... , ako 
                                          je this disjunkcija dobijamo automatski dve grane *)
  proof 
    assume "paran x" 
    show "paran x \<or> neparan x"
      sorry
  next
    assume "\<not> paran x"
    show "paran x \<or> neparan x"
      sorry
  qed
qed

text\<open> (3) Treci korak \<close>
lemma 
  assumes "\<forall> x. \<not> paran x \<longrightarrow> neparan x"
  assumes "\<forall> x. neparan x \<longrightarrow> \<not> paran x"
  shows "\<forall> x. paran x \<or> neparan x"
proof
  fix x
  have "paran x \<or> \<not> paran x" by auto (* dodajemo korak da bi napravili grananje 
                                        po slucajevima *)
  from this show "paran x \<or> neparan x" (* kada stavimo from this show ... , ako je 
                                          this disjunkcija dobijamo automatski dve grane *)
  proof 
    assume "paran x" 
    from this show "paran x \<or> neparan x" by auto
  next
    assume "\<not> paran x"
    from this have "neparan x" using assms(1) by auto
    from this show "paran x \<or> neparan x" by auto
  qed
qed


text\<open> ako svaki konj ima potkovice; 
   i ako ne postoji covek koji ima potkovice; 
   i ako znamo da postoji  makar jedan covek; 
   dokazati da postoji covek koji nije konj \<close>

lemma "(\<forall> x. konj x \<longrightarrow> ima_potkovice x) \<and> \<not> (\<exists> x. covek x \<and> ima_potkovice x) \<and> (\<exists> x. covek x)
       \<longrightarrow> (\<exists> x. covek x \<and> \<not> konj x)" 
  apply (rule impI) (* posto imamo tri konjunkta, konjunkciju razbijamo iz dva puta *)
  apply (erule conjE)
  apply (erule conjE) (* sada imamo samo jedan egzistencijalni kvantifikator u premisama, 
                         i njega prvog oslobadjamo *)
  apply (erule exE) (* sada taj novo uvedeni x koristimo u zakljucku *)
  apply (rule_tac x = "x" in exI) (* sada razbijamo konjunkciju u zakljucku *)
  apply (rule conjI) (* resavamo prvi podcilj *)
   apply assumption (* sada resavamo drugi podcilj *)
  apply (rule notI) (* sada univerzalni kvantifikator u premisama instanciramo vec uvedenim x *)
  apply (erule_tac x = "x" in allE) (* sada se oslobadjamo implikacije u premisama *)
  apply (erule impE)
   apply assumption (* "ne postoji" je primarno negacija, pa moramo da se oslobadjamo nje prvo *)
  apply (erule notE) (* sada je egzistencijalni kvantifikator presao u zakljucak i instanciramo 
                        ga vec uvedenim objektom x *)
  apply (rule_tac x = "x" in exI)
  apply (rule conjI)
   apply assumption
  apply assumption
  done

text\<open> (1) kostur dokaza \<close>
lemma 
  assumes "\<forall> x. konj x \<longrightarrow> ima_potkovice x"
  assumes "\<not> (\<exists> x. covek x \<and> ima_potkovice x)"
  assumes "\<exists> x. covek x"
  shows "\<exists> x. covek x \<and> \<not> konj x" 
proof -
  from assms(3) obtain x where "covek x" by auto
  have "konj x \<or> \<not> konj x" by auto
  from this have "covek x \<and> \<not> konj x"
    sorry
  from this show "\<exists> x. covek x \<and> \<not> konj x" by auto
qed

text\<open> (2) naredni korak raspisan \<close>
lemma 
  assumes "\<forall> x. konj x \<longrightarrow> ima_potkovice x"
  assumes "\<not> (\<exists> x. covek x \<and> ima_potkovice x)"
  assumes "\<exists> x. covek x"
  shows "\<exists> x. covek x \<and> \<not> konj x" 
proof -
  from assms(3) obtain x where "covek x" by auto
  have "konj x \<or> \<not> konj x" by auto
  from this have "covek x \<and> \<not> konj x"
  proof
    assume "konj x"
    show "covek x \<and> \<not> konj x"
      sorry
  next
    assume "\<not> konj x"
    show "covek x \<and> \<not> konj x"
      sorry
  qed
  from this show "\<exists> x. covek x \<and> \<not> konj x" by auto
qed

text\<open> (3) kompletan dokaz --- nije bas elegantan, bolje je koristiti prirodnu dedukciju \<close>
lemma 
  assumes "\<forall> x. konj x \<longrightarrow> ima_potkovice x"
  assumes "\<not> (\<exists> x. covek x \<and> ima_potkovice x)"
  assumes "\<exists> x. covek x"
  shows "\<exists> x. covek x \<and> \<not> konj x" 
proof -
  from assms(3) obtain x where "covek x" by auto
  have "konj x \<or> \<not> konj x" by auto
  from this have "covek x \<and> \<not> konj x"
  proof
    assume "konj x"
    show "covek x \<and> \<not> konj x"
    proof 
      from `covek x` show "covek x" by auto
    next
      show "\<not> konj x"
      proof 
        assume "konj x"
        from this assms(1) have "ima_potkovice x" by auto 
        from `covek x` this have "\<exists> x. covek x \<and> ima_potkovice x" by auto
        from this assms(2) show False by auto
      qed
    qed
  next
    assume "\<not> konj x"
    from this and `covek x`
    show "covek x \<and> \<not> konj x" by auto
  qed
  from this show "\<exists> x. covek x \<and> \<not> konj x" by auto
qed


text\<open> ako je svaki kvadrat romb; 
   i ako je svaki kvadrat pravougaonik; 
   i ako znamo da postoji makar jedan kvadrat;
   onda postoji makar jedan romb koji je istovremeno i pravougaonik \<close>
lemma "(\<forall> x. kvadrat x \<longrightarrow> romb x) \<and> (\<forall> x. kvadrat x \<longrightarrow> pravougaonik x) \<and> (\<exists> x. kvadrat x) \<longrightarrow> 
       (\<exists> x. romb x \<and> pravougaonik x)" 
  apply (rule impI)
  apply (erule conjE)
  apply (erule conjE)
  apply (erule exE) (* ovim se uvodi x koji je kvadrat *)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "x" in allE)
  apply (rule_tac x = "x" in exI)
  apply (rule conjI)
   apply (erule impE)
  apply assumption
  apply assumption
  apply (erule impE)
  apply assumption
  apply (erule impE)
   apply assumption
  apply assumption
  done

lemma 
  assumes "\<forall> x. kvadrat x \<longrightarrow> romb x"
  assumes "\<forall> x. kvadrat x \<longrightarrow> pravougaonik x"
  assumes "\<exists> x. kvadrat x"
  shows "\<exists> x. romb x \<and> pravougaonik x" 
proof -
  from assms(3) obtain x where "kvadrat x" by auto
  from this assms(2) have "pravougaonik x" by auto
  from `kvadrat x` assms(1) have "romb x" by auto
  from this `pravougaonik x` show "\<exists> x. romb x \<and> pravougaonik x" by auto
qed

end