# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257172683 -3600
# Node ID 59578f428bbe6b3f825af5c994f7044699cadf9e
# Parent  22c199522befae9d25b7e9f56979cc1a1edd5d48
Fixes after optimization and preparing for a general FORALL_PRS

diff -r 22c199522bef -r 59578f428bbe FSet.thy
--- a/FSet.thy	Mon Nov 02 14:57:56 2009 +0100
+++ b/FSet.thy	Mon Nov 02 15:38:03 2009 +0100
@@ -367,11 +367,10 @@
 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *}
-ML {* val ind_r_a = simp_allex_prs @{context} quot ind_r_l *}
-ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
-ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
+ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}
+ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}
-ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a1 *}
+ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
 ML {* ObjectLogic.rulify ind_r_s *}
 
diff -r 22c199522bef -r 59578f428bbe IntEx.thy
--- a/IntEx.thy	Mon Nov 02 14:57:56 2009 +0100
+++ b/IntEx.thy	Mon Nov 02 15:38:03 2009 +0100
@@ -119,11 +119,11 @@
 ML {* val qty = @{typ "my_int"} *}
 ML {* val ty_name = "my_int" *}
 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
-ML {* val t_defs = @{thms PLUS_def} *}
+ML {* val defs = @{thms PLUS_def} *}
 
 ML {*
 fun lift_thm_my_int lthy t =
-  lift_thm lthy qty ty_name rsp_thms t_defs t
+  lift_thm lthy qty ty_name rsp_thms defs t
 *}
 
 ML {*
@@ -150,21 +150,19 @@
 
 
 text {* Below is the construction site code used if things do not work *}
-
-
+ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "my_int" *}
 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 *}
-ML {* val t_defs_sym = add_lower_defs @{context} t_defs *}
-
-
+ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
+ML {* val defs_sym = add_lower_defs @{context} defs *}
+ML {* val consts = lookup_quot_consts defs *}
 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *}
-ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
+ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *}
-ML {* val t_a = simp_allex_prs @{context} quot t_l *}
-ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *}
+ML {* val t_a = simp_allex_prs quot [] t_l *}
+ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}
 
+thm FORALL_PRS
 
-