1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 18 19:57:59 2013 +0200
1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 18 20:43:55 2013 +0200
1.3 @@ -31,6 +31,8 @@
1.4 sels: term list,
1.5 pred: int option,
1.6 calls: corec_call list,
1.7 + discI: thm,
1.8 + sel_thms: thm list,
1.9 collapse: thm,
1.10 corec_thm: thm,
1.11 disc_corec: thm,
1.12 @@ -96,6 +98,8 @@
1.13 sels: term list,
1.14 pred: int option,
1.15 calls: corec_call list,
1.16 + discI: thm,
1.17 + sel_thms: thm list,
1.18 collapse: thm,
1.19 corec_thm: thm,
1.20 disc_corec: thm,
1.21 @@ -431,11 +435,13 @@
1.22 else No_Corec) g_i
1.23 | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
1.24
1.25 - fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
1.26 + fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
1.27 + disc_corec sel_corecs =
1.28 let val nullary = not (can dest_funT (fastype_of ctr)) in
1.29 {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
1.30 - calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
1.31 - corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs}
1.32 + calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
1.33 + collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
1.34 + sel_corecs = sel_corecs}
1.35 end;
1.36
1.37 fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
1.38 @@ -445,14 +451,16 @@
1.39 val discs = #discs (nth ctr_sugars index);
1.40 val selss = #selss (nth ctr_sugars index);
1.41 val p_ios = map SOME p_is @ [NONE];
1.42 + val discIs = #discIs (nth ctr_sugars index);
1.43 + val sel_thmss = #sel_thmss (nth ctr_sugars index);
1.44 val collapses = #collapses (nth ctr_sugars index);
1.45 val corec_thms = co_rec_of (nth coiter_thmsss index);
1.46 val disc_corecs = (case co_rec_of (nth disc_coitersss index) of [] => [TrueI]
1.47 | thms => thms);
1.48 val sel_corecss = co_rec_of (nth sel_coiterssss index);
1.49 in
1.50 - map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
1.51 - disc_corecs sel_corecss
1.52 + map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
1.53 + corec_thms disc_corecs sel_corecss
1.54 end;
1.55
1.56 fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,