changeset 48985 5386df44a037
parent 27015 f8537d69f514
child 58305 57752a91eec4
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/Datatype/Fundata.thy	Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,50 @@
+theory Fundata imports Main begin
+datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree"
+Parameter @{typ"'a"} is the type of values stored in
+the @{term Br}anches of the tree, whereas @{typ"'i"} is the index
+type over which the tree branches. If @{typ"'i"} is instantiated to
+@{typ"bool"}, the result is a binary tree; if it is instantiated to
+@{typ"nat"}, we have an infinitely branching tree because each node
+has as many subtrees as there are natural numbers. How can we possibly
+write down such a tree? Using functional notation! For example, the term
+@{term[display]"Br (0::nat) (\<lambda>i. Br i (\<lambda>n. Tip))"}
+of type @{typ"(nat,nat)bigtree"} is the tree whose
+root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
+has merely @{term"Tip"}s as further subtrees.
+Function @{term"map_bt"} applies a function to all labels in a @{text"bigtree"}:
+primrec map_bt :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a,'i)bigtree \<Rightarrow> ('b,'i)bigtree"
+"map_bt f Tip      = Tip" |
+"map_bt f (Br a F) = Br (f a) (\<lambda>i. map_bt f (F i))"
+text{*\noindent This is a valid \isacommand{primrec} definition because the
+recursive calls of @{term"map_bt"} involve only subtrees of
+@{term"F"}, which is itself a subterm of the left-hand side. Thus termination
+is assured.  The seasoned functional programmer might try expressing
+@{term"%i. map_bt f (F i)"} as @{term"map_bt f o F"}, which Isabelle 
+however will reject.  Applying @{term"map_bt"} to only one of its arguments
+makes the termination proof less obvious.
+The following lemma has a simple proof by induction:  *}
+lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
+apply(induct_tac T, simp_all)
+(*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
+apply(induct_tac T, rename_tac[2] F)(*>*)
+Because of the function type, the proof state after induction looks unusual.
+Notice the quantified induction hypothesis: