--- 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],
--- 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,