# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260511111 -3600
# Node ID 8b2c46e116742c81aa154665e68710a8c2ba6bfa
# Parent  b89b578d15e6e5d3a360dde0f820646ba14816a4
reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case

diff -r b89b578d15e6 -r 8b2c46e11674 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 19:05:56 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 06:58:31 2009 +0100
@@ -1002,23 +1002,19 @@
 
 (* - A is the original raw theorem                       *)
 (* - B is the regularized theorem                        *)
-(* - C is the rep/abs injected version of B              *) 
+(* - C is the rep/abs injected version of B              *)
 (* - D is the lifted theorem                             *)
 (*                                                       *)
-(* - b is the regularization step                        *)
-(* - c is the rep/abs injection step                     *)
-(* - d is the cleaning part                              *)
+(* - 1st prem is the regularization step                 *)
+(* - 2nd prem is the rep/abs injection step              *)
+(* - 3rd prem is the cleaning part                       *)
 (*                                                       *)
-(* the QUOT_TRUE premise in c records the lifted theorem *)
+(* the QUOT_TRUE premise in 2 records the lifted theorem *)
 
-lemma lifting_procedure:
-  assumes a: "A"
-  and     b: "A \<longrightarrow> B"
-  and     c: "QUOT_TRUE D \<Longrightarrow> B = C"
-  and     d: "C = D"
-  shows   "D"
-using a b c d
-by (simp add: QUOT_TRUE_def)
+ML {*
+  val lifting_procedure = 
+    @{lemma  "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)}
+*}
 
 ML {*
 fun lift_match_error ctxt fun_str rtrm qtrm =
@@ -1049,7 +1045,7 @@
     [SOME (cterm_of thy rtrm'),
      SOME (cterm_of thy reg_goal),
      NONE,
-     SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
+     SOME (cterm_of thy inj_goal)] lifting_procedure
 end
 *}
 
@@ -1072,6 +1068,7 @@
 ML {*
 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
 
+(* prints warning, if goal is unsolved *)
 fun WARN (tac, msg) i st =
  case Seq.pull ((SOLVES' tac) i st) of
      NONE    => (warning msg; Seq.single st)
@@ -1081,12 +1078,25 @@
 *}
 
 ML {*
+local
+
+val msg1 = "Regularize proof failed."
+val msg2 = cat_lines ["Injection proof failed.", 
+                      "This is probably due to missing respects lemmas.",
+                      "Try invoking the injection_tac manually to see", 
+                      "which lemmas are missing."]
+val msg3 = "Cleaning proof failed."
+
+in
+
 fun lift_tac ctxt rthm =
   procedure_tac ctxt rthm
   THEN' RANGE_WARN 
-     [(regularize_tac ctxt,     "Regularize proof failed."),
-      (all_inj_repabs_tac ctxt, "Injection proof failed."),
-      (clean_tac ctxt,          "Cleaning proof failed.")]
+     [(regularize_tac ctxt, msg1),
+      (all_inj_repabs_tac ctxt, msg2),
+      (clean_tac ctxt, msg3)]
+
+end
 *}
 
 section {* Methods / Interface *}