134   @{text "arg_tyss"} is the list of argument-type-lists.

   134   @{text "arg_tyss"} is the list of argument-type-lists.

   135 *}

   135 *}

   136 

   136 

   137 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =

   137 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =

   138 let

   138 let

   140   val orules = map (Object_Logic.atomize_term thy) rules

   140   val orules = map (Object_Logic.atomize_term thy) rules

   141   val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 

   141   val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 

   142 in

   142 in

   143   fold_map make_defn (prednames ~~ mxs ~~ defs) lthy

   143   fold_map make_defn (prednames ~~ mxs ~~ defs) lthy

   144 end*}

   144 end*}

   146 text {*

   146 text {*

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

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

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

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

   149   into the object logic (since definitions cannot be stated with

   149   into the object logic (since definitions cannot be stated with

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

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

   152   (Line 3); with this theory we can use the function

   152   (Line 3); with this theory we can use the function

   153   @{ML_ind  atomize_term in Object_Logic} to make the transformation (Line 4). The call

   153   @{ML_ind  atomize_term in Object_Logic} to make the transformation (Line 4). The call

   154   to @{ML defn_aux} in Line 5 produces all right-hand sides of the

   154   to @{ML defn_aux} in Line 5 produces all right-hand sides of the

   155   definitions. The actual definitions are then made in Line 7.  The result of

   155   definitions. The actual definitions are then made in Line 7.  The result of

   156   the function is a list of theorems and a local theory (the theorems are

   156   the function is a list of theorems and a local theory (the theorems are

   339   val goal = Logic.list_implies 

   339   val goal = Logic.list_implies 

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

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

   341 in

   341 in

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

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

   343       (fn {prems, ...} => ind_tac defs prems cnewpreds)

   343       (fn {prems, ...} => ind_tac defs prems cnewpreds)

   345 end *}

   345 end *}

   346 

   346 

   347 text {* 

   347 text {* 

   348   In Line 3 we produce names @{text "zs"} for each type in the 

   348   In Line 3 we produce names @{text "zs"} for each type in the 

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

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

   403 ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =

   403 ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =

   404 let

   404 let

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

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

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

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

   407   

   407   

   409 

   409 

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

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

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

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

   412   val cnewpreds = map (cterm_of thy) newpreds

   412   val cnewpreds = map (cterm_of thy) newpreds

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

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

   414 

   414 

   415 in

   415 in

   416   map (prove_ind lthy' defs srules cnewpreds) 

   416   map (prove_ind lthy' defs srules cnewpreds) 

   417         (preds ~~ newpreds ~~ arg_tyss)

   417         (preds ~~ newpreds ~~ arg_tyss)

   419 end*}

   419 end*}

   420 

   420 

   421 text {*

   421 text {*

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

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

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

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