doc-src/TutorialI/Datatype/Nested.thy
author nipkow
Wed, 19 Apr 2000 11:56:31 +0200
changeset 8745 13b32661dde4
child 8751 9ed0548177fb
permissions -rw-r--r--
I wonder which files i forgot.
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.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    19
A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    20
  [Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
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
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    28
\begin{ttbox}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    29
\input{Datatype/tunfoldeddata}\end{ttbox}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    30
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
    31
simulate nested recursion by mutual recursion.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    32
Now we return to the initial definition of \isa{term} using
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    33
nested recursion.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    34
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    35
Let us define a substitution function on terms. Because terms involve term
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    36
lists, we need to define two substitution functions simultaneously:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    37
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    38
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    39
consts
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    40
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
    41
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
    42
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    43
primrec
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    44
  "subst s (Var x) = s x"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    45
  "subst s (App f ts) = App f (substs s ts)"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    46
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    47
  "substs s [] = []"
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    48
  "substs s (t # ts) = subst s t # substs s ts";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    49
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    50
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    51
Similarly, when proving a statement about terms inductively, we need
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    52
to prove a related statement about term lists simultaneously. For example,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    53
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
    54
strengthened and proved as follows:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    55
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    56
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    57
lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    58
        substs Var ts = (ts::('a,'b)term list)";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    59
apply(induct_tac t and ts, auto).;
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    60
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    61
text{*\noindent
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    62
Note that \isa{Var} is the identity substitution because by definition it
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    63
leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    64
that the type annotations are necessary because otherwise there is nothing in
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    65
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
    66
parameters \isa{('a,'b)}. As a result, induction would fail
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    67
because the two halves of the goal would be unrelated.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    68
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    69
\begin{exercise}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    70
The fact that substitution distributes over composition can be expressed
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    71
roughly as follows:
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    72
\begin{ttbox}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    73
subst (f o g) t = subst f (subst g t)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    74
\end{ttbox}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    75
Correct this statement (you will find that it does not type-check),
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    76
strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    77
its definition is found in theorem \isa{o_def}).
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    78
\end{exercise}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    79
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    80
Of course, you may also combine mutual and nested recursion. For example,
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    81
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
    82
expressions as its argument: \isa{Sum "'a aexp list"}.
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    83
*}
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    84
(*<*)
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    85
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    86
lemma "subst s (App f ts) = App f (map (subst s) ts)";
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    87
apply(induct_tac ts, auto).;
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    88
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    89
end
13b32661dde4 I wonder which files i forgot.
nipkow
parents:
diff changeset
    90
(*>*)