theory Cas4_vezbe_postavke
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 \<forall> 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 \<and> B \<longrightarrow> B \<and> A"
  apply (rule impI)
  apply (erule conjE)
  apply (rule conjI)
   apply assumption
  apply assumption
  done

lemma
  "A \<or> B \<longrightarrow> B \<or> A"
  apply (rule impI)
  apply (erule disjE)
   apply (rule disjI2)
   apply assumption
  apply (rule disjI1)
  apply assumption
  done

lemma
  "A \<and> B \<longrightarrow> A \<or> B"
  apply (rule impI)
  apply (erule conjE)
  apply (rule disjI1)
  apply assumption
  done


lemma "(A \<and> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> 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 \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<and> B \<longrightarrow> 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 \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<and> B \<longrightarrow> 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 "\<not> (A \<or> B) \<longrightarrow> \<not> A \<and> \<not> 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 "\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> 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 "\<not> A \<and> \<not> B \<longrightarrow> \<not> (A \<or> 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 \<longrightarrow> Q) \<and> (Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<and> R)"
  sorry

lemma "(P \<longrightarrow> Q) \<and> \<not> Q \<longrightarrow> \<not> P"
  sorry

lemma "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> (Q \<longrightarrow> (P \<longrightarrow> R))"
  sorry

lemma "\<not> (P \<and> \<not>P)"
  sorry

lemma "A \<and> (B \<or> C) \<longrightarrow> (A \<and> B) \<or> (A \<and> C)"
  sorry

lemma "\<not> (A \<and> B) \<longrightarrow> (A \<longrightarrow> \<not>B)"
  sorry

lemma "(A \<longrightarrow> C) \<and> (B \<longrightarrow> \<not> C) \<longrightarrow> \<not> (A \<and> B)"
  sorry

lemma "(A \<and> B) \<longrightarrow> ((A \<longrightarrow> C) \<longrightarrow> \<not> (B \<longrightarrow> \<not> C))"
  sorry

thm iffE

lemma "\<not> (A \<longleftrightarrow> \<not> A)"
  sorry

lemma "(A \<longleftrightarrow> B) \<longrightarrow> (\<not> A \<longleftrightarrow> \<not> B)"
  sorry

lemma "A \<longrightarrow> \<not> \<not> A"
  sorry

lemma "(Q \<longrightarrow> R) \<and> (R \<longrightarrow> P \<and> Q) \<and> (P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longleftrightarrow> Q)"
  sorry

lemma "(A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> \<not> A)"
  sorry

lemma "\<not> A \<or> B \<longrightarrow> (A \<longrightarrow> B)"
  sorry

end