src/HOL/Fun.thy
changeset 56015 57e2cfba9c6e
parent 55990 41c6b99c5fb7
child 56077 d397030fb27e
     1.1 --- a/src/HOL/Fun.thy	Sun Mar 09 22:45:07 2014 +0100
     1.2 +++ b/src/HOL/Fun.thy	Sun Mar 09 22:45:09 2014 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Notions about functions *}
     1.5  
     1.6  theory Fun
     1.7 -imports Complete_Lattices
     1.8 +imports Set
     1.9  keywords "functor" :: thy_goal
    1.10  begin
    1.11  
    1.12 @@ -79,14 +79,6 @@
    1.13    "(g \<circ> f) -` x = f -` (g -` x)"
    1.14    by auto
    1.15  
    1.16 -lemma INF_comp:
    1.17 -  "INFI A (g \<circ> f) = INFI (f ` A) g"
    1.18 -  by (simp add: INF_def image_comp)
    1.19 -
    1.20 -lemma SUP_comp:
    1.21 -  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    1.22 -  by (simp add: SUP_def image_comp)
    1.23 -
    1.24  code_printing
    1.25    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    1.26  
    1.27 @@ -189,44 +181,6 @@
    1.28  lemma inj_on_Int: "inj_on f A \<or> inj_on f B \<Longrightarrow> inj_on f (A \<inter> B)"
    1.29  unfolding inj_on_def by blast
    1.30  
    1.31 -lemma inj_on_INTER:
    1.32 -  "\<lbrakk>I \<noteq> {}; \<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)\<rbrakk> \<Longrightarrow> inj_on f (\<Inter> i \<in> I. A i)"
    1.33 -unfolding inj_on_def by blast
    1.34 -
    1.35 -lemma inj_on_Inter:
    1.36 -  "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> inj_on f A\<rbrakk> \<Longrightarrow> inj_on f (Inter S)"
    1.37 -unfolding inj_on_def by blast
    1.38 -
    1.39 -lemma inj_on_UNION_chain:
    1.40 -  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
    1.41 -         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.42 -  shows "inj_on f (\<Union> i \<in> I. A i)"
    1.43 -proof -
    1.44 -  {
    1.45 -    fix i j x y
    1.46 -    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    1.47 -      and ***: "f x = f y"
    1.48 -    have "x = y"
    1.49 -    proof -
    1.50 -      {
    1.51 -        assume "A i \<le> A j"
    1.52 -        with ** have "x \<in> A j" by auto
    1.53 -        with INJ * ** *** have ?thesis
    1.54 -        by(auto simp add: inj_on_def)
    1.55 -      }
    1.56 -      moreover
    1.57 -      {
    1.58 -        assume "A j \<le> A i"
    1.59 -        with ** have "y \<in> A i" by auto
    1.60 -        with INJ * ** *** have ?thesis
    1.61 -        by(auto simp add: inj_on_def)
    1.62 -      }
    1.63 -      ultimately show ?thesis using CH * by blast
    1.64 -    qed
    1.65 -  }
    1.66 -  then show ?thesis by (unfold inj_on_def UNION_eq) auto
    1.67 -qed
    1.68 -
    1.69  lemma surj_id: "surj id"
    1.70  by simp
    1.71  
    1.72 @@ -456,29 +410,6 @@
    1.73    shows "bij_betw f (A \<union> C) (B \<union> D)"
    1.74    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
    1.75  
    1.76 -lemma bij_betw_UNION_chain:
    1.77 -  assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
    1.78 -         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
    1.79 -  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
    1.80 -proof (unfold bij_betw_def, auto)
    1.81 -  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.82 -  using BIJ bij_betw_def[of f] by auto
    1.83 -  thus "inj_on f (\<Union> i \<in> I. A i)"
    1.84 -  using CH inj_on_UNION_chain[of I A f] by auto
    1.85 -next
    1.86 -  fix i x
    1.87 -  assume *: "i \<in> I" "x \<in> A i"
    1.88 -  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
    1.89 -  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
    1.90 -next
    1.91 -  fix i x'
    1.92 -  assume *: "i \<in> I" "x' \<in> A' i"
    1.93 -  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
    1.94 -  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
    1.95 -    using * by blast
    1.96 -  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by (simp add: image_def)
    1.97 -qed
    1.98 -
    1.99  lemma bij_betw_subset:
   1.100    assumes BIJ: "bij_betw f A A'" and
   1.101            SUB: "B \<le> A" and IM: "f ` B = B'"
   1.102 @@ -539,20 +470,6 @@
   1.103  lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
   1.104  by (blast dest: injD)
   1.105  
   1.106 -(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   1.107 -lemma image_INT:
   1.108 -   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
   1.109 -    ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   1.110 -apply (simp add: inj_on_def, blast)
   1.111 -done
   1.112 -
   1.113 -(*Compare with image_INT: no use of inj_on, and if f is surjective then
   1.114 -  it doesn't matter whether A is empty*)
   1.115 -lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   1.116 -apply (simp add: bij_def)
   1.117 -apply (simp add: inj_on_def surj_def, blast)
   1.118 -done
   1.119 -
   1.120  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
   1.121  by auto
   1.122  
   1.123 @@ -707,10 +624,6 @@
   1.124  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   1.125    by auto
   1.126  
   1.127 -lemma UNION_fun_upd:
   1.128 -  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
   1.129 -by (auto split: if_splits)
   1.130 -
   1.131  
   1.132  subsection {* @{text override_on} *}
   1.133  
   1.134 @@ -927,3 +840,4 @@
   1.135  lemmas vimage_compose = vimage_comp
   1.136  
   1.137  end
   1.138 +