# HG changeset patch # User paulson # Date 1584897676 0 # Node ID 4b1021677f151da54a21c2a0375004f40a948908 # Parent 24b68a932f26f71188dbc6b524f6118b923ad92a tidying up some horrible proofs diff -r 24b68a932f26 -r 4b1021677f15 src/HOL/List.thy --- 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 \ length xs) = (\x ys. xs = x # ys \ n \ length ys)" by (metis Suc_le_D[of n] Suc_le_mono[of n] Suc_length_conv[of _ xs]) -lemma impossible_Cons: "length xs \ length ys ==> xs = x # ys = False" +lemma impossible_Cons: "length xs \ length ys \ 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 \ length us = length vs - ==> (xs@us = ys@vs) = (xs=ys \ us=vs)" + \ (xs@us = ys@vs) = (xs=ys \ 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 \ [] ==> hd xs # tl xs = xs" +lemma hd_Cons_tl: "xs \ [] \ 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 \ [] ==> hd (xs @ ys) = hd xs" +lemma hd_append2 [simp]: "xs \ [] \ hd (xs @ ys) = hd xs" by (simp add: hd_append split: list.split) lemma tl_append: "tl (xs @ ys) = (case xs of [] \ tl ys | z#zs \ zs @ ys)" by (simp split: list.split) -lemma tl_append2 [simp]: "xs \ [] ==> tl (xs @ ys) = tl xs @ ys" +lemma tl_append2 [simp]: "xs \ [] \ tl (xs @ ys) = tl xs @ ys" by (simp add: tl_append split: list.split) @@ -1031,16 +1031,14 @@ text \Trivial rules for solving \@\-equations automatically.\ -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 \ xs = [] @ ys" + by simp + +lemma Cons_eq_appendI: "\x # xs1 = ys; xs = xs1 @ zs\ \ x # xs = ys @ zs" + by auto + +lemma append_eq_appendI: "\xs @ xs1 = zs; ys = xs1 @ us\ \ xs @ ys = zs @ us" + by auto text \ @@ -1100,7 +1098,7 @@ lemma map_tl: "map f (tl xs) = tl (map f xs)" by (cases xs) simp_all -lemma map_ext: "(\x. x \ set xs \ f x = g x) ==> map f xs = map g xs" +lemma map_ext: "(\x. x \ set xs \ f x = g x) \ map f xs = map g xs" by (induct xs) simp_all lemma map_ident [simp]: "map (\x. x) = (\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 \ inj f \ xs = ys" by (induct ys arbitrary: xs) (auto dest!:injD) lemma inj_map_eq_map[simp]: "inj f \ (map f xs = map f ys) = (xs = ys)" by(blast dest:map_injective) -lemma inj_mapI: "inj f ==> inj (map f)" +lemma inj_mapI: "inj f \ 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) \ 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 "\x xs. P xs \ 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 = [] \ P) \(\ys y. xs = ys @ [y] \ P) \ P" by (induct xs rule: rev_induct) auto lemmas rev_cases = rev_exhaust @@ -1475,10 +1476,10 @@ "length(filter P xs) + length(filter (\x. \P x) xs) = length xs" by(induct xs) simp_all -lemma filter_True [simp]: "\x \ set xs. P x ==> filter P xs = xs" +lemma filter_True [simp]: "\x \ set xs. P x \ filter P xs = xs" by (induct xs) auto -lemma filter_False [simp]: "\x \ set xs. \ P x ==> filter P xs = []" +lemma filter_False [simp]: "\x \ set xs. \ P x \ filter P xs = []" by (induct xs) auto lemma filter_empty_conv: "(filter P xs = []) = (\x\set xs. \ 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: "\(x, y) \ set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)" +lemma concat_eq_concat_iff: "\(x, y) \ set (zip xs ys). length x = length y \ length xs = length ys \ (concat xs = concat ys) = (xs = ys)" proof (induct xs arbitrary: ys) case (Cons x xs ys) thus ?case by (cases ys) auto qed (auto) -lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \(x, y) \ set (zip xs ys). length x = length y ==> xs = ys" +lemma concat_injective: "concat xs = concat ys \ length xs = length ys \ \(x, y) \ set (zip xs ys). length x = length y \ xs = ys" by (simp add: concat_eq_concat_iff) 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 \ (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\ (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 \ (xs[i:=x])!i = x" by (simp add: nth_list_update) -lemma nth_list_update_neq [simp]: "i \ j ==> xs[i:=x]!j = xs!j" +lemma nth_list_update_neq [simp]: "i \ j \ xs[i:=x]!j = xs!j" by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split) 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 \ (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 \ n ==> take n xs = xs" +lemma take_all [simp]: "length xs \ n \ take n xs = xs" by (induct n arbitrary: xs) (auto, case_tac xs, auto) -lemma drop_all [simp]: "length xs \ n ==> drop n xs = []" +lemma drop_all [simp]: "length xs \ n \ 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 \ (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 \ length xs ==> (drop n xs)!i = xs!(n + i)" + "n \ length xs \ (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 \ length xs ==> butlast (take n xs) = take (n - 1) xs" + "n \ length xs \ 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 \ 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]: - "(\x. x \ set xs \ P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys" + "(\x. x \ set xs \ P(x)) \ dropWhile P (xs @ ys) = dropWhile P ys" by (induct xs) auto lemma dropWhile_append3: @@ -2419,10 +2420,10 @@ "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys \ \ P y)" by(induct xs, auto) -lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)" +lemma distinct_takeWhile[simp]: "distinct xs \ 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 \ distinct (dropWhile P xs)" by (induct xs) auto lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \ f) xs)" @@ -2582,12 +2583,12 @@ by (induct xs ys rule:list_induct2') auto lemma zip_append [simp]: - "[| length xs = length us |] ==> + "\length xs = length us\ \ zip (xs@ys) (us@vs) = zip xs us @ zip ys vs" by (simp add: zip_append1) lemma zip_rev: - "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)" + "length xs = length ys \ zip (rev xs) (rev ys) = rev (zip xs ys)" by (induct rule:list_induct2, simp_all) lemma zip_map_map: @@ -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)" + "\i < length xs; i < length ys\ \ (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 \\<^const>\list_all2\\ lemma list_all2_lengthD [intro?]: - "list_all2 P xs ys ==> length xs = length ys" + "list_all2 P xs ys \ 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 \ P2 b c \ P3 a c" + shows "!!bs cs. list_all2 P1 as bs \ list_all2 P2 bs cs \ list_all2 P3 as cs" (is "!!bs cs. PROP ?Q as bs cs") 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 \ i ==> [i.. i \ [i.. j \ i)" @@ -3238,11 +3239,11 @@ by (simp add: upt_rec) qed simp -lemma upt_Suc_append: "i \ j ==> [i..<(Suc j)] = [i.. j \ [i..<(Suc j)] = [i.. \Only needed if \upt_Suc\ is deleted from the simpset.\ by simp -lemma upt_conv_Cons: "i < j ==> [i.. [i.. \no precondition\ @@ -3253,14 +3254,14 @@ case True then show ?thesis by (simp add: upt_conv_Cons) qed -lemma upt_add_eq_append: "i<=j ==> [i.. [i.. \LOOPS as a simprule, since \j \ j\.\ by (induct k) auto lemma length_upt [simp]: "length [i.. [i.. [i.. hd[i.. last[i.. n ==> take m [i.. n \ take m [i..i. i + n) [0.. (map f [m.. (map f [m.. xs = ys" by (simp add: list_all2_conv_all_nth nth_equalityI) -lemma take_equalityI: "(\i. take i xs = take i ys) ==> xs = ys" +lemma take_equalityI: "(\i. take i xs = take i ys) \ xs = ys" \ \The famous take-lemma.\ by (metis length_take min.commute order_refl take_all) @@ -3403,10 +3404,11 @@ qed lemma nth_upto[simp]: "i + int k \ j \ [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 \ j \ j \ k \ [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 \ remdups xs = xs" by (induct xs, auto) lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \ distinct xs" @@ -3491,17 +3493,18 @@ "distinct (map f xs) \ 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 \ distinct (filter P xs)" by (induct xs) auto lemma distinct_upt[simp]: "distinct[i.. distinct (take i xs)" proof (induct xs arbitrary: i) @@ -3531,10 +3534,10 @@ by auto next case False + have "set (take i xs) \ 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 \i < length xs\ - 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 \i < length xs\ 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]: "\ i < size xs; j < size xs \ \ +lemma distinct_swap[simp]: "\ i < size xs; j < size xs\ \ 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]: "\ i < size xs; j < size xs \ \ 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 \ 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 \ 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 \ x by (cases x) auto - done + using less_Suc_eq_0_disj by auto also have "\ = f ` {0 ..< length (x1 # x2 # xs)}" proof - have "f 0 = f (Suc 0)" using \x1 = x2\ f_nth[of 0] by simp then show ?thesis - apply safe - apply fastforce - subgoal for \ x by (cases x) auto - done + using less_Suc_eq_0_disj by auto qed also have "\ = {0 ..< length ys}" by fact finally show "?f' ` {0 ..< length (x1 # xs)} = {0 ..< length ys}" . @@ -3842,7 +3838,7 @@ next assume "x1 \ x2" - have "2 \ length ys" + have two: "Suc (Suc 0) \ length ys" proof - have "2 = card {f 0, f 1}" using \x1 \ x2\ f_nth[of 0] by auto also have "\ \ card (f ` {0..< length (x1 # x2 # xs)})" @@ -3862,26 +3858,18 @@ then have "Suc 0 \ f i" for i using \f 0 = 0\ by (cases i) fastforce+ then have "Suc 0 \ f ` {0 ..< length (x1 # x2 # xs)}" by auto - then show False using f_img \2 \ length ys\ by auto + then show False using f_img two by auto qed obtain ys' where "ys = x1 # x2 # ys'" - using \2 \ length ys\ f_nth[of 0] f_nth[of 1] - apply (cases ys) - apply (rename_tac [2] ys', case_tac [2] ys') - apply (auto simp: \f 0 = 0\ \f (Suc 0) = Suc 0\) - done + using two f_nth[of 0] f_nth[of 1] + by (auto simp: Suc_le_length_iff \f 0 = 0\ \f (Suc 0) = Suc 0\) + + have Suc0_le_f_Suc: "Suc 0 \ f (Suc i)" for i + by (metis Suc_le_mono \f (Suc 0) = Suc 0\ f_mono le0 mono_def) define f' where "f' x = f (Suc x) - 1" for x - - { fix i - have "Suc 0 \ f (Suc 0)" using f_nth[of 0] \x1 \ x2\ \f 0 = 0\ by auto - also have "\ \ f (Suc i)" using f_mono by (rule monoD) arith - finally have "Suc 0 \ 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 [] \ [x] | y # xs \ 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) \ remdups_adj xs ! i \ 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 \ 0 ==> hd (replicate n x) = x" +lemma hd_replicate [simp]: "n \ 0 \ 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 \ 0 ==> last (replicate n x) = x" +lemma last_replicate [simp]: "n \ 0 \ 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 \ (replicate n x)!i = x" by (induct n arbitrary: i)(auto simp: nth_Cons split: nat.split) text\Courtesy of Matthias Daum (2 lemmas):\ @@ -4273,7 +4261,7 @@ lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}" by (induct n) auto -lemma set_replicate [simp]: "n \ 0 ==> set (replicate n x) = {x}" +lemma set_replicate [simp]: "n \ 0 \ 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 \xs \ []\ 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 \ 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 \\<^const>\nths\ --- a generalization of \<^const>\nth\ to sets\ 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: "\i < length xs. i \ I \ 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 \ i \ 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 (\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 i \ 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) \ set xs" -by(auto simp add:set_nths) + by(auto simp add:set_nths) lemma notin_set_nthsI[simp]: "x \ set xs \ x \ set(nths xs I)" -by(auto simp add:set_nths) + by(auto simp add:set_nths) lemma in_set_nthsD: "x \ set(nths xs I) \ x \ set xs" -by(auto simp add:set_nths) + by(auto simp add:set_nths) lemma nths_singleton [simp]: "nths [x] A = (if 0 \ A then [x] else [])" -by (simp add: nths_Cons) + by (simp add: nths_Cons) lemma distinct_nthsI[simp]: "distinct xs \ 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 {.. A. \j \ B. card {i' \ 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 \ 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 P(xs!i)}" -by(induction xs) (auto simp: nths_Cons) + by(induction xs) (auto simp: nths_Cons) lemma filter_in_nths: "distinct xs \ filter (%x. x \ set (nths xs s)) xs = nths xs s" @@ -4732,18 +4713,20 @@ subsubsection \\<^const>\splice\\ 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 = [] \ xs = [] \ 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 \\<^const>\shuffles\\ @@ -4768,7 +4751,7 @@ by (induct xs ys rule: shuffles.induct) auto lemma splice_in_shuffles [simp, intro]: "splice xs ys \ 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 = [] \ ys = [] \ [] \ shuffles xs ys" by simp @@ -5001,13 +4984,13 @@ subsubsection \\<^const>\min\ and \<^const>\arg_min\\ lemma min_list_Min: "xs \ [] \ 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 \ [] \ 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 \ [] \ arg_min_list f xs \ set xs" -by(induction xs rule: induct_list012) (auto simp: Let_def) + by(induction xs rule: induct_list012) (auto simp: Let_def) subsubsection \(In)finiteness\ @@ -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 \ 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 \ sorted_list_of_set A = [] \ 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 \ 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 \ B ==> listsp A \ listsp B" +lemma listsp_mono [mono]: "A \ B \ listsp A \ 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 \ 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 ==> \x\set xs. A x" +lemma in_listspD [dest!]: "listsp A xs \ \x\set xs. A x" by (rule in_listsp_conv_set [THEN iffD1]) lemmas in_listsD [dest!] = in_listspD [to_set] -lemma in_listspI [intro!]: "\x\set xs. A x ==> listsp A xs" +lemma in_listspI [intro!]: "\x\set xs. A x \ 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) \ lexn r n \ length xs = n \ 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 "\i j. lexn r i \ lexn r j \ Domain (lexn r i) \ Range (lexn r j) = {}" + by (metis DomainE Int_emptyI RangeE lexn_length) +qed + lemma lexn_conv: "lexn r n = {(xs,ys). length xs = n \ length ys = n \ (\xys x y xs' ys'. xs= xys @ x#xs' \ ys= xys @ y # ys' \ (x, y) \ 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\By Mathias Fleury:\ proposition lexn_transI: @@ -6121,7 +6111,7 @@ (\xys x y xs' ys'. xs = xys @ x # xs' \ ys = xys @ y # ys' \ (x, y) \ r)}" by (force simp add: lex_def lexn_conv) -lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)" +lemma wf_lenlex [intro!]: "wf r \ 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) \ lex r" -by (simp add: lex_conv) + by (simp add: lex_conv) lemma Nil2_notin_lex [iff]: "(xs, []) \ lex r" -by (simp add:lex_conv) + by (simp add:lex_conv) lemma Cons_in_lex [simp]: - "((x # xs, y # ys) \ lex r) = - ((x, y) \ r \ length xs = length ys \ x = y \ (xs, ys) \ 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) \ lex r \ (x, y) \ r \ length xs = length ys \ x = y \ (xs, ys) \ 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) \ lenlex r \ ns \ []" and Nil_lenlex_iff2 [simp]: "(ns,[]) \ lenlex r" @@ -6181,24 +6174,23 @@ lemma lex_append_rightI: "(xs, ys) \ lex r \ length vs = length us \ (xs @ us, ys @ vs) \ lex r" -by (fastforce simp: lex_def lexn_conv) + by (fastforce simp: lex_def lexn_conv) lemma lex_append_leftI: "(ys, zs) \ lex r \ (xs @ ys, xs @ zs) \ lex r" -by (induct xs) auto + by (induct xs) auto lemma lex_append_leftD: "\x. (x,x) \ r \ (xs @ ys, xs @ zs) \ lex r \ (ys, zs) \ lex r" -by (induct xs) auto + by (induct xs) auto lemma lex_append_left_iff: "\x. (x,x) \ r \ (xs @ ys, xs @ zs) \ lex r \ (ys, zs) \ 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) \ 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) \ r" proof - obtain n us x xs' y ys' where "(xs, ys) \ 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) \ lexord r) = ((a,b)\ r \ (a = b \ (x,y)\ lexord r))" - unfolding lexord_def - apply (safe, simp_all) - apply (metis hd_append list.sel(1)) + "(a # x, b # y) \ lexord r \ (a,b)\ r \ (a = b \ (x,y)\ 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: "\ b z. y = b # z \ (x, x @ y) \ lexord r" -by (induct_tac x, auto) + by (induct_tac x, auto) lemma lexord_append_left_rightI: - "(a,b) \ r \ (u @ a # x, u @ b # y) \ lexord r" -by (induct_tac u, auto) + "(a,b) \ r \ (u @ a # x, u @ b # y) \ lexord r" + by (induct_tac u, auto) lemma lexord_append_leftI: " (u,v) \ lexord r \ (x @ u, x @ v) \ lexord r" -by (induct x, auto) + by (induct x, auto) lemma lexord_append_leftD: - "\ (x @ u, x @ v) \ lexord r; (\a. (a,a) \ r) \ \ (u,v) \ lexord r" -by (erule rev_mp, induct_tac x, auto) + "\(x @ u, x @ v) \ lexord r; (\a. (a,a) \ r) \ \ (u,v) \ lexord r" + by (erule rev_mp, induct_tac x, auto) lemma lexord_take_index_conv: "((x,y) \ lexord r) = ((length x < length y \ take (length x) y = x) \ (\i. i < min(length x)(length y) \ take i x = take i y \ (x!i,y!i) \ r))" - apply (unfold lexord_def Let_def, clarsimp) - apply (rule_tac f = "(% a b. a \ 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 "(\a v. y = x @ a # v) = (length x < length y \ take (length x) y = x)" + by (metis Cons_nth_drop_Suc append_eq_conv_conj drop_all list.simps(3) not_le) + moreover + have "(\u a b. (a, b) \ r \ (\v. x = u @ a # v) \ (\w. y = u @ b # w)) = + (\i take i x = take i y \ (x ! i, y ! i) \ 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 \ \lexord is extension of partial ordering List.lex\ lemma lexord_lex: "(x,y) \ lex r = ((x,y) \ lexord r \ length x = length y)" @@ -6539,10 +6538,10 @@ unfolding measures_def by auto -lemma measures_less: "f x < f y ==> (x, y) \ measures (f#fs)" +lemma measures_less: "f x < f y \ (x, y) \ measures (f#fs)" by simp -lemma measures_lesseq: "f x \ f y ==> (x, y) \ measures fs ==> (x, y) \ measures (f#fs)" +lemma measures_lesseq: "f x \ f y \ (x, y) \ measures fs \ (x, y) \ measures (f#fs)" by auto @@ -6685,7 +6684,7 @@ for r :: "('a \ 'b) set" where Nil: "([],[]) \ listrel r" - | Cons: "[| (x,y) \ r; (xs,ys) \ listrel r |] ==> (x#xs, y#ys) \ listrel r" + | Cons: "\(x,y) \ r; (xs,ys) \ listrel r\ \ (x#xs, y#ys) \ listrel r" inductive_cases listrel_Nil1 [elim!]: "([],xs) \ listrel r" inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \ listrel r" diff -r 24b68a932f26 -r 4b1021677f15 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu Mar 19 11:57:43 2020 +0100 +++ b/src/HOL/Nat.thy Sun Mar 22 17:21:16 2020 +0000 @@ -65,15 +65,15 @@ by (rule iffI, rule Suc_Rep_inject) simp_all lemma nat_induct0: - assumes "P 0" - and "\n. P n \ P (Suc n)" + assumes "P 0" and "\n. P n \ P (Suc n)" shows "P n" - using assms - apply (unfold Zero_nat_def Suc_def) - apply (rule Rep_Nat_inverse [THEN subst]) \ \types force good instantiation\ - 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 \Sign.mandatory_path "old"\ 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 \Sign.parent_path\ @@ -356,18 +352,11 @@ qed lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \ m = Suc 0 \ 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 \ m = 1 \ 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 \ m = 1 \ 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 \ m = 1 \ n = 1" + and nat_1_eq_mult_iff [simp]: "1 = m * n \ m = 1 \ n = 1" for m n :: nat + by auto lemma mult_cancel1 [simp]: "k * m = k * n \ m = n \ k = 0" for k m n :: nat @@ -584,22 +573,23 @@ and less: "m < n \ P" and eq: "m = n \ 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 \ P" + using eq by blast + show "\j. \m < j; Suc n = Suc j\ \ P" + by (blast intro: less) +qed lemma Suc_lessE: assumes major: "Suc i < k" and minor: "\j. i < j \ k = Suc j \ 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) \ P" + using lessI minor by iprover + show "\j. \Suc i < j; k = Suc j\ \ P" + using Suc_lessD minor by iprover +qed lemma Suc_less_SucD: "Suc m < Suc n \ m < n" by simp @@ -786,12 +776,16 @@ by (induct k) simp_all text \strict, in both arguments\ -lemma add_less_mono: "i < j \ k < l \ 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 \i < j\ by (induction j) (auto simp: assms) + finally show ?thesis . +qed lemma less_imp_Suc_add: "m < n \ \k. n = Suc (m + k)" proof (induct n) @@ -969,42 +963,55 @@ for P :: "nat \ bool" by (rule Least_equality[OF _ le0]) -lemma Least_Suc: "P n \ \ P 0 \ (LEAST n. P n) = Suc (LEAST m. P (Suc m))" - apply (cases n) - apply auto - apply (frule LeastI) - apply (drule_tac P = "\x. P (Suc x)" in LeastI) - apply (subgoal_tac " (LEAST x. P x) \ Suc (LEAST x. P (Suc x))") - apply (erule_tac [2] Least_le) - apply (cases "LEAST x. P x") - apply auto - apply (drule_tac P = "\x. P (Suc x)" in Least_le) - apply (blast intro: order_antisym) - done +lemma Least_Suc: + assumes "P n" "\ 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) \ Suc (LEAST x. P (Suc x))" + using assms Suc by (force intro: LeastI Least_le) + have \
: "P (LEAST x. P x)" + by (blast intro: LeastI assms) + show "Suc (LEAST m. P (Suc m)) \ (LEAST n. P n)" + proof (cases "(LEAST n. P n)") + case 0 + then show ?thesis + using \
by (simp add: assms) + next + case Suc + with \
show ?thesis + by (auto simp: Least_le) + qed + qed +qed (use assms in auto) lemma Least_Suc2: "P n \ Q m \ \ P 0 \ \k. P (Suc k) = Q k \ Least P = Suc (Least Q)" by (erule (1) Least_Suc [THEN ssubst]) simp -lemma ex_least_nat_le: "\ P 0 \ P n \ \k\n. (\i P i) \ P k" - for P :: "nat \ 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: "\ P 0 \ P n \ \ki\k. \ P i) \ P (k + 1)" - for P :: "nat \ 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 \ bool" + assumes "P n" "\ P 0" + shows "\k\n. (\i P i) \ 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 \ bool" + assumes "P n" "\ P 0" + shows "\ki\k. \ P i) \ P (Suc k)" +proof (cases n) + case (Suc m) + then obtain k where k: "k \ n" "\i 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 \ bool" @@ -1070,11 +1077,10 @@ assumes "P 0" and "\n. n > 0 \ \ P n \ \m. m < n \ \ P m" shows "P n" - apply (rule infinite_descent) - using assms - apply (case_tac "n > 0") - apply auto - done +proof (rule infinite_descent) + show "\n. \ P n \ \m P m" + using assms by (case_tac "n > 0") auto +qed text \ Infinite descent using a mapping to \nat\: @@ -1178,14 +1184,11 @@ lemma not_add_less1 [iff]: "\ 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]: "\ j + i < i" for i j :: nat - by (simp add: add.commute) + by simp lemma add_leD1: "m + k \ n \ m \ n" for k m n :: nat @@ -1193,9 +1196,7 @@ lemma add_leD2: "m + k \ n \ k \ 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 \ n \ (m \ n \ k \ n \ R) \ 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 \ m" for m n :: nat @@ -1345,12 +1343,26 @@ lemma mult_less_cancel2 [simp]: "m * k < n * k \ 0 < k \ 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 \ m < n" + then show "m * k < n * k" + by (blast intro: mult_less_mono1) +qed lemma mult_less_cancel1 [simp]: "k * m < k * n \ 0 < k \ m < n" for k m n :: nat @@ -1379,16 +1391,18 @@ by (cases m) (auto intro: le_add1) text \Lemma for \gcd\\ -lemma mult_eq_self_implies_10: "m = m * n \ n = 1 \ 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 \ m = 0" +proof (rule disjCI) + assume "m \ 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] \m \ 0\ by auto + qed (use assms \m \ 0\ in auto) +qed lemma mono_times_nat: fixes n :: nat @@ -1849,28 +1863,20 @@ by (simp add: Nats_def) lemma Nats_0 [simp]: "0 \ \" - 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 \ \" - 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 \ \ \ b \ \ \ a + b \ \" - 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 \ \ \ b \ \ \ a * b \ \" - 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 \ \" @@ -2303,21 +2309,21 @@ qed qed -lemma GreatestI_nat: - "\ P(k::nat); \y. P y \ y \ b \ \ P (Greatest P)" -apply(drule (1) ex_has_greatest_nat) -using GreatestI2_order by auto - -lemma Greatest_le_nat: - "\ P(k::nat); \y. P y \ y \ b \ \ k \ (Greatest P)" -apply(frule (1) ex_has_greatest_nat) -using GreatestI2_order[where P=P and Q=\\x. k \ x\] by auto +lemma + fixes k::nat + assumes "P k" and minor: "\y. P y \ y \ b" + shows GreatestI_nat: "P (Greatest P)" + and Greatest_le_nat: "k \ Greatest P" +proof - + obtain x where "P x" "\y. P y \ y \ x" + using assms ex_has_greatest_nat by blast + with \P k\ show "P (Greatest P)" "k \ Greatest P" + using GreatestI2_order by blast+ +qed lemma GreatestI_ex_nat: - "\ \k::nat. P k; \y. P y \ y \ b \ \ P (Greatest P)" -apply (erule exE) -apply (erule (1) GreatestI_nat) -done + "\ \k::nat. P k; \y. P y \ y \ b \ \ P (Greatest P)" + by (blast intro: GreatestI_nat) subsection \Monotonicity of \funpow\\ @@ -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 \ k dvd n \ n \ m \ 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 \ 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 \ k dvd m \ n \ m \ k dvd n" for k m n :: nat @@ -2384,13 +2395,19 @@ then show ?thesis .. qed -lemma dvd_mult_cancel1: "0 < m \ m * n dvd m \ 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 \ 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 \ n * m dvd m \ n = 1" for m n :: nat @@ -2441,15 +2458,6 @@ lemma nat_mult_1_right: "n * 1 = n" for n :: nat by (fact mult_1_right) - -lemma nat_add_left_cancel: "k + m = k + n \ m = n" - for k m n :: nat - by (fact add_left_cancel) - -lemma nat_add_right_cancel: "m + k = n + k \ 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,14 +2466,6 @@ for k m n :: nat by (fact right_diff_distrib') -lemma le_add_diff: "k \ n \ m \ n + m - k" - for k m n :: nat - by (fact le_add_diff) (* FIXME delete *) - -lemma le_diff_conv2: "k \ j \ (i \ j - k) = (i + k \ j)" - for i j k :: nat - by (fact le_diff_conv2) (* FIXME delete *) - lemma diff_self_eq_0 [simp]: "m - m = 0" for m :: nat by (fact diff_cancel) diff -r 24b68a932f26 -r 4b1021677f15 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Thu Mar 19 11:57:43 2020 +0100 +++ b/src/HOL/Transcendental.thy Sun Mar 22 17:21:16 2020 +0000 @@ -618,10 +618,6 @@ for r :: "'a::ring_1" by (simp add: sum_subtractf) -lemma lemma_realpow_rev_sumr: - "(\pp 0" @@ -629,26 +625,26 @@ h * (\p< n - Suc 0. \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: "\x k. (\njiijiijppip::nat. p < n \ f p \ K" - and K: "0 \ K" + assumes f: "\p::nat. p < n \ f p \ K" and K: "0 \ K" shows "sum f {.. 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 {.. (\i 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 \ K" by (rule order_trans) - have le_Kn: "\i j n. i + j = n \ norm ((z + h) ^ i * z ^ j) \ 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) \ K ^ n" if "i + j = n" for i j n + proof - + have "norm (z + h) ^ i * norm z ^ j \ 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 "\p q. + \p < n; q < n - Suc 0\ \ norm ((z + h) ^ q * z ^ (n - 2 - q)) \ K ^ (n - 2)" + by simp + then show "norm (\pq 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 "\ = 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 (\n. of_nat n * diffs (\n. norm (c n)) n * r ^ (n - Suc 0))" by (rule diffs_equiv [THEN sums_summable]) also have "(\n. of_nat n * diffs (\n. norm (c n)) n * r ^ (n - Suc 0)) = - (\n. diffs (\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 + (\n. diffs (\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 (\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 "(\n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0)) = (\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 (\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 \ 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))) \ + have "norm (((x + h) ^ n - x ^ n) / h - of_nat n * x ^ (n - Suc 0)) + \ 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))) \ 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 (\x. \n. c n * x^n) x :> (\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 (\n. c n * (of_real (norm x + norm K) / 2) ^ n)" @@ -915,11 +905,8 @@ moreover have "\x. norm x < norm K \ summable (\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 \auto simp: field_simps simp flip: of_real_add\) qed lemma termdiffs_strong_converges_everywhere: @@ -999,11 +986,12 @@ by (blast intro: DERIV_continuous) then have "((\x. \n. a n * x ^ n) \ a 0) (at 0)" by (simp add: continuous_within) - then show ?thesis - apply (rule Lim_transform) + moreover have "(\x. f x - (\n. a n * x ^ n)) \0\ 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 *: "((\x. if x = 0 then a 0 else f x) \ 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 = "(\x. if x = 0 then a 0 else f x)"]) - apply (simp_all add: *) - done + by (simp add: * LIM_equal [where g = "(\x. if x = 0 then a 0 else f x)"]) qed @@ -1591,10 +1577,10 @@ have "1 + x \ (\n<2. inverse (fact n) * x^n)" by (auto simp: numeral_2_eq_2) also have "\ \ (\n. inverse (fact n) * x^n)" - apply (rule sum_le_suminf [OF summable_exp]) - using \0 < x\ - apply (auto simp add: zero_le_mult_iff) - done + proof (rule sum_le_suminf [OF summable_exp]) + show "\m\- {..<2}. 0 \ inverse (fact m) * x ^ m" + using \0 < x\ by (auto simp add: zero_le_mult_iff) + qed auto finally show "1 + x \ exp x" by (simp add: exp_def) qed auto @@ -2049,9 +2035,7 @@ proof (cases "0 \ x \ x \ -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) \ x" @@ -2463,11 +2447,12 @@ lemma powr_non_neg[simp]: "\a powr x < 0" for a x::real using powr_ge_pzero[of a x] by arith +lemma inverse_powr: "\y::real. 0 \ y \ inverse y powr a = inverse (y powr a)" + by (simp add: exp_minus ln_inverse powr_def) + lemma powr_divide: "\0 \ x; 0 \ y\ \ (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 (\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 "\N. \n\N. norm (norm (sin_coeff n *\<^sub>R x ^ n)) \ 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 (\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 "\N. \n\N. norm (norm (cos_coeff n *\<^sub>R x ^ n)) \ 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: "(\n. sin_coeff n *\<^sub>R x^n) sums sin x" unfolding sin_def @@ -3230,8 +3218,7 @@ by (rule sin_converges) finally have "(\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 \ \ \ sin z \ \" @@ -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 \ 'b::{real_normed_field,banach}" +begin + lemma isCont_sin' [simp]: "isCont f a \ isCont (\x. sin (f x)) a" - for f :: "_ \ '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 \ isCont (\x. cos (f x)) a" - for f :: "_ \ 'a::{real_normed_field,banach}" by (rule isCont_o2 [OF _ isCont_cos]) lemma tendsto_sin [tendsto_intros]: "(f \ a) F \ ((\x. sin (f x)) \ sin a) F" - for f :: "_ \ 'a::{real_normed_field,banach}" by (rule isCont_tendsto_compose [OF isCont_sin]) lemma tendsto_cos [tendsto_intros]: "(f \ a) F \ ((\x. cos (f x)) \ cos a) F" - for f :: "_ \ 'a::{real_normed_field,banach}" by (rule isCont_tendsto_compose [OF isCont_cos]) lemma continuous_sin [continuous_intros]: "continuous F f \ continuous F (\x. sin (f x))" - for f :: "_ \ 'a::{real_normed_field,banach}" unfolding continuous_def by (rule tendsto_sin) lemma continuous_on_sin [continuous_intros]: "continuous_on s f \ continuous_on s (\x. sin (f x))" - for f :: "_ \ 'a::{real_normed_field,banach}" unfolding continuous_on_def by (auto intro: tendsto_sin) +lemma continuous_cos [continuous_intros]: "continuous F f \ continuous F (\x. cos (f x))" + unfolding continuous_def by (rule tendsto_cos) + +lemma continuous_on_cos [continuous_intros]: "continuous_on s f \ continuous_on s (\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 \ continuous F (\x. cos (f x))" - for f :: "_ \ 'a::{real_normed_field,banach}" - unfolding continuous_def by (rule tendsto_cos) - -lemma continuous_on_cos [continuous_intros]: "continuous_on s f \ continuous_on s (\x. cos (f x))" - for f :: "_ \ '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 \ DERIV (\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 \ DERIV (\x. cos(g x)) x :> - sin (g x) * m" - by (auto intro!: derivative_eq_intros) + by (fact derivative_intros) subsection \Deriving the Addition Formulas\ @@ -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 \n \ p\ neq0_conv that(1) by blast + then have \
: "(- 1::real) ^ (p div 2 - Suc 0) = - ((- 1) ^ (p div 2))" + using \even p\ by (auto simp add: dvd_def power_eq_if) from \n \ p\ np have *: "n - Suc 0 + (p - Suc n) = p - Suc (Suc 0)" "Suc (Suc 0) \ p" by arith+ have "(p - Suc (Suc 0)) div 2 = p div 2 - Suc 0" by simp - with \n \ p\ 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 \n \ p\ np \
* show ?thesis + by (simp add: flip: div_add power_add) qed then show ?thesis using \n\p\ 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 \ x" "cos x = 0" - shows "\n. odd n \ x = of_nat n * (pi/2) \ n > 0" + shows "\n. odd n \ x = of_nat n * (pi/2)" proof - have xle: "x < (1 + real_of_int \x/pi\) * 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 \ x \ sin x = 0 \ \n::nat. even n \ 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 \ x" "sin x = 0" + shows "\n::nat. even n \ 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: \odd n\) +qed lemma cos_zero_iff: "cos x = 0 \ ((\n. odd n \ x = real n * (pi/2)) \ (\n. odd n \ 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 \ (\n. odd n \ x = of_int n * (pi/2))" +lemma cos_zero_iff_int: "cos x = 0 \ (\i. odd i \ x = of_int i * (pi/2))" proof - have 1: "\n. odd n \ \i. odd i \ 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 \ (\n. even n \ x = of_int n * (pi/2))" +lemma sin_zero_iff_int: "sin x = 0 \ (\i. even i \ 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 "\n. even n \ 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 \ (\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 \ (\i::int. x = of_int i * pi)" +proof - + have "sin x = 0 \ (\i. even i \ x = real_of_int i * (pi / 2))" + by (auto simp: sin_zero_iff_int) + also have "... = (\j. x = real_of_int (2*j) * (pi / 2))" + using dvd_triv_left by blast + also have "... = (\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 \ 0" + assumes "x \ 0" shows "sin x \ x" proof - let ?f = "\x. x - sin x" - from x have "?f x \ ?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 "\u. \0 \ u; u \ x\ \ \y. (?f has_real_derivative 1 - cos u) (at u)" + by (auto intro!: derivative_eq_intros simp: field_simps) + then have "?f x \ ?f 0" + by (metis cos_le_one diff_ge_0_iff_ge DERIV_nonneg_imp_nondecreasing [OF assms]) then show "sin x \ x" by simp qed @@ -4270,11 +4270,10 @@ shows "sin x \ - x" proof - let ?f = "\x. x + sin x" - from x have "?f x \ ?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 \
: "\u. \0 \ u; u \ x\ \ \y. (?f has_real_derivative 1 + cos u) (at u)" + by (auto intro!: derivative_eq_intros simp: field_simps) + have "?f x \ ?f 0" + by (rule DERIV_nonneg_imp_nondecreasing [OF assms]) (use \
real_0_le_add_iff in force) then show "sin x \ -x" by simp qed @@ -4409,9 +4408,8 @@ have "cos(3 * x) = cos(2*x + x)" by simp also have "\ = 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: "\y. (- pi < y \ y \ pi) \ (sin y = sin x \ 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 \ pi - (2 * pi) * frac ((pi - x) / (2 * pi))" + have "-pi < y"" y \ 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 \Tangent\ @@ -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 "\y. \x - 1 < y; y < x + 1\ \ tan (arctan y) = y" using tan_arctan by blast show "1 + x\<^sup>2 \ 0" @@ -5999,19 +6004,15 @@ assumes "x \ 0" shows "arctan (1 / x) = sgn x * pi/2 - arctan x" proof (rule arctan_unique) + have \
: "x > 0 \ 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 \
) 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: "\r::real. \a. x = r * cos a \ y = r * sin a" proof - - have polar_ex1: "0 < y \ \r a. x = r * cos a \ 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: "\r a. x = r * cos a \ 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: "\i. i > m \ a i = 0" and n: "\j. j > n \ b j = 0" shows "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = - (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" -proof - + (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" +proof - + have "\i j. \m + n - i < j; a i \ 0\ \ b j = 0" + by (meson le_add_diff leI le_less_trans m n) + then have \
: "(\(i,j)\(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 "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = (\i\m. \j\n. (a i * x ^ i) * (b j * x ^ j))" by (rule sum_product) also have "\ = (\i\m + n. \j\n + m. a i * x ^ i * (b j * x ^ j))" using assms by (auto simp: sum_up_index_split) also have "\ = (\r\m + n. \j\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 \
) also have "\ = (\(i,j)\{(i,j). i+j \ m+n}. (a i * x ^ i) * (b j * x ^ j))" by (auto simp: pairs_le_eq_Sigma sum.Sigma) + also have "... = (\k\m + n. \i\k. a i * x ^ i * (b (k - i) * x ^ (k - i)))" + by (rule sum.triangle_reindex_eq) also have "\ = (\r\m + n. (\k\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: "\i. i > m \ a i = 0" and n: "\j. j > n \ b j = 0" shows "(\i\m. (a i) * x ^ i) * (\j\n. (b j) * x ^ j) = - (\r\m + n. (\k\r. (a k) * (b (r - k))) * x ^ r)" + (\r\m + n. (\k\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 "(\i=Suc j..n. a i * y^(i - j - 1)) = (\ki. 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 "\k. k < n - j \ k \ (\i. i - Suc j) ` {Suc j..n}" + by (rule_tac x="k + Suc j" in image_eqI, auto) + then have h: "bij_betw (\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