Added datatype hook to declare all case_congs as "fundef_cong" automatically.
1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 07 19:40:56 2006 +0100
1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 07 21:28:14 2006 +0100
1.3 @@ -27,6 +27,7 @@
1.4 val cong_del: attribute
1.5
1.6 val setup : theory -> theory
1.7 + val setup_case_cong_hook : theory -> theory
1.8 val get_congs : theory -> thm list
1.9 end
1.10
1.11 @@ -162,17 +163,35 @@
1.12 val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
1.13 val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
1.14
1.15 +(* Datatype hook to declare datatype congs as "fundef_congs" *)
1.16 +
1.17 +
1.18 +fun add_case_cong n thy =
1.19 + Context.theory_map (map_fundef_congs (Drule.add_rule
1.20 + (DatatypePackage.get_datatype thy n |> the
1.21 + |> #case_cong
1.22 + |> safe_mk_meta_eq)))
1.23 + thy
1.24 +
1.25 +val case_cong_hook = fold add_case_cong
1.26 +
1.27 +val setup_case_cong_hook =
1.28 + DatatypeHooks.add case_cong_hook
1.29 + #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
1.30
1.31 (* setup *)
1.32
1.33 -val setup = FundefData.init #> FundefCongs.init
1.34 - #> Attrib.add_attributes
1.35 - [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
1.36 -
1.37 +val setup =
1.38 + FundefData.init
1.39 + #> FundefCongs.init
1.40 + #> Attrib.add_attributes
1.41 + [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
1.42 + #> setup_case_cong_hook
1.43
1.44 val get_congs = FundefCommon.get_fundef_congs o Context.Theory
1.45
1.46
1.47 +
1.48 (* outer syntax *)
1.49
1.50 local structure P = OuterParse and K = OuterKeyword in