added registration of equational theorems from prim_rec and rec_def to Spec_Rules
authorbulwahn
Wed Jan 20 18:02:22 2010 +0100 (2010-01-20)
changeset 34952bd7e347eb768
parent 34951 1dfb1df1d9d0
child 34953 a053ad2a7a72
added registration of equational theorems from prim_rec and rec_def to Spec_Rules
src/HOL/Tools/old_primrec.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/recdef.ML
     1.1 --- a/src/HOL/Tools/old_primrec.ML	Wed Jan 20 14:09:46 2010 +0100
     1.2 +++ b/src/HOL/Tools/old_primrec.ML	Wed Jan 20 18:02:22 2010 +0100
     1.3 @@ -281,11 +281,14 @@
     1.4        thy'
     1.5        |> fold_map note ((map fst eqns ~~ atts) ~~ map single simps);
     1.6      val simps'' = maps snd simps';
     1.7 +    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
     1.8 +    val specs = (distinct (op =) (map dest_eqn simps''), simps'')
     1.9    in
    1.10      thy''
    1.11      |> note (("simps",
    1.12          [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]), simps'')
    1.13      |> snd
    1.14 +    |> Spec_Rules.add_global Spec_Rules.Equational specs
    1.15      |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
    1.16      |> snd
    1.17      |> Sign.parent_path
     2.1 --- a/src/HOL/Tools/primrec.ML	Wed Jan 20 14:09:46 2010 +0100
     2.2 +++ b/src/HOL/Tools/primrec.ML	Wed Jan 20 18:02:22 2010 +0100
     2.3 @@ -265,6 +265,15 @@
     2.4  
     2.5  local
     2.6  
     2.7 +fun specs_of simps =
     2.8 +  let
     2.9 +    val eqns = maps snd simps
    2.10 +    fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
    2.11 +    val t = distinct (op =) (map dest_eqn eqns)
    2.12 +  in
    2.13 +    (t, eqns)
    2.14 +  end
    2.15 +
    2.16  fun gen_primrec prep_spec raw_fixes raw_spec lthy =
    2.17    let
    2.18      val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
    2.19 @@ -277,7 +286,8 @@
    2.20      lthy
    2.21      |> add_primrec_simple fixes (map snd spec)
    2.22      |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
    2.23 -      #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
    2.24 +      #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')
    2.25 +      ##> (Spec_Rules.add Spec_Rules.Equational (specs_of simps'))))
    2.26      |>> snd
    2.27    end;
    2.28  
     3.1 --- a/src/HOL/Tools/recdef.ML	Wed Jan 20 14:09:46 2010 +0100
     3.2 +++ b/src/HOL/Tools/recdef.ML	Wed Jan 20 18:02:22 2010 +0100
     3.3 @@ -204,13 +204,18 @@
     3.4      val simp_att =
     3.5        if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
     3.6        else [];
     3.7 -
     3.8 +    fun specs_of simps =
     3.9 +      let
    3.10 +        fun dest_eqn th = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
    3.11 +        val ts = distinct (op =) (map dest_eqn simps)
    3.12 +      in (ts, simps) end
    3.13      val ((simps' :: rules', [induct']), thy) =
    3.14        thy
    3.15        |> Sign.add_path bname
    3.16        |> PureThy.add_thmss
    3.17          (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
    3.18 -      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])];
    3.19 +      ||>> PureThy.add_thms [((Binding.name "induct", induct), [])]
    3.20 +      ||> Spec_Rules.add_global Spec_Rules.Equational (specs_of (flat rules));
    3.21      val result = {simps = simps', rules = rules', induct = induct', tcs = tcs};
    3.22      val thy =
    3.23        thy