equal
deleted
inserted
replaced
28 val size_neqN = "size_neq"; |
28 val size_neqN = "size_neq"; |
29 |
29 |
30 val nitpicksimp_attrs = @{attributes [nitpick_simp]}; |
30 val nitpicksimp_attrs = @{attributes [nitpick_simp]}; |
31 val simp_attrs = @{attributes [simp]}; |
31 val simp_attrs = @{attributes [simp]}; |
32 |
32 |
33 fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus}, |
33 fun mk_plus_nat (t1, t2) = Const (\<^const_name>\<open>Groups.plus\<close>, |
34 HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; |
34 HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; |
35 |
35 |
36 fun mk_to_natT T = T --> HOLogic.natT; |
36 fun mk_to_natT T = T --> HOLogic.natT; |
37 |
37 |
38 fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero; |
38 fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero; |
49 ); |
49 ); |
50 |
50 |
51 fun check_size_type thy T_name size_name = |
51 fun check_size_type thy T_name size_name = |
52 let |
52 let |
53 val n = Sign.arity_number thy T_name; |
53 val n = Sign.arity_number thy T_name; |
54 val As = map (fn s => TFree (s, @{sort type})) (Name.invent Name.context Name.aT n); |
54 val As = map (fn s => TFree (s, \<^sort>\<open>type\<close>)) (Name.invent Name.context Name.aT n); |
55 val T = Type (T_name, As); |
55 val T = Type (T_name, As); |
56 val size_T = map mk_to_natT As ---> mk_to_natT T; |
56 val size_T = map mk_to_natT As ---> mk_to_natT T; |
57 val size_const = Const (size_name, size_T); |
57 val size_const = Const (size_name, size_T); |
58 in |
58 in |
59 can (Thm.global_cterm_of thy) size_const orelse |
59 can (Thm.global_cterm_of thy) size_const orelse |
130 |
130 |
131 val size_bs = |
131 val size_bs = |
132 map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o |
132 map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o |
133 Long_Name.base_name) T_names; |
133 Long_Name.base_name) T_names; |
134 |
134 |
135 fun is_prod_C @{type_name prod} [_, T'] = member (op =) Cs T' |
135 fun is_prod_C \<^type_name>\<open>prod\<close> [_, T'] = member (op =) Cs T' |
136 | is_prod_C _ _ = false; |
136 | is_prod_C _ _ = false; |
137 |
137 |
138 fun mk_size_of_typ (T as TFree _) = |
138 fun mk_size_of_typ (T as TFree _) = |
139 pair (case AList.lookup (op =) As_fs T of |
139 pair (case AList.lookup (op =) As_fs T of |
140 SOME f => f |
140 SOME f => f |
225 |
225 |
226 val zeros = map mk_abs_zero_nat As; |
226 val zeros = map mk_abs_zero_nat As; |
227 |
227 |
228 val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts; |
228 val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts; |
229 val overloaded_size_Ts = map fastype_of overloaded_size_rhss; |
229 val overloaded_size_Ts = map fastype_of overloaded_size_rhss; |
230 val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts; |
230 val overloaded_size_consts = map (curry Const \<^const_name>\<open>size\<close>) overloaded_size_Ts; |
231 val overloaded_size_def_bs = |
231 val overloaded_size_def_bs = |
232 map (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs; |
232 map (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs; |
233 |
233 |
234 fun define_overloaded_size def_b lhs0 rhs lthy = |
234 fun define_overloaded_size def_b lhs0 rhs lthy = |
235 let |
235 let |
280 val size_thmss = map2 append size_simpss overloaded_size_simpss; |
280 val size_thmss = map2 append size_simpss overloaded_size_simpss; |
281 val size_gen_thmss = size_simpss; |
281 val size_gen_thmss = size_simpss; |
282 |
282 |
283 fun rhs_is_zero thm = |
283 fun rhs_is_zero thm = |
284 let val Const (trueprop, _) $ (Const (eq, _) $ _ $ rhs) = Thm.prop_of thm in |
284 let val Const (trueprop, _) $ (Const (eq, _) $ _ $ rhs) = Thm.prop_of thm in |
285 trueprop = @{const_name Trueprop} andalso eq = @{const_name HOL.eq} andalso |
285 trueprop = \<^const_name>\<open>Trueprop\<close> andalso eq = \<^const_name>\<open>HOL.eq\<close> andalso |
286 rhs = HOLogic.zero |
286 rhs = HOLogic.zero |
287 end; |
287 end; |
288 |
288 |
289 val size_neq_thmss = @{map 3} (fn fp_sugar => fn size => fn size_thms => |
289 val size_neq_thmss = @{map 3} (fn fp_sugar => fn size => fn size_thms => |
290 if exists rhs_is_zero size_thms then |
290 if exists rhs_is_zero size_thms then |
341 val rec_o_maps = |
341 val rec_o_maps = |
342 fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars []; |
342 fold_rev (curry (op @) o #co_rec_o_maps o the o #fp_co_induct_sugar) fp_sugars []; |
343 |
343 |
344 val size_gen_o_map_thmss = |
344 val size_gen_o_map_thmss = |
345 if nested_size_gen_o_maps_complete |
345 if nested_size_gen_o_maps_complete |
346 andalso forall (fn TFree (_, S) => S = @{sort type}) As then |
346 andalso forall (fn TFree (_, S) => S = \<^sort>\<open>type\<close>) As then |
347 @{map 3} (fn goal => fn size_def => fn rec_o_map => |
347 @{map 3} (fn goal => fn size_def => fn rec_o_map => |
348 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
348 Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => |
349 mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |
349 mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |
350 |> Thm.close_derivation |
350 |> Thm.close_derivation |
351 |> single) |
351 |> single) |
391 end) |
391 end) |
392 T_names size_consts overloaded_size_defs)) |
392 T_names size_consts overloaded_size_defs)) |
393 end |
393 end |
394 | generate_datatype_size _ lthy = lthy; |
394 | generate_datatype_size _ lthy = lthy; |
395 |
395 |
396 val size_plugin = Plugin_Name.declare_setup @{binding size}; |
396 val size_plugin = Plugin_Name.declare_setup \<^binding>\<open>size\<close>; |
397 val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size); |
397 val _ = Theory.setup (fp_sugars_interpretation size_plugin generate_datatype_size); |
398 |
398 |
399 end; |
399 end; |