225
|
1 |
theory Ind_Extensions
|
|
2 |
imports "../Base" Simple_Inductive_Package
|
|
3 |
begin
|
|
4 |
|
|
5 |
section {* Extensions of the Package (TBD) *}
|
|
6 |
|
|
7 |
(*
|
|
8 |
text {*
|
|
9 |
In order to add a new inductive predicate to a theory with the help of our
|
|
10 |
package, the user must \emph{invoke} it. For every package, there are
|
|
11 |
essentially two different ways of invoking it, which we will refer to as
|
|
12 |
\emph{external} and \emph{internal}. By external invocation we mean that the
|
|
13 |
package is called from within a theory document. In this case, the
|
|
14 |
specification of the inductive predicate, including type annotations and
|
|
15 |
introduction rules, are given as strings by the user. Before the package can
|
|
16 |
actually make the definition, the type and introduction rules have to be
|
|
17 |
parsed. In contrast, internal invocation means that the package is called by
|
|
18 |
some other package. For example, the function definition package
|
|
19 |
calls the inductive definition package to define the
|
|
20 |
graph of the function. However, it is not a good idea for the function
|
|
21 |
definition package to pass the introduction rules for the function graph to
|
|
22 |
the inductive definition package as strings.
|
|
23 |
|
|
24 |
In this case, it is better to
|
|
25 |
directly pass the rules to the package as a list of terms, which is more
|
|
26 |
robust than handling strings that are lacking the additional structure of
|
|
27 |
terms. These two ways of invoking the package are reflected in its ML
|
|
28 |
programming interface, which consists of two functions:
|
|
29 |
*}
|
|
30 |
*)
|
|
31 |
|
|
32 |
text {*
|
|
33 |
Things to include at the end:
|
|
34 |
|
|
35 |
\begin{itemize}
|
|
36 |
\item include the code for the parameters
|
|
37 |
\item say something about add-inductive to return
|
|
38 |
the rules
|
|
39 |
\item say something about the two interfaces for calling packages
|
|
40 |
\end{itemize}
|
|
41 |
|
|
42 |
*}
|
|
43 |
|
|
44 |
(*
|
|
45 |
simple_inductive
|
|
46 |
Even and Odd
|
|
47 |
where
|
|
48 |
Even0: "Even 0"
|
|
49 |
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
|
|
50 |
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
|
|
51 |
|
|
52 |
thm Even0
|
|
53 |
thm EvenS
|
|
54 |
thm OddS
|
|
55 |
|
|
56 |
thm Even_Odd.intros
|
|
57 |
thm Even.induct
|
|
58 |
thm Odd.induct
|
|
59 |
|
|
60 |
thm Even_def
|
|
61 |
thm Odd_def
|
|
62 |
*)
|
|
63 |
|
|
64 |
(*
|
|
65 |
text {*
|
|
66 |
Second, we want that the user can specify fixed parameters.
|
|
67 |
Remember in the previous section we stated that the user can give the
|
|
68 |
specification for the transitive closure of a relation @{text R} as
|
|
69 |
*}
|
|
70 |
|
|
71 |
simple_inductive
|
|
72 |
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
73 |
where
|
|
74 |
base: "trcl R x x"
|
|
75 |
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
|
|
76 |
*)
|
|
77 |
|
|
78 |
(*
|
|
79 |
text {*
|
|
80 |
Note that there is no locale given in this specification---the parameter
|
|
81 |
@{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but
|
|
82 |
stays fixed throughout the specification. The problem with this way of
|
|
83 |
stating the specification for the transitive closure is that it derives the
|
|
84 |
following induction principle.
|
|
85 |
|
|
86 |
\begin{center}\small
|
|
87 |
\mprset{flushleft}
|
|
88 |
\mbox{\inferrule{
|
|
89 |
@{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
|
|
90 |
@{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\
|
|
91 |
@{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}
|
|
92 |
{@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}}
|
|
93 |
\end{center}
|
|
94 |
|
|
95 |
But this does not correspond to the induction principle we derived by hand, which
|
|
96 |
was
|
|
97 |
|
|
98 |
|
|
99 |
%\begin{center}\small
|
|
100 |
%\mprset{flushleft}
|
|
101 |
%\mbox{\inferrule{
|
|
102 |
% @ { thm_style prem1 trcl_induct[no_vars]}\\\\
|
|
103 |
% @ { thm_style prem2 trcl_induct[no_vars]}\\\\
|
|
104 |
% @ { thm_style prem3 trcl_induct[no_vars]}}
|
|
105 |
% {@ { thm_style concl trcl_induct[no_vars]}}}
|
|
106 |
%\end{center}
|
|
107 |
|
|
108 |
The difference is that in the one derived by hand the relation @{term R} is not
|
|
109 |
a parameter of the proposition @{term P} to be proved and it is also not universally
|
|
110 |
qunatified in the second and third premise. The point is that the parameter @{term R}
|
|
111 |
stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''
|
|
112 |
argument of the transitive closure, but one that can be freely instantiated.
|
|
113 |
In order to recognise such parameters, we have to extend the specification
|
|
114 |
to include a mechanism to state fixed parameters. The user should be able
|
|
115 |
to write
|
|
116 |
|
|
117 |
*}
|
|
118 |
*)
|
|
119 |
(*
|
|
120 |
simple_inductive
|
|
121 |
trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
122 |
where
|
|
123 |
base: "trcl'' R x x"
|
|
124 |
| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"
|
|
125 |
|
|
126 |
simple_inductive
|
|
127 |
accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
128 |
where
|
|
129 |
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"
|
|
130 |
*)
|
|
131 |
|
|
132 |
text {*
|
|
133 |
\begin{exercise}
|
|
134 |
In Section~\ref{sec:nutshell} we required that introduction rules must be of the
|
|
135 |
form
|
|
136 |
|
|
137 |
\begin{isabelle}
|
|
138 |
@{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
|
|
139 |
\end{isabelle}
|
|
140 |
|
|
141 |
where the @{text "As"} and @{text "Bs"} can be any collection of formulae
|
|
142 |
not containing the @{text "preds"}. This requirement is important,
|
|
143 |
because if violated, the theory behind the inductive package does not work
|
|
144 |
and also the proofs break. Write code that tests whether the introduction
|
|
145 |
rules given by the user fit into the scheme described above. Hint: It
|
|
146 |
is not important in which order the premises ar given; the
|
|
147 |
@{text "As"} and @{text "(\<And>ys. Bs \<Longrightarrow> pred ss)"} premises can occur
|
|
148 |
in any order.
|
|
149 |
\end{exercise}
|
|
150 |
*}
|
|
151 |
|
|
152 |
text_raw {*
|
|
153 |
\begin{exercise}
|
|
154 |
If you define @{text even} and @{text odd} with the standard inductive
|
|
155 |
package
|
|
156 |
\begin{isabelle}
|
|
157 |
*}
|
|
158 |
inductive
|
|
159 |
even_2 and odd_2
|
|
160 |
where
|
|
161 |
even0_2: "even_2 0"
|
|
162 |
| evenS_2: "odd_2 m \<Longrightarrow> even_2 (Suc m)"
|
|
163 |
| oddS_2: "even_2 m \<Longrightarrow> odd_2 (Suc m)"
|
|
164 |
|
|
165 |
text_raw{*
|
|
166 |
\end{isabelle}
|
|
167 |
|
|
168 |
you will see that the generated induction principle for @{text "even'"} (namely
|
|
169 |
@{text "even_2_odd_2.inducts"} has the additional assumptions
|
|
170 |
@{prop "odd_2 m"} and @{prop "even_2 m"} in the recursive cases. These additional
|
|
171 |
assumptions can sometimes make ``life easier'' in proofs. Since
|
|
172 |
more assumptions can be made when proving properties, these induction principles
|
|
173 |
are called strong inductions principles. However, it is the case that the
|
|
174 |
``weak'' induction principles imply the ``strong'' ones. Hint: Prove a property
|
|
175 |
taking a pair (or tuple in case of more than one predicate) as argument: the
|
|
176 |
property that you originally want to prove and the predicate(s) over which the
|
|
177 |
induction proceeds.
|
|
178 |
|
|
179 |
Write code that automates the derivation of the strong induction
|
|
180 |
principles from the weak ones.
|
|
181 |
\end{exercise}
|
228
|
182 |
|
|
183 |
\begin{readmore}
|
|
184 |
The standard inductive package is based on least fix-points. It allows more
|
|
185 |
general introduction rules that can include any monotone operators and also
|
|
186 |
provides a richer reasoning infrastructure. The code of this package can be found in
|
|
187 |
@{ML_file "HOL/Tools/inductive_package.ML"}.
|
|
188 |
\end{readmore}
|
225
|
189 |
*}
|
|
190 |
|
|
191 |
|
|
192 |
|
|
193 |
(*<*)end(*>*) |