# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259913673 -3600
# Node ID 8c7597b19f0e9ca71417f6f9b9e669753066d31a
# Parent  6cdba30c6d66dd3e95655cdfe9c7da8f8374510d
First version of the deterministic rep-abs-inj-tac.

diff -r 6cdba30c6d66 -r 8c7597b19f0e FIXME-TODO
--- a/FIXME-TODO	Thu Dec 03 14:02:05 2009 +0100
+++ b/FIXME-TODO	Fri Dec 04 09:01:13 2009 +0100
@@ -16,6 +16,9 @@
 
 
 
+- Handle theorems that include Ball/Bex
+
+
 
 
 
@@ -27,4 +30,4 @@
 - find clean ways how to write down the "mathematical"
   procedure for a possible submission (Peter submitted 
   his work only to TPHOLs 2005...we would have to go
-  maybe for the Journal of Formalised Mathematics)
\ No newline at end of file
+  maybe for the Journal of Formalised Mathematics)
diff -r 6cdba30c6d66 -r 8c7597b19f0e LFex.thy
--- a/LFex.thy	Thu Dec 03 14:02:05 2009 +0100
+++ b/LFex.thy	Fri Dec 04 09:01:13 2009 +0100
@@ -270,7 +270,8 @@
 ML_prf {* PolyML.profiling 1 *}
 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
-apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac' @{context} quot rel_refl trans2 1 *})
+(*apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})*)
 done
 
 (* Does not work:
diff -r 6cdba30c6d66 -r 8c7597b19f0e QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 14:02:05 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:01:13 2009 +0100
@@ -965,6 +965,61 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
 *}
 
+(* A faster version *)
+
+ML {*
+fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) =>
+(case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
+  ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| (Const (@{const_name "op ="},_) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+      => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
+| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| Const (@{const_name "op ="},_) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
+| (Const (@{const_name FUN_REL}, _) $ _ $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
+      => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
+| 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)])
+| _ $ _ $ _ =>
+    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt quot_thms)]
+) i)
+*}
+
+ML {*
+fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+  (FIRST' [
+    inj_repabs_tac_fast ctxt quot_thms trans2,
+    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
+                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+                        quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    NDT ctxt "E" (atac),
+    NDT ctxt "D" (resolve_tac rel_refl),
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+*}
+
+ML {*
+fun all_inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2)
+*}
+
+
+
 section {* Cleaning of the theorem *}