equal
deleted
inserted
replaced
184 ML_file "Tools/BNF/bnf_lfp_util.ML" |
184 ML_file "Tools/BNF/bnf_lfp_util.ML" |
185 ML_file "Tools/BNF/bnf_lfp_tactics.ML" |
185 ML_file "Tools/BNF/bnf_lfp_tactics.ML" |
186 ML_file "Tools/BNF/bnf_lfp.ML" |
186 ML_file "Tools/BNF/bnf_lfp.ML" |
187 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
187 ML_file "Tools/BNF/bnf_lfp_compat.ML" |
188 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
188 ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" |
|
189 ML_file "Tools/BNF/bnf_lfp_size.ML" |
|
190 ML_file "Tools/Function/old_size.ML" |
|
191 |
|
192 lemma size_bool[code]: "size (b\<Colon>bool) = 0" |
|
193 by (cases b) auto |
|
194 |
|
195 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n" |
|
196 by (induct n) simp_all |
|
197 |
|
198 declare prod.size[no_atp] |
|
199 |
|
200 lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)" |
|
201 by (rule ext) (case_tac x, auto) |
|
202 |
|
203 lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)" |
|
204 by (rule ext) auto |
|
205 |
|
206 setup {* |
|
207 BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} |
|
208 @{thms size_sum_o_map} |
|
209 #> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} |
|
210 @{thms size_prod_o_map} |
|
211 *} |
189 |
212 |
190 hide_fact (open) id_transfer |
213 hide_fact (open) id_transfer |
191 |
214 |
192 end |
215 end |