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

text {*
  \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(*>*)