summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Doc/Tutorial/Datatype/Fundata.thy

author | wenzelm |

Tue, 28 Aug 2012 18:57:32 +0200 | |

changeset 48985 | 5386df44a037 |

parent 27015 | doc-src/TutorialI/Datatype/Fundata.thy@f8537d69f514 |

child 58305 | 57752a91eec4 |

permissions | -rw-r--r-- |

renamed doc-src to src/Doc;
renamed TutorialI to Tutorial;

(*<*) theory Fundata imports Main begin (*>*) datatype ('a,'i)bigtree = Tip | Br 'a "'i \<Rightarrow> ('a,'i)bigtree" text{*\noindent 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" where "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) done (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; apply(induct_tac T, rename_tac[2] F)(*>*) txt{*\noindent Because of the function type, the proof state after induction looks unusual. Notice the quantified induction hypothesis: @{subgoals[display,indent=0]} *} (*<*) oops end (*>*)