# HG changeset patch
# User paulson
# Date 1533338355 -3600
# Node ID 8aedca31957d5409522186f49e2d7b178ceee520
# Parent 6d9eca4805ff91f6ee3f0e8dbdd1ce10eca83d02
de-applying
diff -r 6d9eca4805ff -r 8aedca31957d src/HOL/List.thy
--- a/src/HOL/List.thy Wed Aug 01 22:59:42 2018 +0100
+++ b/src/HOL/List.thy Sat Aug 04 00:19:15 2018 +0100
@@ -1242,7 +1242,7 @@
lemma rev_induct [case_names Nil snoc]:
"[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(simplesubst rev_rev_ident[symmetric])
+apply(subst rev_rev_ident[symmetric])
apply(rule_tac list = "rev xs" in list.induct, simp_all)
done
@@ -1489,8 +1489,7 @@
case Nil thus ?case by simp
next
case (Cons x xs) thus ?case
- apply (auto split:if_split_asm)
- using length_filter_le[of P xs] by arith
+ using Suc_le_eq by fastforce
qed
lemma length_filter_conv_card:
@@ -1558,17 +1557,17 @@
lemma filter_eq_ConsD:
"filter P ys = x#xs \
\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs"
-by(rule Cons_eq_filterD) simp
+ by(rule Cons_eq_filterD) simp
lemma filter_eq_Cons_iff:
"(filter P ys = x#xs) =
(\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)"
-by(auto dest:filter_eq_ConsD)
+ by(auto dest:filter_eq_ConsD)
lemma Cons_eq_filter_iff:
"(x#xs = filter P ys) =
(\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)"
-by(auto dest:Cons_eq_filterD)
+ by(auto dest:Cons_eq_filterD)
lemma inj_on_filter_key_eq:
assumes "inj_on f (insert y (set xs))"
@@ -1583,16 +1582,16 @@
subsubsection \List partitioning\
primrec partition :: "('a \ bool) \'a list \ 'a list \ 'a list" where
-"partition P [] = ([], [])" |
-"partition P (x # xs) =
+ "partition P [] = ([], [])" |
+ "partition P (x # xs) =
(let (yes, no) = partition P xs
in if P x then (x # yes, no) else (yes, x # no))"
lemma partition_filter1: "fst (partition P xs) = filter P xs"
-by (induct xs) (auto simp add: Let_def split_def)
+ by (induct xs) (auto simp add: Let_def split_def)
lemma partition_filter2: "snd (partition P xs) = filter (Not \ P) xs"
-by (induct xs) (auto simp add: Let_def split_def)
+ by (induct xs) (auto simp add: Let_def split_def)
lemma partition_P:
assumes "partition P xs = (yes, no)"
@@ -1614,8 +1613,8 @@
lemma partition_filter_conv[simp]:
"partition f xs = (filter f xs,filter (Not \ f) xs)"
-unfolding partition_filter2[symmetric]
-unfolding partition_filter1[symmetric] by simp
+ unfolding partition_filter2[symmetric]
+ unfolding partition_filter1[symmetric] by simp
declare partition.simps[simp del]
@@ -1623,28 +1622,28 @@
subsubsection \@{const concat}\
lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\xs \ set xss. xs = [])"
-by (induct xss) auto
+ by (induct xss) auto
lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\xs \ set xss. xs = [])"
-by (induct xss) auto
+ by (induct xss) auto
lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
-by (induct xs) auto
+ by (induct xs) auto
lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
-by (induct xs) auto
+ by (induct xs) auto
lemma concat_eq_concat_iff: "\(x, y) \ set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)"
proof (induct xs arbitrary: ys)
@@ -1653,21 +1652,21 @@
qed (auto)
lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \(x, y) \ set (zip xs ys). length x = length y ==> xs = ys"
-by (simp add: concat_eq_concat_iff)
+ by (simp add: concat_eq_concat_iff)
subsubsection \@{const nth}\
lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
-by auto
+ by auto
lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
-by auto
+ by auto
declare nth.simps [simp del]
lemma nth_Cons_pos[simp]: "0 < n \ (x#xs) ! n = xs ! (n - 1)"
-by(auto simp: Nat.gr0_conv_Suc)
+ by(auto simp: Nat.gr0_conv_Suc)
lemma nth_append:
"(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
@@ -1678,10 +1677,10 @@
qed simp
lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
-by (induct xs) auto
+ by (induct xs) auto
lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
-by (induct xs) auto
+ by (induct xs) auto
lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
proof (induct xs arbitrary: n)
@@ -1691,10 +1690,10 @@
qed simp
lemma nth_tl: "n < length (tl xs) \ tl xs ! n = xs ! Suc n"
-by (induction xs) auto
+ by (induction xs) auto
lemma hd_conv_nth: "xs \ [] \ hd xs = xs!0"
-by(cases xs) simp_all
+ by(cases xs) simp_all
lemma list_eq_iff_nth_eq:
@@ -1724,7 +1723,7 @@
qed simp
lemma in_set_conv_nth: "(x \ set xs) = (\i < length xs. xs!i = x)"
-by(auto simp:set_conv_nth)
+ by(auto simp:set_conv_nth)
lemma nth_equal_first_eq:
assumes "x \ set xs"
@@ -1756,18 +1755,18 @@
qed
lemma list_ball_nth: "\n < length xs; \x \ set xs. P x\ \ P(xs!n)"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma nth_mem [simp]: "n < length xs \ xs!n \ set xs"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma all_nth_imp_all_set:
"\\i < length xs. P(xs!i); x \ set xs\ \ P x"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma all_set_conv_all_nth:
"(\x \ set xs. P x) = (\i. i < length xs \ P (xs ! i))"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma rev_nth:
"n < size xs \ rev xs ! n = xs ! (length xs - Suc n)"
@@ -1811,20 +1810,20 @@
subsubsection \@{const list_update}\
lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
-by (induct xs arbitrary: i) (auto split: nat.split)
+ by (induct xs arbitrary: i) (auto split: nat.split)
lemma nth_list_update:
-"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)
+ "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)
+ by (simp add: nth_list_update)
lemma nth_list_update_neq [simp]: "i \ j ==> xs[i:=x]!j = xs!j"
-by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
+ by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
lemma list_update_id[simp]: "xs[i := xs!i] = xs"
-by (induct xs arbitrary: i) (simp_all split:nat.splits)
+ by (induct xs arbitrary: i) (simp_all split:nat.splits)
lemma list_update_beyond[simp]: "length xs \ i \ xs[i:=x] = xs"
proof (induct xs arbitrary: i)
@@ -1834,44 +1833,44 @@
qed simp
lemma list_update_nonempty[simp]: "xs[k:=x] = [] \ xs=[]"
-by (simp only: length_0_conv[symmetric] length_list_update)
+ by (simp only: length_0_conv[symmetric] length_list_update)
lemma list_update_same_conv:
"i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
-by (induct xs arbitrary: i) (auto split: nat.split)
+ by (induct xs arbitrary: i) (auto split: nat.split)
lemma list_update_append1:
"i < size xs \ (xs @ ys)[i:=x] = xs[i:=x] @ ys"
-by (induct xs arbitrary: i)(auto split:nat.split)
+ by (induct xs arbitrary: i)(auto split:nat.split)
lemma list_update_append:
"(xs @ ys) [n:= x] =
(if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
-by (induct xs arbitrary: n) (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)
+ by (induct xs, auto)
lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
-by(induct xs arbitrary: k)(auto split:nat.splits)
+ by(induct xs arbitrary: k)(auto split:nat.splits)
lemma rev_update:
"k < length xs \ rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
-by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
+ by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
lemma update_zip:
"(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)
+ 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)
+ 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])
+ by (blast dest!: set_update_subset_insert [THEN subsetD])
lemma set_update_memI: "n < length xs \ x \ set (xs[n := x])"
-by (induct xs arbitrary: n) (auto split:nat.splits)
+ by (induct xs arbitrary: n) (auto split:nat.splits)
lemma list_update_overwrite[simp]:
"xs [i := x, i := y] = xs [i := y]"
@@ -1885,67 +1884,67 @@
"[][i := y] = []"
"(x # xs)[0 := y] = y # xs"
"(x # xs)[Suc i := y] = x # xs[i := y]"
-by simp_all
+ by simp_all
subsubsection \@{const last} and @{const butlast}\
lemma last_snoc [simp]: "last (xs @ [x]) = x"
-by (induct xs) auto
+ by (induct xs) auto
lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma last_ConsL: "xs = [] \ last(x#xs) = x"
-by simp
+ by simp
lemma last_ConsR: "xs \ [] \ last(x#xs) = last xs"
-by simp
+ by simp
lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
-by (induct xs) (auto)
+ by (induct xs) (auto)
lemma last_appendL[simp]: "ys = [] \ last(xs @ ys) = last xs"
-by(simp add:last_append)
+ by(simp add:last_append)
lemma last_appendR[simp]: "ys \ [] \ last(xs @ ys) = last ys"
-by(simp add:last_append)
+ by(simp add:last_append)
lemma last_tl: "xs = [] \ tl xs \ [] \last (tl xs) = last xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma hd_rev: "xs \ [] \ hd(rev xs) = last xs"
-by(rule rev_exhaust[of xs]) simp_all
+ by(rule rev_exhaust[of xs]) simp_all
lemma last_rev: "xs \ [] \ last(rev xs) = hd xs"
-by(cases xs) simp_all
+ by(cases xs) simp_all
lemma last_in_set[simp]: "as \ [] \ last as \ set as"
-by (induct as) auto
+ by (induct as) auto
lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
-by (induct xs rule: rev_induct) auto
+ by (induct xs rule: rev_induct) auto
lemma butlast_append:
"butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
-by (induct xs arbitrary: ys) auto
+ by (induct xs arbitrary: ys) auto
lemma append_butlast_last_id [simp]:
"xs \ [] \ butlast xs @ [last xs] = xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma in_set_butlastD: "x \ set (butlast xs) \ x \ set xs"
-by (induct xs) (auto split: if_split_asm)
+ by (induct xs) (auto split: if_split_asm)
lemma in_set_butlast_appendI:
"x \ set (butlast xs) \ x \ set (butlast ys) \ x \ set (butlast (xs @ ys))"
-by (auto dest: in_set_butlastD simp add: butlast_append)
+ by (auto dest: in_set_butlastD simp add: butlast_append)
lemma last_drop[simp]: "n < length xs \ last (drop n xs) = last xs"
-by (induct xs arbitrary: n)(auto split:nat.split)
+ by (induct xs arbitrary: n)(auto split:nat.split)
lemma nth_butlast:
assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n"
@@ -1957,82 +1956,82 @@
qed simp
lemma last_conv_nth: "xs\[] \ last xs = xs!(length xs - 1)"
-by(induct xs)(auto simp:neq_Nil_conv)
+ by(induct xs)(auto simp:neq_Nil_conv)
lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
-by (induction xs rule: induct_list012) simp_all
+ by (induction xs rule: induct_list012) simp_all
lemma last_list_update:
"xs \ [] \ last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
-by (auto simp: last_conv_nth)
+ by (auto simp: last_conv_nth)
lemma butlast_list_update:
"butlast(xs[k:=x]) =
(if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
-by(cases xs rule:rev_cases)(auto simp: list_update_append split: nat.splits)
+ by(cases xs rule:rev_cases)(auto simp: list_update_append split: nat.splits)
lemma last_map: "xs \ [] \ last (map f xs) = f (last xs)"
-by (cases xs rule: rev_cases) simp_all
+ by (cases xs rule: rev_cases) simp_all
lemma map_butlast: "map f (butlast xs) = butlast (map f xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma snoc_eq_iff_butlast:
"xs @ [x] = ys \ (ys \ [] \ butlast ys = xs \ last ys = x)"
-by fastforce
+ by fastforce
corollary longest_common_suffix:
"\ss xs' ys'. xs = xs' @ ss \ ys = ys' @ ss
\ (xs' = [] \ ys' = [] \ last xs' \ last ys')"
-using longest_common_prefix[of "rev xs" "rev ys"]
-unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
+ using longest_common_prefix[of "rev xs" "rev ys"]
+ unfolding rev_swap rev_append by (metis last_rev rev_is_Nil_conv)
subsubsection \@{const take} and @{const drop}\
lemma take_0: "take 0 xs = []"
-by (induct xs) auto
+ by (induct xs) auto
lemma drop_0: "drop 0 xs = xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma take0[simp]: "take 0 = (\xs. [])"
-by(rule ext) (rule take_0)
+ by(rule ext) (rule take_0)
lemma drop0[simp]: "drop 0 = (\x. x)"
-by(rule ext) (rule drop_0)
+ by(rule ext) (rule drop_0)
lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
-by simp
+ by simp
lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
-by simp
+ by simp
declare take_Cons [simp del] and drop_Cons [simp del]
lemma take_Suc: "xs \ [] \ take (Suc n) xs = hd xs # take n (tl xs)"
-by(clarsimp simp add:neq_Nil_conv)
+ by(clarsimp simp add:neq_Nil_conv)
lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
-by(cases xs, simp_all)
+ by(cases xs, simp_all)
lemma hd_take[simp]: "j > 0 \ hd (take j xs) = hd xs"
-by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
+ by (metis gr0_conv_Suc list.sel(1) take.simps(1) take_Suc)
lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
-by (induct xs arbitrary: n) simp_all
+ by (induct xs arbitrary: n) simp_all
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)
+ by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
-by (cases n, simp, cases xs, auto)
+ by (cases n, simp, cases xs, auto)
lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
-by (simp only: drop_tl)
+ by (simp only: drop_tl)
lemma nth_via_drop: "drop n xs = y#ys \ xs!n = y"
-by (induct xs arbitrary: n, simp)(auto simp: drop_Cons nth_Cons split: nat.splits)
+ by (induct xs arbitrary: n, simp)(auto simp: drop_Cons nth_Cons split: nat.splits)
lemma take_Suc_conv_app_nth:
"i < length xs \ take (Suc i) xs = take i xs @ [xs!i]"
@@ -2049,24 +2048,24 @@
qed simp
lemma length_take [simp]: "length (take n xs) = min (length xs) n"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+ 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)
+ 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)
+ 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)
+ by (induct n arbitrary: xs) (auto, case_tac xs, auto)
lemma take_append [simp]:
"take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+ by (induct n arbitrary: xs) (auto, case_tac xs, auto)
lemma drop_append [simp]:
"drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
-by (induct n arbitrary: xs) (auto, case_tac xs, auto)
+ by (induct n arbitrary: xs) (auto, case_tac xs, auto)
lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
proof (induct m arbitrary: xs n)
@@ -2087,7 +2086,7 @@
qed auto
lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
-by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
+ by(induct xs arbitrary: m n)(auto simp: take_Cons drop_Cons split: nat.split)
lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
proof (induct n arbitrary: xs)
@@ -2096,10 +2095,10 @@
qed auto
lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \ xs = [])"
-by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
+ by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split)
lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs \ n)"
-by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
+ by (induct xs arbitrary: n) (auto simp: drop_Cons split:nat.split)
lemma take_map: "take n (map f xs) = map f (take n xs)"
proof (induct n arbitrary: xs)
@@ -2146,19 +2145,19 @@
lemma butlast_take:
"n \ length xs ==> butlast (take n xs) = take (n - 1) xs"
-by (simp add: butlast_conv_take min.absorb1 min.absorb2)
+ by (simp add: butlast_conv_take min.absorb1 min.absorb2)
lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
-by (simp add: butlast_conv_take drop_take ac_simps)
+ by (simp add: butlast_conv_take drop_take ac_simps)
lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
-by (simp add: butlast_conv_take min.absorb1)
+ by (simp add: butlast_conv_take min.absorb1)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
-by (simp add: butlast_conv_take drop_take ac_simps)
+ by (simp add: butlast_conv_take drop_take ac_simps)
lemma hd_drop_conv_nth: "n < length xs \ hd(drop n xs) = xs!n"
-by(simp add: hd_conv_nth)
+ by(simp add: hd_conv_nth)
lemma set_take_subset_set_take:
"m \ n \ set(take m xs) \ set(take n xs)"
@@ -2168,10 +2167,10 @@
qed simp
lemma set_take_subset: "set(take n xs) \ set xs"
-by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
+ by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
lemma set_drop_subset: "set(drop n xs) \ set xs"
-by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
+ by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
lemma set_drop_subset_set_drop:
"m \ n \ set(drop m xs) \ set(drop n xs)"
@@ -2182,10 +2181,10 @@
qed simp
lemma in_set_takeD: "x \ set(take n xs) \ x \ set xs"
-using set_take_subset by fast
+ using set_take_subset by fast
lemma in_set_dropD: "x \ set(drop n xs) \ x \ set xs"
-using set_drop_subset by fast
+ using set_drop_subset by fast
lemma append_eq_conv_conj:
"(xs @ ys = zs) = (xs = take (length xs) zs \ ys = drop (length xs) zs)"
@@ -2226,10 +2225,10 @@
qed
lemma take_update_cancel[simp]: "n \ m \ take n (xs[m := y]) = take n xs"
-by(simp add: list_eq_iff_nth_eq)
+ by(simp add: list_eq_iff_nth_eq)
lemma drop_update_cancel[simp]: "n < m \ drop m (xs[n := x]) = drop m xs"
-by(simp add: list_eq_iff_nth_eq)
+ by(simp add: list_eq_iff_nth_eq)
lemma upd_conv_take_nth_drop:
"i < length xs \ xs[i:=a] = take i xs @ a # drop (Suc i) xs"
@@ -2258,27 +2257,27 @@
qed auto
lemma nth_image: "l \ size xs \ nth xs ` {0..@{const takeWhile} and @{const dropWhile}\
lemma length_takeWhile_le: "length (takeWhile P xs) \ length xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_append1 [simp]:
"\x \ set xs; \P(x)\ \ takeWhile P (xs @ ys) = takeWhile P xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_append2 [simp]:
"(\x. x \ set xs \ P x) \ takeWhile P (xs @ ys) = xs @ takeWhile P ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_tail: "\ P x \ takeWhile P (xs @ (x#l)) = takeWhile P xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_nth: "j < length (takeWhile P xs) \ takeWhile P xs ! j = xs ! j"
by (metis nth_append takeWhile_dropWhile_id)
@@ -2288,62 +2287,62 @@
by (metis add.commute nth_append_length_plus takeWhile_dropWhile_id)
lemma length_dropWhile_le: "length (dropWhile P xs) \ length xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_append1 [simp]:
"\x \ set xs; \P(x)\ \ dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_append2 [simp]:
"(\x. x \ set xs \ P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_append3:
"\ P y \dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_last:
"x \ set xs \ \ P x \ last (dropWhile P xs) = last xs"
-by (auto simp add: dropWhile_append3 in_set_conv_decomp)
+ by (auto simp add: dropWhile_append3 in_set_conv_decomp)
lemma set_dropWhileD: "x \ set (dropWhile P xs) \ x \ set xs"
-by (induct xs) (auto split: if_split_asm)
+ by (induct xs) (auto split: if_split_asm)
lemma set_takeWhileD: "x \ set (takeWhile P xs) \ x \ set xs \ P x"
-by (induct xs) (auto split: if_split_asm)
+ by (induct xs) (auto split: if_split_asm)
lemma takeWhile_eq_all_conv[simp]:
"(takeWhile P xs = xs) = (\x \ set xs. P x)"
-by(induct xs, auto)
+ by(induct xs, auto)
lemma dropWhile_eq_Nil_conv[simp]:
"(dropWhile P xs = []) = (\x \ set xs. P x)"
-by(induct xs, auto)
+ by(induct xs, auto)
lemma dropWhile_eq_Cons_conv:
"(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \ \ P y)"
-by(induct xs, auto)
+ by(induct xs, auto)
lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
-by (induct xs) (auto dest: set_takeWhileD)
+ by (induct xs) (auto dest: set_takeWhileD)
lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \ f) xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \ f) xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma hd_dropWhile: "dropWhile P xs \ [] \ \ P (hd (dropWhile P xs))"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_eq_filter:
assumes "\ x. x \ set (dropWhile P xs) \ \ P x"
@@ -2384,12 +2383,12 @@
thus "\ P (xs ! n')" using Cons by auto
qed
ultimately show ?thesis by simp
- qed
+ qed
qed
lemma nth_length_takeWhile:
"length (takeWhile P xs) < length xs \ \ P (xs ! length (takeWhile P xs))"
-by (induct xs) auto
+ by (induct xs) auto
lemma length_takeWhile_less_P_nth:
assumes all: "\ i. i < j \ P (xs ! i)" and "j \ length xs"
@@ -2402,7 +2401,7 @@
lemma takeWhile_neq_rev: "\distinct xs; x \ set xs\ \
takeWhile (\y. y \ x) (rev xs) = rev (tl (dropWhile (\y. y \ x) xs))"
-by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
+ by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
lemma dropWhile_neq_rev: "\distinct xs; x \ set xs\ \
dropWhile (\y. y \ x) (rev xs) = x # rev (takeWhile (\y. y \ x) xs)"
@@ -2414,34 +2413,34 @@
lemma takeWhile_not_last:
"distinct xs \ takeWhile (\y. y \ last xs) xs = butlast xs"
-by(induction xs rule: induct_list012) auto
+ by(induction xs rule: induct_list012) auto
lemma takeWhile_cong [fundef_cong]:
"\l = k; \x. x \ set l \ P x = Q x\
\ takeWhile P l = takeWhile Q k"
-by (induct k arbitrary: l) (simp_all)
+ by (induct k arbitrary: l) (simp_all)
lemma dropWhile_cong [fundef_cong]:
"\l = k; \x. x \ set l \ P x = Q x\
\ dropWhile P l = dropWhile Q k"
-by (induct k arbitrary: l, simp_all)
+ by (induct k arbitrary: l, simp_all)
lemma takeWhile_idem [simp]:
"takeWhile P (takeWhile P xs) = takeWhile P xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_idem [simp]:
"dropWhile P (dropWhile P xs) = dropWhile P xs"
-by (induct xs) auto
+ by (induct xs) auto
subsubsection \@{const zip}\