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}

   182 *}

   183 

   184 

   185 

   186 (*<*)end(*>*)