theory Cas5_vezbe_postavke
imports Main

begin


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

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

text\<open> 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 i u primeni pravila se 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...and vk = tk in R
This method behaves like rule R, while instantiating the variables v1...vk
as specified. *)
  apply (erule impE) (* nakon toga eliminisemo implikaciju *)
   apply assumption
  apply assumption
  done

text\<open> prirodnom dedukcijom dokazati da je ovo teorema logike prvog reda \<close>
lemma "(\<exists> x. P x) \<and> (\<forall> x. P x \<longrightarrow> Q x) \<longrightarrow> (\<exists> x. Q x)"
(* razbijamo iskazni skeleton prvo *)
  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 *)
  (* ovde je bojama napravljena razlika *)
  (* narandzasto x je ovo dobijeno sa exists *)
  (* 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 (* by (rule_tac x = "x" in allE) *)
  from this `P x` have "Q x" by auto (* by (rule impE) *)
  from this show "\<exists> x. Q x" by auto (* 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>

(* treba raspisati oba dokaza za sve leme, ali za naredne necu pisati obe formulacije vec to 
   morate uraditi sami za vezbu *)
(* resenja zadataka cu okaciti za nekoliko dana *)
lemma "(\<forall> a. P a \<longrightarrow> Q a) \<and> (\<forall> b. P b) \<longrightarrow> (\<forall> x. Q x)"
  by auto

lemma 
  assumes "\<forall> a. P a \<longrightarrow> Q a"
  assumes "\<forall> b. P b"
  shows "\<forall> x. Q x"
  sorry

lemma "(\<exists> x. A x \<or> B x) \<longrightarrow> (\<exists> x. A x) \<or> (\<exists> x. B x)"
  by auto

lemma "(\<forall> x. A x \<longrightarrow> \<not> B x) \<longrightarrow> \<not> (\<exists> x. A x \<and> B x)"
  by auto

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))"
  by auto

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)"
  by auto

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)" 
  by auto

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)" 
  by auto

end