# HG changeset patch # User wenzelm # Date 1466454676 -7200 # Node ID 83a91a73fcb551bcf6fdaa8887a11d4d866cea40 # Parent 0c89eef797017a1769f32dbf59c7b83f0010dc37# Parent 9d2470571719ba9ed5f0a102c132edf5d93ea448 merged diff -r 0c89eef79701 -r 83a91a73fcb5 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Mon Jun 20 10:51:34 2016 +0200 +++ b/src/HOL/Fun.thy Mon Jun 20 22:31:16 2016 +0200 @@ -11,11 +11,10 @@ keywords "functor" :: thy_goal begin -lemma apply_inverse: - "f x = u \ (\x. P x \ g (f x) = x) \ P x \ x = g u" +lemma apply_inverse: "f x = u \ (\x. P x \ g (f x) = x) \ P x \ x = g u" by auto -text\Uniqueness, so NOT the axiom of choice.\ +text \Uniqueness, so NOT the axiom of choice.\ lemma uniq_choice: "\x. \!y. Q x y \ \f. \x. Q x (f x)" by (force intro: theI') @@ -24,8 +23,8 @@ subsection \The Identity Function \id\\ -definition id :: "'a \ 'a" where - "id = (\x. x)" +definition id :: "'a \ 'a" + where "id = (\x. x)" lemma id_apply [simp]: "id x = x" by (simp add: id_def) @@ -51,55 +50,51 @@ notation (ASCII) comp (infixl "o" 55) -lemma comp_apply [simp]: "(f o g) x = f (g x)" +lemma comp_apply [simp]: "(f \ g) x = f (g x)" by (simp add: comp_def) -lemma comp_assoc: "(f o g) o h = f o (g o h)" +lemma comp_assoc: "(f \ g) \ h = f \ (g \ h)" by (simp add: fun_eq_iff) -lemma id_comp [simp]: "id o g = g" +lemma id_comp [simp]: "id \ g = g" by (simp add: fun_eq_iff) -lemma comp_id [simp]: "f o id = f" +lemma comp_id [simp]: "f \ id = f" by (simp add: fun_eq_iff) lemma comp_eq_dest: - "a o b = c o d \ a (b v) = c (d v)" + "a \ b = c \ d \ a (b v) = c (d v)" by (simp add: fun_eq_iff) lemma comp_eq_elim: - "a o b = c o d \ ((\v. a (b v) = c (d v)) \ R) \ R" + "a \ b = c \ d \ ((\v. a (b v) = c (d v)) \ R) \ R" by (simp add: fun_eq_iff) -lemma comp_eq_dest_lhs: "a o b = c \ a (b v) = c v" - by clarsimp - -lemma comp_eq_id_dest: "a o b = id o c \ a (b v) = c v" +lemma comp_eq_dest_lhs: "a \ b = c \ a (b v) = c v" by clarsimp -lemma image_comp: - "f ` (g ` r) = (f o g) ` r" +lemma comp_eq_id_dest: "a \ b = id \ c \ a (b v) = c v" + by clarsimp + +lemma image_comp: "f ` (g ` r) = (f \ g) ` r" by auto -lemma vimage_comp: - "f -` (g -` x) = (g \ f) -` x" +lemma vimage_comp: "f -` (g -` x) = (g \ f) -` x" by auto -lemma image_eq_imp_comp: "f ` A = g ` B \ (h o f) ` A = (h o g) ` B" +lemma image_eq_imp_comp: "f ` A = g ` B \ (h \ f) ` A = (h \ g) ` B" by (auto simp: comp_def elim!: equalityE) lemma image_bind: "f ` (Set.bind A g) = Set.bind A (op ` f \ g)" -by(auto simp add: Set.bind_def) + by (auto simp add: Set.bind_def) lemma bind_image: "Set.bind (f ` A) g = Set.bind A (g \ f)" -by(auto simp add: Set.bind_def) + by (auto simp add: Set.bind_def) -lemma (in group_add) minus_comp_minus [simp]: - "uminus \ uminus = id" +lemma (in group_add) minus_comp_minus [simp]: "uminus \ uminus = id" by (simp add: fun_eq_iff) -lemma (in boolean_algebra) minus_comp_minus [simp]: - "uminus \ uminus = id" +lemma (in boolean_algebra) minus_comp_minus [simp]: "uminus \ uminus = id" by (simp add: fun_eq_iff) code_printing @@ -108,8 +103,8 @@ subsection \The Forward Composition Operator \fcomp\\ -definition fcomp :: "('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" (infixl "\>" 60) where - "f \> g = (\x. g (f x))" +definition fcomp :: "('a \ 'b) \ ('b \ 'c) \ 'a \ 'c" (infixl "\>" 60) + where "f \> g = (\x. g (f x))" lemma fcomp_apply [simp]: "(f \> g) x = g (f x)" by (simp add: fcomp_def) @@ -123,7 +118,7 @@ lemma fcomp_id [simp]: "f \> id = f" by (simp add: fcomp_def) -lemma fcomp_comp: "fcomp f g = comp g f" +lemma fcomp_comp: "fcomp f g = comp g f" by (simp add: ext) code_printing @@ -134,168 +129,143 @@ subsection \Mapping functions\ -definition map_fun :: "('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" where - "map_fun f g h = g \ h \ f" +definition map_fun :: "('c \ 'a) \ ('b \ 'd) \ ('a \ 'b) \ 'c \ 'd" + where "map_fun f g h = g \ h \ f" -lemma map_fun_apply [simp]: - "map_fun f g h x = g (h (f x))" +lemma map_fun_apply [simp]: "map_fun f g h x = g (h (f x))" by (simp add: map_fun_def) subsection \Injectivity and Bijectivity\ -definition inj_on :: "('a \ 'b) \ 'a set \ bool" where \ "injective" - "inj_on f A \ (\x\A. \y\A. f x = f y \ x = y)" +definition inj_on :: "('a \ 'b) \ 'a set \ bool" \ \injective\ + where "inj_on f A \ (\x\A. \y\A. f x = f y \ x = y)" -definition bij_betw :: "('a \ 'b) \ 'a set \ 'b set \ bool" where \ "bijective" - "bij_betw f A B \ inj_on f A \ f ` A = B" +definition bij_betw :: "('a \ 'b) \ 'a set \ 'b set \ bool" \ \bijective\ + where "bij_betw f A B \ inj_on f A \ f ` A = B" -text\A common special case: functions injective, surjective or bijective over -the entire domain type.\ +text \A common special case: functions injective, surjective or bijective over + the entire domain type.\ -abbreviation - "inj f \ inj_on f UNIV" +abbreviation "inj f \ inj_on f UNIV" -abbreviation surj :: "('a \ 'b) \ bool" where \ "surjective" - "surj f \ (range f = UNIV)" +abbreviation surj :: "('a \ 'b) \ bool" \ "surjective" + where "surj f \ range f = UNIV" -abbreviation - "bij f \ bij_betw f UNIV UNIV" +abbreviation "bij f \ bij_betw f UNIV UNIV" -text\The negated case:\ +text \The negated case:\ translations -"\ CONST surj f" <= "CONST range f \ CONST UNIV" - -lemma injI: - assumes "\x y. f x = f y \ x = y" - shows "inj f" - using assms unfolding inj_on_def by auto - -theorem range_ex1_eq: "inj f \ b : range f = (EX! x. b = f x)" - by (unfold inj_on_def, blast) + "\ CONST surj f" \ "CONST range f \ CONST UNIV" -lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y" -by (simp add: inj_on_def) - -lemma inj_on_eq_iff: "\inj_on f A; x \ A; y \ A\ \ (f x = f y) = (x = y)" -by (force simp add: inj_on_def) +lemma injI: "(\x y. f x = f y \ x = y) \ inj f" + unfolding inj_on_def by auto -lemma inj_on_cong: - "(\ a. a : A \ f a = g a) \ inj_on f A = inj_on g A" -unfolding inj_on_def by auto - -lemma inj_on_strict_subset: - "inj_on f B \ A \ B \ f ` A \ f ` B" +theorem range_ex1_eq: "inj f \ b \ range f \ (\!x. b = f x)" unfolding inj_on_def by blast -lemma inj_comp: - "inj f \ inj g \ inj (f \ g)" +lemma injD: "inj f \ f x = f y \ x = y" + by (simp add: inj_on_def) + +lemma inj_on_eq_iff: "inj_on f A \ x \ A \ y \ A \ f x = f y \ x = y" + by (force simp add: inj_on_def) + +lemma inj_on_cong: "(\a. a \ A \ f a = g a) \ inj_on f A = inj_on g A" + unfolding inj_on_def by auto + +lemma inj_on_strict_subset: "inj_on f B \ A \ B \ f ` A \ f ` B" + unfolding inj_on_def by blast + +lemma inj_comp: "inj f \ inj g \ inj (f \ g)" by (simp add: inj_on_def) lemma inj_fun: "inj f \ inj (\x y. f x)" by (simp add: inj_on_def fun_eq_iff) -lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)" -by (simp add: inj_on_eq_iff) +lemma inj_eq: "inj f \ f x = f y \ x = y" + by (simp add: inj_on_eq_iff) lemma inj_on_id[simp]: "inj_on id A" by (simp add: inj_on_def) -lemma inj_on_id2[simp]: "inj_on (%x. x) A" -by (simp add: inj_on_def) +lemma inj_on_id2[simp]: "inj_on (\x. x) A" + by (simp add: inj_on_def) lemma inj_on_Int: "inj_on f A \ inj_on f B \ inj_on f (A \ B)" -unfolding inj_on_def by blast + unfolding inj_on_def by blast lemma surj_id: "surj id" -by simp + by simp lemma bij_id[simp]: "bij id" -by (simp add: bij_betw_def) + by (simp add: bij_betw_def) -lemma bij_uminus: - fixes x :: "'a :: ab_group_add" - shows "bij (uminus :: 'a\'a)" -unfolding bij_betw_def inj_on_def -by (force intro: minus_minus [symmetric]) +lemma bij_uminus: "bij (uminus :: 'a \ 'a::ab_group_add)" + unfolding bij_betw_def inj_on_def + by (force intro: minus_minus [symmetric]) -lemma inj_onI [intro?]: - "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A" -by (simp add: inj_on_def) +lemma inj_onI [intro?]: "(\x y. x \ A \ y \ A \ f x = f y \ x = y) \ inj_on f A" + by (simp add: inj_on_def) -lemma inj_on_inverseI: "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A" -by (auto dest: arg_cong [of concl: g] simp add: inj_on_def) - -lemma inj_onD: "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y" -by (unfold inj_on_def, blast) +lemma inj_on_inverseI: "(\x. x \ A \ g (f x) = x) \ inj_on f A" + by (auto dest: arg_cong [of concl: g] simp add: inj_on_def) -lemma comp_inj_on: - "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A" -by (simp add: comp_def inj_on_def) +lemma inj_onD: "inj_on f A \ f x = f y \ x \ A \ y \ A \ x = y" + unfolding inj_on_def by blast -lemma inj_on_imageI: "inj_on (g o f) A \ inj_on g (f ` A)" +lemma comp_inj_on: "inj_on f A \ inj_on g (f ` A) \ inj_on (g \ f) A" + by (simp add: comp_def inj_on_def) + +lemma inj_on_imageI: "inj_on (g \ f) A \ inj_on g (f ` A)" by (auto simp add: inj_on_def) -lemma inj_on_image_iff: "\ ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y); - inj_on f A \ \ inj_on g (f ` A) = inj_on g A" -unfolding inj_on_def by blast +lemma inj_on_image_iff: + "\x\A. \y\A. g (f x) = g (f y) \ g x = g y \ inj_on f A \ inj_on g (f ` A) = inj_on g A" + unfolding inj_on_def by blast -lemma inj_on_contraD: "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)" -unfolding inj_on_def by blast +lemma inj_on_contraD: "inj_on f A \ x \ y \ x \ A \ y \ A \ f x \ f y" + unfolding inj_on_def by blast lemma inj_singleton [simp]: "inj_on (\x. {x}) A" by (simp add: inj_on_def) lemma inj_on_empty[iff]: "inj_on f {}" -by(simp add: inj_on_def) - -lemma subset_inj_on: "[| inj_on f B; A <= B |] ==> inj_on f A" -unfolding inj_on_def by blast + by (simp add: inj_on_def) -lemma inj_on_Un: - "inj_on f (A Un B) = - (inj_on f A & inj_on f B & f`(A-B) Int f`(B-A) = {})" -apply(unfold inj_on_def) -apply (blast intro:sym) -done +lemma subset_inj_on: "inj_on f B \ A \ B \ inj_on f A" + unfolding inj_on_def by blast + +lemma inj_on_Un: "inj_on f (A \ B) \ inj_on f A \ inj_on f B \ f ` (A - B) \ f ` (B - A) = {}" + unfolding inj_on_def by (blast intro: sym) -lemma inj_on_insert[iff]: - "inj_on f (insert a A) = (inj_on f A & f a ~: f`(A-{a}))" -apply(unfold inj_on_def) -apply (blast intro:sym) -done +lemma inj_on_insert [iff]: "inj_on f (insert a A) \ inj_on f A \ f a \ f ` (A - {a})" + unfolding inj_on_def by (blast intro: sym) + +lemma inj_on_diff: "inj_on f A \ inj_on f (A - B)" + unfolding inj_on_def by blast -lemma inj_on_diff: "inj_on f A ==> inj_on f (A-B)" -apply(unfold inj_on_def) -apply (blast) -done +lemma comp_inj_on_iff: "inj_on f A \ inj_on f' (f ` A) \ inj_on (f' \ f) A" + by (auto simp add: comp_inj_on inj_on_def) -lemma comp_inj_on_iff: - "inj_on f A \ inj_on f' (f ` A) \ inj_on (f' o f) A" -by(auto simp add: comp_inj_on inj_on_def) - -lemma inj_on_imageI2: - "inj_on (f' o f) A \ inj_on f A" -by(auto simp add: comp_inj_on inj_on_def) +lemma inj_on_imageI2: "inj_on (f' \ f) A \ inj_on f A" + by (auto simp add: comp_inj_on inj_on_def) lemma inj_img_insertE: assumes "inj_on f A" - assumes "x \ B" and "insert x B = f ` A" - obtains x' A' where "x' \ A'" and "A = insert x' A'" - and "x = f x'" and "B = f ` A'" + assumes "x \ B" + and "insert x B = f ` A" + obtains x' A' where "x' \ A'" and "A = insert x' A'" and "x = f x'" and "B = f ` A'" proof - from assms have "x \ f ` A" by auto then obtain x' where *: "x' \ A" "x = f x'" by auto - then have "A = insert x' (A - {x'})" by auto - with assms * have "B = f ` (A - {x'})" - by (auto dest: inj_on_contraD) + then have A: "A = insert x' (A - {x'})" by auto + with assms * have B: "B = f ` (A - {x'})" by (auto dest: inj_on_contraD) have "x' \ A - {x'}" by simp - from \x' \ A - {x'}\ \A = insert x' (A - {x'})\ \x = f x'\ \B = image f (A - {x'})\ - show ?thesis .. + from this A \x = f x'\ B show ?thesis .. qed lemma linorder_injI: - assumes hyp: "\x y. x < (y::'a::linorder) \ f x \ f y" + assumes hyp: "\x y::'a::linorder. x < y \ f x \ f y" shows "inj f" \ \Courtesy of Stephan Merz\ proof (rule inj_onI) @@ -307,7 +277,9 @@ lemma surj_def: "surj f \ (\y. \x. y = f x)" by auto -lemma surjI: assumes *: "\ x. g (f x) = x" shows "surj g" +lemma surjI: + assumes *: "\ x. g (f x) = x" + shows "surj g" using *[symmetric] by auto lemma surjD: "surj f \ \x. y = f x" @@ -316,15 +288,17 @@ lemma surjE: "surj f \ (\x. y = f x \ C) \ C" by (simp add: surj_def, blast) -lemma comp_surj: "[| surj f; surj g |] ==> surj (g o f)" -apply (simp add: comp_def surj_def, clarify) -apply (drule_tac x = y in spec, clarify) -apply (drule_tac x = x in spec, blast) -done +lemma comp_surj: "surj f \ surj g \ surj (g \ f)" + apply (simp add: comp_def surj_def) + apply clarify + apply (drule_tac x = y in spec) + apply clarify + apply (drule_tac x = x in spec) + apply blast + done -lemma bij_betw_imageI: - "\ inj_on f A; f ` A = B \ \ bij_betw f A B" -unfolding bij_betw_def by clarify +lemma bij_betw_imageI: "inj_on f A \ f ` A = B \ bij_betw f A B" + unfolding bij_betw_def by clarify lemma bij_betw_imp_surj_on: "bij_betw f A B \ f ` A = B" unfolding bij_betw_def by clarify @@ -332,122 +306,119 @@ lemma bij_betw_imp_surj: "bij_betw f A UNIV \ surj f" unfolding bij_betw_def by auto -lemma bij_betw_empty1: - assumes "bij_betw f {} A" - shows "A = {}" -using assms unfolding bij_betw_def by blast +lemma bij_betw_empty1: "bij_betw f {} A \ A = {}" + unfolding bij_betw_def by blast -lemma bij_betw_empty2: - assumes "bij_betw f A {}" - shows "A = {}" -using assms unfolding bij_betw_def by blast +lemma bij_betw_empty2: "bij_betw f A {} \ A = {}" + unfolding bij_betw_def by blast -lemma inj_on_imp_bij_betw: - "inj_on f A \ bij_betw f A (f ` A)" -unfolding bij_betw_def by simp +lemma inj_on_imp_bij_betw: "inj_on f A \ bij_betw f A (f ` A)" + unfolding bij_betw_def by simp lemma bij_def: "bij f \ inj f \ surj f" unfolding bij_betw_def .. -lemma bijI: "[| inj f; surj f |] ==> bij f" -by (simp add: bij_def) +lemma bijI: "inj f \ surj f \ bij f" + by (simp add: bij_def) -lemma bij_is_inj: "bij f ==> inj f" -by (simp add: bij_def) +lemma bij_is_inj: "bij f \ inj f" + by (simp add: bij_def) -lemma bij_is_surj: "bij f ==> surj f" -by (simp add: bij_def) +lemma bij_is_surj: "bij f \ surj f" + by (simp add: bij_def) lemma bij_betw_imp_inj_on: "bij_betw f A B \ inj_on f A" -by (simp add: bij_betw_def) + by (simp add: bij_betw_def) -lemma bij_betw_trans: - "bij_betw f A B \ bij_betw g B C \ bij_betw (g o f) A C" -by(auto simp add:bij_betw_def comp_inj_on) +lemma bij_betw_trans: "bij_betw f A B \ bij_betw g B C \ bij_betw (g \ f) A C" + by (auto simp add:bij_betw_def comp_inj_on) -lemma bij_comp: "bij f \ bij g \ bij (g o f)" +lemma bij_comp: "bij f \ bij g \ bij (g \ f)" by (rule bij_betw_trans) -lemma bij_betw_comp_iff: - "bij_betw f A A' \ bij_betw f' A' A'' \ bij_betw (f' o f) A A''" -by(auto simp add: bij_betw_def inj_on_def) +lemma bij_betw_comp_iff: "bij_betw f A A' \ bij_betw f' A' A'' \ bij_betw (f' \ f) A A''" + by (auto simp add: bij_betw_def inj_on_def) lemma bij_betw_comp_iff2: - assumes BIJ: "bij_betw f' A' A''" and IM: "f ` A \ A'" - shows "bij_betw f A A' \ bij_betw (f' o f) A A''" -using assms -proof(auto simp add: bij_betw_comp_iff) + assumes bij: "bij_betw f' A' A''" + and img: "f ` A \ A'" + shows "bij_betw f A A' \ bij_betw (f' \ f) A A''" + using assms +proof (auto simp add: bij_betw_comp_iff) assume *: "bij_betw (f' \ f) A A''" - thus "bij_betw f A A'" - using IM - proof(auto simp add: bij_betw_def) + then show "bij_betw f A A'" + using img + proof (auto simp add: bij_betw_def) assume "inj_on (f' \ f) A" - thus "inj_on f A" using inj_on_imageI2 by blast + then show "inj_on f A" using inj_on_imageI2 by blast next - fix a' assume **: "a' \ A'" - hence "f' a' \ A''" using BIJ unfolding bij_betw_def by auto - then obtain a where 1: "a \ A \ f'(f a) = f' a'" using * - unfolding bij_betw_def by force - hence "f a \ A'" using IM by auto - hence "f a = a'" using BIJ ** 1 unfolding bij_betw_def inj_on_def by auto - thus "a' \ f ` A" using 1 by auto + fix a' + assume **: "a' \ A'" + then have "f' a' \ A''" using bij unfolding bij_betw_def by auto + then obtain a where 1: "a \ A \ f'(f a) = f' a'" + using * unfolding bij_betw_def by force + then have "f a \ A'" using img by auto + then have "f a = a'" + using bij ** 1 unfolding bij_betw_def inj_on_def by auto + then show "a' \ f ` A" + using 1 by auto qed qed -lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A" +lemma bij_betw_inv: + assumes "bij_betw f A B" + shows "\g. bij_betw g B A" proof - have i: "inj_on f A" and s: "f ` A = B" - using assms by(auto simp:bij_betw_def) - let ?P = "%b a. a:A \ f a = b" let ?g = "%b. The (?P b)" - { fix a b assume P: "?P b a" - hence ex1: "\a. ?P b a" using s by blast - hence uex1: "\!a. ?P b a" by(blast dest:inj_onD[OF i]) - hence " ?g b = a" using the1_equality[OF uex1, OF P] P by simp - } note g = this + using assms by (auto simp: bij_betw_def) + let ?P = "\b a. a \ A \ f a = b" + let ?g = "\b. The (?P b)" + have g: "?g b = a" if P: "?P b a" for a b + proof - + from that have ex1: "\a. ?P b a" using s by blast + then have uex1: "\!a. ?P b a" by (blast dest:inj_onD[OF i]) + then show ?thesis using the1_equality[OF uex1, OF P] P by simp + qed have "inj_on ?g B" - proof(rule inj_onI) - fix x y assume "x:B" "y:B" "?g x = ?g y" - from s \x:B\ obtain a1 where a1: "?P x a1" by blast - from s \y:B\ obtain a2 where a2: "?P y a2" by blast - from g[OF a1] a1 g[OF a2] a2 \?g x = ?g y\ show "x=y" by simp + proof (rule inj_onI) + fix x y + assume "x \ B" "y \ B" "?g x = ?g y" + from s \x \ B\ obtain a1 where a1: "?P x a1" by blast + from s \y \ B\ obtain a2 where a2: "?P y a2" by blast + from g [OF a1] a1 g [OF a2] a2 \?g x = ?g y\ show "x = y" by simp qed moreover have "?g ` B = A" - proof(auto simp: image_def) - fix b assume "b:B" + proof (auto simp: image_def) + fix b + assume "b \ B" with s obtain a where P: "?P b a" by blast - thus "?g b \ A" using g[OF P] by auto + then show "?g b \ A" using g[OF P] by auto next - fix a assume "a:A" + fix a + assume "a \ A" then obtain b where P: "?P b a" using s by blast - then have "b:B" using s by blast + then have "b \ B" using s by blast with g[OF P] show "\b\B. a = ?g b" by blast qed - ultimately show ?thesis by(auto simp:bij_betw_def) + ultimately show ?thesis by (auto simp: bij_betw_def) qed -lemma bij_betw_cong: - "(\ a. a \ A \ f a = g a) \ bij_betw f A A' = bij_betw g A A'" -unfolding bij_betw_def inj_on_def by force +lemma bij_betw_cong: "(\ a. a \ A \ f a = g a) \ bij_betw f A A' = bij_betw g A A'" + unfolding bij_betw_def inj_on_def by force -lemma bij_betw_id[intro, simp]: - "bij_betw id A A" -unfolding bij_betw_def id_def by auto +lemma bij_betw_id[intro, simp]: "bij_betw id A A" + unfolding bij_betw_def id_def by auto -lemma bij_betw_id_iff: - "bij_betw id A B \ A = B" -by(auto simp add: bij_betw_def) +lemma bij_betw_id_iff: "bij_betw id A B \ A = B" + by (auto simp add: bij_betw_def) lemma bij_betw_combine: assumes "bij_betw f A B" "bij_betw f C D" "B \ D = {}" shows "bij_betw f (A \ C) (B \ D)" using assms unfolding bij_betw_def inj_on_Un image_Un by auto -lemma bij_betw_subset: - assumes BIJ: "bij_betw f A A'" and - SUB: "B \ A" and IM: "f ` B = B'" - shows "bij_betw f B B'" -using assms -by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def) +lemma bij_betw_subset: "bij_betw f A A' \ B \ A \ f ` B = B' \ bij_betw f B B'" + by (auto simp add: bij_betw_def inj_on_def) lemma bij_pointE: assumes "bij f" @@ -460,85 +431,77 @@ with that show thesis by blast qed -lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A" -by simp +lemma surj_image_vimage_eq: "surj f \ f ` (f -` A) = A" + by simp lemma surj_vimage_empty: - assumes "surj f" shows "f -` A = {} \ A = {}" - using surj_image_vimage_eq[OF \surj f\, of A] + assumes "surj f" + shows "f -` A = {} \ A = {}" + using surj_image_vimage_eq [OF \surj f\, of A] by (intro iffI) fastforce+ -lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A" -by (simp add: inj_on_def, blast) +lemma inj_vimage_image_eq: "inj f \ f -` (f ` A) = A" + unfolding inj_on_def by blast -lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A" -by (blast intro: sym) +lemma vimage_subsetD: "surj f \ f -` B \ A \ B \ f ` A" + by (blast intro: sym) -lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A" -by (unfold inj_on_def, blast) +lemma vimage_subsetI: "inj f \ B \ f ` A \ f -` B \ A" + unfolding inj_on_def by blast -lemma vimage_subset_eq: "bij f ==> (f -` B <= A) = (B <= f ` A)" -apply (unfold bij_def) -apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD) -done +lemma vimage_subset_eq: "bij f \ f -` B \ A \ B \ f ` A" + unfolding bij_def by (blast del: subsetI intro: vimage_subsetI vimage_subsetD) -lemma inj_on_image_eq_iff: "\ inj_on f C; A \ C; B \ C \ \ f ` A = f ` B \ A = B" -by(fastforce simp add: inj_on_def) +lemma inj_on_image_eq_iff: "inj_on f C \ A \ C \ B \ C \ f ` A = f ` B \ A = B" + by (fastforce simp add: inj_on_def) lemma inj_on_Un_image_eq_iff: "inj_on f (A \ B) \ f ` A = f ` B \ A = B" -by(erule inj_on_image_eq_iff) simp_all + by (erule inj_on_image_eq_iff) simp_all -lemma inj_on_image_Int: - "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B" - by (simp add: inj_on_def, blast) +lemma inj_on_image_Int: "inj_on f C \ A \ C \ B \ C \ f ` (A \ B) = f ` A \ f ` B" + unfolding inj_on_def by blast + +lemma inj_on_image_set_diff: "inj_on f C \ A - B \ C \ B \ C \ f ` (A - B) = f ` A - f ` B" + unfolding inj_on_def by blast -lemma inj_on_image_set_diff: - "[| inj_on f C; A-B \ C; B \ C |] ==> f`(A-B) = f`A - f`B" - by (simp add: inj_on_def, blast) +lemma image_Int: "inj f \ f ` (A \ B) = f ` A \ f ` B" + unfolding inj_on_def by blast -lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B" - by (simp add: inj_on_def, blast) +lemma image_set_diff: "inj f \ f ` (A - B) = f ` A - f ` B" + unfolding inj_on_def by blast -lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B" -by (simp add: inj_on_def, blast) - -lemma inj_on_image_mem_iff: "\inj_on f B; a \ B; A \ B\ \ f a \ f`A \ a \ A" +lemma inj_on_image_mem_iff: "inj_on f B \ a \ B \ A \ B \ f a \ f ` A \ a \ A" by (auto simp: inj_on_def) (*FIXME DELETE*) -lemma inj_on_image_mem_iff_alt: "inj_on f B \ A \ B \ f a \ f`A \ a \ B \ a \ A" +lemma inj_on_image_mem_iff_alt: "inj_on f B \ A \ B \ f a \ f ` A \ a \ B \ a \ A" by (blast dest: inj_onD) -lemma inj_image_mem_iff: "inj f \ f a \ f`A \ a \ A" +lemma inj_image_mem_iff: "inj f \ f a \ f ` A \ a \ A" by (blast dest: injD) -lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)" +lemma inj_image_subset_iff: "inj f \ f ` A \ f ` B \ A \ B" by (blast dest: injD) -lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)" +lemma inj_image_eq_iff: "inj f \ f ` A = f ` B \ A = B" by (blast dest: injD) -lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)" -by auto - -lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)" -by (auto simp add: inj_on_def) +lemma surj_Compl_image_subset: "surj f \ - (f ` A) \ f ` (- A)" + by auto -lemma bij_image_Compl_eq: "bij f ==> f`(-A) = -(f`A)" -apply (simp add: bij_def) -apply (rule equalityI) -apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset) -done +lemma inj_image_Compl_subset: "inj f \ f ` (- A) \ - (f ` A)" + by (auto simp add: inj_on_def) + +lemma bij_image_Compl_eq: "bij f \ f ` (- A) = - (f ` A)" + by (simp add: bij_def inj_image_Compl_subset surj_Compl_image_subset equalityI) lemma inj_vimage_singleton: "inj f \ f -` {a} \ {THE x. f x = a}" - \ \The inverse image of a singleton under an injective function - is included in a singleton.\ + \ \The inverse image of a singleton under an injective function is included in a singleton.\ apply (auto simp add: inj_on_def) apply (blast intro: the_equality [symmetric]) done -lemma inj_on_vimage_singleton: - "inj_on f A \ f -` {a} \ A \ {THE x. x \ A \ f x = a}" +lemma inj_on_vimage_singleton: "inj_on f A \ f -` {a} \ A \ {THE x. x \ A \ f x = a}" by (auto simp add: inj_on_def intro: the_equality [symmetric]) lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A" @@ -548,84 +511,92 @@ by (auto intro!: inj_onI dest: strict_mono_eq) lemma bij_betw_byWitness: -assumes LEFT: "\a \ A. f'(f a) = a" and - RIGHT: "\a' \ A'. f(f' a') = a'" and - IM1: "f ` A \ A'" and IM2: "f' ` A' \ A" -shows "bij_betw f A A'" -using assms -proof(unfold bij_betw_def inj_on_def, safe) - fix a b assume *: "a \ A" "b \ A" and **: "f a = f b" - have "a = f'(f a) \ b = f'(f b)" using * LEFT by simp + assumes left: "\a \ A. f' (f a) = a" + and right: "\a' \ A'. f (f' a') = a'" + and "f ` A \ A'" + and img2: "f' ` A' \ A" + shows "bij_betw f A A'" + using assms +proof (unfold bij_betw_def inj_on_def, safe) + fix a b + assume *: "a \ A" "b \ A" and **: "f a = f b" + have "a = f' (f a) \ b = f'(f b)" using * left by simp with ** show "a = b" by simp next fix a' assume *: "a' \ A'" - hence "f' a' \ A" using IM2 by blast + hence "f' a' \ A" using img2 by blast moreover - have "a' = f(f' a')" using * RIGHT by simp + have "a' = f (f' a')" using * right by simp ultimately show "a' \ f ` A" by blast qed corollary notIn_Un_bij_betw: -assumes NIN: "b \ A" and NIN': "f b \ A'" and - BIJ: "bij_betw f A A'" -shows "bij_betw f (A \ {b}) (A' \ {f b})" -proof- + assumes "b \ A" + and "f b \ A'" + and "bij_betw f A A'" + shows "bij_betw f (A \ {b}) (A' \ {f b})" +proof - have "bij_betw f {b} {f b}" - unfolding bij_betw_def inj_on_def by simp + unfolding bij_betw_def inj_on_def by simp with assms show ?thesis - using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast + using bij_betw_combine[of f A A' "{b}" "{f b}"] by blast qed lemma notIn_Un_bij_betw3: -assumes NIN: "b \ A" and NIN': "f b \ A'" -shows "bij_betw f A A' = bij_betw f (A \ {b}) (A' \ {f b})" + assumes "b \ A" + and "f b \ A'" + shows "bij_betw f A A' = bij_betw f (A \ {b}) (A' \ {f b})" proof assume "bij_betw f A A'" - thus "bij_betw f (A \ {b}) (A' \ {f b})" - using assms notIn_Un_bij_betw[of b A f A'] by blast + then show "bij_betw f (A \ {b}) (A' \ {f b})" + using assms notIn_Un_bij_betw [of b A f A'] by blast next assume *: "bij_betw f (A \ {b}) (A' \ {f b})" have "f ` A = A'" - proof(auto) - fix a assume **: "a \ A" - hence "f a \ A' \ {f b}" using * unfolding bij_betw_def by blast + proof auto + fix a + assume **: "a \ A" + then have "f a \ A' \ {f b}" + using * unfolding bij_betw_def by blast moreover - {assume "f a = f b" - hence "a = b" using * ** unfolding bij_betw_def inj_on_def by blast - with NIN ** have False by blast - } + have False if "f a = f b" + proof - + have "a = b" using * ** that unfolding bij_betw_def inj_on_def by blast + with \b \ A\ ** show ?thesis by blast + qed ultimately show "f a \ A'" by blast next - fix a' assume **: "a' \ A'" - hence "a' \ f`(A \ {b})" - using * by (auto simp add: bij_betw_def) + fix a' + assume **: "a' \ A'" + then have "a' \ f ` (A \ {b})" + using * by (auto simp add: bij_betw_def) then obtain a where 1: "a \ A \ {b} \ f a = a'" by blast moreover - {assume "a = b" with 1 ** NIN' have False by blast - } + have False if "a = b" using 1 ** \f b \ A'\ that by blast ultimately have "a \ A" by blast with 1 show "a' \ f ` A" by blast qed - thus "bij_betw f A A'" using * bij_betw_subset[of f "A \ {b}" _ A] by blast + then show "bij_betw f A A'" + using * bij_betw_subset[of f "A \ {b}" _ A] by blast qed -subsection\Function Updating\ +subsection \Function Updating\ -definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where - "fun_upd f a b == % x. if x=a then b else f x" +definition fun_upd :: "('a \ 'b) \ 'a \ 'b \ ('a \ 'b)" + where "fun_upd f a b = (\x. if x = a then b else f x)" nonterminal updbinds and updbind syntax - "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)") - "" :: "updbind => updbinds" ("_") - "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _") - "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000, 0] 900) + "_updbind" :: "'a \ 'a \ updbind" ("(2_ :=/ _)") + "" :: "updbind \ updbinds" ("_") + "_updbinds":: "updbind \ updbinds \ updbinds" ("_,/ _") + "_Update" :: "'a \ updbinds \ 'a" ("_/'((_)')" [1000, 0] 900) translations - "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" - "f(x:=y)" == "CONST fun_upd f x y" + "_Update f (_updbinds b bs)" \ "_Update (_Update f b) bs" + "f(x:=y)" \ "CONST fun_upd f x y" (* Hint: to define the sum of two functions (or maps), use case_sum. A nice infix syntax could be defined by @@ -633,69 +604,69 @@ case_sum (infixr "'(+')"80) *) -lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)" -apply (simp add: fun_upd_def, safe) -apply (erule subst) -apply (rule_tac [2] ext, auto) -done +lemma fun_upd_idem_iff: "f(x:=y) = f \ f x = y" + unfolding fun_upd_def + apply safe + apply (erule subst) + apply (rule_tac [2] ext) + apply auto + done -lemma fun_upd_idem: "f x = y ==> f(x:=y) = f" +lemma fun_upd_idem: "f x = y \ f(x := y) = f" by (simp only: fun_upd_idem_iff) lemma fun_upd_triv [iff]: "f(x := f x) = f" by (simp only: fun_upd_idem) -lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)" -by (simp add: fun_upd_def) +lemma fun_upd_apply [simp]: "(f(x := y)) z = (if z = x then y else f z)" + by (simp add: fun_upd_def) -(* fun_upd_apply supersedes these two, but they are useful +(* fun_upd_apply supersedes these two, but they are useful if fun_upd_apply is intentionally removed from the simpset *) -lemma fun_upd_same: "(f(x:=y)) x = y" -by simp +lemma fun_upd_same: "(f(x := y)) x = y" + by simp -lemma fun_upd_other: "z~=x ==> (f(x:=y)) z = f z" -by simp - -lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)" -by (simp add: fun_eq_iff) +lemma fun_upd_other: "z \ x \ (f(x := y)) z = f z" + by simp -lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)" -by (rule ext, auto) +lemma fun_upd_upd [simp]: "f(x := y, x := z) = f(x := z)" + by (simp add: fun_eq_iff) -lemma inj_on_fun_updI: - "inj_on f A \ y \ f ` A \ inj_on (f(x := y)) A" +lemma fun_upd_twist: "a \ c \ (m(a := b))(c := d) = (m(c := d))(a := b)" + by (rule ext) auto + +lemma inj_on_fun_updI: "inj_on f A \ y \ f ` A \ inj_on (f(x := y)) A" by (fastforce simp: inj_on_def) -lemma fun_upd_image: - "f(x:=y) ` A = (if x \ A then insert y (f ` (A-{x})) else f ` A)" -by auto +lemma fun_upd_image: "f(x := y) ` A = (if x \ A then insert y (f ` (A - {x})) else f ` A)" + by auto lemma fun_upd_comp: "f \ (g(x := y)) = (f \ g)(x := f y)" by auto lemma fun_upd_eqD: "f(x := y) = g(x := z) \ y = z" -by(simp add: fun_eq_iff split: if_split_asm) + by (simp add: fun_eq_iff split: if_split_asm) + subsection \\override_on\\ -definition override_on :: "('a \ 'b) \ ('a \ 'b) \ 'a set \ 'a \ 'b" where - "override_on f g A = (\a. if a \ A then g a else f a)" +definition override_on :: "('a \ 'b) \ ('a \ 'b) \ 'a set \ 'a \ 'b" + where "override_on f g A = (\a. if a \ A then g a else f a)" lemma override_on_emptyset[simp]: "override_on f g {} = f" -by(simp add:override_on_def) + by (simp add:override_on_def) -lemma override_on_apply_notin[simp]: "a ~: A ==> (override_on f g A) a = f a" -by(simp add:override_on_def) +lemma override_on_apply_notin[simp]: "a \ A \ (override_on f g A) a = f a" + by (simp add:override_on_def) -lemma override_on_apply_in[simp]: "a : A ==> (override_on f g A) a = g a" -by(simp add:override_on_def) +lemma override_on_apply_in[simp]: "a \ A \ (override_on f g A) a = g a" + by (simp add:override_on_def) subsection \\swap\\ definition swap :: "'a \ 'a \ ('a \ 'b) \ ('a \ 'b)" -where - "swap a b f = f (a := f b, b:= f a)" + where "swap a b f = f (a := f b, b:= f a)" lemma swap_apply [simp]: "swap a b f a = f b" @@ -703,20 +674,16 @@ "c \ a \ c \ b \ swap a b f c = f c" by (simp_all add: swap_def) -lemma swap_self [simp]: - "swap a a f = f" +lemma swap_self [simp]: "swap a a f = f" by (simp add: swap_def) -lemma swap_commute: - "swap a b f = swap b a f" +lemma swap_commute: "swap a b f = swap b a f" by (simp add: fun_upd_def swap_def fun_eq_iff) -lemma swap_nilpotent [simp]: - "swap a b (swap a b f) = f" +lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f" by (rule ext, simp add: fun_upd_def swap_def) -lemma swap_comp_involutory [simp]: - "swap a b \ swap a b = id" +lemma swap_comp_involutory [simp]: "swap a b \ swap a b = id" by (rule ext) simp lemma swap_triple: @@ -725,10 +692,11 @@ using assms by (simp add: fun_eq_iff swap_def) lemma comp_swap: "f \ swap a b g = swap a b (f \ g)" - by (rule ext, simp add: fun_upd_def swap_def) + by (rule ext) (simp add: fun_upd_def swap_def) lemma swap_image_eq [simp]: - assumes "a \ A" "b \ A" shows "swap a b f ` A = f ` A" + assumes "a \ A" "b \ A" + shows "swap a b f ` A = f ` A" proof - have subset: "\f. swap a b f ` A \ f ` A" using assms by (auto simp: image_iff swap_def) @@ -736,20 +704,21 @@ with subset[of f] show ?thesis by auto qed -lemma inj_on_imp_inj_on_swap: - "\inj_on f A; a \ A; b \ A\ \ inj_on (swap a b f) A" - by (simp add: inj_on_def swap_def, blast) +lemma inj_on_imp_inj_on_swap: "inj_on f A \ a \ A \ b \ A \ inj_on (swap a b f) A" + by (auto simp add: inj_on_def swap_def) lemma inj_on_swap_iff [simp]: - assumes A: "a \ A" "b \ A" shows "inj_on (swap a b f) A \ inj_on f A" + assumes A: "a \ A" "b \ A" + shows "inj_on (swap a b f) A \ inj_on f A" proof assume "inj_on (swap a b f) A" with A have "inj_on (swap a b (swap a b f)) A" by (iprover intro: inj_on_imp_inj_on_swap) - thus "inj_on f A" by simp + then show "inj_on f A" by simp next assume "inj_on f A" - with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap) + with A show "inj_on (swap a b f) A" + by (iprover intro: inj_on_imp_inj_on_swap) qed lemma surj_imp_surj_swap: "surj f \ surj (swap a b f)" @@ -758,8 +727,7 @@ lemma surj_swap_iff [simp]: "surj (swap a b f) \ surj f" by simp -lemma bij_betw_swap_iff [simp]: - "\ x \ A; y \ A \ \ bij_betw (swap x y f) A B \ bij_betw f A B" +lemma bij_betw_swap_iff [simp]: "x \ A \ y \ A \ bij_betw (swap x y f) A B \ bij_betw f A B" by (auto simp: bij_betw_def) lemma bij_swap_iff [simp]: "bij (swap a b f) \ bij f" @@ -770,114 +738,107 @@ subsection \Inversion of injective functions\ -definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where - "the_inv_into A f == %x. THE y. y : A & f y = x" +definition the_inv_into :: "'a set \ ('a \ 'b) \ ('b \ 'a)" + where "the_inv_into A f = (\x. THE y. y \ A \ f y = x)" + +lemma the_inv_into_f_f: "inj_on f A \ x \ A \ the_inv_into A f (f x) = x" + unfolding the_inv_into_def inj_on_def by blast -lemma the_inv_into_f_f: - "[| inj_on f A; x : A |] ==> the_inv_into A f (f x) = x" -apply (simp add: the_inv_into_def inj_on_def) -apply blast -done - -lemma f_the_inv_into_f: - "inj_on f A ==> y : f`A ==> f (the_inv_into A f y) = y" -apply (simp add: the_inv_into_def) -apply (rule the1I2) - apply(blast dest: inj_onD) -apply blast -done +lemma f_the_inv_into_f: "inj_on f A \ y \ f ` A \ f (the_inv_into A f y) = y" + apply (simp add: the_inv_into_def) + apply (rule the1I2) + apply(blast dest: inj_onD) + apply blast + done -lemma the_inv_into_into: - "[| inj_on f A; x : f ` A; A <= B |] ==> the_inv_into A f x : B" -apply (simp add: the_inv_into_def) -apply (rule the1I2) - apply(blast dest: inj_onD) -apply blast -done +lemma the_inv_into_into: "inj_on f A \ x \ f ` A \ A \ B \ the_inv_into A f x \ B" + apply (simp add: the_inv_into_def) + apply (rule the1I2) + apply(blast dest: inj_onD) + apply blast + done -lemma the_inv_into_onto[simp]: - "inj_on f A ==> the_inv_into A f ` (f ` A) = A" -by (fast intro:the_inv_into_into the_inv_into_f_f[symmetric]) +lemma the_inv_into_onto [simp]: "inj_on f A \ the_inv_into A f ` (f ` A) = A" + by (fast intro: the_inv_into_into the_inv_into_f_f [symmetric]) -lemma the_inv_into_f_eq: - "[| inj_on f A; f x = y; x : A |] ==> the_inv_into A f y = x" +lemma the_inv_into_f_eq: "inj_on f A \ f x = y \ x \ A \ the_inv_into A f y = x" apply (erule subst) - apply (erule the_inv_into_f_f, assumption) + apply (erule the_inv_into_f_f) + apply assumption done lemma the_inv_into_comp: - "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==> - the_inv_into A (f o g) x = (the_inv_into A g o the_inv_into (g ` A) f) x" -apply (rule the_inv_into_f_eq) - apply (fast intro: comp_inj_on) - apply (simp add: f_the_inv_into_f the_inv_into_into) -apply (simp add: the_inv_into_into) -done + "inj_on f (g ` A) \ inj_on g A \ x \ f ` g ` A \ + the_inv_into A (f \ g) x = (the_inv_into A g \ the_inv_into (g ` A) f) x" + apply (rule the_inv_into_f_eq) + apply (fast intro: comp_inj_on) + apply (simp add: f_the_inv_into_f the_inv_into_into) + apply (simp add: the_inv_into_into) + done -lemma inj_on_the_inv_into: - "inj_on f A \ inj_on (the_inv_into A f) (f ` A)" -by (auto intro: inj_onI simp: the_inv_into_f_f) +lemma inj_on_the_inv_into: "inj_on f A \ inj_on (the_inv_into A f) (f ` A)" + by (auto intro: inj_onI simp: the_inv_into_f_f) -lemma bij_betw_the_inv_into: - "bij_betw f A B \ bij_betw (the_inv_into A f) B A" -by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into) +lemma bij_betw_the_inv_into: "bij_betw f A B \ bij_betw (the_inv_into A f) B A" + by (auto simp add: bij_betw_def inj_on_the_inv_into the_inv_into_into) -abbreviation the_inv :: "('a \ 'b) \ ('b \ 'a)" where - "the_inv f \ the_inv_into UNIV f" +abbreviation the_inv :: "('a \ 'b) \ ('b \ 'a)" + where "the_inv f \ the_inv_into UNIV f" lemma the_inv_f_f: assumes "inj f" - shows "the_inv f (f x) = x" using assms UNIV_I - by (rule the_inv_into_f_f) + shows "the_inv f (f x) = x" + using assms UNIV_I by (rule the_inv_into_f_f) subsection \Cantor's Paradox\ -lemma Cantors_paradox: - "\(\f. f ` A = Pow A)" -proof clarify - fix f assume "f ` A = Pow A" hence *: "Pow A \ f ` A" by blast +theorem Cantors_paradox: "\f. f ` A = Pow A" +proof + assume "\f. f ` A = Pow A" + then obtain f where f: "f ` A = Pow A" .. let ?X = "{a \ A. a \ f a}" - have "?X \ Pow A" unfolding Pow_def by auto - with * obtain x where "x \ A \ f x = ?X" by blast - thus False by best + have "?X \ Pow A" by blast + then have "?X \ f ` A" by (simp only: f) + then obtain x where "x \ A" and "f x = ?X" by blast + then show False by blast qed + subsection \Setup\ subsubsection \Proof tools\ -text \simplifies terms of the form - f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\ +text \Simplify terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...)\ simproc_setup fun_upd2 ("f(v := w, x := y)") = \fn _ => -let - fun gen_fun_upd NONE T _ _ = NONE - | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y) - fun dest_fun_T1 (Type (_, T :: Ts)) = T - fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) = - let - fun find (Const (@{const_name fun_upd},T) $ g $ v $ w) = - if v aconv x then SOME g else gen_fun_upd (find g) T v w - | find t = NONE - in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end + let + fun gen_fun_upd NONE T _ _ = NONE + | gen_fun_upd (SOME f) T x y = SOME (Const (@{const_name fun_upd}, T) $ f $ x $ y) + fun dest_fun_T1 (Type (_, T :: Ts)) = T + fun find_double (t as Const (@{const_name fun_upd},T) $ f $ x $ y) = + let + fun find (Const (@{const_name fun_upd},T) $ g $ v $ w) = + if v aconv x then SOME g else gen_fun_upd (find g) T v w + | find t = NONE + in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end - val ss = simpset_of @{context} + val ss = simpset_of @{context} - fun proc ctxt ct = - let - val t = Thm.term_of ct - in - case find_double t of - (T, NONE) => NONE - | (T, SOME rhs) => - SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs)) - (fn _ => - resolve_tac ctxt [eq_reflection] 1 THEN - resolve_tac ctxt @{thms ext} 1 THEN - simp_tac (put_simpset ss ctxt) 1)) - end -in proc end + fun proc ctxt ct = + let + val t = Thm.term_of ct + in + case find_double t of + (T, NONE) => NONE + | (T, SOME rhs) => + SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs)) + (fn _ => + resolve_tac ctxt [eq_reflection] 1 THEN + resolve_tac ctxt @{thms ext} 1 THEN + simp_tac (put_simpset ss ctxt) 1)) + end + in proc end \ @@ -891,6 +852,7 @@ functor vimage by (simp_all add: fun_eq_iff vimage_comp) + text \Legacy theorem names\ lemmas o_def = comp_def @@ -904,4 +866,3 @@ lemmas o_eq_id_dest = comp_eq_id_dest end - diff -r 0c89eef79701 -r 83a91a73fcb5 src/HOL/Groups.thy --- a/src/HOL/Groups.thy Mon Jun 20 10:51:34 2016 +0200 +++ b/src/HOL/Groups.thy Mon Jun 20 22:31:16 2016 +0200 @@ -13,22 +13,26 @@ named_theorems ac_simps "associativity and commutativity simplification rules" -text\The rewrites accumulated in \algebra_simps\ deal with the -classical algebraic structures of groups, rings and family. They simplify -terms by multiplying everything out (in case of a ring) and bringing sums and -products into a canonical form (by ordered rewriting). As a result it decides -group and ring equalities but also helps with inequalities. +text \ + The rewrites accumulated in \algebra_simps\ deal with the + classical algebraic structures of groups, rings and family. They simplify + terms by multiplying everything out (in case of a ring) and bringing sums and + products into a canonical form (by ordered rewriting). As a result it decides + group and ring equalities but also helps with inequalities. -Of course it also works for fields, but it knows nothing about multiplicative -inverses or division. This is catered for by \field_simps\.\ + Of course it also works for fields, but it knows nothing about multiplicative + inverses or division. This is catered for by \field_simps\. +\ named_theorems algebra_simps "algebra simplification rules" -text\Lemmas \field_simps\ multiply with denominators in (in)equations -if they can be proved to be non-zero (for equations) or positive/negative -(for inequations). Can be too aggressive and is therefore separate from the -more benign \algebra_simps\.\ +text \ + Lemmas \field_simps\ multiply with denominators in (in)equations + if they can be proved to be non-zero (for equations) or positive/negative + (for inequations). Can be too aggressive and is therefore separate from the + more benign \algebra_simps\. +\ named_theorems field_simps "algebra simplification rules for fields" @@ -42,15 +46,14 @@ \ locale semigroup = - fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) + fixes f :: "'a \ 'a \ 'a" (infixl "\<^bold>*" 70) assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)" locale abel_semigroup = semigroup + assumes commute [ac_simps]: "a \<^bold>* b = b \<^bold>* a" begin -lemma left_commute [ac_simps]: - "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)" +lemma left_commute [ac_simps]: "b \<^bold>* (a \<^bold>* c) = a \<^bold>* (b \<^bold>* c)" proof - have "(b \<^bold>* a) \<^bold>* c = (a \<^bold>* b) \<^bold>* c" by (simp only: commute) @@ -238,13 +241,11 @@ assumes add_right_imp_eq: "b + a = c + a \ b = c" begin -lemma add_left_cancel [simp]: - "a + b = a + c \ b = c" -by (blast dest: add_left_imp_eq) +lemma add_left_cancel [simp]: "a + b = a + c \ b = c" + by (blast dest: add_left_imp_eq) -lemma add_right_cancel [simp]: - "b + a = c + a \ b = c" -by (blast dest: add_right_imp_eq) +lemma add_right_cancel [simp]: "b + a = c + a \ b = c" + by (blast dest: add_right_imp_eq) end @@ -253,8 +254,7 @@ assumes diff_diff_add [algebra_simps, field_simps]: "a - b - c = a - (b + c)" begin -lemma add_diff_cancel_right' [simp]: - "(a + b) - b = a" +lemma add_diff_cancel_right' [simp]: "(a + b) - b = a" using add_diff_cancel_left' [of b a] by (simp add: ac_simps) subclass cancel_semigroup_add @@ -274,16 +274,13 @@ by simp qed -lemma add_diff_cancel_left [simp]: - "(c + a) - (c + b) = a - b" +lemma add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b" unfolding diff_diff_add [symmetric] by simp -lemma add_diff_cancel_right [simp]: - "(a + c) - (b + c) = a - b" +lemma add_diff_cancel_right [simp]: "(a + c) - (b + c) = a - b" using add_diff_cancel_left [symmetric] by (simp add: ac_simps) -lemma diff_right_commute: - "a - c - b = a - b - c" +lemma diff_right_commute: "a - c - b = a - b - c" by (simp add: diff_diff_add add.commute) end @@ -291,14 +288,13 @@ class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add begin -lemma diff_zero [simp]: - "a - 0 = a" +lemma diff_zero [simp]: "a - 0 = a" using add_diff_cancel_right' [of a 0] by simp -lemma diff_cancel [simp]: - "a - a = 0" +lemma diff_cancel [simp]: "a - a = 0" proof - - have "(a + 0) - (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero) + have "(a + 0) - (a + 0) = 0" + by (simp only: add_diff_cancel_left diff_zero) then show ?thesis by simp qed @@ -306,29 +302,29 @@ assumes "c + b = a" shows "c = a - b" proof - - from assms have "(b + c) - (b + 0) = a - b" by (simp add: add.commute) + from assms have "(b + c) - (b + 0) = a - b" + by (simp add: add.commute) then show "c = a - b" by simp qed -lemma add_cancel_right_right [simp]: - "a = a + b \ b = 0" (is "?P \ ?Q") +lemma add_cancel_right_right [simp]: "a = a + b \ b = 0" + (is "?P \ ?Q") proof - assume ?Q then show ?P by simp + assume ?Q + then show ?P by simp next - assume ?P then have "a - a = a + b - a" by simp + assume ?P + then have "a - a = a + b - a" by simp then show ?Q by simp qed -lemma add_cancel_right_left [simp]: - "a = b + a \ b = 0" +lemma add_cancel_right_left [simp]: "a = b + a \ b = 0" using add_cancel_right_right [of a b] by (simp add: ac_simps) -lemma add_cancel_left_right [simp]: - "a + b = a \ b = 0" +lemma add_cancel_left_right [simp]: "a + b = a \ b = 0" by (auto dest: sym) -lemma add_cancel_left_left [simp]: - "b + a = a \ b = 0" +lemma add_cancel_left_left [simp]: "b + a = a \ b = 0" by (auto dest: sym) end @@ -337,11 +333,12 @@ assumes zero_diff [simp]: "0 - a = 0" begin -lemma diff_add_zero [simp]: - "a - (a + b) = 0" +lemma diff_add_zero [simp]: "a - (a + b) = 0" proof - - have "a - (a + b) = (a + 0) - (a + b)" by simp - also have "\ = 0" by (simp only: add_diff_cancel_left zero_diff) + have "a - (a + b) = (a + 0) - (a + b)" + by simp + also have "\ = 0" + by (simp only: add_diff_cancel_left zero_diff) finally show ?thesis . qed @@ -355,14 +352,14 @@ assumes add_uminus_conv_diff [simp]: "a + (- b) = a - b" begin -lemma diff_conv_add_uminus: - "a - b = a + (- b)" +lemma diff_conv_add_uminus: "a - b = a + (- b)" by simp lemma minus_unique: - assumes "a + b = 0" shows "- a = b" + assumes "a + b = 0" + shows "- a = b" proof - - have "- a = - a + (a + b)" using assms by simp + from assms have "- a = - a + (a + b)" by simp also have "\ = b" by (simp add: add.assoc [symmetric]) finally show ?thesis . qed @@ -370,13 +367,13 @@ lemma minus_zero [simp]: "- 0 = 0" proof - have "0 + 0 = 0" by (rule add_0_right) - thus "- 0 = 0" by (rule minus_unique) + then show "- 0 = 0" by (rule minus_unique) qed lemma minus_minus [simp]: "- (- a) = a" proof - have "- a + a = 0" by (rule left_minus) - thus "- (- a) = a" by (rule minus_unique) + then show "- (- a) = a" by (rule minus_unique) qed lemma right_minus: "a + - a = 0" @@ -386,8 +383,7 @@ finally show ?thesis . qed -lemma diff_self [simp]: - "a - a = 0" +lemma diff_self [simp]: "a - a = 0" using right_minus [of a] by simp subclass cancel_semigroup_add @@ -404,24 +400,19 @@ then show "b = c" unfolding add.assoc by simp qed -lemma minus_add_cancel [simp]: - "- a + (a + b) = b" +lemma minus_add_cancel [simp]: "- a + (a + b) = b" by (simp add: add.assoc [symmetric]) -lemma add_minus_cancel [simp]: - "a + (- a + b) = b" +lemma add_minus_cancel [simp]: "a + (- a + b) = b" by (simp add: add.assoc [symmetric]) -lemma diff_add_cancel [simp]: - "a - b + b = a" +lemma diff_add_cancel [simp]: "a - b + b = a" by (simp only: diff_conv_add_uminus add.assoc) simp -lemma add_diff_cancel [simp]: - "a + b - b = a" +lemma add_diff_cancel [simp]: "a + b - b = a" by (simp only: diff_conv_add_uminus add.assoc) simp -lemma minus_add: - "- (a + b) = - b + - a" +lemma minus_add: "- (a + b) = - b + - a" proof - have "(a + b) + (- b + - a) = 0" by (simp only: add.assoc add_minus_cancel) simp @@ -429,117 +420,103 @@ by (rule minus_unique) qed -lemma right_minus_eq [simp]: - "a - b = 0 \ a = b" +lemma right_minus_eq [simp]: "a - b = 0 \ a = b" proof assume "a - b = 0" have "a = (a - b) + b" by (simp add: add.assoc) also have "\ = b" using \a - b = 0\ by simp finally show "a = b" . next - assume "a = b" thus "a - b = 0" by simp + assume "a = b" + then show "a - b = 0" by simp qed -lemma eq_iff_diff_eq_0: - "a = b \ a - b = 0" +lemma eq_iff_diff_eq_0: "a = b \ a - b = 0" by (fact right_minus_eq [symmetric]) -lemma diff_0 [simp]: - "0 - a = - a" +lemma diff_0 [simp]: "0 - a = - a" by (simp only: diff_conv_add_uminus add_0_left) -lemma diff_0_right [simp]: - "a - 0 = a" +lemma diff_0_right [simp]: "a - 0 = a" by (simp only: diff_conv_add_uminus minus_zero add_0_right) -lemma diff_minus_eq_add [simp]: - "a - - b = a + b" +lemma diff_minus_eq_add [simp]: "a - - b = a + b" by (simp only: diff_conv_add_uminus minus_minus) -lemma neg_equal_iff_equal [simp]: - "- a = - b \ a = b" +lemma neg_equal_iff_equal [simp]: "- a = - b \ a = b" proof assume "- a = - b" - hence "- (- a) = - (- b)" by simp - thus "a = b" by simp + then have "- (- a) = - (- b)" by simp + then show "a = b" by simp next assume "a = b" - thus "- a = - b" by simp + then show "- a = - b" by simp qed -lemma neg_equal_0_iff_equal [simp]: - "- a = 0 \ a = 0" +lemma neg_equal_0_iff_equal [simp]: "- a = 0 \ a = 0" by (subst neg_equal_iff_equal [symmetric]) simp -lemma neg_0_equal_iff_equal [simp]: - "0 = - a \ 0 = a" +lemma neg_0_equal_iff_equal [simp]: "0 = - a \ 0 = a" by (subst neg_equal_iff_equal [symmetric]) simp -text\The next two equations can make the simplifier loop!\ +text \The next two equations can make the simplifier loop!\ -lemma equation_minus_iff: - "a = - b \ b = - a" +lemma equation_minus_iff: "a = - b \ b = - a" proof - - have "- (- a) = - b \ - a = b" by (rule neg_equal_iff_equal) - thus ?thesis by (simp add: eq_commute) + have "- (- a) = - b \ - a = b" + by (rule neg_equal_iff_equal) + then show ?thesis + by (simp add: eq_commute) qed -lemma minus_equation_iff: - "- a = b \ - b = a" +lemma minus_equation_iff: "- a = b \ - b = a" proof - - have "- a = - (- b) \ a = -b" by (rule neg_equal_iff_equal) - thus ?thesis by (simp add: eq_commute) + have "- a = - (- b) \ a = -b" + by (rule neg_equal_iff_equal) + then show ?thesis + by (simp add: eq_commute) qed -lemma eq_neg_iff_add_eq_0: - "a = - b \ a + b = 0" +lemma eq_neg_iff_add_eq_0: "a = - b \ a + b = 0" proof - assume "a = - b" then show "a + b = 0" by simp + assume "a = - b" + then show "a + b = 0" by simp next assume "a + b = 0" moreover have "a + (b + - b) = (a + b) + - b" by (simp only: add.assoc) - ultimately show "a = - b" by simp + ultimately show "a = - b" + by simp qed -lemma add_eq_0_iff2: - "a + b = 0 \ a = - b" +lemma add_eq_0_iff2: "a + b = 0 \ a = - b" by (fact eq_neg_iff_add_eq_0 [symmetric]) -lemma neg_eq_iff_add_eq_0: - "- a = b \ a + b = 0" +lemma neg_eq_iff_add_eq_0: "- a = b \ a + b = 0" by (auto simp add: add_eq_0_iff2) -lemma add_eq_0_iff: - "a + b = 0 \ b = - a" +lemma add_eq_0_iff: "a + b = 0 \ b = - a" by (auto simp add: neg_eq_iff_add_eq_0 [symmetric]) -lemma minus_diff_eq [simp]: - "- (a - b) = b - a" +lemma minus_diff_eq [simp]: "- (a - b) = b - a" by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add.assoc minus_add_cancel) simp -lemma add_diff_eq [algebra_simps, field_simps]: - "a + (b - c) = (a + b) - c" +lemma add_diff_eq [algebra_simps, field_simps]: "a + (b - c) = (a + b) - c" by (simp only: diff_conv_add_uminus add.assoc) -lemma diff_add_eq_diff_diff_swap: - "a - (b + c) = a - c - b" +lemma diff_add_eq_diff_diff_swap: "a - (b + c) = a - c - b" by (simp only: diff_conv_add_uminus add.assoc minus_add) -lemma diff_eq_eq [algebra_simps, field_simps]: - "a - b = c \ a = c + b" +lemma diff_eq_eq [algebra_simps, field_simps]: "a - b = c \ a = c + b" by auto -lemma eq_diff_eq [algebra_simps, field_simps]: - "a = c - b \ a + b = c" +lemma eq_diff_eq [algebra_simps, field_simps]: "a = c - b \ a + b = c" by auto -lemma diff_diff_eq2 [algebra_simps, field_simps]: - "a - (b - c) = (a + c) - b" +lemma diff_diff_eq2 [algebra_simps, field_simps]: "a - (b - c) = (a + c) - b" by (simp only: diff_conv_add_uminus add.assoc) simp -lemma diff_eq_diff_eq: - "a - b = c - d \ a = b \ c = d" +lemma diff_eq_diff_eq: "a - b = c - d \ a = b \ c = d" by (simp only: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d]) end @@ -550,7 +527,7 @@ begin subclass group_add - proof qed (simp_all add: ab_left_minus ab_diff_conv_add_uminus) + by standard (simp_all add: ab_left_minus ab_diff_conv_add_uminus) subclass cancel_comm_monoid_add proof @@ -563,16 +540,13 @@ by (simp add: algebra_simps) qed -lemma uminus_add_conv_diff [simp]: - "- a + b = b - a" +lemma uminus_add_conv_diff [simp]: "- a + b = b - a" by (simp add: add.commute) -lemma minus_add_distrib [simp]: - "- (a + b) = - a + - b" +lemma minus_add_distrib [simp]: "- (a + b) = - a + - b" by (simp add: algebra_simps) -lemma diff_add_eq [algebra_simps, field_simps]: - "(a - b) + c = (a + c) - b" +lemma diff_add_eq [algebra_simps, field_simps]: "(a - b) + c = (a + c) - b" by (simp add: algebra_simps) end @@ -582,35 +556,31 @@ text \ The theory of partially ordered groups is taken from the books: - \begin{itemize} - \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 - \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 - \end{itemize} + + \<^item> \<^emph>\Lattice Theory\ by Garret Birkhoff, American Mathematical Society, 1979 + \<^item> \<^emph>\Partially Ordered Algebraic Systems\, Pergamon Press, 1963 + Most of the used notions can also be looked up in - \begin{itemize} - \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al. - \item \emph{Algebra I} by van der Waerden, Springer. - \end{itemize} + \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al. + \<^item> \<^emph>\Algebra I\ by van der Waerden, Springer \ class ordered_ab_semigroup_add = order + ab_semigroup_add + assumes add_left_mono: "a \ b \ c + a \ c + b" begin -lemma add_right_mono: - "a \ b \ a + c \ b + c" -by (simp add: add.commute [of _ c] add_left_mono) +lemma add_right_mono: "a \ b \ a + c \ b + c" + by (simp add: add.commute [of _ c] add_left_mono) text \non-strict, in both arguments\ -lemma add_mono: - "a \ b \ c \ d \ a + c \ b + d" +lemma add_mono: "a \ b \ c \ d \ a + c \ b + d" apply (erule add_right_mono [THEN order_trans]) apply (simp add: add.commute add_left_mono) done end -text\Strict monotonicity in both arguments\ +text \Strict monotonicity in both arguments\ class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add + assumes add_strict_mono: "a < b \ c < d \ a + c < b + d" @@ -618,13 +588,11 @@ ordered_ab_semigroup_add + cancel_ab_semigroup_add begin -lemma add_strict_left_mono: - "a < b \ c + a < c + b" -by (auto simp add: less_le add_left_mono) +lemma add_strict_left_mono: "a < b \ c + a < c + b" + by (auto simp add: less_le add_left_mono) -lemma add_strict_right_mono: - "a < b \ a + c < b + c" -by (simp add: add.commute [of _ c] add_strict_left_mono) +lemma add_strict_right_mono: "a < b \ a + c < b + c" + by (simp add: add.commute [of _ c] add_strict_left_mono) subclass strict_ordered_ab_semigroup_add apply standard @@ -632,17 +600,15 @@ apply (erule add_strict_left_mono) done -lemma add_less_le_mono: - "a < b \ c \ d \ a + c < b + d" -apply (erule add_strict_right_mono [THEN less_le_trans]) -apply (erule add_left_mono) -done +lemma add_less_le_mono: "a < b \ c \ d \ a + c < b + d" + apply (erule add_strict_right_mono [THEN less_le_trans]) + apply (erule add_left_mono) + done -lemma add_le_less_mono: - "a \ b \ c < d \ a + c < b + d" -apply (erule add_right_mono [THEN le_less_trans]) -apply (erule add_strict_left_mono) -done +lemma add_le_less_mono: "a \ b \ c < d \ a + c < b + d" + apply (erule add_right_mono [THEN le_less_trans]) + apply (erule add_strict_left_mono) + done end @@ -651,63 +617,60 @@ begin lemma add_less_imp_less_left: - assumes less: "c + a < c + b" shows "a < b" + assumes less: "c + a < c + b" + shows "a < b" proof - - from less have le: "c + a <= c + b" by (simp add: order_le_less) - have "a <= b" + from less have le: "c + a \ c + b" + by (simp add: order_le_less) + have "a \ b" apply (insert le) apply (drule add_le_imp_le_left) - by (insert le, drule add_le_imp_le_left, assumption) + apply (insert le) + apply (drule add_le_imp_le_left) + apply assumption + done moreover have "a \ b" proof (rule ccontr) - assume "~(a \ b)" + assume "\ ?thesis" then have "a = b" by simp then have "c + a = c + b" by simp - with less show "False"by simp + with less show "False" by simp qed - ultimately show "a < b" by (simp add: order_le_less) + ultimately show "a < b" + by (simp add: order_le_less) qed -lemma add_less_imp_less_right: - "a + c < b + c \ a < b" -apply (rule add_less_imp_less_left [of c]) -apply (simp add: add.commute) -done +lemma add_less_imp_less_right: "a + c < b + c \ a < b" + by (rule add_less_imp_less_left [of c]) (simp add: add.commute) -lemma add_less_cancel_left [simp]: - "c + a < c + b \ a < b" +lemma add_less_cancel_left [simp]: "c + a < c + b \ a < b" by (blast intro: add_less_imp_less_left add_strict_left_mono) -lemma add_less_cancel_right [simp]: - "a + c < b + c \ a < b" +lemma add_less_cancel_right [simp]: "a + c < b + c \ a < b" by (blast intro: add_less_imp_less_right add_strict_right_mono) -lemma add_le_cancel_left [simp]: - "c + a \ c + b \ a \ b" - by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) +lemma add_le_cancel_left [simp]: "c + a \ c + b \ a \ b" + apply auto + apply (drule add_le_imp_le_left) + apply (simp_all add: add_left_mono) + done -lemma add_le_cancel_right [simp]: - "a + c \ b + c \ a \ b" +lemma add_le_cancel_right [simp]: "a + c \ b + c \ a \ b" by (simp add: add.commute [of a c] add.commute [of b c]) -lemma add_le_imp_le_right: - "a + c \ b + c \ a \ b" -by simp +lemma add_le_imp_le_right: "a + c \ b + c \ a \ b" + by simp -lemma max_add_distrib_left: - "max x y + z = max (x + z) (y + z)" +lemma max_add_distrib_left: "max x y + z = max (x + z) (y + z)" unfolding max_def by auto -lemma min_add_distrib_left: - "min x y + z = min (x + z) (y + z)" +lemma min_add_distrib_left: "min x y + z = min (x + z) (y + z)" unfolding min_def by auto -lemma max_add_distrib_right: - "x + max y z = max (x + y) (x + z)" +lemma max_add_distrib_right: "x + max y z = max (x + y) (x + z)" unfolding max_def by auto -lemma min_add_distrib_right: - "x + min y z = min (x + y) (x + z)" +lemma min_add_distrib_right: "x + min y z = min (x + y) (x + z)" unfolding min_def by auto end @@ -717,36 +680,28 @@ class ordered_comm_monoid_add = comm_monoid_add + ordered_ab_semigroup_add begin -lemma add_nonneg_nonneg [simp]: - "0 \ a \ 0 \ b \ 0 \ a + b" +lemma add_nonneg_nonneg [simp]: "0 \ a \ 0 \ b \ 0 \ a + b" using add_mono[of 0 a 0 b] by simp -lemma add_nonpos_nonpos: - "a \ 0 \ b \ 0 \ a + b \ 0" +lemma add_nonpos_nonpos: "a \ 0 \ b \ 0 \ a + b \ 0" using add_mono[of a 0 b 0] by simp -lemma add_nonneg_eq_0_iff: - "0 \ x \ 0 \ y \ x + y = 0 \ x = 0 \ y = 0" +lemma add_nonneg_eq_0_iff: "0 \ x \ 0 \ y \ x + y = 0 \ x = 0 \ y = 0" using add_left_mono[of 0 y x] add_right_mono[of 0 x y] by auto -lemma add_nonpos_eq_0_iff: - "x \ 0 \ y \ 0 \ x + y = 0 \ x = 0 \ y = 0" +lemma add_nonpos_eq_0_iff: "x \ 0 \ y \ 0 \ x + y = 0 \ x = 0 \ y = 0" using add_left_mono[of y 0 x] add_right_mono[of x 0 y] by auto -lemma add_increasing: - "0 \ a \ b \ c \ b \ a + c" - by (insert add_mono [of 0 a b c], simp) +lemma add_increasing: "0 \ a \ b \ c \ b \ a + c" + using add_mono [of 0 a b c] by simp -lemma add_increasing2: - "0 \ c \ b \ a \ b \ a + c" +lemma add_increasing2: "0 \ c \ b \ a \ b \ a + c" by (simp add: add_increasing add.commute [of a]) -lemma add_decreasing: - "a \ 0 \ c \ b \ a + c \ b" - using add_mono[of a 0 c b] by simp +lemma add_decreasing: "a \ 0 \ c \ b \ a + c \ b" + using add_mono [of a 0 c b] by simp -lemma add_decreasing2: - "c \ 0 \ a \ b \ a + c \ b" +lemma add_decreasing2: "c \ 0 \ a \ b \ a + c \ b" using add_mono[of a b c 0] by simp lemma add_pos_nonneg: "0 < a \ 0 \ b \ 0 < a + b" @@ -776,8 +731,7 @@ class strict_ordered_comm_monoid_add = comm_monoid_add + strict_ordered_ab_semigroup_add begin -lemma pos_add_strict: - shows "0 < a \ b < c \ b < a + c" +lemma pos_add_strict: "0 < a \ b < c \ b < a + c" using add_strict_mono [of 0 a b c] by simp end @@ -788,13 +742,11 @@ subclass ordered_cancel_ab_semigroup_add .. subclass strict_ordered_comm_monoid_add .. -lemma add_strict_increasing: - "0 < a \ b \ c \ b < a + c" - by (insert add_less_le_mono [of 0 a b c], simp) +lemma add_strict_increasing: "0 < a \ b \ c \ b < a + c" + using add_less_le_mono [of 0 a b c] by simp -lemma add_strict_increasing2: - "0 \ a \ b < c \ b < a + c" - by (insert add_le_less_mono [of 0 a b c], simp) +lemma add_strict_increasing2: "0 \ a \ b < c \ b < a + c" + using add_le_less_mono [of 0 a b c] by simp end @@ -807,105 +759,108 @@ proof fix a b c :: 'a assume "c + a \ c + b" - hence "(-c) + (c + a) \ (-c) + (c + b)" by (rule add_left_mono) - hence "((-c) + c) + a \ ((-c) + c) + b" by (simp only: add.assoc) - thus "a \ b" by simp + then have "(-c) + (c + a) \ (-c) + (c + b)" + by (rule add_left_mono) + then have "((-c) + c) + a \ ((-c) + c) + b" + by (simp only: add.assoc) + then show "a \ b" by simp qed subclass ordered_cancel_comm_monoid_add .. -lemma add_less_same_cancel1 [simp]: - "b + a < b \ a < 0" +lemma add_less_same_cancel1 [simp]: "b + a < b \ a < 0" using add_less_cancel_left [of _ _ 0] by simp -lemma add_less_same_cancel2 [simp]: - "a + b < b \ a < 0" +lemma add_less_same_cancel2 [simp]: "a + b < b \ a < 0" using add_less_cancel_right [of _ _ 0] by simp -lemma less_add_same_cancel1 [simp]: - "a < a + b \ 0 < b" +lemma less_add_same_cancel1 [simp]: "a < a + b \ 0 < b" using add_less_cancel_left [of _ 0] by simp -lemma less_add_same_cancel2 [simp]: - "a < b + a \ 0 < b" +lemma less_add_same_cancel2 [simp]: "a < b + a \ 0 < b" using add_less_cancel_right [of 0] by simp -lemma add_le_same_cancel1 [simp]: - "b + a \ b \ a \ 0" +lemma add_le_same_cancel1 [simp]: "b + a \ b \ a \ 0" using add_le_cancel_left [of _ _ 0] by simp -lemma add_le_same_cancel2 [simp]: - "a + b \ b \ a \ 0" +lemma add_le_same_cancel2 [simp]: "a + b \ b \ a \ 0" using add_le_cancel_right [of _ _ 0] by simp -lemma le_add_same_cancel1 [simp]: - "a \ a + b \ 0 \ b" +lemma le_add_same_cancel1 [simp]: "a \ a + b \ 0 \ b" using add_le_cancel_left [of _ 0] by simp -lemma le_add_same_cancel2 [simp]: - "a \ b + a \ 0 \ b" +lemma le_add_same_cancel2 [simp]: "a \ b + a \ 0 \ b" using add_le_cancel_right [of 0] by simp -lemma max_diff_distrib_left: - shows "max x y - z = max (x - z) (y - z)" +lemma max_diff_distrib_left: "max x y - z = max (x - z) (y - z)" using max_add_distrib_left [of x y "- z"] by simp -lemma min_diff_distrib_left: - shows "min x y - z = min (x - z) (y - z)" +lemma min_diff_distrib_left: "min x y - z = min (x - z) (y - z)" using min_add_distrib_left [of x y "- z"] by simp lemma le_imp_neg_le: - assumes "a \ b" shows "-b \ -a" + assumes "a \ b" + shows "- b \ - a" proof - - have "-a+a \ -a+b" using \a \ b\ by (rule add_left_mono) - then have "0 \ -a+b" by simp - then have "0 + (-b) \ (-a + b) + (-b)" by (rule add_right_mono) - then show ?thesis by (simp add: algebra_simps) + from assms have "- a + a \ - a + b" + by (rule add_left_mono) + then have "0 \ - a + b" + by simp + then have "0 + (- b) \ (- a + b) + (- b)" + by (rule add_right_mono) + then show ?thesis + by (simp add: algebra_simps) qed lemma neg_le_iff_le [simp]: "- b \ - a \ a \ b" proof assume "- b \ - a" - hence "- (- a) \ - (- b)" by (rule le_imp_neg_le) - thus "a\b" by simp + then have "- (- a) \ - (- b)" + by (rule le_imp_neg_le) + then show "a \ b" + by simp next - assume "a\b" - thus "-b \ -a" by (rule le_imp_neg_le) + assume "a \ b" + then show "- b \ - a" + by (rule le_imp_neg_le) qed lemma neg_le_0_iff_le [simp]: "- a \ 0 \ 0 \ a" -by (subst neg_le_iff_le [symmetric], simp) + by (subst neg_le_iff_le [symmetric]) simp lemma neg_0_le_iff_le [simp]: "0 \ - a \ a \ 0" -by (subst neg_le_iff_le [symmetric], simp) + by (subst neg_le_iff_le [symmetric]) simp lemma neg_less_iff_less [simp]: "- b < - a \ a < b" -by (force simp add: less_le) + by (auto simp add: less_le) lemma neg_less_0_iff_less [simp]: "- a < 0 \ 0 < a" -by (subst neg_less_iff_less [symmetric], simp) + by (subst neg_less_iff_less [symmetric]) simp lemma neg_0_less_iff_less [simp]: "0 < - a \ a < 0" -by (subst neg_less_iff_less [symmetric], simp) + by (subst neg_less_iff_less [symmetric]) simp -text\The next several equations can make the simplifier loop!\ +text \The next several equations can make the simplifier loop!\ lemma less_minus_iff: "a < - b \ b < - a" proof - - have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less) - thus ?thesis by simp + have "- (-a) < - b \ b < - a" + by (rule neg_less_iff_less) + then show ?thesis by simp qed lemma minus_less_iff: "- a < b \ - b < a" proof - - have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less) - thus ?thesis by simp + have "- a < - (- b) \ - b < a" + by (rule neg_less_iff_less) + then show ?thesis by simp qed lemma le_minus_iff: "a \ - b \ b \ - a" proof - - have mm: "!! a (b::'a). (-(-a)) < -b \ -(-b) < -a" by (simp only: minus_less_iff) - have "(- (- a) <= -b) = (b <= - a)" + have mm: "- (- a) < -b \ - (- b) < -a" for a b :: 'a + by (simp only: minus_less_iff) + have "- (- a) \ -b \ b \ - a" apply (auto simp only: le_less) apply (drule mm) apply (simp_all) @@ -915,60 +870,52 @@ qed lemma minus_le_iff: "- a \ b \ - b \ a" -by (auto simp add: le_less minus_less_iff) + by (auto simp add: le_less minus_less_iff) -lemma diff_less_0_iff_less [simp]: - "a - b < 0 \ a < b" +lemma diff_less_0_iff_less [simp]: "a - b < 0 \ a < b" proof - - have "a - b < 0 \ a + (- b) < b + (- b)" by simp - also have "... \ a < b" by (simp only: add_less_cancel_right) + have "a - b < 0 \ a + (- b) < b + (- b)" + by simp + also have "\ \ a < b" + by (simp only: add_less_cancel_right) finally show ?thesis . qed lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric] -lemma diff_less_eq [algebra_simps, field_simps]: - "a - b < c \ a < c + b" -apply (subst less_iff_diff_less_0 [of a]) -apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) -apply (simp add: algebra_simps) -done +lemma diff_less_eq [algebra_simps, field_simps]: "a - b < c \ a < c + b" + apply (subst less_iff_diff_less_0 [of a]) + apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) + apply (simp add: algebra_simps) + done -lemma less_diff_eq[algebra_simps, field_simps]: - "a < c - b \ a + b < c" -apply (subst less_iff_diff_less_0 [of "a + b"]) -apply (subst less_iff_diff_less_0 [of a]) -apply (simp add: algebra_simps) -done +lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \ a + b < c" + apply (subst less_iff_diff_less_0 [of "a + b"]) + apply (subst less_iff_diff_less_0 [of a]) + apply (simp add: algebra_simps) + done -lemma diff_gt_0_iff_gt [simp]: - "a - b > 0 \ a > b" +lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \ a > b" by (simp add: less_diff_eq) -lemma diff_le_eq [algebra_simps, field_simps]: - "a - b \ c \ a \ c + b" +lemma diff_le_eq [algebra_simps, field_simps]: "a - b \ c \ a \ c + b" by (auto simp add: le_less diff_less_eq ) -lemma le_diff_eq [algebra_simps, field_simps]: - "a \ c - b \ a + b \ c" +lemma le_diff_eq [algebra_simps, field_simps]: "a \ c - b \ a + b \ c" by (auto simp add: le_less less_diff_eq) -lemma diff_le_0_iff_le [simp]: - "a - b \ 0 \ a \ b" +lemma diff_le_0_iff_le [simp]: "a - b \ 0 \ a \ b" by (simp add: algebra_simps) lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric] -lemma diff_ge_0_iff_ge [simp]: - "a - b \ 0 \ a \ b" +lemma diff_ge_0_iff_ge [simp]: "a - b \ 0 \ a \ b" by (simp add: le_diff_eq) -lemma diff_eq_diff_less: - "a - b = c - d \ a < b \ c < d" +lemma diff_eq_diff_less: "a - b = c - d \ a < b \ c < d" by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d]) -lemma diff_eq_diff_less_eq: - "a - b = c - d \ a \ b \ c \ d" +lemma diff_eq_diff_less_eq: "a - b = c - d \ a \ b \ c \ d" by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d]) lemma diff_mono: "a \ b \ d \ c \ a - c \ b - d" @@ -1020,18 +967,18 @@ subclass ordered_ab_semigroup_add_imp_le proof fix a b c :: 'a - assume le: "c + a <= c + b" - show "a <= b" + assume le1: "c + a \ c + b" + show "a \ b" proof (rule ccontr) - assume w: "~ a \ b" - hence "b <= a" by (simp add: linorder_not_le) - hence le2: "c + b <= c + a" by (rule add_left_mono) + assume *: "\ ?thesis" + then have "b \ a" by (simp add: linorder_not_le) + then have le2: "c + b \ c + a" by (rule add_left_mono) have "a = b" - apply (insert le) - apply (insert le2) - apply (drule antisym, simp_all) + apply (insert le1 le2) + apply (drule antisym) + apply simp_all done - with w show False + with * show False by (simp add: linorder_not_le [symmetric]) qed qed @@ -1043,72 +990,71 @@ subclass linordered_cancel_ab_semigroup_add .. -lemma equal_neg_zero [simp]: - "a = - a \ a = 0" +lemma equal_neg_zero [simp]: "a = - a \ a = 0" proof - assume "a = 0" then show "a = - a" by simp + assume "a = 0" + then show "a = - a" by simp next - assume A: "a = - a" show "a = 0" + assume A: "a = - a" + show "a = 0" proof (cases "0 \ a") - case True with A have "0 \ - a" by auto + case True + with A have "0 \ - a" by auto with le_minus_iff have "a \ 0" by simp with True show ?thesis by (auto intro: order_trans) next - case False then have B: "a \ 0" by auto + case False + then have B: "a \ 0" by auto with A have "- a \ 0" by auto with B show ?thesis by (auto intro: order_trans) qed qed -lemma neg_equal_zero [simp]: - "- a = a \ a = 0" +lemma neg_equal_zero [simp]: "- a = a \ a = 0" by (auto dest: sym) -lemma neg_less_eq_nonneg [simp]: - "- a \ a \ 0 \ a" +lemma neg_less_eq_nonneg [simp]: "- a \ a \ 0 \ a" proof - assume A: "- a \ a" show "0 \ a" + assume *: "- a \ a" + show "0 \ a" proof (rule classical) - assume "\ 0 \ a" + assume "\ ?thesis" then have "a < 0" by auto - with A have "- a < 0" by (rule le_less_trans) + with * have "- a < 0" by (rule le_less_trans) then show ?thesis by auto qed next - assume A: "0 \ a" show "- a \ a" - proof (rule order_trans) - show "- a \ 0" using A by (simp add: minus_le_iff) - next - show "0 \ a" using A . - qed + assume *: "0 \ a" + then have "- a \ 0" by (simp add: minus_le_iff) + from this * show "- a \ a" by (rule order_trans) qed -lemma neg_less_pos [simp]: - "- a < a \ 0 < a" +lemma neg_less_pos [simp]: "- a < a \ 0 < a" by (auto simp add: less_le) -lemma less_eq_neg_nonpos [simp]: - "a \ - a \ a \ 0" +lemma less_eq_neg_nonpos [simp]: "a \ - a \ a \ 0" using neg_less_eq_nonneg [of "- a"] by simp -lemma less_neg_neg [simp]: - "a < - a \ a < 0" +lemma less_neg_neg [simp]: "a < - a \ a < 0" using neg_less_pos [of "- a"] by simp -lemma double_zero [simp]: - "a + a = 0 \ a = 0" +lemma double_zero [simp]: "a + a = 0 \ a = 0" proof - assume assm: "a + a = 0" + assume "a + a = 0" then have a: "- a = a" by (rule minus_unique) then show "a = 0" by (simp only: neg_equal_zero) -qed simp +next + assume "a = 0" + then show "a + a = 0" by simp +qed -lemma double_zero_sym [simp]: - "0 = a + a \ a = 0" - by (rule, drule sym) simp_all +lemma double_zero_sym [simp]: "0 = a + a \ a = 0" + apply (rule iffI) + apply (drule sym) + apply simp_all + done -lemma zero_less_double_add_iff_zero_less_single_add [simp]: - "0 < a + a \ 0 < a" +lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \ 0 < a" proof assume "0 < a + a" then have "0 - a < a" by (simp only: diff_less_eq) @@ -1121,32 +1067,27 @@ then show "0 < a + a" by simp qed -lemma zero_le_double_add_iff_zero_le_single_add [simp]: - "0 \ a + a \ 0 \ a" +lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \ a + a \ 0 \ a" by (auto simp add: le_less) -lemma double_add_less_zero_iff_single_add_less_zero [simp]: - "a + a < 0 \ a < 0" +lemma double_add_less_zero_iff_single_add_less_zero [simp]: "a + a < 0 \ a < 0" proof - have "\ a + a < 0 \ \ a < 0" by (simp add: not_less) then show ?thesis by simp qed -lemma double_add_le_zero_iff_single_add_le_zero [simp]: - "a + a \ 0 \ a \ 0" +lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \ 0 \ a \ 0" proof - have "\ a + a \ 0 \ \ a \ 0" by (simp add: not_le) then show ?thesis by simp qed -lemma minus_max_eq_min: - "- max x y = min (-x) (-y)" +lemma minus_max_eq_min: "- max x y = min (- x) (- y)" by (auto simp add: max_def min_def) -lemma minus_min_eq_max: - "- min x y = max (-x) (-y)" +lemma minus_min_eq_max: "- min x y = max (- x) (- y)" by (auto simp add: max_def min_def) end @@ -1181,16 +1122,17 @@ unfolding neg_le_0_iff_le by simp lemma abs_of_nonneg [simp]: - assumes nonneg: "0 \ a" shows "\a\ = a" + assumes nonneg: "0 \ a" + shows "\a\ = a" proof (rule antisym) + show "a \ \a\" by (rule abs_ge_self) from nonneg le_imp_neg_le have "- a \ 0" by simp from this nonneg have "- a \ a" by (rule order_trans) then show "\a\ \ a" by (auto intro: abs_leI) -qed (rule abs_ge_self) +qed lemma abs_idempotent [simp]: "\\a\\ = \a\" -by (rule antisym) - (auto intro!: abs_ge_self abs_leI order_trans [of "- \a\" 0 "\a\"]) + by (rule antisym) (auto intro!: abs_ge_self abs_leI order_trans [of "- \a\" 0 "\a\"]) lemma abs_eq_0 [simp]: "\a\ = 0 \ a = 0" proof - @@ -1206,27 +1148,27 @@ qed lemma abs_zero [simp]: "\0\ = 0" -by simp + by simp lemma abs_0_eq [simp]: "0 = \a\ \ a = 0" proof - have "0 = \a\ \ \a\ = 0" by (simp only: eq_ac) - thus ?thesis by simp + then show ?thesis by simp qed lemma abs_le_zero_iff [simp]: "\a\ \ 0 \ a = 0" proof assume "\a\ \ 0" then have "\a\ = 0" by (rule antisym) simp - thus "a = 0" by simp + then show "a = 0" by simp next assume "a = 0" - thus "\a\ \ 0" by simp + then show "\a\ \ 0" by simp qed lemma abs_le_self_iff [simp]: "\a\ \ a \ 0 \ a" proof - - have "\a. (0::'a) \ \a\" + have "0 \ \a\" using abs_ge_zero by blast then have "\a\ \ a \ 0 \ a" using order.trans by blast @@ -1235,12 +1177,12 @@ qed lemma zero_less_abs_iff [simp]: "0 < \a\ \ a \ 0" -by (simp add: less_le) + by (simp add: less_le) lemma abs_not_less_zero [simp]: "\ \a\ < 0" proof - - have a: "\x y. x \ y \ \ y < x" by auto - show ?thesis by (simp add: a) + have "x \ y \ \ y < x" for x y by auto + then show ?thesis by simp qed lemma abs_ge_minus_self: "- a \ \a\" @@ -1249,39 +1191,40 @@ then show ?thesis by simp qed -lemma abs_minus_commute: - "\a - b\ = \b - a\" +lemma abs_minus_commute: "\a - b\ = \b - a\" proof - - have "\a - b\ = \- (a - b)\" by (simp only: abs_minus_cancel) - also have "... = \b - a\" by simp + have "\a - b\ = \- (a - b)\" + by (simp only: abs_minus_cancel) + also have "\ = \b - a\" by simp finally show ?thesis . qed lemma abs_of_pos: "0 < a \ \a\ = a" -by (rule abs_of_nonneg, rule less_imp_le) + by (rule abs_of_nonneg) (rule less_imp_le) lemma abs_of_nonpos [simp]: - assumes "a \ 0" shows "\a\ = - a" + assumes "a \ 0" + shows "\a\ = - a" proof - let ?b = "- a" have "- ?b \ 0 \ \- ?b\ = - (- ?b)" - unfolding abs_minus_cancel [of "?b"] - unfolding neg_le_0_iff_le [of "?b"] - unfolding minus_minus by (erule abs_of_nonneg) + unfolding abs_minus_cancel [of ?b] + unfolding neg_le_0_iff_le [of ?b] + unfolding minus_minus by (erule abs_of_nonneg) then show ?thesis using assms by auto qed lemma abs_of_neg: "a < 0 \ \a\ = - a" -by (rule abs_of_nonpos, rule less_imp_le) + by (rule abs_of_nonpos) (rule less_imp_le) lemma abs_le_D1: "\a\ \ b \ a \ b" -by (insert abs_ge_self, blast intro: order_trans) + using abs_ge_self by (blast intro: order_trans) lemma abs_le_D2: "\a\ \ b \ - a \ b" -by (insert abs_le_D1 [of "- a"], simp) + using abs_le_D1 [of "- a"] by simp lemma abs_le_iff: "\a\ \ b \ a \ b \ - a \ b" -by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) + by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) lemma abs_triangle_ineq2: "\a\ - \b\ \ \a - b\" proof - @@ -1301,24 +1244,27 @@ lemma abs_triangle_ineq4: "\a - b\ \ \a\ + \b\" proof - - have "\a - b\ = \a + - b\" by (simp add: algebra_simps) - also have "... \ \a\ + \- b\" by (rule abs_triangle_ineq) + have "\a - b\ = \a + - b\" + by (simp add: algebra_simps) + also have "\ \ \a\ + \- b\" + by (rule abs_triangle_ineq) finally show ?thesis by simp qed lemma abs_diff_triangle_ineq: "\a + b - (c + d)\ \ \a - c\ + \b - d\" proof - - have "\a + b - (c+d)\ = \(a-c) + (b-d)\" by (simp add: algebra_simps) - also have "... \ \a-c\ + \b-d\" by (rule abs_triangle_ineq) + have "\a + b - (c + d)\ = \(a - c) + (b - d)\" + by (simp add: algebra_simps) + also have "\ \ \a - c\ + \b - d\" + by (rule abs_triangle_ineq) finally show ?thesis . qed -lemma abs_add_abs [simp]: - "\\a\ + \b\\ = \a\ + \b\" (is "?L = ?R") +lemma abs_add_abs [simp]: "\\a\ + \b\\ = \a\ + \b\" + (is "?L = ?R") proof (rule antisym) - show "?L \ ?R" by(rule abs_ge_self) -next - have "?L \ \\a\\ + \\b\\" by(rule abs_triangle_ineq) + show "?L \ ?R" by (rule abs_ge_self) + have "?L \ \\a\\ + \\b\\" by (rule abs_triangle_ineq) also have "\ = ?R" by simp finally show "?L \ ?R" . qed @@ -1327,8 +1273,9 @@ lemma dense_eq0_I: fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}" - shows "(\e. 0 < e \ \x\ \ e) ==> x = 0" - apply (cases "\x\ = 0", simp) + shows "(\e. 0 < e \ \x\ \ e) \ x = 0" + apply (cases "\x\ = 0") + apply simp apply (simp only: zero_less_abs_iff [symmetric]) apply (drule dense) apply (auto simp add: not_less [symmetric]) @@ -1336,10 +1283,11 @@ hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus -lemmas add_0 = add_0_left \ \FIXME duplicate\ -lemmas mult_1 = mult_1_left \ \FIXME duplicate\ -lemmas ab_left_minus = left_minus \ \FIXME duplicate\ -lemmas diff_diff_eq = diff_diff_add \ \FIXME duplicate\ +lemmas add_0 = add_0_left (* FIXME duplicate *) +lemmas mult_1 = mult_1_left (* FIXME duplicate *) +lemmas ab_left_minus = left_minus (* FIXME duplicate *) +lemmas diff_diff_eq = diff_diff_add (* FIXME duplicate *) + subsection \Canonically ordered monoids\ @@ -1358,14 +1306,14 @@ lemma not_less_zero[simp]: "\ n < 0" by (auto simp: less_le) -lemma zero_less_iff_neq_zero: "(0 < n) \ (n \ 0)" +lemma zero_less_iff_neq_zero: "0 < n \ n \ 0" by (auto simp: less_le) text \This theorem is useful with \blast\\ lemma gr_zeroI: "(n = 0 \ False) \ 0 < n" by (rule zero_less_iff_neq_zero[THEN iffD2]) iprover -lemma not_gr_zero[simp]: "(\ (0 < n)) \ (n = 0)" +lemma not_gr_zero[simp]: "\ 0 < n \ n = 0" by (simp add: zero_less_iff_neq_zero) subclass ordered_comm_monoid_add @@ -1388,54 +1336,48 @@ context fixes a b - assumes "a \ b" + assumes le: "a \ b" begin -lemma add_diff_inverse: - "a + (b - a) = b" - using \a \ b\ by (auto simp add: le_iff_add) +lemma add_diff_inverse: "a + (b - a) = b" + using le by (auto simp add: le_iff_add) -lemma add_diff_assoc: - "c + (b - a) = c + b - a" - using \a \ b\ by (auto simp add: le_iff_add add.left_commute [of c]) +lemma add_diff_assoc: "c + (b - a) = c + b - a" + using le by (auto simp add: le_iff_add add.left_commute [of c]) -lemma add_diff_assoc2: - "b - a + c = b + c - a" - using \a \ b\ by (auto simp add: le_iff_add add.assoc) +lemma add_diff_assoc2: "b - a + c = b + c - a" + using le by (auto simp add: le_iff_add add.assoc) -lemma diff_add_assoc: - "c + b - a = c + (b - a)" - using \a \ b\ by (simp add: add.commute add_diff_assoc) +lemma diff_add_assoc: "c + b - a = c + (b - a)" + using le by (simp add: add.commute add_diff_assoc) -lemma diff_add_assoc2: - "b + c - a = b - a + c" - using \a \ b\by (simp add: add.commute add_diff_assoc) +lemma diff_add_assoc2: "b + c - a = b - a + c" + using le by (simp add: add.commute add_diff_assoc) -lemma diff_diff_right: - "c - (b - a) = c + a - b" +lemma diff_diff_right: "c - (b - a) = c + a - b" by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b - a", symmetric] add.commute) -lemma diff_add: - "b - a + a = b" +lemma diff_add: "b - a + a = b" by (simp add: add.commute add_diff_inverse) -lemma le_add_diff: - "c \ b + c - a" +lemma le_add_diff: "c \ b + c - a" by (auto simp add: add.commute diff_add_assoc2 le_iff_add) -lemma le_imp_diff_is_add: - "a \ b \ b - a = c \ b = c + a" +lemma le_imp_diff_is_add: "a \ b \ b - a = c \ b = c + a" by (auto simp add: add.commute add_diff_inverse) -lemma le_diff_conv2: - "c \ b - a \ c + a \ b" (is "?P \ ?Q") +lemma le_diff_conv2: "c \ b - a \ c + a \ b" + (is "?P \ ?Q") proof assume ?P - then have "c + a \ b - a + a" by (rule add_right_mono) - then show ?Q by (simp add: add_diff_inverse add.commute) + then have "c + a \ b - a + a" + by (rule add_right_mono) + then show ?Q + by (simp add: add_diff_inverse add.commute) next assume ?Q - then have "a + c \ a + (b - a)" by (simp add: add_diff_inverse add.commute) + then have "a + c \ a + (b - a)" + by (simp add: add_diff_inverse add.commute) then show ?P by simp qed @@ -1443,6 +1385,7 @@ end + subsection \Tools setup\ lemma add_mono_thms_linordered_semiring: @@ -1451,7 +1394,7 @@ and "i = j \ k \ l \ i + k \ j + l" and "i \ j \ k = l \ i + k \ j + l" and "i = j \ k = l \ i + k = j + l" -by (rule add_mono, clarify+)+ + by (rule add_mono, clarify+)+ lemma add_mono_thms_linordered_field: fixes i j k :: "'a::ordered_cancel_ab_semigroup_add" @@ -1460,8 +1403,8 @@ and "i < j \ k \ l \ i + k < j + l" and "i \ j \ k < l \ i + k < j + l" and "i < j \ k < l \ i + k < j + l" -by (auto intro: add_strict_right_mono add_strict_left_mono - add_less_le_mono add_le_less_mono add_strict_mono) + by (auto intro: add_strict_right_mono add_strict_left_mono + add_less_le_mono add_le_less_mono add_strict_mono) code_identifier code_module Groups \ (SML) Arith and (OCaml) Arith and (Haskell) Arith diff -r 0c89eef79701 -r 83a91a73fcb5 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Mon Jun 20 10:51:34 2016 +0200 +++ b/src/HOL/Lattices.thy Mon Jun 20 22:31:16 2016 +0200 @@ -21,24 +21,23 @@ begin lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b" -by (simp add: assoc [symmetric]) + by (simp add: assoc [symmetric]) lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b" -by (simp add: assoc) + by (simp add: assoc) end locale semilattice_neutr = semilattice + comm_monoid locale semilattice_order = semilattice + - fixes less_eq :: "'a \ 'a \ bool" (infix "\<^bold>\" 50) - and less :: "'a \ 'a \ bool" (infix "\<^bold><" 50) + fixes less_eq :: "'a \ 'a \ bool" (infix "\<^bold>\" 50) + and less :: "'a \ 'a \ bool" (infix "\<^bold><" 50) assumes order_iff: "a \<^bold>\ b \ a = a \<^bold>* b" and strict_order_iff: "a \<^bold>< b \ a = a \<^bold>* b \ a \ b" begin -lemma orderI: - "a = a \<^bold>* b \ a \<^bold>\ b" +lemma orderI: "a = a \<^bold>* b \ a \<^bold>\ b" by (simp add: order_iff) lemma orderE: @@ -49,7 +48,7 @@ sublocale ordering less_eq less proof fix a b - show "a \<^bold>< b \ a \<^bold>\ b \ a \ b" + show "a \<^bold>< b \ a \<^bold>\ b \ a \ b" for a b by (simp add: order_iff strict_order_iff) next fix a @@ -74,12 +73,10 @@ then show "a \<^bold>\ c" by (rule orderI) qed -lemma cobounded1 [simp]: - "a \<^bold>* b \<^bold>\ a" - by (simp add: order_iff commute) +lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\ a" + by (simp add: order_iff commute) -lemma cobounded2 [simp]: - "a \<^bold>* b \<^bold>\ b" +lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\ b" by (simp add: order_iff) lemma boundedI: @@ -95,8 +92,7 @@ obtains "a \<^bold>\ b" and "a \<^bold>\ c" using assms by (blast intro: trans cobounded1 cobounded2) -lemma bounded_iff [simp]: - "a \<^bold>\ b \<^bold>* c \ a \<^bold>\ b \ a \<^bold>\ c" +lemma bounded_iff [simp]: "a \<^bold>\ b \<^bold>* c \ a \<^bold>\ b \ a \<^bold>\ c" by (blast intro: boundedI elim: boundedE) lemma strict_boundedE: @@ -104,21 +100,17 @@ obtains "a \<^bold>< b" and "a \<^bold>< c" using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+ -lemma coboundedI1: - "a \<^bold>\ c \ a \<^bold>* b \<^bold>\ c" +lemma coboundedI1: "a \<^bold>\ c \ a \<^bold>* b \<^bold>\ c" by (rule trans) auto -lemma coboundedI2: - "b \<^bold>\ c \ a \<^bold>* b \<^bold>\ c" +lemma coboundedI2: "b \<^bold>\ c \ a \<^bold>* b \<^bold>\ c" by (rule trans) auto -lemma strict_coboundedI1: - "a \<^bold>< c \ a \<^bold>* b \<^bold>< c" +lemma strict_coboundedI1: "a \<^bold>< c \ a \<^bold>* b \<^bold>< c" using irrefl by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE) -lemma strict_coboundedI2: - "b \<^bold>< c \ a \<^bold>* b \<^bold>< c" +lemma strict_coboundedI2: "b \<^bold>< c \ a \<^bold>* b \<^bold>< c" using strict_coboundedI1 [of b c a] by (simp add: commute) lemma mono: "a \<^bold>\ c \ b \<^bold>\ d \ a \<^bold>* b \<^bold>\ c \<^bold>* d" @@ -152,7 +144,7 @@ class inf = fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) -class sup = +class sup = fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) @@ -175,10 +167,9 @@ text \Dual lattice\ -lemma dual_semilattice: - "class.semilattice_inf sup greater_eq greater" -by (rule class.semilattice_inf.intro, rule dual_order) - (unfold_locales, simp_all add: sup_least) +lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater" + by (rule class.semilattice_inf.intro, rule dual_order) + (unfold_locales, simp_all add: sup_least) end @@ -190,12 +181,10 @@ context semilattice_inf begin -lemma le_infI1: - "a \ x \ a \ b \ x" +lemma le_infI1: "a \ x \ a \ b \ x" by (rule order_trans) auto -lemma le_infI2: - "b \ x \ a \ b \ x" +lemma le_infI2: "b \ x \ a \ b \ x" by (rule order_trans) auto lemma le_infI: "x \ a \ x \ b \ x \ a \ b" @@ -204,20 +193,16 @@ lemma le_infE: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" by (blast intro: order_trans inf_le1 inf_le2) -lemma le_inf_iff: - "x \ y \ z \ x \ y \ x \ z" +lemma le_inf_iff: "x \ y \ z \ x \ y \ x \ z" by (blast intro: le_infI elim: le_infE) -lemma le_iff_inf: - "x \ y \ x \ y = x" +lemma le_iff_inf: "x \ y \ x \ y = x" by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff) lemma inf_mono: "a \ c \ b \ d \ a \ b \ c \ d" by (fast intro: inf_greatest le_infI1 le_infI2) -lemma mono_inf: - fixes f :: "'a \ 'b::semilattice_inf" - shows "mono f \ f (A \ B) \ f A \ f B" +lemma mono_inf: "mono f \ f (A \ B) \ f A \ f B" for f :: "'a \ 'b::semilattice_inf" by (auto simp add: mono_def intro: Lattices.inf_greatest) end @@ -225,36 +210,28 @@ context semilattice_sup begin -lemma le_supI1: - "x \ a \ x \ a \ b" +lemma le_supI1: "x \ a \ x \ a \ b" + by (rule order_trans) auto + +lemma le_supI2: "x \ b \ x \ a \ b" by (rule order_trans) auto -lemma le_supI2: - "x \ b \ x \ a \ b" - by (rule order_trans) auto - -lemma le_supI: - "a \ x \ b \ x \ a \ b \ x" +lemma le_supI: "a \ x \ b \ x \ a \ b \ x" by (fact sup_least) (* FIXME: duplicate lemma *) -lemma le_supE: - "a \ b \ x \ (a \ x \ b \ x \ P) \ P" +lemma le_supE: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" by (blast intro: order_trans sup_ge1 sup_ge2) -lemma le_sup_iff: - "x \ y \ z \ x \ z \ y \ z" +lemma le_sup_iff: "x \ y \ z \ x \ z \ y \ z" by (blast intro: le_supI elim: le_supE) -lemma le_iff_sup: - "x \ y \ x \ y = y" +lemma le_iff_sup: "x \ y \ x \ y = y" by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff) lemma sup_mono: "a \ c \ b \ d \ a \ b \ c \ d" by (fast intro: sup_least le_supI1 le_supI2) -lemma mono_sup: - fixes f :: "'a \ 'b::semilattice_sup" - shows "mono f \ f A \ f B \ f (A \ B)" +lemma mono_sup: "mono f \ f A \ f B \ f (A \ B)" for f :: "'a \ 'b::semilattice_sup" by (auto simp add: mono_def intro: Lattices.sup_least) end @@ -302,7 +279,7 @@ lemma inf_absorb2: "y \ x \ x \ y = y" by (rule antisym) auto - + lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem end @@ -352,8 +329,7 @@ context lattice begin -lemma dual_lattice: - "class.lattice sup (op \) (op >) inf" +lemma dual_lattice: "class.lattice sup (op \) (op >) inf" by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order) (unfold_locales, auto) @@ -375,47 +351,48 @@ lemma distrib_inf_le: "(x \ y) \ (x \ z) \ x \ (y \ z)" by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) -text\If you have one of them, you have them all.\ +text \If you have one of them, you have them all.\ lemma distrib_imp1: -assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" -shows "x \ (y \ z) = (x \ y) \ (x \ z)" + assumes distrib: "\x y z. x \ (y \ z) = (x \ y) \ (x \ z)" + shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- - have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by simp + have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" + by simp also have "\ = x \ (z \ (x \ y))" - by (simp add: D inf_commute sup_assoc del: sup_inf_absorb) + by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb) also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)" - by(simp add: inf_commute) - also have "\ = (x \ y) \ (x \ z)" by(simp add:D) + by (simp add: inf_commute) + also have "\ = (x \ y) \ (x \ z)" by(simp add:distrib) finally show ?thesis . qed lemma distrib_imp2: -assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" -shows "x \ (y \ z) = (x \ y) \ (x \ z)" + assumes distrib: "\x y z. x \ (y \ z) = (x \ y) \ (x \ z)" + shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- - have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by simp + have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" + by simp also have "\ = x \ (z \ (x \ y))" - by (simp add: D sup_commute inf_assoc del: inf_sup_absorb) + by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb) also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)" - by(simp add: sup_commute) - also have "\ = (x \ y) \ (x \ z)" by(simp add:D) + by (simp add: sup_commute) + also have "\ = (x \ y) \ (x \ z)" by (simp add:distrib) finally show ?thesis . qed end + subsubsection \Strict order\ context semilattice_inf begin -lemma less_infI1: - "a \ x \ a \ b \ x" +lemma less_infI1: "a \ x \ a \ b \ x" by (auto simp add: less_le inf_absorb1 intro: le_infI1) -lemma less_infI2: - "b \ x \ a \ b \ x" +lemma less_infI2: "b \ x \ a \ b \ x" by (auto simp add: less_le inf_absorb2 intro: le_infI2) end @@ -423,13 +400,11 @@ context semilattice_sup begin -lemma less_supI1: - "x \ a \ x \ a \ b" +lemma less_supI1: "x \ a \ x \ a \ b" using dual_semilattice by (rule semilattice_inf.less_infI1) -lemma less_supI2: - "x \ b \ x \ a \ b" +lemma less_supI2: "x \ b \ x \ a \ b" using dual_semilattice by (rule semilattice_inf.less_infI2) @@ -444,31 +419,24 @@ context distrib_lattice begin -lemma sup_inf_distrib2: - "(y \ z) \ x = (y \ x) \ (z \ x)" +lemma sup_inf_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)" by (simp add: sup_commute sup_inf_distrib1) -lemma inf_sup_distrib1: - "x \ (y \ z) = (x \ y) \ (x \ z)" +lemma inf_sup_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" by (rule distrib_imp2 [OF sup_inf_distrib1]) -lemma inf_sup_distrib2: - "(y \ z) \ x = (y \ x) \ (z \ x)" +lemma inf_sup_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)" by (simp add: inf_commute inf_sup_distrib1) -lemma dual_distrib_lattice: - "class.distrib_lattice sup (op \) (op >) inf" +lemma dual_distrib_lattice: "class.distrib_lattice sup (op \) (op >) inf" by (rule class.distrib_lattice.intro, rule dual_lattice) (unfold_locales, fact inf_sup_distrib1) -lemmas sup_inf_distrib = - sup_inf_distrib1 sup_inf_distrib2 +lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2 -lemmas inf_sup_distrib = - inf_sup_distrib1 inf_sup_distrib2 +lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2 -lemmas distrib = - sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 +lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 end @@ -481,8 +449,7 @@ sublocale inf_top: semilattice_neutr inf top + inf_top: semilattice_neutr_order inf top less_eq less proof - fix x - show "x \ \ = x" + show "x \ \ = x" for x by (rule inf_absorb1) simp qed @@ -494,8 +461,7 @@ sublocale sup_bot: semilattice_neutr sup bot + sup_bot: semilattice_neutr_order sup bot greater_eq greater proof - fix x - show "x \ \ = x" + show "x \ \ = x" for x by (rule sup_absorb1) simp qed @@ -506,28 +472,22 @@ subclass bounded_semilattice_sup_bot .. -lemma inf_bot_left [simp]: - "\ \ x = \" +lemma inf_bot_left [simp]: "\ \ x = \" by (rule inf_absorb1) simp -lemma inf_bot_right [simp]: - "x \ \ = \" +lemma inf_bot_right [simp]: "x \ \ = \" by (rule inf_absorb2) simp -lemma sup_bot_left: - "\ \ x = x" +lemma sup_bot_left: "\ \ x = x" by (fact sup_bot.left_neutral) -lemma sup_bot_right: - "x \ \ = x" +lemma sup_bot_right: "x \ \ = x" by (fact sup_bot.right_neutral) -lemma sup_eq_bot_iff [simp]: - "x \ y = \ \ x = \ \ y = \" +lemma sup_eq_bot_iff [simp]: "x \ y = \ \ x = \ \ y = \" by (simp add: eq_iff) -lemma bot_eq_sup_iff [simp]: - "\ = x \ y \ x = \ \ y = \" +lemma bot_eq_sup_iff [simp]: "\ = x \ y \ x = \ \ y = \" by (simp add: eq_iff) end @@ -537,24 +497,19 @@ subclass bounded_semilattice_inf_top .. -lemma sup_top_left [simp]: - "\ \ x = \" +lemma sup_top_left [simp]: "\ \ x = \" by (rule sup_absorb1) simp -lemma sup_top_right [simp]: - "x \ \ = \" +lemma sup_top_right [simp]: "x \ \ = \" by (rule sup_absorb2) simp -lemma inf_top_left: - "\ \ x = x" +lemma inf_top_left: "\ \ x = x" by (fact inf_top.left_neutral) -lemma inf_top_right: - "x \ \ = x" +lemma inf_top_right: "x \ \ = x" by (fact inf_top.right_neutral) -lemma inf_eq_top_iff [simp]: - "x \ y = \ \ x = \ \ y = \" +lemma inf_eq_top_iff [simp]: "x \ y = \ \ x = \ \ y = \" by (simp add: eq_iff) end @@ -565,8 +520,7 @@ subclass bounded_lattice_bot .. subclass bounded_lattice_top .. -lemma dual_bounded_lattice: - "class.bounded_lattice sup greater_eq greater inf \ \" +lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \ \" by unfold_locales (auto simp add: less_le_not_le) end @@ -582,12 +536,10 @@ by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) -lemma compl_inf_bot [simp]: - "- x \ x = \" +lemma compl_inf_bot [simp]: "- x \ x = \" by (simp add: inf_commute inf_compl_bot) -lemma compl_sup_top [simp]: - "- x \ x = \" +lemma compl_sup_top [simp]: "- x \ x = \" by (simp add: sup_commute sup_compl_top) lemma compl_unique: @@ -606,12 +558,10 @@ then show "- x = y" by simp qed -lemma double_compl [simp]: - "- (- x) = x" +lemma double_compl [simp]: "- (- x) = x" using compl_inf_bot compl_sup_top by (rule compl_unique) -lemma compl_eq_compl_iff [simp]: - "- x = - y \ x = y" +lemma compl_eq_compl_iff [simp]: "- x = - y \ x = y" proof assume "- x = - y" then have "- (- x) = - (- y)" by (rule arg_cong) @@ -621,22 +571,19 @@ then show "- x = - y" by simp qed -lemma compl_bot_eq [simp]: - "- \ = \" +lemma compl_bot_eq [simp]: "- \ = \" proof - from sup_compl_top have "\ \ - \ = \" . then show ?thesis by simp qed -lemma compl_top_eq [simp]: - "- \ = \" +lemma compl_top_eq [simp]: "- \ = \" proof - from inf_compl_bot have "\ \ - \ = \" . then show ?thesis by simp qed -lemma compl_inf [simp]: - "- (x \ y) = - x \ - y" +lemma compl_inf [simp]: "- (x \ y) = - x \ - y" proof (rule compl_unique) have "(x \ y) \ (- x \ - y) = (y \ (x \ - x)) \ (x \ (y \ - y))" by (simp only: inf_sup_distrib inf_aci) @@ -649,86 +596,87 @@ by (simp add: sup_compl_top) qed -lemma compl_sup [simp]: - "- (x \ y) = - x \ - y" +lemma compl_sup [simp]: "- (x \ y) = - x \ - y" using dual_boolean_algebra by (rule boolean_algebra.compl_inf) lemma compl_mono: - "x \ y \ - y \ - x" + assumes "x \ y" + shows "- y \ - x" proof - - assume "x \ y" - then have "x \ y = y" by (simp only: le_iff_sup) + from assms have "x \ y = y" by (simp only: le_iff_sup) then have "- (x \ y) = - y" by simp then have "- x \ - y = - y" by simp then have "- y \ - x = - y" by (simp only: inf_commute) - then show "- y \ - x" by (simp only: le_iff_inf) + then show ?thesis by (simp only: le_iff_inf) qed -lemma compl_le_compl_iff [simp]: - "- x \ - y \ y \ x" +lemma compl_le_compl_iff [simp]: "- x \ - y \ y \ x" by (auto dest: compl_mono) lemma compl_le_swap1: - assumes "y \ - x" shows "x \ -y" + assumes "y \ - x" + shows "x \ -y" proof - from assms have "- (- x) \ - y" by (simp only: compl_le_compl_iff) then show ?thesis by simp qed lemma compl_le_swap2: - assumes "- y \ x" shows "- x \ y" + assumes "- y \ x" + shows "- x \ y" proof - from assms have "- x \ - (- y)" by (simp only: compl_le_compl_iff) then show ?thesis by simp qed -lemma compl_less_compl_iff: (* TODO: declare [simp] ? *) - "- x \ - y \ y \ x" +lemma compl_less_compl_iff: "- x \ - y \ y \ x" (* TODO: declare [simp] ? *) by (auto simp add: less_le) lemma compl_less_swap1: - assumes "y \ - x" shows "x \ - y" + assumes "y \ - x" + shows "x \ - y" proof - from assms have "- (- x) \ - y" by (simp only: compl_less_compl_iff) then show ?thesis by simp qed lemma compl_less_swap2: - assumes "- y \ x" shows "- x \ y" + assumes "- y \ x" + shows "- x \ y" proof - from assms have "- x \ - (- y)" by (simp only: compl_less_compl_iff) then show ?thesis by simp qed lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top" -by(simp add: inf_sup_aci sup_compl_top) + by (simp add: inf_sup_aci sup_compl_top) lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top" -by(simp add: inf_sup_aci sup_compl_top) + by (simp add: inf_sup_aci sup_compl_top) lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot" -by(simp add: inf_sup_aci inf_compl_bot) + by (simp add: inf_sup_aci inf_compl_bot) lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot" -by(simp add: inf_sup_aci inf_compl_bot) + by (simp add: inf_sup_aci inf_compl_bot) -declare inf_compl_bot [simp] sup_compl_top [simp] +declare inf_compl_bot [simp] and sup_compl_top [simp] lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top" -by(simp add: sup_assoc[symmetric]) + by (simp add: sup_assoc[symmetric]) lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top" -using sup_compl_top_left1[of "- x" y] by simp + using sup_compl_top_left1[of "- x" y] by simp lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot" -by(simp add: inf_assoc[symmetric]) + by (simp add: inf_assoc[symmetric]) lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot" -using inf_compl_bot_left1[of "- x" y] by simp + using inf_compl_bot_left1[of "- x" y] by simp lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot" -by(subst inf_left_commute) simp + by (subst inf_left_commute) simp end @@ -740,6 +688,7 @@ simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") = \fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\ + subsection \\min/max\ as special case of lattice\ context linorder @@ -749,64 +698,48 @@ + max: semilattice_order max greater_eq greater by standard (auto simp add: min_def max_def) -lemma min_le_iff_disj: - "min x y \ z \ x \ z \ y \ z" +lemma min_le_iff_disj: "min x y \ z \ x \ z \ y \ z" unfolding min_def using linear by (auto intro: order_trans) -lemma le_max_iff_disj: - "z \ max x y \ z \ x \ z \ y" +lemma le_max_iff_disj: "z \ max x y \ z \ x \ z \ y" unfolding max_def using linear by (auto intro: order_trans) -lemma min_less_iff_disj: - "min x y < z \ x < z \ y < z" +lemma min_less_iff_disj: "min x y < z \ x < z \ y < z" unfolding min_def le_less using less_linear by (auto intro: less_trans) -lemma less_max_iff_disj: - "z < max x y \ z < x \ z < y" +lemma less_max_iff_disj: "z < max x y \ z < x \ z < y" unfolding max_def le_less using less_linear by (auto intro: less_trans) -lemma min_less_iff_conj [simp]: - "z < min x y \ z < x \ z < y" +lemma min_less_iff_conj [simp]: "z < min x y \ z < x \ z < y" unfolding min_def le_less using less_linear by (auto intro: less_trans) -lemma max_less_iff_conj [simp]: - "max x y < z \ x < z \ y < z" +lemma max_less_iff_conj [simp]: "max x y < z \ x < z \ y < z" unfolding max_def le_less using less_linear by (auto intro: less_trans) -lemma min_max_distrib1: - "min (max b c) a = max (min b a) (min c a)" +lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)" by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) -lemma min_max_distrib2: - "min a (max b c) = max (min a b) (min a c)" +lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)" by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) -lemma max_min_distrib1: - "max (min b c) a = min (max b a) (max c a)" +lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)" by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) -lemma max_min_distrib2: - "max a (min b c) = min (max a b) (max a c)" +lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)" by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym) lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2 -lemma split_min [no_atp]: - "P (min i j) \ (i \ j \ P i) \ (\ i \ j \ P j)" +lemma split_min [no_atp]: "P (min i j) \ (i \ j \ P i) \ (\ i \ j \ P j)" by (simp add: min_def) -lemma split_max [no_atp]: - "P (max i j) \ (i \ j \ P j) \ (\ i \ j \ P i)" +lemma split_max [no_atp]: "P (max i j) \ (i \ j \ P j) \ (\ i \ j \ P i)" by (simp add: max_def) -lemma min_of_mono: - fixes f :: "'a \ 'b::linorder" - shows "mono f \ min (f m) (f n) = f (min m n)" +lemma min_of_mono: "mono f \ min (f m) (f n) = f (min m n)" for f :: "'a \ 'b::linorder" by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym) -lemma max_of_mono: - fixes f :: "'a \ 'b::linorder" - shows "mono f \ max (f m) (f n) = f (max m n)" +lemma max_of_mono: "mono f \ max (f m) (f n) = f (max m n)" for f :: "'a \ 'b::linorder" by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym) end @@ -821,27 +754,33 @@ subsection \Uniqueness of inf and sup\ lemma (in semilattice_inf) inf_unique: - fixes f (infixl "\" 70) - assumes le1: "\x y. x \ y \ x" and le2: "\x y. x \ y \ y" - and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z" + fixes f (infixl "\" 70) + assumes le1: "\x y. x \ y \ x" + and le2: "\x y. x \ y \ y" + and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z" shows "x \ y = x \ y" proof (rule antisym) - show "x \ y \ x \ y" by (rule le_infI) (rule le1, rule le2) -next - have leI: "\x y z. x \ y \ x \ z \ x \ y \ z" by (blast intro: greatest) - show "x \ y \ x \ y" by (rule leI) simp_all + show "x \ y \ x \ y" + by (rule le_infI) (rule le1, rule le2) + have leI: "\x y z. x \ y \ x \ z \ x \ y \ z" + by (blast intro: greatest) + show "x \ y \ x \ y" + by (rule leI) simp_all qed lemma (in semilattice_sup) sup_unique: - fixes f (infixl "\" 70) - assumes ge1 [simp]: "\x y. x \ x \ y" and ge2: "\x y. y \ x \ y" - and least: "\x y z. y \ x \ z \ x \ y \ z \ x" + fixes f (infixl "\" 70) + assumes ge1 [simp]: "\x y. x \ x \ y" + and ge2: "\x y. y \ x \ y" + and least: "\x y z. y \ x \ z \ x \ y \ z \ x" shows "x \ y = x \ y" proof (rule antisym) - show "x \ y \ x \ y" by (rule le_supI) (rule ge1, rule ge2) -next - have leI: "\x y z. x \ z \ y \ z \ x \ y \ z" by (blast intro: least) - show "x \ y \ x \ y" by (rule leI) simp_all + show "x \ y \ x \ y" + by (rule le_supI) (rule ge1, rule ge2) + have leI: "\x y z. x \ z \ y \ z \ x \ y \ z" + by (blast intro: least) + show "x \ y \ x \ y" + by (rule leI) simp_all qed @@ -850,33 +789,25 @@ instantiation bool :: boolean_algebra begin -definition - bool_Compl_def [simp]: "uminus = Not" +definition bool_Compl_def [simp]: "uminus = Not" -definition - bool_diff_def [simp]: "A - B \ A \ \ B" +definition bool_diff_def [simp]: "A - B \ A \ \ B" -definition - [simp]: "P \ Q \ P \ Q" +definition [simp]: "P \ Q \ P \ Q" -definition - [simp]: "P \ Q \ P \ Q" +definition [simp]: "P \ Q \ P \ Q" -instance proof -qed auto +instance by standard auto end -lemma sup_boolI1: - "P \ P \ Q" +lemma sup_boolI1: "P \ P \ Q" by simp -lemma sup_boolI2: - "Q \ P \ Q" +lemma sup_boolI2: "Q \ P \ Q" by simp -lemma sup_boolE: - "P \ Q \ (P \ R) \ (Q \ R) \ R" +lemma sup_boolE: "P \ Q \ (P \ R) \ (Q \ R) \ R" by auto @@ -885,48 +816,40 @@ instantiation "fun" :: (type, semilattice_sup) semilattice_sup begin -definition - "f \ g = (\x. f x \ g x)" +definition "f \ g = (\x. f x \ g x)" -lemma sup_apply [simp, code]: - "(f \ g) x = f x \ g x" +lemma sup_apply [simp, code]: "(f \ g) x = f x \ g x" by (simp add: sup_fun_def) -instance proof -qed (simp_all add: le_fun_def) +instance by standard (simp_all add: le_fun_def) end instantiation "fun" :: (type, semilattice_inf) semilattice_inf begin -definition - "f \ g = (\x. f x \ g x)" +definition "f \ g = (\x. f x \ g x)" -lemma inf_apply [simp, code]: - "(f \ g) x = f x \ g x" +lemma inf_apply [simp, code]: "(f \ g) x = f x \ g x" by (simp add: inf_fun_def) -instance proof -qed (simp_all add: le_fun_def) +instance by standard (simp_all add: le_fun_def) end instance "fun" :: (type, lattice) lattice .. -instance "fun" :: (type, distrib_lattice) distrib_lattice proof -qed (rule ext, simp add: sup_inf_distrib1) +instance "fun" :: (type, distrib_lattice) distrib_lattice + by standard (rule ext, simp add: sup_inf_distrib1) instance "fun" :: (type, bounded_lattice) bounded_lattice .. instantiation "fun" :: (type, uminus) uminus begin -definition - fun_Compl_def: "- A = (\x. - A x)" +definition fun_Compl_def: "- A = (\x. - A x)" -lemma uminus_apply [simp, code]: - "(- A) x = - (A x)" +lemma uminus_apply [simp, code]: "(- A) x = - (A x)" by (simp add: fun_Compl_def) instance .. @@ -936,19 +859,17 @@ instantiation "fun" :: (type, minus) minus begin -definition - fun_diff_def: "A - B = (\x. A x - B x)" +definition fun_diff_def: "A - B = (\x. A x - B x)" -lemma minus_apply [simp, code]: - "(A - B) x = A x - B x" +lemma minus_apply [simp, code]: "(A - B) x = A x - B x" by (simp add: fun_diff_def) instance .. end -instance "fun" :: (type, boolean_algebra) boolean_algebra proof -qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ +instance "fun" :: (type, boolean_algebra) boolean_algebra + by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+ subsection \Lattice on unary and binary predicates\ @@ -995,10 +916,7 @@ lemma sup2E: "(A \ B) x y \ (A x y \ P) \ (B x y \ P) \ P" by (simp add: sup_fun_def) iprover -text \ - \medskip Classical introduction rule: no commitment to \A\ vs - \B\. -\ +text \ \<^medskip> Classical introduction rule: no commitment to \A\ vs \B\.\ lemma sup1CI: "(\ B x \ A x) \ (A \ B) x" by (auto simp add: sup_fun_def) @@ -1012,4 +930,3 @@ less (infix "\" 50) end - diff -r 0c89eef79701 -r 83a91a73fcb5 src/HOL/Rat.thy --- a/src/HOL/Rat.thy Mon Jun 20 10:51:34 2016 +0200 +++ b/src/HOL/Rat.thy Mon Jun 20 22:31:16 2016 +0200 @@ -12,12 +12,10 @@ subsubsection \Construction of the type of rational numbers\ -definition - ratrel :: "(int \ int) \ (int \ int) \ bool" where - "ratrel = (\x y. snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x)" +definition ratrel :: "(int \ int) \ (int \ int) \ bool" + where "ratrel = (\x y. snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x)" -lemma ratrel_iff [simp]: - "ratrel x y \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x" +lemma ratrel_iff [simp]: "ratrel x y \ snd x \ 0 \ snd y \ 0 \ fst x * snd y = fst y * snd x" by (simp add: ratrel_def) lemma exists_ratrel_refl: "\x. ratrel x x" @@ -50,7 +48,8 @@ by (rule part_equivp_ratrel) lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\x. snd x \ 0)" -by (simp add: rat.domain_eq) + by (simp add: rat.domain_eq) + subsubsection \Representation and basic operations\ @@ -59,40 +58,43 @@ by simp lemma eq_rat: - shows "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b" - and "\a. Fract a 0 = Fract 0 1" - and "\a c. Fract 0 a = Fract 0 c" + "\a b c d. b \ 0 \ d \ 0 \ Fract a b = Fract c d \ a * d = c * b" + "\a. Fract a 0 = Fract 0 1" + "\a c. Fract 0 a = Fract 0 c" by (transfer, simp)+ lemma Rat_cases [case_names Fract, cases type: rat]: - assumes "\a b. q = Fract a b \ b > 0 \ coprime a b \ C" + assumes that: "\a b. q = Fract a b \ b > 0 \ coprime a b \ C" shows C proof - - obtain a b :: int where "q = Fract a b" and "b \ 0" + obtain a b :: int where q: "q = Fract a b" and b: "b \ 0" by transfer simp let ?a = "a div gcd a b" let ?b = "b div gcd a b" - from \b \ 0\ have "?b * gcd a b = b" + from b have "?b * gcd a b = b" by simp - with \b \ 0\ have "?b \ 0" by fastforce - from \q = Fract a b\ \b \ 0\ \?b \ 0\ have q: "q = Fract ?a ?b" + with b have "?b \ 0" + by fastforce + with q b have q2: "q = Fract ?a ?b" by (simp add: eq_rat dvd_div_mult mult.commute [of a]) - from \b \ 0\ have coprime: "coprime ?a ?b" + from b have coprime: "coprime ?a ?b" by (auto intro: div_gcd_coprime) - show C proof (cases "b > 0") + show C + proof (cases "b > 0") case True - note assms - moreover note q - moreover from True have "?b > 0" by (simp add: nonneg1_imp_zdiv_pos_iff) - moreover note coprime - ultimately show C . + then have "?b > 0" + by (simp add: nonneg1_imp_zdiv_pos_iff) + from q2 this coprime show C by (rule that) next case False - note assms - moreover have "q = Fract (- ?a) (- ?b)" unfolding q by transfer simp - moreover from False \b \ 0\ have "- ?b > 0" by (simp add: pos_imp_zdiv_neg_iff) - moreover from coprime have "coprime (- ?a) (- ?b)" by simp - ultimately show C . + have "q = Fract (- ?a) (- ?b)" + unfolding q2 by transfer simp + moreover from False b have "- ?b > 0" + by (simp add: pos_imp_zdiv_neg_iff) + moreover from coprime have "coprime (- ?a) (- ?b)" + by simp + ultimately show C + by (rule that) qed qed @@ -134,8 +136,7 @@ lemma minus_rat_cancel [simp]: "Fract (- a) (- b) = Fract a b" by (cases "b = 0") (simp_all add: eq_rat) -definition - diff_rat_def: "q - r = q + - (r::rat)" +definition diff_rat_def: "q - r = q + - r" for q r :: rat lemma diff_rat [simp]: assumes "b \ 0" and "d \ 0" @@ -161,13 +162,13 @@ lemma inverse_rat [simp]: "inverse (Fract a b) = Fract b a" by transfer simp -definition - divide_rat_def: "q div r = q * inverse (r::rat)" +definition divide_rat_def: "q div r = q * inverse r" for q r :: rat lemma divide_rat [simp]: "Fract a b div Fract c d = Fract (a * d) (b * c)" by (simp add: divide_rat_def) -instance proof +instance +proof fix q r s :: rat show "(q * r) * s = q * (r * s)" by transfer simp @@ -189,8 +190,8 @@ by transfer (simp add: algebra_simps) show "(0::rat) \ 1" by transfer simp - { assume "q \ 0" thus "inverse q * q = 1" - by transfer simp } + show "inverse q * q = 1" if "q \ 0" + using that by transfer simp show "q div r = q * inverse r" by (fact divide_rat_def) show "inverse 0 = (0::rat)" @@ -232,34 +233,44 @@ lemma Rat_cases_nonzero [case_names Fract 0]: assumes Fract: "\a b. q = Fract a b \ b > 0 \ a \ 0 \ coprime a b \ C" - assumes 0: "q = 0 \ C" + and 0: "q = 0 \ C" shows C proof (cases "q = 0") - case True then show C using 0 by auto + case True + then show C using 0 by auto next case False - then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto - with False have "0 \ Fract a b" by simp - with \b > 0\ have "a \ 0" by (simp add: Zero_rat_def eq_rat) - with Fract \q = Fract a b\ \b > 0\ \coprime a b\ show C by blast + then obtain a b where *: "q = Fract a b" "b > 0" "coprime a b" + by (cases q) auto + with False have "0 \ Fract a b" + by simp + with \b > 0\ have "a \ 0" + by (simp add: Zero_rat_def eq_rat) + with Fract * show C by blast qed + subsubsection \Function \normalize\\ lemma Fract_coprime: "Fract (a div gcd a b) (b div gcd a b) = Fract a b" proof (cases "b = 0") - case True then show ?thesis by (simp add: eq_rat) + case True + then show ?thesis by (simp add: eq_rat) next case False moreover have "b div gcd a b * gcd a b = b" by (rule dvd_div_mult_self) simp - ultimately have "b div gcd a b * gcd a b \ 0" by simp - then have "b div gcd a b \ 0" by fastforce - with False show ?thesis by (simp add: eq_rat dvd_div_mult mult.commute [of a]) + ultimately have "b div gcd a b * gcd a b \ 0" + by simp + then have "b div gcd a b \ 0" + by fastforce + with False show ?thesis + by (simp add: eq_rat dvd_div_mult mult.commute [of a]) qed -definition normalize :: "int \ int \ int \ int" where - "normalize p = (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) +definition normalize :: "int \ int \ int \ int" + where "normalize p = + (if snd p > 0 then (let a = gcd (fst p) (snd p) in (fst p div a, snd p div a)) else if snd p = 0 then (0, 1) else (let a = - gcd (fst p) (snd p) in (fst p div a, snd p div a)))" @@ -268,79 +279,92 @@ assumes "normalize (p, q) = normalize (r, s)" shows "p * s = r * q" proof - - have aux: "p * gcd r s = sgn (q * s) * r * gcd p q \ q * gcd r s = sgn (q * s) * s * gcd p q \ p * s = q * r" + have *: "p * s = q * r" + if "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" proof - - assume "p * gcd r s = sgn (q * s) * r * gcd p q" and "q * gcd r s = sgn (q * s) * s * gcd p q" - then have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" by simp - with assms show "p * s = q * r" by (auto simp add: ac_simps sgn_times sgn_0_0) + from that + have "(p * gcd r s) * (sgn (q * s) * s * gcd p q) = (q * gcd r s) * (sgn (q * s) * r * gcd p q)" + by simp + with assms show ?thesis + by (auto simp add: ac_simps sgn_times sgn_0_0) qed from assms show ?thesis - by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times split: if_splits intro: aux) + by (auto simp add: normalize_def Let_def dvd_div_div_eq_mult mult.commute sgn_times + split: if_splits intro: *) qed lemma normalize_eq: "normalize (a, b) = (p, q) \ Fract p q = Fract a b" by (auto simp add: normalize_def Let_def Fract_coprime dvd_div_neg rat_number_collapse - split:if_split_asm) + split: if_split_asm) lemma normalize_denom_pos: "normalize r = (p, q) \ q > 0" by (auto simp add: normalize_def Let_def dvd_div_neg pos_imp_zdiv_neg_iff nonneg1_imp_zdiv_pos_iff - split:if_split_asm) + split: if_split_asm) lemma normalize_coprime: "normalize r = (p, q) \ coprime p q" by (auto simp add: normalize_def Let_def dvd_div_neg div_gcd_coprime - split:if_split_asm) + split: if_split_asm) -lemma normalize_stable [simp]: - "q > 0 \ coprime p q \ normalize (p, q) = (p, q)" +lemma normalize_stable [simp]: "q > 0 \ coprime p q \ normalize (p, q) = (p, q)" by (simp add: normalize_def) -lemma normalize_denom_zero [simp]: - "normalize (p, 0) = (0, 1)" +lemma normalize_denom_zero [simp]: "normalize (p, 0) = (0, 1)" by (simp add: normalize_def) -lemma normalize_negative [simp]: - "q < 0 \ normalize (p, q) = normalize (- p, - q)" +lemma normalize_negative [simp]: "q < 0 \ normalize (p, q) = normalize (- p, - q)" by (simp add: normalize_def Let_def dvd_div_neg dvd_neg_div) text\ Decompose a fraction into normalized, i.e. coprime numerator and denominator: \ -definition quotient_of :: "rat \ int \ int" where - "quotient_of x = (THE pair. x = Fract (fst pair) (snd pair) & - snd pair > 0 & coprime (fst pair) (snd pair))" +definition quotient_of :: "rat \ int \ int" + where "quotient_of x = + (THE pair. x = Fract (fst pair) (snd pair) \ snd pair > 0 \ coprime (fst pair) (snd pair))" -lemma quotient_of_unique: - "\!p. r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" +lemma quotient_of_unique: "\!p. r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" proof (cases r) case (Fract a b) - then have "r = Fract (fst (a, b)) (snd (a, b)) \ snd (a, b) > 0 \ coprime (fst (a, b)) (snd (a, b))" by auto - then show ?thesis proof (rule ex1I) + then have "r = Fract (fst (a, b)) (snd (a, b)) \ snd (a, b) > 0 \ coprime (fst (a, b)) (snd (a, b))" + by auto + then show ?thesis + proof (rule ex1I) fix p - obtain c d :: int where p: "p = (c, d)" by (cases p) + obtain c d :: int where p: "p = (c, d)" + by (cases p) assume "r = Fract (fst p) (snd p) \ snd p > 0 \ coprime (fst p) (snd p)" - with p have Fract': "r = Fract c d" "d > 0" "coprime c d" by simp_all + with p have Fract': "r = Fract c d" "d > 0" "coprime c d" + by simp_all have "c = a \ d = b" proof (cases "a = 0") - case True with Fract Fract' show ?thesis by (simp add: eq_rat) + case True + with Fract Fract' show ?thesis + by (simp add: eq_rat) next case False - with Fract Fract' have *: "c * b = a * d" and "c \ 0" by (auto simp add: eq_rat) - then have "c * b > 0 \ a * d > 0" by auto - with \b > 0\ \d > 0\ have "a > 0 \ c > 0" by (simp add: zero_less_mult_iff) - with \a \ 0\ \c \ 0\ have sgn: "sgn a = sgn c" by (auto simp add: not_less) + with Fract Fract' have *: "c * b = a * d" and "c \ 0" + by (auto simp add: eq_rat) + then have "c * b > 0 \ a * d > 0" + by auto + with \b > 0\ \d > 0\ have "a > 0 \ c > 0" + by (simp add: zero_less_mult_iff) + with \a \ 0\ \c \ 0\ have sgn: "sgn a = sgn c" + by (auto simp add: not_less) from \coprime a b\ \coprime c d\ have "\a\ * \d\ = \c\ * \b\ \ \a\ = \c\ \ \d\ = \b\" by (simp add: coprime_crossproduct_int) - with \b > 0\ \d > 0\ have "\a\ * d = \c\ * b \ \a\ = \c\ \ d = b" by simp - then have "a * sgn a * d = c * sgn c * b \ a * sgn a = c * sgn c \ d = b" by (simp add: abs_sgn) - with sgn * show ?thesis by (auto simp add: sgn_0_0) + with \b > 0\ \d > 0\ have "\a\ * d = \c\ * b \ \a\ = \c\ \ d = b" + by simp + then have "a * sgn a * d = c * sgn c * b \ a * sgn a = c * sgn c \ d = b" + by (simp add: abs_sgn) + with sgn * show ?thesis + by (auto simp add: sgn_0_0) qed - with p show "p = (a, b)" by simp + with p show "p = (a, b)" + by simp qed qed -lemma quotient_of_Fract [code]: - "quotient_of (Fract a b) = normalize (a, b)" +lemma quotient_of_Fract [code]: "quotient_of (Fract a b) = normalize (a, b)" proof - have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract) by (rule sym) (auto intro: normalize_eq) @@ -349,9 +373,9 @@ moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime) by (rule normalize_coprime) simp ultimately have "?Fract \ ?denom_pos \ ?coprime" by blast - with quotient_of_unique have - "(THE p. Fract a b = Fract (fst p) (snd p) \ 0 < snd p \ coprime (fst p) (snd p)) = normalize (a, b)" - by (rule the1_equality) + with quotient_of_unique + have "(THE p. Fract a b = Fract (fst p) (snd p) \ 0 < snd p \ + coprime (fst p) (snd p)) = normalize (a, b)" by (rule the1_equality) then show ?thesis by (simp add: quotient_of_def) qed @@ -376,14 +400,13 @@ assumes "quotient_of a = quotient_of b" shows "a = b" proof - - obtain p q r s where a: "a = Fract p q" - and b: "b = Fract r s" - and "q > 0" and "s > 0" by (cases a, cases b) - with assms show ?thesis by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) + obtain p q r s where a: "a = Fract p q" and b: "b = Fract r s" and "q > 0" and "s > 0" + by (cases a, cases b) + with assms show ?thesis + by (simp add: eq_rat quotient_of_Fract normalize_crossproduct) qed -lemma quotient_of_inject_eq: - "quotient_of a = quotient_of b \ a = b" +lemma quotient_of_inject_eq: "quotient_of a = quotient_of b \ a = b" by (auto simp add: quotient_of_inject) @@ -392,7 +415,7 @@ lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l" by (simp add: Fract_of_int_eq [symmetric]) -lemma Fract_add_one: "n \ 0 ==> Fract (m + n) n = Fract m n + 1" +lemma Fract_add_one: "n \ 0 \ Fract (m + n) n = Fract m n + 1" by (simp add: rat_number_expand) lemma quotient_of_div: @@ -401,23 +424,25 @@ proof - from theI'[OF quotient_of_unique[of r], unfolded r[unfolded quotient_of_def]] have "r = Fract n d" by simp - thus ?thesis using Fract_of_int_quotient by simp + then show ?thesis using Fract_of_int_quotient + by simp qed + subsubsection \The ordered field of rational numbers\ lift_definition positive :: "rat \ bool" is "\x. 0 < fst x * snd x" -proof (clarsimp) +proof clarsimp fix a b c d :: int assume "b \ 0" and "d \ 0" and "a * d = c * b" - hence "a * d * b * d = c * b * b * d" + then have "a * d * b * d = c * b * b * d" by simp - hence "a * b * d\<^sup>2 = c * d * b\<^sup>2" + then have "a * b * d\<^sup>2 = c * d * b\<^sup>2" unfolding power2_eq_square by (simp add: ac_simps) - hence "0 < a * b * d\<^sup>2 \ 0 < c * d * b\<^sup>2" + then have "0 < a * b * d\<^sup>2 \ 0 < c * d * b\<^sup>2" by simp - thus "0 < a * b \ 0 < c * d" + then show "0 < a * b \ 0 < c * d" using \b \ 0\ and \d \ 0\ by (simp add: zero_less_mult_iff) qed @@ -425,52 +450,57 @@ lemma positive_zero: "\ positive 0" by transfer simp -lemma positive_add: - "positive x \ positive y \ positive (x + y)" -apply transfer -apply (simp add: zero_less_mult_iff) -apply (elim disjE, simp_all add: add_pos_pos add_neg_neg - mult_pos_neg mult_neg_pos mult_neg_neg) -done +lemma positive_add: "positive x \ positive y \ positive (x + y)" + apply transfer + apply (simp add: zero_less_mult_iff) + apply (elim disjE, simp_all add: add_pos_pos add_neg_neg mult_pos_neg mult_neg_pos mult_neg_neg) + done -lemma positive_mult: - "positive x \ positive y \ positive (x * y)" -by transfer (drule (1) mult_pos_pos, simp add: ac_simps) +lemma positive_mult: "positive x \ positive y \ positive (x * y)" + apply transfer + apply (drule (1) mult_pos_pos) + apply (simp add: ac_simps) + done -lemma positive_minus: - "\ positive x \ x \ 0 \ positive (- x)" -by transfer (force simp: neq_iff zero_less_mult_iff mult_less_0_iff) +lemma positive_minus: "\ positive x \ x \ 0 \ positive (- x)" + by transfer (auto simp: neq_iff zero_less_mult_iff mult_less_0_iff) instantiation rat :: linordered_field begin -definition - "x < y \ positive (y - x)" +definition "x < y \ positive (y - x)" -definition - "x \ (y::rat) \ x < y \ x = y" +definition "x \ y \ x < y \ x = y" for x y :: rat -definition - "\a::rat\ = (if a < 0 then - a else a)" +definition "\a\ = (if a < 0 then - a else a)" for a :: rat -definition - "sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else - 1)" +definition "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" for a :: rat -instance proof +instance +proof fix a b c :: rat show "\a\ = (if a < 0 then - a else a)" by (rule abs_rat_def) show "a < b \ a \ b \ \ b \ a" unfolding less_eq_rat_def less_rat_def - by (auto, drule (1) positive_add, simp_all add: positive_zero) + apply auto + apply (drule (1) positive_add) + apply (simp_all add: positive_zero) + done show "a \ a" unfolding less_eq_rat_def by simp show "a \ b \ b \ c \ a \ c" unfolding less_eq_rat_def less_rat_def - by (auto, drule (1) positive_add, simp add: algebra_simps) + apply auto + apply (drule (1) positive_add) + apply (simp add: algebra_simps) + done show "a \ b \ b \ a \ a = b" unfolding less_eq_rat_def less_rat_def - by (auto, drule (1) positive_add, simp add: positive_zero) + apply auto + apply (drule (1) positive_add) + apply (simp add: positive_zero) + done show "a \ b \ c + a \ c + b" unfolding less_eq_rat_def less_rat_def by auto show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)" @@ -480,7 +510,9 @@ by (auto dest!: positive_minus) show "a < b \ 0 < c \ c * a < c * b" unfolding less_rat_def - by (drule (1) positive_mult, simp add: algebra_simps) + apply (drule (1) positive_mult) + apply (simp add: algebra_simps) + done qed end @@ -488,14 +520,12 @@ instantiation rat :: distrib_lattice begin -definition - "(inf :: rat \ rat \ rat) = min" +definition "(inf :: rat \ rat \ rat) = min" -definition - "(sup :: rat \ rat \ rat) = max" +definition "(sup :: rat \ rat \ rat) = max" -instance proof -qed (auto simp add: inf_rat_def sup_rat_def max_min_distrib2) +instance + by standard (auto simp add: inf_rat_def sup_rat_def max_min_distrib2) end @@ -525,58 +555,50 @@ assumes step: "\a b. 0 < b \ P (Fract a b)" shows "P q" proof (cases q) - have step': "\a b. b < 0 \ P (Fract a b)" + case (Fract a b) + have step': "P (Fract a b)" if b: "b < 0" for a b :: int proof - - fix a::int and b::int - assume b: "b < 0" - hence "0 < -b" by simp - hence "P (Fract (-a) (-b))" by (rule step) - thus "P (Fract a b)" by (simp add: order_less_imp_not_eq [OF b]) + from b have "0 < - b" + by simp + then have "P (Fract (- a) (- b))" + by (rule step) + then show "P (Fract a b)" + by (simp add: order_less_imp_not_eq [OF b]) qed - case (Fract a b) - thus "P q" by (force simp add: linorder_neq_iff step step') + from Fract show "P q" by (auto simp add: linorder_neq_iff step step') qed -lemma zero_less_Fract_iff: - "0 < b \ 0 < Fract a b \ 0 < a" +lemma zero_less_Fract_iff: "0 < b \ 0 < Fract a b \ 0 < a" by (simp add: Zero_rat_def zero_less_mult_iff) -lemma Fract_less_zero_iff: - "0 < b \ Fract a b < 0 \ a < 0" +lemma Fract_less_zero_iff: "0 < b \ Fract a b < 0 \ a < 0" by (simp add: Zero_rat_def mult_less_0_iff) -lemma zero_le_Fract_iff: - "0 < b \ 0 \ Fract a b \ 0 \ a" +lemma zero_le_Fract_iff: "0 < b \ 0 \ Fract a b \ 0 \ a" by (simp add: Zero_rat_def zero_le_mult_iff) -lemma Fract_le_zero_iff: - "0 < b \ Fract a b \ 0 \ a \ 0" +lemma Fract_le_zero_iff: "0 < b \ Fract a b \ 0 \ a \ 0" by (simp add: Zero_rat_def mult_le_0_iff) -lemma one_less_Fract_iff: - "0 < b \ 1 < Fract a b \ b < a" +lemma one_less_Fract_iff: "0 < b \ 1 < Fract a b \ b < a" by (simp add: One_rat_def mult_less_cancel_right_disj) -lemma Fract_less_one_iff: - "0 < b \ Fract a b < 1 \ a < b" +lemma Fract_less_one_iff: "0 < b \ Fract a b < 1 \ a < b" by (simp add: One_rat_def mult_less_cancel_right_disj) -lemma one_le_Fract_iff: - "0 < b \ 1 \ Fract a b \ b \ a" +lemma one_le_Fract_iff: "0 < b \ 1 \ Fract a b \ b \ a" by (simp add: One_rat_def mult_le_cancel_right) -lemma Fract_le_one_iff: - "0 < b \ Fract a b \ 1 \ a \ b" +lemma Fract_le_one_iff: "0 < b \ Fract a b \ 1 \ a \ b" by (simp add: One_rat_def mult_le_cancel_right) subsubsection \Rationals are an Archimedean field\ -lemma rat_floor_lemma: - shows "of_int (a div b) \ Fract a b \ Fract a b < of_int (a div b + 1)" +lemma rat_floor_lemma: "of_int (a div b) \ Fract a b \ Fract a b < of_int (a div b + 1)" proof - have "Fract a b = of_int (a div b) + Fract (a mod b) b" - by (cases "b = 0", simp, simp add: of_int_rat) + by (cases "b = 0") (simp, simp add: of_int_rat) moreover have "0 \ Fract (a mod b) b \ Fract (a mod b) b < 1" unfolding Fract_of_int_quotient by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg) @@ -585,8 +607,7 @@ instance rat :: archimedean_field proof - fix r :: rat - show "\z. r \ of_int z" + show "\z. r \ of_int z" for r :: rat proof (induct r) case (Fract a b) have "Fract a b \ of_int (a div b + 1)" @@ -598,13 +619,11 @@ instantiation rat :: floor_ceiling begin -definition [code del]: - "\x::rat\ = (THE z. of_int z \ x \ x < of_int (z + 1))" +definition [code del]: "\x\ = (THE z. of_int z \ x \ x < of_int (z + 1))" for x :: rat instance proof - fix x :: rat - show "of_int \x\ \ x \ x < of_int (\x\ + 1)" + show "of_int \x\ \ x \ x < of_int (\x\ + 1)" for x :: rat unfolding floor_rat_def using floor_exists1 by (rule theI') qed @@ -631,8 +650,8 @@ @{thm of_int_minus}, @{thm of_int_diff}, @{thm of_int_of_nat_eq}] #> Lin_Arith.add_simprocs [Numeral_Simprocs.field_divide_cancel_numeral_factor] - #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) - #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int => rat"})) + #> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \ rat"}) + #> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \ rat"})) \ @@ -643,9 +662,9 @@ lift_definition of_rat :: "rat \ 'a" is "\x. of_int (fst x) / of_int (snd x)" -apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) -apply (simp only: of_int_mult [symmetric]) -done + apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) + apply (simp only: of_int_mult [symmetric]) + done end @@ -664,17 +683,14 @@ lemma of_rat_minus: "of_rat (- a) = - of_rat a" by transfer simp -lemma of_rat_neg_one [simp]: - "of_rat (- 1) = - 1" +lemma of_rat_neg_one [simp]: "of_rat (- 1) = - 1" by (simp add: of_rat_minus) lemma of_rat_diff: "of_rat (a - b) = of_rat a - of_rat b" using of_rat_add [of a "- b"] by (simp add: of_rat_minus) lemma of_rat_mult: "of_rat (a * b) = of_rat a * of_rat b" -apply transfer -apply (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps) -done + by transfer (simp add: divide_inverse nonzero_inverse_mult_distrib ac_simps) lemma of_rat_setsum: "of_rat (\a\A. f a) = (\a\A. of_rat (f a))" by (induct rule: infinite_finite_induct) (auto simp: of_rat_add) @@ -682,127 +698,109 @@ lemma of_rat_setprod: "of_rat (\a\A. f a) = (\a\A. of_rat (f a))" by (induct rule: infinite_finite_induct) (auto simp: of_rat_mult) -lemma nonzero_of_rat_inverse: - "a \ 0 \ of_rat (inverse a) = inverse (of_rat a)" -apply (rule inverse_unique [symmetric]) -apply (simp add: of_rat_mult [symmetric]) -done +lemma nonzero_of_rat_inverse: "a \ 0 \ of_rat (inverse a) = inverse (of_rat a)" + by (rule inverse_unique [symmetric]) (simp add: of_rat_mult [symmetric]) -lemma of_rat_inverse: - "(of_rat (inverse a)::'a::{field_char_0, field}) = - inverse (of_rat a)" -by (cases "a = 0", simp_all add: nonzero_of_rat_inverse) +lemma of_rat_inverse: "(of_rat (inverse a) :: 'a::{field_char_0,field}) = inverse (of_rat a)" + by (cases "a = 0") (simp_all add: nonzero_of_rat_inverse) -lemma nonzero_of_rat_divide: - "b \ 0 \ of_rat (a / b) = of_rat a / of_rat b" -by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) +lemma nonzero_of_rat_divide: "b \ 0 \ of_rat (a / b) = of_rat a / of_rat b" + by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse) -lemma of_rat_divide: - "(of_rat (a / b)::'a::{field_char_0, field}) - = of_rat a / of_rat b" -by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) +lemma of_rat_divide: "(of_rat (a / b) :: 'a::{field_char_0,field}) = of_rat a / of_rat b" + by (cases "b = 0") (simp_all add: nonzero_of_rat_divide) + +lemma of_rat_power: "(of_rat (a ^ n) :: 'a::field_char_0) = of_rat a ^ n" + by (induct n) (simp_all add: of_rat_mult) -lemma of_rat_power: - "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n" -by (induct n) (simp_all add: of_rat_mult) +lemma of_rat_eq_iff [simp]: "of_rat a = of_rat b \ a = b" + apply transfer + apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) + apply (simp only: of_int_mult [symmetric] of_int_eq_iff) + done -lemma of_rat_eq_iff [simp]: "(of_rat a = of_rat b) = (a = b)" -apply transfer -apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq) -apply (simp only: of_int_mult [symmetric] of_int_eq_iff) -done - -lemma of_rat_eq_0_iff [simp]: "(of_rat a = 0) = (a = 0)" +lemma of_rat_eq_0_iff [simp]: "of_rat a = 0 \ a = 0" using of_rat_eq_iff [of _ 0] by simp -lemma zero_eq_of_rat_iff [simp]: "(0 = of_rat a) = (0 = a)" +lemma zero_eq_of_rat_iff [simp]: "0 = of_rat a \ 0 = a" by simp -lemma of_rat_eq_1_iff [simp]: "(of_rat a = 1) = (a = 1)" +lemma of_rat_eq_1_iff [simp]: "of_rat a = 1 \ a = 1" using of_rat_eq_iff [of _ 1] by simp -lemma one_eq_of_rat_iff [simp]: "(1 = of_rat a) = (1 = a)" +lemma one_eq_of_rat_iff [simp]: "1 = of_rat a \ 1 = a" by simp -lemma of_rat_less: - "(of_rat r :: 'a::linordered_field) < of_rat s \ r < s" +lemma of_rat_less: "(of_rat r :: 'a::linordered_field) < of_rat s \ r < s" proof (induct r, induct s) fix a b c d :: int assume not_zero: "b > 0" "d > 0" then have "b * d > 0" by simp have of_int_divide_less_eq: - "(of_int a :: 'a) / of_int b < of_int c / of_int d - \ (of_int a :: 'a) * of_int d < of_int c * of_int b" + "(of_int a :: 'a) / of_int b < of_int c / of_int d \ + (of_int a :: 'a) * of_int d < of_int c * of_int b" using not_zero by (simp add: pos_less_divide_eq pos_divide_less_eq) - show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) - \ Fract a b < Fract c d" + show "(of_rat (Fract a b) :: 'a::linordered_field) < of_rat (Fract c d) \ + Fract a b < Fract c d" using not_zero \b * d > 0\ by (simp add: of_rat_rat of_int_divide_less_eq of_int_mult [symmetric] del: of_int_mult) qed -lemma of_rat_less_eq: - "(of_rat r :: 'a::linordered_field) \ of_rat s \ r \ s" +lemma of_rat_less_eq: "(of_rat r :: 'a::linordered_field) \ of_rat s \ r \ s" unfolding le_less by (auto simp add: of_rat_less) -lemma of_rat_le_0_iff [simp]: "((of_rat r :: 'a::linordered_field) \ 0) = (r \ 0)" - using of_rat_less_eq [of r 0, where 'a='a] by simp +lemma of_rat_le_0_iff [simp]: "(of_rat r :: 'a::linordered_field) \ 0 \ r \ 0" + using of_rat_less_eq [of r 0, where 'a = 'a] by simp -lemma zero_le_of_rat_iff [simp]: "(0 \ (of_rat r :: 'a::linordered_field)) = (0 \ r)" - using of_rat_less_eq [of 0 r, where 'a='a] by simp +lemma zero_le_of_rat_iff [simp]: "0 \ (of_rat r :: 'a::linordered_field) \ 0 \ r" + using of_rat_less_eq [of 0 r, where 'a = 'a] by simp -lemma of_rat_le_1_iff [simp]: "((of_rat r :: 'a::linordered_field) \ 1) = (r \ 1)" +lemma of_rat_le_1_iff [simp]: "(of_rat r :: 'a::linordered_field) \ 1 \ r \ 1" using of_rat_less_eq [of r 1] by simp -lemma one_le_of_rat_iff [simp]: "(1 \ (of_rat r :: 'a::linordered_field)) = (1 \ r)" +lemma one_le_of_rat_iff [simp]: "1 \ (of_rat r :: 'a::linordered_field) \ 1 \ r" using of_rat_less_eq [of 1 r] by simp -lemma of_rat_less_0_iff [simp]: "((of_rat r :: 'a::linordered_field) < 0) = (r < 0)" - using of_rat_less [of r 0, where 'a='a] by simp +lemma of_rat_less_0_iff [simp]: "(of_rat r :: 'a::linordered_field) < 0 \ r < 0" + using of_rat_less [of r 0, where 'a = 'a] by simp -lemma zero_less_of_rat_iff [simp]: "(0 < (of_rat r :: 'a::linordered_field)) = (0 < r)" - using of_rat_less [of 0 r, where 'a='a] by simp +lemma zero_less_of_rat_iff [simp]: "0 < (of_rat r :: 'a::linordered_field) \ 0 < r" + using of_rat_less [of 0 r, where 'a = 'a] by simp -lemma of_rat_less_1_iff [simp]: "((of_rat r :: 'a::linordered_field) < 1) = (r < 1)" +lemma of_rat_less_1_iff [simp]: "(of_rat r :: 'a::linordered_field) < 1 \ r < 1" using of_rat_less [of r 1] by simp -lemma one_less_of_rat_iff [simp]: "(1 < (of_rat r :: 'a::linordered_field)) = (1 < r)" +lemma one_less_of_rat_iff [simp]: "1 < (of_rat r :: 'a::linordered_field) \ 1 < r" using of_rat_less [of 1 r] by simp lemma of_rat_eq_id [simp]: "of_rat = id" proof - fix a - show "of_rat a = id a" - by (induct a) - (simp add: of_rat_rat Fract_of_int_eq [symmetric]) + show "of_rat a = id a" for a + by (induct a) (simp add: of_rat_rat Fract_of_int_eq [symmetric]) qed -text\Collapse nested embeddings\ +text \Collapse nested embeddings\ lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n" -by (induct n) (simp_all add: of_rat_add) + by (induct n) (simp_all add: of_rat_add) lemma of_rat_of_int_eq [simp]: "of_rat (of_int z) = of_int z" -by (cases z rule: int_diff_cases) (simp add: of_rat_diff) + by (cases z rule: int_diff_cases) (simp add: of_rat_diff) -lemma of_rat_numeral_eq [simp]: - "of_rat (numeral w) = numeral w" -using of_rat_of_int_eq [of "numeral w"] by simp +lemma of_rat_numeral_eq [simp]: "of_rat (numeral w) = numeral w" + using of_rat_of_int_eq [of "numeral w"] by simp -lemma of_rat_neg_numeral_eq [simp]: - "of_rat (- numeral w) = - numeral w" -using of_rat_of_int_eq [of "- numeral w"] by simp +lemma of_rat_neg_numeral_eq [simp]: "of_rat (- numeral w) = - numeral w" + using of_rat_of_int_eq [of "- numeral w"] by simp lemmas zero_rat = Zero_rat_def lemmas one_rat = One_rat_def -abbreviation - rat_of_nat :: "nat \ rat" -where - "rat_of_nat \ of_nat" +abbreviation rat_of_nat :: "nat \ rat" + where "rat_of_nat \ of_nat" -abbreviation - rat_of_int :: "int \ rat" -where - "rat_of_int \ of_int" +abbreviation rat_of_int :: "int \ rat" + where "rat_of_int \ of_int" + subsection \The Set of Rational Numbers\ @@ -815,92 +813,76 @@ end lemma Rats_of_rat [simp]: "of_rat r \ \" -by (simp add: Rats_def) + by (simp add: Rats_def) lemma Rats_of_int [simp]: "of_int z \ \" -by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat) + by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat) lemma Rats_of_nat [simp]: "of_nat n \ \" -by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat) + by (subst of_rat_of_nat_eq [symmetric]) (rule Rats_of_rat) lemma Rats_number_of [simp]: "numeral w \ \" -by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat) + by (subst of_rat_numeral_eq [symmetric]) (rule Rats_of_rat) lemma Rats_0 [simp]: "0 \ \" -apply (unfold Rats_def) -apply (rule range_eqI) -apply (rule of_rat_0 [symmetric]) -done + unfolding Rats_def by (rule range_eqI) (rule of_rat_0 [symmetric]) lemma Rats_1 [simp]: "1 \ \" -apply (unfold Rats_def) -apply (rule range_eqI) -apply (rule of_rat_1 [symmetric]) -done + unfolding Rats_def by (rule range_eqI) (rule of_rat_1 [symmetric]) -lemma Rats_add [simp]: "\a \ \; b \ \\ \ a + b \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_add [symmetric]) -done +lemma Rats_add [simp]: "a \ \ \ b \ \ \ a + b \ \" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_add [symmetric]) + done lemma Rats_minus [simp]: "a \ \ \ - a \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_minus [symmetric]) -done + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_minus [symmetric]) + done -lemma Rats_diff [simp]: "\a \ \; b \ \\ \ a - b \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_diff [symmetric]) -done +lemma Rats_diff [simp]: "a \ \ \ b \ \ \ a - b \ \" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_diff [symmetric]) + done -lemma Rats_mult [simp]: "\a \ \; b \ \\ \ a * b \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_mult [symmetric]) -done +lemma Rats_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_mult [symmetric]) + done -lemma nonzero_Rats_inverse: - fixes a :: "'a::field_char_0" - shows "\a \ \; a \ 0\ \ inverse a \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (erule nonzero_of_rat_inverse [symmetric]) -done +lemma nonzero_Rats_inverse: "a \ \ \ a \ 0 \ inverse a \ \" for a :: "'a::field_char_0" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (erule nonzero_of_rat_inverse [symmetric]) + done -lemma Rats_inverse [simp]: - fixes a :: "'a::{field_char_0, field}" - shows "a \ \ \ inverse a \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_inverse [symmetric]) -done +lemma Rats_inverse [simp]: "a \ \ \ inverse a \ \" for a :: "'a::{field_char_0,field}" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_inverse [symmetric]) + done -lemma nonzero_Rats_divide: - fixes a b :: "'a::field_char_0" - shows "\a \ \; b \ \; b \ 0\ \ a / b \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (erule nonzero_of_rat_divide [symmetric]) -done +lemma nonzero_Rats_divide: "a \ \ \ b \ \ \ b \ 0 \ a / b \ \" for a b :: "'a::field_char_0" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (erule nonzero_of_rat_divide [symmetric]) + done -lemma Rats_divide [simp]: - fixes a b :: "'a::{field_char_0, field}" - shows "\a \ \; b \ \\ \ a / b \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_divide [symmetric]) -done +lemma Rats_divide [simp]: "a \ \ \ b \ \ \ a / b \ \" for a b :: "'a::{field_char_0, field}" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_divide [symmetric]) + done -lemma Rats_power [simp]: - fixes a :: "'a::field_char_0" - shows "a \ \ \ a ^ n \ \" -apply (auto simp add: Rats_def) -apply (rule range_eqI) -apply (rule of_rat_power [symmetric]) -done +lemma Rats_power [simp]: "a \ \ \ a ^ n \ \" for a :: "'a::field_char_0" + apply (auto simp add: Rats_def) + apply (rule range_eqI) + apply (rule of_rat_power [symmetric]) + done lemma Rats_cases [cases set: Rats]: assumes "q \ \" @@ -911,22 +893,21 @@ then show thesis .. qed -lemma Rats_induct [case_names of_rat, induct set: Rats]: - "q \ \ \ (\r. P (of_rat r)) \ P q" +lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \ \ \ (\r. P (of_rat r)) \ P q" by (rule Rats_cases) auto lemma Rats_infinite: "\ finite \" by (auto dest!: finite_imageD simp: inj_on_def infinite_UNIV_char_0 Rats_def) + subsection \Implementation of rational numbers as pairs of integers\ text \Formal constructor\ -definition Frct :: "int \ int \ rat" where - [simp]: "Frct p = Fract (fst p) (snd p)" +definition Frct :: "int \ int \ rat" + where [simp]: "Frct p = Fract (fst p) (snd p)" -lemma [code abstype]: - "Frct (quotient_of q) = q" +lemma [code abstype]: "Frct (quotient_of q) = q" by (cases q) (auto intro: quotient_of_eq) @@ -935,20 +916,17 @@ declare quotient_of_Fract [code abstract] definition of_int :: "int \ rat" -where - [code_abbrev]: "of_int = Int.of_int" + where [code_abbrev]: "of_int = Int.of_int" + hide_const (open) of_int -lemma quotient_of_int [code abstract]: - "quotient_of (Rat.of_int a) = (a, 1)" +lemma quotient_of_int [code abstract]: "quotient_of (Rat.of_int a) = (a, 1)" by (simp add: of_int_def of_int_rat quotient_of_Fract) -lemma [code_unfold]: - "numeral k = Rat.of_int (numeral k)" +lemma [code_unfold]: "numeral k = Rat.of_int (numeral k)" by (simp add: Rat.of_int_def) -lemma [code_unfold]: - "- numeral k = Rat.of_int (- numeral k)" +lemma [code_unfold]: "- numeral k = Rat.of_int (- numeral k)" by (simp add: Rat.of_int_def) lemma Frct_code_post [code_post]: @@ -966,12 +944,10 @@ text \Operations\ -lemma rat_zero_code [code abstract]: - "quotient_of 0 = (0, 1)" +lemma rat_zero_code [code abstract]: "quotient_of 0 = (0, 1)" by (simp add: Zero_rat_def quotient_of_Fract normalize_def) -lemma rat_one_code [code abstract]: - "quotient_of 1 = (1, 1)" +lemma rat_one_code [code abstract]: "quotient_of 1 = (1, 1)" by (simp add: One_rat_def quotient_of_Fract normalize_def) lemma rat_plus_code [code abstract]: @@ -984,54 +960,55 @@ by (cases p) (simp add: quotient_of_Fract) lemma rat_minus_code [code abstract]: - "quotient_of (p - q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + "quotient_of (p - q) = + (let (a, c) = quotient_of p; (b, d) = quotient_of q in normalize (a * d - b * c, c * d))" by (cases p, cases q) (simp add: quotient_of_Fract) lemma rat_times_code [code abstract]: - "quotient_of (p * q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + "quotient_of (p * q) = + (let (a, c) = quotient_of p; (b, d) = quotient_of q in normalize (a * b, c * d))" by (cases p, cases q) (simp add: quotient_of_Fract) lemma rat_inverse_code [code abstract]: - "quotient_of (inverse p) = (let (a, b) = quotient_of p - in if a = 0 then (0, 1) else (sgn a * b, \a\))" + "quotient_of (inverse p) = + (let (a, b) = quotient_of p + in if a = 0 then (0, 1) else (sgn a * b, \a\))" proof (cases p) - case (Fract a b) then show ?thesis + case (Fract a b) + then show ?thesis by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute) qed lemma rat_divide_code [code abstract]: - "quotient_of (p / q) = (let (a, c) = quotient_of p; (b, d) = quotient_of q + "quotient_of (p / q) = + (let (a, c) = quotient_of p; (b, d) = quotient_of q in normalize (a * d, c * b))" by (cases p, cases q) (simp add: quotient_of_Fract) -lemma rat_abs_code [code abstract]: - "quotient_of \p\ = (let (a, b) = quotient_of p in (\a\, b))" +lemma rat_abs_code [code abstract]: "quotient_of \p\ = (let (a, b) = quotient_of p in (\a\, b))" by (cases p) (simp add: quotient_of_Fract) -lemma rat_sgn_code [code abstract]: - "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" +lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)" proof (cases p) - case (Fract a b) then show ?thesis - by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) + case (Fract a b) + then show ?thesis + by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract) qed -lemma rat_floor_code [code]: - "\p\ = (let (a, b) = quotient_of p in a div b)" +lemma rat_floor_code [code]: "\p\ = (let (a, b) = quotient_of p in a div b)" by (cases p) (simp add: quotient_of_Fract floor_Fract) instantiation rat :: equal begin -definition [code]: - "HOL.equal a b \ quotient_of a = quotient_of b" +definition [code]: "HOL.equal a b \ quotient_of a = quotient_of b" -instance proof -qed (simp add: equal_rat_def quotient_of_inject_eq) +instance + by standard (simp add: equal_rat_def quotient_of_inject_eq) -lemma rat_eq_refl [code nbe]: - "HOL.equal (r::rat) r \ True" +lemma rat_eq_refl [code nbe]: "HOL.equal (r::rat) r \ True" by (rule equal_refl) end @@ -1044,16 +1021,16 @@ "p < q \ (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)" by (cases p, cases q) (simp add: quotient_of_Fract mult.commute) -lemma [code]: - "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)" +lemma [code]: "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)" by (cases p) (simp add: quotient_of_Fract of_rat_rat) text \Quickcheck\ definition (in term_syntax) - valterm_fract :: "int \ (unit \ Code_Evaluation.term) \ int \ (unit \ Code_Evaluation.term) \ rat \ (unit \ Code_Evaluation.term)" where - [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\} k {\} l" + valterm_fract :: "int \ (unit \ Code_Evaluation.term) \ int \ (unit \ Code_Evaluation.term) \ + rat \ (unit \ Code_Evaluation.term)" + where [code_unfold]: "valterm_fract k l = Code_Evaluation.valtermify Fract {\} k {\} l" notation fcomp (infixl "\>" 60) notation scomp (infixl "\\" 60) @@ -1062,9 +1039,10 @@ begin definition - "Quickcheck_Random.random i = Quickcheck_Random.random i \\ (\num. Random.range i \\ (\denom. Pair ( - let j = int_of_integer (integer_of_natural (denom + 1)) - in valterm_fract num (j, \u. Code_Evaluation.term_of j))))" + "Quickcheck_Random.random i = + Quickcheck_Random.random i \\ (\num. Random.range i \\ (\denom. Pair + (let j = int_of_integer (integer_of_natural (denom + 1)) + in valterm_fract num (j, \u. Code_Evaluation.term_of j))))" instance .. @@ -1077,8 +1055,10 @@ begin definition - "exhaustive_rat f d = Quickcheck_Exhaustive.exhaustive - (\l. Quickcheck_Exhaustive.exhaustive (\k. f (Fract k (int_of_integer (integer_of_natural l) + 1))) d) d" + "exhaustive_rat f d = + Quickcheck_Exhaustive.exhaustive + (\l. Quickcheck_Exhaustive.exhaustive + (\k. f (Fract k (int_of_integer (integer_of_natural l) + 1))) d) d" instance .. @@ -1088,35 +1068,49 @@ begin definition - "full_exhaustive_rat f d = Quickcheck_Exhaustive.full_exhaustive (%(l, _). Quickcheck_Exhaustive.full_exhaustive (%k. - f (let j = int_of_integer (integer_of_natural l) + 1 - in valterm_fract k (j, %_. Code_Evaluation.term_of j))) d) d" - -instance .. - -end - -instantiation rat :: partial_term_of -begin + "full_exhaustive_rat f d = + Quickcheck_Exhaustive.full_exhaustive + (\(l, _). Quickcheck_Exhaustive.full_exhaustive + (\k. f + (let j = int_of_integer (integer_of_natural l) + 1 + in valterm_fract k (j, \_. Code_Evaluation.term_of j))) d) d" instance .. end +instance rat :: partial_term_of .. + lemma [code]: - "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" - "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) == - Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'') - (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []], - Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))" -by (rule partial_term_of_anything)+ + "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) \ + Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])" + "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) \ + Code_Evaluation.App + (Code_Evaluation.Const (STR ''Rat.Frct'') + (Typerep.Typerep (STR ''fun'') + [Typerep.Typerep (STR ''Product_Type.prod'') + [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []], + Typerep.Typerep (STR ''Rat.rat'') []])) + (Code_Evaluation.App + (Code_Evaluation.App + (Code_Evaluation.Const (STR ''Product_Type.Pair'') + (Typerep.Typerep (STR ''fun'') + [Typerep.Typerep (STR ''Int.int'') [], + Typerep.Typerep (STR ''fun'') + [Typerep.Typerep (STR ''Int.int'') [], + Typerep.Typerep (STR ''Product_Type.prod'') + [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) + (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))" + by (rule partial_term_of_anything)+ instantiation rat :: narrowing begin definition - "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.apply - (Quickcheck_Narrowing.cons (%nom denom. Fract nom denom)) narrowing) narrowing" + "narrowing = + Quickcheck_Narrowing.apply + (Quickcheck_Narrowing.apply + (Quickcheck_Narrowing.cons (\nom denom. Fract nom denom)) narrowing) narrowing" instance .. @@ -1139,7 +1133,8 @@ (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac})] \ -lemmas [nitpick_unfold] = inverse_rat_inst.inverse_rat +lemmas [nitpick_unfold] = + inverse_rat_inst.inverse_rat one_rat_inst.one_rat ord_rat_inst.less_rat ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat @@ -1178,4 +1173,3 @@ lifting_forget rat.lifting end - diff -r 0c89eef79701 -r 83a91a73fcb5 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Mon Jun 20 10:51:34 2016 +0200 +++ b/src/HOL/Rings.thy Mon Jun 20 22:31:16 2016 +0200 @@ -18,10 +18,9 @@ assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c" begin -text\For the \combine_numerals\ simproc\ -lemma combine_common_factor: - "a * e + (b * e + c) = (a + b) * e + c" -by (simp add: distrib_right ac_simps) +text \For the \combine_numerals\ simproc\ +lemma combine_common_factor: "a * e + (b * e + c) = (a + b) * e + c" + by (simp add: distrib_right ac_simps) end @@ -30,8 +29,7 @@ assumes mult_zero_right [simp]: "a * 0 = 0" begin -lemma mult_not_zero: - "a * b \ 0 \ a \ 0 \ b \ 0" +lemma mult_not_zero: "a * b \ 0 \ a \ 0 \ b \ 0" by auto end @@ -45,11 +43,9 @@ proof fix a :: 'a have "0 * a + 0 * a = 0 * a + 0" by (simp add: distrib_right [symmetric]) - thus "0 * a = 0" by (simp only: add_left_cancel) -next - fix a :: 'a + then show "0 * a = 0" by (simp only: add_left_cancel) have "a * 0 + a * 0 = a * 0 + 0" by (simp add: distrib_left [symmetric]) - thus "a * 0 = 0" by (simp only: add_left_cancel) + then show "a * 0 = 0" by (simp only: add_left_cancel) qed end @@ -63,8 +59,8 @@ fix a b c :: 'a show "(a + b) * c = a * c + b * c" by (simp add: distrib) have "a * (b + c) = (b + c) * a" by (simp add: ac_simps) - also have "... = b * a + c * a" by (simp only: distrib) - also have "... = a * b + a * c" by (simp add: ac_simps) + also have "\ = b * a + c * a" by (simp only: distrib) + also have "\ = a * b + a * c" by (simp add: ac_simps) finally show "a * (b + c) = a * b + a * c" by blast qed @@ -91,27 +87,23 @@ begin lemma one_neq_zero [simp]: "1 \ 0" -by (rule not_sym) (rule zero_neq_one) + by (rule not_sym) (rule zero_neq_one) definition of_bool :: "bool \ 'a" -where - "of_bool p = (if p then 1 else 0)" + where "of_bool p = (if p then 1 else 0)" lemma of_bool_eq [simp, code]: "of_bool False = 0" "of_bool True = 1" by (simp_all add: of_bool_def) -lemma of_bool_eq_iff: - "of_bool p = of_bool q \ p = q" +lemma of_bool_eq_iff: "of_bool p = of_bool q \ p = q" by (simp add: of_bool_def) -lemma split_of_bool [split]: - "P (of_bool p) \ (p \ P 1) \ (\ p \ P 0)" +lemma split_of_bool [split]: "P (of_bool p) \ (p \ P 1) \ (\ p \ P 0)" by (cases p) simp_all -lemma split_of_bool_asm: - "P (of_bool p) \ \ (p \ \ P 1 \ \ p \ \ P 0)" +lemma split_of_bool_asm: "P (of_bool p) \ \ (p \ \ P 1 \ \ p \ \ P 0)" by (cases p) simp_all end @@ -123,8 +115,8 @@ class dvd = times begin -definition dvd :: "'a \ 'a \ bool" (infix "dvd" 50) where - "b dvd a \ (\k. a = b * k)" +definition dvd :: "'a \ 'a \ bool" (infix "dvd" 50) + where "b dvd a \ (\k. a = b * k)" lemma dvdI [intro?]: "a = b * k \ b dvd a" unfolding dvd_def .. @@ -139,8 +131,7 @@ subclass dvd . -lemma dvd_refl [simp]: - "a dvd a" +lemma dvd_refl [simp]: "a dvd a" proof show "a = a * 1" by simp qed @@ -155,32 +146,25 @@ then show ?thesis .. qed -lemma subset_divisors_dvd: - "{c. c dvd a} \ {c. c dvd b} \ a dvd b" +lemma subset_divisors_dvd: "{c. c dvd a} \ {c. c dvd b} \ a dvd b" by (auto simp add: subset_iff intro: dvd_trans) -lemma strict_subset_divisors_dvd: - "{c. c dvd a} \ {c. c dvd b} \ a dvd b \ \ b dvd a" +lemma strict_subset_divisors_dvd: "{c. c dvd a} \ {c. c dvd b} \ a dvd b \ \ b dvd a" by (auto simp add: subset_iff intro: dvd_trans) -lemma one_dvd [simp]: - "1 dvd a" +lemma one_dvd [simp]: "1 dvd a" by (auto intro!: dvdI) -lemma dvd_mult [simp]: - "a dvd c \ a dvd (b * c)" +lemma dvd_mult [simp]: "a dvd c \ a dvd (b * c)" by (auto intro!: mult.left_commute dvdI elim!: dvdE) -lemma dvd_mult2 [simp]: - "a dvd b \ a dvd (b * c)" +lemma dvd_mult2 [simp]: "a dvd b \ a dvd (b * c)" using dvd_mult [of a b c] by (simp add: ac_simps) -lemma dvd_triv_right [simp]: - "a dvd b * a" +lemma dvd_triv_right [simp]: "a dvd b * a" by (rule dvd_mult) (rule dvd_refl) -lemma dvd_triv_left [simp]: - "a dvd a * b" +lemma dvd_triv_left [simp]: "a dvd a * b" by (rule dvd_mult2) (rule dvd_refl) lemma mult_dvd_mono: @@ -194,12 +178,10 @@ then show ?thesis .. qed -lemma dvd_mult_left: - "a * b dvd c \ a dvd c" +lemma dvd_mult_left: "a * b dvd c \ a dvd c" by (simp add: dvd_def mult.assoc) blast -lemma dvd_mult_right: - "a * b dvd c \ b dvd c" +lemma dvd_mult_right: "a * b dvd c \ b dvd c" using dvd_mult_left [of b a c] by (simp add: ac_simps) end @@ -209,18 +191,15 @@ subclass semiring_1 .. -lemma dvd_0_left_iff [simp]: - "0 dvd a \ a = 0" +lemma dvd_0_left_iff [simp]: "0 dvd a \ a = 0" by (auto intro: dvd_refl elim!: dvdE) -lemma dvd_0_right [iff]: - "a dvd 0" +lemma dvd_0_right [iff]: "a dvd 0" proof show "0 = a * 0" by simp qed -lemma dvd_0_left: - "0 dvd a \ a = 0" +lemma dvd_0_left: "0 dvd a \ a = 0" by simp lemma dvd_add [simp]: @@ -245,8 +224,8 @@ end -class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add + - zero_neq_one + comm_monoid_mult + +class comm_semiring_1_cancel = + comm_semiring + cancel_comm_monoid_add + zero_neq_one + comm_monoid_mult + assumes right_diff_distrib' [algebra_simps]: "a * (b - c) = a * b - a * c" begin @@ -254,16 +233,15 @@ subclass comm_semiring_0_cancel .. subclass comm_semiring_1 .. -lemma left_diff_distrib' [algebra_simps]: - "(b - c) * a = b * a - c * a" +lemma left_diff_distrib' [algebra_simps]: "(b - c) * a = b * a - c * a" by (simp add: algebra_simps) -lemma dvd_add_times_triv_left_iff [simp]: - "a dvd c * a + b \ a dvd b" +lemma dvd_add_times_triv_left_iff [simp]: "a dvd c * a + b \ a dvd b" proof - have "a dvd a * c + b \ a dvd b" (is "?P \ ?Q") proof - assume ?Q then show ?P by simp + assume ?Q + then show ?P by simp next assume ?P then obtain d where "a * c + b = a * d" .. @@ -275,23 +253,21 @@ then show "a dvd c * a + b \ a dvd b" by (simp add: ac_simps) qed -lemma dvd_add_times_triv_right_iff [simp]: - "a dvd b + c * a \ a dvd b" +lemma dvd_add_times_triv_right_iff [simp]: "a dvd b + c * a \ a dvd b" using dvd_add_times_triv_left_iff [of a c b] by (simp add: ac_simps) -lemma dvd_add_triv_left_iff [simp]: - "a dvd a + b \ a dvd b" +lemma dvd_add_triv_left_iff [simp]: "a dvd a + b \ a dvd b" using dvd_add_times_triv_left_iff [of a 1 b] by simp -lemma dvd_add_triv_right_iff [simp]: - "a dvd b + a \ a dvd b" +lemma dvd_add_triv_right_iff [simp]: "a dvd b + a \ a dvd b" using dvd_add_times_triv_right_iff [of a b 1] by simp lemma dvd_add_right_iff: assumes "a dvd b" shows "a dvd b + c \ a dvd c" (is "?P \ ?Q") proof - assume ?P then obtain d where "b + c = a * d" .. + assume ?P + then obtain d where "b + c = a * d" .. moreover from \a dvd b\ obtain e where "b = a * e" .. ultimately have "a * e + c = a * d" by simp then have "a * e + c - a * e = a * d - a * e" by simp @@ -299,13 +275,12 @@ then have "c = a * (d - e)" by (simp add: algebra_simps) then show ?Q .. next - assume ?Q with assms show ?P by simp + assume ?Q + with assms show ?P by simp qed -lemma dvd_add_left_iff: - assumes "a dvd c" - shows "a dvd b + c \ a dvd b" - using assms dvd_add_right_iff [of a c b] by (simp add: ac_simps) +lemma dvd_add_left_iff: "a dvd c \ a dvd b + c \ a dvd b" + using dvd_add_right_iff [of a c b] by (simp add: ac_simps) end @@ -317,44 +292,38 @@ text \Distribution rules\ lemma minus_mult_left: "- (a * b) = - a * b" -by (rule minus_unique) (simp add: distrib_right [symmetric]) + by (rule minus_unique) (simp add: distrib_right [symmetric]) lemma minus_mult_right: "- (a * b) = a * - b" -by (rule minus_unique) (simp add: distrib_left [symmetric]) + by (rule minus_unique) (simp add: distrib_left [symmetric]) -text\Extract signs from products\ +text \Extract signs from products\ lemmas mult_minus_left [simp] = minus_mult_left [symmetric] lemmas mult_minus_right [simp] = minus_mult_right [symmetric] lemma minus_mult_minus [simp]: "- a * - b = a * b" -by simp + by simp lemma minus_mult_commute: "- a * b = a * - b" -by simp + by simp -lemma right_diff_distrib [algebra_simps]: - "a * (b - c) = a * b - a * c" +lemma right_diff_distrib [algebra_simps]: "a * (b - c) = a * b - a * c" using distrib_left [of a b "-c "] by simp -lemma left_diff_distrib [algebra_simps]: - "(a - b) * c = a * c - b * c" +lemma left_diff_distrib [algebra_simps]: "(a - b) * c = a * c - b * c" using distrib_right [of a "- b" c] by simp -lemmas ring_distribs = - distrib_left distrib_right left_diff_distrib right_diff_distrib +lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib -lemma eq_add_iff1: - "a * e + c = b * e + d \ (a - b) * e + c = d" -by (simp add: algebra_simps) +lemma eq_add_iff1: "a * e + c = b * e + d \ (a - b) * e + c = d" + by (simp add: algebra_simps) -lemma eq_add_iff2: - "a * e + c = b * e + d \ c = (b - a) * e + d" -by (simp add: algebra_simps) +lemma eq_add_iff2: "a * e + c = b * e + d \ c = (b - a) * e + d" + by (simp add: algebra_simps) end -lemmas ring_distribs = - distrib_left distrib_right left_diff_distrib right_diff_distrib +lemmas ring_distribs = distrib_left distrib_right left_diff_distrib right_diff_distrib class comm_ring = comm_semiring + ab_group_add begin @@ -362,8 +331,7 @@ subclass ring .. subclass comm_semiring_0_cancel .. -lemma square_diff_square_factored: - "x * x - y * y = (x + y) * (x - y)" +lemma square_diff_square_factored: "x * x - y * y = (x + y) * (x - y)" by (simp add: algebra_simps) end @@ -373,8 +341,7 @@ subclass semiring_1_cancel .. -lemma square_diff_one_factored: - "x * x - 1 = (x + 1) * (x - 1)" +lemma square_diff_one_factored: "x * x - 1 = (x + 1) * (x - 1)" by (simp add: algebra_simps) end @@ -410,8 +377,7 @@ then show "- x dvd y" .. qed -lemma dvd_diff [simp]: - "x dvd y \ x dvd z \ x dvd (y - z)" +lemma dvd_diff [simp]: "x dvd y \ x dvd z \ x dvd (y - z)" using dvd_add [of x y "- z"] by simp end @@ -424,19 +390,20 @@ assumes "a * b = 0" shows "a = 0 \ b = 0" proof (rule classical) - assume "\ (a = 0 \ b = 0)" + assume "\ ?thesis" then have "a \ 0" and "b \ 0" by auto with no_zero_divisors have "a * b \ 0" by blast with assms show ?thesis by simp qed -lemma mult_eq_0_iff [simp]: - shows "a * b = 0 \ a = 0 \ b = 0" +lemma mult_eq_0_iff [simp]: "a * b = 0 \ a = 0 \ b = 0" proof (cases "a = 0 \ b = 0") - case False then have "a \ 0" and "b \ 0" by auto + case False + then have "a \ 0" and "b \ 0" by auto then show ?thesis using no_zero_divisors by simp next - case True then show ?thesis by auto + case True + then show ?thesis by auto qed end @@ -448,12 +415,10 @@ and mult_cancel_left [simp]: "c * a = c * b \ c = 0 \ a = b" begin -lemma mult_left_cancel: - "c \ 0 \ c * a = c * b \ a = b" +lemma mult_left_cancel: "c \ 0 \ c * a = c * b \ a = b" by simp -lemma mult_right_cancel: - "c \ 0 \ a * c = b * c \ a = b" +lemma mult_right_cancel: "c \ 0 \ a * c = b * c \ a = b" by simp end @@ -483,32 +448,27 @@ subclass semiring_1_no_zero_divisors .. -lemma square_eq_1_iff: - "x * x = 1 \ x = 1 \ x = - 1" +lemma square_eq_1_iff: "x * x = 1 \ x = 1 \ x = - 1" proof - have "(x - 1) * (x + 1) = x * x - 1" by (simp add: algebra_simps) - hence "x * x = 1 \ (x - 1) * (x + 1) = 0" + then have "x * x = 1 \ (x - 1) * (x + 1) = 0" by simp - thus ?thesis + then show ?thesis by (simp add: eq_neg_iff_add_eq_0) qed -lemma mult_cancel_right1 [simp]: - "c = b * c \ c = 0 \ b = 1" -by (insert mult_cancel_right [of 1 c b], force) +lemma mult_cancel_right1 [simp]: "c = b * c \ c = 0 \ b = 1" + using mult_cancel_right [of 1 c b] by auto -lemma mult_cancel_right2 [simp]: - "a * c = c \ c = 0 \ a = 1" -by (insert mult_cancel_right [of a c 1], simp) +lemma mult_cancel_right2 [simp]: "a * c = c \ c = 0 \ a = 1" + using mult_cancel_right [of a c 1] by simp -lemma mult_cancel_left1 [simp]: - "c = c * b \ c = 0 \ b = 1" -by (insert mult_cancel_left [of c 1 b], force) +lemma mult_cancel_left1 [simp]: "c = c * b \ c = 0 \ b = 1" + using mult_cancel_left [of c 1 b] by force -lemma mult_cancel_left2 [simp]: - "c * a = c \ c = 0 \ a = 1" -by (insert mult_cancel_left [of c a 1], simp) +lemma mult_cancel_left2 [simp]: "c * a = c \ c = 0 \ a = 1" + using mult_cancel_left [of c a 1] by simp end @@ -526,8 +486,7 @@ subclass ring_1_no_zero_divisors .. -lemma dvd_mult_cancel_right [simp]: - "a * c dvd b * c \ c = 0 \ a dvd b" +lemma dvd_mult_cancel_right [simp]: "a * c dvd b * c \ c = 0 \ a dvd b" proof - have "a * c dvd b * c \ (\k. b * c = (a * k) * c)" unfolding dvd_def by (simp add: ac_simps) @@ -536,8 +495,7 @@ finally show ?thesis . qed -lemma dvd_mult_cancel_left [simp]: - "c * a dvd c * b \ c = 0 \ a dvd b" +lemma dvd_mult_cancel_left [simp]: "c * a dvd c * b \ c = 0 \ a dvd b" proof - have "c * a dvd c * b \ (\k. b * c = (a * k) * c)" unfolding dvd_def by (simp add: ac_simps) @@ -562,15 +520,12 @@ text \ The theory of partially ordered rings is taken from the books: - \begin{itemize} - \item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 - \item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 - \end{itemize} + \<^item> \<^emph>\Lattice Theory\ by Garret Birkhoff, American Mathematical Society, 1979 + \<^item> \<^emph>\Partially Ordered Algebraic Systems\, Pergamon Press, 1963 + Most of the used notions can also be looked up in - \begin{itemize} - \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al. - \item \emph{Algebra I} by van der Waerden, Springer. - \end{itemize} + \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al. + \<^item> \<^emph>\Algebra I\ by van der Waerden, Springer \ class divide = @@ -605,49 +560,45 @@ assumes divide_zero [simp]: "a div 0 = 0" begin -lemma nonzero_mult_divide_cancel_left [simp]: - "a \ 0 \ (a * b) div a = b" +lemma nonzero_mult_divide_cancel_left [simp]: "a \ 0 \ (a * b) div a = b" using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps) subclass semiring_no_zero_divisors_cancel proof - fix a b c - { fix a b c - show "a * c = b * c \ c = 0 \ a = b" - proof (cases "c = 0") - case True then show ?thesis by simp - next - case False - { assume "a * c = b * c" - then have "a * c div c = b * c div c" - by simp - with False have "a = b" - by simp - } then show ?thesis by auto - qed - } - from this [of a c b] - show "c * a = c * b \ c = 0 \ a = b" - by (simp add: ac_simps) + show *: "a * c = b * c \ c = 0 \ a = b" for a b c + proof (cases "c = 0") + case True + then show ?thesis by simp + next + case False + { + assume "a * c = b * c" + then have "a * c div c = b * c div c" + by simp + with False have "a = b" + by simp + } + then show ?thesis by auto + qed + show "c * a = c * b \ c = 0 \ a = b" for a b c + using * [of a c b] by (simp add: ac_simps) qed -lemma div_self [simp]: - assumes "a \ 0" - shows "a div a = 1" - using assms nonzero_mult_divide_cancel_left [of a 1] by simp +lemma div_self [simp]: "a \ 0 \ a div a = 1" + using nonzero_mult_divide_cancel_left [of a 1] by simp -lemma divide_zero_left [simp]: - "0 div a = 0" +lemma divide_zero_left [simp]: "0 div a = 0" proof (cases "a = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next - case False then have "a * 0 div a = 0" + case False + then have "a * 0 div a = 0" by (rule nonzero_mult_divide_cancel_left) then show ?thesis by simp qed -lemma divide_1 [simp]: - "a div 1 = a" +lemma divide_1 [simp]: "a div 1 = a" using nonzero_mult_divide_cancel_left [of 1 a] by simp end @@ -668,11 +619,13 @@ assumes "a \ 0" shows "a * b dvd a * c \ b dvd c" (is "?P \ ?Q") proof - assume ?P then obtain d where "a * c = a * b * d" .. + assume ?P + then obtain d where "a * c = a * b * d" .. with assms have "c = b * d" by (simp add: ac_simps) then show ?Q .. next - assume ?Q then obtain d where "c = b * d" .. + assume ?Q + then obtain d where "c = b * d" .. then have "a * c = a * b * d" by (simp add: ac_simps) then show ?P .. qed @@ -680,7 +633,7 @@ lemma dvd_times_right_cancel_iff [simp]: assumes "a \ 0" shows "b * a dvd c * a \ b dvd c" (is "?P \ ?Q") -using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) + using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps) lemma div_dvd_iff_mult: assumes "b \ 0" and "b dvd a" @@ -702,7 +655,8 @@ assumes "a dvd b" and "a dvd c" shows "b div a dvd c div a \ b dvd c" proof (cases "a = 0") - case True with assms show ?thesis by simp + case True + with assms show ?thesis by simp next case False moreover from assms obtain k l where "b = a * k" and "c = a * l" @@ -714,7 +668,8 @@ assumes "c dvd a" and "c dvd b" shows "(a + b) div c = a div c + b div c" proof (cases "c = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next case False moreover from assms obtain k l where "a = c * k" and "b = c * l" @@ -729,7 +684,8 @@ assumes "b dvd a" and "d dvd c" shows "(a div b) * (c div d) = (a * c) div (b * d)" proof (cases "b = 0 \ c = 0") - case True with assms show ?thesis by auto + case True + with assms show ?thesis by auto next case False moreover from assms obtain k l where "a = b * k" and "c = d * l" @@ -748,42 +704,39 @@ next assume "b div a = c" then have "b div a * a = c * a" by simp - moreover from \a \ 0\ \a dvd b\ have "b div a * a = b" + moreover from assms have "b div a * a = b" by (auto elim!: dvdE simp add: ac_simps) ultimately show "b = c * a" by simp qed -lemma dvd_div_mult_self [simp]: - "a dvd b \ b div a * a = b" +lemma dvd_div_mult_self [simp]: "a dvd b \ b div a * a = b" by (cases "a = 0") (auto elim: dvdE simp add: ac_simps) -lemma dvd_mult_div_cancel [simp]: - "a dvd b \ a * (b div a) = b" +lemma dvd_mult_div_cancel [simp]: "a dvd b \ a * (b div a) = b" using dvd_div_mult_self [of a b] by (simp add: ac_simps) lemma div_mult_swap: assumes "c dvd b" shows "a * (b div c) = (a * b) div c" proof (cases "c = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next - case False from assms obtain d where "b = c * d" .. + case False + from assms obtain d where "b = c * d" .. moreover from False have "a * divide (d * c) c = ((a * d) * c) div c" by simp ultimately show ?thesis by (simp add: ac_simps) qed -lemma dvd_div_mult: - assumes "c dvd b" - shows "b div c * a = (b * a) div c" - using assms div_mult_swap [of c b a] by (simp add: ac_simps) +lemma dvd_div_mult: "c dvd b \ b div c * a = (b * a) div c" + using div_mult_swap [of c b a] by (simp add: ac_simps) lemma dvd_div_mult2_eq: assumes "b * c dvd a" shows "a div (b * c) = a div b div c" -using assms proof - fix k - assume "a = b * c * k" +proof - + from assms obtain k where "a = b * c * k" .. then show ?thesis by (cases "b = 0 \ c = 0") (auto, simp add: ac_simps) qed @@ -808,15 +761,12 @@ text \Units: invertible elements in a ring\ abbreviation is_unit :: "'a \ bool" -where - "is_unit a \ a dvd 1" + where "is_unit a \ a dvd 1" -lemma not_is_unit_0 [simp]: - "\ is_unit 0" +lemma not_is_unit_0 [simp]: "\ is_unit 0" by simp -lemma unit_imp_dvd [dest]: - "is_unit b \ b dvd a" +lemma unit_imp_dvd [dest]: "is_unit b \ b dvd a" by (rule dvd_trans [of _ 1]) simp_all lemma unit_dvdE: @@ -829,8 +779,7 @@ ultimately show thesis using that by blast qed -lemma dvd_unit_imp_unit: - "a dvd b \ is_unit b \ is_unit a" +lemma dvd_unit_imp_unit: "a dvd b \ is_unit b \ is_unit a" by (rule dvd_trans) lemma unit_div_1_unit [simp, intro]: @@ -849,27 +798,24 @@ proof (rule that) define b where "b = 1 div a" then show "1 div a = b" by simp - from b_def \is_unit a\ show "is_unit b" by simp - from \is_unit a\ and \is_unit b\ show "a \ 0" and "b \ 0" by auto - from b_def \is_unit a\ show "a * b = 1" by simp + from assms b_def show "is_unit b" by simp + with assms show "a \ 0" and "b \ 0" by auto + from assms b_def show "a * b = 1" by simp then have "1 = a * b" .. with b_def \b \ 0\ show "1 div b = a" by simp - from \is_unit a\ have "a dvd c" .. + from assms have "a dvd c" .. then obtain d where "c = a * d" .. with \a \ 0\ \a * b = 1\ show "c div a = c * b" by (simp add: mult.assoc mult.left_commute [of a]) qed -lemma unit_prod [intro]: - "is_unit a \ is_unit b \ is_unit (a * b)" +lemma unit_prod [intro]: "is_unit a \ is_unit b \ is_unit (a * b)" by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) -lemma is_unit_mult_iff: - "is_unit (a * b) \ is_unit a \ is_unit b" (is "?P \ ?Q") +lemma is_unit_mult_iff: "is_unit (a * b) \ is_unit a \ is_unit b" by (auto dest: dvd_mult_left dvd_mult_right) -lemma unit_div [intro]: - "is_unit a \ is_unit b \ is_unit (a div b)" +lemma unit_div [intro]: "is_unit a \ is_unit b \ is_unit (a div b)" by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod) lemma mult_unit_dvd_iff: @@ -894,7 +840,8 @@ assume "a dvd c * b" with assms have "c * b dvd c * (b * (1 div b))" by (subst mult_assoc [symmetric]) simp - also from \is_unit b\ have "b * (1 div b) = 1" by (rule is_unitE) simp + also from assms have "b * (1 div b) = 1" + by (rule is_unitE) simp finally have "c * b dvd c" by simp with \a dvd c * b\ show "a dvd c" by (rule dvd_trans) next @@ -902,52 +849,40 @@ then show "a dvd c * b" by simp qed -lemma div_unit_dvd_iff: - "is_unit b \ a div b dvd c \ a dvd c" +lemma div_unit_dvd_iff: "is_unit b \ a div b dvd c \ a dvd c" by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff) -lemma dvd_div_unit_iff: - "is_unit b \ a dvd c div b \ a dvd c" +lemma dvd_div_unit_iff: "is_unit b \ a dvd c div b \ a dvd c" by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff) lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff - dvd_mult_unit_iff dvd_div_unit_iff \ \FIXME consider fact collection\ + dvd_mult_unit_iff dvd_div_unit_iff (* FIXME consider named_theorems *) -lemma unit_mult_div_div [simp]: - "is_unit a \ b * (1 div a) = b div a" +lemma unit_mult_div_div [simp]: "is_unit a \ b * (1 div a) = b div a" by (erule is_unitE [of _ b]) simp -lemma unit_div_mult_self [simp]: - "is_unit a \ b div a * a = b" +lemma unit_div_mult_self [simp]: "is_unit a \ b div a * a = b" by (rule dvd_div_mult_self) auto -lemma unit_div_1_div_1 [simp]: - "is_unit a \ 1 div (1 div a) = a" +lemma unit_div_1_div_1 [simp]: "is_unit a \ 1 div (1 div a) = a" by (erule is_unitE) simp -lemma unit_div_mult_swap: - "is_unit c \ a * (b div c) = (a * b) div c" +lemma unit_div_mult_swap: "is_unit c \ a * (b div c) = (a * b) div c" by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c]) -lemma unit_div_commute: - "is_unit b \ (a div b) * c = (a * c) div b" +lemma unit_div_commute: "is_unit b \ (a div b) * c = (a * c) div b" using unit_div_mult_swap [of b c a] by (simp add: ac_simps) -lemma unit_eq_div1: - "is_unit b \ a div b = c \ a = c * b" +lemma unit_eq_div1: "is_unit b \ a div b = c \ a = c * b" by (auto elim: is_unitE) -lemma unit_eq_div2: - "is_unit b \ a = c div b \ a * b = c" +lemma unit_eq_div2: "is_unit b \ a = c div b \ a * b = c" using unit_eq_div1 [of b c a] by auto -lemma unit_mult_left_cancel: - assumes "is_unit a" - shows "a * b = a * c \ b = c" (is "?P \ ?Q") - using assms mult_cancel_left [of a b c] by auto +lemma unit_mult_left_cancel: "is_unit a \ a * b = a * c \ b = c" + using mult_cancel_left [of a b c] by auto -lemma unit_mult_right_cancel: - "is_unit a \ b * a = c * a \ b = c" +lemma unit_mult_right_cancel: "is_unit a \ b * a = c * a \ b = c" using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps) lemma unit_div_cancel: @@ -964,7 +899,8 @@ assumes "is_unit b" and "is_unit c" shows "a div (b * c) = a div b div c" proof - - from assms have "is_unit (b * c)" by (simp add: unit_prod) + from assms have "is_unit (b * c)" + by (simp add: unit_prod) then have "b * c dvd a" by (rule unit_imp_dvd) then show ?thesis @@ -1015,58 +951,57 @@ values rather than associated elements. \ -lemma unit_factor_dvd [simp]: - "a \ 0 \ unit_factor a dvd b" +lemma unit_factor_dvd [simp]: "a \ 0 \ unit_factor a dvd b" by (rule unit_imp_dvd) simp -lemma unit_factor_self [simp]: - "unit_factor a dvd a" +lemma unit_factor_self [simp]: "unit_factor a dvd a" by (cases "a = 0") simp_all -lemma normalize_mult_unit_factor [simp]: - "normalize a * unit_factor a = a" +lemma normalize_mult_unit_factor [simp]: "normalize a * unit_factor a = a" using unit_factor_mult_normalize [of a] by (simp add: ac_simps) -lemma normalize_eq_0_iff [simp]: - "normalize a = 0 \ a = 0" (is "?P \ ?Q") +lemma normalize_eq_0_iff [simp]: "normalize a = 0 \ a = 0" + (is "?P \ ?Q") proof assume ?P moreover have "unit_factor a * normalize a = a" by simp ultimately show ?Q by simp next - assume ?Q then show ?P by simp + assume ?Q + then show ?P by simp qed -lemma unit_factor_eq_0_iff [simp]: - "unit_factor a = 0 \ a = 0" (is "?P \ ?Q") +lemma unit_factor_eq_0_iff [simp]: "unit_factor a = 0 \ a = 0" + (is "?P \ ?Q") proof assume ?P moreover have "unit_factor a * normalize a = a" by simp ultimately show ?Q by simp next - assume ?Q then show ?P by simp + assume ?Q + then show ?P by simp qed lemma is_unit_unit_factor: - assumes "is_unit a" shows "unit_factor a = a" + assumes "is_unit a" + shows "unit_factor a = a" proof - from assms have "normalize a = 1" by (rule is_unit_normalize) moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" . ultimately show ?thesis by simp qed -lemma unit_factor_1 [simp]: - "unit_factor 1 = 1" +lemma unit_factor_1 [simp]: "unit_factor 1 = 1" by (rule is_unit_unit_factor) simp -lemma normalize_1 [simp]: - "normalize 1 = 1" +lemma normalize_1 [simp]: "normalize 1 = 1" by (rule is_unit_normalize) simp -lemma normalize_1_iff: - "normalize a = 1 \ is_unit a" (is "?P \ ?Q") +lemma normalize_1_iff: "normalize a = 1 \ is_unit a" + (is "?P \ ?Q") proof - assume ?Q then show ?P by (rule is_unit_normalize) + assume ?Q + then show ?P by (rule is_unit_normalize) next assume ?P then have "a \ 0" by auto @@ -1079,32 +1014,34 @@ ultimately show ?Q by simp qed -lemma div_normalize [simp]: - "a div normalize a = unit_factor a" +lemma div_normalize [simp]: "a div normalize a = unit_factor a" proof (cases "a = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next - case False then have "normalize a \ 0" by simp + case False + then have "normalize a \ 0" by simp with nonzero_mult_divide_cancel_right have "unit_factor a * normalize a div normalize a = unit_factor a" by blast then show ?thesis by simp qed -lemma div_unit_factor [simp]: - "a div unit_factor a = normalize a" +lemma div_unit_factor [simp]: "a div unit_factor a = normalize a" proof (cases "a = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next - case False then have "unit_factor a \ 0" by simp + case False + then have "unit_factor a \ 0" by simp with nonzero_mult_divide_cancel_left have "unit_factor a * normalize a div unit_factor a = normalize a" by blast then show ?thesis by simp qed -lemma normalize_div [simp]: - "normalize a div a = 1 div unit_factor a" +lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a" proof (cases "a = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next case False have "normalize a div a = normalize a div (unit_factor a * normalize a)" @@ -1114,62 +1051,64 @@ finally show ?thesis . qed -lemma mult_one_div_unit_factor [simp]: - "a * (1 div unit_factor b) = a div unit_factor b" +lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b" by (cases "b = 0") simp_all -lemma normalize_mult: - "normalize (a * b) = normalize a * normalize b" +lemma normalize_mult: "normalize (a * b) = normalize a * normalize b" proof (cases "a = 0 \ b = 0") - case True then show ?thesis by auto + case True + then show ?thesis by auto next case False from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" . - then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp - also have "\ = a * b div unit_factor (b * a)" by (simp add: ac_simps) + then have "normalize (a * b) = a * b div unit_factor (a * b)" + by simp + also have "\ = a * b div unit_factor (b * a)" + by (simp add: ac_simps) also have "\ = a * b div unit_factor b div unit_factor a" using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric]) also have "\ = a * (b div unit_factor b) div unit_factor a" using False by (subst unit_div_mult_swap) simp_all also have "\ = normalize a * normalize b" - using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) + using False + by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric]) finally show ?thesis . qed -lemma unit_factor_idem [simp]: - "unit_factor (unit_factor a) = unit_factor a" +lemma unit_factor_idem [simp]: "unit_factor (unit_factor a) = unit_factor a" by (cases "a = 0") (auto intro: is_unit_unit_factor) -lemma normalize_unit_factor [simp]: - "a \ 0 \ normalize (unit_factor a) = 1" +lemma normalize_unit_factor [simp]: "a \ 0 \ normalize (unit_factor a) = 1" by (rule is_unit_normalize) simp -lemma normalize_idem [simp]: - "normalize (normalize a) = normalize a" +lemma normalize_idem [simp]: "normalize (normalize a) = normalize a" proof (cases "a = 0") - case True then show ?thesis by simp + case True + then show ?thesis by simp next case False - have "normalize a = normalize (unit_factor a * normalize a)" by simp + have "normalize a = normalize (unit_factor a * normalize a)" + by simp also have "\ = normalize (unit_factor a) * normalize (normalize a)" by (simp only: normalize_mult) - finally show ?thesis using False by simp_all + finally show ?thesis + using False by simp_all qed lemma unit_factor_normalize [simp]: assumes "a \ 0" shows "unit_factor (normalize a) = 1" proof - - from assms have "normalize a \ 0" by simp + from assms have *: "normalize a \ 0" + by simp have "unit_factor (normalize a) * normalize (normalize a) = normalize a" by (simp only: unit_factor_mult_normalize) then have "unit_factor (normalize a) * normalize a = normalize a" by simp - with \normalize a \ 0\ - have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" + with * have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a" by simp - with \normalize a \ 0\ - show ?thesis by simp + with * show ?thesis + by simp qed lemma dvd_unit_factor_div: @@ -1196,8 +1135,7 @@ by (cases "b = 0") (simp_all add: normalize_mult) qed -lemma normalize_dvd_iff [simp]: - "normalize a dvd b \ a dvd b" +lemma normalize_dvd_iff [simp]: "normalize a dvd b \ a dvd b" proof - have "normalize a dvd b \ unit_factor a * normalize a dvd b" using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b] @@ -1205,8 +1143,7 @@ then show ?thesis by simp qed -lemma dvd_normalize_iff [simp]: - "a dvd normalize b \ a dvd b" +lemma dvd_normalize_iff [simp]: "a dvd normalize b \ a dvd b" proof - have "a dvd normalize b \ a dvd normalize b * unit_factor b" using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"] @@ -1226,36 +1163,38 @@ assumes "a dvd b" and "b dvd a" shows "normalize a = normalize b" proof (cases "a = 0 \ b = 0") - case True with assms show ?thesis by auto + case True + with assms show ?thesis by auto next case False from \a dvd b\ obtain c where b: "b = a * c" .. moreover from \b dvd a\ obtain d where a: "a = b * d" .. - ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps) + ultimately have "b * 1 = b * (c * d)" + by (simp add: ac_simps) with False have "1 = c * d" unfolding mult_cancel_left by simp - then have "is_unit c" and "is_unit d" by auto - with a b show ?thesis by (simp add: normalize_mult is_unit_normalize) + then have "is_unit c" and "is_unit d" + by auto + with a b show ?thesis + by (simp add: normalize_mult is_unit_normalize) qed -lemma associatedD1: - "normalize a = normalize b \ a dvd b" +lemma associatedD1: "normalize a = normalize b \ a dvd b" using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric] by simp -lemma associatedD2: - "normalize a = normalize b \ b dvd a" +lemma associatedD2: "normalize a = normalize b \ b dvd a" using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric] by simp -lemma associated_unit: - "normalize a = normalize b \ is_unit a \ is_unit b" +lemma associated_unit: "normalize a = normalize b \ is_unit a \ is_unit b" using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2) -lemma associated_iff_dvd: - "normalize a = normalize b \ a dvd b \ b dvd a" (is "?P \ ?Q") +lemma associated_iff_dvd: "normalize a = normalize b \ a dvd b \ b dvd a" + (is "?P \ ?Q") proof - assume ?Q then show ?P by (auto intro!: associatedI) + assume ?Q + then show ?P by (auto intro!: associatedI) next assume ?P then have "unit_factor a * normalize a = unit_factor a * normalize b" @@ -1264,7 +1203,8 @@ by (simp add: ac_simps) show ?Q proof (cases "a = 0 \ b = 0") - case True with \?P\ show ?thesis by auto + case True + with \?P\ show ?thesis by auto next case False then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b" @@ -1291,38 +1231,38 @@ assumes mult_right_mono: "a \ b \ 0 \ c \ a * c \ b * c" begin -lemma mult_mono: - "a \ b \ c \ d \ 0 \ b \ 0 \ c \ a * c \ b * d" -apply (erule mult_right_mono [THEN order_trans], assumption) -apply (erule mult_left_mono, assumption) -done +lemma mult_mono: "a \ b \ c \ d \ 0 \ b \ 0 \ c \ a * c \ b * d" + apply (erule (1) mult_right_mono [THEN order_trans]) + apply (erule (1) mult_left_mono) + done -lemma mult_mono': - "a \ b \ c \ d \ 0 \ a \ 0 \ c \ a * c \ b * d" -apply (rule mult_mono) -apply (fast intro: order_trans)+ -done +lemma mult_mono': "a \ b \ c \ d \ 0 \ a \ 0 \ c \ a * c \ b * d" + apply (rule mult_mono) + apply (fast intro: order_trans)+ + done end class ordered_semiring_0 = semiring_0 + ordered_semiring begin -lemma mult_nonneg_nonneg[simp]: "0 \ a \ 0 \ b \ 0 \ a * b" -using mult_left_mono [of 0 b a] by simp +lemma mult_nonneg_nonneg [simp]: "0 \ a \ 0 \ b \ 0 \ a * b" + using mult_left_mono [of 0 b a] by simp lemma mult_nonneg_nonpos: "0 \ a \ b \ 0 \ a * b \ 0" -using mult_left_mono [of b 0 a] by simp + using mult_left_mono [of b 0 a] by simp lemma mult_nonpos_nonneg: "a \ 0 \ 0 \ b \ a * b \ 0" -using mult_right_mono [of a 0 b] by simp + using mult_right_mono [of a 0 b] by simp text \Legacy - use \mult_nonpos_nonneg\\ lemma mult_nonneg_nonpos2: "0 \ a \ b \ 0 \ b * a \ 0" -by (drule mult_right_mono [of b 0], auto) + apply (drule mult_right_mono [of b 0]) + apply auto + done lemma split_mult_neg_le: "(0 \ a \ b \ 0) \ (a \ 0 \ 0 \ b) \ a * b \ 0" -by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) + by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2) end @@ -1341,44 +1281,34 @@ subclass ordered_cancel_comm_monoid_add .. -lemma mult_left_less_imp_less: - "c * a < c * b \ 0 \ c \ a < b" -by (force simp add: mult_left_mono not_le [symmetric]) +lemma mult_left_less_imp_less: "c * a < c * b \ 0 \ c \ a < b" + by (force simp add: mult_left_mono not_le [symmetric]) -lemma mult_right_less_imp_less: - "a * c < b * c \ 0 \ c \ a < b" -by (force simp add: mult_right_mono not_le [symmetric]) +lemma mult_right_less_imp_less: "a * c < b * c \ 0 \ c \ a < b" + by (force simp add: mult_right_mono not_le [symmetric]) -lemma less_eq_add_cancel_left_greater_eq_zero [simp]: - "a \ a + b \ 0 \ b" +lemma less_eq_add_cancel_left_greater_eq_zero [simp]: "a \ a + b \ 0 \ b" using add_le_cancel_left [of a 0 b] by simp -lemma less_eq_add_cancel_left_less_eq_zero [simp]: - "a + b \ a \ b \ 0" +lemma less_eq_add_cancel_left_less_eq_zero [simp]: "a + b \ a \ b \ 0" using add_le_cancel_left [of a b 0] by simp -lemma less_eq_add_cancel_right_greater_eq_zero [simp]: - "a \ b + a \ 0 \ b" +lemma less_eq_add_cancel_right_greater_eq_zero [simp]: "a \ b + a \ 0 \ b" using add_le_cancel_right [of 0 a b] by simp -lemma less_eq_add_cancel_right_less_eq_zero [simp]: - "b + a \ a \ b \ 0" +lemma less_eq_add_cancel_right_less_eq_zero [simp]: "b + a \ a \ b \ 0" using add_le_cancel_right [of b a 0] by simp -lemma less_add_cancel_left_greater_zero [simp]: - "a < a + b \ 0 < b" +lemma less_add_cancel_left_greater_zero [simp]: "a < a + b \ 0 < b" using add_less_cancel_left [of a 0 b] by simp -lemma less_add_cancel_left_less_zero [simp]: - "a + b < a \ b < 0" +lemma less_add_cancel_left_less_zero [simp]: "a + b < a \ b < 0" using add_less_cancel_left [of a b 0] by simp -lemma less_add_cancel_right_greater_zero [simp]: - "a < b + a \ 0 < b" +lemma less_add_cancel_right_greater_zero [simp]: "a < b + a \ 0 < b" using add_less_cancel_right [of 0 a b] by simp -lemma less_add_cancel_right_less_zero [simp]: - "b + a < a \ b < 0" +lemma less_add_cancel_right_less_zero [simp]: "b + a < a \ b < 0" using add_less_cancel_right [of b a 0] by simp end @@ -1392,7 +1322,8 @@ proof- from assms have "u * x + v * y \ u * a + v * a" by (simp add: add_mono mult_left_mono) - thus ?thesis using assms unfolding distrib_right[symmetric] by simp + with assms show ?thesis + unfolding distrib_right[symmetric] by simp qed end @@ -1416,80 +1347,79 @@ using mult_strict_right_mono by (cases "c = 0") auto qed -lemma mult_left_le_imp_le: - "c * a \ c * b \ 0 < c \ a \ b" -by (force simp add: mult_strict_left_mono _not_less [symmetric]) +lemma mult_left_le_imp_le: "c * a \ c * b \ 0 < c \ a \ b" + by (auto simp add: mult_strict_left_mono _not_less [symmetric]) -lemma mult_right_le_imp_le: - "a * c \ b * c \ 0 < c \ a \ b" -by (force simp add: mult_strict_right_mono not_less [symmetric]) +lemma mult_right_le_imp_le: "a * c \ b * c \ 0 < c \ a \ b" + by (auto simp add: mult_strict_right_mono not_less [symmetric]) lemma mult_pos_pos[simp]: "0 < a \ 0 < b \ 0 < a * b" -using mult_strict_left_mono [of 0 b a] by simp + using mult_strict_left_mono [of 0 b a] by simp lemma mult_pos_neg: "0 < a \ b < 0 \ a * b < 0" -using mult_strict_left_mono [of b 0 a] by simp + using mult_strict_left_mono [of b 0 a] by simp lemma mult_neg_pos: "a < 0 \ 0 < b \ a * b < 0" -using mult_strict_right_mono [of a 0 b] by simp + using mult_strict_right_mono [of a 0 b] by simp text \Legacy - use \mult_neg_pos\\ lemma mult_pos_neg2: "0 < a \ b < 0 \ b * a < 0" -by (drule mult_strict_right_mono [of b 0], auto) - -lemma zero_less_mult_pos: - "0 < a * b \ 0 < a \ 0 < b" -apply (cases "b\0") - apply (auto simp add: le_less not_less) -apply (drule_tac mult_pos_neg [of a b]) - apply (auto dest: less_not_sym) -done + apply (drule mult_strict_right_mono [of b 0]) + apply auto + done -lemma zero_less_mult_pos2: - "0 < b * a \ 0 < a \ 0 < b" -apply (cases "b\0") - apply (auto simp add: le_less not_less) -apply (drule_tac mult_pos_neg2 [of a b]) - apply (auto dest: less_not_sym) -done +lemma zero_less_mult_pos: "0 < a * b \ 0 < a \ 0 < b" + apply (cases "b \ 0") + apply (auto simp add: le_less not_less) + apply (drule_tac mult_pos_neg [of a b]) + apply (auto dest: less_not_sym) + done -text\Strict monotonicity in both arguments\ +lemma zero_less_mult_pos2: "0 < b * a \ 0 < a \ 0 < b" + apply (cases "b \ 0") + apply (auto simp add: le_less not_less) + apply (drule_tac mult_pos_neg2 [of a b]) + apply (auto dest: less_not_sym) + done + +text \Strict monotonicity in both arguments\ lemma mult_strict_mono: assumes "a < b" and "c < d" and "0 < b" and "0 \ c" shows "a * c < b * d" - using assms apply (cases "c=0") - apply (simp) + using assms + apply (cases "c = 0") + apply simp apply (erule mult_strict_right_mono [THEN less_trans]) - apply (force simp add: le_less) - apply (erule mult_strict_left_mono, assumption) + apply (auto simp add: le_less) + apply (erule (1) mult_strict_left_mono) done -text\This weaker variant has more natural premises\ +text \This weaker variant has more natural premises\ lemma mult_strict_mono': assumes "a < b" and "c < d" and "0 \ a" and "0 \ c" shows "a * c < b * d" -by (rule mult_strict_mono) (insert assms, auto) + by (rule mult_strict_mono) (insert assms, auto) lemma mult_less_le_imp_less: assumes "a < b" and "c \ d" and "0 \ a" and "0 < c" shows "a * c < b * d" - using assms apply (subgoal_tac "a * c < b * c") + using assms + apply (subgoal_tac "a * c < b * c") apply (erule less_le_trans) apply (erule mult_left_mono) apply simp - apply (erule mult_strict_right_mono) - apply assumption + apply (erule (1) mult_strict_right_mono) done lemma mult_le_less_imp_less: assumes "a \ b" and "c < d" and "0 < a" and "0 \ c" shows "a * c < b * d" - using assms apply (subgoal_tac "a * c \ b * c") + using assms + apply (subgoal_tac "a * c \ b * c") apply (erule le_less_trans) apply (erule mult_strict_left_mono) apply simp - apply (erule mult_right_mono) - apply simp + apply (erule (1) mult_right_mono) done end @@ -1504,9 +1434,9 @@ shows "u * x + v * y < a" proof - from assms have "u * x + v * y < u * a + v * a" - by (cases "u = 0") - (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono) - thus ?thesis using assms unfolding distrib_right[symmetric] by simp + by (cases "u = 0") (auto intro!: add_less_le_mono mult_strict_left_mono mult_left_mono) + with assms show ?thesis + unfolding distrib_right[symmetric] by simp qed end @@ -1519,8 +1449,8 @@ proof fix a b c :: 'a assume "a \ b" "0 \ c" - thus "c * a \ c * b" by (rule comm_mult_left_mono) - thus "a * c \ b * c" by (simp only: mult.commute) + then show "c * a \ c * b" by (rule comm_mult_left_mono) + then show "a * c \ b * c" by (simp only: mult.commute) qed end @@ -1542,15 +1472,15 @@ proof fix a b c :: 'a assume "a < b" "0 < c" - thus "c * a < c * b" by (rule comm_mult_strict_left_mono) - thus "a * c < b * c" by (simp only: mult.commute) + then show "c * a < c * b" by (rule comm_mult_strict_left_mono) + then show "a * c < b * c" by (simp only: mult.commute) qed subclass ordered_cancel_comm_semiring proof fix a b c :: 'a assume "a \ b" "0 \ c" - thus "c * a \ c * b" + then show "c * a \ c * b" unfolding le_less using mult_strict_left_mono by (cases "c = 0") auto qed @@ -1562,40 +1492,33 @@ subclass ordered_ab_group_add .. -lemma less_add_iff1: - "a * e + c < b * e + d \ (a - b) * e + c < d" -by (simp add: algebra_simps) +lemma less_add_iff1: "a * e + c < b * e + d \ (a - b) * e + c < d" + by (simp add: algebra_simps) -lemma less_add_iff2: - "a * e + c < b * e + d \ c < (b - a) * e + d" -by (simp add: algebra_simps) +lemma less_add_iff2: "a * e + c < b * e + d \ c < (b - a) * e + d" + by (simp add: algebra_simps) -lemma le_add_iff1: - "a * e + c \ b * e + d \ (a - b) * e + c \ d" -by (simp add: algebra_simps) +lemma le_add_iff1: "a * e + c \ b * e + d \ (a - b) * e + c \ d" + by (simp add: algebra_simps) -lemma le_add_iff2: - "a * e + c \ b * e + d \ c \ (b - a) * e + d" -by (simp add: algebra_simps) +lemma le_add_iff2: "a * e + c \ b * e + d \ c \ (b - a) * e + d" + by (simp add: algebra_simps) -lemma mult_left_mono_neg: - "b \ a \ c \ 0 \ c * a \ c * b" +lemma mult_left_mono_neg: "b \ a \ c \ 0 \ c * a \ c * b" apply (drule mult_left_mono [of _ _ "- c"]) apply simp_all done -lemma mult_right_mono_neg: - "b \ a \ c \ 0 \ a * c \ b * c" +lemma mult_right_mono_neg: "b \ a \ c \ 0 \ a * c \ b * c" apply (drule mult_right_mono [of _ _ "- c"]) apply simp_all done lemma mult_nonpos_nonpos: "a \ 0 \ b \ 0 \ 0 \ a * b" -using mult_right_mono_neg [of a 0 b] by simp + using mult_right_mono_neg [of a 0 b] by simp -lemma split_mult_pos_le: - "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b" -by (auto simp add: mult_nonpos_nonpos) +lemma split_mult_pos_le: "(0 \ a \ 0 \ b) \ (a \ 0 \ b \ 0) \ 0 \ a * b" + by (auto simp add: mult_nonpos_nonpos) end @@ -1608,12 +1531,12 @@ proof fix a b show "\a + b\ \ \a\ + \b\" - by (auto simp add: abs_if not_le not_less algebra_simps simp del: add.commute dest: add_neg_neg add_nonneg_nonneg) + by (auto simp add: abs_if not_le not_less algebra_simps + simp del: add.commute dest: add_neg_neg add_nonneg_nonneg) qed (auto simp add: abs_if) lemma zero_le_square [simp]: "0 \ a * a" - using linear [of 0 a] - by (auto simp add: mult_nonpos_nonpos) + using linear [of 0 a] by (auto simp add: mult_nonpos_nonpos) lemma not_square_less_zero [simp]: "\ (a * a < 0)" by (simp add: not_less) @@ -1621,12 +1544,10 @@ proposition abs_eq_iff: "\x\ = \y\ \ x = y \ x = -y" by (auto simp add: abs_if split: if_split_asm) -lemma sum_squares_ge_zero: - "0 \ x * x + y * y" +lemma sum_squares_ge_zero: "0 \ x * x + y * y" by (intro add_nonneg_nonneg zero_le_square) -lemma not_sum_squares_lt_zero: - "\ x * x + y * y < 0" +lemma not_sum_squares_lt_zero: "\ x * x + y * y < 0" by (simp add: not_less sum_squares_ge_zero) end @@ -1638,40 +1559,49 @@ subclass linordered_ring .. lemma mult_strict_left_mono_neg: "b < a \ c < 0 \ c * a < c * b" -using mult_strict_left_mono [of b a "- c"] by simp + using mult_strict_left_mono [of b a "- c"] by simp lemma mult_strict_right_mono_neg: "b < a \ c < 0 \ a * c < b * c" -using mult_strict_right_mono [of b a "- c"] by simp + using mult_strict_right_mono [of b a "- c"] by simp lemma mult_neg_neg: "a < 0 \ b < 0 \ 0 < a * b" -using mult_strict_right_mono_neg [of a 0 b] by simp + using mult_strict_right_mono_neg [of a 0 b] by simp subclass ring_no_zero_divisors proof fix a b - assume "a \ 0" then have A: "a < 0 \ 0 < a" by (simp add: neq_iff) - assume "b \ 0" then have B: "b < 0 \ 0 < b" by (simp add: neq_iff) + assume "a \ 0" + then have A: "a < 0 \ 0 < a" by (simp add: neq_iff) + assume "b \ 0" + then have B: "b < 0 \ 0 < b" by (simp add: neq_iff) have "a * b < 0 \ 0 < a * b" proof (cases "a < 0") - case True note A' = this - show ?thesis proof (cases "b < 0") - case True with A' - show ?thesis by (auto dest: mult_neg_neg) + case A': True + show ?thesis + proof (cases "b < 0") + case True + with A' show ?thesis by (auto dest: mult_neg_neg) next - case False with B have "0 < b" by auto + case False + with B have "0 < b" by auto with A' show ?thesis by (auto dest: mult_strict_right_mono) qed next - case False with A have A': "0 < a" by auto - show ?thesis proof (cases "b < 0") - case True with A' - show ?thesis by (auto dest: mult_strict_right_mono_neg) + case False + with A have A': "0 < a" by auto + show ?thesis + proof (cases "b < 0") + case True + with A' show ?thesis + by (auto dest: mult_strict_right_mono_neg) next - case False with B have "0 < b" by auto + case False + with B have "0 < b" by auto with A' show ?thesis by auto qed qed - then show "a * b \ 0" by (simp add: neq_iff) + then show "a * b \ 0" + by (simp add: neq_iff) qed lemma zero_less_mult_iff: "0 < a * b \ 0 < a \ 0 < b \ a < 0 \ b < 0" @@ -1681,84 +1611,66 @@ lemma zero_le_mult_iff: "0 \ a * b \ 0 \ a \ 0 \ b \ a \ 0 \ b \ 0" by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff) -lemma mult_less_0_iff: - "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" - apply (insert zero_less_mult_iff [of "-a" b]) - apply force - done +lemma mult_less_0_iff: "a * b < 0 \ 0 < a \ b < 0 \ a < 0 \ 0 < b" + using zero_less_mult_iff [of "- a" b] by auto -lemma mult_le_0_iff: - "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" - apply (insert zero_le_mult_iff [of "-a" b]) - apply force - done +lemma mult_le_0_iff: "a * b \ 0 \ 0 \ a \ b \ 0 \ a \ 0 \ 0 \ b" + using zero_le_mult_iff [of "- a" b] by auto -text\Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"}, - also with the relations \\\ and equality.\ +text \ + Cancellation laws for @{term "c * a < c * b"} and @{term "a * c < b * c"}, + also with the relations \\\ and equality. +\ -text\These ``disjunction'' versions produce two cases when the comparison is - an assumption, but effectively four when the comparison is a goal.\ +text \ + These ``disjunction'' versions produce two cases when the comparison is + an assumption, but effectively four when the comparison is a goal. +\ -lemma mult_less_cancel_right_disj: - "a * c < b * c \ 0 < c \ a < b \ c < 0 \ b < a" +lemma mult_less_cancel_right_disj: "a * c < b * c \ 0 < c \ a < b \ c < 0 \ b < a" apply (cases "c = 0") - apply (auto simp add: neq_iff mult_strict_right_mono - mult_strict_right_mono_neg) - apply (auto simp add: not_less - not_le [symmetric, of "a*c"] - not_le [symmetric, of a]) + apply (auto simp add: neq_iff mult_strict_right_mono mult_strict_right_mono_neg) + apply (auto simp add: not_less not_le [symmetric, of "a*c"] not_le [symmetric, of a]) apply (erule_tac [!] notE) - apply (auto simp add: less_imp_le mult_right_mono - mult_right_mono_neg) + apply (auto simp add: less_imp_le mult_right_mono mult_right_mono_neg) done -lemma mult_less_cancel_left_disj: - "c * a < c * b \ 0 < c \ a < b \ c < 0 \ b < a" +lemma mult_less_cancel_left_disj: "c * a < c * b \ 0 < c \ a < b \ c < 0 \ b < a" apply (cases "c = 0") - apply (auto simp add: neq_iff mult_strict_left_mono - mult_strict_left_mono_neg) - apply (auto simp add: not_less - not_le [symmetric, of "c*a"] - not_le [symmetric, of a]) + apply (auto simp add: neq_iff mult_strict_left_mono mult_strict_left_mono_neg) + apply (auto simp add: not_less not_le [symmetric, of "c * a"] not_le [symmetric, of a]) apply (erule_tac [!] notE) - apply (auto simp add: less_imp_le mult_left_mono - mult_left_mono_neg) + apply (auto simp add: less_imp_le mult_left_mono mult_left_mono_neg) done -text\The ``conjunction of implication'' lemmas produce two cases when the -comparison is a goal, but give four when the comparison is an assumption.\ +text \ + The ``conjunction of implication'' lemmas produce two cases when the + comparison is a goal, but give four when the comparison is an assumption. +\ -lemma mult_less_cancel_right: - "a * c < b * c \ (0 \ c \ a < b) \ (c \ 0 \ b < a)" +lemma mult_less_cancel_right: "a * c < b * c \ (0 \ c \ a < b) \ (c \ 0 \ b < a)" using mult_less_cancel_right_disj [of a c b] by auto -lemma mult_less_cancel_left: - "c * a < c * b \ (0 \ c \ a < b) \ (c \ 0 \ b < a)" +lemma mult_less_cancel_left: "c * a < c * b \ (0 \ c \ a < b) \ (c \ 0 \ b < a)" using mult_less_cancel_left_disj [of c a b] by auto -lemma mult_le_cancel_right: - "a * c \ b * c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" -by (simp add: not_less [symmetric] mult_less_cancel_right_disj) +lemma mult_le_cancel_right: "a * c \ b * c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" + by (simp add: not_less [symmetric] mult_less_cancel_right_disj) -lemma mult_le_cancel_left: - "c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" -by (simp add: not_less [symmetric] mult_less_cancel_left_disj) +lemma mult_le_cancel_left: "c * a \ c * b \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" + by (simp add: not_less [symmetric] mult_less_cancel_left_disj) -lemma mult_le_cancel_left_pos: - "0 < c \ c * a \ c * b \ a \ b" -by (auto simp: mult_le_cancel_left) +lemma mult_le_cancel_left_pos: "0 < c \ c * a \ c * b \ a \ b" + by (auto simp: mult_le_cancel_left) -lemma mult_le_cancel_left_neg: - "c < 0 \ c * a \ c * b \ b \ a" -by (auto simp: mult_le_cancel_left) +lemma mult_le_cancel_left_neg: "c < 0 \ c * a \ c * b \ b \ a" + by (auto simp: mult_le_cancel_left) -lemma mult_less_cancel_left_pos: - "0 < c \ c * a < c * b \ a < b" -by (auto simp: mult_less_cancel_left) +lemma mult_less_cancel_left_pos: "0 < c \ c * a < c * b \ a < b" + by (auto simp: mult_less_cancel_left) -lemma mult_less_cancel_left_neg: - "c < 0 \ c * a < c * b \ b < a" -by (auto simp: mult_less_cancel_left) +lemma mult_less_cancel_left_neg: "c < 0 \ c * a < c * b \ b < a" + by (auto simp: mult_less_cancel_left) end @@ -1783,19 +1695,19 @@ begin subclass zero_neq_one - proof qed (insert zero_less_one, blast) + by standard (insert zero_less_one, blast) subclass comm_semiring_1 - proof qed (rule mult_1_left) + by standard (rule mult_1_left) lemma zero_le_one [simp]: "0 \ 1" -by (rule zero_less_one [THEN less_imp_le]) + by (rule zero_less_one [THEN less_imp_le]) lemma not_one_le_zero [simp]: "\ 1 \ 0" -by (simp add: not_le) + by (simp add: not_le) lemma not_one_less_zero [simp]: "\ 1 < 0" -by (simp add: not_less) + by (simp add: not_less) lemma mult_left_le: "c \ 1 \ 0 \ a \ a * c \ a" using mult_left_mono[of c 1 a] by simp @@ -1812,8 +1724,7 @@ assumes le_add_diff_inverse2 [simp]: "b \ a \ a - b + b = a" begin -subclass linordered_nonzero_semiring - proof qed +subclass linordered_nonzero_semiring .. text \Addition is the inverse of subtraction.\ @@ -1823,31 +1734,31 @@ lemma add_diff_inverse: "\ a < b \ b + (a - b) = a" by simp -lemma add_le_imp_le_diff: - shows "i + k \ n \ i \ n - k" +lemma add_le_imp_le_diff: "i + k \ n \ i \ n - k" apply (subst add_le_cancel_right [where c=k, symmetric]) apply (frule le_add_diff_inverse2) apply (simp only: add.assoc [symmetric]) - using add_implies_diff by fastforce + using add_implies_diff apply fastforce + done lemma add_le_add_imp_diff_le: - assumes a1: "i + k \ n" - and a2: "n \ j + k" - shows "\i + k \ n; n \ j + k\ \ n - k \ j" + assumes 1: "i + k \ n" + and 2: "n \ j + k" + shows "i + k \ n \ n \ j + k \ n - k \ j" proof - have "n - (i + k) + (i + k) = n" - using a1 by simp + using 1 by simp moreover have "n - k = n - k - i + i" - using a1 by (simp add: add_le_imp_le_diff) + using 1 by (simp add: add_le_imp_le_diff) ultimately show ?thesis - using a2 + using 2 apply (simp add: add.assoc [symmetric]) - apply (rule add_le_imp_le_diff [of _ k "j+k", simplified add_diff_cancel_right']) - by (simp add: add.commute diff_diff_add) + apply (rule add_le_imp_le_diff [of _ k "j + k", simplified add_diff_cancel_right']) + apply (simp add: add.commute diff_diff_add) + done qed -lemma less_1_mult: - "1 < m \ 1 < n \ 1 < m * n" +lemma less_1_mult: "1 < m \ 1 < n \ 1 < m * n" using mult_strict_mono [of 1 m 1 n] by (simp add: less_trans [OF zero_less_one]) end @@ -1864,90 +1775,73 @@ subclass linordered_semidom proof have "0 \ 1 * 1" by (rule zero_le_square) - thus "0 < 1" by (simp add: le_less) - show "\b a. b \ a \ a - b + b = a" + then show "0 < 1" by (simp add: le_less) + show "b \ a \ a - b + b = a" for a b by simp qed lemma linorder_neqE_linordered_idom: - assumes "x \ y" obtains "x < y" | "y < x" + assumes "x \ y" + obtains "x < y" | "y < x" using assms by (rule neqE) text \These cancellation simprules also produce two cases when the comparison is a goal.\ -lemma mult_le_cancel_right1: - "c \ b * c \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" -by (insert mult_le_cancel_right [of 1 c b], simp) +lemma mult_le_cancel_right1: "c \ b * c \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" + using mult_le_cancel_right [of 1 c b] by simp -lemma mult_le_cancel_right2: - "a * c \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" -by (insert mult_le_cancel_right [of a c 1], simp) +lemma mult_le_cancel_right2: "a * c \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" + using mult_le_cancel_right [of a c 1] by simp -lemma mult_le_cancel_left1: - "c \ c * b \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" -by (insert mult_le_cancel_left [of c 1 b], simp) +lemma mult_le_cancel_left1: "c \ c * b \ (0 < c \ 1 \ b) \ (c < 0 \ b \ 1)" + using mult_le_cancel_left [of c 1 b] by simp -lemma mult_le_cancel_left2: - "c * a \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" -by (insert mult_le_cancel_left [of c a 1], simp) +lemma mult_le_cancel_left2: "c * a \ c \ (0 < c \ a \ 1) \ (c < 0 \ 1 \ a)" + using mult_le_cancel_left [of c a 1] by simp -lemma mult_less_cancel_right1: - "c < b * c \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" -by (insert mult_less_cancel_right [of 1 c b], simp) +lemma mult_less_cancel_right1: "c < b * c \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" + using mult_less_cancel_right [of 1 c b] by simp -lemma mult_less_cancel_right2: - "a * c < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" -by (insert mult_less_cancel_right [of a c 1], simp) +lemma mult_less_cancel_right2: "a * c < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" + using mult_less_cancel_right [of a c 1] by simp -lemma mult_less_cancel_left1: - "c < c * b \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" -by (insert mult_less_cancel_left [of c 1 b], simp) +lemma mult_less_cancel_left1: "c < c * b \ (0 \ c \ 1 < b) \ (c \ 0 \ b < 1)" + using mult_less_cancel_left [of c 1 b] by simp -lemma mult_less_cancel_left2: - "c * a < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" -by (insert mult_less_cancel_left [of c a 1], simp) +lemma mult_less_cancel_left2: "c * a < c \ (0 \ c \ a < 1) \ (c \ 0 \ 1 < a)" + using mult_less_cancel_left [of c a 1] by simp -lemma sgn_sgn [simp]: - "sgn (sgn a) = sgn a" -unfolding sgn_if by simp +lemma sgn_sgn [simp]: "sgn (sgn a) = sgn a" + unfolding sgn_if by simp -lemma sgn_0_0: - "sgn a = 0 \ a = 0" -unfolding sgn_if by simp +lemma sgn_0_0: "sgn a = 0 \ a = 0" + unfolding sgn_if by simp -lemma sgn_1_pos: - "sgn a = 1 \ a > 0" -unfolding sgn_if by simp +lemma sgn_1_pos: "sgn a = 1 \ a > 0" + unfolding sgn_if by simp -lemma sgn_1_neg: - "sgn a = - 1 \ a < 0" -unfolding sgn_if by auto +lemma sgn_1_neg: "sgn a = - 1 \ a < 0" + unfolding sgn_if by auto -lemma sgn_pos [simp]: - "0 < a \ sgn a = 1" -unfolding sgn_1_pos . +lemma sgn_pos [simp]: "0 < a \ sgn a = 1" + by (simp only: sgn_1_pos) -lemma sgn_neg [simp]: - "a < 0 \ sgn a = - 1" -unfolding sgn_1_neg . +lemma sgn_neg [simp]: "a < 0 \ sgn a = - 1" + by (simp only: sgn_1_neg) -lemma sgn_times: - "sgn (a * b) = sgn a * sgn b" -by (auto simp add: sgn_if zero_less_mult_iff) +lemma sgn_times: "sgn (a * b) = sgn a * sgn b" + by (auto simp add: sgn_if zero_less_mult_iff) lemma abs_sgn: "\k\ = k * sgn k" -unfolding sgn_if abs_if by auto + unfolding sgn_if abs_if by auto -lemma sgn_greater [simp]: - "0 < sgn a \ 0 < a" +lemma sgn_greater [simp]: "0 < sgn a \ 0 < a" unfolding sgn_if by auto -lemma sgn_less [simp]: - "sgn a < 0 \ a < 0" +lemma sgn_less [simp]: "sgn a < 0 \ a < 0" unfolding sgn_if by auto -lemma abs_sgn_eq: - "\sgn a\ = (if a = 0 then 0 else 1)" +lemma abs_sgn_eq: "\sgn a\ = (if a = 0 then 0 else 1)" by (simp add: sgn_if) lemma abs_dvd_iff [simp]: "\m\ dvd k \ m dvd k" @@ -1956,36 +1850,31 @@ lemma dvd_abs_iff [simp]: "m dvd \k\ \ m dvd k" by (simp add: abs_if) -lemma dvd_if_abs_eq: - "\l\ = \k\ \ l dvd k" -by(subst abs_dvd_iff[symmetric]) simp +lemma dvd_if_abs_eq: "\l\ = \k\ \ l dvd k" + by (subst abs_dvd_iff [symmetric]) simp -text \The following lemmas can be proven in more general structures, but -are dangerous as simp rules in absence of @{thm neg_equal_zero}, -@{thm neg_less_pos}, @{thm neg_less_eq_nonneg}.\ +text \ + The following lemmas can be proven in more general structures, but + are dangerous as simp rules in absence of @{thm neg_equal_zero}, + @{thm neg_less_pos}, @{thm neg_less_eq_nonneg}. +\ -lemma equation_minus_iff_1 [simp, no_atp]: - "1 = - a \ a = - 1" +lemma equation_minus_iff_1 [simp, no_atp]: "1 = - a \ a = - 1" by (fact equation_minus_iff) -lemma minus_equation_iff_1 [simp, no_atp]: - "- a = 1 \ a = - 1" +lemma minus_equation_iff_1 [simp, no_atp]: "- a = 1 \ a = - 1" by (subst minus_equation_iff, auto) -lemma le_minus_iff_1 [simp, no_atp]: - "1 \ - b \ b \ - 1" +lemma le_minus_iff_1 [simp, no_atp]: "1 \ - b \ b \ - 1" by (fact le_minus_iff) -lemma minus_le_iff_1 [simp, no_atp]: - "- a \ 1 \ - 1 \ a" +lemma minus_le_iff_1 [simp, no_atp]: "- a \ 1 \ - 1 \ a" by (fact minus_le_iff) -lemma less_minus_iff_1 [simp, no_atp]: - "1 < - b \ b < - 1" +lemma less_minus_iff_1 [simp, no_atp]: "1 < - b \ b < - 1" by (fact less_minus_iff) -lemma minus_less_iff_1 [simp, no_atp]: - "- a < 1 \ - 1 < a" +lemma minus_less_iff_1 [simp, no_atp]: "- a < 1 \ - 1 < a" by (fact minus_less_iff) end @@ -1993,15 +1882,16 @@ text \Simprules for comparisons where common factors can be cancelled.\ lemmas mult_compare_simps = - mult_le_cancel_right mult_le_cancel_left - mult_le_cancel_right1 mult_le_cancel_right2 - mult_le_cancel_left1 mult_le_cancel_left2 - mult_less_cancel_right mult_less_cancel_left - mult_less_cancel_right1 mult_less_cancel_right2 - mult_less_cancel_left1 mult_less_cancel_left2 - mult_cancel_right mult_cancel_left - mult_cancel_right1 mult_cancel_right2 - mult_cancel_left1 mult_cancel_left2 + mult_le_cancel_right mult_le_cancel_left + mult_le_cancel_right1 mult_le_cancel_right2 + mult_le_cancel_left1 mult_le_cancel_left2 + mult_less_cancel_right mult_less_cancel_left + mult_less_cancel_right1 mult_less_cancel_right2 + mult_less_cancel_left1 mult_less_cancel_left2 + mult_cancel_right mult_cancel_left + mult_cancel_right1 mult_cancel_right2 + mult_cancel_left1 mult_cancel_left2 + text \Reasoning about inequalities with division\ @@ -2012,7 +1902,7 @@ proof - have "a + 0 < a + 1" by (blast intro: zero_less_one add_strict_left_mono) - thus ?thesis by simp + then show ?thesis by simp qed end @@ -2020,12 +1910,10 @@ context linordered_idom begin -lemma mult_right_le_one_le: - "0 \ x \ 0 \ y \ y \ 1 \ x * y \ x" +lemma mult_right_le_one_le: "0 \ x \ 0 \ y \ y \ 1 \ x * y \ x" by (rule mult_left_le) -lemma mult_left_le_one_le: - "0 \ x \ 0 \ y \ y \ 1 \ y * x \ x" +lemma mult_left_le_one_le: "0 \ x \ 0 \ y \ y \ 1 \ y * x \ x" by (auto simp add: mult_le_cancel_right2) end @@ -2035,12 +1923,10 @@ context linordered_idom begin -lemma mult_sgn_abs: - "sgn x * \x\ = x" +lemma mult_sgn_abs: "sgn x * \x\ = x" unfolding abs_if sgn_if by auto -lemma abs_one [simp]: - "\1\ = 1" +lemma abs_one [simp]: "\1\ = 1" by (simp add: abs_if) end @@ -2052,57 +1938,54 @@ context linordered_idom begin -subclass ordered_ring_abs proof -qed (auto simp add: abs_if not_less mult_less_0_iff) +subclass ordered_ring_abs + by standard (auto simp add: abs_if not_less mult_less_0_iff) -lemma abs_mult: - "\a * b\ = \a\ * \b\" +lemma abs_mult: "\a * b\ = \a\ * \b\" by (rule abs_eq_mult) auto -lemma abs_mult_self [simp]: - "\a\ * \a\ = a * a" +lemma abs_mult_self [simp]: "\a\ * \a\ = a * a" by (simp add: abs_if) lemma abs_mult_less: - "\a\ < c \ \b\ < d \ \a\ * \b\ < c * d" + assumes ac: "\a\ < c" + and bd: "\b\ < d" + shows "\a\ * \b\ < c * d" proof - - assume ac: "\a\ < c" - hence cpos: "0b\ < d" - thus ?thesis by (simp add: ac cpos mult_strict_mono) + from ac have "0 < c" + by (blast intro: le_less_trans abs_ge_zero) + with bd show ?thesis by (simp add: ac mult_strict_mono) qed -lemma abs_less_iff: - "\a\ < b \ a < b \ - a < b" +lemma abs_less_iff: "\a\ < b \ a < b \ - a < b" by (simp add: less_le abs_le_iff) (auto simp add: abs_if) -lemma abs_mult_pos: - "0 \ x \ \y\ * x = \y * x\" +lemma abs_mult_pos: "0 \ x \ \y\ * x = \y * x\" by (simp add: abs_mult) -lemma abs_diff_less_iff: - "\x - a\ < r \ a - r < x \ x < a + r" +lemma abs_diff_less_iff: "\x - a\ < r \ a - r < x \ x < a + r" by (auto simp add: diff_less_eq ac_simps abs_less_iff) -lemma abs_diff_le_iff: - "\x - a\ \ r \ a - r \ x \ x \ a + r" +lemma abs_diff_le_iff: "\x - a\ \ r \ a - r \ x \ x \ a + r" by (auto simp add: diff_le_eq ac_simps abs_le_iff) lemma abs_add_one_gt_zero: "0 < 1 + \x\" - by (force simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans) + by (auto simp: abs_if not_less intro: zero_less_one add_strict_increasing less_trans) end subsection \Dioids\ -text \Dioids are the alternative extensions of semirings, a semiring can either be a ring or a dioid -but never both.\ +text \ + Dioids are the alternative extensions of semirings, a semiring can + either be a ring or a dioid but never both. +\ class dioid = semiring_1 + canonically_ordered_monoid_add begin subclass ordered_semiring - proof qed (auto simp: le_iff_add distrib_left distrib_right) + by standard (auto simp: le_iff_add distrib_left distrib_right) end