Theory Mirrors

Up to index of Isabelle/HOL/IsarTut

theory Mirrors = Main:
theory Mirrors = Main:

text {* Solution to exercise 2.4.1.  I'm not at all sure
why the first few proofs in the ToyList theory went
through without ``from prems'' but these both seem 
to need that clause.  Go figure.  *}

datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"

consts mirror :: "'a tree => 'a tree"
primrec
"mirror Tip = Tip"
"mirror (Node l a r) = Node (mirror r) a (mirror l)"

lemma mirror_mirror: "mirror(mirror t) = t" (is "?mm t")
proof (induct t)
  show "?mm Tip" by simp
next
  fix l a r assume "?mm l" "?mm r"
  from prems show "?mm (Node l a r)" by simp
qed

consts flatten:: "'a tree => 'a list"
primrec
"flatten Tip = []"
"flatten (Node l a r) = (flatten l)@[a]@(flatten r)"

lemma "flatten(mirror t) = rev(flatten t)" (is "?P t")
proof (induct t)
  show "?P Tip" by simp
next
  fix l a r assume "?P l" "?P r"
  from prems show "?P (Node l a r)" by simp
qed

end

lemma mirror_mirror:

  mirror (mirror t) = t

lemma

  flatten (mirror t) = rev (flatten t)