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 (prem1)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

             @{thm (prem2)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\

             @{thm (prem3)  trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}

            {@{thm (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 %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)

  @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}

ML %grayML{*fun pat_completeness_auto ctxt =

  Pat_Completeness.pat_completeness_tac ctxt 1

    THEN auto_tac ctxt*}

ML {*

  val conf = Function_Common.default_config

*}

datatype foo = Foo nat

local_setup{*Primrec.add_primrec [(@{binding "bar"}, NONE, NoSyn)] 

    [(Attrib.empty_binding, @{term "\<And>x. bar (Foo x) = x"})]

  #> snd *}

local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 

    [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]

      conf pat_completeness_auto #> snd*}

(*<*)end(*>*)