7 |
7 |
8 signature BNF_FP_DEF_SUGAR = |
8 signature BNF_FP_DEF_SUGAR = |
9 sig |
9 sig |
10 type fp = |
10 type fp = |
11 {lfp: bool, |
11 {lfp: bool, |
12 fp_index: int, |
12 index: int, |
|
13 pre_bnfs: BNF_Def.bnf list, |
13 fp_res: BNF_FP.fp_result, |
14 fp_res: BNF_FP.fp_result, |
14 ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result}; |
15 ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result}; |
15 |
16 |
16 val fp_of: Proof.context -> string -> fp option |
17 val fp_of: Proof.context -> string -> fp option |
17 |
18 |
57 |
58 |
58 val EqN = "Eq_"; |
59 val EqN = "Eq_"; |
59 |
60 |
60 type fp = |
61 type fp = |
61 {lfp: bool, |
62 {lfp: bool, |
62 fp_index: int, |
63 index: int, |
|
64 pre_bnfs: bnf list, |
63 fp_res: fp_result, |
65 fp_res: fp_result, |
64 ctr_wrap_res: ctr_wrap_result}; |
66 ctr_wrap_res: ctr_wrap_result}; |
65 |
67 |
66 fun eq_fp ({lfp = lfp1, fp_index = fp_index1, fp_res = fp_res1, ...} : fp, |
68 fun eq_fp ({lfp = lfp1, index = index1, fp_res = fp_res1, ...} : fp, |
67 {lfp = lfp2, fp_index = fp_index2, fp_res = fp_res2, ...} : fp) = |
69 {lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp) = |
68 lfp1 = lfp2 andalso fp_index1 = fp_index2 andalso eq_fp_result (fp_res1, fp_res2); |
70 lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); |
69 |
71 |
70 fun morph_fp phi {lfp, fp_index, fp_res, ctr_wrap_res} = |
72 fun morph_fp phi {lfp, index, pre_bnfs, fp_res, ctr_wrap_res} = |
71 {lfp = lfp, fp_index = fp_index, fp_res = morph_fp_result phi fp_res, |
73 {lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, |
72 ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res}; |
74 fp_res = morph_fp_result phi fp_res, ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res}; |
73 |
75 |
74 structure Data = Generic_Data |
76 structure Data = Generic_Data |
75 ( |
77 ( |
76 type T = fp Symtab.table; |
78 type T = fp Symtab.table; |
77 val empty = Symtab.empty; |
79 val empty = Symtab.empty; |
85 Local_Theory.declaration {syntax = false, pervasive = true} |
87 Local_Theory.declaration {syntax = false, pervasive = true} |
86 (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp))); |
88 (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp))); |
87 |
89 |
88 val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; |
90 val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; |
89 |
91 |
90 fun register_fps lfp (fp_res as {ctors, ...}) ctr_wrap_ress lthy = |
92 fun register_fps lfp pre_bnfs (fp_res as {ctors, ...}) ctr_wrap_ress lthy = |
91 ((1, ctors), lthy) |
93 ((1, ctors), lthy) |
92 |> fold (fn ctr_wrap_res => fn ((kk, ctor :: ctors), lthy) => |
94 |> fold (fn ctr_wrap_res => fn ((kk, ctor :: ctors), lthy) => |
93 ((kk + 1, ctors), register_fp (fp_name_of_ctor ctor) {lfp = lfp, fp_index = kk, |
95 ((kk + 1, ctors), register_fp (fp_name_of_ctor ctor) {lfp = lfp, index = kk, |
94 fp_res = fp_res, ctr_wrap_res = ctr_wrap_res} lthy)) ctr_wrap_ress |
96 pre_bnfs = pre_bnfs, fp_res = fp_res, ctr_wrap_res = ctr_wrap_res} lthy)) ctr_wrap_ress |
95 |> snd; |
97 |> snd; |
96 |
98 |
97 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
99 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *) |
98 fun quasi_unambiguous_case_names names = |
100 fun quasi_unambiguous_case_names names = |
99 let |
101 let |
1314 (simpsN, simp_thmss, K [])] |
1316 (simpsN, simp_thmss, K [])] |
1315 |> massage_multi_notes; |
1317 |> massage_multi_notes; |
1316 in |
1318 in |
1317 lthy |
1319 lthy |
1318 |> Local_Theory.notes (common_notes @ notes) |> snd |
1320 |> Local_Theory.notes (common_notes @ notes) |> snd |
1319 |> register_fps true fp_res ctr_wrap_ress |
1321 |> register_fps true pre_bnfs fp_res ctr_wrap_ress |
1320 end; |
1322 end; |
1321 |
1323 |
1322 fun derive_and_note_coinduct_unfold_corec_thms_for_types |
1324 fun derive_and_note_coinduct_unfold_corec_thms_for_types |
1323 ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)), |
1325 ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)), |
1324 (unfolds, corecs, unfold_defs, corec_defs)), lthy) = |
1326 (unfolds, corecs, unfold_defs, corec_defs)), lthy) = |
1372 (unfoldN, unfold_thmss, K corec_like_attrs)] |
1374 (unfoldN, unfold_thmss, K corec_like_attrs)] |
1373 |> massage_multi_notes; |
1375 |> massage_multi_notes; |
1374 in |
1376 in |
1375 lthy |
1377 lthy |
1376 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |
1378 |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |
1377 |> register_fps false fp_res ctr_wrap_ress |
1379 |> register_fps false pre_bnfs fp_res ctr_wrap_ress |
1378 end; |
1380 end; |
1379 |
1381 |
1380 val lthy' = lthy |
1382 val lthy' = lthy |
1381 |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ |
1383 |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ |
1382 fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ |
1384 fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ |