| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Doc/Tutorial/Misc/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 911 B |
|
Quelle Tree.thy Sprache: Isabelle |
|||||||||
|
(*<*)
theory Tree imports Main begin (*>*) text\<open>\noindent Define the datatype of \rmindex{binary trees}: \<close> datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*) primrec mirror :: "'a tree \ "mirror Tip = Tip" | "mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*) text\<open>\noindent Define a function \<^term>\<open>mirror\<close> that mirrors a binary tree by swapping subtrees recursively. Prove \<close> lemma mirror_mirror: "mirror(mirror t) = t" (*<*) apply(induct_tac t) by(auto) primrec flatten :: "'a tree => 'a list" where "flatten Tip = []" | "flatten (Node l x r) = flatten l @ [x] @ flatten r" (*>*) text\<open>\noindent Define a function \<^term>\<open>flatten\<close> that flattens a tree into a list by traversing it in infix order. Prove \<close> lemma "flatten(mirror t) = rev(flatten t)" (*<*) apply(induct_tac t) by(auto) end (*>*) ¤ Dauer der Verarbeitung: 0.3 Sekunden ¤*© Formatika GbR, Deutschland |
|
2026-03-28