11 {T: typ, |
11 {T: typ, |
12 lfp: bool, |
12 lfp: bool, |
13 index: int, |
13 index: int, |
14 pre_bnfs: BNF_Def.bnf list, |
14 pre_bnfs: BNF_Def.bnf list, |
15 fp_res: BNF_FP_Util.fp_result, |
15 fp_res: BNF_FP_Util.fp_result, |
|
16 ctr_defss: thm list list, |
16 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, |
17 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, |
17 un_folds: term list, |
18 un_folds: term list, |
18 co_recs: term list, |
19 co_recs: term list, |
19 co_induct: thm, |
20 co_induct: thm, |
20 strong_co_induct: thm, |
21 strong_co_induct: thm, |
108 |
110 |
109 fun eq_fp_sugar ({T = T1, lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
111 fun eq_fp_sugar ({T = T1, lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
110 {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
112 {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
111 T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
113 T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
112 |
114 |
113 fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs, co_induct, |
115 fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds, co_recs, |
114 strong_co_induct, un_fold_thmss, co_rec_thmss} = |
116 co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} = |
115 {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
117 {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
116 fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, |
118 fp_res = morph_fp_result phi fp_res, ctr_defss = map (map (Morphism.thm phi)) ctr_defss, |
117 un_folds = map (Morphism.term phi) un_folds, co_recs = map (Morphism.term phi) co_recs, |
119 ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds, |
118 co_induct = Morphism.thm phi co_induct, strong_co_induct = Morphism.thm phi strong_co_induct, |
120 co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct, |
|
121 strong_co_induct = Morphism.thm phi strong_co_induct, |
119 un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, |
122 un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, |
120 co_rec_thmss = map (map (Morphism.thm phi)) co_rec_thmss}; |
123 co_rec_thmss = map (map (Morphism.thm phi)) co_rec_thmss}; |
121 |
124 |
122 structure Data = Generic_Data |
125 structure Data = Generic_Data |
123 ( |
126 ( |
131 |
134 |
132 fun register_fp_sugar key fp_sugar = |
135 fun register_fp_sugar key fp_sugar = |
133 Local_Theory.declaration {syntax = false, pervasive = true} |
136 Local_Theory.declaration {syntax = false, pervasive = true} |
134 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
137 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
135 |
138 |
136 fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_sugars un_folds co_recs co_induct |
139 fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars un_folds co_recs |
137 strong_co_induct un_fold_thmss co_rec_thmss lthy = |
140 co_induct strong_co_induct un_fold_thmss co_rec_thmss lthy = |
138 (0, lthy) |
141 (0, lthy) |
139 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
142 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
140 register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, |
143 register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, |
141 ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, co_induct = co_induct, |
144 ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, |
142 strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, |
145 co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, |
143 co_rec_thmss = co_rec_thmss} lthy)) Ts |
146 co_rec_thmss = co_rec_thmss} lthy)) Ts |
144 |> snd; |
147 |> snd; |
145 |
148 |
146 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
149 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
147 fun quasi_unambiguous_case_names names = |
150 fun quasi_unambiguous_case_names names = |
1346 (simpsN, simp_thmss, K [])] |
1349 (simpsN, simp_thmss, K [])] |
1347 |> massage_multi_notes; |
1350 |> massage_multi_notes; |
1348 in |
1351 in |
1349 lthy |
1352 lthy |
1350 |> Local_Theory.notes (common_notes @ notes) |> snd |
1353 |> Local_Theory.notes (common_notes @ notes) |> snd |
1351 |> register_fp_sugars true pre_bnfs fp_res ctr_sugars folds recs induct_thm induct_thm |
1354 |> register_fp_sugars true pre_bnfs fp_res ctr_defss ctr_sugars folds recs induct_thm |
1352 fold_thmss rec_thmss |
1355 induct_thm fold_thmss rec_thmss |
1353 end; |
1356 end; |
1354 |
1357 |
1355 fun derive_and_note_coinduct_unfold_corec_thms_for_types |
1358 fun derive_and_note_coinduct_unfold_corec_thms_for_types |
1356 ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), |
1359 ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), |
1357 (unfolds, corecs, unfold_defs, corec_defs)), lthy) = |
1360 (unfolds, corecs, unfold_defs, corec_defs)), lthy) = |
1405 (unfoldN, unfold_thmss, K coiter_attrs)] |
1408 (unfoldN, unfold_thmss, K coiter_attrs)] |
1406 |> massage_multi_notes; |
1409 |> massage_multi_notes; |
1407 in |
1410 in |
1408 lthy |
1411 lthy |
1409 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |
1412 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |
1410 |> register_fp_sugars false pre_bnfs fp_res ctr_sugars unfolds corecs coinduct_thm |
1413 |> register_fp_sugars false pre_bnfs fp_res ctr_defss ctr_sugars unfolds corecs coinduct_thm |
1411 strong_coinduct_thm unfold_thmss corec_thmss |
1414 strong_coinduct_thm unfold_thmss corec_thmss |
1412 end; |
1415 end; |
1413 |
1416 |
1414 val lthy' = lthy |
1417 val lthy' = lthy |
1415 |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ |
1418 |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ |