# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256626012 -3600
# Node ID c0f2db9a243b5e8eabbec94bfd2789f56e49e363
# Parent  9163c0f9830dd4f86b489a38d6243670dba7ec1e
Further reordering in Int code.

diff -r 9163c0f9830d -r c0f2db9a243b IntEx.thy
--- a/IntEx.thy	Mon Oct 26 19:35:30 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 07:46:52 2009 +0100
@@ -132,6 +132,10 @@
 ML {* val quot = @{thm QUOTIENT_my_int} *}
 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *}
+ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *}
+ML {* val t_defs = @{thms PLUS_def} *}
+
+
 
 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
@@ -150,24 +154,6 @@
   )
 *}
 
-ML {*
-fun make_simp_lam_prs_thm lthy quot_thm typ =
-  let
-    val (_, [lty, rty]) = dest_Type typ;
-    val thy = ProofContext.theory_of lthy;
-    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
-    val inst = [SOME lcty, NONE, SOME rcty];
-    val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS};
-    val tac =
-      (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW
-      (quotient_tac quot_thm);
-    val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
-    val ts = @{thm HOL.sym} OF [t]
-  in
-    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts
-  end
-*}
-
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
@@ -180,25 +166,11 @@
 ML {* t_t2 *}
 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
 
-ML {*
-  fun simp_allex_prs lthy quot thm =
-    let
-      val rwf = @{thm FORALL_PRS} OF [quot];
-      val rwfs = @{thm "HOL.sym"} OF [rwf];
-      val rwe = @{thm EXISTS_PRS} OF [quot];
-      val rwes = @{thm "HOL.sym"} OF [rwe]
-    in
-      (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))
-    end
-    handle _ => thm
-*}
-
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
 
-ML {* val t_defs = @{thms PLUS_def} *}
 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}
 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *}
-ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *}
+ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
 
 lemma 
diff -r 9163c0f9830d -r c0f2db9a243b QuotMain.thy
--- a/QuotMain.thy	Mon Oct 26 19:35:30 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 07:46:52 2009 +0100
@@ -820,4 +820,35 @@
     | _ => []
 *}
 
+ML {*
+fun make_simp_lam_prs_thm lthy quot_thm typ =
+  let
+    val (_, [lty, rty]) = dest_Type typ;
+    val thy = ProofContext.theory_of lthy;
+    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
+    val inst = [SOME lcty, NONE, SOME rcty];
+    val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS};
+    val tac =
+      (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW
+      (quotient_tac quot_thm);
+    val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
+    val ts = @{thm HOL.sym} OF [t]
+  in
+    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts
+  end
+*}
+
+ML {*
+  fun simp_allex_prs lthy quot thm =
+    let
+      val rwf = @{thm FORALL_PRS} OF [quot];
+      val rwfs = @{thm "HOL.sym"} OF [rwf];
+      val rwe = @{thm EXISTS_PRS} OF [quot];
+      val rwes = @{thm "HOL.sym"} OF [rwe]
+    in
+      (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm))
+    end
+    handle _ => thm
+*}
+
 end