# HG changeset patch
# User wenzelm
# Date 1301512068 -7200
# Node ID a7570c66d74606b62683b0ae5cdb44583c0630c7
# Parent  3164e7263b53cd82c7efc540ef5fece9bc279605
inline lemmas instead of accidental physical addressing -- explicit is better than implicit;

diff -r 3164e7263b53 -r a7570c66d746 src/HOL/Tools/list_to_set_comprehension.ML
--- a/src/HOL/Tools/list_to_set_comprehension.ML	Wed Mar 30 20:21:40 2011 +0200
+++ b/src/HOL/Tools/list_to_set_comprehension.ML	Wed Mar 30 21:07:48 2011 +0200
@@ -51,7 +51,7 @@
 
 fun conjunct_assoc_conv ct =
   Conv.try_conv
-    ((rewr_conv' @{thm conj_assoc}) then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
+    (rewr_conv' @{thm conj_assoc} then_conv conj_conv Conv.all_conv conjunct_assoc_conv) ct
 
 fun right_hand_set_comprehension_conv conv ctxt =
   Trueprop_conv (eq_conv Conv.all_conv
@@ -107,7 +107,7 @@
       end
     (* returns condition continuing term option *)
     fun dest_if (Const (@{const_name If}, _) $ cond $ then_t $ Const (@{const_name Nil}, _)) =
-        SOME (cond, then_t)
+          SOME (cond, then_t)
       | dest_if _ = NONE
     fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
       | tac ctxt (If :: cont) =
@@ -117,13 +117,14 @@
           THEN Subgoal.FOCUS (fn {prems, context, ...} =>
             CONVERSION (right_hand_set_comprehension_conv (K
               (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
-               then_conv rewr_conv' @{thm simp_thms(22)})) context) 1) ctxt 1
+               then_conv
+               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
           THEN tac ctxt cont
           THEN rtac @{thm impI} 1
           THEN Subgoal.FOCUS (fn {prems, context, ...} =>
               CONVERSION (right_hand_set_comprehension_conv (K
                 (conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
-                 then_conv rewr_conv' @{thm simp_thms(24)})) context) 1) ctxt 1
+                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
           THEN rtac set_Nil_I 1
       | tac ctxt (Case (T, i) :: cont) =
           let
@@ -148,22 +149,26 @@
                     then_conv (Trueprop_conv (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
                       Conv.repeat_conv
                         (all_but_last_exists_conv
-                          (K (rewr_conv' @{thm simp_thms(39)})) ctxt)) context)))) 1) ctxt 1
+                          (K (rewr_conv'
+                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
                 THEN tac ctxt cont
               else
                 Subgoal.FOCUS (fn {prems, context, ...} =>
-                  CONVERSION ((right_hand_set_comprehension_conv (K
-                    (conj_conv
-                      ((eq_conv Conv.all_conv
-                        (rewr_conv' (List.last prems))) then_conv
-                        (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
-                      Conv.all_conv then_conv
-                      (rewr_conv' @{thm simp_thms(24)}))) context) then_conv
-                      (Trueprop_conv
-                        (eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
-                          Conv.repeat_conv
-                            (Conv.bottom_conv
-                              (K (rewr_conv' @{thm simp_thms(36)})) ctxt)) context)))) 1) ctxt 1
+                  CONVERSION
+                    (right_hand_set_comprehension_conv (K
+                      (conj_conv
+                        ((eq_conv Conv.all_conv
+                          (rewr_conv' (List.last prems))) then_conv
+                          (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))
+                        Conv.all_conv then_conv
+                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
+                      Trueprop_conv
+                        (eq_conv Conv.all_conv
+                          (Collect_conv (fn (_, ctxt) =>
+                            Conv.repeat_conv
+                              (Conv.bottom_conv
+                                (K (rewr_conv'
+                                  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
                 THEN rtac set_Nil_I 1)) (#case_rewrites info))
           end
     fun make_inner_eqs bound_vs Tis eqs t =