# HG changeset patch
# User berghofe
# Date 997205348 -7200
# Node ID ba2c252b55adce15b6643b5451147fa5a6fd2fc7
# Parent  d3a3be6660f936bab9a3222f7ace54e1dfa5cd27
- Fixed bug in isomorphism proofs (caused by migration from SOME to THE)
- Funs_rangeE now requires function g to be injective

diff -r d3a3be6660f9 -r ba2c252b55ad src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Aug 07 19:26:42 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Aug 07 19:29:08 2001 +0200
@@ -411,38 +411,6 @@
         rule_by_tactic (atac 2) (thm RSN (2, inv'))
       end;
 
-    (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
-
-    fun mk_iso_t (((set_name, iso_name), i), T) =
-      let val isoT = T --> Univ_elT
-      in HOLogic.imp $ 
-        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", [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
-      (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
-
-    (* all the theorems are proved by one single simultaneous induction *)
-
-    val iso_thms = if length descr = 1 then [] else
-      drop (length newTs, split_conj_thm
-        (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
-           [indtac rep_induct 1,
-            REPEAT (rtac TrueI 1),
-            REPEAT (EVERY
-              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
-               REPEAT (etac Funs_IntE 1),
-               REPEAT (eresolve_tac [rangeE, Funs_rangeE] 1),
-               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
-                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
-               TRY (hyp_subst_tac 1),
-               rtac (sym RS range_eqI) 1,
-               resolve_tac iso_char_thms 1])])));
-
     (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
 
     fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
@@ -464,7 +432,8 @@
         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
 
         val rewrites = map mk_meta_eq iso_char_thms;
-        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o]) inj_thms);
+        val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
+          (map snd newT_iso_inj_thms @ inj_thms));
 
         val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
@@ -501,16 +470,50 @@
 			 REPEAT (FIRST [atac 1, etac spec 1,
 				 resolve_tac (FunsI :: elem_thms) 1])])]);
 
-      in (inj_thms @ inj_thms'', elem_thms @ (split_conj_thm elem_thm))
+      in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
+      end;
+
+    val (iso_inj_thms_unfolded, iso_elem_thms) = foldr prove_iso_thms
+      (tl descr, ([], map #3 newT_iso_axms));
+    val iso_inj_thms = map snd newT_iso_inj_thms @ iso_inj_thms_unfolded;
+
+    (* prove  x : dt_rep_set_i --> x : range dt_Rep_i *)
+
+    fun mk_iso_t (((set_name, iso_name), i), T) =
+      let val isoT = T --> Univ_elT
+      in HOLogic.imp $ 
+        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", [isoT, HOLogic.mk_setT T] ---> UnivT) $
+               Const (iso_name, isoT) $ Const ("UNIV", HOLogic.mk_setT T)))
       end;
 
-    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 iso_t = HOLogic.mk_Trueprop (mk_conj (map mk_iso_t
+      (rep_set_names ~~ all_rep_names ~~ (0 upto (length descr' - 1)) ~~ recTs)));
+
+    (* all the theorems are proved by one single simultaneous induction *)
+
+    val iso_thms = if length descr = 1 then [] else
+      drop (length newTs, split_conj_thm
+        (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
+           [indtac rep_induct 1,
+            REPEAT (rtac TrueI 1),
+            REPEAT (EVERY
+              [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
+               REPEAT (etac Funs_IntE 1),
+               REPEAT (eresolve_tac (rangeE ::
+                 map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1),
+               REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
+                 map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
+               TRY (hyp_subst_tac 1),
+               rtac (sym RS range_eqI) 1,
+               resolve_tac iso_char_thms 1])])));
 
     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);
+      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');
@@ -589,9 +592,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 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));
+      (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
+    val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded;
 
     fun mk_indrule_lemma ((prems, concls), ((i, _), T)) =
       let