# HG changeset patch
# User blanchet
# Date 1398241406 -7200
# Node ID 15cd15f9b40c2ba2d679f1a8ec43b7c1f15c4246
# Parent  029997d3b5d88b62b152ef84e5582b924d26c1e7
allow registration of custom size functions for BNF-based datatypes

diff -r 029997d3b5d8 -r 15cd15f9b40c src/HOL/BNF_LFP.thy
--- 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
diff -r 029997d3b5d8 -r 15cd15f9b40c src/HOL/Tools/BNF/bnf_lfp_size.ML
--- 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, ...}