# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1262696944 -3600
# Node ID a5495a323b49fa2f8ab0e62acb5fcac94cc738fe
# Parent  43336511993f8f6d563e50bf5658ec779503617f
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)

diff -r 43336511993f -r a5495a323b49 Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Tue Jan 05 10:41:20 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Tue Jan 05 14:09:04 2010 +0100
@@ -11,7 +11,10 @@
    |> writeln;
    equiv_relation_chk ctxt (rty, qty) 
    |> Syntax.string_of_term ctxt
-   |> writeln)  
+   |> writeln;
+   new_equiv_relation_chk ctxt (rty, qty) 
+   |> Syntax.string_of_term ctxt
+   |> writeln)
 *}
 
 definition
@@ -81,6 +84,12 @@
 
 ML {*
 test_funs absF @{context} 
+     (@{typ "('a list)"}, 
+      @{typ "('a fset)"})
+*}
+
+ML {*
+test_funs absF @{context} 
      (@{typ "('a list) list"}, 
       @{typ "('a fset) fset"})
 *}
diff -r 43336511993f -r a5495a323b49 Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Tue Jan 05 10:41:20 2010 +0100
+++ b/Quot/QuotScript.thy	Tue Jan 05 14:09:04 2010 +0100
@@ -1,5 +1,5 @@
 theory QuotScript
-imports Plain ATP_Linkup
+imports Plain ATP_Linkup Predicate
 begin
 
 definition
diff -r 43336511993f -r a5495a323b49 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Tue Jan 05 10:41:20 2010 +0100
+++ b/Quot/quotient_term.ML	Tue Jan 05 14:09:04 2010 +0100
@@ -7,6 +7,9 @@
    val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
    val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
 
+   val new_equiv_relation: Proof.context -> (typ * typ) -> term
+   val new_equiv_relation_chk: Proof.context -> (typ * typ) -> term
+
    val equiv_relation: Proof.context -> (typ * typ) -> term
    val equiv_relation_chk: Proof.context -> (typ * typ) -> term
 
@@ -39,7 +42,7 @@
 
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-fun mk_compose flag (trm1, trm2) = 
+fun mk_fun_compose flag (trm1, trm2) = 
   case flag of
     absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
   | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
@@ -184,7 +187,7 @@
              val map_fun = mk_mapfun ctxt vs rty_pat       
              val result = list_comb (map_fun, args) 
            in
-             mk_compose flag (absrep_const flag ctxt s', result)
+             mk_fun_compose flag (absrep_const flag ctxt s', result)
            end 
     | (TFree x, TFree x') =>
         if x = x'
@@ -212,6 +215,9 @@
   map_types (Envir.subst_type ty_inst) trm
 end
 
+fun mk_rel_compose (trm1, trm2) = 
+  Const (@{const_name "pred_comp"}, dummyT) $ trm1 $ trm2
+
 fun get_relmap ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
@@ -221,6 +227,20 @@
   Const (relmap, dummyT)
 end
 
+fun mk_relmap ctxt vs rty =
+let
+  val vs' = map (mk_Free) vs
+
+  fun mk_relmap_aux rty =
+    case rty of
+      TVar _ => mk_Free rty
+    | Type (_, []) => HOLogic.eq_const rty
+    | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
+    | _ => raise LIFT_MATCH ("mk_relmap (default)")
+in
+  fold_rev Term.lambda vs' (mk_relmap_aux rty)
+end
+
 fun get_equiv_rel ctxt s =
 let
   val thy = ProofContext.theory_of ctxt
@@ -233,6 +253,42 @@
 (* that will be the argument of Respects     *)
 
 (* FIXME: check that the types correspond to each other *)
+fun new_equiv_relation ctxt (rty, qty) =
+  if rty = qty
+  then HOLogic.eq_const rty
+  else
+    case (rty, qty) of
+      (Type (s, tys), Type (s', tys')) =>
+       if s = s' 
+       then 
+         let
+           val args = map (new_equiv_relation ctxt) (tys ~~ tys')
+         in
+           list_comb (get_relmap ctxt s, args) 
+         end  
+       else 
+         let
+           val thy = ProofContext.theory_of ctxt
+           val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+           val rtyenv = Sign.typ_match thy (rty_pat, rty) Vartab.empty
+                        handle MATCH_TYPE => absrep_match_err ctxt rty_pat rty
+           val qtyenv = Sign.typ_match thy (qty_pat, qty) Vartab.empty
+                        handle MATCH_TYPE => absrep_match_err ctxt qty_pat qty 
+           val args_aux = map (double_lookup rtyenv qtyenv) vs 
+           val args = map (new_equiv_relation ctxt) args_aux
+           val rel_map = mk_relmap ctxt vs rty_pat       
+           val result = list_comb (rel_map, args)
+           val eqv_rel = get_equiv_rel ctxt s'
+           val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
+         in
+           mk_rel_compose (eqv_rel', result)
+         end  
+      | _ => HOLogic.eq_const rty
+
+fun new_equiv_relation_chk ctxt (rty, qty) =
+  new_equiv_relation ctxt (rty, qty)
+  |> Syntax.check_term ctxt
+
 fun equiv_relation ctxt (rty, qty) =
   if rty = qty
   then HOLogic.eq_const rty