# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259381362 -3600
# Node ID 5b298c42f6c8cdfa016e1e632416a7361c8fb529
# Parent  123877af04edc55cd89f40b55a57fa0031f7f15b
more tuning of the repabs-tactics

diff -r 123877af04ed -r 5b298c42f6c8 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 04:46:03 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 05:09:22 2009 +0100
@@ -713,7 +713,7 @@
 using a by (simp add: FUN_REL.simps)
 
 ML {*
-val LAMBDA_RES_TAC2 =
+val LAMBDA_RES_TAC =
   Subgoal.FOCUS (fn {concl, ...} =>
     case (term_of concl) of
        (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1
@@ -721,7 +721,7 @@
 *}
 
 ML {*
-val WEAK_LAMBDA_RES_TAC2 =
+val WEAK_LAMBDA_RES_TAC =
   Subgoal.FOCUS (fn {concl, ...} =>
     case (term_of concl) of
        (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1
@@ -741,52 +741,47 @@
 ML {*
 fun APPLY_RSP_TAC rty = 
   Subgoal.FOCUS (fn {concl, ...} =>
-  let
-    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
-    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
-    val insts = Thm.match (pat, concl)
-  in
-    if needs_lift rty (type_of f) then
-      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-    else no_tac
-  end
-  handle _ => no_tac)
+    case (term_of concl) of
+       (_ $ (R $ (f $ _) $ (_ $ _))) =>
+          let
+            val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+            val insts = Thm.match (pat, concl)
+          in
+            if needs_lift rty (fastype_of f) 
+            then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+            else no_tac
+          end
+     | _ => no_tac)
 *}
 
 ML {*
 val ball_rsp_tac = 
   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
-                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-    THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      |_ => no_tac)
 *}
 
 ML {*
 val bex_rsp_tac = 
   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
-                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-    THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
+     case (term_of concl) of
+        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) =>
+            ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+            THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+            THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+            (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+      | _ => no_tac)
 *}
 
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
-           LAMBDA_RES_TAC2 ctxt,
+           LAMBDA_RES_TAC ctxt,
            rtac @{thm RES_FORALL_RSP},
            ball_rsp_tac ctxt,
            rtac @{thm RES_EXISTS_RSP},
@@ -802,7 +797,7 @@
            resolve_tac rel_refl,
            atac,
            SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
-           WEAK_LAMBDA_RES_TAC2 ctxt,
+           WEAK_LAMBDA_RES_TAC ctxt,
            CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))])
 
 fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
@@ -842,7 +837,7 @@
     DT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    DT ctxt "2" (LAMBDA_RES_TAC2 ctxt),
+    DT ctxt "2" (LAMBDA_RES_TAC ctxt),
 
     (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
@@ -879,38 +874,13 @@
     DT ctxt "E" (atac),
 
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
-    DT ctxt "G" (WEAK_LAMBDA_RES_TAC2 ctxt),
+    DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
     DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
 
 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
-ML {*
-fun get_inj_repabs_tac ctxt rel lhs rhs =
-let
-  val _ = tracing "input"
-  val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
-  val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
-  val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
-in  
-  case (rel, lhs, rhs) of
-    (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
-      => rtac @{thm REP_ABS_RSP(1)}
-  | (_, Const (@{const_name "Ball"}, _) $ _, 
-        Const (@{const_name "Ball"}, _) $ _)
-      => rtac @{thm RES_FORALL_RSP}
-  | _ => K no_tac
-end
-*}
-
-ML {* 
-fun inj_repabs_tac ctxt =
-  SUBGOAL (fn (goal, i) =>
-     (case (HOLogic.dest_Trueprop goal) of
-        (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
-      | _ => K no_tac) i)
-*}
 
 section {* Cleaning of the theorem *}