--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Package/Ind_Extensions.thy Thu Apr 02 11:48:35 2009 +0100
@@ -0,0 +1,186 @@
+theory Ind_Extensions
+imports "../Base" Simple_Inductive_Package
+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}
+*}
+
+
+
+(*<*)end(*>*)
\ No newline at end of file