conciliated Inf/Inf_fin
authorhaftmann
Mon Aug 20 18:07:25 2007 +0200 (2007-08-20)
changeset 24342a1d489e254ec
parent 24341 7b8da2396c49
child 24343 acc0f7aac619
conciliated Inf/Inf_fin
NEWS
src/HOL/Finite_Set.thy
     1.1 --- a/NEWS	Mon Aug 20 17:46:32 2007 +0200
     1.2 +++ b/NEWS	Mon Aug 20 18:07:25 2007 +0200
     1.3 @@ -635,6 +635,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* theory Finite_Set: "name-space" locales Lattice, Distrib_lattice, Linorder etc.
     1.8 +have disappeared; operations defined in terms of fold_set now are named
     1.9 +Inf_fin, Sup_fin.  INCOMPATIBILITY.
    1.10 +
    1.11  * HOL-Word:
    1.12    New extensive library and type for generic, fixed size machine
    1.13    words, with arithemtic, bit-wise, shifting and rotating operations,
    1.14 @@ -814,12 +818,12 @@
    1.15      Nat.size ~> Nat.size_class.size
    1.16      Numeral.number_of ~> Numeral.number_class.number_of
    1.17      FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf
    1.18 +    FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
    1.19  
    1.20  * Rudimentary class target mechanism involves constant renames:
    1.21  
    1.22      Orderings.min ~> Orderings.ord_class.min
    1.23      Orderings.max ~> Orderings.ord_class.max
    1.24 -    FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
    1.25  
    1.26  * primrec: missing cases mapped to "undefined" instead of "arbitrary"
    1.27  
    1.28 @@ -871,7 +875,7 @@
    1.29      class "comp_lat" now named "complete_lattice"
    1.30  
    1.31      Instantiation of lattice classes allows explicit definitions
    1.32 -    for "inf" and "sup" operations.
    1.33 +    for "inf" and "sup" operations (or "Inf" and "Sup" for complete lattices).
    1.34  
    1.35    INCOMPATIBILITY.  Theorem renames:
    1.36  
    1.37 @@ -965,6 +969,11 @@
    1.38      Meet_lower              ~> Inf_lower
    1.39      Meet_set_def            ~> Inf_set_def
    1.40  
    1.41 +    Sup_def                 ~> Sup_Inf
    1.42 +    Sup_bool_eq             ~> Sup_bool_def
    1.43 +    Sup_fun_eq              ~> Sup_fun_def
    1.44 +    Sup_set_eq              ~> Sup_set_def
    1.45 +
    1.46      listsp_meetI            ~> listsp_infI
    1.47      listsp_meet_eq          ~> listsp_inf_eq
    1.48  
     2.1 --- a/src/HOL/Finite_Set.thy	Mon Aug 20 17:46:32 2007 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Mon Aug 20 18:07:25 2007 +0200
     2.3 @@ -1775,8 +1775,7 @@
     2.4    apply (blast elim!: equalityE)
     2.5    done
     2.6  
     2.7 -text {* Relates to equivalence classes.  Based on a theorem of
     2.8 -F. Kamm�ller's.  *}
     2.9 +text {* Relates to equivalence classes.  Based on a theorem of F. Kammüller.  *}
    2.10  
    2.11  lemma dvd_partition:
    2.12    "finite (Union C) ==>
    2.13 @@ -2276,7 +2275,7 @@
    2.14  
    2.15  subsection {* Finiteness and quotients *}
    2.16  
    2.17 -text {*Suggested by Florian Kamm�ller*}
    2.18 +text {*Suggested by Florian Kammüller*}
    2.19  
    2.20  lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
    2.21    -- {* recall @{thm equiv_type} *}
    2.22 @@ -2359,25 +2358,23 @@
    2.23  lemmas int_setprod = of_nat_setprod [where 'a=int]
    2.24  
    2.25  
    2.26 -locale Lattice = lattice -- {* we do not pollute the @{text lattice} clas *}
    2.27 +context lattice
    2.28  begin
    2.29  
    2.30  definition
    2.31 -  Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    2.32 +  Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^bsub>fin\<^esub>_" [900] 900)
    2.33  where
    2.34 -  "Inf = fold1 (op \<sqinter>)"
    2.35 +  "Inf_fin = fold1 (op \<sqinter>)"
    2.36  
    2.37  definition
    2.38 -  Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    2.39 +  Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^bsub>fin\<^esub>_" [900] 900)
    2.40  where
    2.41 -  "Sup = fold1 (op \<squnion>)"
    2.42 -
    2.43 -end
    2.44 -
    2.45 -locale Distrib_Lattice = distrib_lattice + Lattice
    2.46 -
    2.47 -lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
    2.48 -apply(unfold Sup_def Inf_def)
    2.49 +  "Sup_fin = fold1 (op \<squnion>)"
    2.50 +
    2.51 +end context lattice begin
    2.52 +
    2.53 +lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A \<sqsubseteq> \<Squnion>\<^bsub>fin\<^esub>A"
    2.54 +apply(unfold Sup_fin_def Inf_fin_def)
    2.55  apply(subgoal_tac "EX a. a:A")
    2.56  prefer 2 apply blast
    2.57  apply(erule exE)
    2.58 @@ -2386,31 +2383,34 @@
    2.59  apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
    2.60  done
    2.61  
    2.62 -lemma (in Lattice) sup_Inf_absorb[simp]:
    2.63 -  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
    2.64 +lemma sup_Inf_absorb [simp]:
    2.65 +  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>\<^bsub>fin\<^esub>A) = a"
    2.66  apply(subst sup_commute)
    2.67 -apply(simp add:Inf_def sup_absorb2 ACIfSL.fold1_belowI[OF ACIfSL_inf])
    2.68 +apply(simp add: Inf_fin_def sup_absorb2 ACIfSL.fold1_belowI [OF ACIfSL_inf])
    2.69  done
    2.70  
    2.71 -lemma (in Lattice) inf_Sup_absorb[simp]:
    2.72 -  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
    2.73 -by(simp add:Sup_def inf_absorb1 ACIfSL.fold1_belowI[OF ACIfSL_sup])
    2.74 -
    2.75 -lemma (in Distrib_Lattice) sup_Inf1_distrib:
    2.76 - "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<squnion> \<Sqinter>A) = \<Sqinter>{x \<squnion> a|a. a \<in> A}"
    2.77 -apply(simp add:Inf_def image_def
    2.78 +lemma inf_Sup_absorb [simp]:
    2.79 +  "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>\<^bsub>fin\<^esub>A) = a"
    2.80 +by(simp add: Sup_fin_def inf_absorb1 ACIfSL.fold1_belowI [OF ACIfSL_sup])
    2.81 +
    2.82 +end
    2.83 +
    2.84 +context distrib_lattice
    2.85 +begin
    2.86 +
    2.87 +lemma sup_Inf1_distrib:
    2.88 + "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<squnion> \<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{x \<squnion> a|a. a \<in> A}"
    2.89 +apply(simp add: Inf_fin_def image_def
    2.90    ACIf.hom_fold1_commute[OF ACIf_inf, where h="sup x", OF sup_inf_distrib1])
    2.91  apply(rule arg_cong, blast)
    2.92  done
    2.93  
    2.94 -
    2.95 -lemma (in Distrib_Lattice) sup_Inf2_distrib:
    2.96 -assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
    2.97 -shows "(\<Sqinter>A \<squnion> \<Sqinter>B) = \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
    2.98 -using A
    2.99 -proof (induct rule: finite_ne_induct)
   2.100 +lemma sup_Inf2_distrib:
   2.101 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   2.102 +  shows "(\<Sqinter>\<^bsub>fin\<^esub>A \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
   2.103 +using A proof (induct rule: finite_ne_induct)
   2.104    case singleton thus ?case
   2.105 -    by (simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def])
   2.106 +    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
   2.107  next
   2.108    case (insert x A)
   2.109    have finB: "finite {x \<squnion> b |b. b \<in> B}"
   2.110 @@ -2422,37 +2422,34 @@
   2.111      thus ?thesis by(simp add: insert(1) B(1))
   2.112    qed
   2.113    have ne: "{a \<squnion> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   2.114 -  have "\<Sqinter>(insert x A) \<squnion> \<Sqinter>B = (x \<sqinter> \<Sqinter>A) \<squnion> \<Sqinter>B"
   2.115 +  have "\<Sqinter>\<^bsub>fin\<^esub>(insert x A) \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B = (x \<sqinter> \<Sqinter>\<^bsub>fin\<^esub>A) \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B"
   2.116      using insert
   2.117 - by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def])
   2.118 -  also have "\<dots> = (x \<squnion> \<Sqinter>B) \<sqinter> (\<Sqinter>A \<squnion> \<Sqinter>B)" by(rule sup_inf_distrib2)
   2.119 -  also have "\<dots> = \<Sqinter>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
   2.120 + by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_fin_def])
   2.121 +  also have "\<dots> = (x \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B) \<sqinter> (\<Sqinter>\<^bsub>fin\<^esub>A \<squnion> \<Sqinter>\<^bsub>fin\<^esub>B)" by(rule sup_inf_distrib2)
   2.122 +  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>{x \<squnion> b|b. b \<in> B} \<sqinter> \<Sqinter>\<^bsub>fin\<^esub>{a \<squnion> b|a b. a \<in> A \<and> b \<in> B}"
   2.123      using insert by(simp add:sup_Inf1_distrib[OF B])
   2.124 -  also have "\<dots> = \<Sqinter>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
   2.125 -    (is "_ = \<Sqinter>?M")
   2.126 +  also have "\<dots> = \<Sqinter>\<^bsub>fin\<^esub>({x\<squnion>b |b. b \<in> B} \<union> {a\<squnion>b |a b. a \<in> A \<and> b \<in> B})"
   2.127 +    (is "_ = \<Sqinter>\<^bsub>fin\<^esub>?M")
   2.128      using B insert
   2.129 -    by(simp add:Inf_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
   2.130 +    by (simp add: Inf_fin_def ACIf.fold1_Un2[OF ACIf_inf finB _ finAB ne])
   2.131    also have "?M = {a \<squnion> b |a b. a \<in> insert x A \<and> b \<in> B}"
   2.132      by blast
   2.133    finally show ?case .
   2.134  qed
   2.135  
   2.136 -
   2.137 -lemma (in Distrib_Lattice) inf_Sup1_distrib:
   2.138 - "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<sqinter> \<Squnion>A) = \<Squnion>{x \<sqinter> a|a. a \<in> A}"
   2.139 -apply(simp add:Sup_def image_def
   2.140 +lemma inf_Sup1_distrib:
   2.141 + "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (x \<sqinter> \<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{x \<sqinter> a|a. a \<in> A}"
   2.142 +apply (simp add: Sup_fin_def image_def
   2.143    ACIf.hom_fold1_commute[OF ACIf_sup, where h="inf x", OF inf_sup_distrib1])
   2.144 -apply(rule arg_cong, blast)
   2.145 +apply (rule arg_cong, blast)
   2.146  done
   2.147  
   2.148 -
   2.149 -lemma (in Distrib_Lattice) inf_Sup2_distrib:
   2.150 -assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   2.151 -shows "(\<Squnion>A \<sqinter> \<Squnion>B) = \<Squnion>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
   2.152 -using A
   2.153 -proof (induct rule: finite_ne_induct)
   2.154 +lemma inf_Sup2_distrib:
   2.155 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   2.156 +  shows "(\<Squnion>\<^bsub>fin\<^esub>A \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
   2.157 +using A proof (induct rule: finite_ne_induct)
   2.158    case singleton thus ?case
   2.159 -    by(simp add: inf_Sup1_distrib[OF B] fold1_singleton_def[OF Sup_def])
   2.160 +    by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
   2.161  next
   2.162    case (insert x A)
   2.163    have finB: "finite {x \<sqinter> b |b. b \<in> B}"
   2.164 @@ -2464,35 +2461,41 @@
   2.165      thus ?thesis by(simp add: insert(1) B(1))
   2.166    qed
   2.167    have ne: "{a \<sqinter> b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   2.168 -  have "\<Squnion>(insert x A) \<sqinter> \<Squnion>B = (x \<squnion> \<Squnion>A) \<sqinter> \<Squnion>B"
   2.169 -    using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_sup Sup_def])
   2.170 -  also have "\<dots> = (x \<sqinter> \<Squnion>B) \<squnion> (\<Squnion>A \<sqinter> \<Squnion>B)" by(rule inf_sup_distrib2)
   2.171 -  also have "\<dots> = \<Squnion>{x \<sqinter> b|b. b \<in> B} \<squnion> \<Squnion>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
   2.172 +  have "\<Squnion>\<^bsub>fin\<^esub>(insert x A) \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B = (x \<squnion> \<Squnion>\<^bsub>fin\<^esub>A) \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B"
   2.173 +    using insert by (simp add: ACIf.fold1_insert_idem_def [OF ACIf_sup Sup_fin_def])
   2.174 +  also have "\<dots> = (x \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B) \<squnion> (\<Squnion>\<^bsub>fin\<^esub>A \<sqinter> \<Squnion>\<^bsub>fin\<^esub>B)" by(rule inf_sup_distrib2)
   2.175 +  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>{x \<sqinter> b|b. b \<in> B} \<squnion> \<Squnion>\<^bsub>fin\<^esub>{a \<sqinter> b|a b. a \<in> A \<and> b \<in> B}"
   2.176      using insert by(simp add:inf_Sup1_distrib[OF B])
   2.177 -  also have "\<dots> = \<Squnion>({x\<sqinter>b |b. b \<in> B} \<union> {a\<sqinter>b |a b. a \<in> A \<and> b \<in> B})"
   2.178 -    (is "_ = \<Squnion>?M")
   2.179 +  also have "\<dots> = \<Squnion>\<^bsub>fin\<^esub>({x\<sqinter>b |b. b \<in> B} \<union> {a\<sqinter>b |a b. a \<in> A \<and> b \<in> B})"
   2.180 +    (is "_ = \<Squnion>\<^bsub>fin\<^esub>?M")
   2.181      using B insert
   2.182 -    by(simp add:Sup_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
   2.183 +    by (simp add: Sup_fin_def ACIf.fold1_Un2[OF ACIf_sup finB _ finAB ne])
   2.184    also have "?M = {a \<sqinter> b |a b. a \<in> insert x A \<and> b \<in> B}"
   2.185      by blast
   2.186    finally show ?case .
   2.187  qed
   2.188  
   2.189 +end
   2.190 +
   2.191 +context complete_lattice
   2.192 +begin
   2.193 +
   2.194  text {*
   2.195 -  Infimum and supremum in complete lattices may also
   2.196 -  be characterized by @{const fold1}:
   2.197 +  Coincidence on finite sets in complete lattices:
   2.198  *}
   2.199  
   2.200 -lemma (in complete_lattice) Inf_fold1:
   2.201 -  "finite A \<Longrightarrow>  A \<noteq> {} \<Longrightarrow> \<Sqinter>A = fold1 (op \<sqinter>) A"
   2.202 -by (induct A set: finite)
   2.203 +lemma Inf_fin_Inf:
   2.204 +  "finite A \<Longrightarrow>  A \<noteq> {} \<Longrightarrow> \<Sqinter>\<^bsub>fin\<^esub>A = \<Sqinter>A"
   2.205 +unfolding Inf_fin_def by (induct A set: finite)
   2.206     (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf])
   2.207  
   2.208 -lemma (in complete_lattice) Sup_fold1:
   2.209 -  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>A = fold1 (op \<squnion>) A"
   2.210 -by (induct A set: finite)
   2.211 +lemma Sup_fin_Sup:
   2.212 +  "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> \<Squnion>\<^bsub>fin\<^esub>A = \<Squnion>A"
   2.213 +unfolding Sup_fin_def by (induct A set: finite)
   2.214     (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup])
   2.215  
   2.216 +end
   2.217 +
   2.218  
   2.219  subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *}
   2.220  
   2.221 @@ -2502,7 +2505,7 @@
   2.222    over (non-empty) sets by means of @{text fold1}.
   2.223  *}
   2.224  
   2.225 -locale Linorder = linorder -- {* we do not pollute the @{text linorder} class *}
   2.226 +context linorder
   2.227  begin
   2.228  
   2.229  definition
   2.230 @@ -2515,6 +2518,8 @@
   2.231  where
   2.232    "Max = fold1 max"
   2.233  
   2.234 +end context linorder begin
   2.235 +
   2.236  text {* recall: @{term min} and @{term max} behave like @{const inf} and @{const sup} *}
   2.237  
   2.238  lemma ACIf_min: "ACIf min"
   2.239 @@ -2648,7 +2653,7 @@
   2.240  
   2.241  end
   2.242  
   2.243 -locale Linorder_ab_semigroup_add = Linorder + pordered_ab_semigroup_add
   2.244 +class linordered_ab_semigroup_add = linorder + pordered_ab_semigroup_add
   2.245  begin
   2.246  
   2.247  lemma add_Min_commute:
   2.248 @@ -2673,37 +2678,6 @@
   2.249  
   2.250  end
   2.251  
   2.252 -definition
   2.253 -  Min :: "'a set \<Rightarrow> 'a\<Colon>linorder"
   2.254 -where
   2.255 -  "Min = fold1 min"
   2.256 -
   2.257 -definition
   2.258 -  Max :: "'a set \<Rightarrow> 'a\<Colon>linorder"
   2.259 -where
   2.260 -  "Max = fold1 max"
   2.261 -
   2.262 -interpretation
   2.263 -  Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
   2.264 -where
   2.265 -  "Linorder.Min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = Min"
   2.266 -  and "Linorder.Max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = Max"
   2.267 -proof -
   2.268 -  show "Linorder (op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool) op <"
   2.269 -  by (rule Linorder.intro, rule linorder_axioms)
   2.270 -  then interpret Linorder: Linorder ["op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <"] .
   2.271 -  show "Linorder.Min = Min" by (simp add: Min_def Linorder.Min_def ord_class.min)
   2.272 -  show "Linorder.Max = Max" by (simp add: Max_def Linorder.Max_def ord_class.max)
   2.273 -qed
   2.274 -
   2.275 -interpretation
   2.276 -  Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"]
   2.277 -proof -
   2.278 -  show "Linorder_ab_semigroup_add (op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool) (op <) (op +)"
   2.279 -  by (rule Linorder_ab_semigroup_add.intro,
   2.280 -    rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms)
   2.281 -qed
   2.282 -
   2.283  
   2.284  subsection {* Class @{text finite} *}
   2.285