# HG changeset patch # User blanchet # Date 1427741954 -7200 # Node ID ed0ca9029021f33862020bebc1c2190a5a3e75d6 # Parent ffd50fdfc7fa50f0cbf905715a0c4c24d88bf66f export more low-level theorems in data structure (partly for 'corec') diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 30 20:59:14 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)); diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 30 20:59:14 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) diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 30 20:59:14 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)) ^ diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 30 20:59:14 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; diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 30 20:59:14 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; diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Mar 30 20:59:14 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 = diff -r ffd50fdfc7fa -r ed0ca9029021 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 30 18:33:22 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 30 20:59:14 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