--- 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' =>