28 val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv}; |
28 val nested_simps = @{thms o_def[abs_def] id_def split fst_conv snd_conv}; |
29 |
29 |
30 fun special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps = |
30 fun special_endgame_tac ctxt fp_nesting_map_ident0s fp_nesting_map_comps fp_nesting_pred_maps = |
31 ALLGOALS (CONVERSION Thm.eta_long_conversion) THEN |
31 ALLGOALS (CONVERSION Thm.eta_long_conversion) THEN |
32 HEADGOAL (simp_tac (ss_only @{thms pred_fun_True_id} ctxt |
32 HEADGOAL (simp_tac (ss_only @{thms pred_fun_True_id} ctxt |
33 addsimprocs [@{simproc NO_MATCH}])) THEN |
33 addsimprocs [\<^simproc>\<open>NO_MATCH\<close>])) THEN |
34 unfold_thms_tac ctxt (nested_simps @ |
34 unfold_thms_tac ctxt (nested_simps @ |
35 map (unfold_thms ctxt @{thms id_def}) (fp_nesting_map_ident0s @ fp_nesting_map_comps @ |
35 map (unfold_thms ctxt @{thms id_def}) (fp_nesting_map_ident0s @ fp_nesting_map_comps @ |
36 fp_nesting_pred_maps)) THEN |
36 fp_nesting_pred_maps)) THEN |
37 ALLGOALS (rtac ctxt refl); |
37 ALLGOALS (rtac ctxt refl); |
38 |
38 |
39 fun is_new_datatype _ @{type_name nat} = true |
39 fun is_new_datatype _ \<^type_name>\<open>nat\<close> = true |
40 | is_new_datatype ctxt s = |
40 | is_new_datatype ctxt s = |
41 (case fp_sugar_of ctxt s of |
41 (case fp_sugar_of ctxt s of |
42 SOME {fp = Least_FP, fp_co_induct_sugar = SOME _, ...} => true |
42 SOME {fp = Least_FP, fp_co_induct_sugar = SOME _, ...} => true |
43 | _ => false); |
43 | _ => false); |
44 |
44 |
45 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, |
45 fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, fp_ctr_sugar = {ctr_sugar, ...}, |
46 fp_co_induct_sugar = SOME {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
46 fp_co_induct_sugar = SOME {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = |
47 {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
47 {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, |
48 recx = recx, rec_thms = rec_thms}; |
48 recx = recx, rec_thms = rec_thms}; |
49 |
49 |
50 fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy = |
50 fun basic_lfp_sugars_of _ [\<^typ>\<open>nat\<close>] _ _ lthy = |
51 ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy) |
51 ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy) |
52 | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
52 | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 = |
53 let |
53 let |
54 val ((missing_arg_Ts, perm0_kks, |
54 val ((missing_arg_Ts, perm0_kks, |
55 fp_sugars as {fp_nesting_bnfs, |
55 fp_sugars as {fp_nesting_bnfs, |
97 fun y_of_y' () = massage_no_call (yU, yT) $ y'; |
97 fun y_of_y' () = massage_no_call (yU, yT) $ y'; |
98 val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
98 val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
99 |
99 |
100 fun massage_mutual_fun U T t = |
100 fun massage_mutual_fun U T t = |
101 (case t of |
101 (case t of |
102 Const (@{const_name comp}, _) $ t1 $ t2 => |
102 Const (\<^const_name>\<open>comp\<close>, _) $ t1 $ t2 => |
103 mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
103 mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
104 | _ => |
104 | _ => |
105 if has_call t then massage_fun U T t else mk_comp bound_Ts (t, massage_no_call (U, T))); |
105 if has_call t then massage_fun U T t else mk_comp bound_Ts (t, massage_no_call (U, T))); |
106 |
106 |
107 fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |
107 fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |