doc-src/TutorialI/Datatype/Nested.thy
author nipkow
Fri, 18 Aug 2000 10:34:08 +0200
changeset 9644 6b0b6b471855
parent 9541 d17c0b34d5c8
child 9689 751fde5307e4
permissions -rw-r--r--
*** empty log message ***
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     1
(*<*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     2
theory Nested = Main:;
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     3
(*>*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     4
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     5
text{*
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     6
So far, all datatypes had the property that on the right-hand side of their
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     7
definition they occurred only at the top-level, i.e.\ directly below a
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     8
constructor. This is not the case any longer for the following model of terms
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
     9
where function symbols can be applied to a list of arguments:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    10
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    11
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    12
datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    13
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    14
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    15
Note that we need to quote \isa{term} on the left to avoid confusion with
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    16
the command \isacommand{term}.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    17
Parameter \isa{'a} is the type of variables and \isa{'b} the type of
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    18
function symbols.
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
    19
A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
    20
  [Var y]]"}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    21
suitable values, e.g.\ numbers or strings.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    22
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    23
What complicates the definition of \isa{term} is the nested occurrence of
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    24
\isa{term} inside \isa{list} on the right-hand side. In principle,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    25
nested recursion can be eliminated in favour of mutual recursion by unfolding
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    26
the offending datatypes, here \isa{list}. The result for \isa{term}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    27
would be something like
8751
9ed0548177fb *** empty log message ***
nipkow
parents: 8745
diff changeset
    28
\medskip
9ed0548177fb *** empty log message ***
nipkow
parents: 8745
diff changeset
    29
9ed0548177fb *** empty log message ***
nipkow
parents: 8745
diff changeset
    30
\input{Datatype/document/unfoldnested.tex}
9ed0548177fb *** empty log message ***
nipkow
parents: 8745
diff changeset
    31
\medskip
9ed0548177fb *** empty log message ***
nipkow
parents: 8745
diff changeset
    32
9ed0548177fb *** empty log message ***
nipkow
parents: 8745
diff changeset
    33
\noindent
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
Although we do not recommend this unfolding to the user, it shows how to
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    35
simulate nested recursion by mutual recursion.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
Now we return to the initial definition of \isa{term} using
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    37
nested recursion.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    38
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    39
Let us define a substitution function on terms. Because terms involve term
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    40
lists, we need to define two substitution functions simultaneously:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    41
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    42
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    43
consts
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    44
subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term      \\<Rightarrow> ('a,'b)term"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    45
substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    46
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    47
primrec
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    48
  "subst s (Var x) = s x"
9644
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    49
  subst_App:
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
  "subst s (App f ts) = App f (substs s ts)"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    51
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    52
  "substs s [] = []"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    53
  "substs s (t # ts) = subst s t # substs s ts";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    54
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    55
text{*\noindent
9644
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    56
You should ignore the label \isa{subst\_App} for the moment.
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    57
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    58
Similarly, when proving a statement about terms inductively, we need
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    59
to prove a related statement about term lists simultaneously. For example,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    60
the fact that the identity substitution does not change a term needs to be
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    61
strengthened and proved as follows:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    62
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    63
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    64
lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    65
        substs Var ts = (ts::('a,'b)term list)";
9458
c613cd06d5cf apply. -> by
nipkow
parents: 8751
diff changeset
    66
by(induct_tac t and ts, auto);
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    67
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    68
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    69
Note that \isa{Var} is the identity substitution because by definition it
9541
d17c0b34d5c8 *** empty log message ***
nipkow
parents: 9458
diff changeset
    70
leaves variables unchanged: @{term"subst Var (Var x) = Var x"}. Note also
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    71
that the type annotations are necessary because otherwise there is nothing in
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    72
the goal to enforce that both halves of the goal talk about the same type
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    73
parameters \isa{('a,'b)}. As a result, induction would fail
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    74
because the two halves of the goal would be unrelated.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    75
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    76
\begin{exercise}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    77
The fact that substitution distributes over composition can be expressed
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    78
roughly as follows:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    79
\begin{ttbox}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    80
subst (f o g) t = subst f (subst g t)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    81
\end{ttbox}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    82
Correct this statement (you will find that it does not type-check),
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    83
strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    84
its definition is found in theorem \isa{o_def}).
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    85
\end{exercise}
9644
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    86
\begin{exercise}\label{ex:trev-trev}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    87
  Define a function \isa{trev} of type @{typ"('a,'b)term => ('a,'b)term"} that
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    88
  recursively reverses the order of arguments of all function symbols in a
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    89
  term. Prove that \isa{trev(trev t) = t}.
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    90
\end{exercise}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    91
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    92
The experienced functional programmer may feel that our above definition of
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    93
\isa{subst} is unnecessarily complicated in that \isa{substs} is completely
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    94
unnecessary. The @{term"App"}-case can be defined directly as
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    95
\begin{quote}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    96
@{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    97
\end{quote}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    98
where @{term"map"} is the standard list function such that
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
    99
\isa{map f [x1,...,xn] = [f x1,...,f xn]}. This is true, but Isabelle insists
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   100
on the above fixed format. Fortunately, we can easily \emph{prove} that the
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   101
suggested equation holds:
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   102
*}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   103
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   104
lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   105
by(induct_tac ts, auto)
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   106
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   107
text{*
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   108
What is more, we can now disable the old defining equation as a
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   109
simplification rule:
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   110
*}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   111
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   112
lemmas [simp del] = subst_App
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   113
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   114
text{*
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   115
The advantage is that now we have replaced @{term"substs"} by @{term"map"},
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   116
we can profit from the large number of pre-proved lemmas about @{term"map"}.
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   117
We illustrate this with an example, reversing terms:
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   118
*}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   119
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   120
consts trev  :: "('a,'b)term => ('a,'b)term"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   121
       trevs :: "('a,'b)term list => ('a,'b)term list"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   122
primrec   "trev (Var x) = Var x"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   123
trev_App: "trev (App f ts) = App f (trevs ts)"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   124
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   125
          "trevs [] = []"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   126
          "trevs (t#ts) = trevs ts @ [trev t]"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   127
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   128
text{*\noindent
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   129
Following the above methodology, we re-express \isa{trev\_App}:
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   130
*}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   131
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   132
lemma [simp]: "trev (App f ts) = App f (rev(map trev ts))"
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   133
by(induct_tac ts, auto)
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   134
lemmas [simp del] = trev_App
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   135
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   136
text{*\noindent
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   137
Now it becomes quite easy to prove @{term"trev(trev t) = t"}, except that we
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   138
still have to come up with the second half of the conjunction:
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   139
*}
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   140
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   141
lemma "trev(trev t) = (t::('a,'b)term) &
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   142
        map trev (map trev ts) = (ts::('a,'b)term list)";
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   143
by(induct_tac t and ts, auto simp add:rev_map);
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   144
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   145
text{*\noindent
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   146
Getting rid of this second conjunct requires deriving a new induction schema
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   147
for \isa{term}, which is beyond what we have learned so far. Please stay
6b0b6b471855 *** empty log message ***
nipkow
parents: 9541
diff changeset
   148
tuned, we will solve this final problem in \S\ref{sec:der-ind-schemas}.
8745
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   149
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   150
Of course, you may also combine mutual and nested recursion. For example,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   151
constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   152
expressions as its argument: \isa{Sum "'a aexp list"}.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   153
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   154
(*<*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   155
end
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
   156
(*>*)