# HG changeset patch # User wenzelm # Date 940524331 -7200 # Node ID 2b551893583e23b8084e2b253ad6e29b7a194a1e # Parent cc6177e1efca472ee1a02b73c439fd73fa8d3296 proper handling of axioms / defs; diff -r cc6177e1efca -r 2b551893583e src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 21 18:44:34 1999 +0200 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 21 18:45:31 1999 +0200 @@ -260,7 +260,7 @@ Theory.add_consts_i (map (fn ((name, T), T') => (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> - Theory.add_defs_i (map (fn ((((name, comb), set), T), T') => + (PureThy.add_defs_i o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T, Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set)))))) @@ -343,7 +343,7 @@ list_comb (reccomb, (flat (take (i, case_dummy_fns))) @ fns2 @ (flat (drop (i + 1, case_dummy_fns))) ))); val thy' = thy |> - Theory.add_consts_i [decl] |> Theory.add_defs_i [def]; + Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def]; in (defs @ [get_def thy' (Sign.base_name name)], thy') end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~ @@ -446,13 +446,13 @@ Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T --> HOLogic.natT, NoSyn)) (drop (length (hd descr), size_names ~~ recTs))) |> - Theory.add_defs_i (map (fn (((s, T), def_name), rec_name) => + (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) => (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT), list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs)))) (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |> parent_path flat_names; - val size_def_thms = map (get_axiom thy') def_names; + val size_def_thms = map (get_thm thy') def_names; val rewrites = size_def_thms @ map mk_meta_eq primrec_thms; val size_thms = map (fn t => prove_goalw_cterm rewrites diff -r cc6177e1efca -r 2b551893583e src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Oct 21 18:44:34 1999 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Oct 21 18:45:31 1999 +0200 @@ -308,7 +308,7 @@ val thy'' = thy' |> Theory.add_path tname |> PureThy.add_axioms_i [((label, t), [])]; - val ax = get_axiom thy'' label + val ax = PureThy.get_thm thy'' label in (Theory.parent_path thy'', ax::axs) end) (tnames ~~ ts, (thy, [])); @@ -434,7 +434,7 @@ Theory.parent_path |> add_and_get_axiomss "inject" new_type_names (DatatypeProp.make_injs descr sorts); - val induct = get_axiom thy3 "induct"; + val induct = get_thm thy3 "induct"; val rec_thms = get_thms thy3 "recs"; val size_thms = if no_size then [] else get_thms thy3 "size"; val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names diff -r cc6177e1efca -r 2b551893583e src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 21 18:44:34 1999 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 21 18:45:31 1999 +0200 @@ -233,9 +233,9 @@ (Const (rep_name, T --> Univ_elT) $ lhs, rhs)); val thy' = thy |> Theory.add_consts_i [(cname', constrT, mx)] |> - Theory.add_defs_i [(def_name, def)]; + (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)]; - in (thy', defs @ [get_axiom thy' def_name], eqns @ [eqn], i + 1) + in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1) end; (* constructor definitions for datatype *) @@ -267,9 +267,9 @@ (* get axioms from theory *) val newT_iso_axms = map (fn s => - (get_axiom thy4 ("Abs_" ^ s ^ "_inverse"), - get_axiom thy4 ("Rep_" ^ s ^ "_inverse"), - get_axiom thy4 ("Rep_" ^ s))) new_type_names; + (get_thm thy4 ("Abs_" ^ s ^ "_inverse"), + get_thm thy4 ("Rep_" ^ s ^ "_inverse"), + get_thm thy4 ("Rep_" ^ s))) new_type_names; (*------------------------------------------------*) (* prove additional theorems: *) @@ -382,8 +382,8 @@ val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $ list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos); - val thy' = Theory.add_defs_i defs thy; - val def_thms = map (get_axiom thy') (map fst defs); + val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy; + val def_thms = map (get_thm thy') (map fst defs); (* prove characteristic equations *) diff -r cc6177e1efca -r 2b551893583e src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Thu Oct 21 18:44:34 1999 +0200 +++ b/src/HOL/Tools/primrec_package.ML Thu Oct 21 18:45:31 1999 +0200 @@ -241,10 +241,10 @@ val thy' = thy |> Theory.add_path (if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name) |> - (if eq_set (names1, names2) then Theory.add_defs_i defs' + (if eq_set (names1, names2) then (PureThy.add_defs_i o map Thm.no_attributes) defs' else primrec_err ("functions " ^ commas_quote names2 ^ "\nare not mutually recursive")); - val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs'); + val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ (map (get_thm thy' o fst) defs'); val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ..."); val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1])) eqns; diff -r cc6177e1efca -r 2b551893583e src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Thu Oct 21 18:44:34 1999 +0200 +++ b/src/ZF/Tools/primrec_package.ML Thu Oct 21 18:45:31 1999 +0200 @@ -168,8 +168,8 @@ foldr (process_eqn thy) (map snd recursion_eqns, None); val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns) val thy' = thy |> Theory.add_path (Sign.base_name (#1 def)) - |> Theory.add_defs_i [def] - val rewrites = get_axiom thy' (#1 def) :: + |> (PureThy.add_defs_i o map Thm.no_attributes) [def] + val rewrites = get_thm thy' (#1 def) :: map mk_meta_eq (#rec_rewrites con_info) val char_thms = (if !Ind_Syntax.trace then (* FIXME message / quiet_mode (!?) *)