# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260668134 -3600
# Node ID 8437359e811c382fef2e94c11c248b9a635aa0fa
# Parent  d151f24427ab6ccc31ac1c1699f0c72d469a8a45
another pass on apply_rsp

diff -r d151f24427ab -r 8437359e811c Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sun Dec 13 01:56:19 2009 +0100
+++ b/Quot/QuotMain.thy	Sun Dec 13 02:35:34 2009 +0100
@@ -559,20 +559,19 @@
 
 ML {*
 fun find_qt_asm asms =
-  let
-    fun find_fun trm =
-      case trm of
-        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
-      | _ => false
-  in
-    case find_first find_fun asms of
-      SOME (_ $ (_ $ (f $ a))) => (f, a)
-    | SOME _ => error "find_qt_asm: no pair"
-    | NONE => error "find_qt_asm: no assumption"
-  end
+let
+  fun find_fun trm =
+    case trm of
+      (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+    | _ => false
+in
+ case find_first find_fun asms of
+   SOME (_ $ (_ $ (f $ a))) => SOME (f, a)
+ | _ => NONE
+end
 *}
 
-(*
+text {*
 To prove that the regularised theorem implies the abs/rep injected, 
 we try:
 
@@ -592,8 +591,7 @@
     (not sure if it is still needed?)
  D) unfolding lambda on one side
  E) simplifying (= ===> =) for simpler respectfulness
-
-*)
+*}
 
 lemma quot_true_dests:
   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
@@ -661,33 +659,33 @@
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 *}
 
-thm apply_rsp
+ML {*
+(* FIXME / TODO: what is asmf and asma in the code below *)
 
-ML {*
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
-    case (HOLogic.dest_Trueprop (term_of concl)) of
-      (R2 $ (f $ x) $ (g $ y)) =>
-        (let
-           val (asmf, asma) = find_qt_asm (map term_of asms)
-         in
-           if (fastype_of asmf) = (fastype_of f) 
-           then no_tac 
-           else 
-             let
-               val ty_a = fastype_of x
-               val ty_b = fastype_of asma
-               val ty_c = range_type (fastype_of f) 
-               val thy = ProofContext.theory_of context
-               val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]
-               val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
-               val thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
-             in
-               (rtac thm THEN' quotient_tac context) 1
-             end
-         end
-        handle ERROR "find_qt_asm: no pair" => no_tac)
-    | _ => no_tac)
+  let
+    val bare_concl = HOLogic.dest_Trueprop (term_of concl)
+    val qt_asm = find_qt_asm (map term_of asms)
+  in
+    case (bare_concl, qt_asm) of
+      (R2 $ (f $ x) $ (g $ y), SOME (asmf, asma)) =>
+         if (fastype_of asmf) = (fastype_of f) 
+         then no_tac 
+         else 
+           let
+             val ty_x = fastype_of x
+             val ty_b = fastype_of asma
+             val ty_f = range_type (fastype_of f) 
+             val thy = ProofContext.theory_of context
+             val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f]
+             val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
+             val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
+           in
+             (rtac inst_thm THEN' quotient_tac context) 1
+           end
+    | _ => no_tac
+  end)
 *}
 
 ML {*