9 sig |
9 sig |
10 type fp_sugar = |
10 type fp_sugar = |
11 {T: typ, |
11 {T: typ, |
12 fp: BNF_FP_Util.fp_kind, |
12 fp: BNF_FP_Util.fp_kind, |
13 index: int, |
13 index: int, |
14 Xs: typ list, |
|
15 ctr_TsssXs : typ list list list, |
|
16 pre_bnfs: BNF_Def.bnf list, |
14 pre_bnfs: BNF_Def.bnf list, |
17 fp_res: BNF_FP_Util.fp_result, |
15 fp_res: BNF_FP_Util.fp_result, |
18 ctr_defss: thm list list, |
16 ctr_defss: thm list list, |
19 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, |
17 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, |
20 un_folds: term list, |
18 un_folds: term list, |
122 |
118 |
123 fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
119 fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
124 {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
120 {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
125 T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
121 T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
126 |
122 |
127 (* There is no point in morphing the low-level fields "Xs" and "ctr_TsssXs". *) |
123 fun morph_fp_sugar phi {T, fp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds, |
128 fun morph_fp_sugar phi {T, fp, index, Xs, ctr_TsssXs, pre_bnfs, fp_res, ctr_defss, ctr_sugars, |
124 co_recs, co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} = |
129 un_folds, co_recs, co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} = |
125 {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) |
130 {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
126 pre_bnfs, fp_res = morph_fp_result phi fp_res, |
131 Xs = Xs, ctr_TsssXs = ctr_TsssXs, fp_res = morph_fp_result phi fp_res, |
|
132 ctr_defss = map (map (Morphism.thm phi)) ctr_defss, |
127 ctr_defss = map (map (Morphism.thm phi)) ctr_defss, |
133 ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds, |
128 ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds, |
134 co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct, |
129 co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct, |
135 strong_co_induct = Morphism.thm phi strong_co_induct, |
130 strong_co_induct = Morphism.thm phi strong_co_induct, |
136 un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, |
131 un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, |
148 |
143 |
149 fun register_fp_sugar key fp_sugar = |
144 fun register_fp_sugar key fp_sugar = |
150 Local_Theory.declaration {syntax = false, pervasive = true} |
145 Local_Theory.declaration {syntax = false, pervasive = true} |
151 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
146 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
152 |
147 |
153 fun register_fp_sugars fp Xs ctr_TsssXs pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds |
148 fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs |
154 co_recs co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy = |
149 co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy = |
155 (0, lthy) |
150 (0, lthy) |
156 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
151 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
157 register_fp_sugar s {T = T, fp = fp, index = kk, Xs = Xs, ctr_TsssXs = ctr_TsssXs, |
152 register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, |
158 pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, |
153 ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, |
159 un_folds = un_folds, co_recs = co_recs, co_induct = co_induct, |
154 co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, |
160 strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, |
|
161 co_rec_thmss = co_rec_thmss} lthy)) Ts |
155 co_rec_thmss = co_rec_thmss} lthy)) Ts |
162 |> snd; |
156 |> snd; |
163 |
157 |
164 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
158 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
165 fun quasi_unambiguous_case_names names = |
159 fun quasi_unambiguous_case_names names = |
1382 (simpsN, simp_thmss, K [])] |
1376 (simpsN, simp_thmss, K [])] |
1383 |> massage_multi_notes; |
1377 |> massage_multi_notes; |
1384 in |
1378 in |
1385 lthy |
1379 lthy |
1386 |> Local_Theory.notes (common_notes @ notes) |> snd |
1380 |> Local_Theory.notes (common_notes @ notes) |> snd |
1387 |> register_fp_sugars Least_FP Xs ctr_TsssXs pre_bnfs fp_res ctr_defss ctr_sugars folds recs |
1381 |> register_fp_sugars Least_FP pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm |
1388 induct_thm induct_thm fold_thmss rec_thmss |
1382 induct_thm fold_thmss rec_thmss |
1389 end; |
1383 end; |
1390 |
1384 |
1391 fun derive_and_note_coinduct_unfold_corec_thms_for_types |
1385 fun derive_and_note_coinduct_unfold_corec_thms_for_types |
1392 ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), |
1386 ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), |
1393 (unfolds, corecs, unfold_defs, corec_defs)), lthy) = |
1387 (unfolds, corecs, unfold_defs, corec_defs)), lthy) = |
1441 (unfoldN, unfold_thmss, K coiter_attrs)] |
1435 (unfoldN, unfold_thmss, K coiter_attrs)] |
1442 |> massage_multi_notes; |
1436 |> massage_multi_notes; |
1443 in |
1437 in |
1444 lthy |
1438 lthy |
1445 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |
1439 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |
1446 |> register_fp_sugars Greatest_FP Xs ctr_TsssXs pre_bnfs fp_res ctr_defss ctr_sugars unfolds |
1440 |> register_fp_sugars Greatest_FP pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs |
1447 corecs coinduct_thm strong_coinduct_thm unfold_thmss corec_thmss |
1441 coinduct_thm strong_coinduct_thm unfold_thmss corec_thmss |
1448 end; |
1442 end; |
1449 |
1443 |
1450 val lthy' = lthy |
1444 val lthy' = lthy |
1451 |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ |
1445 |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ |
1452 fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ |
1446 fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ |