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

text {*
  
  \section*{Wechselseitige Rekursion}

  In bestimmten F\"allen muss man Datentypen definieren, die voneinander abh\"angig 
  sind, d.h. der eine wird im anderen verwendet und anders herum. Um dann Aussagen
  \"uber diese Datentypen machen zu k\"onnen, braucht man wechselseitige Rekursion.

  Wir wollen jetzt einen Datentyp definieren f\"ur arithmetische und boole'sche 
  Aussagen. Der Typ der vorkommenden Variablen soll nicht spezifiziert werden,
  deshalb verwenden wir f\"ur sie den Typparameter @{typ "'a"}.
  Da in arithmetischen Ausdr\"ucken boole'sche verwendet werden k\"onnen
  (Bsp. ``if $m < n$ then $n - m$ else $m - n$'') bzw. anders herum (Bsp. ``$m - n < 
  m + n$''), m\"ussen wir sie wechselseitig rekursiv definieren: *}

datatype 
  'a aexp =   --"arithmetische Ausdr\"ucke"
    IF "'a bexp" "'a aexp" "'a aexp"  --"if-then-else"
  | Sum "'a aexp" "'a aexp"           
  | Diff "'a aexp" "'a aexp"          
  | Var 'a                   --"Variablen (speichern nat\"urliche Zahlen)"
  | Const nat                --"Konstanten (nat\"urliche Zahlen)"

  and --"wechselseitige Rekursion"
  'a bexp =   --"boole'sche Ausdr\"ucke"
    Less "'a aexp" "'a aexp"          
  | And "'a bexp" "'a bexp"           
  | Neg "'a bexp"


text{*Wir brauchen auch noch eine Umgebung, die die Werte der Variablen liefert,
  also eine Funktion von Typ der Variablen (@{typ 'a}) nach @{typ nat}:*}

types 'a env = "'a \<Rightarrow> nat"

text{*Definieren Sie jetzt Auswertungsfunktionen @{text evala} bzw. @{text evalb},
  welche unter Verwendung einer Umgebung @{typ "'a env"} das Resultat der Operation 
  liefert. Da die Datentypen wechselseitig rekursiv sind, sind es auch die 
  Funktionen, die auf ihnen operieren. Deshalb m\"ussen @{text evala} und 
  @{text evalb} innerhalb eines @{text primrec} definiert werden:*}

primrec  evala :: "'a aexp \<Rightarrow> 'a env \<Rightarrow> nat" and evalb :: "'a bexp \<Rightarrow> 'a env \<Rightarrow> bool"
  --"erweitern Sie diese Definition"
where
  "evala (Sum a1 a2) env  = evala a1 env + evala a2 env"

  | "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"


text{*Analog definieren Sie jetzt zwei Funktionen, welche Variablensubstitution 
  durchf\"uhren:*}

consts
  substa :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a aexp \<Rightarrow> 'b aexp"
  substb :: "('a \<Rightarrow> 'b aexp) \<Rightarrow> 'a bexp \<Rightarrow> 'b bexp"

text{*Der erste Parameter ist die Substitution, eine Funktion, welche Variablen auf 
  Ausdr\"ucke abbildet. Sie wird auf alle Variablen des Ausdrucks angewandt, weshalb
  der Resultattyp ein Ausdruck mit Variablen vom Typ @{typ "'b"} ist:*} 


text{*Beweisen Sie nun, dass die Substitutionsfunktion @{term Var}
  einen Ausdruck in sich selbst \"uberf\"uhrt. Wenn man 
  versucht, diese Aussage einzeln f\"ur arithmetische bzw. boole'sche
  Ausdr\"ucke zu zeigen, wird man feststellen, dass man jeweils die Aussage
  f\"ur die entsprechend anderen Ausdr\"ucke im Induktionsschritt ben\"otigt.
  Also m\"ussen beide Theoreme gleichzeitig gezeigt werden. Dazu verwendet man 
  gleichzeitige Induktion \"uber beide Parameter @{text a} und @{text b} mittels
  der Regeln @{text "induct_tac a and b"}:*}

lemma "substa Var (a::'a aexp) = a" 
      "substb Var (b::'a bexp) = b"
  oops

text{*Wir beweisen jetzt ein fundamentales Theorem \"uber die Interaktion zwischen
  Auswertung und Substitution: wenn man eine Substitution @{text s} auf einen
  Ausdruck @{text a} anwendet und dann mittels einer Umgebung @{text env} auswertet,
  erh\"alt man das gleiche Resultat wie wenn man @{text a} auswertet mittels einer
  Umgebung, welche jede Variable @{text x} auf den Wert @{text "s(x)"} unter 
  @{text env} abbildet.*}

lemma "evala (substa s a) env = evala a (\<lambda>x. evala (s x) env)"
      "evalb (substb s b) env = evalb b (\<lambda>x. evala (s x) env)"
  oops


text{*Abschlie{\ss}end sollen Sie eine Normalisierungsfunktion @{text norma}
  definieren. Diese soll @{typ "'a aexp"}s so umbauen, dass in der Bedingung 
  eines @{text IF} nur @{text Less} stehen darf; falls dort @{text And} oder 
  @{text Neg} steht, muss der @{text IF}-Ausdruck umgebaut werden. Daf\"ur
  brauchen sie eine weitere, zu @{text norma} wechselseitig rekursive Funktion;
  wie sieht diese aus?
  Beweisen Sie dann zwei Aussagen dar\"uber:
  \begin{enumerate}
  \item @{text norma} ver\"andert nicht den Wert, den @{text evala} liefert
  \item @{text norma} ist wirklich normal, d.h. keine @{text And}s oder 
    @{text Neg}s tauchen in den @{text IF}-Bedingungen auf (daf\"ur brauchen 
    Sie wiederum zwei wechselseitig rekursive Funktionen; welche?).
  \end{enumerate}
  Beide Lemmas brauchen auch eine Aussage f\"ur die Funktion, welche die @{text IF}s
  umbaut.
 *}

consts norma :: "'a aexp \<Rightarrow> 'a aexp"


(*<*)end(*>*)