# HG changeset patch
# User paulson
# Date 963578835 -7200
# Node ID 9ae89b9ce20687d52f9b726446fe1bdeb6e8438d
# Parent  5d9f02e7556900519288ca896edfe9f39728122d
moved sublist from UNITY/AllocBase to List

diff -r 5d9f02e75569 -r 9ae89b9ce206 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jul 14 14:46:35 2000 +0200
+++ b/src/HOL/List.ML	Fri Jul 14 14:47:15 2000 +0200
@@ -1439,6 +1439,55 @@
 AddIffs [Cons_in_lex];
 
 
+(*** sublist (a generalization of nth to sets) ***)
+
+Goalw [sublist_def] "sublist l {} = []";
+by Auto_tac;
+qed "sublist_empty";
+
+Goalw [sublist_def] "sublist [] A = []";
+by Auto_tac;
+qed "sublist_nil";
+
+Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
+\     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
+by (res_inst_tac [("xs","xs")] rev_induct 1);
+ by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
+by (Simp_tac 1);
+qed "sublist_shift_lemma";
+
+Goalw [sublist_def]
+     "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
+by (res_inst_tac [("xs","l'")] rev_induct 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
+	                              zip_append, sublist_shift_lemma]) 1);
+by (asm_simp_tac (simpset() addsimps [add_commute]) 1);
+qed "sublist_append";
+
+Addsimps [sublist_empty, sublist_nil];
+
+Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
+by (res_inst_tac [("xs","l")] rev_induct 1);
+ by (asm_simp_tac (simpset() delsimps [append_Cons]
+	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
+by (simp_tac (simpset() addsimps [sublist_def]) 1);
+qed "sublist_Cons";
+
+Goal "sublist [x] A = (if 0 : A then [x] else [])";
+by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
+qed "sublist_singleton";
+Addsimps [sublist_singleton];
+
+Goal "sublist l {..n(} = take n l";
+by (res_inst_tac [("xs","l")] rev_induct 1);
+ by (asm_simp_tac (simpset() addsplits [nat_diff_split]
+                             addsimps [sublist_append]) 2);
+by (Simp_tac 1);
+qed "sublist_upt_eq_take";
+Addsimps [sublist_upt_eq_take];
+
+
 (*** Versions of some theorems above using binary numerals ***)
 
 AddIffs (map (rename_numerals thy) 
diff -r 5d9f02e75569 -r 9ae89b9ce206 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Jul 14 14:46:35 2000 +0200
+++ b/src/HOL/List.thy	Fri Jul 14 14:47:15 2000 +0200
@@ -181,11 +181,14 @@
                   {(xs,ys). length xs = Suc n & length ys = Suc n}"
 
 constdefs
- lex :: "('a * 'a)set => ('a list * 'a list)set"
-"lex r == UN n. lexn r n"
+  lex :: "('a * 'a)set => ('a list * 'a list)set"
+    "lex r == UN n. lexn r n"
 
- lexico :: "('a * 'a)set => ('a list * 'a list)set"
-"lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
+  lexico :: "('a * 'a)set => ('a list * 'a list)set"
+    "lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
+
+  sublist :: "['a list, nat set] => 'a list"
+    "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))"
 
 end
 
diff -r 5d9f02e75569 -r 9ae89b9ce206 src/HOL/UNITY/AllocBase.ML
--- a/src/HOL/UNITY/AllocBase.ML	Fri Jul 14 14:46:35 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML	Fri Jul 14 14:47:15 2000 +0200
@@ -28,55 +28,6 @@
 qed "mono_tokens";
 
 
-(*** sublist ***)
-
-Goalw [sublist_def] "sublist l {} = []";
-by Auto_tac;
-qed "sublist_empty";
-
-Goalw [sublist_def] "sublist [] A = []";
-by Auto_tac;
-qed "sublist_nil";
-
-Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] =     \
-\     map fst [p:zip xs [0..length xs(] . snd p + i : A]";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
- by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
-by (Simp_tac 1);
-qed "sublist_shift_lemma";
-
-Goalw [sublist_def]
-     "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
-by (res_inst_tac [("xs","l'")] rev_induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append, 
-	                              zip_append, sublist_shift_lemma]) 1);
-by (asm_simp_tac (simpset() addsimps [add_commute]) 1);
-qed "sublist_append";
-
-Addsimps [sublist_empty, sublist_nil];
-
-Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
-by (res_inst_tac [("xs","l")] rev_induct 1);
- by (asm_simp_tac (simpset() delsimps [append_Cons]
-	 		     addsimps [append_Cons RS sym, sublist_append]) 2);
-by (simp_tac (simpset() addsimps [sublist_def]) 1);
-qed "sublist_Cons";
-
-Goal "sublist [x] A = (if 0 : A then [x] else [])";
-by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
-qed "sublist_singleton";
-Addsimps [sublist_singleton];
-
-Goal "sublist l {..n(} = take n l";
-by (res_inst_tac [("xs","l")] rev_induct 1);
- by (asm_simp_tac (simpset() addsplits [nat_diff_split]
-                             addsimps [sublist_append]) 2);
-by (Simp_tac 1);
-qed "sublist_upt_eq_take";
-Addsimps [sublist_upt_eq_take];
-
-
 (** bag_of **)
 
 Goal "bag_of (l@l') = bag_of l + bag_of l'";
diff -r 5d9f02e75569 -r 9ae89b9ce206 src/HOL/UNITY/AllocBase.thy
--- a/src/HOL/UNITY/AllocBase.thy	Fri Jul 14 14:46:35 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.thy	Fri Jul 14 14:47:15 2000 +0200
@@ -24,10 +24,6 @@
   "tokens [] = 0"
   "tokens (x#xs) = x + tokens xs"
 
-constdefs sublist :: "['a list, nat set] => 'a list"
-    "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"
-
-
 consts
   bag_of :: 'a list => 'a multiset