--- a/src/HOL/List.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/HOL/List.thy Sun Mar 22 17:21:16 2020 +0000
@@ -853,7 +853,7 @@
"(Suc n \<le> length xs) = (\<exists>x ys. xs = x # ys \<and> n \<le> length ys)"
by (metis Suc_le_D[of n] Suc_le_mono[of n] Suc_length_conv[of _ xs])
-lemma impossible_Cons: "length xs \<le> length ys ==> xs = x # ys = False"
+lemma impossible_Cons: "length xs \<le> length ys \<Longrightarrow> xs = x # ys = False"
by (induct xs) auto
lemma list_induct2 [consumes 1, case_names Nil Cons]:
@@ -972,7 +972,7 @@
lemma append_eq_append_conv [simp]:
"length xs = length ys \<or> length us = length vs
- ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
+ \<Longrightarrow> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
by (induct xs arbitrary: ys; case_tac ys; force)
lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
@@ -998,19 +998,19 @@
lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
using append_same_eq [of "[]"] by auto
-lemma hd_Cons_tl: "xs \<noteq> [] ==> hd xs # tl xs = xs"
+lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
by (fact list.collapse)
lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
by (induct xs) auto
-lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
+lemma hd_append2 [simp]: "xs \<noteq> [] \<Longrightarrow> hd (xs @ ys) = hd xs"
by (simp add: hd_append split: list.split)
lemma tl_append: "tl (xs @ ys) = (case xs of [] \<Rightarrow> tl ys | z#zs \<Rightarrow> zs @ ys)"
by (simp split: list.split)
-lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
+lemma tl_append2 [simp]: "xs \<noteq> [] \<Longrightarrow> tl (xs @ ys) = tl xs @ ys"
by (simp add: tl_append split: list.split)
@@ -1031,16 +1031,14 @@
text \<open>Trivial rules for solving \<open>@\<close>-equations automatically.\<close>
-lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
-by simp
-
-lemma Cons_eq_appendI:
-"[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
-by (drule sym) simp
-
-lemma append_eq_appendI:
-"[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
-by (drule sym) simp
+lemma eq_Nil_appendI: "xs = ys \<Longrightarrow> xs = [] @ ys"
+ by simp
+
+lemma Cons_eq_appendI: "\<lbrakk>x # xs1 = ys; xs = xs1 @ zs\<rbrakk> \<Longrightarrow> x # xs = ys @ zs"
+ by auto
+
+lemma append_eq_appendI: "\<lbrakk>xs @ xs1 = zs; ys = xs1 @ us\<rbrakk> \<Longrightarrow> xs @ ys = zs @ us"
+ by auto
text \<open>
@@ -1100,7 +1098,7 @@
lemma map_tl: "map f (tl xs) = tl (map f xs)"
by (cases xs) simp_all
-lemma map_ext: "(\<And>x. x \<in> set xs \<longrightarrow> f x = g x) ==> map f xs = map g xs"
+lemma map_ext: "(\<And>x. x \<in> set xs \<longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g xs"
by (induct xs) simp_all
lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
@@ -1175,16 +1173,16 @@
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 \<Longrightarrow> inj f \<Longrightarrow> xs = ys"
by (induct ys arbitrary: xs) (auto dest!:injD)
lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
by(blast dest:map_injective)
-lemma inj_mapI: "inj f ==> inj (map f)"
+lemma inj_mapI: "inj f \<Longrightarrow> inj (map f)"
by (iprover dest: map_injective injD intro: inj_onI)
-lemma inj_mapD: "inj (map f) ==> inj f"
+lemma inj_mapD: "inj (map f) \<Longrightarrow> inj f"
by (metis (no_types, hide_lams) injI list.inject list.simps(9) the_inv_f_f)
lemma inj_map[iff]: "inj (map f) = inj f"
@@ -1260,13 +1258,16 @@
by(simp add:inj_on_def)
lemma rev_induct [case_names Nil snoc]:
- "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(simplesubst rev_rev_ident[symmetric])
-apply(rule_tac list = "rev xs" in list.induct, simp_all)
-done
+ assumes "P []" and "\<And>x xs. P xs \<Longrightarrow> P (xs @ [x])"
+ shows "P xs"
+proof -
+ have "P (rev (rev xs))"
+ by (rule_tac list = "rev xs" in list.induct, simp_all add: assms)
+ then show ?thesis by simp
+qed
lemma rev_exhaust [case_names Nil snoc]:
- "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
+ "(xs = [] \<Longrightarrow> P) \<Longrightarrow>(\<And>ys y. xs = ys @ [y] \<Longrightarrow> P) \<Longrightarrow> P"
by (induct xs rule: rev_induct) auto
lemmas rev_cases = rev_exhaust
@@ -1475,10 +1476,10 @@
"length(filter P xs) + length(filter (\<lambda>x. \<not>P x) xs) = length xs"
by(induct xs) simp_all
-lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
+lemma filter_True [simp]: "\<forall>x \<in> set xs. P x \<Longrightarrow> filter P xs = xs"
by (induct xs) auto
-lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
+lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x \<Longrightarrow> filter P xs = []"
by (induct xs) auto
lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"
@@ -1664,13 +1665,13 @@
lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
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)"
+lemma concat_eq_concat_iff: "\<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> length xs = length ys \<Longrightarrow> (concat xs = concat ys) = (xs = ys)"
proof (induct xs arbitrary: ys)
case (Cons x xs ys)
thus ?case by (cases ys) auto
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"
+lemma concat_injective: "concat xs = concat ys \<Longrightarrow> length xs = length ys \<Longrightarrow> \<forall>(x, y) \<in> set (zip xs ys). length x = length y \<Longrightarrow> xs = ys"
by (simp add: concat_eq_concat_iff)
lemma concat_eq_appendD:
@@ -1725,7 +1726,7 @@
lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
by (induct xs) auto
-lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
+lemma nth_map [simp]: "n < length xs \<Longrightarrow> (map f xs)!n = f(xs!n)"
proof (induct xs arbitrary: n)
case (Cons x xs)
then show ?case
@@ -1856,13 +1857,13 @@
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)"
+ "i < length xs\<Longrightarrow> (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"
+lemma nth_list_update_eq [simp]: "i < length xs \<Longrightarrow> (xs[i:=x])!i = x"
by (simp add: nth_list_update)
-lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
+lemma nth_list_update_neq [simp]: "i \<noteq> j \<Longrightarrow> xs[i:=x]!j = xs!j"
by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
lemma list_update_id[simp]: "xs[i := xs!i] = xs"
@@ -1879,7 +1880,7 @@
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 \<Longrightarrow> (xs[i := x] = xs) = (xs!i = x)"
by (induct xs arbitrary: i) (auto split: nat.split)
lemma list_update_append1:
@@ -2105,10 +2106,10 @@
lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
-lemma take_all [simp]: "length xs \<le> n ==> take n xs = xs"
+lemma take_all [simp]: "length xs \<le> n \<Longrightarrow> take n xs = xs"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
-lemma drop_all [simp]: "length xs \<le> n ==> drop n xs = []"
+lemma drop_all [simp]: "length xs \<le> n \<Longrightarrow> drop n xs = []"
by (induct n arbitrary: xs) (auto, case_tac xs, auto)
lemma take_append [simp]:
@@ -2206,7 +2207,7 @@
lemma take_rev: "take n (rev xs) = rev (drop (length xs - n) xs)"
by (cases "length xs < n") (auto simp: rev_drop)
-lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
+lemma nth_take [simp]: "i < n \<Longrightarrow> (take n xs)!i = xs!i"
proof (induct xs arbitrary: i n)
case Nil
then show ?case by simp
@@ -2216,7 +2217,7 @@
qed
lemma nth_drop [simp]:
- "n \<le> length xs ==> (drop n xs)!i = xs!(n + i)"
+ "n \<le> length xs \<Longrightarrow> (drop n xs)!i = xs!(n + i)"
proof (induct n arbitrary: xs)
case 0
then show ?case by simp
@@ -2226,13 +2227,13 @@
qed
lemma butlast_take:
- "n \<le> length xs ==> butlast (take n xs) = take (n - 1) xs"
+ "n \<le> length xs \<Longrightarrow> butlast (take n xs) = take (n - 1) xs"
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)
-lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
+lemma take_butlast: "n < length xs \<Longrightarrow> take n (butlast xs) = take n xs"
by (simp add: butlast_conv_take min.absorb1)
lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
@@ -2390,7 +2391,7 @@
by (induct xs) auto
lemma dropWhile_append2 [simp]:
- "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
+ "(\<And>x. x \<in> set xs \<Longrightarrow> P(x)) \<Longrightarrow> dropWhile P (xs @ ys) = dropWhile P ys"
by (induct xs) auto
lemma dropWhile_append3:
@@ -2419,10 +2420,10 @@
"(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \<and> \<not> P y)"
by(induct xs, auto)
-lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
+lemma distinct_takeWhile[simp]: "distinct xs \<Longrightarrow> distinct (takeWhile P xs)"
by (induct xs) (auto dest: set_takeWhileD)
-lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
+lemma distinct_dropWhile[simp]: "distinct xs \<Longrightarrow> distinct (dropWhile P xs)"
by (induct xs) auto
lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
@@ -2582,12 +2583,12 @@
by (induct xs ys rule:list_induct2') auto
lemma zip_append [simp]:
- "[| length xs = length us |] ==>
+ "\<lbrakk>length xs = length us\<rbrakk> \<Longrightarrow>
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 \<Longrightarrow> zip (rev xs) (rev ys) = rev (zip xs ys)"
by (induct rule:list_induct2, simp_all)
lemma zip_map_map:
@@ -2622,7 +2623,7 @@
by(induct xs) auto
lemma nth_zip [simp]:
- "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
+ "\<lbrakk>i < length xs; i < length ys\<rbrakk> \<Longrightarrow> (zip xs ys)!i = (xs!i, ys!i)"
proof (induct ys arbitrary: i xs)
case (Cons y ys)
then show ?case
@@ -2804,7 +2805,7 @@
subsubsection \<open>\<^const>\<open>list_all2\<close>\<close>
lemma list_all2_lengthD [intro?]:
- "list_all2 P xs ys ==> length xs = length ys"
+ "list_all2 P xs ys \<Longrightarrow> length xs = length ys"
by (simp add: list_all2_iff)
lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
@@ -2892,8 +2893,8 @@
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"
+ assumes tr: "!!a b c. P1 a b \<Longrightarrow> P2 b c \<Longrightarrow> P3 a c"
+ shows "!!bs cs. list_all2 P1 as bs \<Longrightarrow> list_all2 P2 bs cs \<Longrightarrow> list_all2 P3 as 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"
@@ -3224,7 +3225,7 @@
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] = []"
+lemma upt_conv_Nil [simp]: "j \<le> i \<Longrightarrow> [i..<j] = []"
by (subst upt_rec) simp
lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j \<le> i)"
@@ -3238,11 +3239,11 @@
by (simp add: upt_rec)
qed simp
-lemma upt_Suc_append: "i \<le> j ==> [i..<(Suc j)] = [i..<j]@[j]"
+lemma upt_Suc_append: "i \<le> j \<Longrightarrow> [i..<(Suc j)] = [i..<j]@[j]"
\<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]"
+lemma upt_conv_Cons: "i < j \<Longrightarrow> [i..<j] = i # [Suc i..<j]"
by (simp add: upt_rec)
lemma upt_conv_Cons_Cons: \<comment> \<open>no precondition\<close>
@@ -3253,14 +3254,14 @@
case True then show ?thesis by (simp add: upt_conv_Cons)
qed
-lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
+lemma upt_add_eq_append: "i<=j \<Longrightarrow> [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
lemma length_upt [simp]: "length [i..<j] = j - i"
by (induct j) (auto simp add: Suc_diff_le)
-lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
+lemma nth_upt [simp]: "i + k < j \<Longrightarrow> [i..<j] ! k = i + k"
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"
@@ -3272,7 +3273,7 @@
lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
by(cases j)(auto simp: upt_Suc_append)
-lemma take_upt [simp]: "i+m \<le> n ==> take m [i..<n] = [i..<i+m]"
+lemma take_upt [simp]: "i+m \<le> n \<Longrightarrow> take m [i..<n] = [i..<i+m]"
proof (induct m arbitrary: i)
case (Suc m)
then show ?case
@@ -3288,7 +3289,7 @@
lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]"
by (induct m) simp_all
-lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
+lemma nth_map_upt: "i < n-m \<Longrightarrow> (map f [m..<n]) ! i = f(m+i)"
proof (induct n m arbitrary: i rule: diff_induct)
case (3 x y)
then show ?case
@@ -3324,7 +3325,7 @@
\<Longrightarrow> xs = ys"
by (simp add: list_all2_conv_all_nth nth_equalityI)
-lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
+lemma take_equalityI: "(\<forall>i. take i xs = take i ys) \<Longrightarrow> xs = ys"
\<comment> \<open>The famous take-lemma.\<close>
by (metis length_take min.commute order_refl take_all)
@@ -3403,10 +3404,11 @@
qed
lemma nth_upto[simp]: "i + int k \<le> j \<Longrightarrow> [i..j] ! k = i + int k"
- apply(induction i j arbitrary: k rule: upto.induct)
-apply(subst upto_rec1)
-apply(auto simp add: nth_Cons')
-done
+proof(induction i j arbitrary: k rule: upto.induct)
+ case (1 i j)
+ then show ?case
+ by (auto simp add: upto_rec1 [of i j] nth_Cons')
+qed
lemma upto_split1:
"i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..k] = [i..j-1] @ [j..k]"
@@ -3454,7 +3456,7 @@
lemma distinct_remdups [iff]: "distinct (remdups xs)"
by (induct xs) auto
-lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
+lemma distinct_remdups_id: "distinct xs \<Longrightarrow> remdups xs = xs"
by (induct xs, auto)
lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
@@ -3491,17 +3493,18 @@
"distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))"
by (induct xs) auto
-lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
+lemma distinct_filter [simp]: "distinct xs \<Longrightarrow> distinct (filter P xs)"
by (induct xs) auto
lemma distinct_upt[simp]: "distinct[i..<j]"
by (induct j) auto
lemma distinct_upto[simp]: "distinct[i..j]"
-apply(induct i j rule:upto.induct)
-apply(subst upto.simps)
-apply(simp)
-done
+proof (induction i j rule: upto.induct)
+ case (1 i j)
+ then show ?case
+ by (simp add: upto.simps [of i])
+qed
lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
proof (induct xs arbitrary: i)
@@ -3531,10 +3534,10 @@
by auto
next
case False
+ have "set (take i xs) \<inter> set (drop (Suc i) xs) = {}"
+ by (metis True d disjoint_insert(1) distinct_append id_take_nth_drop list.set(2))
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))
+ using d False anot \<open>i < length xs\<close> by (simp add: upd_conv_take_nth_drop)
qed
next
case False with d show ?thesis by auto
@@ -3580,21 +3583,20 @@
set(xs[n := x]) = insert x (set xs - {xs!n})"
by(auto simp: set_eq_iff in_set_conv_nth nth_list_update nth_eq_iff_index_eq)
-lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow>
+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 safe
-apply metis+
-done
+ apply (safe; metis)
+ done
lemma set_swap[simp]:
"\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow> set(xs[i := xs!j, j := xs!i]) = set xs"
by(simp add: set_conv_nth nth_list_update) metis
-lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
+lemma distinct_card: "distinct xs \<Longrightarrow> card (set xs) = size xs"
by (induct xs) auto
-lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
+lemma card_distinct: "card (set xs) = size xs \<Longrightarrow> distinct xs"
proof (induct xs)
case (Cons x xs)
show ?case
@@ -3822,18 +3824,12 @@
using f_mono by (simp add: mono_iff_le_Suc)
next
have "?f' ` {0 ..< length (x1 # xs)} = f ` {Suc 0 ..< length (x1 # x2 # xs)}"
- apply safe
- apply fastforce
- subgoal for \<dots> x by (cases x) auto
- done
+ using less_Suc_eq_0_disj by auto
also have "\<dots> = f ` {0 ..< length (x1 # x2 # xs)}"
proof -
have "f 0 = f (Suc 0)" using \<open>x1 = x2\<close> f_nth[of 0] by simp
then show ?thesis
- apply safe
- apply fastforce
- subgoal for \<dots> x by (cases x) auto
- done
+ using less_Suc_eq_0_disj by auto
qed
also have "\<dots> = {0 ..< length ys}" by fact
finally show "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" .
@@ -3842,7 +3838,7 @@
next
assume "x1 \<noteq> x2"
- have "2 \<le> length ys"
+ have two: "Suc (Suc 0) \<le> length ys"
proof -
have "2 = card {f 0, f 1}" using \<open>x1 \<noteq> x2\<close> f_nth[of 0] by auto
also have "\<dots> \<le> card (f ` {0..< length (x1 # x2 # xs)})"
@@ -3862,26 +3858,18 @@
then have "Suc 0 \<noteq> f i" for i using \<open>f 0 = 0\<close>
by (cases i) fastforce+
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
+ then show False using f_img two 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)
- apply (rename_tac [2] ys', case_tac [2] ys')
- apply (auto simp: \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
- done
+ using two f_nth[of 0] f_nth[of 1]
+ by (auto simp: Suc_le_length_iff \<open>f 0 = 0\<close> \<open>f (Suc 0) = Suc 0\<close>)
+
+ have Suc0_le_f_Suc: "Suc 0 \<le> f (Suc i)" for i
+ by (metis Suc_le_mono \<open>f (Suc 0) = Suc 0\<close> f_mono le0 mono_def)
define f' where "f' x = f (Suc x) - 1" for x
-
- { fix i
- have "Suc 0 \<le> f (Suc 0)" using f_nth[of 0] \<open>x1 \<noteq> x2\<close> \<open>f 0 = 0\<close> by auto
- also have "\<dots> \<le> f (Suc i)" using f_mono by (rule monoD) arith
- finally have "Suc 0 \<le> f (Suc i)" .
- } note Suc0_le_f_Suc = this
-
- { fix i have "f (Suc i) = Suc (f' i)"
+ have f_Suc: "f (Suc i) = Suc (f' i)" for i
using Suc0_le_f_Suc[of i] by (auto simp: f'_def)
- } note f_Suc = this
have "remdups_adj (x2 # xs) = (x2 # ys')"
proof (intro "3.hyps" exI conjI impI allI)
@@ -3904,15 +3892,15 @@
qed
lemma hd_remdups_adj[simp]: "hd (remdups_adj xs) = hd xs"
-by (induction xs rule: remdups_adj.induct) simp_all
+ by (induction xs rule: remdups_adj.induct) simp_all
lemma remdups_adj_Cons: "remdups_adj (x # xs) =
(case remdups_adj xs of [] \<Rightarrow> [x] | y # xs \<Rightarrow> if x = y then y # xs else x # y # xs)"
-by (induct xs arbitrary: x) (auto split: list.splits)
+ by (induct xs arbitrary: x) (auto split: list.splits)
lemma remdups_adj_append_two:
"remdups_adj (xs @ [x,y]) = remdups_adj (xs @ [x]) @ (if x = y then [] else [y])"
-by (induct xs rule: remdups_adj.induct, simp_all)
+ by (induct xs rule: remdups_adj.induct, simp_all)
lemma remdups_adj_adjacent:
"Suc i < length (remdups_adj xs) \<Longrightarrow> remdups_adj xs ! i \<noteq> remdups_adj xs ! Suc i"
@@ -4059,8 +4047,8 @@
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)
+ using sum.remove [of X x "count_list xs"]
+ by (auto simp: sum.If_cases simp flip: diff_eq)
qed simp
@@ -4237,16 +4225,16 @@
"filter P (replicate n x) = (if P x then replicate n x else [])"
by(induct n) auto
-lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
+lemma hd_replicate [simp]: "n \<noteq> 0 \<Longrightarrow> hd (replicate n x) = x"
by (induct n) auto
lemma tl_replicate [simp]: "tl (replicate n x) = replicate (n - 1) x"
by (induct n) auto
-lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
+lemma last_replicate [simp]: "n \<noteq> 0 \<Longrightarrow> last (replicate n x) = x"
by (atomize (full), induct n) auto
-lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
+lemma nth_replicate[simp]: "i < n \<Longrightarrow> (replicate n x)!i = x"
by (induct n arbitrary: i)(auto simp: nth_Cons split: nat.split)
text\<open>Courtesy of Matthias Daum (2 lemmas):\<close>
@@ -4273,7 +4261,7 @@
lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
by (induct n) auto
-lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
+lemma set_replicate [simp]: "n \<noteq> 0 \<Longrightarrow> set (replicate n x) = {x}"
by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
@@ -4495,8 +4483,7 @@
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)
+ by (auto simp add: mod_Suc False Suc.hyps drop_Suc rotate1_hd_tl take_Suc Suc_length_conv)
next
case False
with \<open>xs \<noteq> []\<close> Suc
@@ -4508,37 +4495,37 @@
qed simp
lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
-by(simp add:rotate_drop_take)
+ by(simp add:rotate_drop_take)
lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
-by(simp add:rotate_drop_take)
+ by(simp add:rotate_drop_take)
lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
-by (cases xs) simp_all
+ by (cases xs) simp_all
lemma length_rotate[simp]: "length(rotate n xs) = length xs"
-by (induct n arbitrary: xs) (simp_all add:rotate_def)
+ by (induct n arbitrary: xs) (simp_all add:rotate_def)
lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
-by (cases xs) auto
+ by (cases xs) auto
lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
-by (induct n) (simp_all add:rotate_def)
+ by (induct n) (simp_all add:rotate_def)
lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
-by(simp add:rotate_drop_take take_map drop_map)
+ by(simp add:rotate_drop_take take_map drop_map)
lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
-by (cases xs) auto
+ by (cases xs) auto
lemma set_rotate[simp]: "set(rotate n xs) = set xs"
-by (induct n) (simp_all add:rotate_def)
+ by (induct n) (simp_all add:rotate_def)
lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
-by (cases xs) auto
+ by (cases xs) auto
lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
-by (induct n) (simp_all add:rotate_def)
+ by (induct n) (simp_all add:rotate_def)
lemma rotate_rev:
"rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
@@ -4564,21 +4551,20 @@
subsubsection \<open>\<^const>\<open>nths\<close> --- a generalization of \<^const>\<open>nth\<close> to sets\<close>
lemma nths_empty [simp]: "nths xs {} = []"
-by (auto simp add: nths_def)
+ by (auto simp add: nths_def)
lemma nths_nil [simp]: "nths [] A = []"
-by (auto simp add: nths_def)
+ by (auto simp add: nths_def)
lemma nths_all: "\<forall>i < length xs. i \<in> I \<Longrightarrow> nths xs I = xs"
apply (simp add: nths_def)
apply (subst filter_True)
- apply (clarsimp simp: in_set_zip subset_iff)
-apply simp
+ apply (auto simp: in_set_zip subset_iff)
done
lemma length_nths:
"length (nths xs I) = card{i. i < length xs \<and> i \<in> I}"
-by(simp add: nths_def length_filter_conv_card cong:conj_cong)
+ by(simp add: nths_def length_filter_conv_card cong:conj_cong)
lemma nths_shift_lemma_Suc:
"map fst (filter (\<lambda>p. P(Suc(snd p))) (zip xs is)) =
@@ -4612,46 +4598,41 @@
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)
+ 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}"
-by (induct xs arbitrary: I) (auto simp: nths_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
+ 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)
+ by(auto simp add:set_nths)
lemma notin_set_nthsI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(nths xs I)"
-by(auto simp add:set_nths)
+ by(auto simp add:set_nths)
lemma in_set_nthsD: "x \<in> set(nths xs I) \<Longrightarrow> x \<in> set xs"
-by(auto simp add:set_nths)
+ by(auto simp add:set_nths)
lemma nths_singleton [simp]: "nths [x] A = (if 0 \<in> A then [x] else [])"
-by (simp add: nths_Cons)
+ by (simp add: nths_Cons)
lemma distinct_nthsI[simp]: "distinct xs \<Longrightarrow> distinct (nths xs I)"
-by (induct xs arbitrary: I) (auto simp: nths_Cons)
+ by (induct xs arbitrary: I) (auto simp: nths_Cons)
lemma nths_upt_eq_take [simp]: "nths l {..<n} = take n l"
-by (induct l rule: rev_induct)
- (simp_all split: nat_diff_split add: nths_append)
+ by (induct l rule: rev_induct) (simp_all split: nat_diff_split add: nths_append)
lemma nths_nths: "nths (nths xs A) B = nths xs {i \<in> A. \<exists>j \<in> B. card {i' \<in> A. i' < i} = j}"
-apply(induction xs arbitrary: A B)
-apply(auto simp add: nths_Cons card_less_Suc card_less_Suc2)
-done
+ by (induction xs arbitrary: A B) (auto simp add: nths_Cons card_less_Suc card_less_Suc2)
lemma drop_eq_nths: "drop n xs = nths xs {i. i \<ge> n}"
-apply(induction xs arbitrary: n)
-apply (auto simp add: nths_Cons nths_all drop_Cons' intro: arg_cong2[where f=nths, OF refl])
-done
+ by (induction xs arbitrary: n) (auto simp add: nths_Cons nths_all drop_Cons' intro: arg_cong2[where f=nths, OF refl])
lemma nths_drop: "nths (drop n xs) I = nths xs ((+) n ` I)"
by(force simp: drop_eq_nths nths_nths simp flip: atLeastLessThan_iff
intro: arg_cong2[where f=nths, OF refl])
lemma filter_eq_nths: "filter P xs = nths xs {i. i<length xs \<and> P(xs!i)}"
-by(induction xs) (auto simp: nths_Cons)
+ by(induction xs) (auto simp: nths_Cons)
lemma filter_in_nths:
"distinct xs \<Longrightarrow> filter (%x. x \<in> set (nths xs s)) xs = nths xs s"
@@ -4732,18 +4713,20 @@
subsubsection \<open>\<^const>\<open>splice\<close>\<close>
lemma splice_Nil2 [simp]: "splice xs [] = xs"
-by (cases xs) simp_all
+ by (cases xs) simp_all
lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
-by (induct xs ys rule: splice.induct) auto
+ by (induct xs ys rule: splice.induct) auto
lemma split_Nil_iff[simp]: "splice xs ys = [] \<longleftrightarrow> xs = [] \<and> ys = []"
-by (induct xs ys rule: splice.induct) auto
+ by (induct xs ys rule: splice.induct) auto
lemma splice_replicate[simp]: "splice (replicate m x) (replicate n x) = replicate (m+n) x"
-apply(induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
-apply (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
-done
+proof (induction "replicate m x" "replicate n x" arbitrary: m n rule: splice.induct)
+ case (2 x xs)
+ then show ?case
+ by (auto simp add: Cons_replicate_eq dest: gr0_implies_Suc)
+qed auto
subsubsection \<open>\<^const>\<open>shuffles\<close>\<close>
@@ -4768,7 +4751,7 @@
by (induct xs ys rule: shuffles.induct) auto
lemma splice_in_shuffles [simp, intro]: "splice xs ys \<in> shuffles xs ys"
-by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffles_iff shuffles_commutes)
+ by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffles_iff shuffles_commutes)
lemma Nil_in_shufflesI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffles xs ys"
by simp
@@ -5001,13 +4984,13 @@
subsubsection \<open>\<^const>\<open>min\<close> and \<^const>\<open>arg_min\<close>\<close>
lemma min_list_Min: "xs \<noteq> [] \<Longrightarrow> min_list xs = Min (set xs)"
-by (induction xs rule: induct_list012)(auto)
+ by (induction xs rule: induct_list012)(auto)
lemma f_arg_min_list_f: "xs \<noteq> [] \<Longrightarrow> f (arg_min_list f xs) = Min (f ` (set xs))"
-by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
+ by(induction f xs rule: arg_min_list.induct) (auto simp: min_def intro!: antisym)
lemma arg_min_list_in: "xs \<noteq> [] \<Longrightarrow> arg_min_list f xs \<in> set xs"
-by(induction xs rule: induct_list012) (auto simp: Let_def)
+ by(induction xs rule: induct_list012) (auto simp: Let_def)
subsubsection \<open>(In)finiteness\<close>
@@ -5811,19 +5794,19 @@
lemma sorted_list_of_set_empty:
"sorted_list_of_set {} = []"
-by (fact sorted_list_of_set.empty)
+ by (fact sorted_list_of_set.empty)
lemma sorted_list_of_set_insert [simp]:
"finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
-by (fact sorted_list_of_set.insert_remove)
+ by (fact sorted_list_of_set.insert_remove)
lemma sorted_list_of_set_eq_Nil_iff [simp]:
"finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
-by (auto simp: sorted_list_of_set.remove)
+ by (auto simp: sorted_list_of_set.remove)
lemma set_sorted_list_of_set [simp]:
"finite A \<Longrightarrow> set (sorted_list_of_set A) = A"
-by(induct A rule: finite_induct) (simp_all add: set_insort_key)
+ by(induct A rule: finite_induct) (simp_all add: set_insort_key)
lemma sorted_sorted_list_of_set [simp]: "sorted (sorted_list_of_set A)"
proof (cases "finite A")
@@ -5894,13 +5877,13 @@
"listsp A []"
"listsp A (x # xs)"
-lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
+lemma listsp_mono [mono]: "A \<le> B \<Longrightarrow> listsp A \<le> listsp B"
by (rule predicate1I, erule listsp.induct, blast+)
lemmas lists_mono = listsp_mono [to_set]
lemma listsp_infI:
- assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
+ assumes l: "listsp A l" shows "listsp B l \<Longrightarrow> listsp (inf A B) l" using l
by induct blast+
lemmas lists_IntI = listsp_infI [to_set]
@@ -5930,12 +5913,12 @@
lemmas in_lists_conv_set [code_unfold] = in_listsp_conv_set [to_set]
-lemma in_listspD [dest!]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
+lemma in_listspD [dest!]: "listsp A xs \<Longrightarrow> \<forall>x\<in>set xs. A x"
by (rule in_listsp_conv_set [THEN iffD1])
lemmas in_listsD [dest!] = in_listspD [to_set]
-lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
+lemma in_listspI [intro!]: "\<forall>x\<in>set xs. A x \<Longrightarrow> listsp A xs"
by (rule in_listsp_conv_set [THEN iffD2])
lemmas in_listsI [intro!] = in_listspI [to_set]
@@ -6025,24 +6008,31 @@
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)"
+ by (induct n arbitrary: xs ys) auto
+
+lemma wf_lex [intro!]:
+ assumes "wf r" shows "wf (lex r)"
unfolding lex_def
- apply (rule wf_UN)
- apply (simp add: wf_lexn)
- apply (metis DomainE Int_emptyI RangeE lexn_length)
- done
+proof (rule wf_UN)
+ show "wf (lexn r i)" for i
+ by (simp add: assms wf_lexn)
+ show "\<And>i j. lexn r i \<noteq> lexn r j \<Longrightarrow> Domain (lexn r i) \<inter> Range (lexn r j) = {}"
+ by (metis DomainE Int_emptyI RangeE lexn_length)
+qed
+
lemma lexn_conv:
"lexn r n =
{(xs,ys). length xs = n \<and> length ys = n \<and>
(\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y) \<in> r)}"
-apply (induct n, simp)
-apply (simp add: image_Collect lex_prod_def, safe, blast)
- apply (rule_tac x = "ab # xys" in exI, simp)
-apply (case_tac xys, simp_all, blast)
-done
+proof (induction n)
+ case (Suc n)
+ then show ?case
+ apply (simp add: image_Collect lex_prod_def, safe, blast)
+ apply (rule_tac x = "ab # xys" in exI, simp)
+ apply (case_tac xys; force)
+ done
+qed auto
text\<open>By Mathias Fleury:\<close>
proposition lexn_transI:
@@ -6121,7 +6111,7 @@
(\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> r)}"
by (force simp add: lex_def lexn_conv)
-lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
+lemma wf_lenlex [intro!]: "wf r \<Longrightarrow> wf (lenlex r)"
by (unfold lenlex_def) blast
lemma lenlex_conv:
@@ -6152,18 +6142,21 @@
by (meson lex_transI trans_inv_image trans_less_than trans_lex_prod)
lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
-by (simp add: lex_conv)
+ by (simp add: lex_conv)
lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
-by (simp add:lex_conv)
+ by (simp add:lex_conv)
lemma Cons_in_lex [simp]:
- "((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)
- by (metis hd_append append_Nil list.sel(1) list.sel(3) tl_append2)
+ "(x # xs, y # ys) \<in> lex r \<longleftrightarrow> (x, y) \<in> r \<and> length xs = length ys \<or> x = y \<and> (xs, ys) \<in> lex r"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ by (simp add: lex_conv) (metis hd_append list.sel(1) list.sel(3) tl_append2)
+next
+ assume ?rhs then show ?lhs
+ by (simp add: lex_conv) (blast intro: Cons_eq_appendI)
+qed
lemma Nil_lenlex_iff1 [simp]: "([], ns) \<in> lenlex r \<longleftrightarrow> ns \<noteq> []"
and Nil_lenlex_iff2 [simp]: "(ns,[]) \<notin> lenlex r"
@@ -6181,24 +6174,23 @@
lemma lex_append_rightI:
"(xs, ys) \<in> lex r \<Longrightarrow> length vs = length us \<Longrightarrow> (xs @ us, ys @ vs) \<in> lex r"
-by (fastforce simp: lex_def lexn_conv)
+ by (fastforce simp: lex_def lexn_conv)
lemma lex_append_leftI:
"(ys, zs) \<in> lex r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lex r"
-by (induct xs) auto
+ by (induct xs) auto
lemma lex_append_leftD:
"\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lex r \<Longrightarrow> (ys, zs) \<in> lex r"
-by (induct xs) auto
+ by (induct xs) auto
lemma lex_append_left_iff:
"\<forall>x. (x,x) \<notin> r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lex r \<longleftrightarrow> (ys, zs) \<in> lex r"
-by(metis lex_append_leftD lex_append_leftI)
+ by(metis lex_append_leftD lex_append_leftI)
lemma lex_take_index:
assumes "(xs, ys) \<in> lex r"
- obtains i where "i < length xs" and "i < length ys" and "take i xs =
-take i ys"
+ obtains i where "i < length xs" and "i < length ys" and "take i xs = take i ys"
and "(xs ! i, ys ! i) \<in> r"
proof -
obtain n us x xs' y ys' where "(xs, ys) \<in> lexn r n" and "length xs = n" and "length ys = n"
@@ -6225,40 +6217,47 @@
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))"
- unfolding lexord_def
- apply (safe, simp_all)
- apply (metis hd_append list.sel(1))
+ "(a # x, b # y) \<in> lexord r \<longleftrightarrow> (a,b)\<in> r \<or> (a = b \<and> (x,y)\<in> lexord r)" (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ apply (simp add: lexord_def)
apply (metis hd_append list.sel(1) list.sel(3) tl_append2)
- apply blast
- by (meson Cons_eq_appendI)
+ done
+qed (auto simp add: lexord_def; (blast | meson Cons_eq_appendI))
lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
-by (induct_tac x, auto)
+ by (induct_tac x, auto)
lemma lexord_append_left_rightI:
- "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
-by (induct_tac u, auto)
+ "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
+ by (induct_tac u, auto)
lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
-by (induct x, auto)
+ by (induct x, auto)
lemma lexord_append_leftD:
- "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (\<forall>a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
-by (erule rev_mp, induct_tac x, auto)
+ "\<lbrakk>(x @ u, x @ v) \<in> lexord r; (\<forall>a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
+ by (erule rev_mp, induct_tac x, auto)
lemma lexord_take_index_conv:
"((x,y) \<in> lexord r) =
((length x < length y \<and> take (length x) y = x) \<or>
(\<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 ="length u" in exI, simp)
- by (metis id_take_nth_drop)
+proof -
+ have "(\<exists>a v. y = x @ a # v) = (length x < length y \<and> take (length x) y = x)"
+ by (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le)
+ moreover
+ have "(\<exists>u a b. (a, b) \<in> r \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
+ (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r)"
+ apply safe
+ using less_iff_Suc_add apply auto[1]
+ by (metis id_take_nth_drop)
+ ultimately show ?thesis
+ by (auto simp: lexord_def Let_def)
+qed
\<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)"
@@ -6539,10 +6538,10 @@
unfolding measures_def
by auto
-lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
+lemma measures_less: "f x < f y \<Longrightarrow> (x, y) \<in> measures (f#fs)"
by simp
-lemma measures_lesseq: "f x \<le> f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
+lemma measures_lesseq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> measures fs \<Longrightarrow> (x, y) \<in> measures (f#fs)"
by auto
@@ -6685,7 +6684,7 @@
for r :: "('a \<times> 'b) set"
where
Nil: "([],[]) \<in> listrel r"
- | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
+ | Cons: "\<lbrakk>(x,y) \<in> r; (xs,ys) \<in> listrel r\<rbrakk> \<Longrightarrow> (x#xs, y#ys) \<in> listrel r"
inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"