--- a/src/HOL/Basic_BNF_LFPs.thy Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Basic_BNF_LFPs.thy Tue Apr 05 09:54:17 2016 +0200
@@ -15,6 +15,9 @@
lemma xtor_map: "f (xtor x) = xtor (f x)"
unfolding xtor_def by (rule refl)
+lemma xtor_map_unique: "u \<circ> xtor = xtor \<circ> f \<Longrightarrow> u = f"
+ unfolding o_def xtor_def .
+
lemma xtor_set: "f (xtor x) = f x"
unfolding xtor_def by (rule refl)
@@ -50,6 +53,9 @@
lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
+lemma ctor_rec_unique: "g = id \<Longrightarrow> f \<circ> xtor = s \<circ> (id_bnf \<circ> g \<circ> id_bnf) \<Longrightarrow> f = ctor_rec s"
+ unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
+
lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Apr 05 09:54:17 2016 +0200
@@ -524,12 +524,14 @@
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_map_uniques = [],
+ xtor_maps = of_fp_res #xtor_maps (*too general types and terms*),
+ xtor_map_unique = TrueI (*wrong*),
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_legacy = xtor_co_rec_thms (*wrong*),
xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*),
- xtor_un_fold_uniques_legacy = [], xtor_co_rec_uniques = [],
+ xtor_un_fold_unique_legacy = TrueI (*too general types and terms*),
+ xtor_co_rec_unique = TrueI (*wrong*),
xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*),
xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*),
xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [],
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Apr 05 09:54:17 2016 +0200
@@ -25,13 +25,13 @@
ctor_injects: thm list,
dtor_injects: thm list,
xtor_maps: thm list,
- xtor_map_uniques: thm list,
+ xtor_map_unique: thm,
xtor_setss: thm list list,
xtor_rels: thm list,
xtor_un_fold_thms_legacy: thm list,
xtor_co_rec_thms: thm list,
- xtor_un_fold_uniques_legacy: thm list,
- xtor_co_rec_uniques: thm list,
+ xtor_un_fold_unique_legacy: thm,
+ xtor_co_rec_unique: thm,
xtor_un_fold_o_maps_legacy: thm list,
xtor_co_rec_o_maps: thm list,
xtor_un_fold_transfers_legacy: thm list,
@@ -229,13 +229,13 @@
ctor_injects: thm list,
dtor_injects: thm list,
xtor_maps: thm list,
- xtor_map_uniques: thm list,
+ xtor_map_unique: thm,
xtor_setss: thm list list,
xtor_rels: thm list,
xtor_un_fold_thms_legacy: thm list,
xtor_co_rec_thms: thm list,
- xtor_un_fold_uniques_legacy: thm list,
- xtor_co_rec_uniques: thm list,
+ xtor_un_fold_unique_legacy: thm,
+ xtor_co_rec_unique: thm,
xtor_un_fold_o_maps_legacy: thm list,
xtor_co_rec_o_maps: thm list,
xtor_un_fold_transfers_legacy: thm list,
@@ -245,8 +245,8 @@
fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds_legacy,
xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps,
- xtor_map_uniques, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms,
- xtor_un_fold_uniques_legacy, xtor_co_rec_uniques, xtor_un_fold_o_maps_legacy,
+ xtor_map_unique, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms,
+ xtor_un_fold_unique_legacy, xtor_co_rec_unique, xtor_un_fold_o_maps_legacy,
xtor_co_rec_o_maps, xtor_un_fold_transfers_legacy, xtor_co_rec_transfers, xtor_rel_co_induct,
dtor_set_inducts} =
{Ts = map (Morphism.typ phi) Ts,
@@ -263,13 +263,13 @@
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_map_unique = Morphism.thm phi xtor_map_unique,
xtor_setss = map (map (Morphism.thm phi)) xtor_setss,
xtor_rels = map (Morphism.thm phi) xtor_rels,
xtor_un_fold_thms_legacy = map (Morphism.thm phi) xtor_un_fold_thms_legacy,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
- xtor_un_fold_uniques_legacy = map (Morphism.thm phi) xtor_un_fold_uniques_legacy,
- xtor_co_rec_uniques = map (Morphism.thm phi) xtor_co_rec_uniques,
+ xtor_un_fold_unique_legacy = Morphism.thm phi xtor_un_fold_unique_legacy,
+ xtor_co_rec_unique = Morphism.thm phi xtor_co_rec_unique,
xtor_un_fold_o_maps_legacy = map (Morphism.thm phi) xtor_un_fold_o_maps_legacy,
xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps,
xtor_un_fold_transfers_legacy = map (Morphism.thm phi) xtor_un_fold_transfers_legacy,
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Apr 05 09:54:17 2016 +0200
@@ -1745,6 +1745,32 @@
fun mk_dtor_map_DEADID_thm dtor_inject map_id0 =
trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym];
+ fun mk_dtor_map_unique_DEADID_thm () =
+ let
+ val (funs, algs) =
+ HOLogic.conjuncts (HOLogic.dest_Trueprop (Thm.concl_of dtor_unfold_unique_thm))
+ |> map_split HOLogic.dest_eq
+ ||> snd o strip_comb o hd
+ |> @{apply 2} (map (fst o dest_Var));
+ fun mk_fun_insts T ix = Thm.cterm_of lthy (Var (ix, T --> T));
+ val theta =
+ (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) dtors);
+ val dtor_unfold_dtors = (dtor_unfold_unique_thm OF
+ map (fn thm => mk_trans (thm RS @{thm arg_cong2[of _ _ _ _ "op o", OF _ refl]})
+ @{thm trans[OF id_o o_id[symmetric]]}) map_id0s)
+ |> split_conj_thm |> map mk_sym;
+ in
+ infer_instantiate lthy theta dtor_unfold_unique_thm
+ |> Morphism.thm (Local_Theory.target_morphism lthy)
+ |> unfold_thms lthy dtor_unfold_dtors
+ |> (fn thm => thm OF replicate n sym)
+ end;
+(*
+thm trans[OF x.dtor_unfold_unique x.dtor_unfold_unique[symmetric,
+ OF trans[OF arg_cong2[of _ _ _ _ "op o", OF pre_x.map_id0 refl] trans[OF id_o o_id[symmetric]]]],
+ OF sym]
+*)
+
fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf =
trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
@@ -1773,12 +1799,14 @@
REPEAT_DETERM (rtac ctxt allI 1) THEN rtac ctxt (dtor_coinduct_thm OF prems) 1)) lthy;
(*register new codatatypes as BNFs*)
- val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jmap_unique_thms, dtor_Jset_thmss',
+ val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jmap_unique_thm, 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), [],
- replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
+ map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
+ mk_dtor_map_unique_DEADID_thm (),
+ replicate n [],
+ map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
mk_Jrel_DEADID_coinduct_thm (), [], [], lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -2620,7 +2648,7 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jmap_unique_thms, dtor_Jset_thmss',
+ (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jmap_unique_thm, dtor_Jset_thmss',
dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, dtor_Jset_induct_thms,
lthy)
end;
@@ -2696,10 +2724,10 @@
ctors = ctors, dtors = dtors, xtor_un_folds_legacy = 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_map_uniques = dtor_Jmap_unique_thms, xtor_setss = dtor_Jset_thmss',
+ xtor_map_unique = dtor_Jmap_unique_thm, xtor_setss = dtor_Jset_thmss',
xtor_rels = dtor_Jrel_thms, xtor_un_fold_thms_legacy = dtor_unfold_thms,
- xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_uniques_legacy = dtor_unfold_unique_thms,
- xtor_co_rec_uniques = dtor_corec_unique_thms,
+ xtor_co_rec_thms = dtor_corec_thms, xtor_un_fold_unique_legacy = dtor_unfold_unique_thm,
+ xtor_co_rec_unique = dtor_corec_unique_thm,
xtor_un_fold_o_maps_legacy = dtor_unfold_o_Jmap_thms,
xtor_co_rec_o_maps = dtor_corec_o_Jmap_thms,
xtor_un_fold_transfers_legacy = dtor_unfold_transfer_thms,
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML Tue Apr 05 09:54:17 2016 +0200
@@ -2160,7 +2160,7 @@
val [dtor_ctor] = #dtor_ctors fp_res;
val [dtor_inject] = #dtor_injects fp_res;
val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;
- val [dtor_unfold_unique] = #xtor_un_fold_uniques_legacy fp_res;
+ val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res;
val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res;
val [dtor_rel_thm] = #xtor_rels fp_res;
val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
@@ -2410,7 +2410,7 @@
val [ctor_dtor] = #ctor_dtors fp_res;
val [dtor_inject] = #dtor_injects fp_res;
val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;
- val [dtor_unfold_unique] = #xtor_un_fold_uniques_legacy fp_res;
+ val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res;
val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res;
val fp_k_T_rel_eqs =
map rel_eq_of_bnf (map_filter (bnf_of lthy) (fold add_type_namesT [fpT, k_T] []));
@@ -2762,7 +2762,7 @@
val [ctor_dtor] = #ctor_dtors fp_res;
val [dtor_inject] = #dtor_injects fp_res;
val [dtor_unfold_thm] = #xtor_un_fold_thms_legacy fp_res;
- val [dtor_unfold_unique] = #xtor_un_fold_uniques_legacy fp_res;
+ val dtor_unfold_unique = #xtor_un_fold_unique_legacy fp_res;
val [dtor_unfold_transfer] = #xtor_un_fold_transfers_legacy fp_res;
val unsig_thm = the_single (the_single (#sel_thmss sig_ctr_sugar));
val [sig_map_thm] = #map_thms sig_fp_bnf_sugar;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Apr 05 09:54:17 2016 +0200
@@ -1384,6 +1384,26 @@
fun mk_ctor_map_DEADID_thm ctor_inject map_id0 =
trans OF [id_apply, iffD2 OF [ctor_inject, map_id0 RS sym]];
+ fun mk_ctor_map_unique_DEADID_thm () =
+ let
+ val (funs, algs) =
+ HOLogic.conjuncts (HOLogic.dest_Trueprop (Thm.concl_of ctor_fold_unique_thm))
+ |> map_split HOLogic.dest_eq
+ ||> snd o strip_comb o hd
+ |> @{apply 2} (map (fst o dest_Var));
+ fun mk_fun_insts T ix = Thm.cterm_of lthy (Var (ix, T --> T));
+ val theta =
+ (funs ~~ @{map 2} mk_fun_insts Ts funs) @ (algs ~~ map (Thm.cterm_of lthy) ctors);
+ val ctor_fold_ctors = (ctor_fold_unique_thm OF
+ map (fn thm => mk_trans @{thm id_o} (mk_sym (thm RS
+ @{thm trans[OF arg_cong2[of _ _ _ _ "op o", OF refl] o_id]}))) map_id0s)
+ |> split_conj_thm |> map mk_sym;
+ in
+ infer_instantiate lthy theta ctor_fold_unique_thm
+ |> unfold_thms lthy ctor_fold_ctors
+ |> Morphism.thm (Local_Theory.target_morphism lthy)
+ end;
+
fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
@@ -1396,11 +1416,12 @@
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_Imap_unique_thms, ctor_Iset_thmss',
+ val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thm, 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),
+ mk_ctor_map_unique_DEADID_thm (),
replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -1874,7 +1895,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_Imap_unique_thms, ctor_Iset_thmss',
+ (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Imap_unique_thm, ctor_Iset_thmss',
ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy)
end;
@@ -1956,10 +1977,10 @@
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_map_uniques = ctor_Imap_unique_thms, xtor_setss = ctor_Iset_thmss',
+ xtor_map_unique = ctor_Imap_unique_thm, xtor_setss = ctor_Iset_thmss',
xtor_rels = ctor_Irel_thms, xtor_un_fold_thms_legacy = ctor_fold_thms,
- xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_uniques_legacy = ctor_fold_unique_thms,
- xtor_co_rec_uniques = ctor_rec_unique_thms,
+ xtor_co_rec_thms = ctor_rec_thms, xtor_un_fold_unique_legacy = ctor_fold_unique_thm,
+ xtor_co_rec_unique = ctor_rec_unique_thm,
xtor_un_fold_o_maps_legacy = ctor_fold_o_Imap_thms,
xtor_co_rec_o_maps = ctor_rec_o_Imap_thms,
xtor_un_fold_transfers_legacy = ctor_fold_transfer_thms,
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Apr 05 09:54:17 2016 +0200
@@ -33,14 +33,16 @@
val xtors = [Const (@{const_name xtor}, fpT --> fpT)];
val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))];
val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}];
+ val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique};
in
{Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT],
ctors = xtors, dtors = xtors, xtor_un_folds_legacy = 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_map_uniques = [],
- xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], xtor_un_fold_thms_legacy = co_rec_thms,
- xtor_co_rec_thms = co_rec_thms, xtor_un_fold_uniques_legacy = [], xtor_co_rec_uniques = [],
+ dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map],
+ xtor_map_unique = @{thm xtor_map_unique}, xtor_setss = [xtor_sets], xtor_rels = [xtor_rel],
+ xtor_un_fold_thms_legacy = co_rec_thms, xtor_co_rec_thms = co_rec_thms,
+ xtor_un_fold_unique_legacy = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm,
xtor_un_fold_o_maps_legacy = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map],
xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [],
xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []}