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

text {*
  \vspace*{-\baselineskip}
  \section{Rotation mal ungew\"ohnlich}

  Wir definieren eine Funktion auf Listen, welche das erste Element an die letzte 
  Stelle schiebt: *}

fun rot :: "'a list \<Rightarrow> 'a list"
where "rot (x#y#zs) = y # rot(x#zs)"
  | "rot xs = xs"

text {*
  Die von Isabelle automatisch erstellte Rekursionsregel lautet @{text "rot.induct:"}\\
  @{thm rot.induct[no_vars]}\\
  Damit beweisen Sie bitte folgende Aussagen mittels eines \emph{verst\"andlichen} 
  Isar-Beweises:
  *}

lemma "length (rot xs) = length xs"
oops

lemma "xs \<noteq> [] \<Longrightarrow> rot xs = tl xs @ [hd xs]"
oops
  

text {*
  \vspace*{-\baselineskip}
  \section{Reflexiv-transitive H\"ulle}

Wir definieren die reflexiv-transitive H\"ulle einer bin\"aren Pr\"adikats @{text r}
  mittels eines induktiven Pr\"adikats: *}

inductive rtc :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_*)" [1000] 1000)
for r::"'a \<Rightarrow> 'a \<Rightarrow> bool"
where refl: "r* x x"
  | step: "\<lbrakk>r x y; r* y z\<rbrakk> \<Longrightarrow> r* x z"


text {*
  Anstatt @{text "rtc r"} darf man also @{term "r*"} schreiben. Auch hier generiert
  Isabelle automatisch eine Induktionsregel @{text "rtc.induct:"}
  @{thm rtc.induct[no_vars]}
  Zeigen Sie jetzt, dass @{term "r*"} tats\"achlich transitiv ist:
*}

lemma "\<lbrakk>r* x y; r* y z\<rbrakk> \<Longrightarrow> r* x z"
oops

text {*
  Au{\ss}erdem beweisen Sie noch, dass @{term "r*"} idempotent (die 
  reflexiv-transitive H\"ulle von @{term "r*"} gleich @{term "r*"}) ist.
  Dazu brauchen Sie folgende Aussage: @{text "ext: "} @{thm ext}
*}


lemma rtc_idemp: "(r*)* = r*"
proof(rule ext)+
oops


text {* Alle Beweise sollen nat\"urlich mittels Isar erstellt werden.


  \section{Kontextfreie Grammatiken f\"ur Klammerausdr\"ucke}
  
  Im folgenden soll eine Grammatik f\"ur Klammerausdr\"ucke (als Listen) 
  formalisiert werden.
  Solche Grammatiken haben \"ublicherweise folgende Darstellung:
  \[ S \quad\to\quad \varepsilon \quad\mid\quad '('~S~')' \quad\mid\quad S~S \]
  Sie sollen nun diese Grammatik als induktives Pr\"adikat definieren. Dabei soll der 
  folgende Datentyp die Klammern beschreiben, @{text A} eine \"offnende, @{text B}
  eine schlie{\ss}ende Klammer (die normalen Klammern sind in Isabelle
  funktional \"uberladen): *}

datatype brack = A | B

text {*
  Man kann auch noch auf eine andere Weise pr\"ufen, ob Klammerausdr\"ucke korrekt 
  sind: durch Abz\"ahlen der \"offnenden und schlie{\ss}enden Klammern. F\"ur jede
  \"offnende Klammer inkrementiert man einen Z\"ahler, f\"ur jede schlie{\ss}ende
  dekrementiert man ihn. Wenn der Z\"ahler 0 ist, darf er nicht weiter
  dekrementiert werden!

  Definieren Sie ein Pr\"adikat zur Pr\"ufung von Klammerausdr\"ucken, 
  basierend auf dieser Methode.

  Hinweise:
  \begin{itemize}
  \item verwenden sie statt @{text "n + 1"} @{text "Suc n"} 
  \item wenn eine beliebige nat\"urliche Zahl von 0 abgezogen wird, ist das
    Resultat wieder 0
  \item wie muss der Z\"ahler beschaffen sein, wenn man auf eine schlie{\ss}ende
    Klammer trifft?
  \end{itemize} *}

text {* Und nun beweisen Sie, dass jeder Parameter, der das oben definierte 
  induktive Pr\"adikat erf\"ullt auch dieses Pr\"adikat erf\"ullt. *}


(*<*)end(*>*)