# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1263166289 -3600
# Node ID 129caba33c034c9474a88aad68e4a453e105afc3
# Parent  b3bb2bad952f6220c5fbdd02eb406fbbfffa7e3c
the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"

diff -r b3bb2bad952f -r 129caba33c03 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Mon Jan 11 00:31:29 2010 +0100
@@ -369,6 +369,8 @@
 apply(cleaning)
 apply (simp add: finsert_def fconcat_def comp_def)
 apply cleaning
+(* ID PROBLEM *)
+apply(simp add: id_def[symmetric] id_simps)
 done
 
 text {* raw section *}
diff -r b3bb2bad952f -r 129caba33c03 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Jan 11 00:31:29 2010 +0100
@@ -250,10 +250,7 @@
 apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-apply(injection)
-sorry
-(* PROBLEM 
-done*)
+done
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
 by auto
@@ -263,10 +260,7 @@
 apply(rule impI)
 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 apply(simp add: id_rsp)
-apply(injection)
-sorry
-(* PROBLEM 
-done*)
+done
 
 term map
 
diff -r b3bb2bad952f -r 129caba33c03 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 11 00:31:29 2010 +0100
@@ -107,7 +107,7 @@
 lemmas [id_simps] =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
-  id_def[THEN eq_reflection, symmetric]
+  (*id_def[THEN eq_reflection, symmetric]*)
   id_o[THEN eq_reflection]
   o_id[THEN eq_reflection]
   eq_comp_r
diff -r b3bb2bad952f -r 129caba33c03 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Jan 11 00:31:29 2010 +0100
@@ -40,7 +40,7 @@
 let
   val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
   val qconst_bname = Binding.name lhs_str;
-  val absrep_trm = Syntax.check_term lthy (absrep_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs)
+  val absrep_trm = (absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty)) $ rhs
   val prop = Logic.mk_equals (lhs, absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'
diff -r b3bb2bad952f -r 129caba33c03 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Sat Jan 09 09:38:34 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Jan 11 00:31:29 2010 +0100
@@ -24,6 +24,15 @@
 
 exception LIFT_MATCH of string
 
+(* simplifies a term according to the id_rules *)
+fun id_simplify ctxt trm =
+let
+  val thy = ProofContext.theory_of ctxt 
+  val id_thms = id_simps_get ctxt
+in
+  MetaSimplifier.rewrite_term thy id_thms [] trm
+end		
+ 
 (******************************)
 (* Aggregate Rep/Abs Function *)
 (******************************)
@@ -190,9 +199,9 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             if tys' = [] orelse tys' = tys 
+             (*if tys' = [] orelse tys' = tys 
              then absrep_const flag ctxt s'
-             else mk_fun_compose flag (absrep_const flag ctxt s', result)
+             else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
            end
     | (TFree x, TFree x') =>
         if x = x'
@@ -204,7 +213,7 @@
 fun absrep_fun_chk flag ctxt (rty, qty) =
   absrep_fun flag ctxt (rty, qty)
   |> Syntax.check_term ctxt
-
+  |> id_simplify ctxt
 
 (**********************************)
 (* Aggregate Equivalence Relation *)
@@ -291,15 +300,16 @@
            val eqv_rel = get_equiv_rel ctxt s'
            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
          in
-           if tys' = [] orelse tys' = tys 
+           (*if tys' = [] orelse tys' = tys 
            then eqv_rel'
-           else mk_rel_compose (result, eqv_rel')
+           else*) mk_rel_compose (result, eqv_rel')
          end
       | _ => HOLogic.eq_const rty
 
 fun equiv_relation_chk ctxt (rty, qty) =
   equiv_relation ctxt (rty, qty)
   |> Syntax.check_term ctxt
+  |> id_simplify ctxt
 
 
 (******************)
@@ -452,6 +462,7 @@
 fun regularize_trm_chk ctxt (rtrm, qtrm) =
   regularize_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
+  |> id_simplify ctxt
 
 
 (*********************)
@@ -490,6 +501,14 @@
 fun mk_repabs ctxt (T, T') trm = 
   absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm)
 
+fun inj_repabs_err ctxt msg rtrm qtrm =
+let
+  val rtrm_str = Syntax.string_of_term ctxt rtrm
+  val qtrm_str = Syntax.string_of_term ctxt qtrm 
+in
+  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
+end
+
 
 (* bound variables need to be treated properly,     *)
 (* as the type of subterms needs to be calculated   *)
@@ -540,11 +559,12 @@
         else mk_repabs ctxt (rty, T') rtrm
       end   
   
-  | _ => raise (LIFT_MATCH "injection (default)")
+  | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
 
 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
   inj_repabs_trm ctxt (rtrm, qtrm) 
   |> Syntax.check_term ctxt
+  |> id_simplify ctxt
 
 end; (* structure *)