author | wenzelm |
Tue, 07 Oct 2014 22:35:11 +0200 | |
changeset 58620 | 7435b6a3f72e |
parent 58305 | 57752a91eec4 |
child 58860 | fee7cfa69c50 |
permissions | -rw-r--r-- |
8745 | 1 |
(*<*) |
16417 | 2 |
theory Nested imports ABexpr begin |
8745 | 3 |
(*>*) |
4 |
||
5 |
text{* |
|
11458 | 6 |
\index{datatypes!and nested recursion}% |
8745 | 7 |
So far, all datatypes had the property that on the right-hand side of their |
11458 | 8 |
definition they occurred only at the top-level: directly below a |
11256 | 9 |
constructor. Now we consider \emph{nested recursion}, where the recursive |
11310 | 10 |
datatype occurs nested in some other datatype (but not inside itself!). |
11256 | 11 |
Consider the following model of terms |
8745 | 12 |
where function symbols can be applied to a list of arguments: |
13 |
*} |
|
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
27318
diff
changeset
|
14 |
(*<*)hide_const Var(*>*) |
10971 | 15 |
datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"; |
8745 | 16 |
|
17 |
text{*\noindent |
|
10171 | 18 |
Note that we need to quote @{text term} on the left to avoid confusion with |
19 |
the Isabelle command \isacommand{term}. |
|
10971 | 20 |
Parameter @{typ"'v"} is the type of variables and @{typ"'f"} the type of |
8745 | 21 |
function symbols. |
9541 | 22 |
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g |
10171 | 23 |
[Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are |
8745 | 24 |
suitable values, e.g.\ numbers or strings. |
25 |
||
10171 | 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, |
|
8745 | 28 |
nested recursion can be eliminated in favour of mutual recursion by unfolding |
10171 | 29 |
the offending datatypes, here @{text list}. The result for @{text term} |
8745 | 30 |
would be something like |
8751 | 31 |
\medskip |
32 |
||
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
48523
diff
changeset
|
33 |
\input{unfoldnested.tex} |
8751 | 34 |
\medskip |
35 |
||
36 |
\noindent |
|
8745 | 37 |
Although we do not recommend this unfolding to the user, it shows how to |
38 |
simulate nested recursion by mutual recursion. |
|
10171 | 39 |
Now we return to the initial definition of @{text term} using |
8745 | 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 |
||
27015 | 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)" | |
|
8745 | 53 |
|
27015 | 54 |
"substs s [] = []" | |
55 |
"substs s (t # ts) = subst s t # substs s ts" |
|
8745 | 56 |
|
57 |
text{*\noindent |
|
11458 | 58 |
Individual equations in a \commdx{primrec} definition may be |
59 |
named as shown for @{thm[source]subst_App}. |
|
10171 | 60 |
The significance of this device will become apparent below. |
9644 | 61 |
|
8745 | 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 |
||
12334 | 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)"; |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
48985
diff
changeset
|
70 |
apply(induct_tac t and ts rule: subst.induct substs.induct, simp_all); |
10171 | 71 |
done |
8745 | 72 |
|
73 |
text{*\noindent |
|
10171 | 74 |
Note that @{term Var} is the identity substitution because by definition it |
9792 | 75 |
leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also |
8745 | 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 |
|
10971 | 78 |
parameters @{text"('v,'f)"}. As a result, induction would fail |
8745 | 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: |
|
10178 | 84 |
@{text[display]"subst (f \<circ> g) t = subst f (subst g t)"} |
8745 | 85 |
Correct this statement (you will find that it does not type-check), |
10178 | 86 |
strengthen it, and prove it. (Note: @{text"\<circ>"} is function composition; |
9792 | 87 |
its definition is found in theorem @{thm[source]o_def}). |
8745 | 88 |
\end{exercise} |
9644 | 89 |
\begin{exercise}\label{ex:trev-trev} |
10971 | 90 |
Define a function @{term trev} of type @{typ"('v,'f)term => ('v,'f)term"} |
9792 | 91 |
that recursively reverses the order of arguments of all function symbols in a |
92 |
term. Prove that @{prop"trev(trev t) = t"}. |
|
9644 | 93 |
\end{exercise} |
94 |
||
10795 | 95 |
The experienced functional programmer may feel that our definition of |
15904 | 96 |
@{term subst} is too complicated in that @{const substs} is |
10795 | 97 |
unnecessary. The @{term App}-case can be defined directly as |
9644 | 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 |
|
9792 | 100 |
@{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle |
10795 | 101 |
insists on the conjunctive format. Fortunately, we can easily \emph{prove} |
9792 | 102 |
that the suggested equation holds: |
9644 | 103 |
*} |
12334 | 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)" |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
48985
diff
changeset
|
108 |
apply (induct_tac t and ts rule: subst.induct substs.induct) |
12334 | 109 |
apply (simp_all) |
110 |
done |
|
111 |
||
112 |
(* Exercise 2: *) |
|
113 |
||
39795 | 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)]" |
|
12334 | 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)" |
|
58305
57752a91eec4
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
blanchet
parents:
48985
diff
changeset
|
128 |
apply (induct_tac t and ts rule: trev.induct trevs.induct, simp_all) |
12334 | 129 |
done |
130 |
(*>*) |
|
9644 | 131 |
|
132 |
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" |
|
10171 | 133 |
apply(induct_tac ts, simp_all) |
134 |
done |
|
9644 | 135 |
|
9689 | 136 |
text{*\noindent |
9644 | 137 |
What is more, we can now disable the old defining equation as a |
138 |
simplification rule: |
|
139 |
*} |
|
140 |
||
9933 | 141 |
declare subst_App [simp del] |
9644 | 142 |
|
25281
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
143 |
text{*\noindent The advantage is that now we have replaced @{const |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
144 |
substs} by @{const map}, we can profit from the large number of |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
145 |
pre-proved lemmas about @{const map}. Unfortunately, inductive proofs |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
146 |
about type @{text term} are still awkward because they expect a |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
147 |
conjunction. One could derive a new induction principle as well (see |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
148 |
\S\ref{sec:derive-ind}), but simpler is to stop using |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
149 |
\isacommand{primrec} and to define functions with \isacommand{fun} |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
150 |
instead. Simple uses of \isacommand{fun} are described in |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
151 |
\S\ref{sec:fun} below. Advanced applications, including functions |
8d309beb66d6
removed advanced recdef section and replaced it by citation of Alex's tutorial.
nipkow
parents:
25261
diff
changeset
|
152 |
over nested datatypes like @{text term}, are discussed in a |
58620 | 153 |
separate tutorial~@{cite "isabelle-function"}. |
8745 | 154 |
|
10971 | 155 |
Of course, you may also combine mutual and nested recursion of datatypes. For example, |
10171 | 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"}. |
|
8745 | 158 |
*} |
12334 | 159 |
(*<*)end(*>*) |