(*<*)
theory a4 = Main + Hoare + l2:
(*>*)
text {*
\section*{Nat\"urliches Schließen}

In dieser Aufgabe geht es um den Kalk\"ul des nat\"urlichen Schie{\ss}ens, 
mit dessen Hilfe einige Lemmas der Aussagen-Logik bewiesen werden sollen.

F\"ur die Beweise gelten die folgenden Spielregeln: 
\begin{itemize}
\item 
Es d\"urfen nur diese Lemmas verwendet werden: \\
@{text "notI:"}~@{thm notI[of A,no_vars]},\\
@{text "notE:"}~@{thm notE[of A B,no_vars]},\\
@{text "conjI:"}~@{thm conjI[of A B,no_vars]},\\ 
@{text "conjE:"}~@{thm conjE[of A B C,no_vars]},\\
@{text "disjI1:"}~@{thm disjI1[of A B,no_vars]},\\
@{text "disjI2:"}~@{thm disjI2[of A B,no_vars]},\\
@{text "disjE:"}~@{thm disjE[of A B C,no_vars]},\\
@{text "impI:"}~@{thm impI[of A B,no_vars]},\\
@{text "impE:"}~@{thm impE[of A B C,no_vars]},\\
@{text "mp:"}~@{thm mp[of A B,no_vars]}\\
@{text "iffI:"}~@{thm iffI[of A B,no_vars]}, \\
@{text "iffE:"}~@{thm iffE[of A B C,no_vars]}\\
@{text "classical:"}~@{thm classical[of A,no_vars]}
\item
Es d\"urfen nur die 
Methoden @{term rule}, @{term erule} und @{term assumption} verwendet werden. 
\end{itemize}
*}
lemma I: "A \<longrightarrow> A" 
oops
lemma "A \<and> B \<longrightarrow> B \<and> A" 
oops
lemma "(A \<and> B) \<longrightarrow> (A \<or> B)" 
oops
lemma K: "A \<longrightarrow> B \<longrightarrow> A" 
oops
lemma "(A \<or> A) = (A \<and> A)" 
oops
lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C" 
oops
lemma "(A \<longrightarrow> B) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> A \<longrightarrow> C" 
oops
lemma "\<not> \<not> A \<longrightarrow> A" 
oops
lemma "(\<not> A \<longrightarrow> B) \<longrightarrow> (\<not> B \<longrightarrow> A)" 
oops
lemma "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A" 
oops
lemma "A \<or> \<not> A" 
oops
text {* 
\section*{Hoare-Logik}

Die Beschreibung imperativer Programme durch Hoare-Tripel
eignet sich gut, um Eigenschaften von Programmen zu beweisen. Hierbei
werden Programmkonstrukte mit Zusicherungen (= Pr"adikate "uber
die Programmvariablen) annotiert, die das
Verhalten des Programms beschreiben. @{text "{P} c {Q}"} ist genau dann ein
g"ultiges Hoare-Tripel, wenn f"ur das Programm @{text c} und die
Vorbedingung @{text P} nach Ausf"uhrung von @{text c} die Nachbedingung
@{text Q} gilt (siehe z.B.[1]).

F"ur Isabelle/HOL existiert eine Definition der Hoare-Logik
f"ur eine einfache imperative Sprache mit folgenden syntaktischen
Konstrukten: 

\(
\begin{array}{lll}
\name{c} & =   & \name{SKIP}\\
  &\mid &  \name{x} := \name{a}\\
  &\mid &  \name{c}_0;\ \name{c}_1\\
  &\mid &  \name{IF}\ b\ \name{THEN}\ \name{c}_0\ \name{ELSE}\ \name{c}_1\ \name{FI}\\
  &\mid &  \name{WHILE}\ \name{b}\ \name{INV}\ \{\name{I}\}\ \name{DO}\ \name{c}\ \name{OD}\\
  &=  &\{\name{P}\}\ \name{c}\ \{\name{Q}\}
\end{array}
\)

Wie man sieht, gen"ugt es, innerhalb eines Programms den Rumpf
von @{text WHILE}-Schleifen mit einer Schleifeninvariante @{text I}
zu annotieren; f"ur die anderen Konstrukte
lassen sich die schw"achsten Vorbedingungen aus den jeweiligen Nachbedingung
automatisch ableiten. 
Die Methode @{text hoare} erzeugt f"ur ein Hoare-Tripel @{text "{P} c {Q}"}
Verifikationsbedingungen, durch die sich die G"ultigkeit des Tripels
beweisen l"a" st.


Beispiele finden Sie unter 
  \texttt{http://www.in.tum.de/\~\relax isabelle/library/HOL/Hoare}

Wichtige Informationen finden Sie unter\\
  \texttt{http://www4.in.tum.de/\~\relax isabelle/library/HOL/Hoare/README.html} 
 
 Im Folgenden sollen einige imperative Programme mit Hilfe der Hoare
 Logik verifiziert werden.  Die zugrundeliegende Theorie ist in
 \cite{Wenzel:2000:Hoare} genauer beschrieben.  Weitere Informationen
 zur axiomatischen Semantik finden sich z.B.\ in
 \cite[\S5.7.1]{Broy-PartI}
 \cite[\S6]{Winskel:1993} oder \cite[\S4]{Huth-Ryan:2000}.

 \medskip Hier ein einfaches Beispiel zur Anwendung der Hoare Logik.
 Wir verifizieren ein Programm, das zwei nat"urliche Zahlen durch
 wiederholte Addition multipliziert.

 Zuerst deklarieren wir die verwendeten Programmvariablen als
 Record-Typ.
*}

record mult_vars =
  M :: nat
  N :: nat

text {*
 Die zu beweisende Aussage wird als Hoare-Tripel wie folgt formuliert.
 Man beachte die Unterscheidung von Programmvariablen von einfachen
 Werten der Logik: Programmvariablen wie @{text "\<acute>M"} hängen implizit
 vom aktuellen Zustand @{text s} des Programms ab, logische Variablen
 wie @{term a} nicht.
*}

theorem
"\<turnstile> .{\<acute>M = 0 \<and> \<acute>N = 0}.
    WHILE \<acute>M \<noteq> a
    INV .{\<acute>N = \<acute>M * b}.
    DO \<acute>N := \<acute>N + b; \<acute>M := \<acute>M + 1 OD
    .{\<acute>N = a * b}."

  txt {* \normalsize Die Hauptarbeit des Beweises erledigt die
 \name{hoare} Methode, welche ein mit Invarianten annotiertes
 Hoare-Tripel auf ein rein logisches Problem reduziert. Den Rest kann
 man in diesem Beispiel einfach mit \name{auto} erledigen. *}

  apply hoare
  apply auto
  done
 
text {* 
\section*{Quotient und Rest}

Geben Sie ein annotiertes imperatives Program zur Berechnung
des Quotients und Rests zweier nat"urlichen Zahlen @{text x}
 und @{text y}. Beweisen Sie dann folgendes Hoare-Tripel: 
*}
record quo_vars =
  quo  :: nat
  rest :: nat

theorem "\<turnstile> .{True}. programm .{\<acute>quo * y + \<acute>rest = x \<and> \<acute>rest < y }."
oops

text {* 
  \section*{Sortieren}

  Implementieren Sie die Funktion @{term insort} des Sortieralgorithmus 
  aus Aufgabenblatt 2 imperativ. Eingabe ist eine Liste @{text "\<acute>ls"}, Ausgabe
  eine neue Liste @{text "\<acute>ss"}, in die das Element @{text n} geordnet
  eingefügt wurde. Zeigen Sie folgendes Hoare-Tripel:
*}
record insort_vars =
  ls :: "nat list"
  ss :: "nat list"

theorem "\<turnstile> .{\<acute>ls = list}. programm .{\<acute>ss = insort n list}."
  oops

text {*
  \note{Hinweise:}
  \begin{itemize}
  \item Die Eingabeliste @{text "\<acute>ls"} darf verändert werden.
  \item Um eine verkettete Liste zu simulieren, dürfen Sie im Programm
  selbst nur die Funktionen @{term hd}, @{term tl}, und @{text "@ [x]"} 
  (append mit einer einelementigen Liste) benutzen. In den
  Invarianten steht ihnen die volle Mächtigkeit
  von HOL mit allen Funktionen und Ausdrücken zur Verfügung.
  \item Sie werden für die Invariante evtl.~eine neue Funktion
  definieren müssen.
  \end{itemize}

  {\bf Freiwillige Zusatzaufgabe:}\\
  Implementieren Sie den gesamten Sortieralgorithmus (die Funktion @{text sort} von
  Aufgabenblatt 2) imperativ, und beweisen Sie, dass er das gleiche Ergebnis liefert
  wie @{text sort}. Sie können alternativ auch zeigen, dass für das Ergebnis @{text sorted}
  gilt, und @{text count} nicht verändert wird.  
*}

(*<*)
end
(*>*)