summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/List.thy

changeset 24526 | 7fa202789bf6 |

parent 24476 | f7ad9fbbeeaa |

child 24566 | 2bfa0215904c |

--- 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)