# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264055914 -3600
# Node ID a394c73379664120245e20a7255c1852aee3a25c
# Parent  51e5cc3793d273280bc4d77102fb78fdf3994d23
Ex1 -> Bex1 Regularization, Preparing Exeq.

diff -r 51e5cc3793d2 -r a394c7337966 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Jan 20 16:50:31 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 21 07:38:34 2010 +0100
@@ -323,6 +323,17 @@
   (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
+| Const (@{const_name "op ="},_) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      rtac @{thm bex1_rsp} THEN' dtac @{thm QT_ex1}
+
+(* TODO: Check why less _ are needed then in EX/ALL cases *)
+| (Const (@{const_name fun_rel}, _) $ _ $ _) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _)) $
+    (Const(@{const_name Bex1},_) $ (Const (@{const_name Respects}, _) $ _))
+      rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+
     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
 | (Const (@{const_name "op ="},_) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
diff -r 51e5cc3793d2 -r a394c7337966 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Wed Jan 20 16:50:31 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 21 07:38:34 2010 +0100
@@ -366,6 +366,7 @@
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
+val mk_bex1 = Const (@{const_name Bex1}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 
 (* - applies f to the subterm of an abstraction, 
@@ -460,6 +461,24 @@
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end
 
+  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
+       in
+         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
+         else mk_bex1 $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
+       end
+
+  | (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'))
+       in
+         if resrel <> needrel
+         then term_mismatch "regularize(bex1)" ctxt resrel needrel
+         else mk_bex1 $ (mk_resp $ resrel) $ subtrm
+       end
+
   | (* equalities need to be replaced by appropriate equivalence relations *) 
     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
          if ty = ty' then rtrm