# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256662955 -3600
# Node ID f88ea69331bfb6a9a6d83a950faa5be520ee2e30
# Parent  1e8e1b736586719ff22cb93be4b9d389d0021546
Simplfied interface to repabs_injection.

diff -r 1e8e1b736586 -r f88ea69331bf FSet.thy
--- a/FSet.thy	Tue Oct 27 17:08:47 2009 +0100
+++ b/FSet.thy	Tue Oct 27 18:02:35 2009 +0100
@@ -426,28 +426,14 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 done
 
-ML {* val (g, thm, othm) =
+ML {* val ind_r_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
    @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
    (@{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs})
   )
 *}
-
-ML {*
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm); *}
-(* ML {*    val cthm = Goal.prove @{context} [] [] g (fn x => tac2 (#context x) 1);
-*} *)
-
-ML {*
-  val ind_r_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t2 *}
+ML {* val ind_r_l = simp_lam_prs @{context} ind_r_t *}
 lemma app_prs_for_induct: "(ABS_fset ---> id) f (REP_fset T1) = f T1"
   apply (simp add: fun_map.simps QUOT_TYPE_I_fset.thm10)
 done
@@ -468,11 +454,10 @@
 let
   val ind_r_a = atomize_thm thm;
   val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context};
-  val (g, t, ot) =
-    repabs_eq @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
+  val ind_r_t =
+    repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"}
      @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2}
      (@{thms ho_memb_rsp ho_cons_rsp  ho_card1_rsp ho_map_rsp ho_append_rsp} @ @{thms ho_all_prs ho_ex_prs});
-  val ind_r_t = repabs_eq2 @{context} (g, t, ot);
   val ind_r_l = simp_lam_prs @{context} ind_r_t;
   val ind_r_a = simp_allex_prs @{context} quot ind_r_l;
   val ind_r_d = repeat_eqsubst_thm @{context} fset_defs_sym ind_r_a;
@@ -490,10 +475,9 @@
 ML {* lift @{thm list_eq.intros(5)} *}
 ML {* lift @{thm card1_suc} *}
 ML {* lift @{thm map_append} *}
+(* ML {* lift @{thm append_assoc} *}*)
 
-(* ML {* lift @{thm append_assoc} *} *)
-
-thm 
+thm
 
 
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
diff -r 1e8e1b736586 -r f88ea69331bf IntEx.thy
--- a/IntEx.thy	Tue Oct 27 17:08:47 2009 +0100
+++ b/IntEx.thy	Tue Oct 27 18:02:35 2009 +0100
@@ -168,22 +168,16 @@
 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *}
 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *}
 
-ML {* val (g, thm, othm) =
+ML {* val t_t =
   Toplevel.program (fn () =>
-  repabs_eq @{context} t_r consts rty qty
+  repabs @{context} t_r consts rty qty
    quot rel_refl trans2
    rsp_thms
   )
 *}
-ML {*
-  val t_t2 =
-  Toplevel.program (fn () =>
-    repabs_eq2 @{context} (g, thm, othm)
-  )
-*}
-
 
 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 {*
@@ -191,8 +185,8 @@
     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
 *}
-ML {* t_t2 *}
-ML {* val t_l = simp_lam_prs @{context} t_t2 *}
+ML {* t_t *}
+ML {* val t_l = simp_lam_prs @{context} t_t *}
 
 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
 
diff -r 1e8e1b736586 -r f88ea69331bf QuotMain.thy
--- a/QuotMain.thy	Tue Oct 27 17:08:47 2009 +0100
+++ b/QuotMain.thy	Tue Oct 27 18:02:35 2009 +0100
@@ -748,7 +748,7 @@
 *}
 
 ML {*
-fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
+fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms =
   let
     val rt = build_repabs_term lthy thm constructors rty qty;
     val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
@@ -756,19 +756,7 @@
       (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
     val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
   in
-    (rt, cthm, thm)
-  end
-*}
-
-ML {*
-fun repabs_eq2 lthy (rt, thm, othm) =
-  let
-    fun tac2 ctxt =
-     (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm]))
-     THEN' (rtac othm);
-    val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1);
-  in
-    cthm
+    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
   end
 *}
 
@@ -873,14 +861,13 @@
 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv lthy;
-  val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
-  val t_t2 = repabs_eq2 lthy t_t1;
+  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
   val abs = findabs rty (prop_of t_a);
   val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs;
   fun simp_lam_prs lthy thm =
     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
     handle _ => thm
-  val t_l = simp_lam_prs lthy t_t2;
+  val t_l = simp_lam_prs lthy t_t;
   val t_a = simp_allex_prs lthy quot t_l;
   val t_defs_sym = add_lower_defs lthy t_defs;
   val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a;