# HG changeset patch
# User wenzelm
# Date 1430342771 -7200
# Node ID 76853162a87e2c383f01f5ea2663454fa0dca2cb
# Parent  91477b3a2d6b6656fb54fc6e89c2234259787faa
tuned;

diff -r 91477b3a2d6b -r 76853162a87e src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/List.thy	Wed Apr 29 23:26:11 2015 +0200
@@ -539,19 +539,19 @@
 
 fun all_exists_conv cv ctxt ct =
   (case Thm.term_of ct of
-    Const (@{const_name HOL.Ex}, _) $ Abs _ =>
+    Const (@{const_name Ex}, _) $ Abs _ =>
       Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct
   | _ => cv ctxt ct)
 
 fun all_but_last_exists_conv cv ctxt ct =
   (case Thm.term_of ct of
-    Const (@{const_name HOL.Ex}, _) $ Abs (_, _, Const (@{const_name HOL.Ex}, _) $ _) =>
+    Const (@{const_name Ex}, _) $ Abs (_, _, Const (@{const_name Ex}, _) $ _) =>
       Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct
   | _ => cv ctxt ct)
 
 fun Collect_conv cv ctxt ct =
   (case Thm.term_of ct of
-    Const (@{const_name Set.Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
+    Const (@{const_name Collect}, _) $ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct
   | _ => raise CTERM ("Collect_conv", [ct]))
 
 fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)
@@ -567,18 +567,17 @@
 
 (* term abstraction of list comprehension patterns *)
 
-datatype termlets = If | Case of (typ * int)
+datatype termlets = If | Case of typ * int
 
 fun simproc ctxt redex =
   let
-    val set_Nil_I = @{thm trans} OF [@{thm list.set(1)}, @{thm empty_def}]
+    val set_Nil_I = @{lemma "set [] = {x. False}" by (simp add: empty_def [symmetric])}
     val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}
     val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}
-    val del_refl_eq = @{lemma "(t = t & P) == P" by simp}
-    fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)
-    fun dest_set (Const (@{const_name List.set}, _) $ xs) = xs
-    fun dest_singleton_list (Const (@{const_name List.Cons}, _)
-          $ t $ (Const (@{const_name List.Nil}, _))) = t
+    val del_refl_eq = @{lemma "(t = t \<and> P) \<equiv> P" by simp}
+    fun mk_set T = Const (@{const_name set}, HOLogic.listT T --> HOLogic.mk_setT T)
+    fun dest_set (Const (@{const_name set}, _) $ xs) = xs
+    fun dest_singleton_list (Const (@{const_name Cons}, _) $ t $ (Const (@{const_name Nil}, _))) = t
       | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])
     (* We check that one case returns a singleton list and all other cases
        return [], and return the index of the one singleton list case *)
@@ -586,7 +585,7 @@
       let
         fun check (i, case_t) s =
           (case strip_abs_body case_t of
-            (Const (@{const_name List.Nil}, _)) => s
+            (Const (@{const_name Nil}, _)) => s
           | _ => (case s of SOME NONE => SOME (SOME i) | _ => NONE))
       in
         fold_index check cases (SOME NONE) |> the_default NONE
@@ -624,13 +623,13 @@
             CONVERSION (right_hand_set_comprehension_conv (K
               (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv
                then_conv
-               rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1
+               rewr_conv' @{lemma "(True \<and> 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
                 (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv
-                 then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1
+                 then_conv rewr_conv' @{lemma "(False \<and> P) = False" by simp})) context) 1) ctxt 1
           THEN rtac set_Nil_I 1
       | tac ctxt (Case (T, i) :: cont) =
           let
@@ -657,7 +656,7 @@
                       Conv.repeat_conv
                         (all_but_last_exists_conv
                           (K (rewr_conv'
-                            @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
+                            @{lemma "(\<exists>x. x = t \<and> P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1
                 THEN tac ctxt cont
               else
                 Subgoal.FOCUS (fn {prems, context, ...} =>
@@ -668,14 +667,14 @@
                           (rewr_conv' (List.last prems))) then_conv
                           (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) distincts)))
                         Conv.all_conv then_conv
-                        (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv
+                        (rewr_conv' @{lemma "(False \<and> P) = False" by simp}))) context then_conv
                       HOLogic.Trueprop_conv
                         (HOLogic.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
+                                  @{lemma "(\<exists>x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1
                 THEN rtac set_Nil_I 1)) case_thms)
           end
     fun make_inner_eqs bound_vs Tis eqs t =
@@ -699,7 +698,7 @@
             if eqs = [] then NONE (* no rewriting, nothing to be done *)
             else
               let
-                val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)
+                val Type (@{type_name list}, [rT]) = fastype_of1 (map snd bound_vs, t)
                 val pat_eq =
                   (case try dest_singleton_list t of
                     SOME t' =>