1 (*<*) |
|
2 theory Nested imports ABexpr begin |
|
3 (*>*) |
|
4 |
|
5 text{* |
|
6 \index{datatypes!and nested recursion}% |
|
7 So far, all datatypes had the property that on the right-hand side of their |
|
8 definition they occurred only at the top-level: directly below a |
|
9 constructor. Now we consider \emph{nested recursion}, where the recursive |
|
10 datatype occurs nested in some other datatype (but not inside itself!). |
|
11 Consider the following model of terms |
|
12 where function symbols can be applied to a list of arguments: |
|
13 *} |
|
14 (*<*)hide_const Var(*>*) |
|
15 datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"; |
|
16 |
|
17 text{*\noindent |
|
18 Note that we need to quote @{text term} on the left to avoid confusion with |
|
19 the Isabelle command \isacommand{term}. |
|
20 Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of |
|
21 function symbols. |
|
22 A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g |
|
23 [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are |
|
24 suitable values, e.g.\ numbers or strings. |
|
25 |
|
26 What complicates the definition of @{text term} is the nested occurrence of |
|
27 @{text term} inside @{text list} on the right-hand side. In principle, |
|
28 nested recursion can be eliminated in favour of mutual recursion by unfolding |
|
29 the offending datatypes, here @{text list}. The result for @{text term} |
|
30 would be something like |
|
31 \medskip |
|
32 |
|
33 \input{unfoldnested.tex} |
|
34 \medskip |
|
35 |
|
36 \noindent |
|
37 Although we do not recommend this unfolding to the user, it shows how to |
|
38 simulate nested recursion by mutual recursion. |
|
39 Now we return to the initial definition of @{text term} using |
|
40 nested recursion. |
|
41 |
|
42 Let us define a substitution function on terms. Because terms involve term |
|
43 lists, we need to define two substitution functions simultaneously: |
|
44 *} |
|
45 |
|
46 primrec |
|
47 subst :: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term \<Rightarrow> ('v,'f)term" and |
|
48 substs:: "('v\<Rightarrow>('v,'f)term) \<Rightarrow> ('v,'f)term list \<Rightarrow> ('v,'f)term list" |
|
49 where |
|
50 "subst s (Var x) = s x" | |
|
51 subst_App: |
|
52 "subst s (App f ts) = App f (substs s ts)" | |
|
53 |
|
54 "substs s [] = []" | |
|
55 "substs s (t # ts) = subst s t # substs s ts" |
|
56 |
|
57 text{*\noindent |
|
58 Individual equations in a \commdx{primrec} definition may be |
|
59 named as shown for @{thm[source]subst_App}. |
|
60 The significance of this device will become apparent below. |
|
61 |
|
62 Similarly, when proving a statement about terms inductively, we need |
|
63 to prove a related statement about term lists simultaneously. For example, |
|
64 the fact that the identity substitution does not change a term needs to be |
|
65 strengthened and proved as follows: |
|
66 *} |
|
67 |
|
68 lemma subst_id(*<*)(*referred to from ABexpr*)(*>*): "subst Var t = (t ::('v,'f)term) \<and> |
|
69 substs Var ts = (ts::('v,'f)term list)"; |
|
70 apply(induct_tac t and ts, simp_all); |
|
71 done |
|
72 |
|
73 text{*\noindent |
|
74 Note that @{term Var} is the identity substitution because by definition it |
|
75 leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also |
|
76 that the type annotations are necessary because otherwise there is nothing in |
|
77 the goal to enforce that both halves of the goal talk about the same type |
|
78 parameters @{text"('v,'f)"}. As a result, induction would fail |
|
79 because the two halves of the goal would be unrelated. |
|
80 |
|
81 \begin{exercise} |
|
82 The fact that substitution distributes over composition can be expressed |
|
83 roughly as follows: |
|
84 @{text[display]"subst (f \<circ> g) t = subst f (subst g t)"} |
|
85 Correct this statement (you will find that it does not type-check), |
|
86 strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition; |
|
87 its definition is found in theorem @{thm[source]o_def}). |
|
88 \end{exercise} |
|
89 \begin{exercise}\label{ex:trev-trev} |
|
90 Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"} |
|
91 that recursively reverses the order of arguments of all function symbols in a |
|
92 term. Prove that @{prop"trev(trev t) = t"}. |
|
93 \end{exercise} |
|
94 |
|
95 The experienced functional programmer may feel that our definition of |
|
96 @{term subst} is too complicated in that @{const substs} is |
|
97 unnecessary. The @{term App}-case can be defined directly as |
|
98 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"} |
|
99 where @{term"map"} is the standard list function such that |
|
100 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle |
|
101 insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
|
102 that the suggested equation holds: |
|
103 *} |
|
104 (*<*) |
|
105 (* Exercise 1: *) |
|
106 lemma "subst ((subst f) \<circ> g) t = subst f (subst g t) \<and> |
|
107 substs ((subst f) \<circ> g) ts = substs f (substs g ts)" |
|
108 apply (induct_tac t and ts) |
|
109 apply (simp_all) |
|
110 done |
|
111 |
|
112 (* Exercise 2: *) |
|
113 |
|
114 primrec trev :: "('v,'f) term \<Rightarrow> ('v,'f) term" |
|
115 and trevs:: "('v,'f) term list \<Rightarrow> ('v,'f) term list" |
|
116 where |
|
117 "trev (Var v) = Var v" |
|
118 | "trev (App f ts) = App f (trevs ts)" |
|
119 | "trevs [] = []" |
|
120 | "trevs (t#ts) = (trevs ts) @ [(trev t)]" |
|
121 |
|
122 lemma [simp]: "\<forall> ys. trevs (xs @ ys) = (trevs ys) @ (trevs xs)" |
|
123 apply (induct_tac xs, auto) |
|
124 done |
|
125 |
|
126 lemma "trev (trev t) = (t::('v,'f)term) \<and> |
|
127 trevs (trevs ts) = (ts::('v,'f)term list)" |
|
128 apply (induct_tac t and ts, simp_all) |
|
129 done |
|
130 (*>*) |
|
131 |
|
132 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" |
|
133 apply(induct_tac ts, simp_all) |
|
134 done |
|
135 |
|
136 text{*\noindent |
|
137 What is more, we can now disable the old defining equation as a |
|
138 simplification rule: |
|
139 *} |
|
140 |
|
141 declare subst_App [simp del] |
|
142 |
|
143 text{*\noindent The advantage is that now we have replaced @{const |
|
144 substs} by @{const map}, we can profit from the large number of |
|
145 pre-proved lemmas about @{const map}. Unfortunately, inductive proofs |
|
146 about type @{text term} are still awkward because they expect a |
|
147 conjunction. One could derive a new induction principle as well (see |
|
148 \S\ref{sec:derive-ind}), but simpler is to stop using |
|
149 \isacommand{primrec} and to define functions with \isacommand{fun} |
|
150 instead. Simple uses of \isacommand{fun} are described in |
|
151 \S\ref{sec:fun} below. Advanced applications, including functions |
|
152 over nested datatypes like @{text term}, are discussed in a |
|
153 separate tutorial~\cite{isabelle-function}. |
|
154 |
|
155 Of course, you may also combine mutual and nested recursion of datatypes. For example, |
|
156 constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
|
157 expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}. |
|
158 *} |
|
159 (*<*)end(*>*) |
|