src/HOL/Tools/recdef.ML
changeset 35756 cfde251d03a5
parent 35690 863bee3a9153
child 36610 bafd82950e24
     1.1 --- a/src/HOL/Tools/recdef.ML	Thu Mar 11 23:47:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/recdef.ML	Fri Mar 12 12:14:30 2010 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature RECDEF =
     1.5  sig
     1.6    val get_recdef: theory -> string
     1.7 -    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     1.8 +    -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     1.9    val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
    1.10    val simp_add: attribute
    1.11    val simp_del: attribute
    1.12 @@ -17,9 +17,9 @@
    1.13    val wf_del: attribute
    1.14    val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
    1.15      Attrib.src option -> theory -> theory
    1.16 -      * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.17 +      * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.18    val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
    1.19 -    theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.20 +    theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    1.21    val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
    1.22      -> theory -> theory * {induct_rules: thm}
    1.23    val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
    1.24 @@ -84,7 +84,7 @@
    1.25  
    1.26  (* theory data *)
    1.27  
    1.28 -type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    1.29 +type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    1.30  
    1.31  structure GlobalRecdefData = Theory_Data
    1.32  (
    1.33 @@ -198,7 +198,7 @@
    1.34      (*We must remove imp_cong to prevent looping when the induction rule
    1.35        is simplified. Many induction rules have nested implications that would
    1.36        give rise to looping conditional rewriting.*)
    1.37 -    val (thy, {rules = rules_idx, induct, tcs}) =
    1.38 +    val (thy, {lhs, rules = rules_idx, induct, tcs}) =
    1.39          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
    1.40                 congs wfs name R eqs;
    1.41      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
    1.42 @@ -211,8 +211,8 @@
    1.43        |> PureThy.add_thmss
    1.44          (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    1.45        ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
    1.46 -      ||> Spec_Rules.add_global Spec_Rules.Equational (tcs, flat rules);
    1.47 -    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
    1.48 +      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
    1.49 +    val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
    1.50      val thy =
    1.51        thy
    1.52        |> put_recdef name result