--- a/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Mar 03 12:48:20 2014 +0100
@@ -265,6 +265,7 @@
hide_fact (open) id_transfer
datatype_new 'a F = F 'a
+datatype_compat F
primrec f where
"f (F x) = x"
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 12:48:20 2014 +0100
@@ -20,13 +20,13 @@
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_iters: term list,
+ co_rec: term,
maps: thm list,
common_co_inducts: thm list,
co_inducts: thm list,
- co_iter_thmss: thm list list,
- disc_co_iterss: thm list list,
- sel_co_itersss: thm list list list};
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list};
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
@@ -131,17 +131,17 @@
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_iters: term list,
+ co_rec: term,
maps: thm list,
common_co_inducts: thm list,
co_inducts: thm list,
- co_iter_thmss: thm list list,
- disc_co_iterss: thm list list,
- sel_co_itersss: thm list list list};
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list};
fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
- nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_iters, maps, common_co_inducts, co_inducts,
- co_iter_thmss, disc_co_iterss, sel_co_itersss} : fp_sugar) =
+ nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts,
+ co_rec_thms, disc_co_recs, sel_co_recss} : fp_sugar) =
{T = Morphism.typ phi T,
X = Morphism.typ phi X,
fp = fp,
@@ -154,13 +154,13 @@
ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
- co_iters = map (Morphism.term phi) co_iters,
+ co_rec = Morphism.term phi co_rec,
maps = map (Morphism.thm phi) maps,
common_co_inducts = map (Morphism.thm phi) common_co_inducts,
co_inducts = map (Morphism.thm phi) co_inducts,
- co_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
- disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
- sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
+ co_rec_thms = map (Morphism.thm phi) co_rec_thms,
+ disc_co_recs = map (Morphism.thm phi) disc_co_recs,
+ sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss};
val transfer_fp_sugar =
morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -190,17 +190,17 @@
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
fun register_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...})
- ctrXs_Tsss ctr_defss ctr_sugars co_iterss mapss common_co_inducts co_inductss co_iter_thmsss
- disc_co_itersss sel_co_iterssss lthy =
+ ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss
+ disc_co_recss sel_co_recsss lthy =
(0, lthy)
|> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
- ctr_sugar = nth ctr_sugars kk, co_iters = nth co_iterss kk, maps = nth mapss kk,
+ ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, maps = nth mapss kk,
common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
- co_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
- sel_co_itersss = nth sel_co_iterssss kk}
+ co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
+ sel_co_recss = nth sel_co_recsss kk}
lthy)) Ts
|> snd;
@@ -1364,9 +1364,9 @@
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
- val (iterss', rec_thmss') =
- if iterss = [[]] then ([map #casex ctr_sugars], map #case_thms ctr_sugars)
- else (iterss, rec_thmss);
+ val (recs, rec_thmss') =
+ if iterss = [[]] then (map #casex ctr_sugars, map #case_thms ctr_sugars)
+ else (map the_single iterss, rec_thmss);
val simp_thmss =
map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss;
@@ -1388,8 +1388,8 @@
I)
|> Local_Theory.notes (common_notes @ notes) |> snd
|> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
- ctrXs_Tsss ctr_defss ctr_sugars iterss' mapss [induct_thm] (map single induct_thms)
- (map single rec_thmss') (replicate nn []) (replicate nn [])
+ ctrXs_Tsss ctr_defss ctr_sugars recs mapss [induct_thm] (map single induct_thms)
+ rec_thmss' (replicate nn []) (replicate nn [])
end;
fun derive_note_coinduct_coiters_thms_for_types
@@ -1446,9 +1446,9 @@
|> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
|> Local_Theory.notes (common_notes @ notes) |> snd
|> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
- ctrXs_Tsss ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm]
- (transpose [coinduct_thms, strong_coinduct_thms]) (map single corec_thmss)
- (map single disc_corec_thmss) (map single sel_corec_thmsss)
+ ctrXs_Tsss ctr_defss ctr_sugars (map the_single coiterss) mapss
+ [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
+ corec_thmss disc_corec_thmss sel_corec_thmsss
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 12:48:20 2014 +0100
@@ -274,19 +274,20 @@
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
- fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_iters maps
+ fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
co_inducts co_rec_thms disc_corec_thms sel_corec_thmss =
{T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
- ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_iters = co_iters,
+ ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
- co_iter_thmss = [co_rec_thms], disc_co_iterss = [disc_corec_thms],
- sel_co_itersss = [sel_corec_thmss]}
+ co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
+ sel_co_recss = sel_corec_thmss}
|> morph_fp_sugar phi;
val target_fp_sugars =
map14 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
- co_iterss mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss;
+ (map the_single co_iterss) mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
+ sel_corec_thmsss;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 03 12:48:20 2014 +0100
@@ -374,7 +374,7 @@
let
val thy = Proof_Context.theory_of lthy0;
- val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _,
+ val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_rec = corec,
common_co_inducts = common_coinduct_thms, ...} :: _,
(_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
@@ -394,7 +394,7 @@
val perm_Ts = map #T perm_fp_sugars;
val perm_Xs = map #X perm_fp_sugars;
- val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars;
+ val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -454,27 +454,22 @@
end;
fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
- : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
- let
- val p_ios = map SOME p_is @ [NONE];
- val corec_thms = co_rec_of coiter_thmss;
- val disc_corecs = co_rec_of disc_coiterss;
- val sel_corecss = co_rec_of sel_coitersss;
- in
+ : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
+ let val p_ios = map SOME p_is @ [NONE] in
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
disc_excludesss collapses corec_thms disc_corecs sel_corecss
end;
- fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
- co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
- sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
- {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
+ fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec,
+ co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
+ sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' corec,
disc_exhausts = disc_exhausts,
nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
nested_map_comps = map map_comp_of_bnf nested_bnfs,
- ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
- sel_coitersss};
+ ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
+ sel_corecss};
in
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 12:48:20 2014 +0100
@@ -146,8 +146,8 @@
(kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
- val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
- val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
+ val recs = map (fst o dest_Const o #co_rec) fp_sugars;
+ val rec_thms = maps #co_rec_thms fp_sugars;
fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Mar 03 12:48:20 2014 +0100
@@ -21,10 +21,10 @@
fun is_new_datatype ctxt s =
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
-fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_iters = iters,
- co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx,
+ co_rec_thms = rec_thms, ...} : fp_sugar) =
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
+ ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms};
fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let
@@ -35,7 +35,7 @@
val Ts = map #T fp_sugars;
val Xs = map #X fp_sugars;
- val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
+ val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
val Xs_TCs = Xs ~~ (Ts ~~ Cs);
fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]