proper handling of axioms / defs;
authorwenzelm
Thu Oct 21 18:45:31 1999 +0200 (1999-10-21)
changeset 79042b551893583e
parent 7903 cc6177e1efca
child 7905 c5f735f7428c
proper handling of axioms / defs;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/primrec_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 21 18:44:34 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 21 18:45:31 1999 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4        Theory.add_consts_i (map (fn ((name, T), T') =>
     1.5          (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
     1.6            (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
     1.7 -      Theory.add_defs_i (map (fn ((((name, comb), set), T), T') =>
     1.8 +      (PureThy.add_defs_i o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
     1.9          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    1.10             Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.11               HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
    1.12 @@ -343,7 +343,7 @@
    1.13                list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
    1.14                  fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
    1.15            val thy' = thy |>
    1.16 -            Theory.add_consts_i [decl] |> Theory.add_defs_i [def];
    1.17 +            Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
    1.18  
    1.19          in (defs @ [get_def thy' (Sign.base_name name)], thy')
    1.20          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    1.21 @@ -446,13 +446,13 @@
    1.22        Theory.add_consts_i (map (fn (s, T) =>
    1.23          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
    1.24            (drop (length (hd descr), size_names ~~ recTs))) |>
    1.25 -      Theory.add_defs_i (map (fn (((s, T), def_name), rec_name) =>
    1.26 +      (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
    1.27          (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
    1.28            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
    1.29              (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>
    1.30        parent_path flat_names;
    1.31  
    1.32 -    val size_def_thms = map (get_axiom thy') def_names;
    1.33 +    val size_def_thms = map (get_thm thy') def_names;
    1.34      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
    1.35  
    1.36      val size_thms = map (fn t => prove_goalw_cterm rewrites
     2.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 21 18:44:34 1999 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 21 18:45:31 1999 +0200
     2.3 @@ -308,7 +308,7 @@
     2.4        val thy'' = thy' |>
     2.5          Theory.add_path tname |>
     2.6          PureThy.add_axioms_i [((label, t), [])];
     2.7 -      val ax = get_axiom thy'' label
     2.8 +      val ax = PureThy.get_thm thy'' label
     2.9      in (Theory.parent_path thy'', ax::axs)
    2.10      end) (tnames ~~ ts, (thy, []));
    2.11  
    2.12 @@ -434,7 +434,7 @@
    2.13        Theory.parent_path |>
    2.14        add_and_get_axiomss "inject" new_type_names
    2.15          (DatatypeProp.make_injs descr sorts);
    2.16 -    val induct = get_axiom thy3 "induct";
    2.17 +    val induct = get_thm thy3 "induct";
    2.18      val rec_thms = get_thms thy3 "recs";
    2.19      val size_thms = if no_size then [] else get_thms thy3 "size";
    2.20      val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 21 18:44:34 1999 +0200
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Oct 21 18:45:31 1999 +0200
     3.3 @@ -233,9 +233,9 @@
     3.4            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
     3.5          val thy' = thy |>
     3.6            Theory.add_consts_i [(cname', constrT, mx)] |>
     3.7 -          Theory.add_defs_i [(def_name, def)];
     3.8 +          (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
     3.9  
    3.10 -      in (thy', defs @ [get_axiom thy' def_name], eqns @ [eqn], i + 1)
    3.11 +      in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
    3.12        end;
    3.13  
    3.14      (* constructor definitions for datatype *)
    3.15 @@ -267,9 +267,9 @@
    3.16      (* get axioms from theory *)
    3.17  
    3.18      val newT_iso_axms = map (fn s =>
    3.19 -      (get_axiom thy4 ("Abs_" ^ s ^ "_inverse"),
    3.20 -       get_axiom thy4 ("Rep_" ^ s ^ "_inverse"),
    3.21 -       get_axiom thy4 ("Rep_" ^ s))) new_type_names;
    3.22 +      (get_thm thy4 ("Abs_" ^ s ^ "_inverse"),
    3.23 +       get_thm thy4 ("Rep_" ^ s ^ "_inverse"),
    3.24 +       get_thm thy4 ("Rep_" ^ s))) new_type_names;
    3.25  
    3.26      (*------------------------------------------------*)
    3.27      (* prove additional theorems:                     *)
    3.28 @@ -382,8 +382,8 @@
    3.29          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    3.30            equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
    3.31              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
    3.32 -        val thy' = Theory.add_defs_i defs thy;
    3.33 -        val def_thms = map (get_axiom thy') (map fst defs);
    3.34 +        val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    3.35 +        val def_thms = map (get_thm thy') (map fst defs);
    3.36  
    3.37          (* prove characteristic equations *)
    3.38  
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Oct 21 18:44:34 1999 +0200
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Oct 21 18:45:31 1999 +0200
     4.3 @@ -241,10 +241,10 @@
     4.4      val thy' = thy |>
     4.5        Theory.add_path (if alt_name = "" then (space_implode "_"
     4.6          (map (Sign.base_name o #1) defs)) else alt_name) |>
     4.7 -      (if eq_set (names1, names2) then Theory.add_defs_i defs'
     4.8 +      (if eq_set (names1, names2) then (PureThy.add_defs_i o map Thm.no_attributes) defs'
     4.9         else primrec_err ("functions " ^ commas_quote names2 ^
    4.10           "\nare not mutually recursive"));
    4.11 -    val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
    4.12 +    val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ (map (get_thm thy' o fst) defs');
    4.13      val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
    4.14      val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
    4.15          (fn _ => [rtac refl 1])) eqns;
     5.1 --- a/src/ZF/Tools/primrec_package.ML	Thu Oct 21 18:44:34 1999 +0200
     5.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Oct 21 18:45:31 1999 +0200
     5.3 @@ -168,8 +168,8 @@
     5.4  	foldr (process_eqn thy) (map snd recursion_eqns, None);
     5.5      val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns) 
     5.6      val thy' = thy |> Theory.add_path (Sign.base_name (#1 def))
     5.7 -                   |> Theory.add_defs_i [def]
     5.8 -    val rewrites = get_axiom thy' (#1 def) ::
     5.9 +                   |> (PureThy.add_defs_i o map Thm.no_attributes) [def]
    5.10 +    val rewrites = get_thm thy' (#1 def) ::
    5.11  	           map mk_meta_eq (#rec_rewrites con_info)
    5.12      val char_thms = 
    5.13  	(if !Ind_Syntax.trace then	(* FIXME message / quiet_mode (!?) *)