1.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Sep 27 12:26:39 2013 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Sep 27 14:43:26 2013 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4      Proof.context -> thm -> thm -> thm
     1.5  
     1.6    val add_lift_def:
     1.7 -    (binding * mixfix) -> typ -> term -> thm -> thm option -> local_theory -> local_theory
     1.8 +    (binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
     1.9  
    1.10    val lift_def_cmd:
    1.11 -    (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
    1.12 +    (binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
    1.13  
    1.14    val can_generate_code_cert: thm -> bool
    1.15  end
    1.16 @@ -135,14 +135,17 @@
    1.17      error error_msg
    1.18    end
    1.19  
    1.20 -fun generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm =
    1.21 +fun map_ter _ x [] = x
    1.22 +    | map_ter f _ xs = map f xs
    1.23 +
    1.24 +fun generate_transfer_rules lthy quot_thm rsp_thm def_thm par_thms =
    1.25    let
    1.26      val transfer_rule =
    1.27        ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
    1.28        |> Lifting_Term.parametrize_transfer_rule lthy
    1.29    in
    1.30 -    (option_fold transfer_rule (generate_parametric_transfer_rule lthy transfer_rule) opt_par_thm
    1.31 -    handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; transfer_rule))
    1.32 +    (map_ter (generate_parametric_transfer_rule lthy transfer_rule) [transfer_rule] par_thms
    1.33 +    handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; [transfer_rule]))
    1.34    end
    1.35  
    1.36  (* Generation of the code certificate from the rsp theorem *)
    1.37 @@ -399,7 +402,7 @@
    1.38      i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
    1.39  *)
    1.40  
    1.41 -fun add_lift_def var qty rhs rsp_thm opt_par_thm lthy =
    1.42 +fun add_lift_def var qty rhs rsp_thm par_thms lthy =
    1.43    let
    1.44      val rty = fastype_of rhs
    1.45      val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
    1.46 @@ -414,7 +417,7 @@
    1.47      val ((_, (_ , def_thm)), lthy') = 
    1.48        Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
    1.49  
    1.50 -    val transfer_rule = generate_transfer_rule lthy' quot_thm rsp_thm def_thm opt_par_thm
    1.51 +    val transfer_rules = generate_transfer_rules lthy' quot_thm rsp_thm def_thm par_thms
    1.52  
    1.53      val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
    1.54      val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
    1.55 @@ -430,7 +433,7 @@
    1.56    in
    1.57      lthy'
    1.58        |> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
    1.59 -      |> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), [transfer_rule])
    1.60 +      |> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), transfer_rules)
    1.61        |> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm])
    1.62        |> (case opt_rep_eq_thm of 
    1.63              SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
    1.64 @@ -495,7 +498,7 @@
    1.65  
    1.66  *)
    1.67  
    1.68 -fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy =
    1.69 +fun lift_def_cmd (raw_var, rhs_raw, par_xthms) lthy =
    1.70    let
    1.71      val ((binding, SOME qty, mx), lthy) = yield_singleton Proof_Context.read_vars raw_var lthy 
    1.72      val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
    1.73 @@ -504,10 +507,10 @@
    1.74      val forced_rhs = force_rty_type lthy rty_forced rhs;
    1.75      val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
    1.76      val opt_proven_rsp_thm = try_prove_reflexivity lthy internal_rsp_tm
    1.77 -    val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
    1.78 +    val par_thms = Attrib.eval_thms lthy par_xthms
    1.79      
    1.80      fun after_qed internal_rsp_thm lthy = 
    1.81 -      add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
    1.82 +      add_lift_def (binding, mx) qty rhs internal_rsp_thm par_thms lthy
    1.83  
    1.84    in
    1.85      case opt_proven_rsp_thm of
    1.86 @@ -567,8 +570,8 @@
    1.87        error error_msg
    1.88      end
    1.89  
    1.90 -fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, opt_par_xthm) lthy =
    1.91 -  (lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy
    1.92 +fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, par_xthms) lthy =
    1.93 +  (lift_def_cmd (raw_var, rhs_raw, par_xthms) lthy
    1.94      handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
    1.95      handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) => 
    1.96        check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw)
    1.97 @@ -576,7 +579,8 @@
    1.98  (* parser and command *)
    1.99  val liftdef_parser =
   1.100    (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
   1.101 -    --| @{keyword "is"} -- Parse.term -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)) >> Parse.triple1
   1.102 +    --| @{keyword "is"} -- Parse.term -- 
   1.103 +      Scan.optional (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthms1) []) >> Parse.triple1
   1.104  val _ =
   1.105    Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
   1.106      "definition for constants over the quotient type"