refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
authorbulwahn
Fri Mar 12 12:14:30 2010 +0100 (2010-03-12)
changeset 35756cfde251d03a5
parent 35737 19eefc0655b6
child 35757 c2884bec5463
refining and adding Spec_Rules to definitional packages old_primrec, primrec, recdef, size and function
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/recdef.ML
     1.1 --- a/src/HOL/Tools/Function/function.ML	Thu Mar 11 23:47:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Mar 12 12:14:30 2010 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4  
     1.5      fun afterqed [[proof]] lthy =
     1.6        let
     1.7 -        val FunctionResult {fs, R, psimps, trsimps,  simple_pinducts,
     1.8 +        val FunctionResult {fs, R, psimps, trsimps, simple_pinducts,
     1.9            termination, domintros, cases, ...} =
    1.10            cont (Thm.close_derivation proof)
    1.11  
    1.12 @@ -97,7 +97,7 @@
    1.13            |> addsmps (conceal_partial o Binding.qualify false "partial")
    1.14                 "psimps" conceal_partial psimp_attribs psimps
    1.15            ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
    1.16 -          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o (pair fs)) trsimps
    1.17 +          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps
    1.18            ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
    1.19                   [Attrib.internal (K (Rule_Cases.case_names cnames)),
    1.20                    Attrib.internal (K (Rule_Cases.consumes 1)),
    1.21 @@ -165,7 +165,7 @@
    1.22                simps=SOME simps, inducts=SOME inducts, termination=termination }
    1.23              in
    1.24                Local_Theory.declaration false (add_function_data o morph_function_data info')
    1.25 -              #> Spec_Rules.add Spec_Rules.Equational (fs, simps)
    1.26 +              #> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)
    1.27              end)
    1.28          end
    1.29    in
     2.1 --- a/src/HOL/Tools/Function/size.ML	Thu Mar 11 23:47:16 2010 +0100
     2.2 +++ b/src/HOL/Tools/Function/size.ML	Fri Mar 12 12:14:30 2010 +0100
     2.3 @@ -130,8 +130,9 @@
     2.4      fun define_overloaded (def_name, eq) lthy =
     2.5        let
     2.6          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
     2.7 -        val ((_, (_, thm)), lthy') = lthy
     2.8 -          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
     2.9 +        val (thm, lthy') = lthy
    2.10 +          |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
    2.11 +          |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
    2.12          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
    2.13          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
    2.14        in (thm', lthy') end;
     3.1 --- a/src/HOL/Tools/TFL/post.ML	Thu Mar 11 23:47:16 2010 +0100
     3.2 +++ b/src/HOL/Tools/TFL/post.ML	Fri Mar 12 12:14:30 2010 +0100
     3.3 @@ -8,9 +8,9 @@
     3.4  signature TFL =
     3.5  sig
     3.6    val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
     3.7 -    term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
     3.8 +    term -> term list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list}
     3.9    val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
    3.10 -    string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
    3.11 +    string -> string list -> theory * {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list}
    3.12    val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
    3.13    val defer: theory -> thm list -> xstring -> string list -> theory * thm
    3.14  end;
    3.15 @@ -204,12 +204,13 @@
    3.16  fun define_i strict thy cs ss congs wfs fid R eqs =
    3.17    let val {functional,pats} = Prim.mk_functional thy eqs
    3.18        val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
    3.19 +      val (lhs, _) = Logic.dest_equals (prop_of def)
    3.20        val {induct, rules, tcs} = 
    3.21            simplify_defn strict thy cs ss congs wfs fid pats def
    3.22        val rules' = 
    3.23            if strict then derive_init_eqs thy rules eqs
    3.24            else rules
    3.25 -  in (thy, {rules = rules', induct = induct, tcs = tcs}) end;
    3.26 +  in (thy, {lhs = lhs, rules = rules', induct = induct, tcs = tcs}) end;
    3.27  
    3.28  fun define strict thy cs ss congs wfs fid R seqs =
    3.29    define_i strict thy cs ss congs wfs fid
     4.1 --- a/src/HOL/Tools/old_primrec.ML	Thu Mar 11 23:47:16 2010 +0100
     4.2 +++ b/src/HOL/Tools/old_primrec.ML	Fri Mar 12 12:14:30 2010 +0100
     4.3 @@ -281,14 +281,13 @@
     4.4        thy'
     4.5        |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     4.6      val simps'' = maps snd simps';
     4.7 -    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
     4.8 -    val specs = (distinct (op =) (map dest_eqn simps''), simps'')
     4.9 +    val lhss = map (Logic.varify o fst o Logic.dest_equals o snd) defs';
    4.10    in
    4.11      thy''
    4.12      |> note (("simps",
    4.13          [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
    4.14      |> snd
    4.15 -    |> Spec_Rules.add_global Spec_Rules.Equational specs
    4.16 +    |> Spec_Rules.add_global Spec_Rules.Equational (lhss, simps)
    4.17      |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
    4.18      |> snd
    4.19      |> Sign.parent_path
     5.1 --- a/src/HOL/Tools/primrec.ML	Thu Mar 11 23:47:16 2010 +0100
     5.2 +++ b/src/HOL/Tools/primrec.ML	Fri Mar 12 12:14:30 2010 +0100
     5.3 @@ -265,15 +265,6 @@
     5.4  
     5.5  local
     5.6  
     5.7 -fun specs_of simps =
     5.8 -  let
     5.9 -    val eqns = maps snd simps
    5.10 -    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
    5.11 -    val t = distinct (op =) (map dest_eqn eqns)
    5.12 -  in
    5.13 -    (t, eqns)
    5.14 -  end
    5.15 -
    5.16  fun gen_primrec prep_spec raw_fixes raw_spec lthy =
    5.17    let
    5.18      val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
    5.19 @@ -285,10 +276,11 @@
    5.20    in
    5.21      lthy
    5.22      |> add_primrec_simple fixes (map snd spec)
    5.23 -    |-> (fn (prefix, (ts, simps)) => fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
    5.24 +    |-> (fn (prefix, (ts, simps)) =>
    5.25 +      Spec_Rules.add Spec_Rules.Equational (ts, simps)
    5.26 +      #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
    5.27        #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
    5.28 -      #>> (fn (_, simps'') => (ts, simps''))
    5.29 -      ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps'))))
    5.30 +      #>> (fn (_, simps'') => (ts, simps''))))
    5.31    end;
    5.32  
    5.33  in
     6.1 --- a/src/HOL/Tools/recdef.ML	Thu Mar 11 23:47:16 2010 +0100
     6.2 +++ b/src/HOL/Tools/recdef.ML	Fri Mar 12 12:14:30 2010 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  signature RECDEF =
     6.5  sig
     6.6    val get_recdef: theory -> string
     6.7 -    -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     6.8 +    -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
     6.9    val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
    6.10    val simp_add: attribute
    6.11    val simp_del: attribute
    6.12 @@ -17,9 +17,9 @@
    6.13    val wf_del: attribute
    6.14    val add_recdef: bool -> xstring -> string -> ((binding * string) * Attrib.src list) list ->
    6.15      Attrib.src option -> theory -> theory
    6.16 -      * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    6.17 +      * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    6.18    val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
    6.19 -    theory -> theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    6.20 +    theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
    6.21    val defer_recdef: xstring -> string list -> (Facts.ref * Attrib.src list) list
    6.22      -> theory -> theory * {induct_rules: thm}
    6.23    val defer_recdef_i: xstring -> term list -> thm list -> theory -> theory * {induct_rules: thm}
    6.24 @@ -84,7 +84,7 @@
    6.25  
    6.26  (* theory data *)
    6.27  
    6.28 -type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    6.29 +type recdef_info = {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    6.30  
    6.31  structure GlobalRecdefData = Theory_Data
    6.32  (
    6.33 @@ -198,7 +198,7 @@
    6.34      (*We must remove imp_cong to prevent looping when the induction rule
    6.35        is simplified. Many induction rules have nested implications that would
    6.36        give rise to looping conditional rewriting.*)
    6.37 -    val (thy, {rules = rules_idx, induct, tcs}) =
    6.38 +    val (thy, {lhs, rules = rules_idx, induct, tcs}) =
    6.39          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
    6.40                 congs wfs name R eqs;
    6.41      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
    6.42 @@ -211,8 +211,8 @@
    6.43        |> PureThy.add_thmss
    6.44          (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    6.45        ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
    6.46 -      ||> Spec_Rules.add_global Spec_Rules.Equational (tcs, flat rules);
    6.47 -    val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
    6.48 +      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
    6.49 +    val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
    6.50      val thy =
    6.51        thy
    6.52        |> put_recdef name result