doc-src/TutorialI/Recdef/Nested0.thy
author wenzelm
Wed, 18 Aug 2010 23:44:50 +0200
changeset 38479 e628da370072
parent 16417 9bc16273c2d4
permissions -rw-r--r--
more efficient Markup_Tree, based on branches sorted by quasi-order; renamed markup_node.scala to markup_tree.scala and classes/objects accordingly; Position.Range: produce actual Text.Range; Symbol.Index.decode: convert 1-based Isabelle offsets here; added static Command.range; simplified Command.markup; Document_Model.token_marker: flatten markup at most once; tuned;

(*<*)
theory Nested0 imports Main begin
(*>*)

text{*
\index{datatypes!nested}%
In \S\ref{sec:nested-datatype} we defined the datatype of terms
*}

datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"

text{*\noindent
and closed with the observation that the associated schema for the definition
of primitive recursive functions leads to overly verbose definitions. Moreover,
if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
you needed to declare essentially the same function as @{term"rev"}
and prove many standard properties of list reversal all over again. 
We will now show you how \isacommand{recdef} can simplify
definitions and proofs about nested recursive datatypes. As an example we
choose exercise~\ref{ex:trev-trev}:
*}

consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term"
(*<*)end(*>*)