8745

1 
(*<*)

9792

2 
theory Nested = ABexpr:

8745

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 
*}

9933

11 
(*<*)hide const Var(*>*)

8745

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


13 


14 
text{*\noindent

10171

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


16 
the Isabelle command \isacommand{term}.

9792

17 
Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of

8745

18 
function symbols.

9541

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

10171

20 
[Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are

8745

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


22 

10171

23 
What complicates the definition of @{text term} is the nested occurrence of


24 
@{text term} inside @{text list} on the righthand side. In principle,

8745

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

10171

26 
the offending datatypes, here @{text list}. The result for @{text term}

8745

27 
would be something like

8751

28 
\medskip


29 


30 
\input{Datatype/document/unfoldnested.tex}


31 
\medskip


32 


33 
\noindent

8745

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


35 
simulate nested recursion by mutual recursion.

10171

36 
Now we return to the initial definition of @{text term} using

8745

37 
nested recursion.


38 


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


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


41 
*}


42 


43 
consts

10171

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


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

8745

46 


47 
primrec


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

9644

49 
subst_App:

8745

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


51 


52 
"substs s [] = []"


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


54 


55 
text{*\noindent

10171

56 
Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}.


57 
The significance of this device will become apparent below.

9644

58 

8745

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


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


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


62 
strengthened and proved as follows:


63 
*}


64 

10171

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

8745

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

10171

67 
apply(induct_tac t and ts, simp_all);


68 
done

8745

69 


70 
text{*\noindent

10171

71 
Note that @{term Var} is the identity substitution because by definition it

9792

72 
leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also

8745

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


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

9792

75 
parameters @{text"('a,'b)"}. As a result, induction would fail

8745

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


77 


78 
\begin{exercise}


79 
The fact that substitution distributes over composition can be expressed


80 
roughly as follows:

10178

81 
@{text[display]"subst (f \<circ> g) t = subst f (subst g t)"}

8745

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

10178

83 
strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition;

9792

84 
its definition is found in theorem @{thm[source]o_def}).

8745

85 
\end{exercise}

9644

86 
\begin{exercise}\label{ex:trevtrev}

10171

87 
Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"}

9792

88 
that recursively reverses the order of arguments of all function symbols in a


89 
term. Prove that @{prop"trev(trev t) = t"}.

9644

90 
\end{exercise}


91 


92 
The experienced functional programmer may feel that our above definition of

10171

93 
@{term subst} is unnecessarily complicated in that @{term substs} is


94 
completely unnecessary. The @{term App}case can be defined directly as

9644

95 
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}


96 
where @{term"map"} is the standard list function such that

9792

97 
@{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle


98 
insists on the above fixed format. Fortunately, we can easily \emph{prove}


99 
that the suggested equation holds:

9644

100 
*}


101 


102 
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"

10171

103 
apply(induct_tac ts, simp_all)


104 
done

9644

105 

9689

106 
text{*\noindent

9644

107 
What is more, we can now disable the old defining equation as a


108 
simplification rule:


109 
*}


110 

9933

111 
declare subst_App [simp del]

9644

112 


113 
text{*\noindent

10171

114 
The advantage is that now we have replaced @{term substs} by


115 
@{term map}, we can profit from the large number of preproved lemmas


116 
about @{term map}. Unfortunately inductive proofs about type


117 
@{text term} are still awkward because they expect a conjunction. One

9689

118 
could derive a new induction principle as well (see


119 
\S\ref{sec:deriveind}), but turns out to be simpler to define


120 
functions by \isacommand{recdef} instead of \isacommand{primrec}.

10186

121 
The details are explained in \S\ref{sec:nestedrecdef} below.

8745

122 


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

10171

124 
constructor @{text Sum} in \S\ref{sec:datatypemutrec} could take a list of


125 
expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}.

8745

126 
*}


127 
(*<*)


128 
end

10171

129 
(*>*) 