34 lines
855 B
Text
34 lines
855 B
Text
theory Scratch
|
||
imports Main
|
||
begin
|
||
|
||
datatype 'a tree = Leaf 'a ("<_>")
|
||
| Node "'a tree list" ("⟦ _ ⟧")
|
||
|
||
text‹The datatype introduces special pretty printing:›
|
||
lemma "Leaf a = <a>" by simp
|
||
lemma "Node [] = ⟦ [] ⟧" by simp
|
||
|
||
definition "example ≡ ⟦[ ⟦[<1>]⟧, <2>, ⟦[ ⟦[<3>, <4>]⟧, <5>]⟧, ⟦[⟦[⟦[]⟧]⟧]⟧, ⟦[⟦[⟦[<6>]⟧]⟧]⟧, <7>, <8>, ⟦[]⟧ ]⟧"
|
||
|
||
lemma "example =
|
||
Node [
|
||
Node [Leaf 1],
|
||
Leaf 2,
|
||
Node [Node [Leaf 3, Leaf 4], Leaf 5],
|
||
Node [Node [ Node []]],
|
||
Node [Node [Node [Leaf 6]]],
|
||
Leaf 7,
|
||
Leaf 8,
|
||
Node []
|
||
]"
|
||
by(simp add: example_def)
|
||
|
||
fun flatten :: "'a tree ⇒ 'a list" where
|
||
"flatten (Leaf a) = [a]"
|
||
| "flatten (Node xs) = concat (map flatten xs)"
|
||
|
||
lemma "flatten example = [1, 2, 3, 4, 5, 6, 7, 8]"
|
||
by(simp add: example_def)
|
||
|
||
end
|