# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261604550 -3600
# Node ID 06e17083e90bd8339fa0edb702c9c73945641a57
# Parent  86c7ed9f354f9b0f59a32e261734ed546da670d6
modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants

diff -r 86c7ed9f354f -r 06e17083e90b Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Wed Dec 23 21:30:23 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Wed Dec 23 22:42:30 2009 +0100
@@ -9,6 +9,12 @@
   apply(auto)
   done
 
+print_quotients
+
+ML{*
+Quotient_Info.quotient_rules_get @{context}
+*}
+
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
@@ -17,6 +23,8 @@
 quotient_type int = "nat \<times> nat" / intrel
   sorry
 
+print_quotients
+
 ML {*
 open Quotient_Term;
 *}
diff -r 86c7ed9f354f -r 06e17083e90b Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Dec 23 21:30:23 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 22:42:30 2009 +0100
@@ -122,6 +122,15 @@
    for more complicated types of A and B
 *)
 
+(* instantiates TVars so that the term is of type ty *)
+fun force_typ thy trm ty =
+let
+  val trm_ty = fastype_of trm
+  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
+in
+  map_types (Envir.subst_type ty_inst) trm
+end
+
 (* builds the aggregate equivalence relation *)
 (* that will be the argument of Respects     *)
 fun mk_resp_arg ctxt (rty, qty) =
@@ -147,15 +156,14 @@
            val SOME qinfo = quotdata_lookup_thy thy s'
            (* FIXME: check in this case that the rty and qty *)
            (* FIXME: correspond to each other *)
-           val (s, _) = dest_Const (#rel qinfo)
-           (* FIXME: the relation should only be the string        *)
-           (* FIXME: and the type needs to be calculated as below; *)
-           (* FIXME: maybe one should actually have a term         *)
-           (* FIXME: and one needs to force it to have this type   *)
+
+           (* we need to instantiate the TVars in the relation *)
+           val thy = ProofContext.theory_of ctxt 
+           val forced_rel = force_typ thy (#rel qinfo) (rty --> rty --> @{typ bool})
          in
-           Const (s, rty --> rty --> @{typ bool})
+           forced_rel
          end
-      | _ => HOLogic.eq_const dummyT 
+      | _ => HOLogic.eq_const rty
              (* FIXME: check that the types correspond to each other? *)
 end
 
diff -r 86c7ed9f354f -r 06e17083e90b Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Wed Dec 23 21:30:23 2009 +0100
+++ b/Quot/quotient_typ.ML	Wed Dec 23 22:42:30 2009 +0100
@@ -156,9 +156,9 @@
 
   (* storing the quot-info *)
   val lthy4 = quotdata_update qty_full_name 
-               (Logic.varifyT Abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3  
-  (* FIXME: varifyT should not be used *)
-  (* FIXME: the relation can be any term, that later maybe needs to be given *)
+               (Logic.varifyT Abs_ty, Logic.varifyT rty, map_types Logic.varifyT rel, equiv_thm) lthy3  
+  (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *)
+  (* FIXME: The relation can be any term, that later maybe needs to be given *)
   (* FIXME: a different type (in regularize_trm); how should this be done?   *)
 in
   lthy4