1 theory Ind_Code

     2 imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims

     3 begin

     4 

     5 section {* Code *}

     6 

     7 text {*

     8   @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}

     9 

    10   @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}

    11 

    12   @{text [display] "def ::= pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}

    13   

    14   @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}

    15 

    16   @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}

    17   

    18   So we have @{text "pred zs"} and @{text "orules[preds::=Ps]"}; have to show

    19   @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.

    20   Instantiating the @{text "preds"} with @{text "Ps"} gives

    21   @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.

    22 

    23   We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};

    24   expanding the defs 

    25   

    26   @{text [display]

    27   "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow>  (\<forall>preds. orules \<longrightarrow> pred ts"}

    28   

    29   so we have @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},

    30   @{text "orules"}; and have to show @{text "pred ts"}

    31 

    32   the @{text "orules"} are of the form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.

    33   

    34   using the @{text "As"} we ????

    35 *}

    36 

    37 

    38 text {*

    39   First we have to produce for each predicate its definitions of the form

    40 

    41   @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}

    42 

    43   In order to make definitions, we use the following wrapper for 

    44   @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax

    45   annotation and a term representing the right-hand side of the definition.

    46 *}

    47 

    48 ML %linenosgray{*fun make_defs ((predname, syn), trm) lthy =

    49 let 

    50   val arg = ((predname, syn), (Attrib.empty_binding, trm))

    51   val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy

    52 in 

    53   (thm, lthy') 

    54 end*}

    55 

    56 text {*

    57   It returns the definition (as a theorem) and the local theory in which this definition has 

    58   been made. In Line 4, @{ML internalK in Thm} is a flag attached to the 

    59   theorem (others possibilities are @{ML definitionK in Thm} and @{ML axiomK in Thm}). 

    60   These flags just classify theorems and have no significant meaning, except 

    61   for tools that, for example, find theorems in the theorem database. We also

    62   use @{ML empty_binding in Attrib} in Line 3, since the definition does 

    63   not need to have any theorem attributes. A testcase for this function is

    64 *}

    65 

    66 local_setup %gray {* fn lthy =>

    67 let

    68   val arg =  ((@{binding "MyTrue"}, NoSyn), @{term True})

    69   val (def, lthy') = make_defs arg lthy 

    70 in

    71   warning (str_of_thm lthy' def); lthy'

    72 end *}

    73 

    74 text {*

    75   which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. 

    76   Since we are testing the function inside \isacommand{local\_setup}, i.e.~make

    77   changes to the ambient theory, we can query the definition using the usual

    78   command \isacommand{thm}:

    79 

    80   \begin{isabelle}

    81   \isacommand{thm}~@{text "MyTrue_def"}\\

    82   @{text "> MyTrue \<equiv> True"}

    83   \end{isabelle}

    84 

    85   The next two functions construct the terms we need for the definitions for

    86   our \isacommand{simple\_inductive} command. These 

    87   terms are of the form 

    88 

    89   @{text [display] "\<lambda>\<^raw:$zs$>. \<forall>preds. orules \<longrightarrow> pred \<^raw:$zs$>"}

    90 

    91   The variables @{text "\<^raw:$zs$>"} need to be chosen so that they do not occur

    92   in the @{text orules} and also be distinct from the @{text "preds"}. 

    93 

    94   The first function constructs the term for one particular predicate, say

    95   @{text "pred"}; the number of arguments of this predicate is

    96   determined by the number of argument types of @{text "arg_tys"}. 

    97   So it takes these two parameters as arguments. The other arguments are

    98   all the @{text "preds"} and the @{text "orules"}.

    99 *}

   100 

   101 ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_tys) =

   102 let 

   103   fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P

   104 

   105   val fresh_args = 

   106         arg_tys 

   107         |> map (pair "z")

   108         |> Variable.variant_frees lthy (preds @ orules) 

   109         |> map Free

   110 in

   111   list_comb (pred, fresh_args)

   112   |> fold_rev (curry HOLogic.mk_imp) orules

   113   |> fold_rev mk_all preds

   114   |> fold_rev lambda fresh_args 

   115 end*}

   116 

   117 text {*

   118   The function in Line 3 is just a helper function for constructing universal

   119   quantifications. The code in Lines 5 to 9 produces the fresh @{text

   120   "\<^raw:$zs$>"}. For this it pairs every argument type with the string

   121   @{text [quotes] "z"} (Line 7); then generates variants for all these strings

   122   so that they are unique w.r.t.~to the @{text "orules"} and the predicates;

   123   in Line 9 it generates the corresponding variable terms for the unique

   124   strings.

   125 

   126   The unique free variables are applied to the predicate (Line 11) using the

   127   function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in

   128   Line 13 we quantify over all predicates; and in line 14 we just abstract

   129   over all the @{text "\<^raw:$zs$>"}, i.e.~the fresh arguments of the

   130   predicate.

   131 

   132   A testcase for this function is

   133 *}

   134 

   135 local_setup %gray{* fn lthy =>

   136 let

   137   val orules = [@{prop "even 0"},

   138                 @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},

   139                 @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] 

   140   val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}, @{term "z::nat"}]

   141   val pred = @{term "even::nat\<Rightarrow>bool"}

   142   val arg_tys = [@{typ "nat"}]

   143   val def = defs_aux lthy orules preds (pred, arg_tys)

   144 in

   145   warning (Syntax.string_of_term lthy def); lthy

   146 end *}

   147 

   148 text {*

   149   It constructs the left-hand side for the definition of @{text "even"}. So we obtain 

   150   as printout the term

   151 

   152   @{text [display] 

   153 "\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 

   154                          \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}

   155 

   156   The main function for the definitions now has to just iterate the function

   157   @{ML defs_aux} over all predicates. The argument @{text "preds"} is again

   158   the the list of predicates as @{ML_type term}s; the argument @{text

   159   "prednames"} is the list of names of the predicates; @{text "arg_tyss"} is

   160   the list of argument-type-lists for each predicate.

   161 *}

   162 

   163 ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =

   164 let

   165   val thy = ProofContext.theory_of lthy

   166   val orules = map (ObjectLogic.atomize_term thy) rules

   167   val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) 

   168 in

   169   fold_map make_defs (prednames ~~ syns ~~ defs) lthy

   170 end*}

   171 

   172 text {*

   173   The user will state the introduction rules using meta-implications and

   174   meta-quanti\-fications. In Line 4, we transform these introduction rules into

   175   the object logic (since definitions cannot be stated with

   176   meta-connectives). To do this transformation we have to obtain the theory

   177   behind the local theory (Line 3); with this theory we can use the function

   178   @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call

   179   to @{ML defs_aux} in Line 5 produces all left-hand sides of the

   180   definitions. The actual definitions are then made in Line 7.  The result

   181   of the function is a list of theorems and a local theory.

   182 

   183 

   184   A testcase for this function is 

   185 *}

   186 

   187 local_setup %gray {* fn lthy =>

   188 let

   189   val rules = [@{prop "even 0"},

   190                @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},

   191                @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 

   192   val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]

   193   val prednames = [@{binding "even"}, @{binding "odd"}] 

   194   val syns = [NoSyn, NoSyn] 

   195   val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]

   196   val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy

   197 in

   198   warning (str_of_thms lthy' defs); lthy'

   199 end *}

   200 

   201 text {*

   202   where we feed into the functions all parameters corresponding to

   203   the @{text even}-@{text odd} example. The definitions we obtain

   204   are:

   205 

   206   \begin{isabelle}

   207   \isacommand{thm}~@{text "even_def odd_def"}\\

   208   @{text [break]

   209 "> even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 

   210 >                                 \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,

   211 > odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) 

   212 >                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}

   213   \end{isabelle}

   214 

   215 

   216   This completes the code for making the definitions. Next we deal with

   217   the induction principles. Recall that the proof of the induction principle 

   218   for @{text "even"} was:

   219 *}

   220 

   221 lemma man_ind_principle: 

   222 assumes prems: "even n"

   223 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   224 apply(atomize (full))

   225 apply(cut_tac prems)

   226 apply(unfold even_def)

   227 apply(drule spec[where x=P])

   228 apply(drule spec[where x=Q])

   229 apply(assumption)

   230 done

   231 

   232 text {* 

   233   The code for such induction principles has to accomplish two tasks: 

   234   constructing the induction principles from the given introduction

   235   rules and then automatically generating a proof of them using a tactic. 

   236   

   237   The tactic will use the following helper function for instantiating universal 

   238   quantifiers. 

   239 *}

   240 

   241 ML{*fun inst_spec ctrm = 

   242  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}

   243 

   244 text {*

   245   This helper function instantiates the @{text "?x"} in the theorem 

   246   @{thm spec} with a given @{ML_type cterm}. Together with the tactic

   247 *}

   248 

   249 ML{*fun inst_spec_tac ctrms = 

   250   EVERY' (map (dtac o inst_spec) ctrms)*}

   251 

   252 text {*

   253   we can use @{ML inst_spec} in the following proof to instantiate the 

   254   three quantifiers in the assumption. 

   255 *}

   256 

   257 lemma 

   258   fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"

   259   shows "\<forall>x y z. P x y z \<Longrightarrow> True"

   260 apply (tactic {* 

   261   inst_spec_tac  [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})

   262 txt {* 

   263   We obtain the goal state

   264 

   265   \begin{minipage}{\textwidth}

   266   @{subgoals} 

   267   \end{minipage}*}

   268 (*<*)oops(*>*)

   269 

   270 text {*

   271   Now the complete tactic for proving the induction principles can 

   272   be implemented as follows:

   273 *}

   274 

   275 ML %linenosgray{*fun induction_tac defs prems insts =

   276   EVERY1 [ObjectLogic.full_atomize_tac,

   277           cut_facts_tac prems,

   278           K (rewrite_goals_tac defs),

   279           inst_spec_tac insts,

   280           assume_tac]*}

   281 

   282 text {*

   283   We only have to give it as arguments the definitions, the premise 

   284   (like @{text "even n"}) 

   285   and the instantiations. Compare this with the manual proof given for the

   286   lemma @{thm [source] man_ind_principle}.  

   287   A testcase for this tactic is the function

   288 *}

   289 

   290 ML{*fun test_tac prems = 

   291 let

   292   val defs = [@{thm even_def}, @{thm odd_def}]

   293   val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]

   294 in 

   295   induction_tac defs prems insts 

   296 end*}

   297 

   298 text {*

   299   which indeed proves the induction principle: 

   300 *}

   301 

   302 lemma 

   303 assumes prems: "even n"

   304 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

   305 apply(tactic {* test_tac @{thms prems} *})

   306 done

   307 

   308 text {*

   309   While the tactic for the induction principle is relatively simple, 

   310   it is a bit harder to construct the goals from the introduction 

   311   rules the user provides. In general we have to construct for each predicate 

   312   @{text "pred"} a goal of the form

   313 

   314   @{text [display] 

   315   "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}

   316 

   317   where the given predicates @{text preds} are replaced in the introduction 

   318   rules by new distinct variables written @{text "\<^raw:$Ps$>"}. 

   319   We also need to generate fresh arguments for the predicate @{text "pred"} in

   320   the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve

   321   that in two steps. 

   322 

   323   The function below expects that the introduction rules are already appropriately

   324   substituted. The argument @{text "srules"} stands for these substituted

   325    rules; @{text cnewpreds} are the certified terms coresponding

   326   to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for

   327   which we prove the introduction principle; @{text "newpred"} is its

   328   replacement and @{text "tys"} are the argument types of this predicate.

   329 *}

   330 

   331 ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys)  =

   332 let

   333   val zs = replicate (length tys) "z"

   334   val (newargnames, lthy') = Variable.variant_fixes zs lthy;

   335   val newargs = map Free (newargnames ~~ tys)

   336   

   337   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))

   338   val goal = Logic.list_implies 

   339          (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))

   340 in

   341   Goal.prove lthy' [] [prem] goal

   342   (fn {prems, ...} => induction_tac defs prems cnewpreds)

   343   |> singleton (ProofContext.export lthy' lthy)

   344 end *}

   345 

   346 text {* 

   347   In Line 3 we produce names @{text "\<^raw:$zs$>"} for each type in the 

   348   argument type list. Line 4 makes these names unique and declares them as 

   349   \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. In 

   350   Line 5 we just construct the terms corresponding to these variables. 

   351   The term variables are applied to the predicate in Line 7 (this corresponds

   352   to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). 

   353   In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} 

   354   and then add the (substituded) introduction rules as premises. In case that

   355   no introduction rules are given, the conclusion of this implication needs

   356   to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal

   357   mechanism will fail. 

   358 

   359   In Line 11 we set up the goal to be proved; in the next line call the tactic

   360   for proving the induction principle. This tactic expects definitions, the

   361   premise and the (certified) predicates with which the introduction rules

   362   have been substituted. This will return a theorem. However, it is a theorem

   363   proved inside the local theory @{text "lthy'"}, where the variables @{text

   364   "\<^raw:$zs$>"} are fixed, but free. By exporting this theorem from @{text

   365   "lthy'"} (which contains the @{text "\<^raw:$zs$>"} as free) to @{text

   366   "lthy"} (which does not), we obtain the desired quantifications @{text

   367   "\<And>\<^raw:$zs$>"}.

   368 

   369   (FIXME testcase)

   370 

   371 

   372   Now it is left to produce the new predicates with which the introduction

   373   rules are substituted. 

   374 *}

   375 

   376 ML %linenosgray{*fun inductions rules defs preds arg_tyss lthy  =

   377 let

   378   val Ps = replicate (length preds) "P"

   379   val (newprednames, lthy') = Variable.variant_fixes Ps lthy

   380   

   381   val thy = ProofContext.theory_of lthy'

   382 

   383   val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss

   384   val newpreds = map Free (newprednames ~~ tyss')

   385   val cnewpreds = map (cterm_of thy) newpreds

   386   val srules = map (subst_free (preds ~~ newpreds)) rules

   387 

   388 in

   389   map (prove_induction lthy' defs srules cnewpreds) 

   390         (preds ~~ newpreds ~~ arg_tyss)

   391           |> ProofContext.export lthy' lthy

   392 end*}

   393 

   394 text {*

   395   In Line 3 we generate a string @{text [quotes] "P"} for each predicate. 

   396   In Line 4, we use the same trick as in the previous function, that is making the 

   397   @{text "\<^raw:$Ps$>"} fresh and declaring them as fixed but free in

   398   the new local theory @{text "lthy'"}. From the local theory we extract

   399   the ambient theory in Line 6. We need this theory in order to certify 

   400   the new predicates. In Line 8 we calculate the types of these new predicates

   401   using the argument types. Next we turn them into terms and subsequently

   402   certify them. We can now produce the substituted introduction rules 

   403   (Line 11). Line 14 and 15 just iterate the proofs for all predicates.

   404   From this we obtain a list of theorems. Finally we need to export the 

   405   fixed variables @{text "\<^raw:$Ps$>"} to obtain the correct quantification 

   406   (Line 16).

   407 

   408   A testcase for this function is

   409 *}

   410 

   411 local_setup %gray {* fn lthy =>

   412 let 

   413   val rules = [@{prop "even (0::nat)"},

   414                @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},

   415                @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 

   416   val defs = [@{thm even_def}, @{thm odd_def}]

   417   val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]

   418   val tyss = [[@{typ "nat"}], [@{typ "nat"}]]

   419   val ind_thms = inductions rules defs preds tyss lthy

   420 in

   421   warning (str_of_thms lthy ind_thms); lthy

   422 end  

   423 *}

   424 

   425 

   426 text {*

   427   which prints out

   428 

   429 @{text [display]

   430 "> even z \<Longrightarrow> 

   431 >  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> P z,

   432 > odd z \<Longrightarrow> 

   433 >  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> Pa z"}

   434 

   435 

   436   This completes the code for the induction principles. Finally we can 

   437   prove the introduction rules. 

   438 

   439 *}

   440 

   441 ML {* ObjectLogic.rulify  *}

   442 

   443 

   444 ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)

   445 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}

   446 

   447 ML{*fun subproof2 prem params2 prems2 =  

   448  SUBPROOF (fn {prems, ...} =>

   449    let

   450      val prem' = prems MRS prem;

   451      val prem'' = 

   452        case prop_of prem' of

   453            _ $ (Const (@{const_name All}, _) $ _) =>

   454              prem' |> all_elims params2 

   455                    |> imp_elims prems2

   456          | _ => prem';

   457    in 

   458      rtac prem'' 1 

   459    end)*}

   460 

   461 ML{*fun subproof1 rules preds i = 

   462  SUBPROOF (fn {params, prems, context = ctxt', ...} =>

   463    let

   464      val (prems1, prems2) = chop (length prems - length rules) prems;

   465      val (params1, params2) = chop (length params - length preds) params;

   466    in

   467      rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 

   468      THEN

   469      EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)

   470    end)*}

   471 

   472 ML{*

   473 fun introductions_tac defs rules preds i ctxt =

   474   EVERY1 [ObjectLogic.rulify_tac,

   475           K (rewrite_goals_tac defs),

   476           REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),

   477           subproof1 rules preds i ctxt]*}

   478 

   479 lemma evenS: 

   480   shows "odd m \<Longrightarrow> even (Suc m)"

   481 apply(tactic {* 

   482 let

   483   val rules = [@{prop "even (0::nat)"},

   484                  @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},

   485                  @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 

   486   val defs = [@{thm even_def}, @{thm odd_def}]

   487   val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]

   488 in

   489   introductions_tac defs rules preds 1 @{context}

   490 end *})

   491 done

   492 

   493 ML{*fun introductions rules preds defs lthy = 

   494 let

   495   fun prove_intro (i, goal) =

   496     Goal.prove lthy [] [] goal

   497       (fn {context, ...} => introductions_tac defs rules preds i context)

   498 in

   499   map_index prove_intro rules

   500 end*}

   501 

   502 text {* main internal function *}

   503 

   504 ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =

   505 let

   506   val syns = map snd pred_specs

   507   val pred_specs' = map fst pred_specs

   508   val prednames = map fst pred_specs'

   509   val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'

   510 

   511   val tyss = map (binder_types o fastype_of) preds   

   512   val (attrs, rules) = split_list rule_specs    

   513 

   514   val (defs, lthy') = definitions rules preds prednames syns tyss lthy      

   515   val ind_rules = inductions rules defs preds tyss lthy' 	

   516   val intro_rules = introductions rules preds defs lthy'

   517 

   518   val mut_name = space_implode "_" (map Binding.name_of prednames)

   519   val case_names = map (Binding.name_of o fst) attrs

   520 in

   521     lthy' 

   522     |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>

   523         ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) 

   524     |-> (fn intross => LocalTheory.note Thm.theoremK

   525          ((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross)) 

   526     |>> snd 

   527     ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>

   528          ((Binding.qualify false (Binding.name_of R) (@{binding "induct"}),

   529           [Attrib.internal (K (RuleCases.case_names case_names)),

   530            Attrib.internal (K (RuleCases.consumes 1)),

   531            Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))

   532           (pred_specs ~~ ind_rules)) #>> maps snd) 

   533     |> snd

   534 end*}

   535 

   536 ML{*fun add_inductive_cmd pred_specs rule_specs lthy =

   537 let

   538   val ((pred_specs', rule_specs'), _) = 

   539          Specification.read_spec pred_specs rule_specs lthy

   540 in

   541   add_inductive pred_specs' rule_specs' lthy

   542 end*} 

   543 

   544 ML{*val spec_parser = 

   545    OuterParse.fixes -- 

   546    Scan.optional 

   547      (OuterParse.$$$ "where" |--

   548         OuterParse.!!! 

   549           (OuterParse.enum1 "|" 

   550              (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}

   551 

   552 ML{*val specification =

   553   spec_parser >>

   554     (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}

   555 

   556 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 

   557               "define inductive predicates"

   558                  OuterKeyword.thy_decl specification*}

   559 

   560 text {*

   561   Things to include at the end:

   562 

   563   \begin{itemize}

   564   \item say something about add-inductive-i to return

   565   the rules

   566   \item say that the induction principle is weaker (weaker than

   567   what the standard inductive package generates)

   568   \end{itemize}

   569   

   570 *}

   571 

   572 simple_inductive

   573   Even and Odd

   574 where

   575   Even0: "Even 0"

   576 | EvenS: "Odd n \<Longrightarrow> Even (Suc n)"

   577 | OddS: "Even n \<Longrightarrow> Odd (Suc n)"

   578 

   579 end