# HG changeset patch
# User nipkow
# Date 1188912631 -7200
# Node ID 7fa202789bf6890ae753fb8594606134b140c00a
# Parent  ea0f9b8db436f4d6a03261ff06ade4bd821de326
tuned lemma; replaced !! by arbitrary

diff -r ea0f9b8db436 -r 7fa202789bf6 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 04 14:32:29 2007 +0200
+++ b/src/HOL/List.thy	Tue Sep 04 15:30:31 2007 +0200
@@ -408,12 +408,12 @@
 apply auto
 done
 
-lemma list_induct2[consumes 1]: "\<And>ys.
- \<lbrakk> length xs = length ys;
+lemma list_induct2[consumes 1]:
+  "\<lbrakk> length xs = length ys;
    P [] [];
    \<And>x xs y ys. \<lbrakk> length xs = length ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
  \<Longrightarrow> P xs ys"
-apply(induct xs)
+apply(induct xs arbitrary: ys)
  apply simp
 apply(case_tac ys)
  apply simp
@@ -495,17 +495,16 @@
 by (induct xs) auto
 
 lemma append_eq_append_conv [simp,noatp]:
- "!!ys. length xs = length ys \<or> length us = length vs
+ "length xs = length ys \<or> length us = length vs
  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
-apply (induct xs)
+apply (induct xs arbitrary: ys)
  apply (case_tac ys, simp, force)
 apply (case_tac ys, force, simp)
 done
 
