--- a/src/HOL/Finite_Set.thy Tue Feb 10 23:02:39 2015 +0100
+++ b/src/HOL/Finite_Set.thy Wed Feb 11 12:01:56 2015 +0000
@@ -262,6 +262,10 @@
"finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
by (simp add: image_Collect [symmetric])
+lemma finite_image_set2:
+ "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y | x y. P x \<and> Q y}"
+ by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {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 \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
+ by (blast intro: card_image_le card_mono le_trans)
+
lemma card_bij_eq:
"[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
finite A; finite B |] ==> card A = card B"
--- a/src/HOL/Fun.thy Tue Feb 10 23:02:39 2015 +0100
+++ b/src/HOL/Fun.thy Wed Feb 11 12:01:56 2015 +0000
@@ -15,6 +15,12 @@
"f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
by auto
+text{*Uniqueness, so NOT the axiom of choice.*}
+lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
+ by (force intro: theI')
+
+lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
+ by (force intro: theI')
subsection {* The Identity Function @{text id} *}
@@ -79,6 +85,9 @@
"f -` (g -` x) = (g \<circ> f) -` x"
by auto
+lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
+ by (auto simp: comp_def elim!: equalityE)
+
code_printing
constant comp \<rightharpoonup> (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: "\<lbrakk>inj_on f B; a \<in> B; A \<subseteq> B\<rbrakk> \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
+ by (auto simp: inj_on_def)
+
+lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> 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
--- a/src/HOL/HOL.thy Tue Feb 10 23:02:39 2015 +0100
+++ b/src/HOL/HOL.thy Wed Feb 11 12:01:56 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" "\<And>x. P x \<Longrightarrow> 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!]
@@ -925,6 +867,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" "\<And>x. P x \<Longrightarrow> 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" ..
@@ -1100,8 +1075,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
--- a/src/HOL/Library/Infinite_Set.thy Tue Feb 10 23:02:39 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Wed Feb 11 12:01:56 2015 +0000
@@ -238,7 +238,7 @@
from inf have "infinite {x. P x}" unfolding Inf_many_def .
moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
ultimately show ?thesis
- by (simp add: Inf_many_def infinite_super)
+ using Inf_many_def infinite_super by blast
qed
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
--- a/src/HOL/Library/Nat_Bijection.thy Tue Feb 10 23:02:39 2015 +0100
+++ b/src/HOL/Library/Nat_Bijection.thy Wed Feb 11 12:01:56 2015 +0000
@@ -293,6 +293,9 @@
lemma set_encode_empty [simp]: "set_encode {} = 0"
by (simp add: set_encode_def)
+lemma set_encode_inf: "~ finite A \<Longrightarrow> set_encode A = 0"
+ by (simp add: set_encode_def)
+
lemma set_encode_insert [simp]:
"\<lbrakk>finite A; n \<notin> A\<rbrakk> \<Longrightarrow> set_encode (insert n A) = 2^n + set_encode A"
by (simp add: set_encode_def)
--- a/src/HOL/Set.thy Tue Feb 10 23:02:39 2015 +0100
+++ b/src/HOL/Set.thy Wed Feb 11 12:01:56 2015 +0000
@@ -1020,6 +1020,9 @@
"f ` A - f ` B \<subseteq> f ` (A - B)"
by blast
+lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
+ by blast
+
lemma ball_imageD:
assumes "\<forall>x\<in>f ` A. P x"
shows "\<forall>x\<in>A. P (f x)"
@@ -1055,7 +1058,7 @@
"{u. \<exists>x. u = f x} = range f"
by auto
-lemma range_composition:
+lemma range_composition:
"range (\<lambda>x. f (g x)) = f ` range g"
by auto
@@ -1241,6 +1244,9 @@
lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
by blast
+lemma Collect_mono_iff: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
+ by blast
+
text {* \medskip @{text insert}. *}
@@ -1803,7 +1809,7 @@
by blast
lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
- by blast
+ by blast
lemma vimage_const [simp]: "((\<lambda>x. c) -` A) = (if c \<in> A then UNIV else {})"
by auto