theory Ind_Extensionsimports Simple_Inductive_Package Ind_Introbeginsection \<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 Oddwhere Even0: "Even 0"| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"| OddS: "Even n \<Longrightarrow> Odd (Suc n)"thm Even0thm EvenSthm OddSthm Even_Odd.introsthm Even.inductthm Odd.inductthm Even_defthm 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_2where 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 natlocal_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(*>*)