| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Tutorial/Misc/ (Isabelle Prover Version 2025-1©) Datei vom 16.11.2025 mit Größe 911 B |
|
Quelle Tree.thySprache: Isabelle |
|||||||||||||||
|
(*<*) theory Tree imports Main begin (*>*) text‹\noindent the datatype of \rmindex{binary trees}: › datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*) primrec mirror :: "'a tree → 'a tree" where "mirror Tip = Tip" | "mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*) text‹\noindent a function term‹mirror› that mirrors a binary tree swapping subtrees recursively. Prove › 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‹\noindent a function term‹flatten› that flattens a tree into a list traversing it in infix order. Prove › lemma "flatten(mirror t) = rev(flatten t)" (*<*) apply(induct_tac t) by(auto) end (*>*)
¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet am 2026-06-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09