--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Mar 31 00:21:07 2015 +0200
@@ -290,8 +290,7 @@
val dtor_corec_transfer' = cterm_instantiate_pos
(SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
in
- HEADGOAL Goal.conjunction_tac THEN
- REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+ HEADGOAL Goal.conjunction_tac THEN REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
unfold_thms_tac ctxt [corec_def] THEN
HEADGOAL (etac (mk_rel_funDN_rotated (1 + length actives) dtor_corec_transfer')) THEN
unfold_thms_tac ctxt (rel_pre_T_defs @ rel_eqs)
@@ -492,8 +491,7 @@
SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o atac)))));
fun mk_set_intros_tac ctxt sets =
- TRYALL Goal.conjunction_tac THEN
- unfold_thms_tac ctxt sets THEN
+ TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN
TRYALL (REPEAT o
(resolve_tac ctxt @{thms UnI1 UnI2} ORELSE'
eresolve_tac ctxt @{thms UN_I UN_I[rotated]}) THEN' (rtac @{thm singletonI} ORELSE' atac));
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Mar 31 00:21:07 2015 +0200
@@ -484,12 +484,16 @@
ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
ctor_injects = of_fp_res #ctor_injects (*too general types*),
dtor_injects = of_fp_res #dtor_injects (*too general types*),
- xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
+ xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), xtor_map_uniques = [],
xtor_setss = of_fp_res #xtor_setss (*too general types and terms*),
xtor_rels = of_fp_res #xtor_rels (*too general types and terms*),
- xtor_un_fold_thms = xtor_co_rec_thms (*wrong*), xtor_co_rec_thms = xtor_co_rec_thms,
+ xtor_un_fold_thms = xtor_co_rec_thms (*wrong*),
+ xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*),
+ xtor_un_fold_uniques = [], xtor_co_rec_uniques = [],
+ xtor_un_fold_o_maps = fp_rec_o_maps (*wrong*),
xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
- xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = [], xtor_co_rec_transfers = []}
+ xtor_un_fold_transfers = [], xtor_co_rec_transfers = [],
+ xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
(fp_res, lthy)
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 31 00:21:07 2015 +0200
@@ -23,14 +23,19 @@
ctor_injects: thm list,
dtor_injects: thm list,
xtor_maps: thm list,
+ xtor_map_uniques: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
+ xtor_un_fold_uniques: thm list,
+ xtor_co_rec_uniques: thm list,
+ xtor_un_fold_o_maps: thm list,
xtor_co_rec_o_maps: thm list,
+ xtor_un_fold_transfers: thm list,
+ xtor_co_rec_transfers: thm list,
xtor_rel_co_induct: thm,
- dtor_set_inducts: thm list,
- xtor_co_rec_transfers: thm list}
+ dtor_set_inducts: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -207,7 +212,7 @@
type fp_result =
{Ts: typ list,
- bnfs: BNF_Def.bnf list,
+ bnfs: bnf list,
ctors: term list,
dtors: term list,
xtor_un_folds: term list,
@@ -218,19 +223,25 @@
ctor_injects: thm list,
dtor_injects: thm list,
xtor_maps: thm list,
+ xtor_map_uniques: thm list,
xtor_setss: thm list list,
xtor_rels: thm list,
xtor_un_fold_thms: thm list,
xtor_co_rec_thms: thm list,
+ xtor_un_fold_uniques: thm list,
+ xtor_co_rec_uniques: thm list,
+ xtor_un_fold_o_maps: thm list,
xtor_co_rec_o_maps: thm list,
+ xtor_un_fold_transfers: thm list,
+ xtor_co_rec_transfers: thm list,
xtor_rel_co_induct: thm,
- dtor_set_inducts: thm list,
- xtor_co_rec_transfers: thm list};
+ dtor_set_inducts: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
- dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
- xtor_un_fold_thms, xtor_co_rec_thms, xtor_co_rec_o_maps, xtor_rel_co_induct, dtor_set_inducts,
- xtor_co_rec_transfers} =
+ dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_map_uniques, xtor_setss,
+ xtor_rels, xtor_un_fold_thms, xtor_co_rec_thms, xtor_un_fold_uniques, xtor_co_rec_uniques,
+ xtor_un_fold_o_maps, xtor_co_rec_o_maps, xtor_un_fold_transfers, xtor_co_rec_transfers,
+ xtor_rel_co_induct, dtor_set_inducts} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -243,14 +254,19 @@
ctor_injects = map (Morphism.thm phi) ctor_injects,
dtor_injects = map (Morphism.thm phi) dtor_injects,
xtor_maps = map (Morphism.thm phi) xtor_maps,
+ xtor_map_uniques = map (Morphism.thm phi) xtor_map_uniques,
xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
xtor_rels = map (Morphism.thm phi) xtor_rels,
xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
+ xtor_un_fold_uniques = map (Morphism.thm phi) xtor_un_fold_uniques,
+ xtor_co_rec_uniques = map (Morphism.thm phi) xtor_co_rec_uniques,
+ xtor_un_fold_o_maps = map (Morphism.thm phi) xtor_un_fold_o_maps,
xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
+ xtor_un_fold_transfers = map (Morphism.thm phi) xtor_un_fold_transfers,
+ xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers,
xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct,
- dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts,
- xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers};
+ dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts};
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 31 00:21:07 2015 +0200
@@ -1667,11 +1667,11 @@
REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
(*register new codatatypes as BNFs*)
- val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss',
+ val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jmap_unique_thms, dtor_Jset_thmss',
dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
- map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
+ map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids), [],
replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
mk_Jrel_DEADID_coinduct_thm (), [], [], lthy)
else let
@@ -1808,7 +1808,7 @@
map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
end;
- val dtor_Jmap_unique_thm =
+ val (dtor_Jmap_unique_thms, dtor_Jmap_unique_thm) =
let
fun mk_prem u map dtor dtor' =
mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
@@ -1818,11 +1818,11 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) us fs_Jmaps));
in
- Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+ `split_conj_thm (Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
(fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
|> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy lthy)
+ |> singleton (Proof_Context.export names_lthy lthy))
end;
val Jmap_comp0_thms =
@@ -2455,13 +2455,13 @@
val ls' = if m = 1 then [0] else ls;
val Jbnf_common_notes =
- [(dtor_map_uniqueN, [dtor_Jmap_unique_thm])] @
map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_Jset_induct_thms
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val Jbnf_notes =
[(dtor_mapN, map single dtor_Jmap_thms),
+ (dtor_map_uniqueN, map single dtor_Jmap_unique_thms),
(dtor_relN, map single dtor_Jrel_thms),
(dtor_set_inclN, dtor_Jset_incl_thmss),
(dtor_set_set_inclN, map flat dtor_set_Jset_incl_thmsss)] @
@@ -2471,7 +2471,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss',
+ (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jmap_unique_thms, dtor_Jset_thmss',
dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, dtor_Jset_induct_thms,
lthy)
end;
@@ -2510,8 +2510,7 @@
val common_notes =
[(dtor_coinductN, [dtor_coinduct_thm]),
- (dtor_rel_coinductN, [Jrel_coinduct_thm]),
- (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
+ (dtor_rel_coinductN, [Jrel_coinduct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
@@ -2520,15 +2519,16 @@
(ctor_exhaustN, ctor_exhaust_thms),
(ctor_injectN, ctor_inject_thms),
(dtor_corecN, dtor_corec_thms),
+ (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms),
(dtor_corec_transferN, dtor_corec_transfer_thms),
+ (dtor_corec_uniqueN, dtor_corec_unique_thms),
(dtor_ctorN, dtor_ctor_thms),
(dtor_exhaustN, dtor_exhaust_thms),
(dtor_injectN, dtor_inject_thms),
(dtor_unfoldN, dtor_unfold_thms),
- (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
- (dtor_corec_uniqueN, dtor_corec_unique_thms),
(dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms),
- (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)]
+ (dtor_unfold_transferN, dtor_unfold_transfer_thms),
+ (dtor_unfold_uniqueN, dtor_unfold_unique_thms)]
|> map (apsnd (map single))
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
@@ -2541,11 +2541,15 @@
{Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds,
xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
- dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms, xtor_setss = dtor_Jset_thmss',
+ dtor_injects = dtor_inject_thms, xtor_maps = dtor_Jmap_thms,
+ xtor_map_uniques = dtor_Jmap_unique_thms, xtor_setss = dtor_Jset_thmss',
xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms = dtor_unfold_thms,
- xtor_co_rec_thms = dtor_corec_thms, xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms,
- xtor_rel_co_induct = Jrel_coinduct_thm, dtor_set_inducts = dtor_Jset_induct_thms,
- xtor_co_rec_transfers = dtor_corec_transfer_thms};
+ xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_uniques = dtor_unfold_unique_thms,
+ xtor_co_rec_uniques = dtor_corec_unique_thms, xtor_un_fold_o_maps = dtor_unfold_o_Jmap_thms,
+ xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms,
+ xtor_un_fold_transfers = dtor_unfold_transfer_thms,
+ xtor_co_rec_transfers = dtor_corec_transfer_thms, xtor_rel_co_induct = Jrel_coinduct_thm,
+ dtor_set_inducts = dtor_Jset_induct_thms};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 31 00:21:07 2015 +0200
@@ -1309,11 +1309,11 @@
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
(*register new datatypes as BNFs*)
- val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Iset_thmss',
+ val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thms, ctor_Iset_thmss',
ctor_Irel_thms, Ibnf_notes, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
- map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
+ map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids), [],
replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -1757,7 +1757,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Iset_thmss',
+ (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thms, ctor_Iset_thmss',
ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy)
end;
@@ -1798,8 +1798,6 @@
val common_notes =
[(ctor_inductN, [ctor_induct_thm]),
(ctor_induct2N, [ctor_induct2_thm]),
- (ctor_fold_transferN, ctor_fold_transfer_thms),
- (ctor_rec_transferN, ctor_rec_transfer_thms),
(ctor_rel_inductN, [Irel_induct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
@@ -1808,10 +1806,12 @@
[(ctor_dtorN, ctor_dtor_thms),
(ctor_exhaustN, ctor_exhaust_thms),
(ctor_foldN, ctor_fold_thms),
+ (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
+ (ctor_fold_transferN, ctor_fold_transfer_thms),
(ctor_fold_uniqueN, ctor_fold_unique_thms),
+ (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
+ (ctor_rec_transferN, ctor_rec_transfer_thms),
(ctor_rec_uniqueN, ctor_rec_unique_thms),
- (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
- (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
(ctor_injectN, ctor_inject_thms),
(ctor_recN, ctor_rec_thms),
(dtor_ctorN, dtor_ctor_thms),
@@ -1829,11 +1829,14 @@
{Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds,
xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
- dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms, xtor_setss = ctor_Iset_thmss',
+ dtor_injects = dtor_inject_thms, xtor_maps = ctor_Imap_thms,
+ xtor_map_uniques = ctor_Imap_unique_thms, xtor_setss = ctor_Iset_thmss',
xtor_rels = ctor_Irel_thms, xtor_un_fold_thms = ctor_fold_thms,
- xtor_co_rec_thms = ctor_rec_thms, xtor_co_rec_o_maps = ctor_rec_o_Imap_thms,
- xtor_rel_co_induct = Irel_induct_thm, dtor_set_inducts = [],
- xtor_co_rec_transfers = ctor_rec_transfer_thms};
+ xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_uniques = ctor_fold_unique_thms,
+ xtor_co_rec_uniques = ctor_rec_unique_thms, xtor_un_fold_o_maps = ctor_fold_o_Imap_thms,
+ xtor_co_rec_o_maps = ctor_rec_o_Imap_thms, xtor_un_fold_transfers = ctor_fold_transfer_thms,
+ xtor_co_rec_transfers = ctor_rec_transfer_thms, xtor_rel_co_induct = Irel_induct_thm,
+ dtor_set_inducts = []};
in
timer; (fp_res, lthy')
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Mar 31 00:21:07 2015 +0200
@@ -37,10 +37,12 @@
{Ts = [fpT], bnfs = [fp_bnf], ctors = xtors, dtors = xtors, xtor_un_folds = co_recs,
xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor},
ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject},
- dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_setss = [xtor_sets],
- xtor_rels = [xtor_rel], xtor_un_fold_thms = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
- xtor_co_rec_o_maps = [ctor_rec_o_map], xtor_rel_co_induct = xtor_rel_induct,
- dtor_set_inducts = [], xtor_co_rec_transfers = []}
+ dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], xtor_map_uniques = [],
+ xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], xtor_un_fold_thms = co_rec_thms,
+ xtor_co_rec_thms = co_rec_thms, xtor_un_fold_uniques = [], xtor_co_rec_uniques = [],
+ xtor_un_fold_o_maps = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map],
+ xtor_un_fold_transfers = [], xtor_co_rec_transfers = [], xtor_rel_co_induct = xtor_rel_induct,
+ dtor_set_inducts = []}
end;
fun fp_sugar_of_sum ctxt =
--- a/src/HOL/Tools/BNF/bnf_util.ML Tue Mar 31 00:11:54 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Tue Mar 31 00:21:07 2015 +0200
@@ -313,7 +313,7 @@
end;
fun mk_leq t1 t2 =
- Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
+ Const (@{const_name less_eq}, fastype_of t1 --> fastype_of t2 --> HOLogic.boolT) $ t1 $ t2;
fun mk_card_binop binop typop t1 t2 =
let