(*<*)theory Simplification imports Main begin(*>*)

text {*

\section*{1. Pr\"adikatenlogik und Simplifikation}

  In klassischer Aussagenlogik k\"onnen die Operatoren @{text "=, \<or>, \<not>"} 
  durch @{text "\<longrightarrow>, \<and>, False"} ersetzt werden.
  Definieren und beweisen Sie entsprechende Simplifikationslemmas. Benutzen Sie
  daf\"ur wieder nur die Methoden @{term rule}, @{term erule} und @{term assumption}
  und die bisher bekannten Regeln, zus\"atzlich noch folgende:
  @{text "FalseE:"}~@{thm FalseE[no_vars]}\\
  @{text "TrueI:"}~@{thm TrueI[no_vars]}
  *}

lemma rewrite_not:"(\<not> A) = \<dots>"
oops

lemma rewrite_eq:"(A = B) = \<dots>"
oops

lemma rewrite_or:"(A \<or> B) = \<dots>"
oops


text {* Versuchen Sie nun, folgende Ausdr\"ucke soweit wie m\"oglich umzuschreiben.
  Benutzen Sie dazu die Methode @{term simp} mit der Option @{text only}. Sie 
  k\"onnen danach versuchen, das Resultat zu beweisen (nat\"urlich nur mit den Regeln
  f\"ur @{text \<longrightarrow>} bzw. @{text \<and>}) oder den Beweis einfach mittels 
  @{term oops} abbrechen. *}

lemma "(A \<and> True) = A"
oops

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

lemma "(\<not> (A \<and> B)) = (\<not> A \<or> \<not> B)"
oops


text {*

\section*{2. Simplifikation am Beispiel xor}

  In dieser Aufgabe soll ein neuer Operator @{text xor} bzw. @{text \<oplus>} wie \"ublich 
  definiert werden. Anschlie{\ss}end werden ein paar Termersetzungsregeln formuliert 
  und bewiesen und schlie{\ss}lich an einem gr\"o{\ss}eren Beispiel das Verhalten des 
  Simplifiers simuliert.
  
  Definieren Sie zun\"achst analog zum @{text nand} Beispiel aus den Folien den 
  Operator @{text xor}:
*}

(*<*)consts DUMMY :: bool ("....")(*>*)

definition
  xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<oplus>" 60)
  where "A \<oplus> B \<equiv> ...."

text {* Jetzt beweisen wir ein paar Simplifikationsregeln, indem wir als erstes
  die Definition von @{text xor} auffalten mittels \texttt{apply(simp only:xor\_def)}
  und das Resultat dann mit den aus den bisherigen \"Ubungen bekannten Methoden 
  beweisen. *}

lemma xor_True:"True \<oplus> A = (\<not> A)"
-- "Auffalten der Definition, auch in den folgenden Lemmas jeweils erster Schritt"
apply(simp only:xor_def)
-- "Und jetzt der Beweis"
oops

lemma xor_False:"False \<oplus> A = A"
oops

  -- "Sie ben\"otigen evtl. Fallunterscheidung nach A, um dies zu beweisen"
lemma xor_asym_aux:"A \<oplus> (\<not> A)"
oops

lemma xor_not_sym_aux:"\<not> A \<oplus> A"
oops

text {* Die letzten beiden Lemmas k\"onnen wir nicht als Termersetzungsregeln 
  verwenden, da sie nicht die ben\"otigte Gleichungsform haben. Jedoch kann man jetzt
  die ben\"otigten Simplifikationslemmas formulieren und jene verwenden, um sie
  zu beweisen. *}

  -- "einfach Beweis 'entkommentieren' und oops entfernen"
lemma xor_asym:"A \<oplus> (\<not> A) = True"
(* apply(simp only:xor_asym_aux)
   done *)
oops

lemma xor_not_sym:"A \<oplus> A = False"
(* apply(simp only:xor_not_sym_aux)
   done *)
oops

text {* \eject Und zum Schlu{\ss} noch eine etwas komplizierter zu zeigende Regel: *}

  -- "Auch hier k\"onnen Fallunterscheidungen n\"otig sein"
lemma xor_simp:"A \<oplus> (A \<oplus> B) = B"
oops


text {* Beim folgenden Lemma sollen nun Sie den Simplifier direkt anleiten. Sie
  d\"urfen daf\"ur alle obigen Termersetzungsregeln verwenden, aber jedoch nur eine 
  pro Schritt, also:\\
  \texttt{apply(simp only: $Regel_x$)}\\
  \texttt{apply(simp only: $Regel_y$)}\\
  $\dots$ *}

lemma "(B \<oplus> ((((A \<oplus> (A \<oplus> (\<not> B))) \<oplus> (\<not> B)) \<oplus> B) \<oplus> A)) \<oplus> 
       (((\<not> B) \<oplus> ((A \<oplus> (\<not> A)) \<oplus> B)) \<oplus> A) = False"
oops




(*<*) end (*>*)