# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260622441 -3600
# Node ID 33cd648df179913428abb9216d8f79fd0a20034c
# Parent  e16523f01908fe7e2d74d745dcb4de396f1e247d# Parent  8d5408322de50529b6f0a52ed7e981d6bc0d01f5
merged

diff -r 8d5408322de5 -r 33cd648df179 Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Sat Dec 12 09:27:06 2009 +0100
+++ b/Quot/Examples/LFex.thy	Sat Dec 12 13:54:01 2009 +0100
@@ -259,7 +259,7 @@
 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 ()))) *}
 *)
-done
+ done
 
 (* Does not work:
 lemma
diff -r 8d5408322de5 -r 33cd648df179 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Dec 12 09:27:06 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 13:54:01 2009 +0100
@@ -286,12 +286,14 @@
        in 
          if rel' = rel then rtrm else raise exc
        end  
+
   | (_, Const (s, Type(st, _))) =>
        let 
          fun same_name (Const (s, _)) (Const (s', _)) = (s = s')
            | same_name _ _ = false
        in
-         (* TODO/FIXME: This test is not enough *)
+         (* TODO/FIXME: This test is not enough. *) 
+         (*             Why?                     *)
          if same_name rtrm qtrm then rtrm
          else 
            let 
@@ -300,11 +302,8 @@
              val thy = ProofContext.theory_of lthy
              val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
            in 
-             if Pattern.matches thy (rtrm', rtrm) then rtrm else
-               let
-                 val _ = tracing ("rtrm := " ^ Syntax.string_of_term @{context} rtrm);
-                 val _ = tracing ("rtrm':= " ^ Syntax.string_of_term @{context} rtrm');
-               in raise exc2 end
+             if Pattern.matches thy (rtrm', rtrm) 
+             then rtrm else raise exc2
            end
        end 
 
@@ -320,8 +319,11 @@
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
   | (rt, qt) =>
-       let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in
-       raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))
+       let 
+         val rts = Syntax.string_of_term lthy rt
+         val qts = Syntax.string_of_term lthy qt
+       in
+         raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))
        end
 *}
 
@@ -395,7 +397,15 @@
   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 by (simp add: equivp_reflp)
 
-(* Regularize Tactic *)
+ML {*
+fun quotient_tac ctxt =
+  REPEAT_ALL_NEW (FIRST'
+    [rtac @{thm identity_quotient},
+     resolve_tac (quotient_rules_get ctxt)])
+
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
 
 (* 0. preliminary simplification step according to *)
 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
@@ -405,22 +415,12 @@
 (* 2. monos *)
 (* 3. commutation rules for ball and bex *)
 thm ball_all_comm bex_ex_comm
-(* 4. then rel-equality (which need to be instantiated to avoid loops *)
+(* 4. then rel-equality (which need to be instantiated to avoid loops) *)
 thm eq_imp_rel
 (* 5. then simplification like 0 *)
 (* finally jump back to 1 *)
 
 ML {*
-fun quotient_tac ctxt =
-  REPEAT_ALL_NEW (FIRST'
-    [rtac @{thm identity_quotient},
-     resolve_tac (quotient_rules_get ctxt)])
-
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun regularize_tac ctxt =
 let
   val thy = ProofContext.theory_of ctxt
@@ -517,8 +517,6 @@
 
   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
-    (* FIXME: check here that rtrm is the corresponding definition for the const *)
-    (* Hasn't it already been checked in regularize? *)
   | (_, Const (_, T')) =>
       let
         val rty = fastype_of rtrm
@@ -858,7 +856,7 @@
 ML {*
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-   ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+   (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
      (let
        val thy = ProofContext.theory_of ctxt
        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
@@ -914,7 +912,8 @@
 (*    and simplification with                          *)
 thm babs_prs all_prs ex_prs 
 (* 2. unfolding of ---> in front of everything, except *)
-(*    bound variables                                  *)
+(*    bound variables (this prevents lambda_prs from   *)
+(*    becoming stuck                                   *)
 thm fun_map.simps
 (* 3. simplification with *)
 thm lambda_prs