# HG changeset patch # User wenzelm # Date 916145691 -3600 # Node ID d9db67970c73bf0e42a9dde283f2a1333c0293fc # Parent e3cdbd929a24c40cc79f71f54343fe8098f1442a eliminated tthm type and Attribute structure; diff -r e3cdbd929a24 -r d9db67970c73 TFL/tfl.sml --- a/TFL/tfl.sml Tue Jan 12 13:40:08 1999 +0100 +++ b/TFL/tfl.sml Tue Jan 12 13:54:51 1999 +0100 @@ -339,7 +339,7 @@ Sign.infer_types (sign_of thy) (K None) (K None) [] false ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], propT) - in PureThy.add_defs_i [Attribute.none (def_name, def_term)] thy end + in PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy end end; @@ -461,7 +461,7 @@ val R'abs = S.rand R' val theory = thy - |> PureThy.add_defs_i [Attribute.none (Name ^ "_def", subst_free[(R1,R')] proto_def)]; + |> PureThy.add_defs_i [Thm.no_attributes (Name ^ "_def", subst_free[(R1,R')] proto_def)]; val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq) val fconst = #lhs(S.dest_eq(concl def)) val tych = Thry.typecheck theory diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/HOL.ML --- a/src/HOL/HOL.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/HOL.ML Tue Jan 12 13:54:51 1999 +0100 @@ -422,7 +422,7 @@ local -fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x; +fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; in diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 12 13:54:51 1999 +0100 @@ -275,7 +275,7 @@ in (thy2 |> Theory.add_path (space_implode "_" new_type_names) |> - PureThy.add_tthmss [(("recs", Attribute.tthms_of rec_thms), [])] |> + PureThy.add_thmss [(("recs", rec_thms), [])] |> Theory.parent_path, reccomb_names, rec_thms) end; @@ -518,7 +518,7 @@ in (thy' |> Theory.add_path big_name |> - PureThy.add_tthmss [(("size", Attribute.tthms_of size_thms), [])] |> + PureThy.add_thmss [(("size", size_thms), [])] |> Theory.parent_path, size_thms) end; diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Tue Jan 12 13:54:51 1999 +0100 @@ -78,14 +78,14 @@ fun store_thmss label tnames thmss thy = foldr (fn ((tname, thms), thy') => thy' |> Theory.add_path tname |> - PureThy.add_tthmss [((label, Attribute.tthms_of thms), [])] |> + PureThy.add_thmss [((label, thms), [])] |> Theory.parent_path) (tnames ~~ thmss, thy); fun store_thms label tnames thms thy = foldr (fn ((tname, thm), thy') => thy' |> Theory.add_path tname |> - PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |> + PureThy.add_thms [((label, thm), [])] |> Theory.parent_path) (tnames ~~ thms, thy); diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -402,7 +402,7 @@ val thy11 = thy10 |> Theory.add_path (space_implode "_" new_type_names) |> - PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |> + PureThy.add_thmss [(("simps", simps), [])] |> put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> Theory.parent_path; @@ -459,7 +459,7 @@ val thy11 = thy10 |> Theory.add_path (space_implode "_" new_type_names) |> - PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |> + PureThy.add_thmss [(("simps", simps), [])] |> put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> Theory.parent_path; @@ -550,7 +550,7 @@ val thy9 = thy8 |> Theory.add_path (space_implode "_" new_type_names) |> - PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), [])] |> + PureThy.add_thmss [(("simps", simps), [])] |> put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |> Theory.parent_path; @@ -571,8 +571,7 @@ simps = simps}) end; -val rep_datatype = gen_rep_datatype - (fn thy => Attribute.thms_of o PureThy.get_tthmss thy) get_thm; +val rep_datatype = gen_rep_datatype (fn thy => PureThy.get_thmss thy) get_thm; val rep_datatype_i = gen_rep_datatype (K I) (K I); (******************************** add datatype ********************************) diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 12 13:54:51 1999 +0100 @@ -535,7 +535,7 @@ val thy7 = thy6 |> Theory.add_path big_name |> - PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |> + PureThy.add_thms [(("induct", dt_induct), [])] |> Theory.parent_path; in (thy7, constr_inject, dist_rewrites, dt_induct) diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -464,12 +464,11 @@ else standard (raw_induct RSN (2, rev_mp)); val thy'' = thy' |> - PureThy.add_tthmss [(("intrs", Attribute.tthms_of intrs), [])] |> - (if no_elim then I else PureThy.add_tthmss - [(("elims", Attribute.tthms_of elims), [])]) |> - (if no_ind then I else PureThy.add_tthms - [(((if coind then "co" else "") ^ "induct", - Attribute.tthm_of induct), [])]) |> + PureThy.add_thmss [(("intrs", intrs), [])] |> + (if no_elim then I else PureThy.add_thmss + [(("elims", elims), [])]) |> + (if no_ind then I else PureThy.add_thms + [(((if coind then "co" else "") ^ "induct", induct), [])]) |> Theory.parent_path; in (thy'', @@ -517,7 +516,7 @@ val thy'' = thy' |> (if coind then I - else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |> + else PureThy.add_thms [(("induct", induct), [])]) |> Theory.parent_path in (thy'', @@ -600,8 +599,8 @@ val intr_ts'' = map subst intr_ts'; in add_inductive_i verbose false "" coind false false cs'' intr_ts'' - (Attribute.thms_of (PureThy.get_tthmss thy monos)) - (Attribute.thms_of (PureThy.get_tthmss thy con_defs)) thy + (PureThy.get_thmss thy monos) + (PureThy.get_thmss thy con_defs) thy end; end; diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/primrec_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -235,11 +235,11 @@ commas names1 ^ " ..."); val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1])) eqns; - val tsimps = Attribute.tthms_of char_thms; + val simps = char_thms; val thy'' = thy' |> - PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |> - PureThy.add_tthms (map (rpair []) - (filter_out (equal "" o fst) (map fst eqns ~~ tsimps))) |> + PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> + PureThy.add_thms (map (rpair []) + (filter_out (equal "" o fst) (map fst eqns ~~ simps))) |> Theory.parent_path; in (thy'', char_thms) diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/record_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -53,7 +53,7 @@ let val ss = Simplifier.simpset_ref_of thy; val cs = Classical.claset_ref_of thy; - val (cs', ss') = (! cs, ! ss) addIffs [Attribute.thm_of th]; + val (cs', ss') = (! cs, ! ss) addIffs [th]; in ss := ss'; cs := cs'; (thy, th) end; fun add_wrapper wrapper thy = @@ -68,7 +68,7 @@ val (op :==) = Logic.mk_defpair; val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq; -fun get_defs thy specs = map (PureThy.get_tthm thy o fst) specs; +fun get_defs thy specs = map (PureThy.get_thm thy o fst) specs; (* proof by simplification *) @@ -76,14 +76,13 @@ fun prove_simp thy tacs simps = let val sign = Theory.sign_of thy; - val ss = Simplifier.addsimps (HOL_basic_ss, Attribute.thms_of simps); + val ss = Simplifier.addsimps (HOL_basic_ss, simps); fun prove goal = - Attribute.tthm_of - (Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal) - (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)])) - handle ERROR => error ("The error(s) above occurred while trying to prove " - ^ quote (Sign.string_of_term sign goal))); + Goals.prove_goalw_cterm [] (Thm.cterm_of sign goal) + (K (tacs @ [ALLGOALS (Simplifier.simp_tac ss)])) + handle ERROR => error ("The error(s) above occurred while trying to prove " + ^ quote (Sign.string_of_term sign goal)); in prove end; @@ -328,12 +327,12 @@ {args: (string * sort) list, parent: (typ list * string) option, fields: (string * typ) list, - simps: tthm list}; + simps: thm list}; type parent_info = {name: string, fields: (string * typ) list, - simps: tthm list}; + simps: thm list}; (* data kind 'HOL/records' *) @@ -519,12 +518,10 @@ (* 1st stage: types_thy *) - val (types_thy, simps) = + val (types_thy, datatype_simps) = thy |> field_type_defs fieldT_specs; - val datatype_simps = Attribute.tthms_of simps; - (* 2nd stage: defs_thy *) @@ -532,7 +529,7 @@ types_thy |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls) - |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal]))) + |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) (field_specs @ dest_specs); val field_defs = get_defs defs_thy field_specs; @@ -547,14 +544,14 @@ val field_injects = map prove_std inject_props; val dest_convs = map prove_std dest_props; val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1] - (map (apfst Thm.symmetric) field_defs @ dest_convs)) surj_props; + (map Thm.symmetric field_defs @ dest_convs)) surj_props; fun mk_split th = SplitPairedAll.rule (th RS eq_reflection); - val field_splits = map (fn (th, _) => Attribute.tthm_of (mk_split th)) surj_pairs; + val field_splits = map mk_split surj_pairs; val thms_thy = defs_thy - |> (PureThy.add_tthmss o map Attribute.none) + |> (PureThy.add_thmss o map Thm.no_attributes) [("field_defs", field_defs), ("dest_defs", dest_defs), ("dest_convs", dest_convs), @@ -692,7 +689,7 @@ |> Theory.add_path bname |> field_definitions fields names zeta moreT more vars named_vars; - val named_splits = map2 (fn (c, (th, _)) => (suffix field_typeN c, th)) (names, field_splits); + val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits); (* 2nd stage: defs_thy *) @@ -705,9 +702,9 @@ |> Theory.add_trfuns ([], [], field_tr's, []) |> (Theory.add_consts_i o map Syntax.no_syn) (sel_decls @ update_decls @ make_decls) - |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal]))) + |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) (sel_specs @ update_specs) - |> (PureThy.add_defs_i o map Attribute.none) make_specs; + |> (PureThy.add_defs_i o map Thm.no_attributes) make_specs; val sel_defs = get_defs defs_thy sel_specs; val update_defs = get_defs defs_thy update_specs; @@ -726,13 +723,13 @@ val thms_thy = defs_thy - |> (PureThy.add_tthmss o map Attribute.none) + |> (PureThy.add_thmss o map Thm.no_attributes) [("select_defs", sel_defs), ("update_defs", update_defs), ("make_defs", make_defs), ("select_convs", sel_convs), ("update_convs", update_convs)] - |> PureThy.add_tthmss + |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global]), (("iffs", field_injects), [add_iffs_global])]; diff -r e3cdbd929a24 -r d9db67970c73 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOL/Tools/typedef_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -141,9 +141,9 @@ ((if no_def then [] else [(name, setT, NoSyn)]) @ [(Rep_name, newT --> oldT, NoSyn), (Abs_name, oldT --> newT, NoSyn)]) - |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none) + |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes) [(name ^ "_def", Logic.mk_equals (setC, set))]) - |> (PureThy.add_axioms_i o map Attribute.none) + |> (PureThy.add_axioms_i o map Thm.no_attributes) [(Rep_name, rep_type), (Rep_name ^ "_inverse", rep_type_inv), (Abs_name ^ "_inverse", abs_type_inv)] diff -r e3cdbd929a24 -r d9db67970c73 src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOLCF/domain/axioms.ML Tue Jan 12 13:54:51 1999 +0100 @@ -86,7 +86,7 @@ [take_def, finite_def]) end; (* let *) -val add_axioms_i = PureThy.add_axioms_i o map Attribute.none; +val add_axioms_i = PureThy.add_axioms_i o map Thm.no_attributes; in (* local *) diff -r e3cdbd929a24 -r d9db67970c73 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/HOLCF/domain/theorems.ML Tue Jan 12 13:54:51 1999 +0100 @@ -323,7 +323,7 @@ (filter (fn (_,args)=>exists is_nonlazy_rec args) cons); val copy_rews = copy_strict::copy_apps @ copy_stricts; in thy |> Theory.add_path (Sign.base_name dname) - |> (PureThy.add_tthmss o map Attribute.no_attrss) [ + |> (PureThy.add_thmss o map Thm.no_attributes) [ ("iso_rews" , iso_rews ), ("exhaust" , [exhaust] ), ("casedist" , [casedist]), @@ -598,7 +598,7 @@ in thy |> Theory.add_path comp_dnam - |> (PureThy.add_tthmss o map Attribute.no_attrss) [ + |> (PureThy.add_thmss o map Thm.no_attributes) [ ("take_rews" , take_rews ), ("take_lemmas", take_lemmas), ("finites" , finites ), diff -r e3cdbd929a24 -r d9db67970c73 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -245,7 +245,7 @@ if need_recursor then thy |> Theory.add_consts_i [(recursor_base_name, recursor_typ, NoSyn)] - |> PureThy.add_defs_i [Attribute.none recursor_def] + |> PureThy.add_defs_i [Thm.no_attributes recursor_def] else thy; val thy0 = thy_path @@ -253,7 +253,7 @@ ((case_base_name, case_typ, NoSyn) :: map #1 (flat con_ty_lists)) |> PureThy.add_defs_i - (map Attribute.none + (map Thm.no_attributes (case_def :: flat (ListPair.map mk_con_defs (1 upto npart, con_ty_lists)))) @@ -392,8 +392,7 @@ in (*Updating theory components: simprules and datatype info*) (thy1 |> Theory.add_path big_rec_base_name - |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), - [Simplifier.simp_add_global])] + |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> DatatypesData.put (Symtab.update ((big_rec_name, dt_info), DatatypesData.get thy1)) diff -r e3cdbd929a24 -r d9db67970c73 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Tue Jan 12 13:54:51 1999 +0100 @@ -165,8 +165,7 @@ in thy |> Theory.add_path (Sign.base_name big_rec_name) - |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), - [Simplifier.simp_add_global])] + |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] |> DatatypesData.put (Symtab.update ((big_rec_name, dt_info), DatatypesData.get thy)) diff -r e3cdbd929a24 -r d9db67970c73 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -169,7 +169,7 @@ (*add definitions of the inductive sets*) val thy1 = thy |> Theory.add_path big_rec_base_name - |> PureThy.add_defs_i (map Attribute.none axpairs) + |> PureThy.add_defs_i (map Thm.no_attributes axpairs) (*fetch fp definitions from the theory*) @@ -519,9 +519,9 @@ and mutual_induct = CP.remove_split mutual_induct_fsplit in (thy - |> PureThy.add_tthms - [(("induct", Attribute.tthm_of induct), []), - (("mutual_induct", Attribute.tthm_of mutual_induct), [])], + |> PureThy.add_thms + [(("induct", induct), []), + (("mutual_induct", mutual_induct), [])], induct, mutual_induct) end; (*of induction_rules*) @@ -534,13 +534,13 @@ in (thy2 - |> PureThy.add_tthms - [(("bnd_mono", Attribute.tthm_of bnd_mono), []), - (("dom_subset", Attribute.tthm_of dom_subset), []), - (("elim", Attribute.tthm_of elim), [])] - |> PureThy.add_tthmss - [(("defs", Attribute.tthms_of defs), []), - (("intrs", Attribute.tthms_of intrs), [])] + |> (PureThy.add_thms o map Thm.no_attributes) + [("bnd_mono", bnd_mono), + ("dom_subset", dom_subset), + ("elim", elim)] + |> (PureThy.add_thmss o map Thm.no_attributes) + [("defs", defs), + ("intrs", intrs)] |> Theory.parent_path, {defs = defs, bnd_mono = bnd_mono, diff -r e3cdbd929a24 -r d9db67970c73 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Jan 12 13:40:08 1999 +0100 +++ b/src/ZF/Tools/primrec_package.ML Tue Jan 12 13:54:51 1999 +0100 @@ -173,20 +173,20 @@ val rewrites = get_axiom thy' (#1 def) :: map mk_meta_eq (#rec_rewrites con_info) val char_thms = - (if !Ind_Syntax.trace then + (if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *) writeln ("Proving equations for primrec function " ^ fname) else (); - map (fn (_,t) => + map (fn (_,t) => prove_goalw_cterm rewrites (Ind_Syntax.traceIt "next primrec equation = " (cterm_of (sign_of thy') t)) (fn _ => [rtac refl 1])) recursion_eqns); - val tsimps = Attribute.tthms_of char_thms; + val simps = char_thms; val thy'' = thy' - |> PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] - |> PureThy.add_tthms (map (rpair []) - (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ tsimps))) + |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])] + |> PureThy.add_thms (map (rpair []) + (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps))) |> Theory.parent_path; in (thy'', char_thms)