src/HOL/BNF_FP_Base.thy
changeset 56846 9df717fef2bb
parent 56684 d8f32f55e463
child 57279 88263522c31e
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Sun May 04 16:17:53 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Sun May 04 18:14:58 2014 +0200
     1.3 @@ -195,22 +195,22 @@
     1.4  lemma size_bool[code]: "size (b\<Colon>bool) = 0"
     1.5    by (cases b) auto
     1.6  
     1.7 -lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
     1.8 +lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
     1.9    by (induct n) simp_all
    1.10  
    1.11  declare prod.size[no_atp]
    1.12  
    1.13 -lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
    1.14 +lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    1.15    by (rule ext) (case_tac x, auto)
    1.16  
    1.17 -lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
    1.18 +lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    1.19    by (rule ext) auto
    1.20  
    1.21  setup {*
    1.22 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name sum_size} @{thms sum.size}
    1.23 -  @{thms sum_size_o_map}
    1.24 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name prod_size} @{thms prod.size}
    1.25 -  @{thms prod_size_o_map}
    1.26 +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    1.27 +  @{thms size_sum_o_map}
    1.28 +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    1.29 +  @{thms size_prod_o_map}
    1.30  *}
    1.31  
    1.32  end