src/HOL/List.ML

 
 Goal "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us";
 by (dtac sym 1);
 by (Asm_simp_tac 1);
 qed "append_eq_appendI";
-
-
-(** map **)
-
-section "map";
-
-Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
-
-Goal "map (%x. x) = (%xs. xs)";
-by (rtac ext 1);
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_ident";
-Addsimps[map_ident];
-
-Goal "map f (xs@ys) = map f xs @ map f ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_append";
-Addsimps[map_append];
-
-Goalw [o_def] "map (f o g) xs = map f (map g xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_compose";
-Addsimps[map_compose];
-
-Goal "rev(map f xs) = map f (rev xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "rev_map";
-
-(* a congruence rule for map: *)
-Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
-by (rtac impI 1);
-by (hyp_subst_tac 1);
-by (induct_tac "ys" 1);
-by Auto_tac;
-val lemma = result();
-bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
-
-Goal "(map f xs = []) = (xs = [])";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_is_Nil_conv";
-AddIffs [map_is_Nil_conv];
-
-Goal "([] = map f xs) = (xs = [])";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "Nil_is_map_conv";
-AddIffs [Nil_is_map_conv];
-
-
-(** rev **)
-
-section "rev";
-
-Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "rev_append";
-Addsimps[rev_append];
-
-Goal "rev(rev l) = l";
-by (induct_tac "l" 1);
-by Auto_tac;
-qed "rev_rev_ident";
-Addsimps[rev_rev_ident];
-
-Goal "(rev xs = []) = (xs = [])";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "rev_is_Nil_conv";
-AddIffs [rev_is_Nil_conv];
-
-Goal "([] = rev xs) = (xs = [])";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "Nil_is_rev_conv";
-AddIffs [Nil_is_rev_conv];
-
-val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
-by (stac (rev_rev_ident RS sym) 1);
-br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
-by (ALLGOALS Simp_tac);
-by (resolve_tac prems 1);
-by (eresolve_tac prems 1);
-qed "rev_induct";
-
-fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
-
-Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
-by Auto_tac;
-bind_thm ("rev_exhaust",
-  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
-
-
-(** mem **)
-
-section "mem";
-
-Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "mem_append";
-Addsimps[mem_append];
-
-Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "mem_filter";
-Addsimps[mem_filter];
-
-(** set **)
-
-section "set";
-
-qed_goal "finite_set" thy "finite (set xs)" 
-	(K [induct_tac "xs" 1, Auto_tac]);
-Addsimps[finite_set];
-AddSIs[finite_set];
-
-Goal "set (xs@ys) = (set xs Un set ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_append";
-Addsimps[set_append];
-
-Goal "(x mem xs) = (x: set xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_mem_eq";
-
-Goal "set l <= set (x#l)";
-by Auto_tac;
-qed "set_subset_Cons";
-
-Goal "(set xs = {}) = (xs = [])";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_empty";
-Addsimps [set_empty];
-
-Goal "set(rev xs) = set(xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_rev";
-Addsimps [set_rev];
-
-Goal "set(map f xs) = f``(set xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "set_map";
-Addsimps [set_map];
-
-Goal "(x : set(filter P xs)) = (x : set xs & P x)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "in_set_filter";
-Addsimps [in_set_filter];
-
-Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (Asm_simp_tac 1);
-by (rtac iffI 1);
-by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
-by (REPEAT(etac exE 1));
-by (exhaust_tac "ys" 1);
-by Auto_tac;
-qed "in_set_conv_decomp";
-
-(* eliminate `lists' in favour of `set' *)
-
-Goal "(xs : lists A) = (!x : set xs. x : A)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "in_lists_conv_set";
-
-bind_thm("in_listsD",in_lists_conv_set RS iffD1);
-AddSDs [in_listsD];
-bind_thm("in_listsI",in_lists_conv_set RS iffD2);
-AddSIs [in_listsI];
-
-(** list_all **)
-
-section "list_all";
-
-Goal "list_all (%x. True) xs = True";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "list_all_True";
-Addsimps [list_all_True];
-
-Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "list_all_append";
-Addsimps [list_all_append];
-
-Goal "list_all P xs = (!x. x mem xs --> P(x))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "list_all_mem_conv";
-
-
-(** filter **)
-
-section "filter";
-
-Goal "filter P (xs@ys) = filter P xs @ filter P ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "filter_append";
-Addsimps [filter_append];
-
-Goal "filter (%x. True) xs = xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "filter_True";
-Addsimps [filter_True];
-
-Goal "filter (%x. False) xs = []";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "filter_False";
-Addsimps [filter_False];
-
-Goal "length (filter P xs) <= length xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "length_filter";
-
-
-(** concat **)
-
-section "concat";
-
-Goal  "concat(xs@ys) = concat(xs)@concat(ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed"concat_append";
-Addsimps [concat_append];
-
-Goal "(concat xss = []) = (!xs:set xss. xs=[])";
-by (induct_tac "xss" 1);
-by Auto_tac;
-qed "concat_eq_Nil_conv";
-AddIffs [concat_eq_Nil_conv];
-
-Goal "([] = concat xss) = (!xs:set xss. xs=[])";
-by (induct_tac "xss" 1);
-by Auto_tac;
-qed "Nil_eq_concat_conv";
-AddIffs [Nil_eq_concat_conv];
-
-Goal  "set(concat xs) = Union(set `` set xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed"set_concat";
-Addsimps [set_concat];
-
-Goal "map f (concat xs) = concat (map (map f) xs)"; 
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "map_concat";
-
-Goal "filter p (concat xs) = concat (map (filter p) xs)"; 
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed"filter_concat"; 
-
-Goal "rev(concat xs) = concat (map rev (rev xs))";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "rev_concat";
-
-(** nth **)
-
-section "nth";
-
-Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
-by (induct_tac "n" 1);
- by (Asm_simp_tac 1);
- by (rtac allI 1);
- by (exhaust_tac "xs" 1);
-  by Auto_tac;
-qed_spec_mp "nth_append";
-
-Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
-by (induct_tac "xs" 1);
-(* case [] *)
-by (Asm_full_simp_tac 1);
-(* case x#xl *)
-by (rtac allI 1);
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "nth_map";
-Addsimps [nth_map];
-
-Goal "!n. n < length xs --> list_all P xs --> P(xs!n)";
-by (induct_tac "xs" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (rtac allI 1);
-by (induct_tac "n" 1);
-by Auto_tac;
-qed_spec_mp "list_all_nth";
-
-Goal "!n. n < length xs --> xs!n mem xs";
-by (induct_tac "xs" 1);
-(* case [] *)
-by (Simp_tac 1);
-(* case x#xl *)
-by (rtac allI 1);
-by (induct_tac "n" 1);
-(* case 0 *)
-by (Asm_full_simp_tac 1);
-(* case Suc x *)
-by (Asm_full_simp_tac 1);
-qed_spec_mp "nth_mem";
-Addsimps [nth_mem];
-
-(** list update **)
-
-section "list update";
-
-Goal "!i. length(xs[i:=x]) = length xs";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
-qed_spec_mp "length_list_update";
-Addsimps [length_list_update];
-
-
-(** last & butlast **)
-
-Goal "last(xs@[x]) = x";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "last_snoc";
-Addsimps [last_snoc];
-
-Goal "butlast(xs@[x]) = xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "butlast_snoc";
-Addsimps [butlast_snoc];
-
-Goal "length(butlast xs) = length xs - 1";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
-by Auto_tac;
-qed "length_butlast";
-Addsimps [length_butlast];
-
-Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "butlast_append";
-
-Goal "x:set(butlast xs) --> x:set xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "in_set_butlastD";
-
-Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
-by (blast_tac (claset() addDs [in_set_butlastD]) 1);
-qed "in_set_butlast_appendI1";
-
-Goal "x:set(butlast ys) ==> x:set(butlast(xs@ys))";
-by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
-by (Clarify_tac 1);
-by (Full_simp_tac 1);
-qed "in_set_butlast_appendI2";
-
-(** take  & drop **)
-section "take & drop";
-
-Goal "take 0 xs = []";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "take_0";
-
-Goal "drop 0 xs = xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "drop_0";
-
-Goal "take (Suc n) (x#xs) = x # take n xs";
-by (Simp_tac 1);
-qed "take_Suc_Cons";
-
-Goal "drop (Suc n) (x#xs) = drop n xs";
-by (Simp_tac 1);
-qed "drop_Suc_Cons";
-
-Delsimps [take_Cons,drop_Cons];
-Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
-
-Goal "!xs. length(take n xs) = min (length xs) n";
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "length_take";
-Addsimps [length_take];
-
-Goal "!xs. length(drop n xs) = (length xs - n)";
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "length_drop";
-Addsimps [length_drop];
-
-Goal "!xs. length xs <= n --> take n xs = xs";
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "take_all";
-
-Goal "!xs. length xs <= n --> drop n xs = []";
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "drop_all";
-
-Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "take_append";
-Addsimps [take_append];
-
-Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "drop_append";
-Addsimps [drop_append];
-
-Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
-by (induct_tac "m" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-by (exhaust_tac "na" 1);
- by Auto_tac;
-qed_spec_mp "take_take";
-
-Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
-by (induct_tac "m" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "drop_drop";
-
-Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
-by (induct_tac "m" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "take_drop";
-
-Goal "!xs. take n (map f xs) = map f (take n xs)"; 
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "take_map"; 
-
-Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "drop_map";
-
-Goal "!n i. i < n --> (take n xs)!i = xs!i";
-by (induct_tac "xs" 1);
- by Auto_tac;
-by (exhaust_tac "n" 1);
- by (Blast_tac 1);
-by (exhaust_tac "i" 1);
- by Auto_tac;
-qed_spec_mp "nth_take";
-Addsimps [nth_take];
-
-Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
-by (induct_tac "n" 1);
- by Auto_tac;
-by (exhaust_tac "xs" 1);
- by Auto_tac;
-qed_spec_mp "nth_drop";
-Addsimps [nth_drop];
-
-(** takeWhile & dropWhile **)
-
-section "takeWhile & dropWhile";
-
-Goal "takeWhile P xs @ dropWhile P xs = xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "takeWhile_dropWhile_id";
-Addsimps [takeWhile_dropWhile_id];
-
-Goal  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
-by (induct_tac "xs" 1);
-by Auto_tac;
-bind_thm("takeWhile_append1", conjI RS (result() RS mp));
-Addsimps [takeWhile_append1];
-
-Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-bind_thm("takeWhile_append2", ballI RS (result() RS mp));
-Addsimps [takeWhile_append2];
-
-Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-bind_thm("dropWhile_append1", conjI RS (result() RS mp));
-Addsimps [dropWhile_append1];
-
-Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-bind_thm("dropWhile_append2", ballI RS (result() RS mp));
-Addsimps [dropWhile_append2];
-
-Goal "x:set(takeWhile P xs) --> x:set xs & P x";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp"set_take_whileD";
-
-qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
-qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
-						      (K [Simp_tac 1]);
-
-
-(** foldl **)
-section "foldl";
-
-Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "foldl_append";
-Addsimps [foldl_append];
-
-(* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use
-   because it requires an additional transitivity step
-*)
-Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
-by (induct_tac "ns" 1);
- by (Simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addIs [trans_le_add1]) 1);
-qed_spec_mp "start_le_sum";
-
-Goal "n : set ns ==> n <= foldl op+ 0 ns";
-by (auto_tac (claset() addIs [start_le_sum],
-             simpset() addsimps [in_set_conv_decomp]));
-qed "elem_le_sum";
-
-Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
-by (induct_tac "ns" 1);
-by Auto_tac;
-qed_spec_mp "sum_eq_0_conv";
-AddIffs [sum_eq_0_conv];
-
-(** 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();
-
-Goalw [upto_def] "j<i ==> [i..j] = []";
-br trans 1;
-brs paired_upto.rules 1;
-br lemma 1;
-by(Asm_simp_tac 1);
-qed "upto_conv_Nil";
-
-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";
-
-Addsimps [upto_conv_Nil,upto_conv_Cons];
-
-(** nodups & remdups **)
-section "nodups & remdups";
-
-Goal "set(remdups xs) = set xs";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
-qed "set_remdups";
-Addsimps [set_remdups];
-
-Goal "nodups(remdups xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed "nodups_remdups";
-
-Goal "nodups xs --> nodups (filter P xs)";
-by (induct_tac "xs" 1);
-by Auto_tac;
-qed_spec_mp "nodups_filter";
-
-(** replicate **)
-section "replicate";
-
-Goal "set(replicate (Suc n) x) = {x}";
-by (induct_tac "n" 1);
-by Auto_tac;
-val lemma = result();
-
-Goal "n ~= 0 ==> set(replicate n x) = {x}";
-by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
-qed "set_replicate";
-Addsimps [set_replicate];
-
-
-(*** Lexcicographic orderings on lists ***)
-section"Lexcicographic orderings on lists";
-
-Goal "wf r ==> wf(lexn r n)";
-by (induct_tac "n" 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (rtac wf_subset 1);
-by (rtac Int_lower1 2);
-by (rtac wf_prod_fun_image 1);
-by (rtac injI 2);
-by (Auto_tac);
-qed "wf_lexn";
-
-Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "lexn_length";
-
-Goalw [lex_def] "wf r ==> wf(lex r)";
-by (rtac wf_UN 1);
-by (blast_tac (claset() addIs [wf_lexn]) 1);
-by (Clarify_tac 1);
-by (rename_tac "m n" 1);
-by (subgoal_tac "m ~= n" 1);
- by (Blast_tac 2);
-by (blast_tac (claset() addDs [lexn_length,not_sym]) 1);
-qed "wf_lex";
-AddSIs [wf_lex];
-
-Goal
- "lexn r n = \
-\ {(xs,ys). length xs = n & length ys = n & \
-\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
-by (induct_tac "n" 1);
- by (Simp_tac 1);
- by (Blast_tac 1);
-by (asm_full_simp_tac (simpset() delsimps [length_Suc_conv] 
-				addsimps [lex_prod_def]) 1);
-by (auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
-  by (Blast_tac 1);
- by (rename_tac "a xys x xs' y ys'" 1);
- by (res_inst_tac [("x","a#xys")] exI 1);
- by (Simp_tac 1);
-by (exhaust_tac "xys" 1);
- by (ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
-by (Blast_tac 1);
-qed "lexn_conv";
-
-Goalw [lex_def]
- "lex r = \
-\ {(xs,ys). length xs = length ys & \
-\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
-by (force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
-qed "lex_conv";
-
-Goalw [lexico_def] "wf r ==> wf(lexico r)";
-by (Blast_tac 1);
-qed "wf_lexico";
-AddSIs [wf_lexico];
-
-Goalw
- [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
-"lexico r = {(xs,ys). length xs < length ys | \
-\                     length xs = length ys & (xs,ys) : lex r}";
-by (Simp_tac 1);
-qed "lexico_conv";
-
-Goal "([],ys) ~: lex r";
-by (simp_tac (simpset() addsimps [lex_conv]) 1);
-qed "Nil_notin_lex";
-
-Goal "(xs,[]) ~: lex r";
-by (simp_tac (simpset() addsimps [lex_conv]) 1);
-qed "Nil2_notin_lex";
-
-AddIffs [Nil_notin_lex,Nil2_notin_lex];
-
-Goal "((x#xs,y#ys) : lex r) = \
-\     ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";
-by (simp_tac (simpset() addsimps [lex_conv]) 1);
-by (rtac iffI 1);
- by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
-by (REPEAT(eresolve_tac [conjE, exE] 1));
-by (exhaust_tac "xys" 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-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

 in
 val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
 end;
 
 Addsimprocs [list_eq_simproc];
+
+
+(** map **)
+
+section "map";
+
+Goal "(!x. x : set xs --> f x = g x) --> map f xs = map g xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
+
+Goal "map (%x. x) = (%xs. xs)";
+by (rtac ext 1);
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_ident";
+Addsimps[map_ident];
+
+Goal "map f (xs@ys) = map f xs @ map f ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_append";
+Addsimps[map_append];
+
+Goalw [o_def] "map (f o g) xs = map f (map g xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_compose";
+Addsimps[map_compose];
+
+Goal "rev(map f xs) = map f (rev xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "rev_map";
+
+(* a congruence rule for map: *)
+Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
+by (rtac impI 1);
+by (hyp_subst_tac 1);
+by (induct_tac "ys" 1);
+by Auto_tac;
+val lemma = result();
+bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
+
+Goal "(map f xs = []) = (xs = [])";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_is_Nil_conv";
+AddIffs [map_is_Nil_conv];
+
+Goal "([] = map f xs) = (xs = [])";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "Nil_is_map_conv";
+AddIffs [Nil_is_map_conv];
+
+
+(** rev **)
+
+section "rev";
+
+Goal "rev(xs@ys) = rev(ys) @ rev(xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "rev_append";
+Addsimps[rev_append];
+
+Goal "rev(rev l) = l";
+by (induct_tac "l" 1);
+by Auto_tac;
+qed "rev_rev_ident";
+Addsimps[rev_rev_ident];
+
+Goal "(rev xs = []) = (xs = [])";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "rev_is_Nil_conv";
+AddIffs [rev_is_Nil_conv];
+
+Goal "([] = rev xs) = (xs = [])";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "Nil_is_rev_conv";
+AddIffs [Nil_is_rev_conv];
+
+val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
+by (stac (rev_rev_ident RS sym) 1);
+br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
+by (ALLGOALS Simp_tac);
+by (resolve_tac prems 1);
+by (eresolve_tac prems 1);
+qed "rev_induct";
+
+fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
+
+Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
+by (res_inst_tac [("xs","xs")] rev_induct 1);
+by Auto_tac;
+bind_thm ("rev_exhaust",
+  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
+
+
+(** mem **)
+
+section "mem";
+
+Goal "x mem (xs@ys) = (x mem xs | x mem ys)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "mem_append";
+Addsimps[mem_append];
+
+Goal "x mem [x:xs. P(x)] = (x mem xs & P(x))";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "mem_filter";
+Addsimps[mem_filter];
+
+(** set **)
+
+section "set";
+
+qed_goal "finite_set" thy "finite (set xs)" 
+	(K [induct_tac "xs" 1, Auto_tac]);
+Addsimps[finite_set];
+AddSIs[finite_set];
+
+Goal "set (xs@ys) = (set xs Un set ys)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "set_append";
+Addsimps[set_append];
+
+Goal "(x mem xs) = (x: set xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "set_mem_eq";
+
+Goal "set l <= set (x#l)";
+by Auto_tac;
+qed "set_subset_Cons";
+
+Goal "(set xs = {}) = (xs = [])";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "set_empty";
+Addsimps [set_empty];
+
+Goal "set(rev xs) = set(xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "set_rev";
+Addsimps [set_rev];
+
+Goal "set(map f xs) = f``(set xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "set_map";
+Addsimps [set_map];
+
+Goal "(x : set(filter P xs)) = (x : set xs & P x)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "in_set_filter";
+Addsimps [in_set_filter];
+
+Goal "(x : set xs) = (? ys zs. xs = ys@x#zs)";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (Asm_simp_tac 1);
+by (rtac iffI 1);
+by (blast_tac (claset() addIs [eq_Nil_appendI,Cons_eq_appendI]) 1);
+by (REPEAT(etac exE 1));
+by (exhaust_tac "ys" 1);
+by Auto_tac;
+qed "in_set_conv_decomp";
+
+(* eliminate `lists' in favour of `set' *)
+
+Goal "(xs : lists A) = (!x : set xs. x : A)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "in_lists_conv_set";
+
+bind_thm("in_listsD",in_lists_conv_set RS iffD1);
+AddSDs [in_listsD];
+bind_thm("in_listsI",in_lists_conv_set RS iffD2);
+AddSIs [in_listsI];
+
+(** list_all **)
+
+section "list_all";
+
+Goal "list_all (%x. True) xs = True";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "list_all_True";
+Addsimps [list_all_True];
+
+Goal "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "list_all_append";
+Addsimps [list_all_append];
+
+Goal "list_all P xs = (!x. x mem xs --> P(x))";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "list_all_mem_conv";
+
+
+(** filter **)
+
+section "filter";
+
+Goal "filter P (xs@ys) = filter P xs @ filter P ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "filter_append";
+Addsimps [filter_append];
+
+Goal "filter (%x. True) xs = xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "filter_True";
+Addsimps [filter_True];
+
+Goal "filter (%x. False) xs = []";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "filter_False";
+Addsimps [filter_False];
+
+Goal "length (filter P xs) <= length xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "length_filter";
+
+
+(** concat **)
+
+section "concat";
+
+Goal  "concat(xs@ys) = concat(xs)@concat(ys)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed"concat_append";
+Addsimps [concat_append];
+
+Goal "(concat xss = []) = (!xs:set xss. xs=[])";
+by (induct_tac "xss" 1);
+by Auto_tac;
+qed "concat_eq_Nil_conv";
+AddIffs [concat_eq_Nil_conv];
+
+Goal "([] = concat xss) = (!xs:set xss. xs=[])";
+by (induct_tac "xss" 1);
+by Auto_tac;
+qed "Nil_eq_concat_conv";
+AddIffs [Nil_eq_concat_conv];
+
+Goal  "set(concat xs) = Union(set `` set xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed"set_concat";
+Addsimps [set_concat];
+
+Goal "map f (concat xs) = concat (map (map f) xs)"; 
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "map_concat";
+
+Goal "filter p (concat xs) = concat (map (filter p) xs)"; 
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed"filter_concat"; 
+
+Goal "rev(concat xs) = concat (map rev (rev xs))";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "rev_concat";
+
+(** nth **)
+
+section "nth";
+
+Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+ by (rtac allI 1);
+ by (exhaust_tac "xs" 1);
+  by Auto_tac;
+qed_spec_mp "nth_append";
+
+Goal "!n. n < length xs --> (map f xs)!n = f(xs!n)";
+by (induct_tac "xs" 1);
+(* case [] *)
+by (Asm_full_simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "nth_map";
+Addsimps [nth_map];
+
+Goal "!n. n < length xs --> list_all P xs --> P(xs!n)";
+by (induct_tac "xs" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "list_all_nth";
+
+Goal "!n. n < length xs --> xs!n mem xs";
+by (induct_tac "xs" 1);
+(* case [] *)
+by (Simp_tac 1);
+(* case x#xl *)
+by (rtac allI 1);
+by (induct_tac "n" 1);
+(* case 0 *)
+by (Asm_full_simp_tac 1);
+(* case Suc x *)
+by (Asm_full_simp_tac 1);
+qed_spec_mp "nth_mem";
+Addsimps [nth_mem];
+
+(** list update **)
+
+section "list update";
+
+Goal "!i. length(xs[i:=x]) = length xs";
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [nat.split]) 1);
+qed_spec_mp "length_list_update";
+Addsimps [length_list_update];
+
+
+(** last & butlast **)
+
+Goal "last(xs@[x]) = x";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "last_snoc";
+Addsimps [last_snoc];
+
+Goal "butlast(xs@[x]) = xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "butlast_snoc";
+Addsimps [butlast_snoc];
+
+Goal "length(butlast xs) = length xs - 1";
+by (res_inst_tac [("xs","xs")] rev_induct 1);
+by Auto_tac;
+qed "length_butlast";
+Addsimps [length_butlast];
+
+Goal "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "butlast_append";
+
+Goal "x:set(butlast xs) --> x:set xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "in_set_butlastD";
+
+Goal "x:set(butlast xs) ==> x:set(butlast(xs@ys))";
+by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
+by (blast_tac (claset() addDs [in_set_butlastD]) 1);
+qed "in_set_butlast_appendI1";
+
+Goal "x:set(butlast ys) ==> x:set(butlast(xs@ys))";
+by (asm_simp_tac (simpset() addsimps [butlast_append]) 1);
+by (Clarify_tac 1);
+by (Full_simp_tac 1);
+qed "in_set_butlast_appendI2";
+
+(** take  & drop **)
+section "take & drop";
+
+Goal "take 0 xs = []";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "take_0";
+
+Goal "drop 0 xs = xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "drop_0";
+
+Goal "take (Suc n) (x#xs) = x # take n xs";
+by (Simp_tac 1);
+qed "take_Suc_Cons";
+
+Goal "drop (Suc n) (x#xs) = drop n xs";
+by (Simp_tac 1);
+qed "drop_Suc_Cons";
+
+Delsimps [take_Cons,drop_Cons];
+Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
+
+Goal "!xs. length(take n xs) = min (length xs) n";
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "length_take";
+Addsimps [length_take];
+
+Goal "!xs. length(drop n xs) = (length xs - n)";
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "length_drop";
+Addsimps [length_drop];
+
+Goal "!xs. length xs <= n --> take n xs = xs";
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "take_all";
+
+Goal "!xs. length xs <= n --> drop n xs = []";
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "drop_all";
+
+Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "take_append";
+Addsimps [take_append];
+
+Goal "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "drop_append";
+Addsimps [drop_append];
+
+Goal "!xs n. take n (take m xs) = take (min n m) xs"; 
+by (induct_tac "m" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+by (exhaust_tac "na" 1);
+ by Auto_tac;
+qed_spec_mp "take_take";
+
+Goal "!xs. drop n (drop m xs) = drop (n + m) xs"; 
+by (induct_tac "m" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "drop_drop";
+
+Goal "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
+by (induct_tac "m" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "take_drop";
+
+Goal "!xs. take n (map f xs) = map f (take n xs)"; 
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "take_map"; 
+
+Goal "!xs. drop n (map f xs) = map f (drop n xs)"; 
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "drop_map";
+
+Goal "!n i. i < n --> (take n xs)!i = xs!i";
+by (induct_tac "xs" 1);
+ by Auto_tac;
+by (exhaust_tac "n" 1);
+ by (Blast_tac 1);
+by (exhaust_tac "i" 1);
+ by Auto_tac;
+qed_spec_mp "nth_take";
+Addsimps [nth_take];
+
+Goal  "!xs i. n + i <= length xs --> (drop n xs)!i = xs!(n+i)";
+by (induct_tac "n" 1);
+ by Auto_tac;
+by (exhaust_tac "xs" 1);
+ by Auto_tac;
+qed_spec_mp "nth_drop";
+Addsimps [nth_drop];
+
+(** takeWhile & dropWhile **)
+
+section "takeWhile & dropWhile";
+
+Goal "takeWhile P xs @ dropWhile P xs = xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "takeWhile_dropWhile_id";
+Addsimps [takeWhile_dropWhile_id];
+
+Goal  "x:set xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+bind_thm("takeWhile_append1", conjI RS (result() RS mp));
+Addsimps [takeWhile_append1];
+
+Goal "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+bind_thm("takeWhile_append2", ballI RS (result() RS mp));
+Addsimps [takeWhile_append2];
+
+Goal "x:set xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+bind_thm("dropWhile_append1", conjI RS (result() RS mp));
+Addsimps [dropWhile_append1];
+
+Goal "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+bind_thm("dropWhile_append2", ballI RS (result() RS mp));
+Addsimps [dropWhile_append2];
+
+Goal "x:set(takeWhile P xs) --> x:set xs & P x";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp"set_take_whileD";
+
+qed_goal "zip_Nil_Nil"   thy "zip []     []     = []" (K [Simp_tac 1]);
+qed_goal "zip_Cons_Cons" thy "zip (x#xs) (y#ys) = (x,y)#zip xs ys" 
+						      (K [Simp_tac 1]);
+
+
+(** foldl **)
+section "foldl";
+
+Goal "!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "foldl_append";
+Addsimps [foldl_append];
+
+(* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use
+   because it requires an additional transitivity step
+*)
+Goal "!n::nat. m <= n --> m <= foldl op+ n ns";
+by (induct_tac "ns" 1);
+ by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [trans_le_add1]) 1);
+qed_spec_mp "start_le_sum";
+
+Goal "n : set ns ==> n <= foldl op+ 0 ns";
+by (auto_tac (claset() addIs [start_le_sum],
+             simpset() addsimps [in_set_conv_decomp]));
+qed "elem_le_sum";
+
+Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
+by (induct_tac "ns" 1);
+by Auto_tac;
+qed_spec_mp "sum_eq_0_conv";
+AddIffs [sum_eq_0_conv];
+
+(** upto **)
+
+(* 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";
+
+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;
+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];
+
+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];
+
+
+(** nodups & remdups **)
+section "nodups & remdups";
+
+Goal "set(remdups xs) = set xs";
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [insert_absorb]) 1);
+qed "set_remdups";
+Addsimps [set_remdups];
+
+Goal "nodups(remdups xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "nodups_remdups";
+
+Goal "nodups xs --> nodups (filter P xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "nodups_filter";
+
+(** replicate **)
+section "replicate";
+
+Goal "set(replicate (Suc n) x) = {x}";
+by (induct_tac "n" 1);
+by Auto_tac;
+val lemma = result();
+
+Goal "n ~= 0 ==> set(replicate n x) = {x}";
+by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
+qed "set_replicate";
+Addsimps [set_replicate];
+
+
+(*** Lexcicographic orderings on lists ***)
+section"Lexcicographic orderings on lists";
+
+Goal "wf r ==> wf(lexn r n)";
+by (induct_tac "n" 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (rtac wf_subset 1);
+by (rtac Int_lower1 2);
+by (rtac wf_prod_fun_image 1);
+by (rtac injI 2);
+by (Auto_tac);
+qed "wf_lexn";
+
+Goal "!xs ys. (xs,ys) : lexn r n --> length xs = n & length ys = n";
+by (induct_tac "n" 1);
+by (Auto_tac);
+qed_spec_mp "lexn_length";
+
+Goalw [lex_def] "wf r ==> wf(lex r)";
+by (rtac wf_UN 1);
+by (blast_tac (claset() addIs [wf_lexn]) 1);
+by (Clarify_tac 1);
+by (rename_tac "m n" 1);
+by (subgoal_tac "m ~= n" 1);
+ by (Blast_tac 2);
+by (blast_tac (claset() addDs [lexn_length,not_sym]) 1);
+qed "wf_lex";
+AddSIs [wf_lex];
+
+Goal
+ "lexn r n = \
+\ {(xs,ys). length xs = n & length ys = n & \
+\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [length_Suc_conv] 
+				addsimps [lex_prod_def]) 1);
+by (auto_tac (claset(), simpset() delsimps [length_Suc_conv]));
+  by (Blast_tac 1);
+ by (rename_tac "a xys x xs' y ys'" 1);
+ by (res_inst_tac [("x","a#xys")] exI 1);
+ by (Simp_tac 1);
+by (exhaust_tac "xys" 1);
+ by (ALLGOALS (asm_full_simp_tac (simpset() delsimps [length_Suc_conv])));
+by (Blast_tac 1);
+qed "lexn_conv";
+
+Goalw [lex_def]
+ "lex r = \
+\ {(xs,ys). length xs = length ys & \
+\           (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}";
+by (force_tac (claset(), simpset() delsimps [length_Suc_conv] addsimps [lexn_conv]) 1);
+qed "lex_conv";
+
+Goalw [lexico_def] "wf r ==> wf(lexico r)";
+by (Blast_tac 1);
+qed "wf_lexico";
+AddSIs [wf_lexico];
+
+Goalw
+ [lexico_def,diag_def,lex_prod_def,measure_def,inv_image_def]
+"lexico r = {(xs,ys). length xs < length ys | \
+\                     length xs = length ys & (xs,ys) : lex r}";
+by (Simp_tac 1);
+qed "lexico_conv";
+
+Goal "([],ys) ~: lex r";
+by (simp_tac (simpset() addsimps [lex_conv]) 1);
+qed "Nil_notin_lex";
+
+Goal "(xs,[]) ~: lex r";
+by (simp_tac (simpset() addsimps [lex_conv]) 1);
+qed "Nil2_notin_lex";
+
+AddIffs [Nil_notin_lex,Nil2_notin_lex];
+
+Goal "((x#xs,y#ys) : lex r) = \
+\     ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";
+by (simp_tac (simpset() addsimps [lex_conv]) 1);
+by (rtac iffI 1);
+ by (blast_tac (claset() addIs [Cons_eq_appendI]) 2);
+by (REPEAT(eresolve_tac [conjE, exE] 1));
+by (exhaust_tac "xys" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
+qed "Cons_in_lex";
+AddIffs [Cons_in_lex];