--- a/src/HOL/List.thy Sun Jul 29 14:29:50 2007 +0200
+++ b/src/HOL/List.thy Sun Jul 29 14:29:51 2007 +0200
@@ -376,16 +376,16 @@
by (induct xs arbitrary: ys) (case_tac x, auto)+
lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
-apply(rule Eq_FalseI)
-by auto
-
+ by (rule Eq_FalseI) auto
+
+simproc_setup list_neq ("(xs::'a list) = ys") = {*
(*
Reduces xs=ys to False if xs and ys cannot be of the same length.
This is the case if the atomic sublists of one are a submultiset
of those of the other list and there are fewer Cons's in one than the other.
*)
-ML_setup {*
-local
+
+let
fun len (Const("List.list.Nil",_)) acc = acc
| len (Const("List.list.Cons",_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
@@ -394,8 +394,9 @@
| len (Const("List.map",_) $ _ $ xs) acc = len xs acc
| len t (ts,n) = (t::ts,n);
-fun list_eq ss (Const(_,eqT) $ lhs $ rhs) =
+fun list_neq _ ss ct =
let
+ val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
fun prove_neq() =
let
@@ -411,15 +412,7 @@
n < m andalso submultiset (op aconv) (rs,ls)
then prove_neq() else NONE
end;
-
-in
-
-val list_neq_simproc =
- Simplifier.simproc @{theory} "list_neq" ["(xs::'a list) = ys"] (K list_eq);
-
-end;
-
-Addsimprocs [list_neq_simproc];
+in list_neq end;
*}