src/HOL/List.thy

 
 (* conversion *)
 
 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)
 
 fun conjunct_assoc_conv ct =

     (Collect_conv (all_exists_conv conv o #2) ctxt))
 
 
 (* 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 *)
     fun possible_index_of_singleton_case cases =
       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
       end
     (* returns (case_expr type index chosen_case constr_name) option  *)

           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_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
             val SOME {injects, distincts, case_thms, split, ...} =
               Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))

                         then_conv conjunct_assoc_conv)) context
                     then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>
                       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, ...} =>
                   CONVERSION
                     (right_hand_set_comprehension_conv (K
                       (HOLogic.conj_conv
                         ((HOLogic.eq_conv Conv.all_conv
                           (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 =
       (case dest_case t of
         SOME (x, T, i, cont, constr_name) =>

             SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont
           | NONE =>
             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' =>
                       Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $
                         Bound (length bound_vs) $ t'