# HG changeset patch # User paulson # Date 1423584491 0 # Node ID 8c6747dba7316222f951b56c454650c58378b906 # Parent ef195926dd981c95a0c97e528723cb32c325ad5d New lemmas and a bit of tidying up. diff -r ef195926dd98 -r 8c6747dba731 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Feb 10 12:27:30 2015 +0100 +++ b/src/HOL/Finite_Set.thy Tue Feb 10 16:08:11 2015 +0000 @@ -262,6 +262,10 @@ "finite {x. P x} \ finite { f x | x. P x }" by (simp add: image_Collect [symmetric]) +lemma finite_image_set2: + "finite {x. P x} \ finite {y. Q y} \ finite {f x y | x y. P x \ Q y}" + by (rule finite_subset [where B = "\x \ {x. P x}. \y \ {y. Q y}. {f x y}"]) auto + lemma finite_imageD: assumes "finite (f ` A)" and "inj_on f A" shows "finite A" @@ -1618,6 +1622,9 @@ by (force intro: card_mono simp: card_image [symmetric]) qed +lemma surj_card_le: "finite A \ B \ f ` A \ card B \ card A" + by (blast intro: card_image_le card_mono le_trans) + lemma card_bij_eq: "[|inj_on f A; f ` A \ B; inj_on g B; g ` B \ A; finite A; finite B |] ==> card A = card B" diff -r ef195926dd98 -r 8c6747dba731 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Tue Feb 10 12:27:30 2015 +0100 +++ b/src/HOL/Fun.thy Tue Feb 10 16:08:11 2015 +0000 @@ -15,6 +15,12 @@ "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.*} +lemma uniq_choice: "\x. \!y. Q x y \ \f. \x. Q x (f x)" + by (force intro: theI') + +lemma b_uniq_choice: "\x\S. \!y. Q x y \ \f. \x\S. Q x (f x)" + by (force intro: theI') subsection {* The Identity Function @{text id} *} @@ -79,6 +85,9 @@ "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" + by (auto simp: comp_def elim!: equalityE) + code_printing constant comp \ (SML) infixl 5 "o" and (Haskell) infixr 9 "." @@ -477,14 +486,17 @@ lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B" by (simp add: inj_on_def, blast) -lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)" -by (blast dest: injD) +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) + +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)" -by (simp add: inj_on_def, blast) + by (blast dest: injD) lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)" -by (blast dest: injD) + by (blast dest: injD) lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)" by auto diff -r ef195926dd98 -r 8c6747dba731 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Feb 10 12:27:30 2015 +0100 +++ b/src/HOL/HOL.thy Tue Feb 10 16:08:11 2015 +0000 @@ -550,63 +550,6 @@ done -subsubsection {*THE: definite description operator*} - -lemma the_equality: - assumes prema: "P a" - and premx: "!!x. P x ==> x=a" - shows "(THE x. P x) = a" -apply (rule trans [OF _ the_eq_trivial]) -apply (rule_tac f = "The" in arg_cong) -apply (rule ext) -apply (rule iffI) - apply (erule premx) -apply (erule ssubst, rule prema) -done - -lemma theI: - assumes "P a" and "!!x. P x ==> x=a" - shows "P (THE x. P x)" -by (iprover intro: assms the_equality [THEN ssubst]) - -lemma theI': "EX! x. P x ==> P (THE x. P x)" -apply (erule ex1E) -apply (erule theI) -apply (erule allE) -apply (erule mp) -apply assumption -done - -(*Easier to apply than theI: only one occurrence of P*) -lemma theI2: - assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" - shows "Q (THE x. P x)" -by (iprover intro: assms theI) - -lemma the1I2: assumes "EX! x. P x" "\x. P x \ Q x" shows "Q (THE x. P x)" -by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] - elim:allE impE) - -lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a" -apply (rule the_equality) -apply assumption -apply (erule ex1E) -apply (erule all_dupE) -apply (drule mp) -apply assumption -apply (erule ssubst) -apply (erule allE) -apply (erule mp) -apply assumption -done - -lemma the_sym_eq_trivial: "(THE y. x=y) = x" -apply (rule the_equality) -apply (rule refl) -apply (erule sym) -done - - subsubsection {*Classical intro rules for disjunction and existential quantifiers*} lemma disjCI: @@ -876,7 +819,6 @@ declare ex_ex1I [intro!] and allI [intro!] - and the_equality [intro] and exI [intro] declare exE [elim!] @@ -924,6 +866,39 @@ *} +subsubsection {*THE: definite description operator*} + +lemma the_equality [intro]: + assumes "P a" + and "!!x. P x ==> x=a" + shows "(THE x. P x) = a" + by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial]) + +lemma theI: + assumes "P a" and "!!x. P x ==> x=a" + shows "P (THE x. P x)" +by (iprover intro: assms the_equality [THEN ssubst]) + +lemma theI': "EX! x. P x ==> P (THE x. P x)" + by (blast intro: theI) + +(*Easier to apply than theI: only one occurrence of P*) +lemma theI2: + assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x" + shows "Q (THE x. P x)" +by (iprover intro: assms theI) + +lemma the1I2: assumes "EX! x. P x" "\x. P x \ Q x" shows "Q (THE x. P x)" +by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)] + elim:allE impE) + +lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a" + by blast + +lemma the_sym_eq_trivial: "(THE y. x=y) = x" + by blast + + subsubsection {* Simplifier *} lemma eta_contract_eq: "(%s. f s) = f" .. @@ -1099,8 +1074,7 @@ lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))" -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *} - apply (simplesubst split_if, blast) - done + by (simplesubst split_if) blast lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover diff -r ef195926dd98 -r 8c6747dba731 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Feb 10 12:27:30 2015 +0100 +++ b/src/HOL/Set.thy Tue Feb 10 16:08:11 2015 +0000 @@ -1020,6 +1020,9 @@ "f ` A - f ` B \ f ` (A - B)" by blast +lemma Setcompr_eq_image: "{f x | x. x \ A} = f ` A" + by blast + lemma ball_imageD: assumes "\x\f ` A. P x" shows "\x\A. P (f x)" @@ -1241,6 +1244,9 @@ lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \ {x. Q x}" by blast +lemma Collect_mono_iff [simp]: "Collect P \ Collect Q \ (\x. P x \ Q x)" + by blast + text {* \medskip @{text insert}. *}