more unfolding and more folding in size equations, to look more natural in the nested case
authorblanchet
Fri Apr 25 12:09:15 2014 +0200 (2014-04-25)
changeset 56684d8f32f55e463
parent 56683 7f4ae504e059
child 56721 f2ffead641d4
more unfolding and more folding in size equations, to look more natural in the nested case
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_lfp_size.ML
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Fri Apr 25 11:58:10 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Fri Apr 25 12:09:15 2014 +0200
     1.3 @@ -166,10 +166,7 @@
     1.4  lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
     1.5    by (erule arg_cong)
     1.6  
     1.7 -lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
     1.8 -  by (rule ext) simp
     1.9 -
    1.10 -lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
    1.11 +lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
    1.12    unfolding inj_on_def by simp
    1.13  
    1.14  lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Apr 25 11:58:10 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Fri Apr 25 12:09:15 2014 +0200
     2.3 @@ -217,18 +217,23 @@
     2.4      val overloaded_size_defs' =
     2.5        map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
     2.6  
     2.7 +    val all_overloaded_size_defs = overloaded_size_defs @
     2.8 +      (Spec_Rules.retrieve lthy0 @{const size ('a)}
     2.9 +       |> map_filter (try (fn (Equational, (_, [thm])) => thm)));
    2.10 +
    2.11      val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
    2.12      val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
    2.13  
    2.14      fun derive_size_simp size_def' simp0 =
    2.15        (trans OF [size_def', simp0])
    2.16 -      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @
    2.17 +      |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def snd_conv} @
    2.18          all_inj_maps @ nested_size_maps) lthy2)
    2.19        |> fold_thms lthy2 size_defs_unused_0;
    2.20 -    fun derive_overloaded_size_simp size_def' simp0 =
    2.21 -      (trans OF [size_def', simp0])
    2.22 +
    2.23 +    fun derive_overloaded_size_simp overloaded_size_def' simp0 =
    2.24 +      (trans OF [overloaded_size_def', simp0])
    2.25        |> unfold_thms lthy2 @{thms add_0_left add_0_right}
    2.26 -      |> fold_thms lthy2 overloaded_size_defs;
    2.27 +      |> fold_thms lthy2 all_overloaded_size_defs;
    2.28  
    2.29      val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
    2.30      val size_simps = flat size_simpss;