--- a/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200
@@ -207,8 +207,6 @@
lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
by (simp add: inj_on_def)
-declare [[ML_print_depth = 10000]] (*###*)
-
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
@@ -218,59 +216,4 @@
hide_fact (open) id_transfer
-datatype_new 'a i = I 'a
-thm i.size i.rec_o_map i.size_o_map
-
-datatype_new ('a, 'b) j = J0 | J 'a "('a, 'b) j"
-thm j.size j.rec_o_map j.size_o_map
-
-datatype_new 'a l = N nat nat | C 'a "'a l"
-thm l.size l.rec_o_map l.size_o_map
-
-datatype_new ('a, 'b) x = XN 'b | XC 'a "('a, 'b) x"
-thm x.size x.rec_o_map x.size_o_map
-
-datatype_new
- 'a tl = TN | TC "'a mt" "'a tl" and
- 'a mt = MT 'a "'a tl"
-thm tl.size tl.rec_o_map tl.size_o_map
-thm mt.size mt.rec_o_map mt.size_o_map
-
-datatype_new 'a t = T nat 'a "'a t l"
-thm t.size t.rec_o_map t.size_o_map
-
-datatype_new 'a fset = FSet0 | FSet 'a "'a fset"
-thm fset.size fset.rec_o_map fset.size_o_map
-
-datatype_new 'a u = U 'a "'a u fset"
-thm u.size u.rec_o_map u.size_o_map
-
-datatype_new
- ('a, 'b) v = V "nat l" | V' 'a "('a, 'b) w" and
- ('a, 'b) w = W 'b "('a, 'b) v fset l"
-thm v.size v.rec_o_map v.size_o_map
-thm w.size w.rec_o_map w.size_o_map
-
-(*TODO:
-* what happens if recursion through arbitrary bnf, like 'fsize'?
- * by default
- * offer possibility to register size function and theorems
-* compat with old size?
- * recursion of old through new (e.g. through list)?
- * recursion of new through old?
- * should they share theory data?
-* code generator setup?
-*)
-
-
end
-datatype_new 'a x = X0 | X 'a (*###*)
-thm x.size
-thm x.size_o_map
-datatype_new 'a x = X0 | X 'a "'a x" (*###*)
-thm x.size
-thm x.size_o_map
-datatype_new 'a l = N | C 'a "'a l"
-datatype_new ('a, 'b) tl = TN 'b | TC 'a "'a l"
-
-end
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:26 2014 +0200
@@ -5,7 +5,12 @@
Generation of size functions for new-style datatypes.
*)
-structure BNF_LFP_Size : sig end =
+signature BNF_LFP_SIZE =
+sig
+ val register_size: string -> string -> thm list -> thm list -> theory -> theory
+end;
+
+structure BNF_LFP_Size : BNF_LFP_SIZE =
struct
open BNF_Util
@@ -27,6 +32,9 @@
fun merge data = Symtab.merge (K true) data;
);
+fun register_size T_name size_name size_simps size_o_maps =
+ Data.map (Symtab.update_new (T_name, (size_name, (size_simps, size_o_maps))));
+
val zero_nat = @{const zero_class.zero (nat)};
fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
@@ -52,12 +60,13 @@
(ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @ rec_o_map_simp_thms) ctxt));
val size_o_map_simp_thms =
- @{thms o_apply prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
+ @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
unfold_thms_tac ctxt [size_def] THEN
HEADGOAL (rtac (rec_o_map RS trans) THEN'
- asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt));
+ asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN
+ IF_UNSOLVED (unfold_thms_tac ctxt [o_apply] THEN HEADGOAL (rtac refl));
fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs, ...}