# HG changeset patch # User traytel # Date 1459842857 -7200 # Node ID e0b894bba6ff6ffc7c4f4f61e0423f277b074cf3 # Parent 007c454d0d0fe0d0de1fdb34f375aad8ec5a2ceb single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Basic_BNF_LFPs.thy --- 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 \ xtor = xtor \ f \ 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 \ ctor_rec f (xtor x) = f ((id_bnf \ g \ 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 \ f \ xtor = s \ (id_bnf \ g \ id_bnf) \ 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 \ id_bnf)" unfolding ctor_rec_def id_bnf_def comp_def by (rule refl) diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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 = [], diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Tools/BNF/bnf_fp_util.ML --- 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, diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Tools/BNF/bnf_gfp.ML --- 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, diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Tools/BNF/bnf_gfp_grec.ML --- 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; diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Tools/BNF/bnf_lfp.ML --- 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, diff -r 007c454d0d0f -r e0b894bba6ff src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- 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 = []}