# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257265843 -3600
# Node ID c55883442514ace654b47f5910149200d27d95c6
# Parent  fe6eb116b341099298d4553ac10bfbb307d5a16a# Parent  4d58c02289caa91dc10b0e97a80ee7c7b3a8200d
merge

diff -r 4d58c02289ca -r c55883442514 FSet.thy
--- a/FSet.thy	Tue Nov 03 16:51:33 2009 +0100
+++ b/FSet.thy	Tue Nov 03 17:30:43 2009 +0100
@@ -301,7 +301,7 @@
 
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
 ML {* val rsp_thms =
   @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp}
@@ -358,9 +358,6 @@
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
-thm APP_PRS
-ML 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 thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}
diff -r 4d58c02289ca -r c55883442514 LamEx.thy
--- a/LamEx.thy	Tue Nov 03 16:51:33 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 17:30:43 2009 +0100
@@ -166,7 +166,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "lam" *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
 ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *}
 
diff -r 4d58c02289ca -r c55883442514 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 03 16:51:33 2009 +0100
+++ b/QuotMain.thy	Tue Nov 03 17:30:43 2009 +0100
@@ -962,6 +962,37 @@
   end
 *}
 
+ML {*
+fun applic_prs lthy rty qty absrep ty =
+ let
+  fun absty ty =
+    old_exchange_ty rty qty ty
+  fun mk_rep tm =
+    let
+      val ty = old_exchange_ty rty qty (fastype_of tm)
+    in fst (old_get_fun repF rty qty lthy ty) $ tm end;
+  fun mk_abs tm =
+      let
+        val ty = old_exchange_ty rty qty (fastype_of tm) in
+      fst (old_get_fun absF rty qty lthy ty) $ tm end;
+  val (l, ltl) = Term.strip_type ty;
+  val nl = map absty l;
+  val vs = map (fn _ => "x") l;
+  val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy;
+  val args = map Free (vfs ~~ nl);
+  val lhs = list_comb((Free (fname, nl ---> ltl)), args);
+  val rargs = map mk_rep args;
+  val f = Free (fname, nl ---> ltl);
+  val rhs = mk_abs (list_comb((mk_rep f), rargs));
+  val eq = Logic.mk_equals (rhs, lhs);
+  val ceq = cterm_of (ProofContext.theory_of lthy') eq;
+  val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps});
+  val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1)
+  val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t;
+ in
+  singleton (ProofContext.export lthy' lthy) t_id
+ end
+*}
 
 ML {*
 fun lookup_quot_data lthy qty =
@@ -983,9 +1014,10 @@
     val thy = ProofContext.theory_of lthy;
     val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
     val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
+    val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
     val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name)
   in
-    (trans2, reps_same, quot)
+    (trans2, reps_same, absrep, quot)
   end
 *}
 
@@ -1002,7 +1034,7 @@
 ML {*
 fun lift_thm lthy qty qty_name rsp_thms defs t = let
   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
-  val (trans2, reps_same, quot) = lookup_quot_thms lthy qty_name;
+  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
   val consts = lookup_quot_consts defs;
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
@@ -1013,7 +1045,7 @@
   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
   val abs = findabs rty (prop_of t_a);
   val aps = findaps rty (prop_of t_a);
-  val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps;
+  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
   val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
   val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
   val defs_sym = add_lower_defs lthy defs;