src/HOL/BNF_Least_Fixpoint.thy
changeset 58352 37745650a3f4
parent 58314 ee1be8b3032e
child 58376 c9d3074f83b3
     1.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -4,10 +4,10 @@
     1.4      Author:     Jasmin Blanchette, TU Muenchen
     1.5      Copyright   2012, 2013, 2014
     1.6  
     1.7 -Least fixed point operation on bounded natural functors.
     1.8 +Least fixpoint (datatype) operation on bounded natural functors.
     1.9  *)
    1.10  
    1.11 -header {* Least Fixed Point Operation on Bounded Natural Functors *}
    1.12 +header {* Least Fixpoint (Datatype) Operation on Bounded Natural Functors *}
    1.13  
    1.14  theory BNF_Least_Fixpoint
    1.15  imports BNF_Fixpoint_Base
    1.16 @@ -234,27 +234,6 @@
    1.17  ML_file "Tools/Function/old_size.ML"
    1.18  ML_file "Tools/datatype_realizer.ML"
    1.19  
    1.20 -lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.21 -  by (cases b) auto
    1.22 -
    1.23 -lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    1.24 -  by (induct n) simp_all
    1.25 -
    1.26 -declare prod.size[no_atp]
    1.27 -
    1.28 -lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    1.29 -  by (rule ext) (case_tac x, auto)
    1.30 -
    1.31 -lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    1.32 -  by (rule ext) auto
    1.33 -
    1.34 -setup {*
    1.35 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    1.36 -  @{thms size_sum_o_map}
    1.37 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    1.38 -  @{thms size_prod_o_map}
    1.39 -*}
    1.40 -
    1.41  hide_fact (open) id_transfer
    1.42  
    1.43  end