# HG changeset patch
# User wenzelm
# Date 995659151 -7200
# Node ID bd1a7f53c11b759bf148ef5cad68415990b6db24
# Parent  996bd4eb0ef366d9ae42f0c7841493e45fcaa98d
replaced "Eps" by "The";

diff -r 996bd4eb0ef3 -r bd1a7f53c11b src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 20 21:58:19 2001 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Jul 20 21:59:11 2001 +0200
@@ -245,8 +245,7 @@
         (cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
       end;
 
-    val rec_total_thms = map (fn r =>
-      r RS ex1_implies_ex RS (some_eq_ex RS iffD2)) rec_unique_thms;
+    val rec_total_thms = map (fn r => r RS theI') rec_unique_thms;
 
     (* define primrec combinators *)
 
@@ -265,7 +264,7 @@
           (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
       (PureThy.add_defs_i false 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',
+           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>>
       parent_path flat_names;
@@ -277,7 +276,7 @@
 
     val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
       (cterm_of (Theory.sign_of thy2) t) (fn _ =>
-        [rtac some1_equality 1,
+        [rtac the1_equality 1,
          resolve_tac rec_unique_thms 1,
          resolve_tac rec_intrs 1,
          rewrite_goals_tac [o_def, fun_rel_comp_def],
diff -r 996bd4eb0ef3 -r bd1a7f53c11b src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 20 21:58:19 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Jul 20 21:59:11 2001 +0200
@@ -29,12 +29,12 @@
 
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
-(* figure out internal names *)
+
+(** theory context references **)
 
-val image_name = Sign.intern_const (Theory.sign_of Set.thy) "image";
-val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV";
-val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on";
-val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv";
+val f_myinv_f = thm "f_myinv_f";
+val myinv_f_f = thm "myinv_f_f";
+
 
 fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
   #exhaustion (the (Symtab.lookup (dt_info, tname)));
@@ -287,7 +287,7 @@
 	    prove_goalw_cterm [] 
 	      (cterm_of sg
 	       (HOLogic.mk_Trueprop 
-		(Const (inj_on_name, [AbsT, UnivT] ---> HOLogic.boolT) $
+		(Const ("Fun.inj_on", [AbsT, UnivT] ---> HOLogic.boolT) $
 		 Const (Abs_name, AbsT) $ Const (rep_set_name, UnivT))))
               (fn _ => [rtac inj_on_inverseI 1, etac thm1 1]);
 
@@ -297,8 +297,8 @@
 	    prove_goalw_cterm []
 	      (cterm_of sg
 	       (HOLogic.mk_Trueprop
-		(Const (inj_on_name, [RepT, setT] ---> HOLogic.boolT) $
-		 Const (Rep_name, RepT) $ Const (UNIV_name, setT))))
+		(Const ("Fun.inj_on", [RepT, setT] ---> HOLogic.boolT) $
+		 Const (Rep_name, RepT) $ Const ("UNIV", setT))))
               (fn _ => [rtac inj_inverseI 1, rtac thm2 1])
 
       in (inj_Abs_thm, inj_Rep_thm) end;
@@ -419,8 +419,8 @@
         HOLogic.mk_mem (mk_Free "x" Univ_elT i, Const (set_name, UnivT)) $
           (if i < length newTs then Const ("True", HOLogic.boolT)
            else HOLogic.mk_mem (mk_Free "x" Univ_elT i,
-             Const (image_name, [isoT, HOLogic.mk_setT T] ---> UnivT) $
-               Const (iso_name, isoT) $ Const (UNIV_name, HOLogic.mk_setT T)))
+             Const ("image", [isoT, HOLogic.mk_setT T] ---> UnivT) $
+               Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T)))
       end;
 
     val iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
@@ -443,11 +443,6 @@
                rtac (sym RS range_eqI) 1,
                resolve_tac iso_char_thms 1])])));
 
-    val Abs_inverse_thms' = (map #1 newT_iso_axms) @ map (fn r => r RS mp RS f_inv_f) iso_thms;
-
-    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
-      map mk_funs_inv Abs_inverse_thms');
-
     (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
 
     fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
@@ -511,6 +506,14 @@
 
     val (iso_inj_thms, iso_elem_thms) = foldr prove_iso_thms
       (tl descr, (map snd newT_iso_inj_thms, map #3 newT_iso_axms));
+    val iso_inj_thms_unfolded = drop (length (hd descr), iso_inj_thms);
+
+    val Abs_inverse_thms' =
+      map #1 newT_iso_axms @
+      map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) (iso_inj_thms_unfolded, iso_thms);
+
+    val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
+      map mk_funs_inv Abs_inverse_thms');
 
     (******************* freeness theorems for constructors *******************)
 
@@ -586,8 +589,8 @@
     val _ = message "Proving induction rule for datatypes ...";
 
     val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
-      (map (fn r => r RS inv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
-    val Rep_inverse_thms' = map (fn r => r RS inv_f_f)
+      (map (fn r => r RS myinv_f_f RS subst) (drop (length newTs, iso_inj_thms)));
+    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f)
       (drop (length newTs, iso_inj_thms));
 
     fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
@@ -598,7 +601,7 @@
         val Abs_t = if i < length newTs then
             Const (Sign.intern_const (Theory.sign_of thy6)
               ("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T)
-          else Const (inv_name, [T --> Univ_elT, Univ_elT] ---> T) $
+          else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $
             Const (nth_elem (i, all_rep_names), T --> Univ_elT)
 
       in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t,