8745

1 
(*<*)


2 
theory Nested = Main:;


3 
(*>*)


4 


5 
text{*


6 
So far, all datatypes had the property that on the righthand side of their


7 
definition they occurred only at the toplevel, i.e.\ directly below a


8 
constructor. This is not the case any longer for the following model of terms


9 
where function symbols can be applied to a list of arguments:


10 
*}


11 


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


13 


14 
text{*\noindent


15 
Note that we need to quote \isa{term} on the left to avoid confusion with


16 
the command \isacommand{term}.


17 
Parameter \isa{'a} is the type of variables and \isa{'b} the type of


18 
function symbols.


19 
A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g


20 
[Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are


21 
suitable values, e.g.\ numbers or strings.


22 


23 
What complicates the definition of \isa{term} is the nested occurrence of


24 
\isa{term} inside \isa{list} on the righthand side. In principle,


25 
nested recursion can be eliminated in favour of mutual recursion by unfolding


26 
the offending datatypes, here \isa{list}. The result for \isa{term}


27 
would be something like


28 
\begin{ttbox}


29 
\input{Datatype/tunfoldeddata}\end{ttbox}


30 
Although we do not recommend this unfolding to the user, it shows how to


31 
simulate nested recursion by mutual recursion.


32 
Now we return to the initial definition of \isa{term} using


33 
nested recursion.


34 


35 
Let us define a substitution function on terms. Because terms involve term


36 
lists, we need to define two substitution functions simultaneously:


37 
*}


38 


39 
consts


40 
subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term \\<Rightarrow> ('a,'b)term"


41 
substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";


42 


43 
primrec


44 
"subst s (Var x) = s x"


45 
"subst s (App f ts) = App f (substs s ts)"


46 


47 
"substs s [] = []"


48 
"substs s (t # ts) = subst s t # substs s ts";


49 


50 
text{*\noindent


51 
Similarly, when proving a statement about terms inductively, we need


52 
to prove a related statement about term lists simultaneously. For example,


53 
the fact that the identity substitution does not change a term needs to be


54 
strengthened and proved as follows:


55 
*}


56 


57 
lemma "subst Var t = (t ::('a,'b)term) \\<and>


58 
substs Var ts = (ts::('a,'b)term list)";


59 
apply(induct_tac t and ts, auto).;


60 


61 
text{*\noindent


62 
Note that \isa{Var} is the identity substitution because by definition it


63 
leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also


64 
that the type annotations are necessary because otherwise there is nothing in


65 
the goal to enforce that both halves of the goal talk about the same type


66 
parameters \isa{('a,'b)}. As a result, induction would fail


67 
because the two halves of the goal would be unrelated.


68 


69 
\begin{exercise}


70 
The fact that substitution distributes over composition can be expressed


71 
roughly as follows:


72 
\begin{ttbox}


73 
subst (f o g) t = subst f (subst g t)


74 
\end{ttbox}


75 
Correct this statement (you will find that it does not typecheck),


76 
strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;


77 
its definition is found in theorem \isa{o_def}).


78 
\end{exercise}


79 


80 
Of course, you may also combine mutual and nested recursion. For example,


81 
constructor \isa{Sum} in \S\ref{sec:datatypemutrec} could take a list of


82 
expressions as its argument: \isa{Sum "'a aexp list"}.


83 
*}


84 
(*<*)


85 


86 
lemma "subst s (App f ts) = App f (map (subst s) ts)";


87 
apply(induct_tac ts, auto).;


88 


89 
end


90 
(*>*)