-lemma append_eq_append_conv2: "!!ys zs ts.
- (xs @ ys = zs @ ts) =
- (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
-apply (induct xs)
+lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
+  (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
+apply (induct xs arbitrary: ys zs ts)
  apply fastsimp
 apply(case_tac zs)
  apply simp
@@ -672,8 +671,8 @@
 by(induct ys, auto simp add: Cons_eq_map_conv)
 
 lemma map_eq_imp_length_eq:
-  "!!xs. map f xs = map f ys ==> length xs = length ys"
-apply (induct ys)
+  "map f xs = map f ys ==> length xs = length ys"
+apply (induct ys arbitrary: xs)
  apply simp
 apply(simp (no_asm_use))
 apply clarify
@@ -697,8 +696,8 @@
 by(blast dest:map_inj_on)
 
 lemma map_injective:
- "!!xs. map f xs = map f ys ==> inj f ==> xs = ys"
-by (induct ys) (auto dest!:injD)
+ "map f xs = map f ys ==> inj f ==> xs = ys"
+by (induct ys arbitrary: xs) (auto dest!:injD)
 
 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
 by(blast dest:map_injective)
@@ -1054,8 +1053,8 @@
 declare nth.simps [simp del]
 
 lemma nth_append:
-"!!n. (xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
-apply (induct "xs", simp)
+  "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
+apply (induct xs arbitrary: n, simp)
 apply (case_tac n, auto)
 done
 
@@ -1065,8 +1064,8 @@
 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
 by (induct "xs") auto
 
-lemma nth_map [simp]: "!!n. n < length xs ==> (map f xs)!n = f(xs!n)"
-apply (induct xs, simp)
+lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
+apply (induct xs arbitrary: n, simp)
 apply (case_tac n, auto)
 done
 
@@ -1075,8 +1074,8 @@
 
 
 lemma list_eq_iff_nth_eq:
- "!!ys. (xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
-apply(induct xs)
+ "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
+apply(induct xs arbitrary: ys)
  apply simp apply blast
 apply(case_tac ys)
  apply simp
@@ -1113,67 +1112,65 @@
 
 subsubsection {* @{text list_update} *}
 
-lemma length_list_update [simp]: "!!i. length(xs[i:=x]) = length xs"
-by (induct xs) (auto split: nat.split)
+lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
+by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma nth_list_update:
-"!!i j. i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
-by (induct xs) (auto simp add: nth_Cons split: nat.split)
+"i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
+by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
 
 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
 by (simp add: nth_list_update)
 
-lemma nth_list_update_neq [simp]: "!!i j. i \<noteq> j ==> xs[i:=x]!j = xs!j"
-by (induct xs) (auto simp add: nth_Cons split: nat.split)
+lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
+by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
 
 lemma list_update_overwrite [simp]:
-"!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
-by (induct xs) (auto split: nat.split)
-
-lemma list_update_id[simp]: "!!i. i < length xs ==> xs[i := xs!i] = xs"
-apply (induct xs, simp)
-apply(simp split:nat.splits)
-done
-
-lemma list_update_beyond[simp]: "\<And>i. length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
-apply (induct xs)
+"i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
+by (induct xs arbitrary: i) (auto split: nat.split)
+
+lemma list_update_id[simp]: "xs[i := xs!i] = xs"
+by (induct xs arbitrary: i) (simp_all split:nat.splits)
+
+lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
+apply (induct xs arbitrary: i)
  apply simp
 apply (case_tac i)
 apply simp_all
 done
 
 lemma list_update_same_conv:
-"!!i. i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
-by (induct xs) (auto split: nat.split)
+"i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
+by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma list_update_append1:
- "!!i. i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
-apply (induct xs, simp)
+ "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
+apply (induct xs arbitrary: i, simp)
 apply(simp split:nat.split)
 done
 
 lemma list_update_append:
-  "!!n. (xs @ ys) [n:= x] = 
+  "(xs @ ys) [n:= x] = 
   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
-by (induct xs) (auto split:nat.splits)
+by (induct xs arbitrary: n) (auto split:nat.splits)
 
 lemma list_update_length [simp]:
  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
 by (induct xs, auto)
 
 lemma update_zip:
-"!!i xy xs. length xs = length ys ==>
-(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
-by (induct ys) (auto, case_tac xs, auto split: nat.split)
-
-lemma set_update_subset_insert: "!!i. set(xs[i:=x]) <= insert x (set xs)"
-by (induct xs) (auto split: nat.split)
+  "length xs = length ys ==>
+  (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
+by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
+
+lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
+by (induct xs arbitrary: i) (auto split: nat.split)
 
 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
 by (blast dest!: set_update_subset_insert [THEN subsetD])
 
-lemma set_update_memI: "!!n. n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
-by (induct xs) (auto split:nat.splits)
+lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
+by (induct xs arbitrary: n) (auto split:nat.splits)
 
 
 subsubsection {* @{text last} and @{text butlast} *}
@@ -1212,8 +1209,8 @@
 by (induct xs rule: rev_induct) auto
 
 lemma butlast_append:
-"!!ys. butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
-by (induct xs) auto
+  "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
+by (induct xs arbitrary: ys) auto
 
 lemma append_butlast_last_id [simp]:
 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
@@ -1226,8 +1223,8 @@
 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
 by (auto dest: in_set_butlastD simp add: butlast_append)
 
-lemma last_drop[simp]: "!!n. n < length xs \<Longrightarrow> last (drop n xs) = last xs"
-apply (induct xs)
+lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
+apply (induct xs arbitrary: n)
  apply simp
 apply (auto split:nat.split)
 done
@@ -1257,125 +1254,125 @@
 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
 by(cases xs, simp_all)
 
-lemma drop_tl: "!!n. drop n (tl xs) = tl(drop n xs)"
-by(induct xs, simp_all add:drop_Cons drop_Suc split:nat.split)
-
-lemma nth_via_drop: "!!n. drop n xs = y#ys \<Longrightarrow> xs!n = y"
-apply (induct xs, simp)
+lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
+by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
+
+lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
+apply (induct xs arbitrary: n, simp)
 apply(simp add:drop_Cons nth_Cons split:nat.splits)
 done
 
 lemma take_Suc_conv_app_nth:
- "!!i. i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
-apply (induct xs, simp)
+  "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
+apply (induct xs arbitrary: i, simp)
 apply (case_tac i, auto)
 done
 
 lemma drop_Suc_conv_tl:
-  "!!i. i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
-apply (induct xs, simp)
+  "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
+apply (induct xs arbitrary: i, simp)
 apply (case_tac i, auto)
 done
 
-lemma length_take [simp]: "!!xs. length (take n xs) = min (length xs) n"
-by (induct n) (auto, case_tac xs, auto)
-
-lemma length_drop [simp]: "!!xs. length (drop n xs) = (length xs - n)"
-by (induct n) (auto, case_tac xs, auto)
-
-lemma take_all [simp]: "!!xs. length xs <= n ==> take n xs = xs"
-by (induct n) (auto, case_tac xs, auto)
-
-lemma drop_all [simp]: "!!xs. length xs <= n ==> drop n xs = []"
-by (induct n) (auto, case_tac xs, auto)
+lemma length_take [simp]: "length (take n xs) = min (length xs) n"
+by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+
+lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
+by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+
+lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
+by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+
+lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
+by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma take_append [simp]:
-"!!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
-by (induct n) (auto, case_tac xs, auto)
+  "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
+by (induct n arbitrary: xs) (auto, case_tac xs, auto)
 
 lemma drop_append [simp]:
-"!!xs. drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
-by (induct n) (auto, case_tac xs, auto)
-
-lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs"
-apply (induct m, auto)
+  "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
+by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+
+lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
+apply (induct m arbitrary: xs n, auto)
 apply (case_tac xs, auto)
 apply (case_tac n, auto)
 done
 
-lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs"
-apply (induct m, auto)
+lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
+apply (induct m arbitrary: xs, auto)
 apply (case_tac xs, auto)
 done
 
-lemma take_drop: "!!xs n. take n (drop m xs) = drop m (take (n + m) xs)"
-apply (induct m, auto)
+lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
+apply (induct m arbitrary: xs n, auto)
 apply (case_tac xs, auto)
 done
 
-lemma drop_take: "!!m n. drop n (take m xs) = take (m-n) (drop n xs)"
-apply(induct xs)
+lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
+apply(induct xs arbitrary: m n)
  apply simp
 apply(simp add: take_Cons drop_Cons split:nat.split)
 done
 
-lemma append_take_drop_id [simp]: "!!xs. take n xs @ drop n xs = xs"
-apply (induct n, auto)
+lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
+apply (induct n arbitrary: xs, auto)
 apply (case_tac xs, auto)
 done
 
-lemma take_eq_Nil[simp]: "!!n. (take n xs = []) = (n = 0 \<or> xs = [])"
-apply(induct xs)
+lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
+apply(induct xs arbitrary: n)
  apply simp
 apply(simp add:take_Cons split:nat.split)
 done
 
-lemma drop_eq_Nil[simp]: "!!n. (drop n xs = []) = (length xs <= n)"
-apply(induct xs)
+lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
+apply(induct xs arbitrary: n)
 apply simp
 apply(simp add:drop_Cons split:nat.split)
 done
 
-lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)"
-apply (induct n, auto)
+lemma take_map: "take n (map f xs) = map f (take n xs)"
+apply (induct n arbitrary: xs, auto)
 apply (case_tac xs, auto)
 done
 
-lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)"
-apply (induct n, auto)
+lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
+apply (induct n arbitrary: xs, auto)
 apply (case_tac xs, auto)
 done
 
-lemma rev_take: "!!i. rev (take i xs) = drop (length xs - i) (rev xs)"
-apply (induct xs, auto)
+lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
+apply (induct xs arbitrary: i, auto)
 apply (case_tac i, auto)
 done
 
-lemma rev_drop: "!!i. rev (drop i xs) = take (length xs - i) (rev xs)"
-apply (induct xs, auto)
+lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
+apply (induct xs arbitrary: i, auto)
 apply (case_tac i, auto)
 done
 
-lemma nth_take [simp]: "!!n i. i < n ==> (take n xs)!i = xs!i"
-apply (induct xs, auto)
+lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
+apply (induct xs arbitrary: i n, auto)
 apply (case_tac n, blast)
 apply (case_tac i, auto)
 done
 
 lemma nth_drop [simp]:
-"!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
-apply (induct n, auto)
+  "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
+apply (induct n arbitrary: xs i, auto)
 apply (case_tac xs, auto)
 done
 
 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
 by(simp add: hd_conv_nth)
 
-lemma set_take_subset: "\<And>n. set(take n xs) \<subseteq> set xs"
-by(induct xs)(auto simp:take_Cons split:nat.split)
-
-lemma set_drop_subset: "\<And>n. set(drop n xs) \<subseteq> set xs"
-by(induct xs)(auto simp:drop_Cons split:nat.split)
+lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
+by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
+
+lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
+by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
 
 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
 using set_take_subset by fast
@@ -1384,31 +1381,31 @@
 using set_drop_subset by fast
 
 lemma append_eq_conv_conj:
-"!!zs. (xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
-apply (induct xs, simp, clarsimp)
+  "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
+apply (induct xs arbitrary: zs, simp, clarsimp)
 apply (case_tac zs, auto)
 done
 
-lemma take_add [rule_format]: 
-    "\<forall>i. i+j \<le> length(xs) --> take (i+j) xs = take i xs @ take j (drop i xs)"
-apply (induct xs, auto) 
-apply (case_tac i, simp_all) 
+lemma take_add: 
+  "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
+apply (induct xs arbitrary: i, auto) 
+apply (case_tac i, simp_all)
 done
 
 lemma append_eq_append_conv_if:
- "!! ys\<^isub>1. (xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
+ "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
   (if size xs\<^isub>1 \<le> size ys\<^isub>1
    then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2
    else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
-apply(induct xs\<^isub>1)
+apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
  apply simp
 apply(case_tac ys\<^isub>1)
 apply simp_all
 done
 
 lemma take_hd_drop:
-  "!!n. n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
-apply(induct xs)
+  "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (n+1) xs"
+apply(induct xs arbitrary: n)
 apply simp
 apply(simp add:drop_Cons split:nat.split)
 done
@@ -1562,8 +1559,8 @@
 done
 
 lemma nth_zip [simp]:
-"!!i xs. [| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
-apply (induct ys, simp)
+"[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
+apply (induct ys arbitrary: i xs, simp)
 apply (case_tac xs)
  apply (simp_all add: nth.simps split: nat.split)
 done
@@ -1577,22 +1574,22 @@
 by (rule sym, simp add: update_zip)
 
 lemma zip_replicate [simp]:
-"!!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
-apply (induct i, auto)
+  "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
+apply (induct i arbitrary: j, auto)
 apply (case_tac j, auto)
 done
 
 lemma take_zip:
- "!!xs ys. take n (zip xs ys) = zip (take n xs) (take n ys)"
-apply (induct n)
+  "take n (zip xs ys) = zip (take n xs) (take n ys)"
+apply (induct n arbitrary: xs ys)
  apply simp
 apply (case_tac xs, simp)
 apply (case_tac ys, simp_all)
 done
 
 lemma drop_zip:
- "!!xs ys. drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
-apply (induct n)
+  "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
+apply (induct n arbitrary: xs ys)
  apply simp
 apply (case_tac xs, simp)
 apply (case_tac ys, simp_all)
@@ -1731,26 +1728,26 @@
 by (simp add: list_all2_lengthD list_all2_update_cong)
 
 lemma list_all2_takeI [simp,intro?]:
-  "\<And>n ys. list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
-  apply (induct xs)
-   apply simp
-  apply (clarsimp simp add: list_all2_Cons1)
-  apply (case_tac n)
-  apply auto
-  done
+  "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
+apply (induct xs arbitrary: n ys)
+ apply simp
+apply (clarsimp simp add: list_all2_Cons1)
+apply (case_tac n)
+apply auto
+done
 
 lemma list_all2_dropI [simp,intro?]:
-  "\<And>n bs. list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
-  apply (induct as, simp)
-  apply (clarsimp simp add: list_all2_Cons1)
-  apply (case_tac n, simp, simp)
-  done
+  "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
+apply (induct as arbitrary: n bs, simp)
+apply (clarsimp simp add: list_all2_Cons1)
+apply (case_tac n, simp, simp)
+done
 
 lemma list_all2_mono [intro?]:
-  "\<And>y. list_all2 P x y \<Longrightarrow> (\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> list_all2 Q x y"
-  apply (induct x, simp)
-  apply (case_tac y, auto)
-  done
+  "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
+apply (induct xs arbitrary: ys, simp)
+apply (case_tac ys, auto)
+done
 
 lemma list_all2_eq:
   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
@@ -1760,8 +1757,8 @@
 subsubsection {* @{text foldl} and @{text foldr} *}
 
 lemma foldl_append [simp]:
-"!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
-by (induct xs) auto
+  "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
+by (induct xs arbitrary: a) auto
 
 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
 by (induct xs) auto
@@ -1820,15 +1817,15 @@
 difficult to use because it requires an additional transitivity step.
 *}
 
-lemma start_le_sum: "!!n::nat. m <= n ==> m <= foldl (op +) n ns"
-by (induct ns) auto
-
-lemma elem_le_sum: "!!n::nat. n : set ns ==> n <= foldl (op +) 0 ns"
+lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
+by (induct ns arbitrary: n) auto
+
+lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
 by (force intro: start_le_sum simp add: in_set_conv_decomp)
 
 lemma sum_eq_0_conv [iff]:
-"!!m::nat. (foldl (op +) m ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
-by (induct ns) auto
+  "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
+by (induct ns arbitrary: m) auto
 
 lemma foldr_invariant: 
   "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f x y) \<rbrakk> \<Longrightarrow> Q (foldr f xs x)"
@@ -1902,8 +1899,8 @@
 by(induct j)simp_all
 
 lemma upt_eq_Cons_conv:
- "!!x xs. ([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
-apply(induct j)
+ "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
+apply(induct j arbitrary: x xs)
  apply simp
 apply(clarsimp simp add: append_eq_Cons_conv)
 apply arith
@@ -1940,8 +1937,8 @@
  apply simp
 by(simp add:upt_Suc_append)
 
-lemma take_upt [simp]: "!!i. i+m <= n ==> take m [i..<n] = [i..<i+m]"
-apply (induct m, simp)
+lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
+apply (induct m arbitrary: i, simp)
 apply (subst upt_rec)
 apply (rule sym)
 apply (subst upt_rec)
@@ -1956,16 +1953,16 @@
 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..n]"
 by (induct n) auto
 
-lemma nth_map_upt: "!!i. i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
-apply (induct n m rule: diff_induct)
+lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
+apply (induct n m  arbitrary: i rule: diff_induct)
 prefer 3 apply (subst map_Suc_upt[symmetric])
 apply (auto simp add: less_diff_conv nth_upt)
 done
 
 lemma nth_take_lemma:
-  "!!xs ys. k <= length xs ==> k <= length ys ==>
+  "k <= length xs ==> k <= length ys ==>
      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
-apply (atomize, induct k)
+apply (atomize, induct k arbitrary: xs ys)
 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
 txt {* Both lists must be non-empty *}
 apply (case_tac xs, simp)
@@ -2063,16 +2060,16 @@
 lemma distinct_upt[simp]: "distinct[i..<j]"
 by (induct j) auto
 
-lemma distinct_take[simp]: "\<And>i. distinct xs \<Longrightarrow> distinct (take i xs)"
-apply(induct xs)
+lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
+apply(induct xs arbitrary: i)
  apply simp
 apply (case_tac i)
  apply simp_all
 apply(blast dest:in_set_takeD)
 done
 
-lemma distinct_drop[simp]: "\<And>i. distinct xs \<Longrightarrow> distinct (drop i xs)"
-apply(induct xs)
+lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
+apply(induct xs arbitrary: i)
  apply simp
 apply (case_tac i)
  apply simp_all
@@ -2227,8 +2224,8 @@
 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
 by (atomize (full), induct n) auto
 
-lemma nth_replicate[simp]: "!!i. i < n ==> (replicate n x)!i = x"
-apply (induct n, simp)
+lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
+apply (induct n arbitrary: i, simp)
 apply (simp add: nth_Cons split: nat.split)
 done
 
@@ -2243,8 +2240,8 @@
 apply (simp add: replicate_add [symmetric])
 done
 
-lemma drop_replicate[simp]: "!!i. drop i (replicate k x) = replicate (k-i) x"
-apply (induct k)
+lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
+apply (induct k arbitrary: i)
  apply simp
 apply clarsimp
 apply (case_tac i)
@@ -2322,8 +2319,8 @@
 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
 by(simp add:rotate1_def split:list.split)
 
-lemma length_rotate[simp]: "!!xs. length(rotate n xs) = length xs"
-by (induct n) (simp_all add:rotate_def)
+lemma length_rotate[simp]: "length(rotate n xs) = length xs"
+by (induct n arbitrary: xs) (simp_all add:rotate_def)
 
 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
 by(simp add:rotate1_def split:list.split) blast
@@ -2376,9 +2373,9 @@
 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
 
 lemma sublist_shift_lemma_Suc:
-  "!!is. map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
-         map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
-apply(induct xs)
+  "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
+   map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
+apply(induct xs arbitrary: "is")
  apply simp
 apply (case_tac "is")
  apply simp
@@ -2405,8 +2402,8 @@
 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
 done
 
-lemma set_sublist: "!!I. set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
-apply(induct xs)
+lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
+apply(induct xs arbitrary: I)
  apply simp
 apply(auto simp add:sublist_Cons nth_Cons split:nat.split elim: lessE)
  apply(erule lessE)
@@ -2428,8 +2425,8 @@
 by (simp add: sublist_Cons)
 
 
-lemma distinct_sublistI[simp]: "!!I. distinct xs \<Longrightarrow> distinct(sublist xs I)"
-apply(induct xs)
+lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
+apply(induct xs arbitrary: I)
  apply simp
 apply(auto simp add:sublist_Cons)
 done
@@ -2440,9 +2437,9 @@
 apply (simp split: nat_diff_split add: sublist_append)
 done
 
-lemma filter_in_sublist: "\<And>s. distinct xs \<Longrightarrow>
-  filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
-proof (induct xs)
+lemma filter_in_sublist:
+ "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
+proof (induct xs arbitrary: s)
   case Nil thus ?case by simp
 next
   case (Cons a xs)
@@ -2463,8 +2460,8 @@
 
 declare splice.simps(2) [simp del, code del]
 
-lemma length_splice[simp]: "!!ys. length(splice xs ys) = length xs + length ys"
-apply(induct xs) apply simp
+lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
+apply(induct xs arbitrary: ys) apply simp
 apply(case_tac ys)
  apply auto
 done
@@ -2601,8 +2598,8 @@
 done
 
 lemma lexn_length:
-     "!!xs ys. (xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
-by (induct n) auto
+  "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
+by (induct n arbitrary: xs ys) auto
 
 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
 apply (unfold lex_def)