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   \underline{Induction proof}

    19   

    20   After ``objectivication'' we have 

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

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

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

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

    25 

    26   \underline{Intro proof}

    27 

    28   Assume we want to prove the $i$th intro rule. 

    29 

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

    31   expanding the defs, gives 

    32   

    33   @{text [display]

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

    35   

    36   applying as many allI and impI as possible

    37   

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

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

    40 

    41   the $i$th @{text "orule"} is of the 

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

    43   

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

    45 *}

    46 

    47 

    48 text {*

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

    50 

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

    52 

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

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

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

    56 *}

    57 

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

    59 let 

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

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

    62 in 

    63   (thm, lthy') 

    64 end*}

    65 

    66 text {*

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

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

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

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

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

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

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

    74 *}

    75 

    76 local_setup %gray {* fn lthy =>

    77 let

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

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

    80 in

    81   warning (str_of_thm lthy' def); lthy'

    82 end *}

    83 

    84 text {*

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

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

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

    88   command \isacommand{thm}:

    89 

    90   \begin{isabelle}

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

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

    93   \end{isabelle}

    94 

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

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

    97   terms are of the form 

    98 

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

   100 

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

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

   103 

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

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

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

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

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

   109 *}

   110 

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

   112 let 

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

   114 

   115   val fresh_args = 

   116         arg_tys 

   117         |> map (pair "z")

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

   119         |> map Free

   120 in

   121   list_comb (pred, fresh_args)

   122   |> fold_rev (curry HOLogic.mk_imp) orules

   123   |> fold_rev mk_all preds

   124   |> fold_rev lambda fresh_args 

   125 end*}

   126 

   127 text {*

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

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

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

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

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

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

   134   strings.

   135 

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

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

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

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

   140   predicate.

   141 

   142   A testcase for this function is

   143 *}

   144 

   145 local_setup %gray{* fn lthy =>

   146 let

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

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

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

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

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

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

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

   154 in

   155   warning (Syntax.string_of_term lthy def); lthy

   156 end *}

   157 

   158 text {*

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

   160   as printout the term

   161 

   162   @{text [display] 

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

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

   165 

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

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

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

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

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

   171 *}

   172 

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

   174 let

   175   val thy = ProofContext.theory_of lthy

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

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

   178 in

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

   180 end*}

   181 

   182 text {*

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

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

   185   the object logic (since definitions cannot be stated with

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

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

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

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

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

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

   192 

   193 

   194   A testcase for this function is 

   195 *}

   196 

   197 local_setup %gray {* fn lthy =>

   198 let

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

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

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

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

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

   204   val syns = [NoSyn, NoSyn] 

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

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

   207 in

   208   warning (str_of_thms lthy' defs); lthy'

   209 end *}

   210 

   211 text {*

   212   where we feed into the functions all parameters corresponding to

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

   214   are:

   215 

   216   \begin{isabelle}

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

   218   @{text [break]

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

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

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

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

   223   \end{isabelle}

   224 

   225 

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

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

   228   for @{text "even"} was:

   229 *}

   230 

   231 lemma man_ind_principle: 

   232 assumes prems: "even n"

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

   234 apply(atomize (full))

   235 apply(cut_tac prems)

   236 apply(unfold even_def)

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

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

   239 apply(assumption)

   240 done

   241 

   242 text {* 

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

   244   constructing the induction principles from the given introduction

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

   246   

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

   248   quantifiers. 

   249 *}

   250 

   251 ML{*fun inst_spec ctrm = 

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

   253 

   254 text {*

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

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

   257 *}

   258 

   259 ML{*fun inst_spec_tac ctrms = 

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

   261 

   262 text {*

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

   264   three quantifiers in the assumption. 

   265 *}

   266 

   267 lemma 

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

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

   270 apply (tactic {* 

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

   272 txt {* 

   273   We obtain the goal state

   274 

   275   \begin{minipage}{\textwidth}

   276   @{subgoals} 

   277   \end{minipage}*}

   278 (*<*)oops(*>*)

   279 

   280 text {*

   281   Now the complete tactic for proving the induction principles can 

   282   be implemented as follows:

   283 *}

   284 

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

   286   EVERY1 [ObjectLogic.full_atomize_tac,

   287           cut_facts_tac prems,

   288           K (rewrite_goals_tac defs),

   289           inst_spec_tac insts,

   290           assume_tac]*}

   291 

   292 text {*

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

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

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

   296   lemma @{thm [source] man_ind_principle}.  

   297   A testcase for this tactic is the function

   298 *}

   299 

   300 ML{*fun test_tac prems = 

   301 let

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

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

   304 in 

   305   induction_tac defs prems insts 

   306 end*}

   307 

   308 text {*

   309   which indeed proves the induction principle: 

   310 *}

   311 

   312 lemma 

   313 assumes prems: "even n"

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

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

   316 done

   317 

   318 text {*

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

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

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

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

   323 

   324   @{text [display] 

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

   326 

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

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

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

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

   331   that in two steps. 

   332 

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

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

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

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

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

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

   339 *}

   340 

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

   342 let

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

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

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

   346   

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

   348   val goal = Logic.list_implies 

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

   350 in

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

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

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

   354 end *}

   355 

   356 text {* 

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

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

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

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

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

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

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

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

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

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

   367   mechanism will fail. 

   368 

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

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

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

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

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

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

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

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

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

   378 

   379   (FIXME testcase)

   380 

   381 

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

   383   rules are substituted. 

   384 *}

   385 

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

   387 let

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

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

   390   

   391   val thy = ProofContext.theory_of lthy'

   392 

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

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

   395   val cnewpreds = map (cterm_of thy) newpreds

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

   397 

   398 in

   399   map (prove_induction lthy' defs srules cnewpreds) 

   400         (preds ~~ newpreds ~~ arg_tyss)

   401           |> ProofContext.export lthy' lthy

   402 end*}

   403 

   404 text {*

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

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

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

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

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

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

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

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

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

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

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

   416   (Line 16).

   417 

   418   A testcase for this function is

   419 *}

   420 

   421 local_setup %gray {* fn lthy =>

   422 let 

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

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

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

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

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

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

   429   val ind_thms = inductions rules defs preds tyss lthy

   430 in

   431   warning (str_of_thms lthy ind_thms); lthy

   432 end  

   433 *}

   434 

   435 

   436 text {*

   437   which prints out

   438 

   439 @{text [display]

   440 "> even z \<Longrightarrow> 

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

   442 > odd z \<Longrightarrow> 

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

   444 

   445 

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

   447   prove the introduction rules. 

   448 

   449 *}

   450 

   451 ML {* ObjectLogic.rulify  *}

   452 

   453 

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

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

   456 

   457 ML{*fun subproof2 prem params2 prems2 =  

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

   459    let

   460      val prem' = prems MRS prem;

   461      val prem'' = 

   462        case prop_of prem' of

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

   464              prem' |> all_elims params2 

   465                    |> imp_elims prems2

   466          | _ => prem';

   467    in 

   468      rtac prem'' 1 

   469    end)*}

   470 

   471 ML{*fun subproof1 rules preds i = 

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

   473    let

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

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

   476    in

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

   478      THEN

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

   480    end)*}

   481 

   482 ML{*

   483 fun introductions_tac defs rules preds i ctxt =

   484   EVERY1 [ObjectLogic.rulify_tac,

   485           K (rewrite_goals_tac defs),

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

   487           subproof1 rules preds i ctxt]*}

   488 

   489 lemma evenS: 

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

   491 apply(tactic {* 

   492 let

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

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

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

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

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

   498 in

   499   introductions_tac defs rules preds 1 @{context}

   500 end *})

   501 done

   502 

   503 ML{*fun introductions rules preds defs lthy = 

   504 let

   505   fun prove_intro (i, goal) =

   506     Goal.prove lthy [] [] goal

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

   508 in

   509   map_index prove_intro rules

   510 end*}

   511 

   512 text {* main internal function *}

   513 

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

   515 let

   516   val syns = map snd pred_specs

   517   val pred_specs' = map fst pred_specs

   518   val prednames = map fst pred_specs'

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

   520 

   521   val tyss = map (binder_types o fastype_of) preds   

   522   val (attrs, rules) = split_list rule_specs    

   523 

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

   525   val ind_rules = inductions rules defs preds tyss lthy' 	

   526   val intro_rules = introductions rules preds defs lthy'

   527 

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

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

   530 in

   531     lthy' 

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

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

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

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

   536     |>> snd 

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

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

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

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

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

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

   543     |> snd

   544 end*}

   545 

   546 ML{*fun add_inductive_cmd pred_specs rule_specs lthy =

   547 let

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

   549          Specification.read_spec pred_specs rule_specs lthy

   550 in

   551   add_inductive pred_specs' rule_specs' lthy

   552 end*} 

   553 

   554 ML{*val spec_parser = 

   555    OuterParse.fixes -- 

   556    Scan.optional 

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

   558         OuterParse.!!! 

   559           (OuterParse.enum1 "|" 

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

   561 

   562 ML{*val specification =

   563   spec_parser >>

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

   565 

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

   567               "define inductive predicates"

   568                  OuterKeyword.thy_decl specification*}

   569 

   570 text {*

   571   Things to include at the end:

   572 

   573   \begin{itemize}

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

   575   the rules

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

   577   what the standard inductive package generates)

   578   \end{itemize}

   579   

   580 *}

   581 

   582 simple_inductive

   583   Even and Odd

   584 where

   585   Even0: "Even 0"

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

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

   588 

   589 end