10 *} |
10 *} |
11 (*<*)hide const Var(*>*) |
11 (*<*)hide const Var(*>*) |
12 datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"; |
12 datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"; |
13 |
13 |
14 text{*\noindent |
14 text{*\noindent |
15 Note that we need to quote @{text"term"} on the left to avoid confusion with |
15 Note that we need to quote @{text term} on the left to avoid confusion with |
16 the command \isacommand{term}. |
16 the Isabelle command \isacommand{term}. |
17 Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of |
17 Parameter @{typ"'a"} is the type of variables and @{typ"'b"} the type of |
18 function symbols. |
18 function symbols. |
19 A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g |
19 A mathematical term like $f(x,g(y))$ becomes @{term"App f [Var x, App g |
20 [Var y]]"}, where @{term"f"}, @{term"g"}, @{term"x"}, @{term"y"} are |
20 [Var y]]"}, where @{term f}, @{term g}, @{term x}, @{term y} are |
21 suitable values, e.g.\ numbers or strings. |
21 suitable values, e.g.\ numbers or strings. |
22 |
22 |
23 What complicates the definition of @{text"term"} is the nested occurrence of |
23 What complicates the definition of @{text term} is the nested occurrence of |
24 @{text"term"} inside @{text"list"} on the right-hand side. In principle, |
24 @{text term} inside @{text list} on the right-hand side. In principle, |
25 nested recursion can be eliminated in favour of mutual recursion by unfolding |
25 nested recursion can be eliminated in favour of mutual recursion by unfolding |
26 the offending datatypes, here @{text"list"}. The result for @{text"term"} |
26 the offending datatypes, here @{text list}. The result for @{text term} |
27 would be something like |
27 would be something like |
28 \medskip |
28 \medskip |
29 |
29 |
30 \input{Datatype/document/unfoldnested.tex} |
30 \input{Datatype/document/unfoldnested.tex} |
31 \medskip |
31 \medskip |
32 |
32 |
33 \noindent |
33 \noindent |
34 Although we do not recommend this unfolding to the user, it shows how to |
34 Although we do not recommend this unfolding to the user, it shows how to |
35 simulate nested recursion by mutual recursion. |
35 simulate nested recursion by mutual recursion. |
36 Now we return to the initial definition of @{text"term"} using |
36 Now we return to the initial definition of @{text term} using |
37 nested recursion. |
37 nested recursion. |
38 |
38 |
39 Let us define a substitution function on terms. Because terms involve term |
39 Let us define a substitution function on terms. Because terms involve term |
40 lists, we need to define two substitution functions simultaneously: |
40 lists, we need to define two substitution functions simultaneously: |
41 *} |
41 *} |
42 |
42 |
43 consts |
43 consts |
44 subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term \\<Rightarrow> ('a,'b)term" |
44 subst :: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term \<Rightarrow> ('a,'b)term" |
45 substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list"; |
45 substs:: "('a\<Rightarrow>('a,'b)term) \<Rightarrow> ('a,'b)term list \<Rightarrow> ('a,'b)term list"; |
46 |
46 |
47 primrec |
47 primrec |
48 "subst s (Var x) = s x" |
48 "subst s (Var x) = s x" |
49 subst_App: |
49 subst_App: |
50 "subst s (App f ts) = App f (substs s ts)" |
50 "subst s (App f ts) = App f (substs s ts)" |
51 |
51 |
52 "substs s [] = []" |
52 "substs s [] = []" |
53 "substs s (t # ts) = subst s t # substs s ts"; |
53 "substs s (t # ts) = subst s t # substs s ts"; |
54 |
54 |
55 text{*\noindent |
55 text{*\noindent |
56 (Please ignore the label @{thm[source]subst_App} for the moment.) |
56 Individual equations in a primrec definition may be named as shown for @{thm[source]subst_App}. |
|
57 The significance of this device will become apparent below. |
57 |
58 |
58 Similarly, when proving a statement about terms inductively, we need |
59 Similarly, when proving a statement about terms inductively, we need |
59 to prove a related statement about term lists simultaneously. For example, |
60 to prove a related statement about term lists simultaneously. For example, |
60 the fact that the identity substitution does not change a term needs to be |
61 the fact that the identity substitution does not change a term needs to be |
61 strengthened and proved as follows: |
62 strengthened and proved as follows: |
62 *} |
63 *} |
63 |
64 |
64 lemma "subst Var t = (t ::('a,'b)term) \\<and> |
65 lemma "subst Var t = (t ::('a,'b)term) \<and> |
65 substs Var ts = (ts::('a,'b)term list)"; |
66 substs Var ts = (ts::('a,'b)term list)"; |
66 by(induct_tac t and ts, simp_all); |
67 apply(induct_tac t and ts, simp_all); |
|
68 done |
67 |
69 |
68 text{*\noindent |
70 text{*\noindent |
69 Note that @{term"Var"} is the identity substitution because by definition it |
71 Note that @{term Var} is the identity substitution because by definition it |
70 leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also |
72 leaves variables unchanged: @{prop"subst Var (Var x) = Var x"}. Note also |
71 that the type annotations are necessary because otherwise there is nothing in |
73 that the type annotations are necessary because otherwise there is nothing in |
72 the goal to enforce that both halves of the goal talk about the same type |
74 the goal to enforce that both halves of the goal talk about the same type |
73 parameters @{text"('a,'b)"}. As a result, induction would fail |
75 parameters @{text"('a,'b)"}. As a result, induction would fail |
74 because the two halves of the goal would be unrelated. |
76 because the two halves of the goal would be unrelated. |
80 Correct this statement (you will find that it does not type-check), |
82 Correct this statement (you will find that it does not type-check), |
81 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition; |
83 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition; |
82 its definition is found in theorem @{thm[source]o_def}). |
84 its definition is found in theorem @{thm[source]o_def}). |
83 \end{exercise} |
85 \end{exercise} |
84 \begin{exercise}\label{ex:trev-trev} |
86 \begin{exercise}\label{ex:trev-trev} |
85 Define a function @{text"trev"} of type @{typ"('a,'b)term => ('a,'b)term"} |
87 Define a function @{term trev} of type @{typ"('a,'b)term => ('a,'b)term"} |
86 that recursively reverses the order of arguments of all function symbols in a |
88 that recursively reverses the order of arguments of all function symbols in a |
87 term. Prove that @{prop"trev(trev t) = t"}. |
89 term. Prove that @{prop"trev(trev t) = t"}. |
88 \end{exercise} |
90 \end{exercise} |
89 |
91 |
90 The experienced functional programmer may feel that our above definition of |
92 The experienced functional programmer may feel that our above definition of |
91 @{term"subst"} is unnecessarily complicated in that @{term"substs"} is |
93 @{term subst} is unnecessarily complicated in that @{term substs} is |
92 completely unnecessary. The @{term"App"}-case can be defined directly as |
94 completely unnecessary. The @{term App}-case can be defined directly as |
93 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"} |
95 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"} |
94 where @{term"map"} is the standard list function such that |
96 where @{term"map"} is the standard list function such that |
95 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle |
97 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle |
96 insists on the above fixed format. Fortunately, we can easily \emph{prove} |
98 insists on the above fixed format. Fortunately, we can easily \emph{prove} |
97 that the suggested equation holds: |
99 that the suggested equation holds: |
98 *} |
100 *} |
99 |
101 |
100 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" |
102 lemma [simp]: "subst s (App f ts) = App f (map (subst s) ts)" |
101 by(induct_tac ts, simp_all) |
103 apply(induct_tac ts, simp_all) |
|
104 done |
102 |
105 |
103 text{*\noindent |
106 text{*\noindent |
104 What is more, we can now disable the old defining equation as a |
107 What is more, we can now disable the old defining equation as a |
105 simplification rule: |
108 simplification rule: |
106 *} |
109 *} |
107 |
110 |
108 declare subst_App [simp del] |
111 declare subst_App [simp del] |
109 |
112 |
110 text{*\noindent |
113 text{*\noindent |
111 The advantage is that now we have replaced @{term"substs"} by |
114 The advantage is that now we have replaced @{term substs} by |
112 @{term"map"}, we can profit from the large number of pre-proved lemmas |
115 @{term map}, we can profit from the large number of pre-proved lemmas |
113 about @{term"map"}. Unfortunately inductive proofs about type |
116 about @{term map}. Unfortunately inductive proofs about type |
114 @{text"term"} are still awkward because they expect a conjunction. One |
117 @{text term} are still awkward because they expect a conjunction. One |
115 could derive a new induction principle as well (see |
118 could derive a new induction principle as well (see |
116 \S\ref{sec:derive-ind}), but turns out to be simpler to define |
119 \S\ref{sec:derive-ind}), but turns out to be simpler to define |
117 functions by \isacommand{recdef} instead of \isacommand{primrec}. |
120 functions by \isacommand{recdef} instead of \isacommand{primrec}. |
118 The details are explained in \S\ref{sec:advanced-recdef} below. |
121 The details are explained in \S\ref{sec:advanced-recdef} below. |
119 |
122 |
120 Of course, you may also combine mutual and nested recursion. For example, |
123 Of course, you may also combine mutual and nested recursion. For example, |
121 constructor @{text"Sum"} in \S\ref{sec:datatype-mut-rec} could take a list of |
124 constructor @{text Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
122 expressions as its argument: @{text"Sum"}~@{typ[quotes]"'a aexp list"}. |
125 expressions as its argument: @{text Sum}~@{typ[quotes]"'a aexp list"}. |
123 *} |
126 *} |
124 (*<*) |
127 (*<*) |
125 end |
128 end |
126 (*>*) |
129 (*>*) |