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

section {* Zum Warmwerden *}

text {*
  $\rhd$ Definieren sie die Fakultätsfunktion @{term "fac"} auf natürlichen Zahlen.
  Sie können dazu die Multiplikation
  @{term "m * n"} auf natürlichen Zahlen verwenden.
*}

consts
  fac :: "nat \<Rightarrow> nat"

text {*
  $\rhd$ Definieren sie eine Funktion @{term sum}, die eine Liste natürlicher Zahlen aufsummiert. 
  Die Additon @{term "m + n"} auf natürlichen Zahlen ist bereits definiert.
*}

consts
  sum :: "nat list \<Rightarrow> nat"



text {* $\rhd$ Zeigen Sie: *}
lemma "sum (rev xs) = sum xs"
(*<*)sorry(*>*)

text {*
  Eine Liste von Listen lässt sich durch Aneinanderhängen der einzelnen Listen ">flachklopfen"<.
  Dazu gibt es bereits eine vordefinierte Funktion in der Listentheorie 
  \emph{List.thy}. Weiterhin lierfert die Funktion @{term length} die Länge einer Liste.
  
  $\rhd$ Formulieren
  und beweisen Sie: die Länge einer flachgeklopften Liste von Listen ist
  die Summe der Längen der einzelnen Listen. Zum Formulieren ist die
  Funktion @{const map} hilfreich (oder definieren sie eine geeignete Hilfsfunktion).
*}

text {*
  $\rhd$ Zeigen Sie eine ähnliche Eigenschaft über flachgeklopfte Listen und @{const sum}.
*}

section {* Assozationslisten *}

text {*
  Assoziazinslisten sind Listen von Paaren, die endliche partielle
  Abbildungen repräsentieren. Wir definieren zwei Operationen @{text lookup} und @{text update} 
  zum Nachschlagen von Werten und Aktualisieren von Assoziazionslisten:
*}

consts
  lookup :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option"
  update :: "'a \<times> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"

primrec
  "lookup [] k = None"
  "lookup (x#xs) k = (if k = fst x then Some (snd x) else lookup xs k)"

primrec
  "update (k, v) xs = (k, v) # xs"

text {*
  $\rhd$ Beweisen oder widerlegen Sie:
*}

lemma lookup_update:
  "lookup (update (k, v) xs) k = Some v"
(*<*)sorry(*>*)

lemma lookup_update2:
  "lookup (update (x, a) (update (y, b) xs)) y = Some b"
(*<*)sorry(*>*)

text {*
  $\rhd$ Definieren Sie eine Funktion @{term delete}, die einen Eintrag aus
  einer Assoziationsliste löscht.
*}

consts
  delete :: "'a \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"

text {* $\rhd$ Zeigen Sie: *}

lemma lookup_delete:
  "lookup (delete k xs) k = None"
(*<*)sorry(*>*)

text {*
  Unsere Assoziationslisten haben das Problem, dass sich bei
  wiederholten Updates jedesmal neuer Müll in der Liste ansammelt, der
  nicht mehr relevant ist.
  
  $\rhd$ Definieren sie eine Funktion @{term normalize},
  die alle nicht mehr benötigten Paare aus der Liste
  löscht.
*}

consts 
  normalize :: "('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"

text {*
  $\rhd$ Man erwartet natürlich, dass die normalisierten Listen sich
  noch genauso verhalten wie das
  Original. Zeigen Sie die entscheidende Korrektheitseigenschaft:
*}

theorem [simp]: "lookup (normalize xs) k = lookup xs k"
(*<*)sorry(*>*)
text {*
  \emph{Hinweis}: Wahrscheinlich benötigen Sie hier wieder ein
  geeignetes Hilfslemma, eine Eigenschaft über das Zusammenspiel von
  @{const delete} und @{const lookup}.
*}



section {* Ein verifizierter Mini-Compiler *}

subsection {* Quellspache: Einfache artihmetische Ausdrücke *}

text {*
  Wie definieren einfache arithmetische Ausdrücke über
  den ganzen Zahlen. Diese bestehen aus Numeralen (">-7"<, ">42"<),
  Variablen (die wir der Einfachheit halber mit natürlichen Zahlen
  bezeichnen) und den binären Operationen \emph{Add} und \emph{Mult}
  (siehe hierzu auch Abschnitt 3.3.~des Tutorials).
  Repräsentiert werden diese Ausdrücke durch folgenden Datentyp: 
*}

datatype aexp = 
  Num int
  | Var nat
  | Add aexp aexp
  | Mult aexp aexp

text {*
  Der Wert von Variablen wird aus einer \emph{Umgebung}
  (environment) abgerufen. Das ist einfach eine Funktion
  von Variablenname (bei uns: natürliche Zahl) auf Wert (ganze Zahl):
*}

types
  env = "nat \<Rightarrow> int"

text {*
  Um die Semantik dieser Ausdrücke zu erklären, definieren wir eine
  Auswertungsfunktion:
*}

