--- a/src/HOL/List.thy Sun Mar 22 22:03:48 2020 +0100
+++ b/src/HOL/List.thy Mon Mar 23 10:26:08 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"
--- a/src/HOL/Nat.thy Sun Mar 22 22:03:48 2020 +0100
+++ b/src/HOL/Nat.thy Mon Mar 23 10:26:08 2020 +0000
@@ -65,15 +65,15 @@
by (rule iffI, rule Suc_Rep_inject) simp_all
lemma nat_induct0:
- assumes "P 0"
- and "\<And>n. P n \<Longrightarrow> P (Suc n)"
+ assumes "P 0" and "\<And>n. P n \<Longrightarrow> P (Suc n)"
shows "P n"
- using assms
- apply (unfold Zero_nat_def Suc_def)
- apply (rule Rep_Nat_inverse [THEN subst]) \<comment> \<open>types force good instantiation\<close>
- apply (erule Nat_Rep_Nat [THEN Nat.induct])
- apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
- done
+proof -
+ have "P (Abs_Nat (Rep_Nat n))"
+ using assms unfolding Zero_nat_def Suc_def
+ by (iprover intro: Nat_Rep_Nat [THEN Nat.induct] elim: Nat_Abs_Nat_inverse [THEN subst])
+ then show ?thesis
+ by (simp add: Rep_Nat_inverse)
+qed
free_constructors case_nat for "0 :: nat" | Suc pred
where "pred (0 :: nat) = (0 :: nat)"
@@ -87,11 +87,7 @@
setup \<open>Sign.mandatory_path "old"\<close>
old_rep_datatype "0 :: nat" Suc
- apply (erule nat_induct0)
- apply assumption
- apply (rule nat.inject)
- apply (rule nat.distinct(1))
- done
+ by (erule nat_induct0) auto
setup \<open>Sign.parent_path\<close>
@@ -356,18 +352,11 @@
qed
lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
- apply (rule trans)
- apply (rule_tac [2] mult_eq_1_iff)
- apply fastforce
- done
-
-lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
- for m n :: nat
- unfolding One_nat_def by (rule mult_eq_1_iff)
-
-lemma nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
- for m n :: nat
- unfolding One_nat_def by (rule one_eq_mult_iff)
+ by (simp add: eq_commute flip: mult_eq_1_iff)
+
+lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \<longleftrightarrow> m = 1 \<and> n = 1"
+ and nat_1_eq_mult_iff [simp]: "1 = m * n \<longleftrightarrow> m = 1 \<and> n = 1" for m n :: nat
+ by auto
lemma mult_cancel1 [simp]: "k * m = k * n \<longleftrightarrow> m = n \<or> k = 0"
for k m n :: nat
@@ -584,22 +573,23 @@
and less: "m < n \<Longrightarrow> P"
and eq: "m = n \<Longrightarrow> P"
shows P
- apply (rule major [THEN lessE])
- apply (rule eq)
- apply blast
- apply (rule less)
- apply blast
- done
+proof (rule major [THEN lessE])
+ show "Suc n = Suc m \<Longrightarrow> P"
+ using eq by blast
+ show "\<And>j. \<lbrakk>m < j; Suc n = Suc j\<rbrakk> \<Longrightarrow> P"
+ by (blast intro: less)
+qed
lemma Suc_lessE:
assumes major: "Suc i < k"
and minor: "\<And>j. i < j \<Longrightarrow> k = Suc j \<Longrightarrow> P"
shows P
- apply (rule major [THEN lessE])
- apply (erule lessI [THEN minor])
- apply (erule Suc_lessD [THEN minor])
- apply assumption
- done
+proof (rule major [THEN lessE])
+ show "k = Suc (Suc i) \<Longrightarrow> P"
+ using lessI minor by iprover
+ show "\<And>j. \<lbrakk>Suc i < j; k = Suc j\<rbrakk> \<Longrightarrow> P"
+ using Suc_lessD minor by iprover
+qed
lemma Suc_less_SucD: "Suc m < Suc n \<Longrightarrow> m < n"
by simp
@@ -786,12 +776,16 @@
by (induct k) simp_all
text \<open>strict, in both arguments\<close>
-lemma add_less_mono: "i < j \<Longrightarrow> k < l \<Longrightarrow> i + k < j + l"
- for i j k l :: nat
- apply (rule add_less_mono1 [THEN less_trans], assumption+)
- apply (induct j)
- apply simp_all
- done
+lemma add_less_mono:
+ fixes i j k l :: nat
+ assumes "i < j" "k < l" shows "i + k < j + l"
+proof -
+ have "i + k < j + k"
+ by (simp add: add_less_mono1 assms)
+ also have "... < j + l"
+ using \<open>i < j\<close> by (induction j) (auto simp: assms)
+ finally show ?thesis .
+qed
lemma less_imp_Suc_add: "m < n \<Longrightarrow> \<exists>k. n = Suc (m + k)"
proof (induct n)
@@ -969,42 +963,55 @@
for P :: "nat \<Rightarrow> bool"
by (rule Least_equality[OF _ le0])
-lemma Least_Suc: "P n \<Longrightarrow> \<not> P 0 \<Longrightarrow> (LEAST n. P n) = Suc (LEAST m. P (Suc m))"
- apply (cases n)
- apply auto
- apply (frule LeastI)
- apply (drule_tac P = "\<lambda>x. P (Suc x)" in LeastI)
- apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
- apply (erule_tac [2] Least_le)
- apply (cases "LEAST x. P x")
- apply auto
- apply (drule_tac P = "\<lambda>x. P (Suc x)" in Least_le)
- apply (blast intro: order_antisym)
- done
+lemma Least_Suc:
+ assumes "P n" "\<not> P 0"
+ shows "(LEAST n. P n) = Suc (LEAST m. P (Suc m))"
+proof (cases n)
+ case (Suc m)
+ show ?thesis
+ proof (rule antisym)
+ show "(LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))"
+ using assms Suc by (force intro: LeastI Least_le)
+ have \<section>: "P (LEAST x. P x)"
+ by (blast intro: LeastI assms)
+ show "Suc (LEAST m. P (Suc m)) \<le> (LEAST n. P n)"
+ proof (cases "(LEAST n. P n)")
+ case 0
+ then show ?thesis
+ using \<section> by (simp add: assms)
+ next
+ case Suc
+ with \<section> show ?thesis
+ by (auto simp: Least_le)
+ qed
+ qed
+qed (use assms in auto)
lemma Least_Suc2: "P n \<Longrightarrow> Q m \<Longrightarrow> \<not> P 0 \<Longrightarrow> \<forall>k. P (Suc k) = Q k \<Longrightarrow> Least P = Suc (Least Q)"
by (erule (1) Least_Suc [THEN ssubst]) simp
-lemma ex_least_nat_le: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
- for P :: "nat \<Rightarrow> bool"
- apply (cases n)
- apply blast
- apply (rule_tac x="LEAST k. P k" in exI)
- apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
- done
-
-lemma ex_least_nat_less: "\<not> P 0 \<Longrightarrow> P n \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (k + 1)"
- for P :: "nat \<Rightarrow> bool"
- apply (cases n)
- apply blast
- apply (frule (1) ex_least_nat_le)
- apply (erule exE)
- apply (case_tac k)
- apply simp
- apply (rename_tac k1)
- apply (rule_tac x=k1 in exI)
- apply (auto simp add: less_eq_Suc_le)
- done
+lemma ex_least_nat_le:
+ fixes P :: "nat \<Rightarrow> bool"
+ assumes "P n" "\<not> P 0"
+ shows "\<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
+proof (cases n)
+ case (Suc m)
+ with assms show ?thesis
+ by (blast intro: Least_le LeastI_ex dest: not_less_Least)
+qed (use assms in auto)
+
+lemma ex_least_nat_less:
+ fixes P :: "nat \<Rightarrow> bool"
+ assumes "P n" "\<not> P 0"
+ shows "\<exists>k<n. (\<forall>i\<le>k. \<not> P i) \<and> P (Suc k)"
+proof (cases n)
+ case (Suc m)
+ then obtain k where k: "k \<le> n" "\<forall>i<k. \<not> P i" "P k"
+ using ex_least_nat_le [OF assms] by blast
+ show ?thesis
+ by (cases k) (use assms k less_eq_Suc_le in auto)
+qed (use assms in auto)
+
lemma nat_less_induct:
fixes P :: "nat \<Rightarrow> bool"
@@ -1070,11 +1077,10 @@
assumes "P 0"
and "\<And>n. n > 0 \<Longrightarrow> \<not> P n \<Longrightarrow> \<exists>m. m < n \<and> \<not> P m"
shows "P n"
- apply (rule infinite_descent)
- using assms
- apply (case_tac "n > 0")
- apply auto
- done
+proof (rule infinite_descent)
+ show "\<And>n. \<not> P n \<Longrightarrow> \<exists>m<n. \<not> P m"
+ using assms by (case_tac "n > 0") auto
+qed
text \<open>
Infinite descent using a mapping to \<open>nat\<close>:
@@ -1178,14 +1184,11 @@
lemma not_add_less1 [iff]: "\<not> i + j < i"
for i j :: nat
- apply (rule notI)
- apply (drule add_lessD1)
- apply (erule less_irrefl [THEN notE])
- done
+ by simp
lemma not_add_less2 [iff]: "\<not> j + i < i"
for i j :: nat
- by (simp add: add.commute)
+ by simp
lemma add_leD1: "m + k \<le> n \<Longrightarrow> m \<le> n"
for k m n :: nat
@@ -1193,9 +1196,7 @@
lemma add_leD2: "m + k \<le> n \<Longrightarrow> k \<le> n"
for k m n :: nat
- apply (simp add: add.commute)
- apply (erule add_leD1)
- done
+ by (force simp add: add.commute dest: add_leD1)
lemma add_leE: "m + k \<le> n \<Longrightarrow> (m \<le> n \<Longrightarrow> k \<le> n \<Longrightarrow> R) \<Longrightarrow> R"
for k m n :: nat
@@ -1213,10 +1214,7 @@
by (induct m n rule: diff_induct) simp_all
lemma diff_less_Suc: "m - n < Suc m"
- apply (induct m n rule: diff_induct)
- apply (erule_tac [3] less_SucE)
- apply (simp_all add: less_Suc_eq)
- done
+ by (induct m n rule: diff_induct) (auto simp: less_Suc_eq)
lemma diff_le_self [simp]: "m - n \<le> m"
for m n :: nat
@@ -1345,12 +1343,26 @@
lemma mult_less_cancel2 [simp]: "m * k < n * k \<longleftrightarrow> 0 < k \<and> m < n"
for k m n :: nat
- apply (safe intro!: mult_less_mono1)
- apply (cases k)
- apply auto
- apply (simp add: linorder_not_le [symmetric])
- apply (blast intro: mult_le_mono1)
- done
+proof (intro iffI conjI)
+ assume m: "m * k < n * k"
+ then show "0 < k"
+ by (cases k) auto
+ show "m < n"
+ proof (cases k)
+ case 0
+ then show ?thesis
+ using m by auto
+ next
+ case (Suc k')
+ then show ?thesis
+ using m
+ by (simp flip: linorder_not_le) (blast intro: add_mono mult_le_mono1)
+ qed
+next
+ assume "0 < k \<and> m < n"
+ then show "m * k < n * k"
+ by (blast intro: mult_less_mono1)
+qed
lemma mult_less_cancel1 [simp]: "k * m < k * n \<longleftrightarrow> 0 < k \<and> m < n"
for k m n :: nat
@@ -1379,16 +1391,18 @@
by (cases m) (auto intro: le_add1)
text \<open>Lemma for \<open>gcd\<close>\<close>
-lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0"
- for m n :: nat
- apply (drule sym)
- apply (rule disjCI)
- apply (rule linorder_cases)
- defer
- apply assumption
- apply (drule mult_less_mono2)
- apply auto
- done
+lemma mult_eq_self_implies_10:
+ fixes m n :: nat
+ assumes "m = m * n" shows "n = 1 \<or> m = 0"
+proof (rule disjCI)
+ assume "m \<noteq> 0"
+ show "n = 1"
+ proof (cases n "1::nat" rule: linorder_cases)
+ case greater
+ show ?thesis
+ using assms mult_less_mono2 [OF greater, of m] \<open>m \<noteq> 0\<close> by auto
+ qed (use assms \<open>m \<noteq> 0\<close> in auto)
+qed
lemma mono_times_nat:
fixes n :: nat
@@ -1849,28 +1863,20 @@
by (simp add: Nats_def)
lemma Nats_0 [simp]: "0 \<in> \<nat>"
- apply (simp add: Nats_def)
- apply (rule range_eqI)
- apply (rule of_nat_0 [symmetric])
- done
+ using of_nat_0 [symmetric] unfolding Nats_def
+ by (rule range_eqI)
lemma Nats_1 [simp]: "1 \<in> \<nat>"
- apply (simp add: Nats_def)
- apply (rule range_eqI)
- apply (rule of_nat_1 [symmetric])
- done
+ using of_nat_1 [symmetric] unfolding Nats_def
+ by (rule range_eqI)
lemma Nats_add [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a + b \<in> \<nat>"
- apply (auto simp add: Nats_def)
- apply (rule range_eqI)
- apply (rule of_nat_add [symmetric])
- done
+ unfolding Nats_def using of_nat_add [symmetric]
+ by (blast intro: range_eqI)
lemma Nats_mult [simp]: "a \<in> \<nat> \<Longrightarrow> b \<in> \<nat> \<Longrightarrow> a * b \<in> \<nat>"
- apply (auto simp add: Nats_def)
- apply (rule range_eqI)
- apply (rule of_nat_mult [symmetric])
- done
+ unfolding Nats_def using of_nat_mult [symmetric]
+ by (blast intro: range_eqI)
lemma Nats_cases [cases set: Nats]:
assumes "x \<in> \<nat>"
@@ -2303,21 +2309,21 @@
qed
qed
-lemma GreatestI_nat:
- "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
-apply(drule (1) ex_has_greatest_nat)
-using GreatestI2_order by auto
-
-lemma Greatest_le_nat:
- "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> k \<le> (Greatest P)"
-apply(frule (1) ex_has_greatest_nat)
-using GreatestI2_order[where P=P and Q=\<open>\<lambda>x. k \<le> x\<close>] by auto
+lemma
+ fixes k::nat
+ assumes "P k" and minor: "\<And>y. P y \<Longrightarrow> y \<le> b"
+ shows GreatestI_nat: "P (Greatest P)"
+ and Greatest_le_nat: "k \<le> Greatest P"
+proof -
+ obtain x where "P x" "\<And>y. P y \<Longrightarrow> y \<le> x"
+ using assms ex_has_greatest_nat by blast
+ with \<open>P k\<close> show "P (Greatest P)" "k \<le> Greatest P"
+ using GreatestI2_order by blast+
+qed
lemma GreatestI_ex_nat:
- "\<lbrakk> \<exists>k::nat. P k; \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
-apply (erule exE)
-apply (erule (1) GreatestI_nat)
-done
+ "\<lbrakk> \<exists>k::nat. P k; \<And>y. P y \<Longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
+ by (blast intro: GreatestI_nat)
subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
@@ -2363,11 +2369,16 @@
for k m n :: nat
unfolding dvd_def by (blast intro: right_diff_distrib' [symmetric])
-lemma dvd_diffD: "k dvd m - n \<Longrightarrow> k dvd n \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd m"
- for k m n :: nat
- apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
- apply (blast intro: dvd_add)
- done
+lemma dvd_diffD:
+ fixes k m n :: nat
+ assumes "k dvd m - n" "k dvd n" "n \<le> m"
+ shows "k dvd m"
+proof -
+ have "k dvd n + (m - n)"
+ using assms by (blast intro: dvd_add)
+ with assms show ?thesis
+ by simp
+qed
lemma dvd_diffD1: "k dvd m - n \<Longrightarrow> k dvd m \<Longrightarrow> n \<le> m \<Longrightarrow> k dvd n"
for k m n :: nat
@@ -2384,13 +2395,19 @@
then show ?thesis ..
qed
-lemma dvd_mult_cancel1: "0 < m \<Longrightarrow> m * n dvd m \<longleftrightarrow> n = 1"
- for m n :: nat
- apply auto
- apply (subgoal_tac "m * n dvd m * 1")
- apply (drule dvd_mult_cancel)
- apply auto
- done
+lemma dvd_mult_cancel1:
+ fixes m n :: nat
+ assumes "0 < m"
+ shows "m * n dvd m \<longleftrightarrow> n = 1"
+proof
+ assume "m * n dvd m"
+ then have "m * n dvd m * 1"
+ by simp
+ then have "n dvd 1"
+ by (iprover intro: assms dvd_mult_cancel)
+ then show "n = 1"
+ by auto
+qed auto
lemma dvd_mult_cancel2: "0 < m \<Longrightarrow> n * m dvd m \<longleftrightarrow> n = 1"
for m n :: nat
@@ -2442,14 +2459,6 @@
for n :: nat
by (fact mult_1_right)
-lemma nat_add_left_cancel: "k + m = k + n \<longleftrightarrow> m = n"
- for k m n :: nat
- by (fact add_left_cancel)
-
-lemma nat_add_right_cancel: "m + k = n + k \<longleftrightarrow> m = n"
- for k m n :: nat
- by (fact add_right_cancel)
-
lemma diff_mult_distrib: "(m - n) * k = (m * k) - (n * k)"
for k m n :: nat
by (fact left_diff_distrib')
@@ -2458,13 +2467,10 @@
for k m n :: nat
by (fact right_diff_distrib')
-lemma le_add_diff: "k \<le> n \<Longrightarrow> m \<le> n + m - k"
- for k m n :: nat
- by (fact le_add_diff) (* FIXME delete *)
-
+(*Used in AUTO2 and Groups.le_diff_conv2 (with variables renamed) doesn't work for some reason*)
lemma le_diff_conv2: "k \<le> j \<Longrightarrow> (i \<le> j - k) = (i + k \<le> j)"
for i j k :: nat
- by (fact le_diff_conv2) (* FIXME delete *)
+ by (fact le_diff_conv2)
lemma diff_self_eq_0 [simp]: "m - m = 0"
for m :: nat
--- a/src/HOL/Transcendental.thy Sun Mar 22 22:03:48 2020 +0100
+++ b/src/HOL/Transcendental.thy Mon Mar 23 10:26:08 2020 +0000
@@ -618,10 +618,6 @@
for r :: "'a::ring_1"
by (simp add: sum_subtractf)
-lemma lemma_realpow_rev_sumr:
- "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) = (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
- by (subst sum.nat_diff_reindex[symmetric]) simp
-
lemma lemma_termdiff2:
fixes h :: "'a::field"
assumes h: "h \<noteq> 0"
@@ -629,26 +625,26 @@
h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
(is "?lhs = ?rhs")
proof (cases n)
- case (Suc n)
+ case (Suc m)
have 0: "\<And>x k. (\<Sum>n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) =
(\<Sum>j<Suc k. h * ((h + z) ^ j * z ^ (x + k - j)))"
- apply (rule sum.cong [OF refl])
- by (simp add: power_add [symmetric] mult.commute)
- have *: "(\<Sum>i<n. z ^ i * ((z + h) ^ (n - i) - z ^ (n - i))) =
- (\<Sum>i<n. \<Sum>j<n - i. h * ((z + h) ^ j * z ^ (n - Suc j)))"
- apply (rule sum.cong [OF refl])
- apply (clarsimp simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
- simp del: sum.lessThan_Suc power_Suc)
- done
- have "h * ?lhs = h * ?rhs"
- apply (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
- using Suc
- apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
+ by (auto simp add: power_add [symmetric] mult.commute intro: sum.cong)
+ have *: "(\<Sum>i<m. z ^ i * ((z + h) ^ (m - i) - z ^ (m - i))) =
+ (\<Sum>i<m. \<Sum>j<m - i. h * ((z + h) ^ j * z ^ (m - Suc j)))"
+ by (force simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
+ simp del: sum.lessThan_Suc power_Suc intro: sum.cong)
+ have "h * ?lhs = (z + h) ^ n - z ^ n - h * of_nat n * z ^ (n - Suc 0)"
+ by (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
+ also have "... = h * ((\<Sum>p<Suc m. (z + h) ^ p * z ^ (m - p)) - of_nat (Suc m) * z ^ m)"
+ by (simp add: Suc diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
del: power_Suc sum.lessThan_Suc of_nat_Suc)
- apply (subst lemma_realpow_rev_sumr)
- apply (subst sumr_diff_mult_const2)
- apply (simp add: lemma_termdiff1 sum_distrib_left *)
- done
+ also have "... = h * ((\<Sum>p<Suc m. (z + h) ^ (m - p) * z ^ p) - of_nat (Suc m) * z ^ m)"
+ by (subst sum.nat_diff_reindex[symmetric]) simp
+ also have "... = h * (\<Sum>i<Suc m. (z + h) ^ (m - i) * z ^ i - z ^ m)"
+ by (simp add: sum_subtractf)
+ also have "... = h * ?rhs"
+ by (simp add: lemma_termdiff1 sum_distrib_left Suc *)
+ finally have "h * ?lhs = h * ?rhs" .
then show ?thesis
by (simp add: h)
qed auto
@@ -656,12 +652,15 @@
lemma real_sum_nat_ivl_bounded2:
fixes K :: "'a::linordered_semidom"
- assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
- and K: "0 \<le> K"
+ assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K" and K: "0 \<le> K"
shows "sum f {..<n-k} \<le> of_nat n * K"
- apply (rule order_trans [OF sum_mono [OF f]])
- apply (auto simp: mult_right_mono K)
- done
+proof -
+ have "sum f {..<n-k} \<le> (\<Sum>i<n - k. K)"
+ by (rule sum_mono [OF f]) auto
+ also have "... \<le> of_nat n * K"
+ by (auto simp: mult_right_mono K)
+ finally show ?thesis .
+qed
lemma lemma_termdiff3:
fixes h z :: "'a::real_normed_field"
@@ -678,21 +677,23 @@
proof (rule mult_right_mono [OF _ norm_ge_zero])
from norm_ge_zero 2 have K: "0 \<le> K"
by (rule order_trans)
- have le_Kn: "\<And>i j n. i + j = n \<Longrightarrow> norm ((z + h) ^ i * z ^ j) \<le> K ^ n"
- apply (erule subst)
- apply (simp only: norm_mult norm_power power_add)
- apply (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
- done
+ have le_Kn: "norm ((z + h) ^ i * z ^ j) \<le> K ^ n" if "i + j = n" for i j n
+ proof -
+ have "norm (z + h) ^ i * norm z ^ j \<le> K ^ i * K ^ j"
+ by (intro mult_mono power_mono 2 3 norm_ge_zero zero_le_power K)
+ also have "... = K^n"
+ by (metis power_add that)
+ finally show ?thesis
+ by (simp add: norm_mult norm_power)
+ qed
+ then have "\<And>p q.
+ \<lbrakk>p < n; q < n - Suc 0\<rbrakk> \<Longrightarrow> norm ((z + h) ^ q * z ^ (n - 2 - q)) \<le> K ^ (n - 2)"
+ by simp
+ then
show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) \<le>
of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"
- apply (intro
- order_trans [OF norm_sum]
- real_sum_nat_ivl_bounded2
- mult_nonneg_nonneg
- of_nat_0_le_iff
- zero_le_power K)
- apply (rule le_Kn, simp)
- done
+ by (intro order_trans [OF norm_sum]
+ real_sum_nat_ivl_bounded2 mult_nonneg_nonneg of_nat_0_le_iff zero_le_power K)
qed
also have "\<dots> = of_nat n * of_nat (n - Suc 0) * K ^ (n - 2) * norm h"
by (simp only: mult.assoc)
@@ -775,39 +776,30 @@
then have "summable (\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0))"
by (rule diffs_equiv [THEN sums_summable])
also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
- (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
- apply (rule ext)
- apply (case_tac n)
- apply (simp_all add: diffs_def r_neq_0)
- done
+ (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
+ by (simp add: diffs_def r_neq_0 fun_eq_iff split: nat_diff_split)
finally have "summable
(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
by (rule diffs_equiv [THEN sums_summable])
also have
"(\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) =
(\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))"
- apply (rule ext)
- apply (case_tac n, simp)
- apply (rename_tac nat)
- apply (case_tac nat, simp)
- apply (simp add: r_neq_0)
- done
+ by (rule ext) (simp add: r_neq_0 split: nat_diff_split)
finally show "summable (\<lambda>n. norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2))" .
next
- fix h :: 'a
- fix n :: nat
+ fix h :: 'a and n
assume h: "h \<noteq> 0"
assume "norm h < r - norm x"
then have "norm x + norm h < r" by simp
- with norm_triangle_ineq have xh: "norm (x + h) < r"
+ with norm_triangle_ineq
+ have xh: "norm (x + h) < r"
by (rule order_le_less_trans)
- show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<le>
+ have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0))
+ \<le> real n * (real (n - Suc 0) * (r ^ (n - 2) * norm h))"
+ by (metis (mono_tags, lifting) h mult.assoc lemma_termdiff3 less_eq_real_def r1 xh)
+ then show "norm (c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<le>
norm (c n) * of_nat n * of_nat (n - Suc 0) * r ^ (n - 2) * norm h"
- apply (simp only: norm_mult mult.assoc)
- apply (rule mult_left_mono [OF _ norm_ge_zero])
- apply (simp add: mult.assoc [symmetric])
- apply (metis h lemma_termdiff3 less_eq_real_def r1 xh)
- done
+ by (simp only: norm_mult mult.assoc mult_left_mono [OF _ norm_ge_zero])
qed
qed
@@ -900,12 +892,10 @@
and K: "norm x < norm K"
shows "DERIV (\<lambda>x. \<Sum>n. c n * x^n) x :> (\<Sum>n. diffs c n * x^n)"
proof -
- have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
- using K
- apply (auto simp: norm_divide field_simps)
- apply (rule le_less_trans [of _ "of_real (norm K) + of_real (norm x)"])
- apply (auto simp: mult_2_right norm_triangle_mono)
- done
+ have "norm K + norm x < norm K + norm K"
+ using K by force
+ then have K2: "norm ((of_real (norm K) + of_real (norm x)) / 2 :: 'a) < norm K"
+ by (auto simp: norm_triangle_lt norm_divide field_simps)
then have [simp]: "norm ((of_real (norm K) + of_real (norm x)) :: 'a) < norm K * 2"
by simp
have "summable (\<lambda>n. c n * (of_real (norm x + norm K) / 2) ^ n)"
@@ -915,11 +905,8 @@
moreover have "\<And>x. norm x < norm K \<Longrightarrow> summable (\<lambda>n. diffs(diffs c) n * x ^ n)"
by (blast intro: sm termdiff_converges powser_inside)
ultimately show ?thesis
- apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
- using K
- apply (auto simp: field_simps)
- apply (simp flip: of_real_add)
- done
+ by (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
+ (use K in \<open>auto simp: field_simps simp flip: of_real_add\<close>)
qed
lemma termdiffs_strong_converges_everywhere:
@@ -999,11 +986,12 @@
by (blast intro: DERIV_continuous)
then have "((\<lambda>x. \<Sum>n. a n * x ^ n) \<longlongrightarrow> a 0) (at 0)"
by (simp add: continuous_within)
- then show ?thesis
- apply (rule Lim_transform)
+ moreover have "(\<lambda>x. f x - (\<Sum>n. a n * x ^ n)) \<midarrow>0\<rightarrow> 0"
apply (clarsimp simp: LIM_eq)
apply (rule_tac x=s in exI)
using s sm sums_unique by fastforce
+ ultimately show ?thesis
+ by (rule Lim_transform)
qed
lemma powser_limit_0_strong:
@@ -1015,9 +1003,7 @@
have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
show ?thesis
- apply (subst LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
- apply (simp_all add: *)
- done
+ by (simp add: * LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
qed
@@ -1591,10 +1577,10 @@
have "1 + x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
by (auto simp: numeral_2_eq_2)
also have "\<dots> \<le> (\<Sum>n. inverse (fact n) * x^n)"
- apply (rule sum_le_suminf [OF summable_exp])
- using \<open>0 < x\<close>
- apply (auto simp add: zero_le_mult_iff)
- done
+ proof (rule sum_le_suminf [OF summable_exp])
+ show "\<forall>m\<in>- {..<2}. 0 \<le> inverse (fact m) * x ^ m"
+ using \<open>0 < x\<close> by (auto simp add: zero_le_mult_iff)
+ qed auto
finally show "1 + x \<le> exp x"
by (simp add: exp_def)
qed auto
@@ -2049,9 +2035,7 @@
proof (cases "0 \<le> x \<or> x \<le> -1")
case True
then show ?thesis
- apply (rule disjE)
- apply (simp add: exp_ge_add_one_self_aux)
- using exp_ge_zero order_trans real_add_le_0_iff by blast
+ by (meson exp_ge_add_one_self_aux exp_ge_zero order.trans real_add_le_0_iff)
next
case False
then have ln1: "ln (1 + x) \<le> x"
@@ -2463,11 +2447,12 @@
lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
using powr_ge_pzero[of a x] by arith
+lemma inverse_powr: "\<And>y::real. 0 \<le> y \<Longrightarrow> inverse y powr a = inverse (y powr a)"
+ by (simp add: exp_minus ln_inverse powr_def)
+
lemma powr_divide: "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
for a b x :: real
- apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
- apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
- done
+ by (simp add: divide_inverse powr_mult inverse_powr)
lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
for a b x :: "'a::{ln,real_normed_field}"
@@ -3198,17 +3183,20 @@
lemma summable_norm_sin: "summable (\<lambda>n. norm (sin_coeff n *\<^sub>R x^n))"
for x :: "'a::{real_normed_algebra_1,banach}"
- unfolding sin_coeff_def
- apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
- apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
- done
+proof (rule summable_comparison_test [OF _ summable_norm_exp])
+ show "\<exists>N. \<forall>n\<ge>N. norm (norm (sin_coeff n *\<^sub>R x ^ n)) \<le> norm (x ^ n /\<^sub>R fact n)"
+ unfolding sin_coeff_def
+ by (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
+qed
lemma summable_norm_cos: "summable (\<lambda>n. norm (cos_coeff n *\<^sub>R x^n))"
for x :: "'a::{real_normed_algebra_1,banach}"
- unfolding cos_coeff_def
- apply (rule summable_comparison_test [OF _ summable_norm_exp [where x=x]])
- apply (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
- done
+proof (rule summable_comparison_test [OF _ summable_norm_exp])
+ show "\<exists>N. \<forall>n\<ge>N. norm (norm (cos_coeff n *\<^sub>R x ^ n)) \<le> norm (x ^ n /\<^sub>R fact n)"
+ unfolding cos_coeff_def
+ by (auto simp: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff)
+qed
+
lemma sin_converges: "(\<lambda>n. sin_coeff n *\<^sub>R x^n) sums sin x"
unfolding sin_def
@@ -3230,8 +3218,7 @@
by (rule sin_converges)
finally have "(\<lambda>n. of_real (sin_coeff n *\<^sub>R x^n)) sums (sin (of_real x))" .
then show ?thesis
- using sums_unique2 sums_of_real [OF sin_converges]
- by blast
+ using sums_unique2 sums_of_real [OF sin_converges] by blast
qed
corollary sin_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> sin z \<in> \<real>"
@@ -3317,44 +3304,41 @@
lemma continuous_on_cos_real: "continuous_on {a..b} cos" for a::real
using continuous_at_imp_continuous_on isCont_cos by blast
+
+context
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::{real_normed_field,banach}"
+begin
+
lemma isCont_sin' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. sin (f x)) a"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
by (rule isCont_o2 [OF _ isCont_sin])
-(* FIXME a context for f would be better *)
-
lemma isCont_cos' [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. cos (f x)) a"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
by (rule isCont_o2 [OF _ isCont_cos])
lemma tendsto_sin [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. sin (f x)) \<longlongrightarrow> sin a) F"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
by (rule isCont_tendsto_compose [OF isCont_sin])
lemma tendsto_cos [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. cos (f x)) \<longlongrightarrow> cos a) F"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
by (rule isCont_tendsto_compose [OF isCont_cos])
lemma continuous_sin [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sin (f x))"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
unfolding continuous_def by (rule tendsto_sin)
lemma continuous_on_sin [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. sin (f x))"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
unfolding continuous_on_def by (auto intro: tendsto_sin)
+lemma continuous_cos [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
+ unfolding continuous_def by (rule tendsto_cos)
+
+lemma continuous_on_cos [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
+ unfolding continuous_on_def by (auto intro: tendsto_cos)
+
+end
+
lemma continuous_within_sin: "continuous (at z within s) sin"
for z :: "'a::{real_normed_field,banach}"
by (simp add: continuous_within tendsto_sin)
-lemma continuous_cos [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. cos (f x))"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
- unfolding continuous_def by (rule tendsto_cos)
-
-lemma continuous_on_cos [continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. cos (f x))"
- for f :: "_ \<Rightarrow> 'a::{real_normed_field,banach}"
- unfolding continuous_on_def by (auto intro: tendsto_cos)
-
lemma continuous_within_cos: "continuous (at z within s) cos"
for z :: "'a::{real_normed_field,banach}"
by (simp add: continuous_within tendsto_cos)
@@ -3369,10 +3353,10 @@
by (simp add: cos_def cos_coeff_def scaleR_conv_of_real)
lemma DERIV_fun_sin: "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. sin (g x)) x :> cos (g x) * m"
- by (auto intro!: derivative_intros)
+ by (fact derivative_intros)
lemma DERIV_fun_cos: "DERIV g x :> m \<Longrightarrow> DERIV (\<lambda>x. cos(g x)) x :> - sin (g x) * m"
- by (auto intro!: derivative_eq_intros)
+ by (fact derivative_intros)
subsection \<open>Deriving the Addition Formulas\<close>
@@ -3428,15 +3412,16 @@
have "(-1) ^ ((n - Suc 0) div 2) * (-1) ^ ((p - Suc n) div 2) = - ((-1 :: real) ^ (p div 2))"
if np: "odd n" "even p"
proof -
+ have "p > 0"
+ using \<open>n \<le> p\<close> neq0_conv that(1) by blast
+ then have \<section>: "(- 1::real) ^ (p div 2 - Suc 0) = - ((- 1) ^ (p div 2))"
+ using \<open>even p\<close> by (auto simp add: dvd_def power_eq_if)
from \<open>n \<le> p\<close> np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \<le> p"
by arith+
have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0"
by simp
- with \<open>n \<le> p\<close> np * show ?thesis
- apply (simp add: power_add [symmetric] div_add [symmetric] del: div_add)
- apply (metis (no_types) One_nat_def Suc_1 le_div_geq minus_minus
- mult.left_neutral mult_minus_left power.simps(2) zero_less_Suc)
- done
+ with \<open>n \<le> p\<close> np \<section> * show ?thesis
+ by (simp add: flip: div_add power_add)
qed
then show ?thesis
using \<open>n\<le>p\<close> by (auto simp: algebra_simps sin_coeff_def binomial_fact)
@@ -3884,22 +3869,31 @@
lemma sin_two_pi [simp]: "sin (2 * pi) = 0"
by (simp add: sin_double)
+context
+ fixes w :: "'a::{real_normed_field,banach}"
+
+begin
+
lemma sin_times_sin: "sin w * sin z = (cos (w - z) - cos (w + z)) / 2"
- for w :: "'a::{real_normed_field,banach}"
by (simp add: cos_diff cos_add)
lemma sin_times_cos: "sin w * cos z = (sin (w + z) + sin (w - z)) / 2"
- for w :: "'a::{real_normed_field,banach}"
by (simp add: sin_diff sin_add)
lemma cos_times_sin: "cos w * sin z = (sin (w + z) - sin (w - z)) / 2"
- for w :: "'a::{real_normed_field,banach}"
by (simp add: sin_diff sin_add)
lemma cos_times_cos: "cos w * cos z = (cos (w - z) + cos (w + z)) / 2"
- for w :: "'a::{real_normed_field,banach}"
by (simp add: cos_diff cos_add)
+lemma cos_double_cos: "cos (2 * w) = 2 * cos w ^ 2 - 1"
+ by (simp add: cos_double sin_squared_eq)
+
+lemma cos_double_sin: "cos (2 * w) = 1 - 2 * sin w ^ 2"
+ by (simp add: cos_double sin_squared_eq)
+
+end
+
lemma sin_plus_sin: "sin w + sin z = 2 * sin ((w + z) / 2) * cos ((w - z) / 2)"
for w :: "'a::{real_normed_field,banach}"
apply (simp add: mult.assoc sin_times_cos)
@@ -3924,14 +3918,6 @@
apply (simp add: field_simps)
done
-lemma cos_double_cos: "cos (2 * z) = 2 * cos z ^ 2 - 1"
- for z :: "'a::{real_normed_field,banach}"
- by (simp add: cos_double sin_squared_eq)
-
-lemma cos_double_sin: "cos (2 * z) = 1 - 2 * sin z ^ 2"
- for z :: "'a::{real_normed_field,banach}"
- by (simp add: cos_double sin_squared_eq)
-
lemma sin_pi_minus [simp]: "sin (pi - x) = sin x"
by (metis sin_minus sin_periodic_pi minus_minus uminus_add_conv_diff)
@@ -4074,7 +4060,7 @@
lemma cos_zero_lemma:
assumes "0 \<le> x" "cos x = 0"
- shows "\<exists>n. odd n \<and> x = of_nat n * (pi/2) \<and> n > 0"
+ shows "\<exists>n. odd n \<and> x = of_nat n * (pi/2)"
proof -
have xle: "x < (1 + real_of_int \<lfloor>x/pi\<rfloor>) * pi"
using floor_correct [of "x/pi"]
@@ -4101,12 +4087,17 @@
by (rule_tac x = "Suc (2 * n)" in exI) (simp add: algebra_simps)
qed
-lemma sin_zero_lemma: "0 \<le> x \<Longrightarrow> sin x = 0 \<Longrightarrow> \<exists>n::nat. even n \<and> x = real n * (pi/2)"
- using cos_zero_lemma [of "x + pi/2"]
- apply (clarsimp simp add: cos_add)
- apply (rule_tac x = "n - 1" in exI)
- apply (simp add: algebra_simps of_nat_diff)
- done
+lemma sin_zero_lemma:
+ assumes "0 \<le> x" "sin x = 0"
+ shows "\<exists>n::nat. even n \<and> x = real n * (pi/2)"
+proof -
+ obtain n where "odd n" and n: "x + pi/2 = of_nat n * (pi/2)" "n > 0"
+ using cos_zero_lemma [of "x + pi/2"] assms by (auto simp add: cos_add)
+ then have "x = real (n - 1) * (pi / 2)"
+ by (simp add: algebra_simps of_nat_diff)
+ then show ?thesis
+ by (simp add: \<open>odd n\<close>)
+qed
lemma cos_zero_iff:
"cos x = 0 \<longleftrightarrow> ((\<exists>n. odd n \<and> x = real n * (pi/2)) \<or> (\<exists>n. odd n \<and> x = - (real n * (pi/2))))"
@@ -4146,7 +4137,7 @@
using that assms by (auto simp: sin_zero_iff)
qed auto
-lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
+lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>i. odd i \<and> x = of_int i * (pi/2))"
proof -
have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"
by (metis even_of_nat of_int_of_nat_eq)
@@ -4159,15 +4150,21 @@
by (force simp: cos_zero_iff intro!: 1 2 3)
qed
-lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>n. even n \<and> x = of_int n * (pi/2))"
+lemma sin_zero_iff_int: "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = of_int i * (pi/2))" (is "?lhs = ?rhs")
proof safe
- assume "sin x = 0"
+ assume ?lhs
+ then consider (plus) n where "even n" "x = real n * (pi/2)" | (minus) n where "even n" "x = - (real n * (pi/2))"
+ using sin_zero_iff by auto
then show "\<exists>n. even n \<and> x = of_int n * (pi/2)"
- apply (simp add: sin_zero_iff, safe)
- apply (metis even_of_nat of_int_of_nat_eq)
- apply (rule_tac x="- (int n)" in exI)
- apply simp
- done
+ proof cases
+ case plus
+ then show ?rhs
+ by (metis even_of_nat of_int_of_nat_eq)
+ next
+ case minus
+ then show ?thesis
+ by (rule_tac x="- (int n)" in exI) simp
+ qed
next
fix i :: int
assume "even i"
@@ -4175,12 +4172,16 @@
by (cases i rule: int_cases2, simp_all add: sin_zero_iff)
qed
-lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = of_int n * pi)"
- apply (simp only: sin_zero_iff_int)
- apply (safe elim!: evenE)
- apply (simp_all add: field_simps)
- using dvd_triv_left apply fastforce
- done
+lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>i::int. x = of_int i * pi)"
+proof -
+ have "sin x = 0 \<longleftrightarrow> (\<exists>i. even i \<and> x = real_of_int i * (pi / 2))"
+ by (auto simp: sin_zero_iff_int)
+ also have "... = (\<exists>j. x = real_of_int (2*j) * (pi / 2))"
+ using dvd_triv_left by blast
+ also have "... = (\<exists>i::int. x = of_int i * pi)"
+ by auto
+ finally show ?thesis .
+qed
lemma sin_npi_int [simp]: "sin (pi * of_int n) = 0"
by (simp add: sin_zero_iff_int2)
@@ -4252,15 +4253,14 @@
lemma sin_x_le_x:
fixes x :: real
- assumes x: "x \<ge> 0"
+ assumes "x \<ge> 0"
shows "sin x \<le> x"
proof -
let ?f = "\<lambda>x. x - sin x"
- from x have "?f x \<ge> ?f 0"
- apply (rule DERIV_nonneg_imp_nondecreasing)
- apply (intro allI impI exI[of _ "1 - cos x" for x])
- apply (auto intro!: derivative_eq_intros simp: field_simps)
- done
+ have "\<And>u. \<lbrakk>0 \<le> u; u \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. (?f has_real_derivative 1 - cos u) (at u)"
+ by (auto intro!: derivative_eq_intros simp: field_simps)
+ then have "?f x \<ge> ?f 0"
+ by (metis cos_le_one diff_ge_0_iff_ge DERIV_nonneg_imp_nondecreasing [OF assms])
then show "sin x \<le> x" by simp
qed
@@ -4270,11 +4270,10 @@
shows "sin x \<ge> - x"
proof -
let ?f = "\<lambda>x. x + sin x"
- from x have "?f x \<ge> ?f 0"
- apply (rule DERIV_nonneg_imp_nondecreasing)
- apply (intro allI impI exI[of _ "1 + cos x" for x])
- apply (auto intro!: derivative_eq_intros simp: field_simps real_0_le_add_iff)
- done
+ have \<section>: "\<And>u. \<lbrakk>0 \<le> u; u \<le> x\<rbrakk> \<Longrightarrow> \<exists>y. (?f has_real_derivative 1 + cos u) (at u)"
+ by (auto intro!: derivative_eq_intros simp: field_simps)
+ have "?f x \<ge> ?f 0"
+ by (rule DERIV_nonneg_imp_nondecreasing [OF assms]) (use \<section> real_0_le_add_iff in force)
then show "sin x \<ge> -x" by simp
qed
@@ -4409,9 +4408,8 @@
have "cos(3 * x) = cos(2*x + x)"
by simp
also have "\<dots> = 4 * cos x ^ 3 - 3 * cos x"
- apply (simp only: cos_add cos_double sin_double)
- apply (simp add: * field_simps power2_eq_square power3_eq_cube)
- done
+ unfolding cos_add cos_double sin_double
+ by (simp add: * field_simps power2_eq_square power3_eq_cube)
finally show ?thesis .
qed
@@ -4482,12 +4480,18 @@
by (metis Ints_of_int sin_integer_2pi)
lemma sincos_principal_value: "\<exists>y. (- pi < y \<and> y \<le> pi) \<and> (sin y = sin x \<and> cos y = cos x)"
- apply (rule exI [where x="pi - (2 * pi) * frac ((pi - x) / (2 * pi))"])
- apply (auto simp: field_simps frac_lt_1)
- apply (simp_all add: frac_def field_simps)
- apply (simp_all add: add_divide_distrib diff_divide_distrib)
- apply (simp_all add: sin_add cos_add mult.assoc [symmetric])
- done
+proof -
+ define y where "y \<equiv> pi - (2 * pi) * frac ((pi - x) / (2 * pi))"
+ have "-pi < y"" y \<le> pi"
+ by (auto simp: field_simps frac_lt_1 y_def)
+ moreover
+ have "sin y = sin x" "cos y = cos x"
+ unfolding y_def
+ apply (simp_all add: frac_def divide_simps sin_add cos_add)
+ by (metis sin_int_2pin cos_int_2pin diff_zero add.right_neutral mult.commute mult.left_neutral mult_zero_left)+
+ ultimately
+ show ?thesis by metis
+qed
subsection \<open>Tangent\<close>
@@ -5238,10 +5242,11 @@
qed (use assms isCont_arccos in auto)
lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
-proof (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
- show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
- apply (rule derivative_eq_intros | simp)+
+proof (rule DERIV_inverse_function)
+ have "inverse ((cos (arctan x))\<^sup>2) = 1 + x\<^sup>2"
by (metis arctan cos_arctan_not_zero power_inverse tan_sec)
+ then show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
+ by (auto intro!: derivative_eq_intros)
show "\<And>y. \<lbrakk>x - 1 < y; y < x + 1\<rbrakk> \<Longrightarrow> tan (arctan y) = y"
using tan_arctan by blast
show "1 + x\<^sup>2 \<noteq> 0"
@@ -5999,19 +6004,15 @@
assumes "x \<noteq> 0"
shows "arctan (1 / x) = sgn x * pi/2 - arctan x"
proof (rule arctan_unique)
+ have \<section>: "x > 0 \<Longrightarrow> arctan x < pi"
+ using arctan_bounded [of x] by linarith
show "- (pi/2) < sgn x * pi/2 - arctan x"
- using arctan_bounded [of x] assms
- unfolding sgn_real_def
- apply (auto simp: arctan algebra_simps)
- apply (drule zero_less_arctan_iff [THEN iffD2], arith)
- done
+ using assms by (auto simp: sgn_real_def arctan algebra_simps \<section>)
show "sgn x * pi/2 - arctan x < pi/2"
using arctan_bounded [of "- x"] assms
- unfolding sgn_real_def arctan_minus
- by (auto simp: algebra_simps)
+ by (auto simp: algebra_simps sgn_real_def arctan_minus)
show "tan (sgn x * pi/2 - arctan x) = 1 / x"
- unfolding tan_inverse [of "arctan x", unfolded tan_arctan]
- unfolding sgn_real_def
+ unfolding tan_inverse [of "arctan x", unfolded tan_arctan] sgn_real_def
by (simp add: tan_def cos_arctan sin_arctan sin_diff cos_diff)
qed
@@ -6032,18 +6033,18 @@
by (rule power2_le_imp_le [OF _ zero_le_one])
(simp add: power_divide divide_le_eq not_sum_power2_lt_zero)
-lemmas cos_arccos_lemma1 = cos_arccos_abs [OF cos_x_y_le_one]
-
-lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
-
lemma polar_Ex: "\<exists>r::real. \<exists>a. x = r * cos a \<and> y = r * sin a"
proof -
- have polar_ex1: "0 < y \<Longrightarrow> \<exists>r a. x = r * cos a \<and> y = r * sin a" for y
- apply (rule exI [where x = "sqrt (x\<^sup>2 + y\<^sup>2)"])
- apply (rule exI [where x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))"])
- apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
- real_sqrt_mult [symmetric] right_diff_distrib)
- done
+ have polar_ex1: "\<exists>r a. x = r * cos a \<and> y = r * sin a" if "0 < y" for y
+ proof -
+ have "x = sqrt (x\<^sup>2 + y\<^sup>2) * cos (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))"
+ by (simp add: cos_arccos_abs [OF cos_x_y_le_one])
+ moreover have "y = sqrt (x\<^sup>2 + y\<^sup>2) * sin (arccos (x / sqrt (x\<^sup>2 + y\<^sup>2)))"
+ using that
+ by (simp add: sin_arccos_abs [OF cos_x_y_le_one] power_divide right_diff_distrib flip: real_sqrt_mult)
+ ultimately show ?thesis
+ by blast
+ qed
show ?thesis
proof (cases "0::real" y rule: linorder_cases)
case less
@@ -6083,24 +6084,24 @@
assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
- (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-proof -
+ (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+proof -
+ have "\<And>i j. \<lbrakk>m + n - i < j; a i \<noteq> 0\<rbrakk> \<Longrightarrow> b j = 0"
+ by (meson le_add_diff leI le_less_trans m n)
+ then have \<section>: "(\<Sum>(i,j)\<in>(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0"
+ by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
have "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = (\<Sum>i\<le>m. \<Sum>j\<le>n. (a i * x ^ i) * (b j * x ^ j))"
by (rule sum_product)
also have "\<dots> = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
using assms by (auto simp: sum_up_index_split)
also have "\<dots> = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
- apply (simp add: add_ac sum.Sigma product_atMost_eq_Un)
- apply (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
- apply (metis add_diff_assoc2 add.commute add_lessD1 leD m n nat_le_linear neqE)
- done
+ by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint \<section>)
also have "\<dots> = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
by (auto simp: pairs_le_eq_Sigma sum.Sigma)
+ also have "... = (\<Sum>k\<le>m + n. \<Sum>i\<le>k. a i * x ^ i * (b (k - i) * x ^ (k - i)))"
+ by (rule sum.triangle_reindex_eq)
also have "\<dots> = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
- apply (subst sum.triangle_reindex_eq)
- apply (auto simp: algebra_simps sum_distrib_left intro!: sum.cong)
- apply (metis le_add_diff_inverse power_add)
- done
+ by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong)
finally show ?thesis .
qed
@@ -6109,7 +6110,7 @@
assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
- (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+ (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
using polynomial_product [of m a n b x] assms
by (simp only: of_nat_mult [symmetric] of_nat_power [symmetric]
of_nat_eq_iff Int.int_sum [symmetric])
@@ -6148,10 +6149,10 @@
have "(\<Sum>i=Suc j..n. a i * y^(i - j - 1)) = (\<Sum>k<n-j. a(j+k+1) * y^k)"
if "j < n" for j :: nat
proof -
- have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
- apply (auto simp: bij_betw_def inj_on_def)
- apply (rule_tac x="x + Suc j" in image_eqI, auto)
- done
+ have "\<And>k. k < n - j \<Longrightarrow> k \<in> (\<lambda>i. i - Suc j) ` {Suc j..n}"
+ by (rule_tac x="k + Suc j" in image_eqI, auto)
+ then have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
+ by (auto simp: bij_betw_def inj_on_def)
then show ?thesis
by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
qed