# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260281556 -3600
# Node ID df42285e7286e705794b190686c9139519c2db20
# Parent  88f831f86b9647bceea14fc07dfbc52b5c678a39
trans2 replaced with equals_rsp_tac

diff -r 88f831f86b96 -r df42285e7286 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 13:09:21 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 15:12:36 2009 +0100
@@ -814,6 +814,18 @@
 *}
 
 ML {*
+fun equals_rsp_tac R ctxt =
+  let
+    val t = domain_type (fastype_of R);
+    val thy = ProofContext.theory_of ctxt
+    val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+  in
+    rtac thm THEN' RANGE [quotient_tac ctxt]
+  end
+  handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac
+*}
+
+ML {*
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
@@ -833,7 +845,7 @@
 *}
 
 ML {*
-fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
 (case (bare_concl goal) of
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
@@ -868,11 +880,12 @@
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 
+| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE'
+    (equals_rsp_tac R ctxt THEN' RANGE [
+       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
+
     (* reflexivity of operators arising from Cong_tac *)
-| Const (@{const_name "op ="},_) $ _ $ _ 
-      => rtac @{thm refl} (*ORELSE'
-          (resolve_tac trans2 THEN' RANGE [
-            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*)
+| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl}
 
    (* respectfulness of constants; in particular of a simple relation *)
 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
@@ -888,17 +901,13 @@
 *}
 
 ML {*
-fun inj_repabs_step_tac ctxt rel_refl trans2 =
+fun inj_repabs_step_tac ctxt rel_refl =
   (FIRST' [
-    NDT ctxt "0" (inj_repabs_tac_match ctxt trans2),
+    NDT ctxt "0" (inj_repabs_tac_match ctxt),
     (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
     
     NDT ctxt "A" (apply_rsp_tac ctxt THEN'
                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),
-    
-    (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *)
-    NDT ctxt "B" (resolve_tac trans2 THEN' 
-                 RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
 
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
@@ -921,9 +930,8 @@
 fun inj_repabs_tac ctxt =
 let
   val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
-  val trans2 = map (OF1 @{thm equals_rsp}) (quotient_rules_get ctxt)
 in
-  inj_repabs_step_tac ctxt rel_refl trans2
+  inj_repabs_step_tac ctxt rel_refl
 end
 
 fun all_inj_repabs_tac ctxt =
diff -r 88f831f86b96 -r df42285e7286 Quot/ROOT.ML
--- a/Quot/ROOT.ML	Tue Dec 08 13:09:21 2009 +0100
+++ b/Quot/ROOT.ML	Tue Dec 08 15:12:36 2009 +0100
@@ -2,7 +2,7 @@
 
 no_document use_thys
    ["QuotMain",
-    "Examples/Fset",
+    "Examples/FSet",
     "Examples/IntEx",
     "Examples/IntEx2",
     "Examples/LFex",