src/HOL/Tools/recdef_package.ML
changeset 8625 93a11ebacf32
parent 8481 89d498a8d3f6
child 8657 b9475dad85ed
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Thu Mar 30 19:45:51 2000 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Mar 30 19:47:17 2000 +0200
     1.3 @@ -9,13 +9,13 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val print_recdefs: theory -> unit
     1.7 -  val get_recdef: theory -> string -> {rules: thm list, induct: thm, tcs: term list} option
     1.8 +  val get_recdef: theory -> string -> {simps: thm list, induct: thm, tcs: term list} option
     1.9    val add_recdef: xstring -> string -> string list -> simpset option
    1.10      -> (xstring * Args.src list) list -> theory
    1.11 -    -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.12 +    -> theory * {simps: thm list, induct: thm, tcs: term list}
    1.13    val add_recdef_i: xstring -> term -> term list -> simpset option
    1.14      -> (thm * theory attribute list) list
    1.15 -    -> theory -> theory * {rules: thm list, induct: thm, tcs: term list}
    1.16 +    -> theory -> theory * {simps: thm list, induct: thm, tcs: term list}
    1.17    val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
    1.18      -> theory -> theory * {induct_rules: thm}
    1.19    val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
    1.20 @@ -35,7 +35,7 @@
    1.21  
    1.22  (* data kind 'HOL/recdef' *)
    1.23  
    1.24 -type recdef_info = {rules: thm list, induct: thm, tcs: term list};
    1.25 +type recdef_info = {simps: thm list, induct: thm, tcs: term list};
    1.26  
    1.27  structure RecdefArgs =
    1.28  struct
    1.29 @@ -72,6 +72,13 @@
    1.30  
    1.31  fun requires_recdef thy = Theory.requires thy "Recdef" "recursive functions";
    1.32  
    1.33 +
    1.34 +fun prepare_simps no_tcs ixsimps =
    1.35 +  let val partnd = partition_eq (fn ((_,i),(_,j)) => i=j) ixsimps;
    1.36 +      val attr = if no_tcs then [Simplifier.simp_add_global] else []
    1.37 +  in map (fn (rl,i)::rls => ((string_of_int i, rl::map fst rls), attr)) partnd
    1.38 +  end;
    1.39 +
    1.40  fun gen_add_recdef tfl_fn prep_ss app_thms raw_name R eqs raw_ss raw_congs thy =
    1.41    let
    1.42      val name = Sign.intern_const (Theory.sign_of thy) raw_name;
    1.43 @@ -83,13 +90,14 @@
    1.44      val ss = (case raw_ss of None => Simplifier.simpset_of thy | Some x => prep_ss x);
    1.45      val (thy, congs) = thy |> app_thms raw_congs;
    1.46      val (thy, {rules, induct, tcs}) = tfl_fn thy name R (ss, congs) eqs;
    1.47 +    val named_simps = prepare_simps (null tcs) rules
    1.48      val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
    1.49 -    val (thy, ([rules], [induct])) =
    1.50 +    val (thy, (simpss, [induct])) =
    1.51        thy
    1.52        |> Theory.add_path bname
    1.53 -      |> PureThy.add_thmss [(("rules", rules), [])]
    1.54 +      |> PureThy.add_thmss named_simps
    1.55        |>>> PureThy.add_thms [(("induct", induct), [RuleCases.case_names case_numbers])];
    1.56 -    val result = {rules = rules, induct = induct, tcs = tcs};
    1.57 +    val result = {simps = flat simpss, induct = induct, tcs = tcs};
    1.58      val thy =
    1.59        thy
    1.60        |> put_recdef name result