nipkow@9645: (*<*)
haftmann@16417: theory Nested0 imports Main begin
nipkow@9645: (*>*)
nipkow@9645: 
nipkow@9645: text{*
paulson@11494: \index{datatypes!nested}%
nipkow@9645: In \S\ref{sec:nested-datatype} we defined the datatype of terms
nipkow@9645: *}
nipkow@9645: 
nipkow@9645: datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"
nipkow@9645: 
nipkow@9645: text{*\noindent
nipkow@9645: and closed with the observation that the associated schema for the definition
nipkow@9645: of primitive recursive functions leads to overly verbose definitions. Moreover,
nipkow@9645: if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
paulson@10885: you needed to declare essentially the same function as @{term"rev"}
nipkow@11196: and prove many standard properties of list reversal all over again. 
paulson@10885: We will now show you how \isacommand{recdef} can simplify
nipkow@9645: definitions and proofs about nested recursive datatypes. As an example we
nipkow@9754: choose exercise~\ref{ex:trev-trev}:
nipkow@9645: *}
nipkow@10186: 
nipkow@10186: consts trev  :: "('a,'b)term \<Rightarrow> ('a,'b)term"
nipkow@10186: (*<*)end(*>*)