theory Ind_Extensions
imports Simple_Inductive_Package Ind_Intro
begin

section \<open>Extensions of the Package (TBD)\<close>

(*
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 \<open>
  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}
  
\<close>

(*
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 \<open>
  \begin{exercise}
  In Section~\ref{sec:nutshell} we required that introduction rules must be of the
  form

  \begin{isabelle}
  \<open>rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts\<close>
  \end{isabelle}

  where the \<open>As\<close> and \<open>Bs\<close> can be any collection of formulae
  not containing the \<open>preds\<close>. 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
  \<open>As\<close> and \<open>(\<And>ys. Bs \<Longrightarrow> pred ss)\<close> premises can occur
  in any order.
  \end{exercise}
\<close>  

text_raw \<open>
  \begin{exercise}
  If you define \<open>even\<close> and \<open>odd\<close> with the standard inductive
  package
  \begin{isabelle}
\<close>
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\<open>
  \end{isabelle}

  you will see that the generated induction principle for \<open>even'\<close> (namely
  \<open>even_2_odd_2.inducts\<close> 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}
\<close>

section \<open>Definitional Packages\<close>

text \<open>Type declarations\<close>

(*
ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
  @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}
*)

ML %grayML\<open>fun pat_completeness_auto ctxt =
  Pat_Completeness.pat_completeness_tac ctxt 1
    THEN auto_tac ctxt\<close>

ML \<open>
  val conf = Function_Common.default_config
\<close>

datatype foo = Foo nat

local_setup\<open>Function.add_function [(@{binding "baz"}, NONE, NoSyn)] 
    [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])]
      conf pat_completeness_auto #> snd\<close>

(*<*)end(*>*)