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