author | berghofe |
Thu, 12 Jan 2012 00:14:20 +0100 | |
changeset 46192 | 93eaaacc1955 |
parent 43564 | 9864182c6bad |
permissions | -rw-r--r-- |
10365 | 1 |
% |
11187 | 2 |
\begin{isabellebody}% |
3 |
\def\isabellecontext{Advanced}% |
|
17056 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
23848 | 10 |
% |
17056 | 11 |
\endisatagtheory |
12 |
{\isafoldtheory}% |
|
13 |
% |
|
14 |
\isadelimtheory |
|
15 |
% |
|
16 |
\endisadelimtheory |
|
23848 | 17 |
% |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
18 |
\isadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
19 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
20 |
\endisadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
21 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
22 |
\isatagML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
23 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
24 |
\endisatagML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
25 |
{\isafoldML}% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
26 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
27 |
\isadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
28 |
% |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
29 |
\endisadelimML |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
40406
diff
changeset
|
30 |
% |
23848 | 31 |
\begin{isamarkuptext}% |
32 |
The premises of introduction rules may contain universal quantifiers and |
|
33 |
monotone functions. A universal quantifier lets the rule |
|
34 |
refer to any number of instances of |
|
35 |
the inductively defined set. A monotone function lets the rule refer |
|
36 |
to existing constructions (such as ``list of'') over the inductively defined |
|
37 |
set. The examples below show how to use the additional expressiveness |
|
38 |
and how to reason from the resulting definitions.% |
|
39 |
\end{isamarkuptext}% |
|
40 |
\isamarkuptrue% |
|
41 |
% |
|
42 |
\isamarkupsubsection{Universal Quantifiers in Introduction Rules \label{sec:gterm-datatype}% |
|
43 |
} |
|
44 |
\isamarkuptrue% |
|
45 |
% |
|
46 |
\begin{isamarkuptext}% |
|
47 |
\index{ground terms example|(}% |
|
48 |
\index{quantifiers!and inductive definitions|(}% |
|
49 |
As a running example, this section develops the theory of \textbf{ground |
|
50 |
terms}: terms constructed from constant and function |
|
51 |
symbols but not variables. To simplify matters further, we regard a |
|
52 |
constant as a function applied to the null argument list. Let us declare a |
|
53 |
datatype \isa{gterm} for the type of ground terms. It is a type constructor |
|
54 |
whose argument is a type of function symbols.% |
|
55 |
\end{isamarkuptext}% |
|
56 |
\isamarkuptrue% |
|
17175 | 57 |
\isacommand{datatype}\isamarkupfalse% |
40406 | 58 |
\ {\isaliteral{27}{\isacharprime}}f\ gterm\ {\isaliteral{3D}{\isacharequal}}\ Apply\ {\isaliteral{27}{\isacharprime}}f\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ gterm\ list{\isaliteral{22}{\isachardoublequoteclose}}% |
23848 | 59 |
\begin{isamarkuptext}% |
60 |
To try it out, we declare a datatype of some integer operations: |
|
61 |
integer constants, the unary minus operator and the addition |
|
62 |
operator.% |
|
63 |
\end{isamarkuptext}% |
|
64 |
\isamarkuptrue% |
|
17175 | 65 |
\isacommand{datatype}\isamarkupfalse% |
40406 | 66 |
\ integer{\isaliteral{5F}{\isacharunderscore}}op\ {\isaliteral{3D}{\isacharequal}}\ Number\ int\ {\isaliteral{7C}{\isacharbar}}\ UnaryMinus\ {\isaliteral{7C}{\isacharbar}}\ Plus% |
23848 | 67 |
\begin{isamarkuptext}% |
40406 | 68 |
Now the type \isa{integer{\isaliteral{5F}{\isacharunderscore}}op\ gterm} denotes the ground |
23848 | 69 |
terms built over those symbols. |
70 |
||
71 |
The type constructor \isa{gterm} can be generalized to a function |
|
72 |
over sets. It returns |
|
73 |
the set of ground terms that can be formed over a set \isa{F} of function symbols. For |
|
74 |
example, we could consider the set of ground terms formed from the finite |
|
40406 | 75 |
set \isa{{\isaliteral{7B}{\isacharbraceleft}}Number\ {\isadigit{2}}{\isaliteral{2C}{\isacharcomma}}\ UnaryMinus{\isaliteral{2C}{\isacharcomma}}\ Plus{\isaliteral{7D}{\isacharbraceright}}}. |
23848 | 76 |
|
77 |
This concept is inductive. If we have a list \isa{args} of ground terms |
|
78 |
over~\isa{F} and a function symbol \isa{f} in \isa{F}, then we |
|
79 |
can apply \isa{f} to \isa{args} to obtain another ground term. |
|
80 |
The only difficulty is that the argument list may be of any length. Hitherto, |
|
81 |
each rule in an inductive definition referred to the inductively |
|
82 |
defined set a fixed number of times, typically once or twice. |
|
83 |
A universal quantifier in the premise of the introduction rule |
|
84 |
expresses that every element of \isa{args} belongs |
|
85 |
to our inductively defined set: is a ground term |
|
86 |
over~\isa{F}. The function \isa{set} denotes the set of elements in a given |
|
87 |
list.% |
|
88 |
\end{isamarkuptext}% |
|
89 |
\isamarkuptrue% |
|
40406 | 90 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
23733 | 91 |
\isanewline |
40406 | 92 |
\ \ gterms\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ set\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
93 |
\ \ \isakeyword{for}\ F\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23733 | 94 |
\isakeyword{where}\isanewline |
40406 | 95 |
step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\ \ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
96 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23848 | 97 |
\begin{isamarkuptext}% |
98 |
To demonstrate a proof from this definition, let us |
|
99 |
show that the function \isa{gterms} |
|
100 |
is \textbf{monotone}. We shall need this concept shortly.% |
|
101 |
\end{isamarkuptext}% |
|
102 |
\isamarkuptrue% |
|
17175 | 103 |
\isacommand{lemma}\isamarkupfalse% |
40406 | 104 |
\ gterms{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}F{\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}G\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ gterms\ F\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ gterms\ G{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
17056 | 105 |
% |
106 |
\isadelimproof |
|
107 |
% |
|
108 |
\endisadelimproof |
|
109 |
% |
|
110 |
\isatagproof |
|
17175 | 111 |
\isacommand{apply}\isamarkupfalse% |
112 |
\ clarify\isanewline |
|
113 |
\isacommand{apply}\isamarkupfalse% |
|
40406 | 114 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ gterms{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
17175 | 115 |
\isacommand{apply}\isamarkupfalse% |
116 |
\ blast\isanewline |
|
117 |
\isacommand{done}\isamarkupfalse% |
|
118 |
% |
|
17056 | 119 |
\endisatagproof |
120 |
{\isafoldproof}% |
|
121 |
% |
|
122 |
\isadelimproof |
|
123 |
% |
|
124 |
\endisadelimproof |
|
11866 | 125 |
% |
23848 | 126 |
\isadelimproof |
127 |
% |
|
128 |
\endisadelimproof |
|
129 |
% |
|
130 |
\isatagproof |
|
131 |
% |
|
132 |
\begin{isamarkuptxt}% |
|
133 |
Intuitively, this theorem says that |
|
134 |
enlarging the set of function symbols enlarges the set of ground |
|
135 |
terms. The proof is a trivial rule induction. |
|
136 |
First we use the \isa{clarify} method to assume the existence of an element of |
|
137 |
\isa{gterms\ F}. (We could have used \isa{intro\ subsetI}.) We then |
|
138 |
apply rule induction. Here is the resulting subgoal: |
|
11187 | 139 |
\begin{isabelle}% |
40406 | 140 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
141 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}F\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ G{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
142 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G% |
|
11173 | 143 |
\end{isabelle} |
23848 | 144 |
The assumptions state that \isa{f} belongs |
145 |
to~\isa{F}, which is included in~\isa{G}, and that every element of the list \isa{args} is |
|
146 |
a ground term over~\isa{G}. The \isa{blast} method finds this chain of reasoning easily.% |
|
147 |
\end{isamarkuptxt}% |
|
148 |
\isamarkuptrue% |
|
149 |
% |
|
150 |
\endisatagproof |
|
151 |
{\isafoldproof}% |
|
152 |
% |
|
153 |
\isadelimproof |
|
154 |
% |
|
155 |
\endisadelimproof |
|
156 |
% |
|
157 |
\begin{isamarkuptext}% |
|
158 |
\begin{warn} |
|
159 |
Why do we call this function \isa{gterms} instead |
|
160 |
of \isa{gterm}? A constant may have the same name as a type. However, |
|
161 |
name clashes could arise in the theorems that Isabelle generates. |
|
40406 | 162 |
Our choice of names keeps \isa{gterms{\isaliteral{2E}{\isachardot}}induct} separate from |
163 |
\isa{gterm{\isaliteral{2E}{\isachardot}}induct}. |
|
23848 | 164 |
\end{warn} |
10469 | 165 |
|
23848 | 166 |
Call a term \textbf{well-formed} if each symbol occurring in it is applied |
167 |
to the correct number of arguments. (This number is called the symbol's |
|
168 |
\textbf{arity}.) We can express well-formedness by |
|
169 |
generalizing the inductive definition of |
|
170 |
\isa{gterms}. |
|
171 |
Suppose we are given a function called \isa{arity}, specifying the arities |
|
172 |
of all symbols. In the inductive step, we have a list \isa{args} of such |
|
173 |
terms and a function symbol~\isa{f}. If the length of the list matches the |
|
174 |
function's arity then applying \isa{f} to \isa{args} yields a well-formed |
|
175 |
term.% |
|
176 |
\end{isamarkuptext}% |
|
177 |
\isamarkuptrue% |
|
40406 | 178 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
23848 | 179 |
\isanewline |
40406 | 180 |
\ \ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
181 |
\ \ \isakeyword{for}\ arity\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23848 | 182 |
\isakeyword{where}\isanewline |
40406 | 183 |
step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{3B}{\isacharsemicolon}}\ \ \isanewline |
184 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
185 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23848 | 186 |
\begin{isamarkuptext}% |
187 |
The inductive definition neatly captures the reasoning above. |
|
188 |
The universal quantification over the |
|
189 |
\isa{set} of arguments expresses that all of them are well-formed.% |
|
190 |
\index{quantifiers!and inductive definitions|)}% |
|
11187 | 191 |
\end{isamarkuptext}% |
17175 | 192 |
\isamarkuptrue% |
23848 | 193 |
% |
194 |
\isamarkupsubsection{Alternative Definition Using a Monotone Function% |
|
195 |
} |
|
196 |
\isamarkuptrue% |
|
197 |
% |
|
198 |
\begin{isamarkuptext}% |
|
199 |
\index{monotone functions!and inductive definitions|(}% |
|
200 |
An inductive definition may refer to the |
|
201 |
inductively defined set through an arbitrary monotone function. To |
|
202 |
demonstrate this powerful feature, let us |
|
203 |
change the inductive definition above, replacing the |
|
204 |
quantifier by a use of the function \isa{lists}. This |
|
205 |
function, from the Isabelle theory of lists, is analogous to the |
|
206 |
function \isa{gterms} declared above: if \isa{A} is a set then |
|
207 |
\isa{lists\ A} is the set of lists whose elements belong to |
|
208 |
\isa{A}. |
|
209 |
||
210 |
In the inductive definition of well-formed terms, examine the one |
|
211 |
introduction rule. The first premise states that \isa{args} belongs to |
|
212 |
the \isa{lists} of well-formed terms. This formulation is more |
|
213 |
direct, if more obscure, than using a universal quantifier.% |
|
214 |
\end{isamarkuptext}% |
|
215 |
\isamarkuptrue% |
|
40406 | 216 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
10365 | 217 |
\isanewline |
40406 | 218 |
\ \ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}f\ gterm\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
219 |
\ \ \isakeyword{for}\ arity\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
23848 | 220 |
\isakeyword{where}\isanewline |
40406 | 221 |
step{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ \ \isanewline |
222 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
223 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Apply\ f\ args{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
224 |
\isakeyword{monos}\ lists{\isaliteral{5F}{\isacharunderscore}}mono% |
|
11187 | 225 |
\begin{isamarkuptext}% |
40406 | 226 |
We cite the theorem \isa{lists{\isaliteral{5F}{\isacharunderscore}}mono} to justify |
23848 | 227 |
using the function \isa{lists}.% |
228 |
\footnote{This particular theorem is installed by default already, but we |
|
229 |
include the \isakeyword{monos} declaration in order to illustrate its syntax.} |
|
11187 | 230 |
\begin{isabelle}% |
40406 | 231 |
A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ lists\ A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ lists\ B\rulename{lists{\isaliteral{5F}{\isacharunderscore}}mono}% |
23848 | 232 |
\end{isabelle} |
233 |
Why must the function be monotone? An inductive definition describes |
|
234 |
an iterative construction: each element of the set is constructed by a |
|
235 |
finite number of introduction rule applications. For example, the |
|
236 |
elements of \isa{even} are constructed by finitely many applications of |
|
237 |
the rules |
|
238 |
\begin{isabelle}% |
|
40406 | 239 |
{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\isasep\isanewline% |
240 |
n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even% |
|
11187 | 241 |
\end{isabelle} |
23848 | 242 |
All references to a set in its |
243 |
inductive definition must be positive. Applications of an |
|
244 |
introduction rule cannot invalidate previous applications, allowing the |
|
245 |
construction process to converge. |
|
246 |
The following pair of rules do not constitute an inductive definition: |
|
247 |
\begin{trivlist} |
|
40406 | 248 |
\item \isa{{\isadigit{0}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even} |
249 |
\item \isa{n\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ even\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Suc\ n\ {\isaliteral{5C3C696E3E}{\isasymin}}\ even} |
|
23848 | 250 |
\end{trivlist} |
251 |
Showing that 4 is even using these rules requires showing that 3 is not |
|
252 |
even. It is far from trivial to show that this set of rules |
|
253 |
characterizes the even numbers. |
|
10469 | 254 |
|
23848 | 255 |
Even with its use of the function \isa{lists}, the premise of our |
256 |
introduction rule is positive: |
|
257 |
\begin{isabelle}% |
|
40406 | 258 |
args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}% |
23848 | 259 |
\end{isabelle} |
260 |
To apply the rule we construct a list \isa{args} of previously |
|
261 |
constructed well-formed terms. We obtain a |
|
262 |
new term, \isa{Apply\ f\ args}. Because \isa{lists} is monotone, |
|
263 |
applications of the rule remain valid as new terms are constructed. |
|
264 |
Further lists of well-formed |
|
265 |
terms become available and none are taken away.% |
|
266 |
\index{monotone functions!and inductive definitions|)}% |
|
267 |
\end{isamarkuptext}% |
|
268 |
\isamarkuptrue% |
|
269 |
% |
|
270 |
\isamarkupsubsection{A Proof of Equivalence% |
|
271 |
} |
|
272 |
\isamarkuptrue% |
|
273 |
% |
|
274 |
\begin{isamarkuptext}% |
|
275 |
We naturally hope that these two inductive definitions of ``well-formed'' |
|
276 |
coincide. The equality can be proved by separate inclusions in |
|
277 |
each direction. Each is a trivial rule induction.% |
|
11187 | 278 |
\end{isamarkuptext}% |
17175 | 279 |
\isamarkuptrue% |
280 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 281 |
\ {\isaliteral{22}{\isachardoublequoteopen}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
17056 | 282 |
% |
283 |
\isadelimproof |
|
284 |
% |
|
285 |
\endisadelimproof |
|
286 |
% |
|
287 |
\isatagproof |
|
17175 | 288 |
\isacommand{apply}\isamarkupfalse% |
23848 | 289 |
\ clarify\isanewline |
290 |
\isacommand{apply}\isamarkupfalse% |
|
40406 | 291 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
23848 | 292 |
\isacommand{apply}\isamarkupfalse% |
293 |
\ auto\isanewline |
|
294 |
\isacommand{done}\isamarkupfalse% |
|
295 |
% |
|
296 |
\endisatagproof |
|
297 |
{\isafoldproof}% |
|
298 |
% |
|
299 |
\isadelimproof |
|
300 |
% |
|
301 |
\endisadelimproof |
|
302 |
% |
|
303 |
\isadelimproof |
|
304 |
% |
|
305 |
\endisadelimproof |
|
306 |
% |
|
307 |
\isatagproof |
|
308 |
% |
|
309 |
\begin{isamarkuptxt}% |
|
310 |
The \isa{clarify} method gives |
|
40406 | 311 |
us an element of \isa{well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity} on which to perform |
23848 | 312 |
induction. The resulting subgoal can be proved automatically: |
313 |
\begin{isabelle}% |
|
40406 | 314 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
315 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\isanewline |
|
316 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ \ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity\ {\isaliteral{5C3C616E643E}{\isasymand}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
317 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
318 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity% |
|
23848 | 319 |
\end{isabelle} |
320 |
This proof resembles the one given in |
|
321 |
{\S}\ref{sec:gterm-datatype} above, especially in the form of the |
|
322 |
induction hypothesis. Next, we consider the opposite inclusion:% |
|
323 |
\end{isamarkuptxt}% |
|
324 |
\isamarkuptrue% |
|
325 |
% |
|
326 |
\endisatagproof |
|
327 |
{\isafoldproof}% |
|
328 |
% |
|
329 |
\isadelimproof |
|
330 |
% |
|
331 |
\endisadelimproof |
|
332 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 333 |
\ {\isaliteral{22}{\isachardoublequoteopen}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
23848 | 334 |
% |
335 |
\isadelimproof |
|
336 |
% |
|
337 |
\endisadelimproof |
|
338 |
% |
|
339 |
\isatagproof |
|
340 |
\isacommand{apply}\isamarkupfalse% |
|
341 |
\ clarify\isanewline |
|
342 |
\isacommand{apply}\isamarkupfalse% |
|
40406 | 343 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
23848 | 344 |
\isacommand{apply}\isamarkupfalse% |
345 |
\ auto\isanewline |
|
346 |
\isacommand{done}\isamarkupfalse% |
|
17175 | 347 |
% |
17056 | 348 |
\endisatagproof |
349 |
{\isafoldproof}% |
|
350 |
% |
|
351 |
\isadelimproof |
|
23848 | 352 |
% |
353 |
\endisadelimproof |
|
354 |
% |
|
355 |
\isadelimproof |
|
17056 | 356 |
% |
357 |
\endisadelimproof |
|
23848 | 358 |
% |
359 |
\isatagproof |
|
360 |
% |
|
361 |
\begin{isamarkuptxt}% |
|
27167 | 362 |
The proof script is virtually identical, |
363 |
but the subgoal after applying induction may be surprising: |
|
23848 | 364 |
\begin{isabelle}% |
40406 | 365 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x\ args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
366 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}args\isanewline |
|
367 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}}{\isaliteral{5C3C696E3E}{\isasymin}}\ lists\isanewline |
|
368 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C696E3E}{\isasymin}}\ \ }{\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\isanewline |
|
369 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C696E3E}{\isasymin}}\ \ {\isaliteral{28}{\isacharparenleft}}}{\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
370 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }length\ args\ {\isaliteral{3D}{\isacharequal}}\ arity\ f{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
371 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity% |
|
23848 | 372 |
\end{isabelle} |
373 |
The induction hypothesis contains an application of \isa{lists}. Using a |
|
374 |
monotone function in the inductive definition always has this effect. The |
|
375 |
subgoal may look uninviting, but fortunately |
|
376 |
\isa{lists} distributes over intersection: |
|
377 |
\begin{isabelle}% |
|
46192 | 378 |
lists\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ lists\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ lists\ B\rulename{lists{\isaliteral{5F}{\isacharunderscore}}Int{\isaliteral{5F}{\isacharunderscore}}eq}% |
23848 | 379 |
\end{isabelle} |
380 |
Thanks to this default simplification rule, the induction hypothesis |
|
381 |
is quickly replaced by its two parts: |
|
382 |
\begin{trivlist} |
|
40406 | 383 |
\item \isa{args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{27}{\isacharprime}}\ arity{\isaliteral{29}{\isacharparenright}}} |
384 |
\item \isa{args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ lists\ {\isaliteral{28}{\isacharparenleft}}well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm\ arity{\isaliteral{29}{\isacharparenright}}} |
|
23848 | 385 |
\end{trivlist} |
40406 | 386 |
Invoking the rule \isa{well{\isaliteral{5F}{\isacharunderscore}}formed{\isaliteral{5F}{\isacharunderscore}}gterm{\isaliteral{2E}{\isachardot}}step} completes the proof. The |
23848 | 387 |
call to \isa{auto} does all this work. |
388 |
||
389 |
This example is typical of how monotone functions |
|
390 |
\index{monotone functions} can be used. In particular, many of them |
|
391 |
distribute over intersection. Monotonicity implies one direction of |
|
392 |
this set equality; we have this theorem: |
|
393 |
\begin{isabelle}% |
|
40406 | 394 |
mono\ f\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ f\ B\rulename{mono{\isaliteral{5F}{\isacharunderscore}}Int}% |
23848 | 395 |
\end{isabelle}% |
396 |
\end{isamarkuptxt}% |
|
397 |
\isamarkuptrue% |
|
398 |
% |
|
399 |
\endisatagproof |
|
400 |
{\isafoldproof}% |
|
401 |
% |
|
402 |
\isadelimproof |
|
403 |
% |
|
404 |
\endisadelimproof |
|
405 |
% |
|
406 |
\isamarkupsubsection{Another Example of Rule Inversion% |
|
407 |
} |
|
408 |
\isamarkuptrue% |
|
409 |
% |
|
410 |
\begin{isamarkuptext}% |
|
411 |
\index{rule inversion|(}% |
|
412 |
Does \isa{gterms} distribute over intersection? We have proved that this |
|
40406 | 413 |
function is monotone, so \isa{mono{\isaliteral{5F}{\isacharunderscore}}Int} gives one of the inclusions. The |
23848 | 414 |
opposite inclusion asserts that if \isa{t} is a ground term over both of the |
415 |
sets |
|
416 |
\isa{F} and~\isa{G} then it is also a ground term over their intersection, |
|
40406 | 417 |
\isa{F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G}.% |
23848 | 418 |
\end{isamarkuptext}% |
419 |
\isamarkuptrue% |
|
420 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 421 |
\ gterms{\isaliteral{5F}{\isacharunderscore}}IntI{\isaliteral{3A}{\isacharcolon}}\isanewline |
422 |
\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{5C3C696E7465723E}{\isasyminter}}G{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23848 | 423 |
\isadelimproof |
424 |
% |
|
425 |
\endisadelimproof |
|
426 |
% |
|
427 |
\isatagproof |
|
428 |
% |
|
429 |
\endisatagproof |
|
430 |
{\isafoldproof}% |
|
431 |
% |
|
432 |
\isadelimproof |
|
433 |
% |
|
434 |
\endisadelimproof |
|
435 |
% |
|
436 |
\begin{isamarkuptext}% |
|
437 |
Attempting this proof, we get the assumption |
|
40406 | 438 |
\isa{Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G}, which cannot be broken down. |
23848 | 439 |
It looks like a job for rule inversion:\cmmdx{inductive\protect\_cases}% |
440 |
\end{isamarkuptext}% |
|
441 |
\isamarkuptrue% |
|
40406 | 442 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}cases}\isamarkupfalse% |
443 |
\ gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim\ {\isaliteral{5B}{\isacharbrackleft}}elim{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{22}{\isachardoublequoteclose}}% |
|
11187 | 444 |
\begin{isamarkuptext}% |
23848 | 445 |
Here is the result. |
11187 | 446 |
\begin{isabelle}% |
40406 | 447 |
{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
448 |
\isaindent{\ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F{\isaliteral{3B}{\isacharsemicolon}}\ f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
449 |
{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\rulename{gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim}% |
|
10469 | 450 |
\end{isabelle} |
23848 | 451 |
This rule replaces an assumption about \isa{Apply\ f\ args} by |
452 |
assumptions about \isa{f} and~\isa{args}. |
|
453 |
No cases are discarded (there was only one to begin |
|
454 |
with) but the rule applies specifically to the pattern \isa{Apply\ f\ args}. |
|
455 |
It can be applied repeatedly as an elimination rule without looping, so we |
|
40406 | 456 |
have given the \isa{elim{\isaliteral{21}{\isacharbang}}} attribute. |
23848 | 457 |
|
458 |
Now we can prove the other half of that distributive law.% |
|
11187 | 459 |
\end{isamarkuptext}% |
17175 | 460 |
\isamarkuptrue% |
461 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 462 |
\ gterms{\isaliteral{5F}{\isacharunderscore}}IntI\ {\isaliteral{5B}{\isacharbrackleft}}rule{\isaliteral{5F}{\isacharunderscore}}format{\isaliteral{2C}{\isacharcomma}}\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
463 |
\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{5C3C696E7465723E}{\isasyminter}}G{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
17056 | 464 |
% |
465 |
\isadelimproof |
|
466 |
% |
|
467 |
\endisadelimproof |
|
468 |
% |
|
469 |
\isatagproof |
|
17175 | 470 |
\isacommand{apply}\isamarkupfalse% |
40406 | 471 |
\ {\isaliteral{28}{\isacharparenleft}}erule\ gterms{\isaliteral{2E}{\isachardot}}induct{\isaliteral{29}{\isacharparenright}}\isanewline |
17175 | 472 |
\isacommand{apply}\isamarkupfalse% |
473 |
\ blast\isanewline |
|
474 |
\isacommand{done}\isamarkupfalse% |
|
475 |
% |
|
17056 | 476 |
\endisatagproof |
477 |
{\isafoldproof}% |
|
478 |
% |
|
479 |
\isadelimproof |
|
480 |
% |
|
481 |
\endisadelimproof |
|
11866 | 482 |
% |
23848 | 483 |
\isadelimproof |
484 |
% |
|
485 |
\endisadelimproof |
|
486 |
% |
|
487 |
\isatagproof |
|
488 |
% |
|
489 |
\begin{isamarkuptxt}% |
|
490 |
The proof begins with rule induction over the definition of |
|
491 |
\isa{gterms}, which leaves a single subgoal: |
|
11187 | 492 |
\begin{isabelle}% |
40406 | 493 |
\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}args\ f{\isaliteral{2E}{\isachardot}}\isanewline |
494 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t{\isaliteral{5C3C696E3E}{\isasymin}}set\ args{\isaliteral{2E}{\isachardot}}\isanewline |
|
495 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ \ \ }t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ F\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
496 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ \ }f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
497 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\isanewline |
|
498 |
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ }Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}% |
|
11173 | 499 |
\end{isabelle} |
40406 | 500 |
To prove this, we assume \isa{Apply\ f\ args\ {\isaliteral{5C3C696E3E}{\isasymin}}\ gterms\ G}. Rule inversion, |
501 |
in the form of \isa{gterm{\isaliteral{5F}{\isacharunderscore}}Apply{\isaliteral{5F}{\isacharunderscore}}elim}, infers |
|
23848 | 502 |
that every element of \isa{args} belongs to |
503 |
\isa{gterms\ G}; hence (by the induction hypothesis) it belongs |
|
40406 | 504 |
to \isa{gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}}. Rule inversion also yields |
505 |
\isa{f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ G} and hence \isa{f\ {\isaliteral{5C3C696E3E}{\isasymin}}\ F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G}. |
|
23848 | 506 |
All of this reasoning is done by \isa{blast}. |
507 |
||
508 |
\smallskip |
|
509 |
Our distributive law is a trivial consequence of previously-proved results:% |
|
510 |
\end{isamarkuptxt}% |
|
17175 | 511 |
\isamarkuptrue% |
23848 | 512 |
% |
513 |
\endisatagproof |
|
514 |
{\isafoldproof}% |
|
515 |
% |
|
516 |
\isadelimproof |
|
517 |
% |
|
518 |
\endisadelimproof |
|
17175 | 519 |
\isacommand{lemma}\isamarkupfalse% |
40406 | 520 |
\ gterms{\isaliteral{5F}{\isacharunderscore}}Int{\isaliteral{5F}{\isacharunderscore}}eq\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
521 |
\ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}gterms\ {\isaliteral{28}{\isacharparenleft}}F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ G{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ gterms\ F\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ gterms\ G{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
17056 | 522 |
% |
523 |
\isadelimproof |
|
524 |
% |
|
525 |
\endisadelimproof |
|
526 |
% |
|
527 |
\isatagproof |
|
17175 | 528 |
\isacommand{by}\isamarkupfalse% |
40406 | 529 |
\ {\isaliteral{28}{\isacharparenleft}}blast\ intro{\isaliteral{21}{\isacharbang}}{\isaliteral{3A}{\isacharcolon}}\ mono{\isaliteral{5F}{\isacharunderscore}}Int\ monoI\ gterms{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{29}{\isacharparenright}}% |
17056 | 530 |
\endisatagproof |
531 |
{\isafoldproof}% |
|
532 |
% |
|
533 |
\isadelimproof |
|
534 |
% |
|
535 |
\endisadelimproof |
|
12156
d2758965362e
new-style numerals without leading #, along with generic 0 and 1
paulson
parents:
11866
diff
changeset
|
536 |
% |
23848 | 537 |
\index{rule inversion|)}% |
538 |
\index{ground terms example|)} |
|
539 |
||
540 |
||
541 |
\begin{isamarkuptext} |
|
542 |
\begin{exercise} |
|
543 |
A function mapping function symbols to their |
|
544 |
types is called a \textbf{signature}. Given a type |
|
545 |
ranging over type symbols, we can represent a function's type by a |
|
546 |
list of argument types paired with the result type. |
|
547 |
Complete this inductive definition: |
|
548 |
\begin{isabelle} |
|
40406 | 549 |
\isacommand{inductive{\isaliteral{5F}{\isacharunderscore}}set}\isamarkupfalse% |
23733 | 550 |
\isanewline |
40406 | 551 |
\ \ well{\isaliteral{5F}{\isacharunderscore}}typed{\isaliteral{5F}{\isacharunderscore}}gterm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}t\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}f\ gterm\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}t{\isaliteral{29}{\isacharparenright}}set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
552 |
\ \ \isakeyword{for}\ sig\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}f\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}t\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}t{\isaliteral{22}{\isachardoublequoteclose}}% |
|
23848 | 553 |
\end{isabelle} |
554 |
\end{exercise} |
|
555 |
\end{isamarkuptext} |
|
17056 | 556 |
% |
557 |
\isadelimproof |
|
558 |
% |
|
559 |
\endisadelimproof |
|
560 |
% |
|
561 |
\isatagproof |
|
17175 | 562 |
% |
17056 | 563 |
\endisatagproof |
564 |
{\isafoldproof}% |
|
565 |
% |
|
566 |
\isadelimproof |
|
567 |
% |
|
568 |
\endisadelimproof |
|
11866 | 569 |
% |
17056 | 570 |
\isadelimproof |
571 |
% |
|
572 |
\endisadelimproof |
|
573 |
% |
|
574 |
\isatagproof |
|
17175 | 575 |
% |
17056 | 576 |
\endisatagproof |
577 |
{\isafoldproof}% |
|
578 |
% |
|
579 |
\isadelimproof |
|
580 |
% |
|
581 |
\endisadelimproof |
|
582 |
% |
|
583 |
\isadelimtheory |
|
584 |
% |
|
585 |
\endisadelimtheory |
|
586 |
% |
|
587 |
\isatagtheory |
|
17175 | 588 |
% |
17056 | 589 |
\endisatagtheory |
590 |
{\isafoldtheory}% |
|
591 |
% |
|
592 |
\isadelimtheory |
|
593 |
% |
|
594 |
\endisadelimtheory |
|
11187 | 595 |
\end{isabellebody}% |
10365 | 596 |
%%% Local Variables: |
597 |
%%% mode: latex |
|
598 |
%%% TeX-master: "root" |
|
599 |
%%% End: |