# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264578102 -3600
# Node ID 9c3b3eaecaff5f0c78d79cf59e4bf3d0ebdde340
# Parent  62f0344b219c266b6b46ccf652d563a50c775ddf
use of equiv_relation_chk in quotient_term

diff -r 62f0344b219c -r 9c3b3eaecaff FIXME-TODO
--- a/FIXME-TODO	Wed Jan 27 08:20:31 2010 +0100
+++ b/FIXME-TODO	Wed Jan 27 08:41:42 2010 +0100
@@ -1,6 +1,10 @@
 Highest Priority
 ================
 
+- give examples for the new quantifier translations in regularization
+  (quotient_term.ML)
+
+
 Higher Priority
 ===============
 
diff -r 62f0344b219c -r 9c3b3eaecaff Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_def.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,9 @@
+(*  Title:      quotient_def.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Definitions for constants on quotient types.
+
+*)
 
 signature QUOTIENT_DEF =
 sig 
diff -r 62f0344b219c -r 9c3b3eaecaff Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_info.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,11 @@
+(*  Title:      quotient_info.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Data slots for the quotient package.
+
+*)
+
+
 signature QUOTIENT_INFO =
 sig
   exception NotFound
diff -r 62f0344b219c -r 9c3b3eaecaff Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,10 @@
+(*  Title:      quotient_tacs.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Tactics for solving goal arising from lifting
+    theorems to quotient types.
+*)
+
 signature QUOTIENT_TACS =
 sig
   val regularize_tac: Proof.context -> int -> tactic
diff -r 62f0344b219c -r 9c3b3eaecaff Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,11 +1,16 @@
+(*  Title:      quotient_term.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Constructs terms corresponding to goals from
+    lifting theorems to quotient types.
+*)
+
 signature QUOTIENT_TERM =
 sig
   exception LIFT_MATCH of string
 
   datatype flag = absF | repF
 
-  val absrep_const_chk: flag -> Proof.context -> string -> term
-
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
 
@@ -128,9 +133,6 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
-fun absrep_const_chk flag ctxt qty_str =
-  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
-
 fun absrep_match_err ctxt ty_pat ty =
 let
   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
@@ -434,13 +436,14 @@
          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') =>
+  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+     Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(ball)" ctxt resrel needrel
+         then term_mismatch "regularize (Ball)" ctxt resrel needrel
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
@@ -452,13 +455,14 @@
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+     Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(bex)" ctxt resrel needrel
+         then term_mismatch "regularize (Bex)" ctxt resrel needrel
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end
 
@@ -473,20 +477,21 @@
   | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(bex1_res)" ctxt resrel needrel
+         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
          else mk_bexeq $ resrel $ subtrm
        end
 
-  | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+     Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(bex1)" ctxt resrel needrel
+         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
          else mk_bexeq $ resrel $ subtrm
        end
 
@@ -501,7 +506,8 @@
          val rel_ty = fastype_of rel
          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') 
        in
-         if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
+         if rel' aconv rel then rtrm 
+         else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
        end
 
   | (_, Const _) =>
diff -r 62f0344b219c -r 9c3b3eaecaff Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,3 +1,10 @@
+(*  Title:      quotient_typ.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Definition of a quotient type.
+
+*)
+
 signature QUOTIENT_TYPE =
 sig
   val quotient_type: ((string list * binding * mixfix) * (typ * term)) list