New lemmas and a bit of tidying up.
authorpaulson <lp15@cam.ac.uk>
Tue Feb 10 16:08:11 2015 +0000 (2015-02-10)
changeset 595048c6747dba731
parent 59492 ef195926dd98
child 59505 d64d48eb71cc
New lemmas and a bit of tidying up.
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Feb 10 12:27:30 2015 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Feb 10 16:08:11 2015 +0000
     1.3 @@ -262,6 +262,10 @@
     1.4    "finite {x. P x} \<Longrightarrow> finite { f x | x. P x }"
     1.5    by (simp add: image_Collect [symmetric])
     1.6  
     1.7 +lemma finite_image_set2:
     1.8 +  "finite {x. P x} \<Longrightarrow> finite {y. Q y} \<Longrightarrow> finite {f x y | x y. P x \<and> Q y}"
     1.9 +  by (rule finite_subset [where B = "\<Union>x \<in> {x. P x}. \<Union>y \<in> {y. Q y}. {f x y}"]) auto
    1.10 +
    1.11  lemma finite_imageD:
    1.12    assumes "finite (f ` A)" and "inj_on f A"
    1.13    shows "finite A"
    1.14 @@ -1618,6 +1622,9 @@
    1.15     by (force intro: card_mono simp: card_image [symmetric])
    1.16  qed
    1.17  
    1.18 +lemma surj_card_le: "finite A \<Longrightarrow> B \<subseteq> f ` A \<Longrightarrow> card B \<le> card A"
    1.19 +  by (blast intro: card_image_le card_mono le_trans)
    1.20 +
    1.21  lemma card_bij_eq:
    1.22    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
    1.23       finite A; finite B |] ==> card A = card B"
     2.1 --- a/src/HOL/Fun.thy	Tue Feb 10 12:27:30 2015 +0100
     2.2 +++ b/src/HOL/Fun.thy	Tue Feb 10 16:08:11 2015 +0000
     2.3 @@ -15,6 +15,12 @@
     2.4    "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
     2.5    by auto
     2.6  
     2.7 +text{*Uniqueness, so NOT the axiom of choice.*}
     2.8 +lemma uniq_choice: "\<forall>x. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x. Q x (f x)"
     2.9 +  by (force intro: theI')
    2.10 +
    2.11 +lemma b_uniq_choice: "\<forall>x\<in>S. \<exists>!y. Q x y \<Longrightarrow> \<exists>f. \<forall>x\<in>S. Q x (f x)"
    2.12 +  by (force intro: theI')
    2.13  
    2.14  subsection {* The Identity Function @{text id} *}
    2.15  
    2.16 @@ -79,6 +85,9 @@
    2.17    "f -` (g -` x) = (g \<circ> f) -` x"
    2.18    by auto
    2.19  
    2.20 +lemma image_eq_imp_comp: "f ` A = g ` B \<Longrightarrow> (h o f) ` A = (h o g) ` B"
    2.21 +  by (auto simp: comp_def elim!: equalityE)
    2.22 +
    2.23  code_printing
    2.24    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    2.25  
    2.26 @@ -477,14 +486,17 @@
    2.27  lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
    2.28  by (simp add: inj_on_def, blast)
    2.29  
    2.30 -lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)"
    2.31 -by (blast dest: injD)
    2.32 +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"
    2.33 +  by (auto simp: inj_on_def)
    2.34 +
    2.35 +lemma inj_image_mem_iff: "inj f \<Longrightarrow> f a \<in> f`A \<longleftrightarrow> a \<in> A"
    2.36 +  by (blast dest: injD)
    2.37  
    2.38  lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)"
    2.39 -by (simp add: inj_on_def, blast)
    2.40 +  by (blast dest: injD)
    2.41  
    2.42  lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
    2.43 -by (blast dest: injD)
    2.44 +  by (blast dest: injD)
    2.45  
    2.46  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
    2.47  by auto
     3.1 --- a/src/HOL/HOL.thy	Tue Feb 10 12:27:30 2015 +0100
     3.2 +++ b/src/HOL/HOL.thy	Tue Feb 10 16:08:11 2015 +0000
     3.3 @@ -550,63 +550,6 @@
     3.4  done
     3.5  
     3.6  
     3.7 -subsubsection {*THE: definite description operator*}
     3.8 -
     3.9 -lemma the_equality:
    3.10 -  assumes prema: "P a"
    3.11 -      and premx: "!!x. P x ==> x=a"
    3.12 -  shows "(THE x. P x) = a"
    3.13 -apply (rule trans [OF _ the_eq_trivial])
    3.14 -apply (rule_tac f = "The" in arg_cong)
    3.15 -apply (rule ext)
    3.16 -apply (rule iffI)
    3.17 - apply (erule premx)
    3.18 -apply (erule ssubst, rule prema)
    3.19 -done
    3.20 -
    3.21 -lemma theI:
    3.22 -  assumes "P a" and "!!x. P x ==> x=a"
    3.23 -  shows "P (THE x. P x)"
    3.24 -by (iprover intro: assms the_equality [THEN ssubst])
    3.25 -
    3.26 -lemma theI': "EX! x. P x ==> P (THE x. P x)"
    3.27 -apply (erule ex1E)
    3.28 -apply (erule theI)
    3.29 -apply (erule allE)
    3.30 -apply (erule mp)
    3.31 -apply assumption
    3.32 -done
    3.33 -
    3.34 -(*Easier to apply than theI: only one occurrence of P*)
    3.35 -lemma theI2:
    3.36 -  assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
    3.37 -  shows "Q (THE x. P x)"
    3.38 -by (iprover intro: assms theI)
    3.39 -
    3.40 -lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
    3.41 -by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
    3.42 -           elim:allE impE)
    3.43 -
    3.44 -lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
    3.45 -apply (rule the_equality)
    3.46 -apply  assumption
    3.47 -apply (erule ex1E)
    3.48 -apply (erule all_dupE)
    3.49 -apply (drule mp)
    3.50 -apply  assumption
    3.51 -apply (erule ssubst)
    3.52 -apply (erule allE)
    3.53 -apply (erule mp)
    3.54 -apply assumption
    3.55 -done
    3.56 -
    3.57 -lemma the_sym_eq_trivial: "(THE y. x=y) = x"
    3.58 -apply (rule the_equality)
    3.59 -apply (rule refl)
    3.60 -apply (erule sym)
    3.61 -done
    3.62 -
    3.63 -
    3.64  subsubsection {*Classical intro rules for disjunction and existential quantifiers*}
    3.65  
    3.66  lemma disjCI:
    3.67 @@ -876,7 +819,6 @@
    3.68  
    3.69  declare ex_ex1I [intro!]
    3.70    and allI [intro!]
    3.71 -  and the_equality [intro]
    3.72    and exI [intro]
    3.73  
    3.74  declare exE [elim!]
    3.75 @@ -924,6 +866,39 @@
    3.76  *}
    3.77  
    3.78  
    3.79 +subsubsection {*THE: definite description operator*}
    3.80 +
    3.81 +lemma the_equality [intro]:
    3.82 +  assumes "P a"
    3.83 +      and "!!x. P x ==> x=a"
    3.84 +  shows "(THE x. P x) = a"
    3.85 +  by (blast intro: assms trans [OF arg_cong [where f=The] the_eq_trivial])
    3.86 +
    3.87 +lemma theI:
    3.88 +  assumes "P a" and "!!x. P x ==> x=a"
    3.89 +  shows "P (THE x. P x)"
    3.90 +by (iprover intro: assms the_equality [THEN ssubst])
    3.91 +
    3.92 +lemma theI': "EX! x. P x ==> P (THE x. P x)"
    3.93 +  by (blast intro: theI)
    3.94 +
    3.95 +(*Easier to apply than theI: only one occurrence of P*)
    3.96 +lemma theI2:
    3.97 +  assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
    3.98 +  shows "Q (THE x. P x)"
    3.99 +by (iprover intro: assms theI)
   3.100 +
   3.101 +lemma the1I2: assumes "EX! x. P x" "\<And>x. P x \<Longrightarrow> Q x" shows "Q (THE x. P x)"
   3.102 +by(iprover intro:assms(2) theI2[where P=P and Q=Q] ex1E[OF assms(1)]
   3.103 +           elim:allE impE)
   3.104 +
   3.105 +lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
   3.106 +  by blast
   3.107 +
   3.108 +lemma the_sym_eq_trivial: "(THE y. x=y) = x"
   3.109 +  by blast
   3.110 +
   3.111 +
   3.112  subsubsection {* Simplifier *}
   3.113  
   3.114  lemma eta_contract_eq: "(%s. f s) = f" ..
   3.115 @@ -1099,8 +1074,7 @@
   3.116  
   3.117  lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
   3.118    -- {* And this form is useful for expanding @{text "if"}s on the LEFT. *}
   3.119 -  apply (simplesubst split_if, blast)
   3.120 -  done
   3.121 +  by (simplesubst split_if) blast
   3.122  
   3.123  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
   3.124  lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
     4.1 --- a/src/HOL/Set.thy	Tue Feb 10 12:27:30 2015 +0100
     4.2 +++ b/src/HOL/Set.thy	Tue Feb 10 16:08:11 2015 +0000
     4.3 @@ -1020,6 +1020,9 @@
     4.4    "f ` A - f ` B \<subseteq> f ` (A - B)"
     4.5    by blast
     4.6  
     4.7 +lemma Setcompr_eq_image: "{f x | x. x \<in> A} = f ` A"
     4.8 +  by blast
     4.9 +
    4.10  lemma ball_imageD:
    4.11    assumes "\<forall>x\<in>f ` A. P x"
    4.12    shows "\<forall>x\<in>A. P (f x)"
    4.13 @@ -1241,6 +1244,9 @@
    4.14  lemma Collect_conj_eq: "{x. P x & Q x} = {x. P x} \<inter> {x. Q x}"
    4.15    by blast
    4.16  
    4.17 +lemma Collect_mono_iff [simp]: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)"
    4.18 +  by blast
    4.19 +
    4.20  
    4.21  text {* \medskip @{text insert}. *}
    4.22