consts
  eval :: "env \<Rightarrow> aexp \<Rightarrow> int"
primrec 
  "eval env (Num n) = n"
  "eval env (Var v) = env v"
  "eval env (Add e1 e2) = eval env e1 + eval env e2"
  "eval env (Mult e1 e2) = eval env e1 * eval env e2"

text {*
  Wenn von vornherein feststeht, in welcher Umgebung ein Ausdruck
  ausgewertet werden soll, kann man die Werte der Variablen auch
  direkt in den Ausdruck einsetzen und erhält einen Ausdruck
  ohne Variablen.

  $\rhd$ Definieren Sie dazu eine Funktion @{term elim_var}.
*}

consts
  elim_var :: "env \<Rightarrow> aexp \<Rightarrow> aexp"

text {*
  $\rhd$ Zeigen Sie: Die Auswertung eines Ausdrucks in einer Umgebung
  liefert das gleiche Ergebnis wie die Auswertung des gleichen Ausdrucks,
  in dem zuvor alle Variablen eliminiert worden sind, in einer beliebigen
  (anderen) Umgebung.
*}

subsection {* Zielarchitektur: Eine einfache Stackmaschine *}

text {*
  Nun definieren wir eine Stackmaschine, die einfache
  arithmetische Berechnungen ausführen kann. Sie hat folgenden
  Befehlssatz: *}

datatype instr =
  IStore int
  | IVar nat
  | IAdd
  | IMult

text {*
  Dabei haben die einzelnen Instruktionen folgende Semantik:
  \begin{enumerate}
    \item @{term "IStore k"}: Lege den Wert @{term k} auf den Stack
    \item @{term "IVar n"}: Lege den Wert der Variablen @{term n} auf den Stack
    \item @{term IAdd}: Nimm die beiden obersten Werte vom Stack, addiere
      sie und lege das Ergebnis wiederum auf den Stack
    \item @{term IMult}: Nimm die beiden obersten Werte vom Stack, multipliziere
      sie und lege das Ergebnis wiederum auf den Stack
  \end{enumerate}

  Die Stackmaschine verarbeitet in einem Schritt eine Instruktion @{typ "instr"}
  innerhalb einer Umgebung @{typ env} auf einem Eingangszustand des Stack
  und endet mit einem Ausgangszustand des Stack. Den Stack modellieren wir
  als @{typ "int list"}.
*}

consts
  exec :: "env \<Rightarrow> instr \<Rightarrow> int list \<Rightarrow> int list"

text {*
  Für die Instruktionen @{const IAdd} und @{const IMult} benötigen wir eine
  Hilfsfunktion, die zwei Elemente vom Stack nimmt, sie mit einer Operation
  verknüpft und das Ergebnis wieder auf den Stack legt. Für diese (nicht-rekursive)
  Definition können wir \emph{constdefs} verwenden%
  \footnote{Statt der (Objektlogik-)\-Gleichheit @{text "="} muss
  bei \emph{constdefs} die (Metalogik-)\-Gleichheit @{text "\<equiv>"} verwendet werden.}.


*}

constdefs
  ap2 :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"
  [simp]: "ap2 f xs \<equiv> f (hd xs) (hd (tl xs)) # tl (tl xs)"

text {*
  Nun zur Definition von @{const exec}\footnote{
Wie in ML bazeichnet die Syntax @{term "(op +)"}, dass ein Infix-Operator
  in Präfix-Position verwendet wird.}:
*}

primrec
  "exec env (IStore n) s  = n # s"
  "exec env (IVar v) s = (env v) # s"
  "exec env IAdd s = ap2 (op +) s"
  "exec env IMult s = ap2 (op *) s"

text {*
  

  Bislang haben wir nur definiert, was in einem Verarbeitungsschritt
  (@{typ instr}) passiert. Die Stackmaschine soll aber eine Liste
  von Instruktionen hintereinander abarbeiten:
*}

consts
  lexec :: "env \<Rightarrow> instr list \<Rightarrow> int list \<Rightarrow> int list"

text {*
  $\rhd$ Definieren Sie @{const lexec} in geeigneter Weise!
*}

subsection {* Der Compiler *}

text {*
  Wir werden nun einen kleinen Compiler von arithmetischen Ausdrücken
  in die Sprache der Stackmaschine schreiben und seine Korrektheit zeigen.

  Der Compiler übersetzt arithmetische Ausdrücke in Listen von
  Instruktionen für die Stackmaschine:
*}

consts
  compile :: "aexp \<Rightarrow> instr list"

text {*
  $\rhd$ Geben Sie die Definition von @{const compile} an!
*}

text {*
  $\rhd$ Formulieren und Beweisen Sie die Korrektheit des Compilers
  Dazu werden sie wahrscheinlich Hilfslemmata
  benötigen. Auch kann es nötig sein, die zu beweisende Aussage zu generalisieren.
  Hilfreiche Hinweise dazu finden Sie in Abschnitt 3.2.~des Tutorials.
*}

(*<*)
end
(*>*)