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