--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
@@ -10,16 +10,18 @@
val datatypes: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
BNF_Def.BNF list -> local_theory ->
- (term list * term list * term list *term list * term list * thm * thm list * thm list *
- thm list * thm list * thm list) * local_theory) ->
+ (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
+ thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
+ local_theory) ->
bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
(binding * typ) list) * (binding * term) list) * mixfix) list) list ->
local_theory -> local_theory
val parse_datatype_cmd: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
BNF_Def.BNF list -> local_theory ->
- (term list * term list * term list * term list * term list * thm * thm list * thm list *
- thm list * thm list * thm list) * local_theory) ->
+ (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
+ thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
+ local_theory) ->
(local_theory -> local_theory) parser
end;
@@ -33,10 +35,9 @@
open BNF_FP_Sugar_Tactics
val simp_attrs = @{attributes [simp]};
+val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
-fun split_list9 xs =
- (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
- map #9 xs);
+fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);
fun resort_tfree S (TFree (s, _)) = TFree (s, S);
@@ -60,6 +61,18 @@
fun mk_uncurried2_fun f xss =
mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
+fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
+ Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
+
+fun flip_rels lthy n thm =
+ let
+ val Rs = Term.add_vars (prop_of thm) [];
+ val Rs' = rev (drop (length Rs - n) Rs);
+ val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs';
+ in
+ Drule.cterm_instantiate cRs thm
+ end;
+
fun mk_ctor_or_dtor get_T Ts t =
let val Type (_, Ts0) = get_T (fastype_of t) in
Term.subst_atomic_types (Ts0 ~~ Ts) t
@@ -83,13 +96,10 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun mk_rel Ts Us t =
- let
- val ((Type (_, Ts0), Type (_, Us0)), body) =
- strip_type (fastype_of t) |>> split_last |>> apfst List.last;
- in
- Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
- end;
+fun liveness_of_fp_bnf n bnf =
+ (case T_of_bnf bnf of
+ Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
+ | _ => replicate n false);
fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
@@ -120,7 +130,7 @@
fun defaults_of ((_, ds), _) = ds;
fun ctr_mixfix_of (_, mx) = mx;
-fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
+fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp (no_dests, specs)
no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
@@ -143,11 +153,13 @@
val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
- val ((Xs, Cs), no_defs_lthy) =
+ val (((Bs0, Cs), Xs), no_defs_lthy) =
no_defs_lthy0
|> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
- |> variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS) |>> map TFree
- ||>> mk_TFrees nn;
+ |> mk_TFrees (length unsorted_As)
+ ||>> mk_TFrees nn
+ ||>> apfst (map TFree) o
+ variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS);
(* TODO: cleaner handling of fake contexts, without "background_theory" *)
(*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
@@ -208,9 +220,13 @@
val fp_eqs =
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
- val (pre_bnfs, ((dtors0, ctors0, rels0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
- ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
- fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+ (* TODO: clean up list *)
+ val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
+ dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss, fp_rel_thms,
+ fp_fold_thms, fp_rec_thms), lthy)) =
+ fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+
+ val timer = time (Timer.startRealTimer ());
fun add_nesty_bnf_names Us =
let
@@ -227,11 +243,23 @@
val nesting_bnfs = nesty_bnfs As;
val nested_bnfs = nesty_bnfs Xs;
- val timer = time (Timer.startRealTimer ());
+ val pre_map_defs = map map_def_of_bnf pre_bnfs;
+ val pre_set_defss = map set_defs_of_bnf pre_bnfs;
+ val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
+ val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
+ val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
+ val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
+
+ val live = live_of_bnf any_fp_bnf;
+
+ val Bs =
+ map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
+ (liveness_of_fp_bnf (length As) any_fp_bnf) As Bs0;
+
+ val B_ify = Term.typ_subst_atomic (As ~~ Bs);
val ctors = map (mk_ctor As) ctors0;
val dtors = map (mk_dtor As) dtors0;
- val rels = map (mk_rel As As) rels0; (*FIXME*)
val fpTs = map (domain_type o fastype_of) dtors;
@@ -243,11 +271,11 @@
val mss = map (map length) ctr_Tsss;
val Css = map2 replicate ns Cs;
- val fp_folds as fp_fold1 :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
- val fp_recs as fp_rec1 :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
+ val fp_folds as any_fp_fold :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
+ val fp_recs as any_fp_rec :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
- val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
- val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
+ val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_fold)));
+ val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_rec)));
val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
(zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
@@ -351,9 +379,10 @@
(mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
end;
- fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_fold), fp_rec),
- ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
- disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
+ fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
+ fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
+ pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings),
+ ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -367,14 +396,17 @@
|> yield_singleton (mk_Frees "w") dtorT
||>> mk_Frees "f" case_Ts
||>> mk_Freess "x" ctr_Tss
- ||>> mk_Freess "y" ctr_Tss
+ ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
||>> yield_singleton Variable.variant_fixes fp_b_name;
val u = Free (u', fpT);
+ val tuple_xs = map HOLogic.mk_tuple xss;
+ val tuple_ys = map HOLogic.mk_tuple yss;
+
val ctr_rhss =
- map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $
- mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
+ map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
+ mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
@@ -391,6 +423,8 @@
val phi = Proof_Context.export_morphism lthy lthy';
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
+ val ctr_defs' =
+ map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
val case_def = Morphism.thm phi raw_case_def;
val ctrs0 = map (Morphism.term phi) raw_ctrs;
@@ -398,45 +432,130 @@
val ctrs = map (mk_ctr As) ctrs0;
- fun exhaust_tac {context = ctxt, ...} =
+ fun wrap lthy =
let
- val ctor_iff_dtor_thm =
+ fun exhaust_tac {context = ctxt, ...} =
let
- val goal =
- fold_rev Logic.all [w, u]
- (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ val ctor_iff_dtor_thm =
+ let
+ val goal =
+ fold_rev Logic.all [w, u]
+ (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ in
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
+ (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
+ |> Thm.close_derivation
+ |> Morphism.thm phi
+ end;
+
+ val sumEN_thm' =
+ unfold_thms lthy @{thms all_unit_eq}
+ (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
+ (mk_sumEN_balanced n))
+ |> Morphism.thm phi;
in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
- (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
- |> Thm.close_derivation
- |> Morphism.thm phi
+ mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
end;
- val sumEN_thm' =
- unfold_thms lthy @{thms all_unit_eq}
- (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
- (mk_sumEN_balanced n))
- |> Morphism.thm phi;
+ val inject_tacss =
+ map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
+ mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+
+ val half_distinct_tacss =
+ map (map (fn (def, def') => fn {context = ctxt, ...} =>
+ mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs));
+
+ val case_tacs =
+ map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
+ mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
+
+ val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+
+ val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
in
- mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
+ wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
+ sel_defaultss))) lthy
end;
- val inject_tacss =
- map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
- mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+ fun derive_maps_sets_rels (wrap_res, lthy) =
+ let
+ val rel_flip = rel_flip_of_bnf fp_bnf;
+ val nones = replicate live NONE;
+
+ val ctor_cong =
+ if lfp then Drule.dummy_thm
+ else cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor)] arg_cong;
+
+ fun mk_cIn ify =
+ certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
+ mk_InN_balanced (ify ctr_sum_prod_T) n;
+
+ val cxIns = map2 (mk_cIn I) tuple_xs ks;
+ val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
+
+ fun thaw xs = Thm.generalize ([], map (fst o dest_Free) xs) 1 o Drule.zero_var_indexes;
- val half_distinct_tacss =
- map (map (fn (def, def') => fn {context = ctxt, ...} =>
- mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss ctr_defs);
+ fun mk_map_thm ctr_def' xs cxIn =
+ fold_thms lthy [ctr_def']
+ (unfold_thms lthy (pre_map_def ::
+ (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
+ (cterm_instantiate_pos (nones @ [SOME cxIn])
+ (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
+ |> thaw xs;
+
+ fun mk_set_thm fp_set_thm ctr_def' xs cxIn =
+ fold_thms lthy [ctr_def']
+ (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @
+ (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
+ (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
+ |> thaw xs;
+
+ fun mk_set_thms fp_set_thm = map3 (mk_set_thm fp_set_thm) ctr_defs' xss cxIns;
+
+ val map_thms = map3 mk_map_thm ctr_defs' xss cxIns;
+ val set_thmss = map mk_set_thms fp_set_thms;
- val case_tacs =
- map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
- mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
+ val rel_infos = (ctr_defs' ~~ xss ~~ cxIns, ctr_defs' ~~ yss ~~ cyIns);
+
+ fun mk_rel_thm finish_off ctr_defs' xs cxIn ys cyIn =
+ fold_thms lthy ctr_defs'
+ (unfold_thms lthy (pre_rel_def ::
+ (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+ (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
+ |> finish_off |> thaw (xs @ ys);
+
+ fun mk_pos_rel_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
+ mk_rel_thm (perhaps (try (fn th => th RS @{thm eq_sym_Unity_imp}))) [ctr_def']
+ xs cxIn ys cyIn;
+
+ val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
+
+ fun mk_half_neg_rel_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
+ mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
+ xs cxIn ys cyIn;
- val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+ fun mk_other_half_neg_rel_thm thm =
+ flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
+
+ val half_neg_rel_thmss = map (map mk_half_neg_rel_thm) (mk_half_pairss rel_infos);
+ val other_half_neg_rel_thmss = map (map mk_other_half_neg_rel_thm) half_neg_rel_thmss;
+ val (neg_rel_thms, _) = join_halves n half_neg_rel_thmss other_half_neg_rel_thmss;
+
+ val rel_thms = pos_rel_thms @ neg_rel_thms;
- fun define_fold_rec (wrap_res, no_defs_lthy) =
+ val notes =
+ [(mapsN, map_thms, code_simp_attrs),
+ (relsN, rel_thms, code_simp_attrs),
+ (setsN, flat set_thmss, code_simp_attrs)]
+ |> filter_out (null o #2)
+ |> map (fn (thmN, thms, attrs) =>
+ ((Binding.qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
+ in
+ (wrap_res, lthy |> Local_Theory.notes notes |> snd)
+ end;
+
+ fun define_fold_rec no_defs_lthy =
let
val fpT_to_C = fpT --> C;
@@ -468,10 +587,10 @@
val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
in
- ((wrap_res, ctrs, foldx, recx, xss, yss, ctr_defs, fold_def, rec_def), lthy)
+ ((foldx, recx, fold_def, rec_def), lthy)
end;
- fun define_unfold_corec (wrap_res, no_defs_lthy) =
+ fun define_unfold_corec no_defs_lthy =
let
val B_to_fpT = C --> fpT;
@@ -508,27 +627,20 @@
val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
in
- ((wrap_res, ctrs, unfold, corec, xss, yss, ctr_defs, unfold_def, corec_def), lthy)
- end;
-
- fun wrap lthy =
- let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
- wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
- sel_defaultss))) lthy
+ ((unfold, corec, unfold_def, corec_def), lthy)
end;
val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
+
+ fun massage_res ((wrap_res, rec_like_res), lthy) =
+ (((ctrs, xss, ctr_defs, wrap_res), rec_like_res), lthy);
in
- ((wrap, define_rec_likes), lthy')
+ (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy')
end;
- fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
- fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list9
-
- val pre_map_defs = map map_def_of_bnf pre_bnfs;
- val pre_set_defss = map set_defs_of_bnf pre_bnfs;
- val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
- val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
+ fun wrap_types_and_more (wrap_types_and_mores, lthy) =
+ fold_map I wrap_types_and_mores lthy
+ |>> apsnd split_list4 o apfst split_list4 o split_list;
fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
let
@@ -539,12 +651,13 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
+ (* TODO: Add map, sets, rel simps *)
val mk_simp_thmss =
map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
injects @ distincts @ cases @ rec_likes @ fold_likes);
- fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, _, ctr_defss,
- fold_defs, rec_defs), lthy) =
+ fun derive_induct_fold_rec_thms_for_types (((ctrss, xsss, ctr_defss, wrap_ress), (folds, recs,
+ fold_defs, rec_defs)), lthy) =
let
val (((phis, phis'), us'), names_lthy) =
lthy
@@ -687,8 +800,6 @@
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
- (* TODO: Also note "recs", "simps", and "splits" if "nn > 1" (for compatibility with the
- old package)? And for codatatypes as well? *)
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
|> map (fn (thmN, thms, attrs) =>
@@ -697,9 +808,9 @@
val notes =
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
- (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
- (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
- (simpsN, simp_thmss, K [])] (* TODO: Add relator simps *)
+ (foldsN, fold_thmss, K (code_simp_attrs)),
+ (recsN, rec_thmss, K (code_simp_attrs)),
+ (simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
map3 (fn b => fn Type (T_name, _) => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
@@ -708,8 +819,8 @@
lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
- fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, _,
- ctr_defss, unfold_defs, corec_defs), lthy) =
+ fun derive_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress), (unfolds,
+ corecs, unfold_defs, corec_defs)), lthy) =
let
val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
val selsss = map #2 wrap_ress;
@@ -725,6 +836,9 @@
val (coinduct_thms, coinduct_thm) =
let
+(* val goal =
+ *)
+
val coinduct_thm = fp_induct;
in
`(conj_dests nn) coinduct_thm
@@ -874,13 +988,13 @@
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
(corecsN, corec_thmss, []),
- (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
+ (disc_corec_iffsN, disc_corec_iff_thmss, simp_attrs),
+ (disc_corecsN, disc_corec_thmss, simp_attrs),
+ (disc_unfold_iffsN, disc_unfold_iff_thmss, simp_attrs),
(disc_unfoldsN, disc_unfold_thmss, simp_attrs),
- (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
- (disc_corecsN, disc_corec_thmss, simp_attrs),
(sel_unfoldsN, sel_unfold_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
- (simpsN, simp_thmss, []), (* TODO: Add relator simps *)
+ (simpsN, simp_thmss, []),
(unfoldsN, unfold_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
map_filter (fn (_, []) => NONE | (b, thms) =>
@@ -890,86 +1004,15 @@
lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
end;
- fun derive_rel_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, xsss, ysss, ctr_defss,
- unfold_defs, corec_defs), lthy) =
- let
- val selsss = map #2 wrap_ress;
-
- val theta_Ts = [] (*###*)
-
- val (thetas, _) =
- lthy
- |> mk_Frees "Q" (map mk_pred1T theta_Ts);
-
- val (rel_thmss, rel_thmsss) =
- let
- val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
- val yctrss = map2 (map2 (curry Term.list_comb)) ctrss ysss;
- val threls = map (fold_rev rapp thetas) rels;
-
- fun mk_goal threl (xctr, xs) (yctr, ys) =
- let
- val lhs = threl $ xctr $ yctr;
-
- (* ### fixme: lift rel *)
- fun mk_conjunct x y = HOLogic.mk_eq (x, y);
-
- fun mk_rhs () =
- Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct xs ys);
- in
- HOLogic.mk_Trueprop
- (if Term.head_of xctr = Term.head_of yctr then
- if null xs then
- lhs
- else
- HOLogic.mk_eq (lhs, mk_rhs ())
- else
- HOLogic.mk_not lhs)
- end;
-
-(*###*)
- (* TODO: Prove and exploit symmetry of relators to halve the number of goals. *)
- fun mk_goals threl xctrs xss yctrs yss =
- map_product (mk_goal threl) (xctrs ~~ xss) (yctrs ~~ yss);
-
- val goalsss = map5 mk_goals threls xctrss xsss yctrss ysss;
-
-(*###
- val goalsss = map6 (fn threl =>
- map5 (fn xctr => fn xs => fn sels =>
- map2 (mk_goal threl xctr xs sels))) threls xctrss xsss selsss yctrss ysss;
-*)
-(* val _ = tracing ("goalsss: " ^ PolyML.makestring goalsss) (*###*) *)
- in
- ([], [])
- end;
-
- val (sel_rel_thmss, sel_rel_thmsss) =
- let
- in
- ([], [])
- end;
-
- val notes =
- [(* (relsN, rel_thmss, []),
- (sel_relsN, sel_rel_thmss, []) *)]
- |> maps (fn (thmN, thmss, attrs) =>
- map2 (fn b => fn thms =>
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
- [(thms, [])])) fp_bs thmss);
- in
- lthy |> Local_Theory.notes notes |> snd
- end;
-
val lthy' = lthy
- |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
- fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
- ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
- |>> split_list |> wrap_types_and_define_rec_likes
- |> `(if lfp then derive_induct_fold_rec_thms_for_types
- else derive_coinduct_unfold_corec_thms_for_types)
- |> swap |>> fst
- |> (if null rels then snd else derive_rel_thms_for_types);
+ |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
+ fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
+ pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~
+ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
+ raw_sel_defaultsss)
+ |> wrap_types_and_more
+ |> (if lfp then derive_induct_fold_rec_thms_for_types
+ else derive_coinduct_unfold_corec_thms_for_types);
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
(if lfp then "" else "co") ^ "datatype"));
@@ -995,6 +1038,6 @@
val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
-fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct;
+fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
end;