bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
authorhaftmann
Sun Mar 09 22:45:09 2014 +0100 (2014-03-09)
changeset 5601557e2cfba9c6e
parent 56014 aaa3f2365fc5
child 56016 8875cdcfc85b
child 56022 8c9ab5d91d5a
bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
* * *
tuned
src/HOL/Complete_Lattices.thy
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Sun Mar 09 22:45:07 2014 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Mar 09 22:45:09 2014 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  header {* Complete lattices *}
     1.5  
     1.6  theory Complete_Lattices
     1.7 -imports Set
     1.8 +imports Fun
     1.9  begin
    1.10  
    1.11  notation
    1.12 @@ -20,6 +20,10 @@
    1.13  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.14    INF_def: "INFI A f = \<Sqinter>(f ` A)"
    1.15  
    1.16 +lemma INF_comp: -- {* FIXME drop *}
    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 INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
    1.21    by (simp add: INF_def image_image)
    1.22  
    1.23 @@ -35,6 +39,10 @@
    1.24  definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.25    SUP_def: "SUPR A f = \<Squnion>(f ` A)"
    1.26  
    1.27 +lemma SUP_comp: -- {* FIXME drop *}
    1.28 +  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    1.29 +  by (simp add: SUP_def image_comp)
    1.30 +
    1.31  lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
    1.32    by (simp add: SUP_def image_image)
    1.33  
    1.34 @@ -1224,6 +1232,88 @@
    1.35    by (fact Sup_inf_eq_bot_iff)
    1.36  
    1.37  
    1.38 +subsection {* Injections and bijections *}
    1.39 +
    1.40 +lemma inj_on_Inter:
    1.41 +  "S \<noteq> {} \<Longrightarrow> (\<And>A. A \<in> S \<Longrightarrow> inj_on f A) \<Longrightarrow> inj_on f (\<Inter>S)"
    1.42 +  unfolding inj_on_def by blast
    1.43 +
    1.44 +lemma inj_on_INTER:
    1.45 +  "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> inj_on f (A i)) \<Longrightarrow> inj_on f (\<Inter>i \<in> I. A i)"
    1.46 +  unfolding inj_on_def by blast
    1.47 +
    1.48 +lemma inj_on_UNION_chain:
    1.49 +  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.50 +         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.51 +  shows "inj_on f (\<Union> i \<in> I. A i)"
    1.52 +proof -
    1.53 +  {
    1.54 +    fix i j x y
    1.55 +    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    1.56 +      and ***: "f x = f y"
    1.57 +    have "x = y"
    1.58 +    proof -
    1.59 +      {
    1.60 +        assume "A i \<le> A j"
    1.61 +        with ** have "x \<in> A j" by auto
    1.62 +        with INJ * ** *** have ?thesis
    1.63 +        by(auto simp add: inj_on_def)
    1.64 +      }
    1.65 +      moreover
    1.66 +      {
    1.67 +        assume "A j \<le> A i"
    1.68 +        with ** have "y \<in> A i" by auto
    1.69 +        with INJ * ** *** have ?thesis
    1.70 +        by(auto simp add: inj_on_def)
    1.71 +      }
    1.72 +      ultimately show ?thesis using CH * by blast
    1.73 +    qed
    1.74 +  }
    1.75 +  then show ?thesis by (unfold inj_on_def UNION_eq) auto
    1.76 +qed
    1.77 +
    1.78 +lemma bij_betw_UNION_chain:
    1.79 +  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.80 +         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
    1.81 +  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
    1.82 +proof (unfold bij_betw_def, auto)
    1.83 +  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    1.84 +  using BIJ bij_betw_def[of f] by auto
    1.85 +  thus "inj_on f (\<Union> i \<in> I. A i)"
    1.86 +  using CH inj_on_UNION_chain[of I A f] by auto
    1.87 +next
    1.88 +  fix i x
    1.89 +  assume *: "i \<in> I" "x \<in> A i"
    1.90 +  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
    1.91 +  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
    1.92 +next
    1.93 +  fix i x'
    1.94 +  assume *: "i \<in> I" "x' \<in> A' i"
    1.95 +  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
    1.96 +  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
    1.97 +    using * by blast
    1.98 +  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by blast
    1.99 +qed
   1.100 +
   1.101 +(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   1.102 +lemma image_INT:
   1.103 +   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
   1.104 +    ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   1.105 +apply (simp add: inj_on_def, blast)
   1.106 +done
   1.107 +
   1.108 +(*Compare with image_INT: no use of inj_on, and if f is surjective then
   1.109 +  it doesn't matter whether A is empty*)
   1.110 +lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   1.111 +apply (simp add: bij_def)
   1.112 +apply (simp add: inj_on_def surj_def, blast)
   1.113 +done
   1.114 +
   1.115 +lemma UNION_fun_upd:
   1.116 +  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
   1.117 +by (auto split: if_splits)
   1.118 +
   1.119 +
   1.120  subsubsection {* Complement *}
   1.121  
   1.122  lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
     2.1 --- a/src/HOL/Fun.thy	Sun Mar 09 22:45:07 2014 +0100
     2.2 +++ b/src/HOL/Fun.thy	Sun Mar 09 22:45:09 2014 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* Notions about functions *}
     2.5  
     2.6  theory Fun
     2.7 -imports Complete_Lattices
     2.8 +imports Set
     2.9  keywords "functor" :: thy_goal
    2.10  begin
    2.11  
    2.12 @@ -79,14 +79,6 @@
    2.13    "(g \<circ> f) -` x = f -` (g -` x)"
    2.14    by auto
    2.15  
    2.16 -lemma INF_comp:
    2.17 -  "INFI A (g \<circ> f) = INFI (f ` A) g"
    2.18 -  by (simp add: INF_def image_comp)
    2.19 -
    2.20 -lemma SUP_comp:
    2.21 -  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    2.22 -  by (simp add: SUP_def image_comp)
    2.23 -
    2.24  code_printing
    2.25    constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    2.26  
    2.27 @@ -189,44 +181,6 @@
    2.28  lemma inj_on_Int: "inj_on f A \<or> inj_on f B \<Longrightarrow> inj_on f (A \<inter> B)"
    2.29  unfolding inj_on_def by blast
    2.30  
    2.31 -lemma inj_on_INTER:
    2.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)"
    2.33 -unfolding inj_on_def by blast
    2.34 -
    2.35 -lemma inj_on_Inter:
    2.36 -  "\<lbrakk>S \<noteq> {}; \<And> A. A \<in> S \<Longrightarrow> inj_on f A\<rbrakk> \<Longrightarrow> inj_on f (Inter S)"
    2.37 -unfolding inj_on_def by blast
    2.38 -
    2.39 -lemma inj_on_UNION_chain:
    2.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
    2.41 -         INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    2.42 -  shows "inj_on f (\<Union> i \<in> I. A i)"
    2.43 -proof -
    2.44 -  {
    2.45 -    fix i j x y
    2.46 -    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    2.47 -      and ***: "f x = f y"
    2.48 -    have "x = y"
    2.49 -    proof -
    2.50 -      {
    2.51 -        assume "A i \<le> A j"
    2.52 -        with ** have "x \<in> A j" by auto
    2.53 -        with INJ * ** *** have ?thesis
    2.54 -        by(auto simp add: inj_on_def)
    2.55 -      }
    2.56 -      moreover
    2.57 -      {
    2.58 -        assume "A j \<le> A i"
    2.59 -        with ** have "y \<in> A i" by auto
    2.60 -        with INJ * ** *** have ?thesis
    2.61 -        by(auto simp add: inj_on_def)
    2.62 -      }
    2.63 -      ultimately show ?thesis using CH * by blast
    2.64 -    qed
    2.65 -  }
    2.66 -  then show ?thesis by (unfold inj_on_def UNION_eq) auto
    2.67 -qed
    2.68 -
    2.69  lemma surj_id: "surj id"
    2.70  by simp
    2.71  
    2.72 @@ -456,29 +410,6 @@
    2.73    shows "bij_betw f (A \<union> C) (B \<union> D)"
    2.74    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
    2.75  
    2.76 -lemma bij_betw_UNION_chain:
    2.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
    2.78 -         BIJ: "\<And> i. i \<in> I \<Longrightarrow> bij_betw f (A i) (A' i)"
    2.79 -  shows "bij_betw f (\<Union> i \<in> I. A i) (\<Union> i \<in> I. A' i)"
    2.80 -proof (unfold bij_betw_def, auto)
    2.81 -  have "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
    2.82 -  using BIJ bij_betw_def[of f] by auto
    2.83 -  thus "inj_on f (\<Union> i \<in> I. A i)"
    2.84 -  using CH inj_on_UNION_chain[of I A f] by auto
    2.85 -next
    2.86 -  fix i x
    2.87 -  assume *: "i \<in> I" "x \<in> A i"
    2.88 -  hence "f x \<in> A' i" using BIJ bij_betw_def[of f] by auto
    2.89 -  thus "\<exists>j \<in> I. f x \<in> A' j" using * by blast
    2.90 -next
    2.91 -  fix i x'
    2.92 -  assume *: "i \<in> I" "x' \<in> A' i"
    2.93 -  hence "\<exists>x \<in> A i. x' = f x" using BIJ bij_betw_def[of f] by blast
    2.94 -  then have "\<exists>j \<in> I. \<exists>x \<in> A j. x' = f x"
    2.95 -    using * by blast
    2.96 -  then show "x' \<in> f ` (\<Union>x\<in>I. A x)" by (simp add: image_def)
    2.97 -qed
    2.98 -
    2.99  lemma bij_betw_subset:
   2.100    assumes BIJ: "bij_betw f A A'" and
   2.101            SUB: "B \<le> A" and IM: "f ` B = B'"
   2.102 @@ -539,20 +470,6 @@
   2.103  lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
   2.104  by (blast dest: injD)
   2.105  
   2.106 -(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   2.107 -lemma image_INT:
   2.108 -   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
   2.109 -    ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   2.110 -apply (simp add: inj_on_def, blast)
   2.111 -done
   2.112 -
   2.113 -(*Compare with image_INT: no use of inj_on, and if f is surjective then
   2.114 -  it doesn't matter whether A is empty*)
   2.115 -lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   2.116 -apply (simp add: bij_def)
   2.117 -apply (simp add: inj_on_def surj_def, blast)
   2.118 -done
   2.119 -
   2.120  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
   2.121  by auto
   2.122  
   2.123 @@ -707,10 +624,6 @@
   2.124  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
   2.125    by auto
   2.126  
   2.127 -lemma UNION_fun_upd:
   2.128 -  "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
   2.129 -by (auto split: if_splits)
   2.130 -
   2.131  
   2.132  subsection {* @{text override_on} *}
   2.133  
   2.134 @@ -927,3 +840,4 @@
   2.135  lemmas vimage_compose = vimage_comp
   2.136  
   2.137  end
   2.138 +