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_defss: thm list list, |
17 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, |
17 ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, |
18 un_folds: term list, |
18 co_iterss: term list list, |
19 co_recs: term list, |
|
20 co_induct: thm, |
19 co_induct: thm, |
21 strong_co_induct: thm, |
20 strong_co_induct: thm, |
22 un_fold_thmss: thm list list, |
21 un_fold_thmss: thm list list, |
23 co_rec_thmss: thm list list}; |
22 co_rec_thmss: thm list list}; |
24 |
23 |
101 index: int, |
100 index: int, |
102 pre_bnfs: bnf list, |
101 pre_bnfs: bnf list, |
103 fp_res: fp_result, |
102 fp_res: fp_result, |
104 ctr_defss: thm list list, |
103 ctr_defss: thm list list, |
105 ctr_sugars: ctr_sugar list, |
104 ctr_sugars: ctr_sugar list, |
106 un_folds: term list, |
105 co_iterss: term list list, |
107 co_recs: term list, |
|
108 co_induct: thm, |
106 co_induct: thm, |
109 strong_co_induct: thm, |
107 strong_co_induct: thm, |
110 un_fold_thmss: thm list list, |
108 un_fold_thmss: thm list list, |
111 co_rec_thmss: thm list list}; |
109 co_rec_thmss: thm list list}; |
112 |
110 |
114 |
112 |
115 fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
113 fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar, |
116 {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
114 {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) = |
117 T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
115 T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
118 |
116 |
119 fun morph_fp_sugar phi {T, fp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, un_folds, |
117 fun morph_fp_sugar phi {T, fp, index, pre_bnfs, fp_res, ctr_defss, ctr_sugars, co_iterss, co_induct, |
120 co_recs, co_induct, strong_co_induct, un_fold_thmss, co_rec_thmss} = |
118 strong_co_induct, un_fold_thmss, co_rec_thmss} = |
121 {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) |
119 {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) |
122 pre_bnfs, fp_res = morph_fp_result phi fp_res, |
120 pre_bnfs, fp_res = morph_fp_result phi fp_res, |
123 ctr_defss = map (map (Morphism.thm phi)) ctr_defss, |
121 ctr_defss = map (map (Morphism.thm phi)) ctr_defss, |
124 ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, un_folds = map (Morphism.term phi) un_folds, |
122 ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, |
125 co_recs = map (Morphism.term phi) co_recs, co_induct = Morphism.thm phi co_induct, |
123 co_iterss = map (map (Morphism.term phi)) co_iterss, co_induct = Morphism.thm phi co_induct, |
126 strong_co_induct = Morphism.thm phi strong_co_induct, |
124 strong_co_induct = Morphism.thm phi strong_co_induct, |
127 un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, |
125 un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss, |
128 co_rec_thmss = map (map (Morphism.thm phi)) co_rec_thmss}; |
126 co_rec_thmss = map (map (Morphism.thm phi)) co_rec_thmss}; |
129 |
127 |
130 structure Data = Generic_Data |
128 structure Data = Generic_Data |
139 |
137 |
140 fun register_fp_sugar key fp_sugar = |
138 fun register_fp_sugar key fp_sugar = |
141 Local_Theory.declaration {syntax = false, pervasive = true} |
139 Local_Theory.declaration {syntax = false, pervasive = true} |
142 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
140 (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar))); |
143 |
141 |
144 fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars [un_folds, co_recs] |
142 fun register_fp_sugars fp pre_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss' |
145 co_induct strong_co_induct [un_fold_thmss, co_rec_thmss] lthy = |
143 co_induct strong_co_induct [un_fold_thmss, co_rec_thmss] lthy = |
146 (0, lthy) |
144 (0, lthy) |
147 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
145 |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, |
148 register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, |
146 register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res, |
149 ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, |
147 ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = transpose co_iterss', |
150 co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, |
148 co_induct = co_induct, strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss, |
151 co_rec_thmss = co_rec_thmss} lthy)) Ts |
149 co_rec_thmss = co_rec_thmss} lthy)) Ts |
152 |> snd; |
150 |> snd; |
153 |
151 |
154 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
152 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |