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

text {*

  \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 [] = []"
  | "rot [x] = [x]"
  | "rot (x#y#zs) = y # rot(x#zs)"

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 {*
  
  \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. *}

(*<*)end(*>*)