diff -r 566f47250bd0 -r 26c9a7c0b36b src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Sep 03 16:40:02 1998 +0200
+++ b/src/HOL/List.ML	Fri Sep 04 11:01:59 1998 +0200
@@ -246,6 +246,63 @@
 qed "append_eq_appendI";
 
 
+(***
+Simplification procedure for all list equalities.
+Currently only tries to rearranges @ to see if
+- both lists end in a singleton list,
+- or both lists end in the same list.
+***)
+local
+
+val list_eq_pattern =
+  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
+
+fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
+      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
+  | last (Const("List.op @",_) $ _ $ ys) = last ys
+  | last t = t;
+
+fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
+  | list1 _ = false;
+
+fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
+      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
+  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
+  | butlast xs = Const("List.list.[]",fastype_of xs);
+
+val rearr_tac =
+  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
+
+fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+  let
+    val lastl = last lhs and lastr = last rhs
+    fun rearr conv =
+      let val lhs1 = butlast lhs and rhs1 = butlast rhs
+          val Type(_,listT::_) = eqT
+          val appT = [listT,listT] ---> listT
+          val app = Const("List.op @",appT)
+          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
+          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
+          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
+            handle ERROR =>
+            error("The error(s) above occurred while trying to prove " ^
+                  string_of_cterm ct)
+      in Some((conv RS (thm RS trans)) RS eq_reflection) end
+
+  in if list1 lastl andalso list1 lastr
+     then rearr append1_eq_conv
+     else
+     if lastl aconv lastr
+     then rearr append_same_eq
+     else None
+  end;
+in
+val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
+end;
+
+Addsimprocs [list_eq_simproc];
+
+
 (** map **)
 
 section "map";
@@ -827,27 +884,59 @@
 
 (** upto **)
 
-Goal "!i j. ~ j < i --> j - i < Suc j - i";
-by(strip_tac 1);
-br diff_less_Suc_diff 1;
-be leI 1;
-val lemma = result();
+(* Does not terminate! *)
+Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
+by(induct_tac "j" 1);
+by Auto_tac;
+by(REPEAT(trans_tac 1));
+qed "upt_rec";
 
-Goalw [upto_def] "j<i ==> [i..j] = []";
+Goal "j<=i ==> [i..j(] = []";
+by(stac upt_rec 1);
+by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+qed "upt_conv_Nil";
+Addsimps [upt_conv_Nil];
+
+Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";
+by (Asm_simp_tac 1);
+qed "upt_Suc";
+
+Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
 br trans 1;
-brs paired_upto.rules 1;
-br lemma 1;
-by(Asm_simp_tac 1);
-qed "upto_conv_Nil";
+by(stac upt_rec 1);
+br refl 2;
+by (Asm_simp_tac 1);
+qed "upt_conv_Cons";
+
+Goal "length [i..j(] = j-i";
+by(induct_tac "j" 1);
+ by (Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
+qed "length_upt";
+Addsimps [length_upt];
 
-Goalw [upto_def] "i<=j ==> [i..j] = i#[Suc i..j]";
-br trans 1;
-brs paired_upto.rules 1;
-br lemma 1;
-by(asm_simp_tac (simpset() addsimps [leD]) 1);
-qed "upto_conv_Cons";
+Goal "i+k < j --> [i..j(] ! k = i+k";
+by(induct_tac "j" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps ([nth_append,less_diff_conv]@add_ac)
+                           addSolver cut_trans_tac) 1);
+br conjI 1;
+ by(Clarify_tac 1);
+ bd add_lessD1 1;
+ by(trans_tac 1);
+by(Clarify_tac 1);
+br conjI 1;
+ by(Clarify_tac 1);
+ by(subgoal_tac "n=i+k" 1);
+  by(Asm_full_simp_tac 1);
+ by(trans_tac 1);
+by(Clarify_tac 1);
+by(subgoal_tac "n=i+k" 1);
+ by(Asm_full_simp_tac 1);
+by(trans_tac 1);
+qed_spec_mp "nth_upt";
+Addsimps [nth_upt];
 
-Addsimps [upto_conv_Nil,upto_conv_Cons];
 
 (** nodups & remdups **)
 section "nodups & remdups";
@@ -973,60 +1062,3 @@
 by (Blast_tac 1);
 qed "Cons_in_lex";
 AddIffs [Cons_in_lex];
-
-
-(***
-Simplification procedure for all list equalities.
-Currently only tries to rearranges @ to see if
-- both lists end in a singleton list,
-- or both lists end in the same list.
-***)
-local
-
-val list_eq_pattern =
-  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
-
-fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
-      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
-  | last (Const("List.op @",_) $ _ $ ys) = last ys
-  | last t = t;
-
-fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
-  | list1 _ = false;
-
-fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
-      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
-  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
-  | butlast xs = Const("List.list.[]",fastype_of xs);
-
-val rearr_tac =
-  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
-
-fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
-  let
-    val lastl = last lhs and lastr = last rhs
-    fun rearr conv =
-      let val lhs1 = butlast lhs and rhs1 = butlast rhs
-          val Type(_,listT::_) = eqT
-          val appT = [listT,listT] ---> listT
-          val app = Const("List.op @",appT)
-          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
-          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
-          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
-            handle ERROR =>
-            error("The error(s) above occurred while trying to prove " ^
-                  string_of_cterm ct)
-      in Some((conv RS (thm RS trans)) RS eq_reflection) end
-
-  in if list1 lastl andalso list1 lastr
-     then rearr append1_eq_conv
-     else
-     if lastl aconv lastr
-     then rearr append_same_eq
-     else None
-  end;
-in
-val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
-end;
-
-Addsimprocs [list_eq_simproc];