diff -r 647cab4a72c2 -r 7859fc59249a ProgTutorial/Package/Ind_Extensions.thy
--- /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