theory Ind_Extensions+ −
imports Simple_Inductive_Package Ind_Intro+ −
begin+ −
+ −
section {* Extensions of the Package (TBD) *}+ −
+ −
(*+ −
text {*+ −
In order to add a new inductive predicate to a theory with the help of our+ −
package, the user must \emph{invoke} it. For every package, there are+ −
essentially two different ways of invoking it, which we will refer to as+ −
\emph{external} and \emph{internal}. By external invocation we mean that the+ −
package is called from within a theory document. In this case, the+ −
specification of the inductive predicate, including type annotations and+ −
introduction rules, are given as strings by the user. Before the package can+ −
actually make the definition, the type and introduction rules have to be+ −
parsed. In contrast, internal invocation means that the package is called by+ −
some other package. For example, the function definition package+ −
calls the inductive definition package to define the+ −
graph of the function. However, it is not a good idea for the function+ −
definition package to pass the introduction rules for the function graph to+ −
the inductive definition package as strings. + −
+ −
In this case, it is better to+ −
directly pass the rules to the package as a list of terms, which is more+ −
robust than handling strings that are lacking the additional structure of+ −
terms. These two ways of invoking the package are reflected in its ML+ −
programming interface, which consists of two functions:+ −
*}+ −
*)+ −
+ −
text {*+ −
Things to include at the end:+ −
+ −
\begin{itemize}+ −
\item include the code for the parameters+ −
\item say something about add-inductive to return+ −
the rules+ −
\item say something about the two interfaces for calling packages+ −
\end{itemize}+ −
+ −
*}+ −
+ −
(*+ −
simple_inductive+ −
Even and Odd+ −
where+ −
Even0: "Even 0"+ −
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"+ −
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"+ −
+ −
thm Even0+ −
thm EvenS+ −
thm OddS+ −
+ −
thm Even_Odd.intros+ −
thm Even.induct+ −
thm Odd.induct+ −
+ −
thm Even_def+ −
thm Odd_def+ −
*)+ −
+ −
(*+ −
text {* + −
Second, we want that the user can specify fixed parameters.+ −
Remember in the previous section we stated that the user can give the + −
specification for the transitive closure of a relation @{text R} as + −
*}+ −
+ −
simple_inductive+ −
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
base: "trcl R x x"+ −
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"+ −
*)+ −
+ −
(*+ −
text {*+ −
Note that there is no locale given in this specification---the parameter+ −
@{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but+ −
stays fixed throughout the specification. The problem with this way of+ −
stating the specification for the transitive closure is that it derives the+ −
following induction principle.+ −
+ −
\begin{center}\small+ −
\mprset{flushleft}+ −
\mbox{\inferrule{+ −
@{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\+ −
@{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\+ −
@{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}+ −
{@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}} + −
\end{center}+ −
+ −
But this does not correspond to the induction principle we derived by hand, which+ −
was+ −
+ −
+ −
%\begin{center}\small+ −
%\mprset{flushleft}+ −
%\mbox{\inferrule{+ −
% @ { thm_style prem1 trcl_induct[no_vars]}\\\\+ −
% @ { thm_style prem2 trcl_induct[no_vars]}\\\\+ −
% @ { thm_style prem3 trcl_induct[no_vars]}}+ −
% {@ { thm_style concl trcl_induct[no_vars]}}} + −
%\end{center}+ −
+ −
The difference is that in the one derived by hand the relation @{term R} is not+ −
a parameter of the proposition @{term P} to be proved and it is also not universally+ −
qunatified in the second and third premise. The point is that the parameter @{term R}+ −
stays fixed thoughout the definition and we do not want to regard it as an ``ordinary''+ −
argument of the transitive closure, but one that can be freely instantiated. + −
In order to recognise such parameters, we have to extend the specification+ −
to include a mechanism to state fixed parameters. The user should be able+ −
to write + −
+ −
*}+ −
*)+ −
(*+ −
simple_inductive+ −
trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
base: "trcl'' R x x"+ −
| step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z"+ −
+ −
simple_inductive+ −
accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"+ −
where+ −
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x"+ −
*)+ −
+ −
text {*+ −
\begin{exercise}+ −
In Section~\ref{sec:nutshell} we required that introduction rules must be of the+ −
form+ −
+ −
\begin{isabelle}+ −
@{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}+ −
\end{isabelle}+ −
+ −
where the @{text "As"} and @{text "Bs"} can be any collection of formulae+ −
not containing the @{text "preds"}. This requirement is important,+ −
because if violated, the theory behind the inductive package does not work+ −
and also the proofs break. Write code that tests whether the introduction+ −
rules given by the user fit into the scheme described above. Hint: It + −
is not important in which order the premises ar given; the+ −
@{text "As"} and @{text "(\<And>ys. Bs \<Longrightarrow> pred ss)"} premises can occur+ −
in any order.+ −
\end{exercise}+ −
*} + −
+ −
text_raw {*+ −
\begin{exercise}+ −
If you define @{text even} and @{text odd} with the standard inductive+ −
package+ −
\begin{isabelle}+ −
*}+ −
inductive + −
even_2 and odd_2+ −
where+ −
even0_2: "even_2 0"+ −
| evenS_2: "odd_2 m \<Longrightarrow> even_2 (Suc m)"+ −
| oddS_2: "even_2 m \<Longrightarrow> odd_2 (Suc m)"+ −
+ −
text_raw{*+ −
\end{isabelle}+ −
+ −
you will see that the generated induction principle for @{text "even'"} (namely+ −
@{text "even_2_odd_2.inducts"} has the additional assumptions + −
@{prop "odd_2 m"} and @{prop "even_2 m"} in the recursive cases. These additional + −
assumptions can sometimes make ``life easier'' in proofs. Since + −
more assumptions can be made when proving properties, these induction principles + −
are called strong inductions principles. However, it is the case that the + −
``weak'' induction principles imply the ``strong'' ones. Hint: Prove a property + −
taking a pair (or tuple in case of more than one predicate) as argument: the + −
property that you originally want to prove and the predicate(s) over which the + −
induction proceeds.+ −
+ −
Write code that automates the derivation of the strong induction + −
principles from the weak ones.+ −
\end{exercise}+ −
+ −
\begin{readmore}+ −
The standard inductive package is based on least fix-points. It allows more + −
general introduction rules that can include any monotone operators and also+ −
provides a richer reasoning infrastructure. The code of this package can be found in + −
@{ML_file "HOL/Tools/inductive.ML"}.+ −
\end{readmore}+ −
*}+ −
+ −
section {* Definitional Packages *}+ −
+ −
text {* Type declarations *}+ −
+ −
ML{*Typedef.add_typedef false NONE (@{binding test},[],NoSyn)+ −
@{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}+ −
+ −
+ −
(*<*)end(*>*)+ −