theory Tree_Demo imports Main begin datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" lemma "Tip ~= Node l x r" apply auto done fun mirror :: "'a tree \ 'a tree" where "mirror Tip = Tip" | "mirror (Node l x r) = Node (mirror r) x (mirror l)" value "mirror(Node (Node Tip a Tip) b t)" lemma mirror_mirros[simp]: "mirror(mirror t) = t" apply(induct t) apply auto done (* fun *) fun sep :: "'a \ 'a list \ 'a list" where "sep a [] = []" | "sep a [x] = [x]" | "sep a (x#y#zs) = x # a # sep a (y#zs)" value "sep a [x,y,z]" end