# HG changeset patch # User nipkow # Date 1414577003 -3600 # Node ID 5b068376ff2027a768e8c03805ebb350a2091ce6 # Parent bb5ab5fce93af382ac41907755240c0fcc2c50c7 tuned layout and proofs diff -r bb5ab5fce93a -r 5b068376ff20 src/HOL/List.thy --- a/src/HOL/List.thy Tue Oct 28 17:16:22 2014 +0100 +++ b/src/HOL/List.thy Wed Oct 29 11:03:23 2014 +0100 @@ -329,22 +329,20 @@ Nil [iff]: "sorted []" | Cons: "\y\set xs. x \ y \ sorted xs \ sorted (x # xs)" -lemma sorted_single [iff]: - "sorted [x]" - by (rule sorted.Cons) auto - -lemma sorted_many: - "x \ y \ sorted (y # zs) \ sorted (x # y # zs)" - by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto) +lemma sorted_single [iff]: "sorted [x]" +by (rule sorted.Cons) auto + +lemma sorted_many: "x \ y \ sorted (y # zs) \ sorted (x # y # zs)" +by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto) lemma sorted_many_eq [simp, code]: "sorted (x # y # zs) \ x \ y \ sorted (y # zs)" - by (auto intro: sorted_many elim: sorted.cases) +by (auto intro: sorted_many elim: sorted.cases) lemma [code]: "sorted [] \ True" "sorted [x] \ True" - by simp_all +by simp_all primrec insort_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where "insort_key f x [] = [x]" | @@ -738,8 +736,7 @@ "xs \ x # xs" by (induct xs) auto -lemma not_Cons_self2 [simp]: - "x # xs \ xs" +lemma not_Cons_self2 [simp]: "x # xs \ xs" by (rule not_Cons_self [symmetric]) lemma neq_Nil_conv: "(xs \ []) = (\y ys. xs = y # ys)" @@ -815,13 +812,13 @@ by (induct xs) auto lemma Suc_length_conv: -"(Suc n = length xs) = (\y ys. xs = y # ys \ length ys = n)" + "(Suc n = length xs) = (\y ys. xs = y # ys \ length ys = n)" apply (induct xs, simp, simp) apply blast done lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False" - by (induct xs) auto +by (induct xs) auto lemma list_induct2 [consumes 1, case_names Nil Cons]: "length xs = length ys \ P [] [] \ @@ -931,8 +928,8 @@ by (induct xs) auto lemma append_eq_append_conv [simp]: - "length xs = length ys \ length us = length vs - ==> (xs@us = ys@vs) = (xs=ys \ us=vs)" + "length xs = length ys \ length us = length vs + ==> (xs@us = ys@vs) = (xs=ys \ us=vs)" apply (induct xs arbitrary: ys) apply (case_tac ys, simp, force) apply (case_tac ys, force, simp) @@ -1052,13 +1049,11 @@ subsubsection {* @{const map} *} -lemma hd_map: - "xs \ [] \ hd (map f xs) = f (hd xs)" - by (cases xs) simp_all - -lemma map_tl: - "map f (tl xs) = tl (map f xs)" - by (cases xs) simp_all +lemma hd_map: "xs \ [] \ hd (map f xs) = f (hd xs)" +by (cases xs) simp_all + +lemma map_tl: "map f (tl xs) = tl (map f xs)" +by (cases xs) simp_all lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs" by (induct xs) simp_all @@ -1073,9 +1068,7 @@ by (induct xs) auto lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)" -apply(rule ext) -apply(simp) -done +by (rule ext) simp lemma rev_map: "rev (map f xs) = map f (rev xs)" by (induct xs) auto @@ -1085,7 +1078,7 @@ lemma map_cong [fundef_cong]: "xs = ys \ (\x. x \ set ys \ f x = g x) \ map f xs = map g ys" - by simp +by simp lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])" by (cases xs) auto @@ -1094,11 +1087,11 @@ by (cases xs) auto lemma map_eq_Cons_conv: - "(map f xs = y#ys) = (\z zs. xs = z#zs \ f z = y \ map f zs = ys)" + "(map f xs = y#ys) = (\z zs. xs = z#zs \ f z = y \ map f zs = ys)" by (cases xs) auto lemma Cons_eq_map_conv: - "(x#xs = map f ys) = (\z zs. ys = z#zs \ x = f z \ xs = map f zs)" + "(x#xs = map f ys) = (\z zs. ys = z#zs \ x = f z \ xs = map f zs)" by (cases ys) auto lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1] @@ -1134,11 +1127,11 @@ done lemma inj_on_map_eq_map: - "inj_on f (set xs Un set ys) \ (map f xs = map f ys) = (xs = ys)" + "inj_on f (set xs Un set ys) \ (map f xs = map f ys) = (xs = ys)" by(blast dest:map_inj_on) lemma map_injective: - "map f xs = map f ys ==> inj f ==> xs = ys" + "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 \ (map f xs = map f ys) = (xs = ys)" @@ -1441,8 +1434,7 @@ apply simp done -lemma filter_map: - "filter P (map f xs) = map f (filter (P o f) xs)" +lemma filter_map: "filter P (map f xs) = map f (filter (P o f) xs)" by (induct xs) simp_all lemma length_filter_map[simp]: @@ -1464,7 +1456,7 @@ qed lemma length_filter_conv_card: - "length(filter p xs) = card{i. i < length xs & p(xs!i)}" + "length(filter p xs) = card{i. i < length xs & p(xs!i)}" proof (induct xs) case Nil thus ?case by simp next @@ -1498,7 +1490,7 @@ qed lemma Cons_eq_filterD: - "x#xs = filter P ys \ + "x#xs = filter P ys \ \us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs" (is "_ \ \us vs. ?P ys us vs") proof(induct ys) @@ -1526,22 +1518,22 @@ qed lemma filter_eq_ConsD: - "filter P ys = x#xs \ + "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 lemma filter_eq_Cons_iff: - "(filter P ys = x#xs) = + "(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) lemma Cons_eq_filter_iff: - "(x#xs = filter P ys) = + "(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) lemma filter_cong[fundef_cong]: - "xs = ys \ (\x. x \ set ys \ P x = Q x) \ filter P xs = filter Q ys" + "xs = ys \ (\x. x \ set ys \ P x = Q x) \ filter P xs = filter Q ys" apply simp apply(erule thin_rl) by (induct ys) simp_all @@ -1555,12 +1547,10 @@ (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" +lemma partition_filter1: "fst (partition P xs) = filter P xs" by (induct xs) (auto simp add: Let_def split_def) -lemma partition_filter2: - "snd (partition P xs) = filter (Not o P) xs" +lemma partition_filter2: "snd (partition P xs) = filter (Not o P) xs" by (induct xs) (auto simp add: Let_def split_def) lemma partition_P: @@ -1664,7 +1654,7 @@ lemma list_eq_iff_nth_eq: - "(xs = ys) = (length xs = length ys \ (ALL i (ALL i P x" + "[| !i < length xs. P(xs!i); x : set xs|] ==> P x" 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))" + "(\x \ set xs. P x) = (\i. i < length xs --> P (xs ! i))" by (auto simp add: set_conv_nth) lemma rev_nth: @@ -1795,14 +1785,12 @@ 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)" + "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)" by (induct xs arbitrary: i) (auto split: nat.split) lemma list_update_append1: - "i < size xs \ (xs @ ys)[i:=x] = xs[i:=x] @ ys" -apply (induct xs arbitrary: i, simp) -apply(simp split:nat.split) -done + "i < size xs \ (xs @ ys)[i:=x] = xs[i:=x] @ ys" +by (induct xs arbitrary: i)(auto split:nat.split) lemma list_update_append: "(xs @ ys) [n:= x] = @@ -1810,7 +1798,7 @@ by (induct xs arbitrary: n) (auto split:nat.splits) lemma list_update_length [simp]: - "(xs @ x # ys)[length xs := y] = (xs @ y # ys)" + "(xs @ x # ys)[length xs := y] = (xs @ y # ys)" by (induct xs, auto) lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]" @@ -1853,7 +1841,7 @@ "[][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} *} @@ -1865,10 +1853,10 @@ 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) @@ -1902,21 +1890,18 @@ by (induct xs arbitrary: ys) auto lemma append_butlast_last_id [simp]: -"xs \ [] ==> butlast xs @ [last xs] = xs" + "xs \ [] ==> butlast xs @ [last xs] = xs" by (induct xs) auto lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs" by (induct xs) (auto split: split_if_asm) lemma in_set_butlast_appendI: -"x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))" + "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 < length xs \ last (drop n xs) = last xs" -apply (induct xs arbitrary: n) - apply simp -apply (auto split:nat.split) -done +by (induct xs arbitrary: n)(auto split:nat.split) lemma nth_butlast: assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n" @@ -1939,19 +1924,14 @@ lemma butlast_list_update: "butlast(xs[k:=x]) = - (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])" -apply(cases xs rule:rev_cases) -apply simp -apply(simp add:list_update_append split:nat.splits) -done - -lemma last_map: - "xs \ [] \ last (map f xs) = f (last xs)" - by (cases xs rule: rev_cases) simp_all - -lemma map_butlast: - "map f (butlast xs) = butlast (map f xs)" - by (induct xs) simp_all + (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) + +lemma last_map: "xs \ [] \ last (map f xs) = f (last xs)" +by (cases xs rule: rev_cases) simp_all + +lemma map_butlast: "map f (butlast xs) = butlast (map f xs)" +by (induct xs) simp_all lemma snoc_eq_iff_butlast: "xs @ [x] = ys \ (ys \ [] & butlast ys = xs & last ys = x)" @@ -1975,10 +1955,10 @@ declare take_Cons [simp del] and drop_Cons [simp del] lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]" - unfolding One_nat_def by simp +by simp lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs" - unfolding One_nat_def by simp +by simp lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)" by(clarsimp simp add:neq_Nil_conv) @@ -1999,9 +1979,7 @@ by (simp only: drop_tl) lemma nth_via_drop: "drop n xs = y#ys \ xs!n = y" -apply (induct xs arbitrary: n, simp) -apply(simp add:drop_Cons nth_Cons split:nat.splits) -done +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]" @@ -2037,25 +2015,22 @@ 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 xs, auto) apply (case_tac n, auto) done lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs" apply (induct m arbitrary: xs, auto) -apply (case_tac xs, auto) + apply (case_tac xs, auto) done 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) + apply (case_tac xs, auto) done 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 +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" apply (induct n arbitrary: xs, auto) @@ -2063,47 +2038,41 @@ done lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \ xs = [])" -apply(induct xs arbitrary: n) - apply simp -apply(simp add:take_Cons split:nat.split) -done +by(induct xs arbitrary: n)(auto simp: take_Cons split:nat.split) 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 +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)" apply (induct n arbitrary: xs, auto) -apply (case_tac xs, auto) + apply (case_tac xs, auto) done lemma drop_map: "drop n (map f xs) = map f (drop n xs)" apply (induct n arbitrary: xs, auto) -apply (case_tac xs, auto) + apply (case_tac xs, auto) done lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)" apply (induct xs arbitrary: i, auto) -apply (case_tac i, auto) + apply (case_tac i, auto) done lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)" apply (induct xs arbitrary: i, auto) -apply (case_tac i, auto) + apply (case_tac i, auto) done 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 n, blast) apply (case_tac i, auto) done lemma nth_drop [simp]: "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)" apply (induct n arbitrary: xs i, auto) -apply (case_tac xs, auto) + apply (case_tac xs, auto) done lemma butlast_take: @@ -2125,7 +2094,7 @@ lemma set_take_subset_set_take: "m <= n \ set(take m xs) <= set(take n xs)" apply (induct xs arbitrary: m n) -apply simp + apply simp apply (case_tac n) apply (auto simp: take_Cons) done @@ -2139,7 +2108,7 @@ lemma set_drop_subset_set_drop: "m >= n \ set(drop m xs) <= set(drop n xs)" apply(induct xs arbitrary: m n) -apply(auto simp:drop_Cons split:nat.split) + apply(auto simp:drop_Cons split:nat.split) by (metis set_drop_subset subset_iff) lemma in_set_takeD: "x : set(take n xs) \ x : set xs" @@ -2151,17 +2120,16 @@ lemma append_eq_conv_conj: "(xs @ ys = zs) = (xs = take (length xs) zs \ ys = drop (length xs) zs)" apply (induct xs arbitrary: zs, simp, clarsimp) -apply (case_tac zs, auto) + apply (case_tac zs, auto) done -lemma take_add: - "take (i+j) xs = take i xs @ take j (drop i xs)" +lemma take_add: "take (i+j) xs = take i xs @ take j (drop i xs)" apply (induct xs arbitrary: i, auto) -apply (case_tac i, simp_all) + apply (case_tac i, simp_all) done lemma append_eq_append_conv_if: - "(xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>1 @ ys\<^sub>2) = + "(xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>1 @ ys\<^sub>2) = (if size xs\<^sub>1 \ size ys\<^sub>1 then xs\<^sub>1 = take (size xs\<^sub>1) ys\<^sub>1 \ xs\<^sub>2 = drop (size xs\<^sub>1) ys\<^sub>1 @ ys\<^sub>2 else take (size ys\<^sub>1) xs\<^sub>1 = ys\<^sub>1 \ drop (size ys\<^sub>1) xs\<^sub>1 @ xs\<^sub>2 = ys\<^sub>2)" @@ -2174,12 +2142,12 @@ lemma take_hd_drop: "n < length xs \ take n xs @ [hd (drop n xs)] = take (Suc n) xs" apply(induct xs arbitrary: n) -apply simp + apply simp apply(simp add:drop_Cons split:nat.split) done lemma id_take_nth_drop: - "i < length xs \ xs = take i xs @ xs!i # drop (Suc i) xs" + "i < length xs \ xs = take i xs @ xs!i # drop (Suc i) xs" proof - assume si: "i < length xs" hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto @@ -2190,7 +2158,7 @@ qed lemma upd_conv_take_nth_drop: - "i < length xs \ xs[i:=a] = take i xs @ a # drop (Suc i) xs" + "i < length xs \ xs[i:=a] = take i xs @ a # drop (Suc i) xs" proof - assume i: "i < length xs" have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]" @@ -2204,17 +2172,17 @@ subsubsection {* @{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 lemma takeWhile_append1 [simp]: -"[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs" + "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs" by (induct xs) auto lemma takeWhile_append2 [simp]: -"(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys" + "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys" by (induct xs) auto lemma takeWhile_tail: "\ P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs" @@ -2223,18 +2191,19 @@ lemma takeWhile_nth: "j < length (takeWhile P xs) \ takeWhile P xs ! j = xs ! j" apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto -lemma dropWhile_nth: "j < length (dropWhile P xs) \ dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))" +lemma dropWhile_nth: "j < length (dropWhile P xs) \ + dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))" apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto lemma length_dropWhile_le: "length (dropWhile P xs) \ length xs" by (induct xs) auto lemma dropWhile_append1 [simp]: -"[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" + "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys" by (induct xs) auto lemma dropWhile_append2 [simp]: -"(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" + "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" by (induct xs) auto lemma dropWhile_append3: @@ -2252,15 +2221,15 @@ by (induct xs) (auto split: split_if_asm) lemma takeWhile_eq_all_conv[simp]: - "(takeWhile P xs = xs) = (\x \ set xs. P x)" + "(takeWhile P xs = xs) = (\x \ set xs. P x)" by(induct xs, auto) lemma dropWhile_eq_Nil_conv[simp]: - "(dropWhile P xs = []) = (\x \ set xs. P x)" + "(dropWhile P xs = []) = (\x \ set xs. P x)" by(induct xs, auto) lemma dropWhile_eq_Cons_conv: - "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \ P y)" + "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \ P y)" by(induct xs, auto) lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)" @@ -2281,8 +2250,7 @@ lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs" by (induct xs) auto -lemma hd_dropWhile: - "dropWhile P xs \ [] \ \ P (hd (dropWhile P xs))" +lemma hd_dropWhile: "dropWhile P xs \ [] \ \ P (hd (dropWhile P xs))" using assms by (induct xs) auto lemma takeWhile_eq_filter: @@ -2334,7 +2302,7 @@ property. *} lemma takeWhile_neq_rev: "\distinct xs; x \ set xs\ \ - takeWhile (\y. y \ x) (rev xs) = rev (tl (dropWhile (\y. y \ x) xs))" + takeWhile (\y. y \ x) (rev xs) = rev (tl (dropWhile (\y. y \ x) xs))" by(induct xs) (auto simp: takeWhile_tail[where l="[]"]) lemma dropWhile_neq_rev: "\distinct xs; x \ set xs\ \ @@ -2347,7 +2315,7 @@ done lemma takeWhile_not_last: - "distinct xs \ takeWhile (\y. y \ last xs) xs = butlast xs" + "distinct xs \ takeWhile (\y. y \ last xs) xs = butlast xs" apply(induct xs) apply simp apply(case_tac xs) @@ -2366,11 +2334,11 @@ 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} *} @@ -2387,14 +2355,14 @@ "zip [] ys = []" "zip xs [] = []" "zip (x # xs) (y # ys) = (x, y) # zip xs ys" - by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+ +by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+ lemma zip_Cons1: - "zip (x#xs) ys = (case ys of [] \ [] | y#ys \ (x,y)#zip xs ys)" + "zip (x#xs) ys = (case ys of [] \ [] | y#ys \ (x,y)#zip xs ys)" by(auto split:list.split) lemma length_zip [simp]: -"length (zip xs ys) = min (length xs) (length ys)" + "length (zip xs ys) = min (length xs) (length ys)" by (induct xs ys rule:list_induct2') auto lemma zip_obtain_same_length: @@ -2415,22 +2383,22 @@ qed lemma zip_append1: -"zip (xs @ ys) zs = -zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" + "zip (xs @ ys) zs = + zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)" by (induct xs zs rule:list_induct2') auto lemma zip_append2: -"zip xs (ys @ zs) = -zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs" + "zip xs (ys @ zs) = + zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs" by (induct xs ys rule:list_induct2') auto lemma zip_append [simp]: - "[| length xs = length us |] ==> -zip (xs@ys) (us@vs) = zip xs us @ zip ys vs" + "[| length xs = length us |] ==> + zip (xs@ys) (us@vs) = zip xs us @ zip ys vs" by (simp add: zip_append1) lemma zip_rev: -"length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" + "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" by (induct rule:list_induct2, simp_all) lemma zip_map_map: @@ -2454,25 +2422,25 @@ lemma map_zip_map: "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)" -unfolding zip_map1 by auto +by (auto simp: zip_map1) lemma map_zip_map2: "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)" -unfolding zip_map2 by auto +by (auto simp: zip_map2) text{* Courtesy of Andreas Lochbihler: *} lemma zip_same_conv_map: "zip xs xs = map (\x. (x, x)) xs" by(induct xs) auto lemma nth_zip [simp]: -"[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)" + "[| 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 lemma set_zip: -"set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}" + "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}" by(simp add: set_conv_nth cong: rev_conj_cong) lemma zip_same: "((a,b) \ set (zip xs xs)) = (a \ set xs \ a = b)" @@ -2514,30 +2482,27 @@ case (Cons x xs) thus ?case by (cases ys) auto qed simp -lemma set_zip_leftD: - "(x,y)\ set (zip xs ys) \ x \ set xs" +lemma set_zip_leftD: "(x,y)\ set (zip xs ys) \ x \ set xs" by (induct xs ys rule:list_induct2') auto -lemma set_zip_rightD: - "(x,y)\ set (zip xs ys) \ y \ set ys" +lemma set_zip_rightD: "(x,y)\ set (zip xs ys) \ y \ set ys" by (induct xs ys rule:list_induct2') auto lemma in_set_zipE: "(x,y) : set(zip xs ys) \ (\ x : set xs; y : set ys \ \ R) \ R" by(blast dest: set_zip_leftD set_zip_rightD) -lemma zip_map_fst_snd: - "zip (map fst zs) (map snd zs) = zs" - by (induct zs) simp_all +lemma zip_map_fst_snd: "zip (map fst zs) (map snd zs) = zs" +by (induct zs) simp_all lemma zip_eq_conv: "length xs = length ys \ zip xs ys = zs \ map fst zs = xs \ map snd zs = ys" - by (auto simp add: zip_map_fst_snd) +by (auto simp add: zip_map_fst_snd) lemma in_set_zip: "p \ set (zip xs ys) \ (\n. xs ! n = fst p \ ys ! n = snd p - \ n < length xs \ n < length ys)" - by (cases p) (auto simp add: set_zip) + \ n < length xs \ n < length ys)" +by (cases p) (auto simp add: set_zip) lemma pair_list_eqI: assumes "map fst xs = map fst ys" and "map snd xs = map snd ys" @@ -2566,11 +2531,11 @@ by (auto simp add: list_all2_iff) lemma list_all2_Cons1: -"list_all2 P (x # xs) ys = (\z zs. ys = z # zs \ P x z \ list_all2 P xs zs)" + "list_all2 P (x # xs) ys = (\z zs. ys = z # zs \ P x z \ list_all2 P xs zs)" by (cases ys) auto lemma list_all2_Cons2: -"list_all2 P xs (y # ys) = (\z zs. xs = z # zs \ P z y \ list_all2 P zs ys)" + "list_all2 P xs (y # ys) = (\z zs. xs = z # zs \ P z y \ list_all2 P zs ys)" by (cases xs) auto lemma list_all2_induct @@ -2584,17 +2549,17 @@ by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons) lemma list_all2_rev [iff]: -"list_all2 P (rev xs) (rev ys) = list_all2 P xs ys" + "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys" by (simp add: list_all2_iff zip_rev cong: conj_cong) lemma list_all2_rev1: -"list_all2 P (rev xs) ys = list_all2 P xs (rev ys)" + "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)" by (subst list_all2_rev [symmetric]) simp lemma list_all2_append1: -"list_all2 P (xs @ ys) zs = -(EX us vs. zs = us @ vs \ length us = length xs \ length vs = length ys \ -list_all2 P xs us \ list_all2 P ys vs)" + "list_all2 P (xs @ ys) zs = + (EX us vs. zs = us @ vs \ length us = length xs \ length vs = length ys \ + list_all2 P xs us \ list_all2 P ys vs)" apply (simp add: list_all2_iff zip_append1) apply (rule iffI) apply (rule_tac x = "take (length xs) zs" in exI) @@ -2604,9 +2569,9 @@ done lemma list_all2_append2: -"list_all2 P xs (ys @ zs) = -(EX us vs. xs = us @ vs \ length us = length ys \ length vs = length zs \ -list_all2 P us ys \ list_all2 P vs zs)" + "list_all2 P xs (ys @ zs) = + (EX us vs. xs = us @ vs \ length us = length ys \ length vs = length zs \ + list_all2 P us ys \ list_all2 P vs zs)" apply (simp add: list_all2_iff zip_append2) apply (rule iffI) apply (rule_tac x = "take (length ys) xs" in exI) @@ -2625,8 +2590,8 @@ by (simp add: list_all2_append list_all2_lengthD) lemma list_all2_conv_all_nth: -"list_all2 P xs ys = -(length xs = length ys \ (\i < length xs. P (xs!i) (ys!i)))" + "list_all2 P xs ys = + (length xs = length ys \ (\i < length xs. P (xs!i) (ys!i)))" by (force simp add: list_all2_iff set_zip) lemma list_all2_trans: @@ -2710,13 +2675,12 @@ subsubsection {* @{const List.product} and @{const product_lists} *} -lemma set_product[simp]: - "set (List.product xs ys) = set xs \ set ys" - by (induct xs) auto +lemma set_product[simp]: "set (List.product xs ys) = set xs \ set ys" +by (induct xs) auto lemma length_product [simp]: "length (List.product xs ys) = length xs * length ys" - by (induct xs) simp_all +by (induct xs) simp_all lemma product_nth: assumes "n < length xs * length ys" @@ -2732,7 +2696,7 @@ lemma in_set_product_lists_length: "xs \ set (product_lists xss) \ length xs = length xss" - by (induct xss arbitrary: xs) auto +by (induct xss arbitrary: xs) auto lemma product_lists_set: "set (product_lists xss) = {xs. list_all2 (\x ys. x \ set ys) xs xss}" (is "?L = Collect ?R") @@ -2751,28 +2715,25 @@ lemma fold_simps [code]: -- {* eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala *} "fold f [] s = s" "fold f (x # xs) s = fold f xs (f x s)" - by simp_all +by simp_all lemma fold_remove1_split: - assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" - and x: "x \ set xs" - shows "fold f xs = fold f (remove1 x xs) \ f x" - using assms by (induct xs) (auto simp add: comp_assoc) + "\ \x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x; + x \ set xs \ + \ fold f xs = fold f (remove1 x xs) \ f x" +by (induct xs) (auto simp add: comp_assoc) lemma fold_cong [fundef_cong]: "a = b \ xs = ys \ (\x. x \ set xs \ f x = g x) \ fold f xs a = fold g ys b" - by (induct ys arbitrary: a b xs) simp_all - -lemma fold_id: - assumes "\x. x \ set xs \ f x = id" - shows "fold f xs = id" - using assms by (induct xs) simp_all +by (induct ys arbitrary: a b xs) simp_all + +lemma fold_id: "(\x. x \ set xs \ f x = id) \ fold f xs = id" +by (induct xs) simp_all lemma fold_commute: - assumes "\x. x \ set xs \ h \ g x = f x \ h" - shows "h \ fold g xs = fold f xs \ h" - using assms by (induct xs) (simp_all add: fun_eq_iff) + "(\x. x \ set xs \ h \ g x = f x \ h) \ h \ fold g xs = fold f xs \ h" +by (induct xs) (simp_all add: fun_eq_iff) lemma fold_commute_apply: assumes "\x. x \ set xs \ h \ g x = f x \ h" @@ -2783,52 +2744,45 @@ qed lemma fold_invariant: - assumes "\x. x \ set xs \ Q x" and "P s" - and "\x s. Q x \ P s \ P (f x s)" - shows "P (fold f xs s)" - using assms by (induct xs arbitrary: s) simp_all - -lemma fold_append [simp]: - "fold f (xs @ ys) = fold f ys \ fold f xs" - by (induct xs) simp_all - -lemma fold_map [code_unfold]: - "fold g (map f xs) = fold (g o f) xs" - by (induct xs) simp_all + "\ \x. x \ set xs \ Q x; P s; \x s. Q x \ P s \ P (f x s) \ + \ P (fold f xs s)" +by (induct xs arbitrary: s) simp_all + +lemma fold_append [simp]: "fold f (xs @ ys) = fold f ys \ fold f xs" +by (induct xs) simp_all + +lemma fold_map [code_unfold]: "fold g (map f xs) = fold (g o f) xs" +by (induct xs) simp_all lemma fold_filter: "fold f (filter P xs) = fold (\x. if P x then f x else id) xs" - by (induct xs) simp_all +by (induct xs) simp_all lemma fold_rev: - assumes "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ f y" - shows "fold f (rev xs) = fold f xs" -using assms by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff) - -lemma fold_Cons_rev: - "fold Cons xs = append (rev xs)" - by (induct xs) simp_all - -lemma rev_conv_fold [code]: - "rev xs = fold Cons xs []" - by (simp add: fold_Cons_rev) - -lemma fold_append_concat_rev: - "fold append xss = append (concat (rev xss))" - by (induct xss) simp_all + "(\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ f y) + \ fold f (rev xs) = fold f xs" +by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff) + +lemma fold_Cons_rev: "fold Cons xs = append (rev xs)" +by (induct xs) simp_all + +lemma rev_conv_fold [code]: "rev xs = fold Cons xs []" +by (simp add: fold_Cons_rev) + +lemma fold_append_concat_rev: "fold append xss = append (concat (rev xss))" +by (induct xss) simp_all text {* @{const Finite_Set.fold} and @{const fold} *} lemma (in comp_fun_commute) fold_set_fold_remdups: "Finite_Set.fold f y (set xs) = fold f (remdups xs) y" - by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb) +by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm insert_absorb) lemma (in comp_fun_idem) fold_set_fold: "Finite_Set.fold f y (set xs) = fold f xs y" - by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm) - -lemma union_set_fold [code]: - "set xs \ A = fold Set.insert xs A" +by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm) + +lemma union_set_fold [code]: "set xs \ A = fold Set.insert xs A" proof - interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) @@ -2837,10 +2791,9 @@ lemma union_coset_filter [code]: "List.coset xs \ A = List.coset (List.filter (\x. x \ A) xs)" - by auto - -lemma minus_set_fold [code]: - "A - set xs = fold Set.remove xs A" +by auto + +lemma minus_set_fold [code]: "A - set xs = fold Set.remove xs A" proof - interpret comp_fun_idem Set.remove by (fact comp_fun_idem_remove) @@ -2850,15 +2803,15 @@ lemma minus_coset_filter [code]: "A - List.coset xs = set (List.filter (\x. x \ A) xs)" - by auto +by auto lemma inter_set_filter [code]: "A \ set xs = set (List.filter (\x. x \ A) xs)" - by auto +by auto lemma inter_coset_fold [code]: "A \ List.coset xs = fold Set.remove xs A" - by (simp add: Diff_eq [symmetric] minus_set_fold) +by (simp add: Diff_eq [symmetric] minus_set_fold) lemma (in semilattice_set) set_eq_fold [code]: "F (set (x # xs)) = fold f xs x" @@ -2905,58 +2858,53 @@ text {* Correspondence *} -lemma foldr_conv_fold [code_abbrev]: - "foldr f xs = fold f (rev xs)" - by (induct xs) simp_all - -lemma foldl_conv_fold: - "foldl f s xs = fold (\x s. f s x) xs s" - by (induct xs arbitrary: s) simp_all +lemma foldr_conv_fold [code_abbrev]: "foldr f xs = fold f (rev xs)" +by (induct xs) simp_all + +lemma foldl_conv_fold: "foldl f s xs = fold (\x s. f s x) xs s" +by (induct xs arbitrary: s) simp_all lemma foldr_conv_foldl: -- {* The ``Third Duality Theorem'' in Bird \& Wadler: *} "foldr f xs a = foldl (\x y. f y x) a (rev xs)" - by (simp add: foldr_conv_fold foldl_conv_fold) +by (simp add: foldr_conv_fold foldl_conv_fold) lemma foldl_conv_foldr: "foldl f a xs = foldr (\x y. f y x) (rev xs) a" - by (simp add: foldr_conv_fold foldl_conv_fold) +by (simp add: foldr_conv_fold foldl_conv_fold) lemma foldr_fold: - assumes "\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ f y" - shows "foldr f xs = fold f xs" - using assms unfolding foldr_conv_fold by (rule fold_rev) + "(\x y. x \ set xs \ y \ set xs \ f y \ f x = f x \ f y) + \ foldr f xs = fold f xs" +unfolding foldr_conv_fold by (rule fold_rev) lemma foldr_cong [fundef_cong]: "a = b \ l = k \ (\a x. x \ set l \ f x a = g x a) \ foldr f l a = foldr g k b" - by (auto simp add: foldr_conv_fold intro!: fold_cong) +by (auto simp add: foldr_conv_fold intro!: fold_cong) lemma foldl_cong [fundef_cong]: "a = b \ l = k \ (\a x. x \ set l \ f a x = g a x) \ foldl f a l = foldl g b k" - by (auto simp add: foldl_conv_fold intro!: fold_cong) - -lemma foldr_append [simp]: - "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" - by (simp add: foldr_conv_fold) - -lemma foldl_append [simp]: - "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" - by (simp add: foldl_conv_fold) - -lemma foldr_map [code_unfold]: - "foldr g (map f xs) a = foldr (g o f) xs a" - by (simp add: foldr_conv_fold fold_map rev_map) +by (auto simp add: foldl_conv_fold intro!: fold_cong) + +lemma foldr_append [simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)" +by (simp add: foldr_conv_fold) + +lemma foldl_append [simp]: "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys" +by (simp add: foldl_conv_fold) + +lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g o f) xs a" +by (simp add: foldr_conv_fold fold_map rev_map) lemma foldr_filter: "foldr f (filter P xs) = foldr (\x. if P x then f x else id) xs" - by (simp add: foldr_conv_fold rev_filter fold_filter) +by (simp add: foldr_conv_fold rev_filter fold_filter) lemma foldl_map [code_unfold]: "foldl g a (map f xs) = foldl (\a x. g a (f x)) a xs" - by (simp add: foldl_conv_fold fold_map comp_def) +by (simp add: foldl_conv_fold fold_map comp_def) lemma concat_conv_foldr [code]: "concat xss = foldr append xss []" - by (simp add: fold_append_concat_rev foldr_conv_fold) +by (simp add: fold_append_concat_rev foldr_conv_fold) subsubsection {* @{const upt} *} @@ -2986,7 +2934,7 @@ by simp lemma upt_conv_Cons: "i < j ==> [i.. [i.. [i.. hd[i.. last[i.. take m [i..i. i + n) [0.. (map f [m..n. n - Suc 0) [Suc m..n. n - Suc 0) [Suc m.. xs = ys" - by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all + "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys" +by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all lemma map_nth: "map (\