equal
deleted
inserted
replaced
52 |
52 |
53 fun mk_to_natT T = T --> HOLogic.natT; |
53 fun mk_to_natT T = T --> HOLogic.natT; |
54 |
54 |
55 fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero; |
55 fun mk_abs_zero_nat T = Term.absdummy T HOLogic.zero; |
56 |
56 |
57 fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong); |
57 fun mk_pointful ctxt thm = unfold_thms ctxt [o_apply] (thm RS fun_cong); |
58 |
58 |
59 fun mk_unabs_def_unused_0 n = |
59 fun mk_unabs_def_unused_0 n = |
60 funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); |
60 funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong); |
61 |
61 |
62 val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
62 val size_gen_o_map_simps = @{thms inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
233 |
233 |
234 val all_overloaded_size_defs = overloaded_size_defs @ |
234 val all_overloaded_size_defs = overloaded_size_defs @ |
235 (Spec_Rules.retrieve lthy0 @{const size ('a)} |
235 (Spec_Rules.retrieve lthy0 @{const size ('a)} |
236 |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); |
236 |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); |
237 |
237 |
238 val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; |
238 val nested_size_maps = map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; |
239 val all_inj_maps = |
239 val all_inj_maps = |
240 @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) |
240 @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) |
241 |> distinct Thm.eq_thm_prop; |
241 |> distinct Thm.eq_thm_prop; |
242 |
242 |
243 fun derive_size_simp size_def' simp0 = |
243 fun derive_size_simp size_def' simp0 = |