# HG changeset patch
# User blanchet
# Date 1398420555 -7200
# Node ID d8f32f55e4633a9e4fbc96ae0df9c9ddfe9924eb
# Parent  7f4ae504e059399fa63ce18fe16822767933b698
more unfolding and more folding in size equations, to look more natural in the nested case

diff -r 7f4ae504e059 -r d8f32f55e463 src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Fri Apr 25 11:58:10 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy	Fri Apr 25 12:09:15 2014 +0200
@@ -166,10 +166,7 @@
 lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
   by (erule arg_cong)
 
-lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
-  by (rule ext) simp
-
-lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
+lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
   unfolding inj_on_def by simp
 
 lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
diff -r 7f4ae504e059 -r d8f32f55e463 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Apr 25 11:58:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Apr 25 12:09:15 2014 +0200
@@ -217,18 +217,23 @@
     val overloaded_size_defs' =
       map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
 
+    val all_overloaded_size_defs = overloaded_size_defs @
+      (Spec_Rules.retrieve lthy0 @{const size ('a)}
+       |> map_filter (try (fn (Equational, (_, [thm])) => thm)));
+
     val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
     val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
 
     fun derive_size_simp size_def' simp0 =
       (trans OF [size_def', simp0])
-      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @
+      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def snd_conv} @
         all_inj_maps @ nested_size_maps) lthy2)
       |> fold_thms lthy2 size_defs_unused_0;
-    fun derive_overloaded_size_simp size_def' simp0 =
-      (trans OF [size_def', simp0])
+
+    fun derive_overloaded_size_simp overloaded_size_def' simp0 =
+      (trans OF [overloaded_size_def', simp0])
       |> unfold_thms lthy2 @{thms add_0_left add_0_right}
-      |> fold_thms lthy2 overloaded_size_defs;
+      |> fold_thms lthy2 all_overloaded_size_defs;
 
     val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
     val size_simps = flat size_simpss;