# HG changeset patch # User wenzelm # Date 1323896072 -3600 # Node ID 71b8d0d170b1baf671448cc1e7b060260b3e0f79 # Parent 2dad374cf4407fe823a7c41dc3c155dc6a9a5a11 avoid fragile Sign.intern_const -- pass internal names directly; tuned; diff -r 2dad374cf440 -r 71b8d0d170b1 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Dec 14 20:36:17 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Dec 14 21:54:32 2011 +0100 @@ -2045,7 +2045,7 @@ resolve_tac rec_intrs 1, REPEAT (solve (prems @ rec_total_thms) prems 1)]) end) (rec_eq_prems ~~ - Datatype_Prop.make_primrecs new_type_names descr' thy12); + Datatype_Prop.make_primrecs reccomb_names descr' thy12); val dt_infos = map_index (make_dt_info pdescr induct reccomb_names rec_thms) (descr1 ~~ distinct_thms ~~ inject_thms); diff -r 2dad374cf440 -r 71b8d0d170b1 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Dec 14 20:36:17 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Dec 14 21:54:32 2011 +0100 @@ -199,10 +199,9 @@ (*********************** definition of constructors ***********************) val big_rep_name = big_name ^ "_Rep_"; - val rep_names = map (prefix "Rep_") new_type_names; val rep_names' = map (fn i => big_rep_name ^ string_of_int i) (1 upto length (flat (tl descr))); val all_rep_names = - map (Sign.intern_const thy3) rep_names @ + map (#Rep_name o #1 o #2) typedefs @ map (Sign.full_bname thy3) rep_names'; (* isomorphism declarations *) @@ -212,7 +211,8 @@ (* constructor definitions *) - fun make_constr_def tname T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) = + fun make_constr_def tname (typedef: Typedef.info) T n + ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) = let fun constr_arg dt (j, l_args, r_args) = let @@ -224,19 +224,18 @@ (j + 1, free_t :: l_args, mk_lim (Const (nth all_rep_names m, U --> Univ_elT) $ Datatype_Aux.app_bnds free_t (length Us)) Us :: r_args) - | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) + | _ => (j + 1, free_t :: l_args, (Leaf $ mk_inj T free_t) :: r_args)) end; val (_, l_args, r_args) = fold_rev constr_arg cargs (1, [], []); val constrT = map (Datatype_Aux.typ_of_dtyp descr') cargs ---> T; - val abs_name = Sign.intern_const thy ("Abs_" ^ tname); - val rep_name = Sign.intern_const thy ("Rep_" ^ tname); + val ({Abs_name, Rep_name, ...}, _) = typedef; val lhs = list_comb (Const (cname, constrT), l_args); val rhs = mk_univ_inj r_args n i; - val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs); + val def = Logic.mk_equals (lhs, Const (Abs_name, Univ_elT --> T) $ rhs); val def_name = Long_Name.base_name cname ^ "_def"; val eqn = - HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs)); + HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (Rep_name, T --> Univ_elT) $ lhs, rhs)); val ([def_thm], thy') = thy |> Sign.add_consts_i [(cname', constrT, mx)] @@ -246,12 +245,11 @@ (* constructor definitions for datatype *) - fun dt_constr_defs ((((_, (_, _, constrs)), tname), T), constr_syntax) + fun dt_constr_defs (((((_, (_, _, constrs)), tname), typedef: Typedef.info), T), constr_syntax) (thy, defs, eqns, rep_congs, dist_lemmas) = let val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong; - val rep_const = - cterm_of thy (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> Univ_elT)); + val rep_const = cterm_of thy (Const (#Rep_name (#1 typedef), T --> Univ_elT)); val cong' = Drule.export_without_context (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong); @@ -259,7 +257,7 @@ Drule.export_without_context (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); val (thy', defs', eqns', _) = - fold ((make_constr_def tname T) (length constrs)) + fold (make_constr_def tname typedef T (length constrs)) (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1); in (Sign.parent_path thy', defs', eqns @ [eqns'], @@ -268,7 +266,7 @@ val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = fold dt_constr_defs - (hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax) + (hd descr ~~ new_type_names ~~ map #2 typedefs ~~ newTs ~~ constr_syntax) (thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []); @@ -276,12 +274,11 @@ val _ = Datatype_Aux.message config "Proving isomorphism properties ..."; - val newT_iso_axms = map (fn (_, (_, td)) => - (collect_simp (#Abs_inverse td), #Rep_inverse td, - collect_simp (#Rep td))) typedefs; + val newT_iso_axms = typedefs |> map (fn (_, (_, {Abs_inverse, Rep_inverse, Rep, ...})) => + (collect_simp Abs_inverse, Rep_inverse, collect_simp Rep)); - val newT_iso_inj_thms = map (fn (_, (_, td)) => - (collect_simp (#Abs_inject td) RS iffD1, #Rep_inject td RS iffD1)) typedefs; + val newT_iso_inj_thms = typedefs |> map (fn (_, (_, {Abs_inject, Rep_inject, ...})) => + (collect_simp Abs_inject RS iffD1, Rep_inject RS iffD1)); (********* isomorphisms between existing types and "unfolded" types *******) @@ -300,8 +297,7 @@ let val argTs = map (Datatype_Aux.typ_of_dtyp descr') cargs; val T = nth recTs k; - val rep_name = nth all_rep_names k; - val rep_const = Const (rep_name, T --> Univ_elT); + val rep_const = Const (nth all_rep_names k, T --> Univ_elT); val constr = Const (cname, argTs ---> T); fun process_arg ks' dt (i2, i2', ts, Ts) = @@ -409,14 +405,14 @@ val T = nth recTs i; val Rep_t = Const (nth all_rep_names i, T --> Univ_elT); val rep_set_name = nth rep_set_names i; - in - (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ + val concl1 = + HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ HOLogic.mk_eq (Rep_t $ Datatype_Aux.mk_Free "x" T i, Rep_t $ Bound 0) $ - HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)), - Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i)) - end; + HOLogic.mk_eq (Datatype_Aux.mk_Free "x" T i, Bound 0)); + val concl2 = Const (rep_set_name, UnivT') $ (Rep_t $ Datatype_Aux.mk_Free "x" T i); + in (concl1, concl2) end; - val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds); + val (ind_concl1, ind_concl2) = split_list (map mk_ind_concl ds); val rewrites = map mk_meta_eq iso_char_thms; val inj_thms' = map snd newT_iso_inj_thms @ map (fn r => r RS @{thm injD}) inj_thms; @@ -592,28 +588,26 @@ map (fn r => r RS @{thm the_inv_f_f} RS subst) iso_inj_thms_unfolded; val Rep_inverse_thms' = map (fn r => r RS @{thm the_inv_f_f}) iso_inj_thms_unfolded; - fun mk_indrule_lemma ((i, _), T) (prems, concls) = + fun mk_indrule_lemma (i, _) T = let - val Rep_t = - Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i; - + val Rep_t = Const (nth all_rep_names i, T --> Univ_elT) $ Datatype_Aux.mk_Free "x" T i; val Abs_t = if i < length newTs then - Const (Sign.intern_const thy6 ("Abs_" ^ nth new_type_names i), Univ_elT --> T) - else Const (@{const_name the_inv_into}, + Const (#Abs_name (#1 (#2 (nth typedefs i))), Univ_elT --> T) + else + Const (@{const_name the_inv_into}, [HOLogic.mk_setT T, T --> Univ_elT, Univ_elT] ---> T) $ HOLogic.mk_UNIV T $ Const (nth all_rep_names i, T --> Univ_elT); - in - (prems @ - [HOLogic.imp $ + val prem = + HOLogic.imp $ (Const (nth rep_set_names i, UnivT') $ Rep_t) $ - (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], - concls @ - [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i]) - end; + (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t)); + val concl = + Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i; + in (prem, concl) end; val (indrule_lemma_prems, indrule_lemma_concls) = - fold mk_indrule_lemma (descr' ~~ recTs) ([], []); + split_list (map2 mk_indrule_lemma descr' recTs); val cert = cterm_of thy6; diff -r 2dad374cf440 -r 71b8d0d170b1 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Dec 14 20:36:17 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Dec 14 21:54:32 2011 +0100 @@ -16,13 +16,13 @@ thm -> theory -> (string list * thm list) * theory val prove_case_thms : config -> string list -> descr list -> string list -> thm list -> theory -> (thm list list * string list) * theory - val prove_split_thms : config -> string list -> descr list -> + val prove_split_thms : config -> string list -> string list -> descr list -> thm list list -> thm list list -> thm list -> thm list list -> theory -> (thm * thm) list * theory val prove_nchotomys : config -> string list -> descr list -> thm list -> theory -> thm list * theory - val prove_weak_case_congs : string list -> descr list -> theory -> thm list * theory - val prove_case_congs : string list -> descr list -> + val prove_weak_case_congs : string list -> string list -> descr list -> theory -> thm list * theory + val prove_case_congs : string list -> string list -> descr list -> thm list -> thm list list -> theory -> thm list * theory end; @@ -262,7 +262,7 @@ resolve_tac rec_unique_thms 1, resolve_tac rec_intrs 1, REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)])) - (Datatype_Prop.make_primrecs new_type_names descr thy2); + (Datatype_Prop.make_primrecs reccomb_names descr thy2); in thy2 |> Sign.add_path (space_implode "_" new_type_names) @@ -338,7 +338,7 @@ Skip_Proof.prove_global thy2 [] [] t (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])) - (Datatype_Prop.make_cases new_type_names descr thy2); + (Datatype_Prop.make_cases case_names descr thy2); in thy2 |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms) @@ -351,7 +351,7 @@ (******************************* case splitting *******************************) fun prove_split_thms (config : Datatype_Aux.config) - new_type_names descr constr_inject dist_rewrites casedist_thms case_thms thy = + new_type_names case_names descr constr_inject dist_rewrites casedist_thms case_thms thy = let val _ = Datatype_Aux.message config "Proving equations for case splitting ..."; @@ -374,10 +374,10 @@ val split_thm_pairs = map prove_split_thms - (Datatype_Prop.make_splits new_type_names descr thy ~~ constr_inject ~~ + (Datatype_Prop.make_splits case_names descr thy ~~ constr_inject ~~ dist_rewrites ~~ casedist_thms ~~ case_thms ~~ newTs); - val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs + val (split_thms, split_asm_thms) = split_list split_thm_pairs in thy @@ -386,14 +386,14 @@ |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2)) end; -fun prove_weak_case_congs new_type_names descr thy = +fun prove_weak_case_congs new_type_names case_names descr thy = let fun prove_weak_case_cong t = Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t) - (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1]); + (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]); val weak_case_congs = - map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs new_type_names descr thy); + map prove_weak_case_cong (Datatype_Prop.make_weak_case_congs case_names descr thy); in thy |> Datatype_Aux.store_thms "weak_case_cong" new_type_names weak_case_congs end; @@ -421,7 +421,7 @@ in thy |> Datatype_Aux.store_thms "nchotomy" new_type_names nchotomys end; -fun prove_case_congs new_type_names descr nchotomys case_thms thy = +fun prove_case_congs new_type_names case_names descr nchotomys case_thms thy = let fun prove_case_cong ((t, nchotomy), case_rewrites) = let @@ -444,8 +444,8 @@ end; val case_congs = - map prove_case_cong (Datatype_Prop.make_case_congs - new_type_names descr thy ~~ nchotomys ~~ case_thms); + map prove_case_cong + (Datatype_Prop.make_case_congs case_names descr thy ~~ nchotomys ~~ case_thms); in thy |> Datatype_Aux.store_thms "case_cong" new_type_names case_congs end; diff -r 2dad374cf440 -r 71b8d0d170b1 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Dec 14 20:36:17 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Dec 14 21:54:32 2011 +0100 @@ -300,12 +300,13 @@ val ((case_rewrites, case_names), thy6) = thy5 |> Datatype_Abs_Proofs.prove_case_thms config new_type_names descr rec_names rec_rewrites; val (case_congs, thy7) = thy6 - |> Datatype_Abs_Proofs.prove_case_congs new_type_names descr nchotomys case_rewrites; + |> Datatype_Abs_Proofs.prove_case_congs new_type_names case_names descr + nchotomys case_rewrites; val (weak_case_congs, thy8) = thy7 - |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names descr; + |> Datatype_Abs_Proofs.prove_weak_case_congs new_type_names case_names descr; val (splits, thy9) = thy8 |> Datatype_Abs_Proofs.prove_split_thms - config new_type_names descr inject distinct exhaust case_rewrites; + config new_type_names case_names descr inject distinct exhaust case_rewrites; val inducts = Project_Rule.projections (Proof_Context.init_global thy2) induct; val dt_infos = map_index diff -r 2dad374cf440 -r 71b8d0d170b1 src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Dec 14 20:36:17 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Dec 14 21:54:32 2011 +0100 @@ -204,7 +204,7 @@ in (rec_result_Ts, reccomb_fn_Ts) end; -fun make_primrecs new_type_names descr thy = +fun make_primrecs reccomb_names descr thy = let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr'; @@ -216,11 +216,6 @@ map (uncurry (Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts))); - val big_reccomb_name = space_implode "_" new_type_names ^ "_rec"; - val reccomb_names = - map (Sign.intern_const thy) - (if length descr' = 1 then [big_reccomb_name] - else (map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'))); val reccombs = map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns)) (reccomb_names ~~ recTs ~~ rec_result_Ts); @@ -256,7 +251,7 @@ (****************** make terms of form t_case f1 ... fn *********************) -fun make_case_combs new_type_names descr thy fname = +fun make_case_combs case_names descr thy fname = let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr'; @@ -268,8 +263,6 @@ map (fn (_, cargs) => let val Ts = map (Datatype_Aux.typ_of_dtyp descr') cargs in Ts ---> T' end) constrs) (hd descr); - - val case_names = map (fn s => Sign.intern_const thy (s ^ "_case")) new_type_names; in map (fn ((name, Ts), T) => list_comb (Const (name, Ts @ [T] ---> T'), @@ -279,7 +272,7 @@ (**************** characteristic equations for case combinator ****************) -fun make_cases new_type_names descr thy = +fun make_cases case_names descr thy = let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr'; @@ -296,14 +289,14 @@ end; in map (fn (((_, (_, _, constrs)), T), comb_t) => - map (make_case T comb_t) (constrs ~~ (snd (strip_comb comb_t)))) - ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr thy "f")) + map (make_case T comb_t) (constrs ~~ snd (strip_comb comb_t))) + (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f") end; (*************************** the "split" - equations **************************) -fun make_splits new_type_names descr thy = +fun make_splits case_names descr thy = let val descr' = flat descr; val recTs = Datatype_Aux.get_rec_types descr'; @@ -338,14 +331,14 @@ end in - map make_split (hd descr ~~ newTs ~~ make_case_combs new_type_names descr thy "f") + map make_split (hd descr ~~ newTs ~~ make_case_combs case_names descr thy "f") end; (************************* additional rules for TFL ***************************) -fun make_weak_case_congs new_type_names descr thy = +fun make_weak_case_congs case_names descr thy = let - val case_combs = make_case_combs new_type_names descr thy "f"; + val case_combs = make_case_combs case_names descr thy "f"; fun mk_case_cong comb = let @@ -372,10 +365,10 @@ * (ty_case f1..fn M = ty_case g1..gn M') *---------------------------------------------------------------------------*) -fun make_case_congs new_type_names descr thy = +fun make_case_congs case_names descr thy = let - val case_combs = make_case_combs new_type_names descr thy "f"; - val case_combs' = make_case_combs new_type_names descr thy "g"; + val case_combs = make_case_combs case_names descr thy "f"; + val case_combs' = make_case_combs case_names descr thy "g"; fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) = let diff -r 2dad374cf440 -r 71b8d0d170b1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 14 20:36:17 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 14 21:54:32 2011 +0100 @@ -903,9 +903,9 @@ fun datatype_names_of_case_name thy case_name = map (#1 o #2) (#descr (the (Datatype_Data.info_of_case thy case_name))) -fun make_case_distribs new_type_names descr thy = +fun make_case_distribs case_names descr thy = let - val case_combs = Datatype_Prop.make_case_combs new_type_names descr thy "f"; + val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f"; fun make comb = let val Type ("fun", [T, T']) = fastype_of comb; @@ -932,10 +932,10 @@ fun case_rewrites thy Tcon = let - val {descr, ...} = Datatype.the_info thy Tcon + val {descr, case_name, ...} = Datatype.the_info thy Tcon in map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop) - (make_case_distribs [Tcon] [descr] thy) + (make_case_distribs [case_name] [descr] thy) end fun instantiated_case_rewrites thy Tcon =