equal
deleted
inserted
replaced
57 fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong); |
57 fun mk_pointfull ctxt th = unfold_thms ctxt [o_apply] (th 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 rec_o_map_simps = |
|
63 @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def}; |
|
64 |
|
65 val size_gen_o_map_simps = @{thms prod.inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
62 val size_gen_o_map_simps = @{thms prod.inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; |
66 |
63 |
67 fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = |
64 fun mk_size_gen_o_map_tac ctxt size_def rec_o_map inj_maps size_maps = |
68 unfold_thms_tac ctxt [size_def] THEN |
65 unfold_thms_tac ctxt [size_def] THEN |
69 HEADGOAL (rtac (rec_o_map RS trans) THEN' |
66 HEADGOAL (rtac (rec_o_map RS trans) THEN' |
75 ALLGOALS (hyp_subst_tac ctxt) THEN |
72 ALLGOALS (hyp_subst_tac ctxt) THEN |
76 Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN |
73 Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN |
77 ALLGOALS (REPEAT_DETERM o (rtac @{thm zero_less_Suc} ORELSE' rtac @{thm trans_less_add2})); |
74 ALLGOALS (REPEAT_DETERM o (rtac @{thm zero_less_Suc} ORELSE' rtac @{thm trans_less_add2})); |
78 |
75 |
79 fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, |
76 fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, |
80 fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_maps = ctor_rec_o_maps, ...}, fp_nesting_bnfs, |
77 fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _) |
81 live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 = |
78 lthy0 = |
82 let |
79 let |
83 val data = Data.get (Context.Proof lthy0); |
80 val data = Data.get (Context.Proof lthy0); |
84 |
81 |
85 val Ts = map #T fp_sugars |
82 val Ts = map #T fp_sugars |
86 val T_names = map (fst o dest_Type) Ts; |
83 val T_names = map (fst o dest_Type) Ts; |