--- a/src/HOL/List.thy Fri Aug 03 21:38:54 2018 +0200
+++ b/src/HOL/List.thy Sat Aug 04 00:19:23 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 \<Longrightarrow>
\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> 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) =
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> 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) =
(\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> 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 \<open>List partitioning\<close>
primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> '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 \<circ> 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 \<circ> 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 \<open>@{const concat}\<close>
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 = []) = (\<forall>xs \<in> set xss. xs = [])"
-by (induct xss) auto
+ by (induct xss) auto
lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> 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: "\<forall>(x, y) \<in> 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 ==> \<forall>(x, y) \<in> 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 \<open>@{const nth}\<close>
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 \<Longrightarrow> (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) \<Longrightarrow> tl xs ! n = xs ! Suc n"
-by (induction xs) auto
+ by (induction xs) auto
lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> 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 \<in> set xs) = (\<exists>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 \<notin> set xs"
@@ -1756,18 +1755,18 @@
qed
lemma list_ball_nth: "\<lbrakk>n < length xs; \<forall>x \<in> set xs. P x\<rbrakk> \<Longrightarrow> P(xs!n)"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma nth_mem [simp]: "n < length xs \<Longrightarrow> xs!n \<in> set xs"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma all_nth_imp_all_set:
"\<lbrakk>\<forall>i < length xs. P(xs!i); x \<in> set xs\<rbrakk> \<Longrightarrow> P x"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma all_set_conv_all_nth:
"(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
-by (auto simp add: set_conv_nth)
+ by (auto simp add: set_conv_nth)
lemma rev_nth:
"n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
@@ -1811,20 +1810,20 @@
subsubsection \<open>@{const list_update}\<close>
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 \<noteq> 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 \<le> i \<Longrightarrow> xs[i:=x] = xs"
proof (induct xs arbitrary: i)
@@ -1834,44 +1833,44 @@
qed simp
lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> 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 \<Longrightarrow> (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 \<Longrightarrow> 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]) \<le> 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: "\<lbrakk>set xs \<subseteq> A; x \<in> A\<rbrakk> \<Longrightarrow> set(xs[i := x]) \<subseteq> 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 \<Longrightarrow> x \<in> 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 \<open>@{const last} and @{const butlast}\<close>
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 = [] \<Longrightarrow> last(x#xs) = x"
-by simp
+ by simp
lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> 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 = [] \<Longrightarrow> last(xs @ ys) = last xs"
-by(simp add:last_append)
+ by(simp add:last_append)
lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
-by(simp add:last_append)
+ by(simp add:last_append)
lemma last_tl: "xs = [] \<or> tl xs \<noteq> [] \<Longrightarrow>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 \<noteq> [] \<Longrightarrow> 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 \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
-by(cases xs) simp_all
+ by(cases xs) simp_all
lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> 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 \<noteq> [] \<Longrightarrow> butlast xs @ [last xs] = xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma in_set_butlastD: "x \<in> set (butlast xs) \<Longrightarrow> x \<in> set xs"
-by (induct xs) (auto split: if_split_asm)
+ by (induct xs) (auto split: if_split_asm)
lemma in_set_butlast_appendI:
"x \<in> set (butlast xs) \<or> x \<in> set (butlast ys) \<Longrightarrow> x \<in> 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 \<Longrightarrow> 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\<noteq>[] \<Longrightarrow> 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 \<noteq> [] \<Longrightarrow> 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 \<noteq> [] \<Longrightarrow> 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 \<longleftrightarrow> (ys \<noteq> [] \<and> butlast ys = xs \<and> last ys = x)"
-by fastforce
+ by fastforce
corollary longest_common_suffix:
"\<exists>ss xs' ys'. xs = xs' @ ss \<and> ys = ys' @ ss
\<and> (xs' = [] \<or> ys' = [] \<or> last xs' \<noteq> 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 \<open>@{const take} and @{const drop}\<close>
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 = (\<lambda>xs. [])"
-by(rule ext) (rule take_0)
+ by(rule ext) (rule take_0)
lemma drop0[simp]: "drop 0 = (\<lambda>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 \<noteq> [] \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> 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 \<le> 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 \<le> 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 \<or> 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 \<le> 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 \<le> 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 \<Longrightarrow> 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 \<le> n \<Longrightarrow> set(take m xs) \<le> set(take n xs)"
@@ -2168,10 +2167,10 @@
qed simp
lemma set_take_subset: "set(take n xs) \<subseteq> 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) \<subseteq> 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 \<ge> n \<Longrightarrow> set(drop m xs) \<le> set(drop n xs)"
@@ -2182,10 +2181,10 @@
qed simp
lemma in_set_takeD: "x \<in> set(take n xs) \<Longrightarrow> x \<in> set xs"
-using set_take_subset by fast
+ using set_take_subset by fast
lemma in_set_dropD: "x \<in> set(drop n xs) \<Longrightarrow> x \<in> 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 \<and> ys = drop (length xs) zs)"
@@ -2226,10 +2225,10 @@
qed
lemma take_update_cancel[simp]: "n \<le> m \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
@@ -2258,27 +2257,27 @@
qed auto
lemma nth_image: "l \<le> size xs \<Longrightarrow> nth xs ` {0..<l} = set(take l xs)"
-by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
+ by(auto simp: set_conv_nth image_def) (metis Suc_le_eq nth_take order_trans)
subsubsection \<open>@{const takeWhile} and @{const dropWhile}\<close>
lemma length_takeWhile_le: "length (takeWhile P xs) \<le> 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]:
"\<lbrakk>x \<in> set xs; \<not>P(x)\<rbrakk> \<Longrightarrow> takeWhile P (xs @ ys) = takeWhile P xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_append2 [simp]:
"(\<And>x. x \<in> set xs \<Longrightarrow> P x) \<Longrightarrow> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_tail: "\<not> P x \<Longrightarrow> takeWhile P (xs @ (x#l)) = takeWhile P xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> 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) \<le> length xs"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_append1 [simp]:
"\<lbrakk>x \<in> set xs; \<not>P(x)\<rbrakk> \<Longrightarrow> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_append2 [simp]:
"(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_append3:
"\<not> P y \<Longrightarrow>dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_last:
"x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> 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 \<in> set (dropWhile P xs) \<Longrightarrow> x \<in> set xs"
-by (induct xs) (auto split: if_split_asm)
+ by (induct xs) (auto split: if_split_asm)
lemma set_takeWhileD: "x \<in> set (takeWhile P xs) \<Longrightarrow> x \<in> set xs \<and> 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) = (\<forall>x \<in> set xs. P x)"
-by(induct xs, auto)
+ by(induct xs, auto)
lemma dropWhile_eq_Nil_conv[simp]:
"(dropWhile P xs = []) = (\<forall>x \<in> 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 \<and> \<not> 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 \<circ> f) xs)"
-by (induct xs) auto
+ by (induct xs) auto
lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> 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 \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
-by (induct xs) auto
+ by (induct xs) auto
lemma takeWhile_eq_filter:
assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
@@ -2384,12 +2383,12 @@
thus "\<not> 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 \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
-by (induct xs) auto
+ by (induct xs) auto
lemma length_takeWhile_less_P_nth:
assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
@@ -2402,7 +2401,7 @@
lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
-by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
+ by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
@@ -2414,34 +2413,34 @@
lemma takeWhile_not_last:
"distinct xs \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
-by(induction xs rule: induct_list012) auto
+ by(induction xs rule: induct_list012) auto
lemma takeWhile_cong [fundef_cong]:
"\<lbrakk>l = k; \<And>x. x \<in> set l \<Longrightarrow> P x = Q x\<rbrakk>
\<Longrightarrow> 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]:
"\<lbrakk>l = k; \<And>x. x \<in> set l \<Longrightarrow> P x = Q x\<rbrakk>
\<Longrightarrow> 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 \<open>@{const zip}\<close>
lemma zip_Nil [simp]: "zip [] ys = []"
-by (induct ys) auto
+ by (induct ys) auto
lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
-by simp
+ by simp
declare zip_Cons [simp del]
@@ -2449,15 +2448,15 @@
"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 [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
-by(auto split:list.split)
+ by(auto split:list.split)
lemma length_zip [simp]:
"length (zip xs ys) = min (length xs) (length ys)"
-by (induct xs ys rule:list_induct2') auto
+ by (induct xs ys rule:list_induct2') auto
lemma zip_obtain_same_length:
assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
@@ -2479,21 +2478,21 @@
lemma zip_append1:
"zip (xs @ ys) zs =
zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
-by (induct xs zs rule:list_induct2') auto
+ 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"
-by (induct xs ys rule:list_induct2') auto
+ 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"
-by (simp add: zip_append1)
+ by (simp add: zip_append1)
lemma zip_rev:
"length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
-by (induct rule:list_induct2, simp_all)
+ by (induct rule:list_induct2, simp_all)
lemma zip_map_map:
"zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
@@ -2508,23 +2507,23 @@
lemma zip_map1:
"zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
-using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
+ using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
lemma zip_map2:
"zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
-using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
+ using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
lemma map_zip_map:
"map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
-by (auto simp: zip_map1)
+ 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)"
-by (auto simp: zip_map2)
+ by (auto simp: zip_map2)
text\<open>Courtesy of Andreas Lochbihler:\<close>
lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
-by(induct xs) auto
+ by(induct xs) auto
lemma nth_zip [simp]:
"[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
@@ -2536,10 +2535,10 @@
lemma set_zip:
"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)
+ by(simp add: set_conv_nth cong: rev_conj_cong)
lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
-by(induct xs) auto
+ by(induct xs) auto
lemma zip_update: "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
by (simp add: update_zip)
@@ -2553,7 +2552,7 @@
qed auto
lemma zip_replicate1: "zip (replicate n x) ys = map (Pair x) (take n ys)"
-by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
+ by(induction ys arbitrary: n)(case_tac [2] n, simp_all)
lemma take_zip: "take n (zip xs ys) = zip (take n xs) (take n ys)"
proof (induct n arbitrary: xs ys)
@@ -2580,26 +2579,26 @@
qed simp
lemma set_zip_leftD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
-by (induct xs ys rule:list_induct2') auto
+ by (induct xs ys rule:list_induct2') auto
lemma set_zip_rightD: "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
-by (induct xs ys rule:list_induct2') auto
+ by (induct xs ys rule:list_induct2') auto
lemma in_set_zipE:
"(x,y) \<in> set(zip xs ys) \<Longrightarrow> (\<lbrakk> x \<in> set xs; y \<in> set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
-by(blast dest: set_zip_leftD set_zip_rightD)
+ 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
+ by (induct zs) simp_all
lemma zip_eq_conv:
"length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> 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 \<in> set (zip xs ys) \<longleftrightarrow> (\<exists>n. xs ! n = fst p \<and> ys ! n = snd p
\<and> n < length xs \<and> n < length ys)"
-by (cases p) (auto simp add: set_zip)
+ by (cases p) (auto simp add: set_zip)
lemma in_set_impl_in_set_zip1:
assumes "length xs = length ys"
@@ -2633,25 +2632,25 @@
lemma list_all2_lengthD [intro?]:
"list_all2 P xs ys ==> length xs = length ys"
-by (simp add: list_all2_iff)
+ by (simp add: list_all2_iff)
lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
-by (simp add: list_all2_iff)
+ by (simp add: list_all2_iff)
lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
-by (simp add: list_all2_iff)
+ by (simp add: list_all2_iff)
lemma list_all2_Cons [iff, code]:
"list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
-by (auto simp add: list_all2_iff)
+ by (auto simp add: list_all2_iff)
lemma list_all2_Cons1:
"list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
-by (cases ys) auto
+ by (cases ys) auto
lemma list_all2_Cons2:
"list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
-by (cases xs) auto
+ by (cases xs) auto
lemma list_all2_induct
[consumes 1, case_names Nil Cons, induct set: list_all2]:
@@ -2660,16 +2659,16 @@
assumes Cons: "\<And>x xs y ys.
\<lbrakk>P x y; list_all2 P xs ys; R xs ys\<rbrakk> \<Longrightarrow> R (x # xs) (y # ys)"
shows "R xs ys"
-using P
-by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)
+ using P
+ 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"
-by (simp add: list_all2_iff zip_rev cong: conj_cong)
+ 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)"
-by (subst list_all2_rev [symmetric]) simp
+ by (subst list_all2_rev [symmetric]) simp
lemma list_all2_append1:
"list_all2 P (xs @ ys) zs =
@@ -2708,21 +2707,21 @@
lemma list_all2_append:
"length xs = length ys \<Longrightarrow>
list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
-by (induct rule:list_induct2, simp_all)
+ by (induct rule:list_induct2, simp_all)
lemma list_all2_appendI [intro?, trans]:
"\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
-by (simp add: list_all2_append list_all2_lengthD)
+ by (simp add: list_all2_append list_all2_lengthD)
lemma list_all2_conv_all_nth:
"list_all2 P xs ys =
(length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
-by (force simp add: list_all2_iff set_zip)
+ by (force simp add: list_all2_iff set_zip)
lemma list_all2_trans:
assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
- (is "!!bs cs. PROP ?Q as bs cs")
+ (is "!!bs cs. PROP ?Q as bs cs")
proof (induct as)
fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
show "!!cs. PROP ?Q (x # xs) bs cs"
@@ -2735,35 +2734,35 @@
lemma list_all2_all_nthI [intro?]:
"length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
-by (simp add: list_all2_conv_all_nth)
+ by (simp add: list_all2_conv_all_nth)
lemma list_all2I:
"\<forall>x \<in> set (zip a b). case_prod P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
-by (simp add: list_all2_iff)
+ by (simp add: list_all2_iff)
lemma list_all2_nthD:
"\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
-by (simp add: list_all2_conv_all_nth)
+ by (simp add: list_all2_conv_all_nth)
lemma list_all2_nthD2:
"\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
-by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
+ by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
lemma list_all2_map1:
"list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
-by (simp add: list_all2_conv_all_nth)
+ by (simp add: list_all2_conv_all_nth)
lemma list_all2_map2:
"list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
-by (auto simp add: list_all2_conv_all_nth)
+ by (auto simp add: list_all2_conv_all_nth)
lemma list_all2_refl [intro?]:
"(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
-by (simp add: list_all2_conv_all_nth)
+ by (simp add: list_all2_conv_all_nth)
lemma list_all2_update_cong:
"\<lbrakk> list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
-by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
+ by (cases "i < length ys") (auto simp add: list_all2_conv_all_nth nth_list_update)
lemma list_all2_takeI [simp,intro?]:
"list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
@@ -2787,46 +2786,46 @@
lemma list_all2_eq:
"xs = ys \<longleftrightarrow> list_all2 (=) xs ys"
-by (induct xs ys rule: list_induct2') auto
+ by (induct xs ys rule: list_induct2') auto
lemma list_eq_iff_zip_eq:
"xs = ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x,y) \<in> set (zip xs ys). x = y)"
-by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
+ by(auto simp add: set_zip list_all2_eq list_all2_conv_all_nth cong: conj_cong)
lemma list_all2_same: "list_all2 P xs xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x x)"
-by(auto simp add: list_all2_conv_all_nth set_conv_nth)
+ by(auto simp add: list_all2_conv_all_nth set_conv_nth)
lemma zip_assoc:
"zip xs (zip ys zs) = map (\<lambda>((x, y), z). (x, y, z)) (zip (zip xs ys) zs)"
-by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
+ by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
lemma zip_commute: "zip xs ys = map (\<lambda>(x, y). (y, x)) (zip ys xs)"
-by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
+ by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
lemma zip_left_commute:
"zip xs (zip ys zs) = map (\<lambda>(y, (x, z)). (x, y, z)) (zip ys (zip xs zs))"
-by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
+ by(rule list_all2_all_nthI[where P="(=)", unfolded list.rel_eq]) simp_all
lemma zip_replicate2: "zip xs (replicate n y) = map (\<lambda>x. (x, y)) (take n xs)"
-by(subst zip_commute)(simp add: zip_replicate1)
+ by(subst zip_commute)(simp add: zip_replicate1)
subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
lemma product_concat_map:
"List.product xs ys = concat (map (\<lambda>x. map (\<lambda>y. (x,y)) ys) xs)"
-by(induction xs) (simp)+
+ by(induction xs) (simp)+
lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
-by (induct xs) auto
+ 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"
shows "List.product xs ys ! n = (xs ! (n div length ys), ys ! (n mod length ys))"
-using assms proof (induct xs arbitrary: n)
+ using assms proof (induct xs arbitrary: n)
case Nil then show ?case by simp
next
case (Cons x xs n)
@@ -2837,7 +2836,7 @@
lemma in_set_product_lists_length:
"xs \<in> set (product_lists xss) \<Longrightarrow> 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 (\<lambda>x ys. x \<in> set ys) xs xss}" (is "?L = Collect ?R")
@@ -2856,25 +2855,25 @@
lemma fold_simps [code]: \<comment> \<open>eta-expanded variant for generated code -- enables tail-recursion optimisation in Scala\<close>
"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:
"\<lbrakk> \<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x;
x \<in> set xs \<rbrakk>
\<Longrightarrow> fold f xs = fold f (remove1 x xs) \<circ> f x"
-by (induct xs) (auto simp add: comp_assoc)
+ by (induct xs) (auto simp add: comp_assoc)
lemma fold_cong [fundef_cong]:
"a = b \<Longrightarrow> xs = ys \<Longrightarrow> (\<And>x. x \<in> set xs \<Longrightarrow> f x = g x)
\<Longrightarrow> fold f xs a = fold g ys b"
-by (induct ys arbitrary: a b xs) simp_all
+ by (induct ys arbitrary: a b xs) simp_all
lemma fold_id: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = id) \<Longrightarrow> fold f xs = id"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma fold_commute:
"(\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h) \<Longrightarrow> h \<circ> fold g xs = fold f xs \<circ> h"
-by (induct xs) (simp_all add: fun_eq_iff)
+ by (induct xs) (simp_all add: fun_eq_iff)
lemma fold_commute_apply:
assumes "\<And>x. x \<in> set xs \<Longrightarrow> h \<circ> g x = f x \<circ> h"
@@ -2887,41 +2886,41 @@
lemma fold_invariant:
"\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> Q x; P s; \<And>x s. Q x \<Longrightarrow> P s \<Longrightarrow> P (f x s) \<rbrakk>
\<Longrightarrow> P (fold f xs s)"
-by (induct xs arbitrary: s) simp_all
+ by (induct xs arbitrary: s) simp_all
lemma fold_append [simp]: "fold f (xs @ ys) = fold f ys \<circ> fold f xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma fold_map [code_unfold]: "fold g (map f xs) = fold (g \<circ> f) xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma fold_filter:
"fold f (filter P xs) = fold (\<lambda>x. if P x then f x else id) xs"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma fold_rev:
"(\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y)
\<Longrightarrow> fold f (rev xs) = fold f xs"
-by (induct xs) (simp_all add: fold_commute_apply fun_eq_iff)
+ 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
+ by (induct xs) simp_all
lemma rev_conv_fold [code]: "rev xs = fold Cons xs []"
-by (simp add: fold_Cons_rev)
+ by (simp add: fold_Cons_rev)
lemma fold_append_concat_rev: "fold append xss = append (concat (rev xss))"
-by (induct xss) simp_all
+ by (induct xss) simp_all
text \<open>@{const Finite_Set.fold} and @{const fold}\<close>
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)
+ by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_left_comm)
lemma union_set_fold [code]: "set xs \<union> A = fold Set.insert xs A"
proof -
@@ -2932,7 +2931,7 @@
lemma union_coset_filter [code]:
"List.coset xs \<union> A = List.coset (List.filter (\<lambda>x. x \<notin> A) xs)"
-by auto
+ by auto
lemma minus_set_fold [code]: "A - set xs = fold Set.remove xs A"
proof -
@@ -2944,15 +2943,15 @@
lemma minus_coset_filter [code]:
"A - List.coset xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
-by auto
+ by auto
lemma inter_set_filter [code]:
"A \<inter> set xs = set (List.filter (\<lambda>x. x \<in> A) xs)"
-by auto
+ by auto
lemma inter_coset_fold [code]:
"A \<inter> 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"
@@ -3000,70 +2999,70 @@
text \<open>Correspondence\<close>
lemma foldr_conv_fold [code_abbrev]: "foldr f xs = fold f (rev xs)"
-by (induct xs) simp_all
+ by (induct xs) simp_all
lemma foldl_conv_fold: "foldl f s xs = fold (\<lambda>x s. f s x) xs s"
-by (induct xs arbitrary: s) simp_all
+ by (induct xs arbitrary: s) simp_all
lemma foldr_conv_foldl: \<comment> \<open>The ``Third Duality Theorem'' in Bird \& Wadler:\<close>
"foldr f xs a = foldl (\<lambda>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 (\<lambda>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:
"(\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f y \<circ> f x = f x \<circ> f y)
\<Longrightarrow> foldr f xs = fold f xs"
-unfolding foldr_conv_fold by (rule fold_rev)
+ unfolding foldr_conv_fold by (rule fold_rev)
lemma foldr_cong [fundef_cong]:
"a = b \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f x a = g x a) \<Longrightarrow> 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 \<Longrightarrow> l = k \<Longrightarrow> (\<And>a x. x \<in> set l \<Longrightarrow> f a x = g a x) \<Longrightarrow> foldl f a l = foldl g b k"
-by (auto simp add: foldl_conv_fold intro!: fold_cong)
+ 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)
+ 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)
+ by (simp add: foldl_conv_fold)
lemma foldr_map [code_unfold]: "foldr g (map f xs) a = foldr (g \<circ> f) xs a"
-by (simp add: foldr_conv_fold fold_map rev_map)
+ by (simp add: foldr_conv_fold fold_map rev_map)
lemma foldr_filter:
"foldr f (filter P xs) = foldr (\<lambda>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 (\<lambda>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 \<open>@{const upt}\<close>
lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
-\<comment> \<open>simp does not terminate!\<close>
-by (induct j) auto
+ \<comment> \<open>simp does not terminate!\<close>
+ by (induct j) auto
lemmas upt_rec_numeral[simp] = upt_rec[of "numeral m" "numeral n"] for m n
lemma upt_conv_Nil [simp]: "j \<le> i ==> [i..<j] = []"
-by (subst upt_rec) simp
+ by (subst upt_rec) simp
lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j \<le> i)"
-by(induct j)simp_all
+ by(induct j)simp_all
lemma upt_eq_Cons_conv:
- "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
+ "([i..<j] = x#xs) = (i < j \<and> i = x \<and> [i+1..<j] = xs)"
proof (induct j arbitrary: x xs)
case (Suc j)
then show ?case
@@ -3071,11 +3070,11 @@
qed simp
lemma upt_Suc_append: "i \<le> j ==> [i..<(Suc j)] = [i..<j]@[j]"
-\<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
-by simp
+ \<comment> \<open>Only needed if \<open>upt_Suc\<close> is deleted from the simpset.\<close>
+ by simp
lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
-by (simp add: upt_rec)
+ by (simp add: upt_rec)
lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
"m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
@@ -3086,23 +3085,23 @@
qed
lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
-\<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
-by (induct k) auto
+ \<comment> \<open>LOOPS as a simprule, since \<open>j \<le> j\<close>.\<close>
+ by (induct k) auto
lemma length_upt [simp]: "length [i..<j] = j - i"
-by (induct j) (auto simp add: Suc_diff_le)
+ by (induct j) (auto simp add: Suc_diff_le)
lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
-by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
+ by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
-by(simp add:upt_conv_Cons)
+ by(simp add:upt_conv_Cons)
lemma tl_upt: "tl [m..<n] = [Suc m..<n]"
-by (simp add: upt_rec)
+ by (simp add: upt_rec)
lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
-by(cases j)(auto simp: upt_Suc_append)
+ by(cases j)(auto simp: upt_Suc_append)
lemma take_upt [simp]: "i+m \<le> n ==> take m [i..<n] = [i..<i+m]"
proof (induct m arbitrary: i)
@@ -3112,26 +3111,26 @@
qed simp
lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
-by(induct j) auto
+ by(induct j) auto
lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
-by (induct n) auto
+ by (induct n) auto
lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
-by (induct m) simp_all
+ by (induct m) simp_all
lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
proof (induct n m arbitrary: i rule: diff_induct)
-case (3 x y)
+ case (3 x y)
then show ?case
by (metis add.commute length_upt less_diff_conv nth_map nth_upt)
qed auto
lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
+ by (induct n) simp_all
lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
-by (induct n arbitrary: f) auto
+ by (induct n arbitrary: f) auto
lemma nth_take_lemma:
"k \<le> length xs \<Longrightarrow> k \<le> length ys \<Longrightarrow>
@@ -3145,24 +3144,20 @@
lemma nth_equalityI:
"[| length xs = length ys; \<forall>i < length xs. xs!i = ys!i |] ==> xs = ys"
-by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
+ by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
lemma map_nth:
"map (\<lambda>i. xs ! i) [0..<length xs] = xs"
-by (rule nth_equalityI, auto)
+ by (rule nth_equalityI, auto)
lemma list_all2_antisym:
"\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk>
\<Longrightarrow> xs = ys"
-apply (simp add: list_all2_conv_all_nth)
-apply (rule nth_equalityI, blast, simp)
-done
+ by (simp add: list_all2_conv_all_nth nth_equalityI)
lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
\<comment> \<open>The famous take-lemma.\<close>
-apply (drule_tac x = "max (length xs) (length ys)" in spec)
-apply (simp add: le_max_iff_disj)
-done
+ by (metis length_take min.commute order_refl take_all)
lemma take_Cons':
"take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
@@ -3239,7 +3234,7 @@
qed
lemma nth_upto: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
-apply(induction i j arbitrary: k rule: upto.induct)
+ apply(induction i j arbitrary: k rule: upto.induct)
apply(subst upto_rec1)
apply(auto simp add: nth_Cons')
done
@@ -3310,12 +3305,11 @@
lemma length_remdups_eq[iff]:
"(length (remdups xs) = length xs) = (remdups xs = xs)"
-apply(induct xs)
- apply auto
-apply(subgoal_tac "length (remdups xs) \<le> length xs")
- apply arith
-apply(rule length_remdups_leq)
-done
+proof (induct xs)
+ case (Cons a xs)
+ then show ?case
+ by simp (metis Suc_n_not_le_n impossible_Cons length_remdups_leq)
+qed auto
lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
by (induct xs) auto
@@ -3341,31 +3335,38 @@
done
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
+proof (induct xs arbitrary: i)
+ case (Cons a xs)
+ then show ?case
+ by (metis Cons.prems append_take_drop_id distinct_append)
+qed auto
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
-done
+proof (induct xs arbitrary: i)
+ case (Cons a xs)
+ then show ?case
+ by (metis Cons.prems append_take_drop_id distinct_append)
+qed auto
lemma distinct_list_update:
-assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
-shows "distinct (xs[i:=a])"
+ assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
+ shows "distinct (xs[i:=a])"
proof (cases "i < length xs")
case True
- with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
- apply (drule_tac id_take_nth_drop) by simp
- with d True show ?thesis
- apply (simp add: upd_conv_take_nth_drop)
- apply (drule subst [OF id_take_nth_drop]) apply assumption
- apply simp apply (cases "a = xs!i") apply simp by blast
+ with a have anot: "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
+ by simp (metis in_set_dropD in_set_takeD)
+ show ?thesis
+ proof (cases "a = xs!i")
+ case True
+ with d show ?thesis
+ by auto
+ next
+ case False
+ then show ?thesis
+ using d anot \<open>i < length xs\<close>
+ apply (simp add: upd_conv_take_nth_drop)
+ by (metis disjoint_insert(1) distinct_append id_take_nth_drop set_simps(2))
+ qed
next
case False with d show ?thesis by auto
qed
@@ -3380,22 +3381,14 @@
text \<open>It is best to avoid this indexed version of distinct, but
sometimes it is useful.\<close>
-lemma distinct_conv_nth:
-"distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
-apply (induct xs, simp, simp)
-apply (rule iffI, clarsimp)
- apply (case_tac i)
-apply (case_tac j, simp)
-apply (simp add: set_conv_nth)
- apply (case_tac j)
-apply (clarsimp simp add: set_conv_nth, simp)
-apply (rule conjI)
- apply (clarsimp simp add: set_conv_nth)
- apply (erule_tac x = 0 in allE, simp)
- apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
-apply (erule_tac x = "Suc i" in allE, simp)
-apply (erule_tac x = "Suc j" in allE, simp)
-done
+lemma distinct_conv_nth: "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
+proof (induct xs)
+ case (Cons x xs)
+ show ?case
+ apply (auto simp add: Cons nth_Cons split: nat.split_asm)
+ apply (metis Suc_less_eq2 in_set_conv_nth less_not_refl zero_less_Suc)+
+ done
+qed auto
lemma nth_eq_iff_index_eq:
"\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
@@ -3420,7 +3413,7 @@
lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow>
distinct(xs[i := xs!j, j := xs!i]) = distinct xs"
-apply (simp add: distinct_conv_nth nth_list_update)
+ apply (simp add: distinct_conv_nth nth_list_update)
apply safe
apply metis+
done
@@ -3434,8 +3427,6 @@
lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
proof (induct xs)
- case Nil thus ?case by simp
-next
case (Cons x xs)
show ?case
proof (cases "x \<in> set xs")
@@ -3448,17 +3439,20 @@
ultimately have False by simp
thus ?thesis ..
qed
-qed
+qed simp
lemma distinct_length_filter: "distinct xs \<Longrightarrow> length (filter P xs) = card ({x. P x} Int set xs)"
by (induct xs) (auto)
lemma not_distinct_decomp: "\<not> distinct ws \<Longrightarrow> \<exists>xs ys zs y. ws = xs@[y]@ys@[y]@zs"
-apply (induct n == "length ws" arbitrary:ws) apply simp
-apply(case_tac ws) apply simp
-apply (simp split:if_split_asm)
-apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
-done
+proof (induct n == "length ws" arbitrary:ws)
+ case (Suc n ws)
+ then show ?case
+ using length_Suc_conv [of ws n]
+ apply (auto simp: eq_commute)
+ apply (metis append_Nil in_set_conv_decomp_first)
+ by (metis append_Cons)
+qed simp
lemma not_distinct_conv_prefix:
defines "dec as xs y ys \<equiv> y \<in> set xs \<and> distinct xs \<and> as = xs @ y # ys"
@@ -3690,7 +3684,6 @@
then have "Suc 0 \<notin> f ` {0 ..< length (x1 # x2 # xs)}" by auto
then show False using f_img \<open>2 \<le> length ys\<close> by auto
qed
-
obtain ys' where "ys = x1 # x2 # ys'"
using \<open>2 \<le> length ys\<close> f_nth[of 0] f_nth[of 1]
apply (cases ys)
@@ -3715,10 +3708,7 @@
using Suc0_le_f_Suc f_mono by (auto simp: f'_def mono_iff_le_Suc le_diff_iff)
next
have "f' ` {0 ..< length (x2 # xs)} = (\<lambda>x. f x - 1) ` {0 ..< length (x1 # x2 #xs)}"
- apply safe
- apply (rename_tac [!] n, case_tac [!] n)
- apply (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> intro: rev_image_eqI)
- done
+ by (auto simp: f'_def \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close> image_def Bex_def less_Suc_eq_0_disj)
also have "\<dots> = (\<lambda>x. x - 1) ` f ` {0 ..< length (x1 # x2 #xs)}"
by (auto simp: image_comp)
also have "\<dots> = (\<lambda>x. x - 1) ` {0 ..< length ys}"
@@ -3885,10 +3875,12 @@
lemma sum_count_set:
"set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
-apply(induction xs arbitrary: X)
- apply simp
-apply (simp add: sum.If_cases)
-by (metis Diff_eq sum.remove)
+proof (induction xs arbitrary: X)
+ case (Cons x xs)
+ then show ?case
+ apply (auto simp: sum.If_cases sum.remove)
+ by (metis (no_types) Cons.IH Cons.prems(2) diff_eq sum.remove)
+qed simp
subsubsection \<open>@{const List.extract}\<close>
@@ -3931,23 +3923,13 @@
lemma in_set_remove1[simp]:
"a \<noteq> b \<Longrightarrow> a \<in> set(remove1 b xs) = (a \<in> set xs)"
-apply (induct xs)
- apply auto
-done
+ by (induct xs) auto
lemma set_remove1_subset: "set(remove1 x xs) \<subseteq> set xs"
-apply(induct xs)
- apply simp
-apply simp
-apply blast
-done
+ by (induct xs) auto
lemma set_remove1_eq [simp]: "distinct xs \<Longrightarrow> set(remove1 x xs) = set xs - {x}"
-apply(induct xs)
- apply simp
-apply simp
-apply blast
-done
+ by (induct xs) auto
lemma length_remove1:
"length(remove1 x xs) = (if x \<in> set xs then length xs - 1 else length xs)"
@@ -4067,9 +4049,7 @@
text\<open>Courtesy of Matthias Daum:\<close>
lemma append_replicate_commute:
"replicate n x @ replicate k x = replicate k x @ replicate n x"
-apply (simp add: replicate_add [symmetric])
-apply (simp add: add.commute)
-done
+ by (metis add.commute replicate_add)
text\<open>Courtesy of Andreas Lochbihler:\<close>
lemma filter_replicate:
@@ -4090,23 +4070,24 @@
text\<open>Courtesy of Matthias Daum (2 lemmas):\<close>
lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
-apply (case_tac "k \<le> i")
- apply (simp add: min_def)
-apply (drule not_le_imp_less)
-apply (simp add: min_def)
-apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
- apply simp
-apply (simp add: replicate_add [symmetric])
-done
+proof (cases "k \<le> i")
+ case True
+ then show ?thesis
+ by (simp add: min_def)
+next
+ case False
+ then have "replicate k x = replicate i x @ replicate (k - i) x"
+ by (simp add: replicate_add [symmetric])
+ then show ?thesis
+ by (simp add: min_def)
+qed
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)
- apply simp
-apply clarsimp
-done
+proof (induct k arbitrary: i)
+ case (Suc k)
+ then show ?case
+ by (simp add: drop_Cons')
+qed simp
lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
by (induct n) auto
@@ -4148,11 +4129,11 @@
lemma replicate_eq_replicate[simp]:
"(replicate m x = replicate n y) \<longleftrightarrow> (m=n \<and> (m\<noteq>0 \<longrightarrow> x=y))"
-apply(induct m arbitrary: n)
- apply simp
-apply(induct_tac n)
-apply auto
-done
+proof (induct m arbitrary: n)
+ case (Suc m n)
+ then show ?case
+ by (induct n) auto
+qed simp
lemma replicate_length_filter:
"replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
@@ -4239,10 +4220,7 @@
lemma enumerate_simps [simp, code]:
"enumerate n [] = []"
"enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
-apply (auto simp add: enumerate_eq_zip not_le)
-apply (cases "n < n + length xs")
- apply (auto simp add: upt_conv_Cons)
-done
+ by (simp_all add: enumerate_eq_zip upt_rec)
lemma length_enumerate [simp]:
"length (enumerate n xs) = length xs"
@@ -4288,12 +4266,7 @@
lemma enumerate_append_eq:
"enumerate n (xs @ ys) = enumerate n xs @ enumerate (n + length xs) ys"
-unfolding enumerate_eq_zip
-apply auto
- apply (subst zip_append [symmetric]) apply simp
- apply (subst upt_add_eq_append [symmetric])
- apply (simp_all add: ac_simps)
-done
+ by (simp add: enumerate_eq_zip add.assoc zip_append2)
lemma enumerate_map_upt:
"enumerate n (map f [n..<m]) = map (\<lambda>k. (k, f k)) [n..<m]"
@@ -4322,27 +4295,33 @@
by(cases xs) simp_all
lemma rotate_length01[simp]: "length xs \<le> 1 \<Longrightarrow> rotate n xs = xs"
-apply(induct n)
- apply simp
-apply (simp add:rotate_def)
-done
+ by (induct n) (simp_all add:rotate_def)
lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
by (cases xs) simp_all
lemma rotate_drop_take:
"rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
-apply(induct n)
- apply simp
-apply(simp add:rotate_def)
-apply(cases "xs = []")
- apply (simp)
-apply(case_tac "n mod length xs = 0")
- apply(simp add:mod_Suc)
- apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
-apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
- take_hd_drop linorder_not_le)
-done
+proof (induct n)
+ case (Suc n)
+ show ?case
+ proof (cases "xs = []")
+ case False
+ then show ?thesis
+ proof (cases "n mod length xs = 0")
+ case True
+ then show ?thesis
+ apply (simp add: mod_Suc)
+ by (simp add: False Suc.hyps drop_Suc rotate1_hd_tl take_Suc)
+ next
+ case False
+ with \<open>xs \<noteq> []\<close> Suc
+ show ?thesis
+ by (simp add: rotate_def mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
+ take_hd_drop linorder_not_le)
+ qed
+ qed simp
+qed simp
lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
by(simp add:rotate_drop_take)
@@ -4385,11 +4364,14 @@
by(simp add:rotate_drop_take rev_drop rev_take)
qed force
-lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
-apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
-apply(subgoal_tac "length xs \<noteq> 0")
- prefer 2 apply simp
-using mod_less_divisor[of "length xs" n] by arith
+lemma hd_rotate_conv_nth:
+ assumes "xs \<noteq> []" shows "hd(rotate n xs) = xs!(n mod length xs)"
+proof -
+ have "n mod length xs < length xs"
+ using assms by simp
+ then show ?thesis
+ by (metis drop_eq_Nil hd_append2 hd_drop_conv_nth leD rotate_drop_take)
+qed
lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
@@ -4408,14 +4390,13 @@
by(simp add: nths_def length_filter_conv_card cong:conj_cong)
lemma nths_shift_lemma_Suc:
- "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
-apply simp
-done
+ "map fst (filter (\<lambda>p. P(Suc(snd p))) (zip xs is)) =
+ map fst (filter (\<lambda>p. P(snd p)) (zip xs (map Suc is)))"
+proof (induct xs arbitrary: "is")
+ case (Cons x xs "is")
+ show ?case
+ by (cases "is") (auto simp add: Cons.hyps)
+qed simp
lemma nths_shift_lemma:
"map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [i..<i + length xs])) =
@@ -4424,26 +4405,26 @@
lemma nths_append:
"nths (l @ l') A = nths l A @ nths l' {j. j + length l \<in> A}"
-apply (unfold nths_def)
-apply (induct l' rule: rev_induct, simp)
-apply (simp add: upt_add_eq_append[of 0] nths_shift_lemma)
-apply (simp add: add.commute)
-done
+ unfolding nths_def
+proof (induct l' rule: rev_induct)
+ case (snoc x xs)
+ then show ?case
+ by (simp add: upt_add_eq_append[of 0] nths_shift_lemma add.commute)
+qed auto
lemma nths_Cons:
"nths (x # l) A = (if 0 \<in> A then [x] else []) @ nths l {j. Suc j \<in> A}"
-apply (induct l rule: rev_induct)
- apply (simp add: nths_def)
-apply (simp del: append_Cons add: append_Cons[symmetric] nths_append)
-done
+proof (induct l rule: rev_induct)
+ case (snoc x xs)
+ then show ?case
+ by (simp flip: append_Cons add: nths_append)
+qed (auto simp: nths_def)
lemma nths_map: "nths (map f xs) I = map f (nths xs I)"
by(induction xs arbitrary: I) (simp_all add: nths_Cons)
lemma set_nths: "set(nths xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
-apply(induct xs arbitrary: I)
-apply(auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
-done
+ by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
lemma set_nths_subset: "set(nths xs I) \<subseteq> set xs"
by(auto simp add:set_nths)
@@ -4792,8 +4773,7 @@
show ?thesis
unfolding transpose.simps \<open>i = Suc j\<close> nth_Cons_Suc "3.hyps"[OF j_less]
apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
- apply (rule list.exhaust)
- by auto
+ by (simp add: nth_tl)
qed
qed simp_all
@@ -4917,11 +4897,7 @@
qed
lemma infinite_UNIV_listI: "\<not> finite(UNIV::'a list set)"
-apply (rule notI)
-apply (drule finite_maxlen)
-apply clarsimp
-apply (erule_tac x = "replicate n undefined" in allE)
-by simp
+ by (metis UNIV_I finite_maxlen length_replicate less_irrefl)
subsection \<open>Sorting\<close>
@@ -4936,10 +4912,11 @@
by(simp)
lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))"
-apply(induction zs arbitrary: x y)
-apply(auto dest: transpD)
-apply (meson transpD)
-done
+proof (induction zs arbitrary: x y)
+ case (Cons z zs)
+ then show ?case
+ by simp (meson transpD)+
+qed auto
lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
@@ -4969,9 +4946,7 @@
lemma sorted_wrt_iff_nth_less:
"sorted_wrt P xs = (\<forall>i j. i < j \<longrightarrow> j < length xs \<longrightarrow> P (xs ! i) (xs ! j))"
-apply(induction xs)
-apply(auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
-done
+ by (induction xs) (auto simp add: in_set_conv_nth Ball_def nth_Cons split: nat.split)
lemma sorted_wrt_nth_less:
"\<lbrakk> sorted_wrt P xs; i < j; j < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) (xs ! j)"
@@ -4981,10 +4956,11 @@
by(induction n) (auto simp: sorted_wrt_append)
lemma sorted_wrt_upto[simp]: "sorted_wrt (<) [i..j]"
-apply(induction i j rule: upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
+proof(induct i j rule:upto.induct)
+ case (1 i j)
+ from this show ?case
+ unfolding upto.simps[of i j] by auto
+qed
text \<open>Each element is greater or equal to its index:\<close>
@@ -5313,12 +5289,13 @@
qed
lemma finite_sorted_distinct_unique:
-shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
-apply(drule finite_distinct_list)
-apply clarify
-apply(rule_tac a="sort xs" in ex1I)
-apply (auto simp: sorted_distinct_set_unique)
-done
+ assumes "finite A" shows "\<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
+proof -
+ obtain xs where "distinct xs" "A = set xs"
+ using finite_distinct_list [OF assms] by metis
+ then show ?thesis
+ by (rule_tac a="sort xs" in ex1I) (auto simp: sorted_distinct_set_unique)
+qed
lemma insort_insert_key_triv:
"f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
@@ -5741,12 +5718,12 @@
| insert: "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
-apply (rule iffI)
- apply (induct set: ListMem)
- apply auto
-apply (induct xs)
- apply (auto intro: ListMem.intros)
-done
+proof
+ show "ListMem x xs \<Longrightarrow> x \<in> set xs"
+ by (induct set: ListMem) auto
+ show "x \<in> set xs \<Longrightarrow> ListMem x xs"
+ by (induct xs) (auto intro: ListMem.intros)
+qed
subsubsection \<open>Lists as Cartesian products\<close>
@@ -5789,20 +5766,23 @@
"lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
\<comment> \<open>Compares lists by their length and then lexicographically\<close>
-lemma wf_lexn: "wf r ==> wf (lexn r n)"
-apply (induct n, simp, simp)
-apply(rule wf_subset)
- prefer 2 apply (rule Int_lower1)
-apply(rule wf_map_prod_image)
- prefer 2 apply (rule inj_onI, auto)
-done
+lemma wf_lexn: assumes "wf r" shows "wf (lexn r n)"
+proof (induct n)
+ case (Suc n)
+ have inj: "inj (\<lambda>(x, xs). x # xs)"
+ using assms by (auto simp: inj_on_def)
+ have wf: "wf (map_prod (\<lambda>(x, xs). x # xs) (\<lambda>(x, xs). x # xs) ` (r <*lex*> lexn r n))"
+ by (simp add: Suc.hyps assms wf_lex_prod wf_map_prod_image [OF _ inj])
+ then show ?case
+ by (rule wf_subset) auto
+qed auto
lemma lexn_length:
"(xs, ys) \<in> lexn r n \<Longrightarrow> 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)
+ unfolding lex_def
apply (rule wf_UN)
apply (simp add: wf_lexn)
apply (metis DomainE Int_emptyI RangeE lexn_length)
@@ -5905,14 +5885,12 @@
by (simp add:lex_conv)
lemma Cons_in_lex [simp]:
- "((x # xs, y # ys) \<in> lex r) =
+ "((x # xs, y # ys) \<in> lex r) =
((x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r)"
-apply (simp add: lex_conv)
-apply (rule iffI)
- prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
-apply (case_tac xys, simp, simp)
-apply blast
- done
+ apply (simp add: lex_conv)
+ apply (rule iffI)
+ prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
+ by (metis hd_append append_Nil list.sel(1) list.sel(3) tl_append2)
lemma lex_append_rightI:
"(xs, ys) \<in> lex r \<Longrightarrow> length vs = length us \<Longrightarrow> (xs @ us, ys @ vs) \<in> lex r"
@@ -5960,12 +5938,13 @@
by (unfold lexord_def, induct_tac x, auto)
lemma lexord_cons_cons[simp]:
- "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r))"
- apply (unfold lexord_def, safe, simp_all)
- apply (case_tac u, simp, simp)
- apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
- apply (erule_tac x="b # u" in allE)
- by force
+ "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r))"
+ unfolding lexord_def
+ apply (safe, simp_all)
+ apply (metis hd_append list.sel(1))
+ apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
+ apply blast
+ by (meson Cons_eq_appendI)
lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
@@ -5989,24 +5968,17 @@
(\<exists>i. i < min(length x)(length y) \<and> take i x = take i y \<and> (x!i,y!i) \<in> r))"
apply (unfold lexord_def Let_def, clarsimp)
apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
+ apply (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
apply auto
- apply (rule_tac x="hd (drop (length x) y)" in exI)
- apply (rule_tac x="tl (drop (length x) y)" in exI)
- apply (erule subst, simp add: min_def)
apply (rule_tac x ="length u" in exI, simp)
- apply (rule_tac x ="take i x" in exI)
- apply (rule_tac x ="x ! i" in exI)
- apply (rule_tac x ="y ! i" in exI, safe)
- apply (rule_tac x="drop (Suc i) x" in exI)
- apply (drule sym, simp add: Cons_nth_drop_Suc)
- apply (rule_tac x="drop (Suc i) y" in exI)
- by (simp add: Cons_nth_drop_Suc)
+ by (metis id_take_nth_drop)
\<comment> \<open>lexord is extension of partial ordering List.lex\<close>
lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
- apply (rule_tac x = y in spec)
- apply (induct_tac x, clarsimp)
- by (clarify, case_tac x, simp, force)
+proof (induction x arbitrary: y)
+ case (Cons a x y) then show ?case
+ by (cases y) (force+)
+qed auto
lemma lexord_irreflexive: "\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
by (induct xs) auto
@@ -6049,12 +6021,15 @@
lemma lexord_transI: "trans r \<Longrightarrow> trans (lexord r)"
by (rule transI, drule lexord_trans, blast)
-lemma lexord_linear: "(\<forall>a b. (a,b)\<in> r \<or> a = b \<or> (b,a) \<in> r) \<Longrightarrow> (x,y) \<in> lexord r \<or> x = y \<or> (y,x) \<in> lexord r"
- apply (rule_tac x = y in spec)
- apply (induct_tac x, rule allI)
- apply (case_tac x, simp, simp)
- apply (rule allI, case_tac x, simp, simp)
- by blast
+lemma lexord_linear: "(\<forall>a b. (a,b) \<in> r \<or> a = b \<or> (b,a) \<in> r) \<Longrightarrow> (x,y) \<in> lexord r \<or> x = y \<or> (y,x) \<in> lexord r"
+proof (induction x arbitrary: y)
+ case Nil
+ then show ?case
+ by (metis lexord_Nil_left list.exhaust)
+next
+ case (Cons a x y) then show ?case
+ by (cases y) (force+)
+qed
lemma lexord_irrefl:
"irrefl R \<Longrightarrow> irrefl (lexord R)"
@@ -6220,27 +6195,17 @@
lemma lexordp_eq_trans:
assumes "lexordp_eq xs ys" and "lexordp_eq ys zs"
shows "lexordp_eq xs zs"
-using assms
-apply(induct arbitrary: zs)
-apply(case_tac [2-3] zs)
-apply auto
-done
+ using assms
+ by (induct arbitrary: zs) (case_tac zs; auto)+
lemma lexordp_trans:
assumes "lexordp xs ys" "lexordp ys zs"
shows "lexordp xs zs"
-using assms
-apply(induct arbitrary: zs)
-apply(case_tac [2-3] zs)
-apply auto
-done
+ using assms
+ by (induct arbitrary: zs) (case_tac zs; auto)+
lemma lexordp_linear: "lexordp xs ys \<or> xs = ys \<or> lexordp ys xs"
-proof(induct xs arbitrary: ys)
- case Nil thus ?case by(cases ys) simp_all
-next
- case Cons thus ?case by(cases ys) auto
-qed
+ by(induct xs arbitrary: ys; case_tac ys; fastforce)
lemma lexordp_conv_lexordp_eq: "lexordp xs ys \<longleftrightarrow> lexordp_eq xs ys \<and> \<not> lexordp_eq ys xs"
(is "?lhs \<longleftrightarrow> ?rhs")
@@ -6258,13 +6223,11 @@
by(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl dest: lexordp_eq_antisym)
lemma lexordp_eq_linear: "lexordp_eq xs ys \<or> lexordp_eq ys xs"
-apply(induct xs arbitrary: ys)
-apply(case_tac [!] ys)
-apply auto
-done
+ by (induct xs arbitrary: ys) (case_tac ys; auto)+
lemma lexordp_linorder: "class.linorder lexordp_eq lexordp"
-by unfold_locales(auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
+ by unfold_locales
+ (auto simp add: lexordp_conv_lexordp_eq lexordp_eq_refl lexordp_eq_antisym intro: lexordp_eq_trans del: disjCI intro: lexordp_eq_linear)
end
@@ -6402,17 +6365,20 @@
apply (induct arbitrary: xs set: Wellfounded.acc)
apply (erule thin_rl)
apply (erule acc_induct)
-apply (rule accI)
+ apply (rule accI)
apply (blast)
done
lemma lists_accD: "xs \<in> lists (Wellfounded.acc r) \<Longrightarrow> xs \<in> Wellfounded.acc (listrel1 r)"
-apply (induct set: lists)
- apply (rule accI)
- apply simp
-apply (rule accI)
-apply (fast dest: acc_downward)
-done
+proof (induct set: lists)
+ case Nil
+ then show ?case
+ by (meson acc.intros not_listrel1_Nil)
+next
+ case (Cons a l)
+ then show ?case
+ by blast
+qed
lemma lists_accI: "xs \<in> Wellfounded.acc (listrel1 r) \<Longrightarrow> xs \<in> lists (Wellfounded.acc r)"
apply (induct set: Wellfounded.acc)
@@ -6459,10 +6425,7 @@
lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
-apply clarify
-apply (erule listrel.induct)
-apply (blast intro: listrel.intros)+
-done
+ by (meson listrel_iff_nth subrelI subset_eq)
lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
apply clarify
@@ -6477,10 +6440,7 @@
done
lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"
-apply (auto simp add: sym_def)
-apply (erule listrel.induct)
-apply (blast intro: listrel.intros)+
-done
+ by (simp add: listrel_iff_nth sym_def)
lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"
apply (simp add: trans_def)
@@ -7365,10 +7325,7 @@
"(rel_set A ===> rel_set (list_all2 A) ===> rel_set (list_all2 A))
set_Cons set_Cons"
unfolding rel_fun_def rel_set_def set_Cons_def
- apply safe
- apply (simp add: list_all2_Cons1, fast)
- apply (simp add: list_all2_Cons2, fast)
- done
+ by (fastforce simp add: list_all2_Cons1 list_all2_Cons2)
lemma listset_transfer [transfer_rule]:
"(list_all2 (rel_set A) ===> rel_set (list_all2 A)) listset listset"