# HG changeset patch # User blanchet # Date 1347418998 -7200 # Node ID 6190b701e4f49c4867b9d2cde0a5ba46927436bf # Parent 30916e44d8282d5be6febdea4776601432940f32 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/BNF_Comp.thy --- a/src/HOL/Codatatype/BNF_Comp.thy Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/BNF_Comp.thy Wed Sep 12 05:03:18 2012 +0200 @@ -12,7 +12,6 @@ uses "Tools/bnf_comp_tactics.ML" "Tools/bnf_comp.ML" - "Tools/bnf_fp_util.ML" begin end diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/BNF_FP.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Codatatype/BNF_FP.thy Wed Sep 12 05:03:18 2012 +0200 @@ -0,0 +1,21 @@ +(* Title: HOL/Codatatype/BNF_FP.thy + Author: Dmitriy Traytel, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Composition of bounded natural functors. +*) + +header {* Composition of Bounded Natural Functors *} + +theory BNF_FP +imports BNF_Comp BNF_Wrap +keywords + "defaults" +uses + "Tools/bnf_fp_util.ML" + "Tools/bnf_fp_sugar_tactics.ML" + "Tools/bnf_fp_sugar.ML" +begin + +end diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/BNF_GFP.thy --- a/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/BNF_GFP.thy Wed Sep 12 05:03:18 2012 +0200 @@ -8,9 +8,10 @@ header {* Greatest Fixed Point Operation on Bounded Natural Functors *} theory BNF_GFP -imports BNF_Comp +imports BNF_FP keywords - "codata_raw" :: thy_decl + "codata_raw" :: thy_decl and + "codata" :: thy_decl uses "Tools/bnf_gfp_util.ML" "Tools/bnf_gfp_tactics.ML" diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/BNF_LFP.thy --- a/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/BNF_LFP.thy Wed Sep 12 05:03:18 2012 +0200 @@ -8,9 +8,10 @@ header {* Least Fixed Point Operation on Bounded Natural Functors *} theory BNF_LFP -imports BNF_Comp +imports BNF_FP keywords - "data_raw" :: thy_decl + "data_raw" :: thy_decl and + "data" :: thy_decl uses "Tools/bnf_lfp_util.ML" "Tools/bnf_lfp_tactics.ML" diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/Codatatype.thy --- a/src/HOL/Codatatype/Codatatype.thy Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/Codatatype.thy Wed Sep 12 05:03:18 2012 +0200 @@ -10,14 +10,7 @@ header {* The (Co)datatype Package *} theory Codatatype -imports BNF_LFP BNF_GFP BNF_Wrap -keywords - "data" :: thy_decl and - "codata" :: thy_decl and - "defaults" -uses - "Tools/bnf_fp_sugar_tactics.ML" - "Tools/bnf_fp_sugar.ML" +imports BNF_LFP BNF_GFP begin end diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 05:03:18 2012 +0200 @@ -8,9 +8,19 @@ signature BNF_FP_SUGAR = sig val datatyp: 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 * thm list * thm 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 * thm list * thm list * thm list * thm list * + thm list) * local_theory) -> + (local_theory -> local_theory) parser end; structure BNF_FP_Sugar : BNF_FP_SUGAR = @@ -20,8 +30,6 @@ open BNF_Wrap open BNF_Def open BNF_FP_Util -open BNF_LFP -open BNF_GFP open BNF_FP_Sugar_Tactics val caseN = "case"; @@ -79,7 +87,6 @@ if length As = length As' then map2 merge_type_arg As As' else cannot_merge_types (); fun type_args_constrained_of (((cAs, _), _), _) = cAs; -val type_args_of = map fst o type_args_constrained_of; fun type_binder_of (((_, b), _), _) = b; fun mixfix_of ((_, mx), _) = mx; fun ctr_specs_of (_, ctr_specs) = ctr_specs; @@ -90,7 +97,7 @@ fun defaults_of ((_, ds), _) = ds; fun ctr_mixfix_of (_, mx) = mx; -fun define_datatype prepare_constraint prepare_typ prepare_term lfp (no_dests, specs) +fun define_datatype prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs) no_defs_lthy0 = let (* TODO: sanity checks on arguments *) @@ -148,7 +155,7 @@ val fake_ctr_Tsss0 = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss; val raw_sel_defaultsss = map (map defaults_of) ctr_specss; - val (Ass as As :: _) :: fake_ctr_Tsss = + val (As :: _) :: fake_ctr_Tsss = burrow (burrow (Syntax.check_typs fake_lthy)) (Ass0 :: fake_ctr_Tsss0); val _ = (case duplicates (op =) unsorted_As of [] => () @@ -178,8 +185,7 @@ val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects, fp_iter_thms, fp_rec_thms), lthy)) = - fp_bnf (if lfp then bnf_lfp else bnf_gfp) fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs - no_defs_lthy0; + fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; val add_nested_bnf_names = let @@ -694,7 +700,7 @@ val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ (if lfp then "" else "co") ^ "datatype")); in - (timer; lthy') + timer; lthy' end; val datatyp = define_datatype (K I) (K I) (K I); @@ -717,12 +723,6 @@ val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec; -val _ = - Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes" - (parse_datatype >> datatype_cmd true); - -val _ = - Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes" - (parse_datatype >> datatype_cmd false); +fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct; end; diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Wed Sep 12 05:03:18 2012 +0200 @@ -352,7 +352,7 @@ val timer = time (timer "FP construction in total"); in - (bnfs'', res) + timer; (bnfs'', res) end; fun fp_bnf construct bs mixfixes resBs eqs lthy = diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Wed Sep 12 05:03:18 2012 +0200 @@ -22,6 +22,7 @@ open BNF_Util open BNF_Tactics open BNF_FP_Util +open BNF_FP_Sugar open BNF_GFP_Util open BNF_GFP_Tactics @@ -49,7 +50,7 @@ (I, nth flds i $ (Term.list_comb (snd (nth (nth witss i) nwit), map (snd o tree_to_fld_wit vars flds witss) subtrees))); -fun tree_to_coind_wits _ (Leaf j) = [] +fun tree_to_coind_wits _ (Leaf _) = [] | tree_to_coind_wits lwitss (Node ((i, nwit, I), subtrees)) = ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees; @@ -147,7 +148,6 @@ val bds = map3 mk_bd_of_bnf Dss Ass bnfs; val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); - val witss = map wits_of_bnf bnfs; val emptys = map (fn T => HOLogic.mk_set T []) passiveAs; val Zeros = map (fn empty => @@ -272,7 +272,6 @@ val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's; val in_mono'_thms = map (fn thm => (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos; - val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs; val map_arg_cong_thms = let @@ -1860,7 +1859,6 @@ val prodTs = map (HOLogic.mk_prodT o `I) Ts; val prodFTs = mk_FTs (passiveAs @ prodTs); val FTs_setss = mk_setss (passiveAs @ Ts); - val FTs'_setss = mk_setss (passiveBs @ Ts); val prodFT_setss = mk_setss (passiveAs @ prodTs); val map_FTs = map2 (fn Ds => mk_map_of_bnf Ds treeQTs (passiveAs @ Ts)) Dss bnfs; val map_FT_nths = map2 (fn Ds => @@ -2318,13 +2316,13 @@ val XTs = mk_Ts passiveXs; val YTs = mk_Ts passiveYs; - val (((((((((((((((((((((fs, fs'), (fs_copy, fs'_copy)), (gs, gs')), us), + val ((((((((((((((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), set_induct_phiss), JRs), Jphis), - B1s), B2s), AXs), Xs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)), + B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)), names_lthy) = names_lthy |> mk_Frees' "f" fTs - ||>> mk_Frees' "f" fTs - ||>> mk_Frees' "g" gTs + ||>> mk_Frees "f" fTs + ||>> mk_Frees "g" gTs ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' @@ -2334,7 +2332,6 @@ ||>> mk_Frees "B1" B1Ts ||>> mk_Frees "B2" B2Ts ||>> mk_Frees "A" AXTs - ||>> mk_Frees "x" XTs ||>> mk_Frees "f1" f1Ts ||>> mk_Frees "f2" f2Ts ||>> mk_Frees "p1" p1Ts @@ -2414,7 +2411,7 @@ |> Thm.close_derivation) end; - val (map_unique_thms, map_unique_thm) = + val map_unique_thm = let fun mk_prem u map unf unf' = mk_Trueprop_eq (HOLogic.mk_comp (unf', u), @@ -2423,12 +2420,11 @@ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) us fs_maps)); - val unique = Skip_Proof.prove lthy [] [] + in + Skip_Proof.prove lthy [] [] (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal))) (mk_map_unique_tac coiter_unique_thm map_comps) - |> Thm.close_derivation; - in - `split_conj_thm unique + |> Thm.close_derivation end; val timer = time (timer "map functions for the new codatatypes"); @@ -2437,11 +2433,6 @@ val timer = time (timer "bounds for the new codatatypes"); - fun mk_set_Ts T = passiveAs @ replicate n (HOLogic.mk_setT T); - val setsss = map (mk_setss o mk_set_Ts) passiveAs; - val map_setss = map (fn T => map2 (fn Ds => - mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs; - val setss_by_bnf = map (fn i => map2 (mk_hset unfs i) ls passiveAs) ks; val setss_by_bnf' = map (fn i => map2 (mk_hset unf's i) ls passiveBs) ks; val setss_by_range = transpose setss_by_bnf; @@ -2778,11 +2769,11 @@ end; val nat_witss = - map3 (fn i => fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) + map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf |> map (fn (I, wit) => (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I)))))) - ks Dss bnfs; + Dss bnfs; val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs) @@ -2969,7 +2960,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd + timer; lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd end; val common_notes = @@ -3006,9 +2997,14 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points of BNF equations" + Outer_Syntax.local_theory @{command_spec "codata_raw"} + "define BNF-based coinductive datatypes (low-level)" (Parse.and_list1 ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >> (snd oo fp_bnf_cmd bnf_gfp o apsnd split_list o split_list)); +val _ = + Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes" + (parse_datatype_cmd false bnf_gfp); + end; diff -r 30916e44d828 -r 6190b701e4f4 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 02:06:31 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Wed Sep 12 05:03:18 2012 +0200 @@ -21,6 +21,7 @@ open BNF_Util open BNF_Tactics open BNF_FP_Util +open BNF_FP_Sugar open BNF_LFP_Util open BNF_LFP_Tactics @@ -1118,8 +1119,8 @@ `split_conj_thm unique_mor end; - val (iter_unique_thms, iter_unique_thm) = - `split_conj_thm (mk_conjIN n RS + val iter_unique_thms = + split_conj_thm (mk_conjIN n RS (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm)) val iter_fld_thms = @@ -1791,7 +1792,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd + timer; lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd end; val common_notes = @@ -1821,9 +1822,14 @@ end; val _ = - Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations" + Outer_Syntax.local_theory @{command_spec "data_raw"} + "define BNF-based inductive datatypes (low-level)" (Parse.and_list1 ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >> (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list)); +val _ = + Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes" + (parse_datatype_cmd true bnf_lfp); + end;