1.1 --- a/src/HOL/Finite_Set.thy Mon Apr 18 10:36:05 2005 +0200
1.2 +++ b/src/HOL/Finite_Set.thy Mon Apr 18 15:53:51 2005 +0200
1.3 @@ -509,21 +509,30 @@
1.4
1.5 lemmas (in ACIf) ACI = AC idem idem2
1.6
1.7 -text{* Instantiation of locales: *}
1.8 +text{* Interpretation of locales: *}
1.9
1.10 +interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
1.11 +by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
1.12 +
1.13 +interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
1.14 + apply -
1.15 + apply (fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
1.16 + apply (fastsimp intro: ACe_axioms.intro mult_assoc ab_semigroup_mult.mult_commute)
1.17 + done
1.18 +
1.19 +(*
1.20 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
1.21 by(fastsimp intro: ACf.intro add_assoc add_commute)
1.22
1.23 lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
1.24 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
1.25
1.26 -
1.27 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
1.28 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
1.29
1.30 -lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
1.31 +lemma ACe_mult: "ACe (op * ) (1::'a::comm_monoid_mult)"
1.32 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
1.33 -
1.34 +*)
1.35
1.36 subsubsection{*From @{term foldSet} to @{term fold}*}
1.37
1.38 @@ -878,14 +887,14 @@
1.39
1.40 lemma setsum_insert [simp]:
1.41 "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
1.42 - by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
1.43 + by (simp add: setsum_def)
1.44
1.45 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
1.46 by (simp add: setsum_def)
1.47
1.48 lemma setsum_reindex:
1.49 "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
1.50 -by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
1.51 +by(auto simp add: setsum_def AC_add.fold_reindex dest!:finite_imageD)
1.52
1.53 lemma setsum_reindex_id:
1.54 "inj_on f B ==> setsum f B = setsum id (f ` B)"
1.55 @@ -893,7 +902,7 @@
1.56
1.57 lemma setsum_cong:
1.58 "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
1.59 -by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
1.60 +by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
1.61
1.62 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
1.63 by (rule setsum_cong[OF refl], auto);
1.64 @@ -905,7 +914,7 @@
1.65
1.66 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
1.67 apply (clarsimp simp: setsum_def)
1.68 -apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
1.69 +apply (erule finite_induct, auto)
1.70 done
1.71
1.72 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
1.73 @@ -914,7 +923,7 @@
1.74 lemma setsum_Un_Int: "finite A ==> finite B ==>
1.75 setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
1.76 -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
1.77 -by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
1.78 +by(simp add: setsum_def AC_add.fold_Un_Int [symmetric])
1.79
1.80 lemma setsum_Un_disjoint: "finite A ==> finite B
1.81 ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
1.82 @@ -926,7 +935,7 @@
1.83 "finite I ==> (ALL i:I. finite (A i)) ==>
1.84 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.85 setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
1.86 -by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
1.87 +by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong)
1.88
1.89 text{*No need to assume that @{term C} is finite. If infinite, the rhs is
1.90 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
1.91 @@ -945,7 +954,7 @@
1.92 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1.93 (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
1.94 (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
1.95 -by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
1.96 +by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
1.97
1.98 text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.99 lemma setsum_cartesian_product:
1.100 @@ -960,7 +969,7 @@
1.101 done
1.102
1.103 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
1.104 -by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
1.105 +by(simp add:setsum_def AC_add.fold_distrib)
1.106
1.107
1.108 subsubsection {* Properties in more restricted classes of structures *}
1.109 @@ -1241,21 +1250,21 @@
1.110
1.111 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
1.112 setprod f (insert a A) = f a * setprod f A"
1.113 -by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
1.114 +by (simp add: setprod_def)
1.115
1.116 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
1.117 by (simp add: setprod_def)
1.118
1.119 lemma setprod_reindex:
1.120 "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
1.121 -by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
1.122 +by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
1.123
1.124 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
1.125 by (auto simp add: setprod_reindex)
1.126
1.127 lemma setprod_cong:
1.128 "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
1.129 -by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
1.130 +by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
1.131
1.132 lemma setprod_reindex_cong: "inj_on f A ==>
1.133 B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
1.134 @@ -1275,7 +1284,7 @@
1.135
1.136 lemma setprod_Un_Int: "finite A ==> finite B
1.137 ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
1.138 -by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
1.139 +by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
1.140
1.141 lemma setprod_Un_disjoint: "finite A ==> finite B
1.142 ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
1.143 @@ -1285,7 +1294,7 @@
1.144 "finite I ==> (ALL i:I. finite (A i)) ==>
1.145 (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
1.146 setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
1.147 -by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
1.148 +by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
1.149
1.150 lemma setprod_Union_disjoint:
1.151 "[| (ALL A:C. finite A);
1.152 @@ -1300,7 +1309,7 @@
1.153 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
1.154 (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
1.155 (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
1.156 -by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
1.157 +by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
1.158
1.159 text{*Here we can eliminate the finiteness assumptions, by cases.*}
1.160 lemma setprod_cartesian_product:
1.161 @@ -1316,7 +1325,7 @@
1.162
1.163 lemma setprod_timesf:
1.164 "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
1.165 -by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
1.166 +by(simp add:setprod_def AC_mult.fold_distrib)
1.167
1.168
1.169 subsubsection {* Properties in more restricted classes of structures *}
1.170 @@ -1434,7 +1443,7 @@
1.171
1.172 lemma card_insert_disjoint [simp]:
1.173 "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
1.174 -by(simp add: card_def ACf.fold_insert[OF ACf_add])
1.175 +by(simp add: card_def)
1.176
1.177 lemma card_insert_if:
1.178 "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
1.179 @@ -2231,70 +2240,54 @@
1.180 text{* Before we can do anything, we need to show that @{text min} and
1.181 @{text max} are ACI and the ordering is linear: *}
1.182
1.183 -lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.184 +interpretation AC_min [rule del]: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
1.185 apply(rule ACf.intro)
1.186 apply(auto simp:min_def)
1.187 done
1.188
1.189 -lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.190 -apply(rule ACIf.intro[OF ACf_min])
1.191 +interpretation AC_min [rule del]: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
1.192 apply(rule ACIf_axioms.intro)
1.193 apply(auto simp:min_def)
1.194 done
1.195
1.196 -lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.197 +interpretation AC_max [rule del]: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
1.198 apply(rule ACf.intro)
1.199 apply(auto simp:max_def)
1.200 done
1.201
1.202 -lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
1.203 -apply(rule ACIf.intro[OF ACf_max])
1.204 +interpretation AC_max [rule del]: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
1.205 apply(rule ACIf_axioms.intro)
1.206 apply(auto simp:max_def)
1.207 done
1.208
1.209 -lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
1.210 -apply(rule ACIfSL.intro)
1.211 -apply(rule ACf_min)
1.212 -apply(rule ACIf.axioms[OF ACIf_min])
1.213 +interpretation AC_min [rule del]: ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
1.214 apply(rule ACIfSL_axioms.intro)
1.215 apply(auto simp:min_def)
1.216 done
1.217
1.218 -lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
1.219 -apply(rule ACIfSLlin.intro)
1.220 -apply(rule ACf_min)
1.221 -apply(rule ACIf.axioms[OF ACIf_min])
1.222 -apply(rule ACIfSL.axioms[OF ACIfSL_min])
1.223 +interpretation AC_min [rule del]: ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
1.224 apply(rule ACIfSLlin_axioms.intro)
1.225 apply(auto simp:min_def)
1.226 done
1.227
1.228 -lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
1.229 -apply(rule ACIfSL.intro)
1.230 -apply(rule ACf_max)
1.231 -apply(rule ACIf.axioms[OF ACIf_max])
1.232 +interpretation AC_max [rule del]: ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
1.233 apply(rule ACIfSL_axioms.intro)
1.234 apply(auto simp:max_def)
1.235 done
1.236
1.237 -lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
1.238 -apply(rule ACIfSLlin.intro)
1.239 -apply(rule ACf_max)
1.240 -apply(rule ACIf.axioms[OF ACIf_max])
1.241 -apply(rule ACIfSL.axioms[OF ACIfSL_max])
1.242 +interpretation AC_max [rule del]: ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
1.243 apply(rule ACIfSLlin_axioms.intro)
1.244 apply(auto simp:max_def)
1.245 done
1.246
1.247 -lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
1.248 +lemma Lattice_min_max [rule del]: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
1.249 apply(rule Lattice.intro)
1.250 apply(rule partial_order_order)
1.251 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
1.252 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
1.253 done
1.254
1.255 -lemma Distrib_Lattice_min_max:
1.256 +lemma Distrib_Lattice_min_max [rule del]:
1.257 "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
1.258 apply(rule Distrib_Lattice.intro)
1.259 apply(rule partial_order_order)
1.260 @@ -2303,56 +2296,73 @@
1.261 apply(rule distrib_lattice.axioms[OF distrib_lattice_min_max])
1.262 done
1.263
1.264 +interpretation Lattice_min_max [rule del]:
1.265 + Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
1.266 +using Lattice_min_max
1.267 +by (auto dest: Lattice.axioms)
1.268 +
1.269 +interpretation Lattice_min_max [rule del]:
1.270 + Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
1.271 +using Distrib_Lattice_min_max
1.272 +by (fast dest: Distrib_Lattice.axioms)
1.273 +
1.274 +text {* Classical rules from the locales are deleted in the above
1.275 + interpretations, since they interfere with the claset setup for
1.276 + {text "op \<le>"}. *)
1.277 +
1.278 text{* Now we instantiate the recursion equations and declare them
1.279 simplification rules: *}
1.280
1.281 +(* Making Min (resp. Max) a defined parameter of a locale suitably
1.282 + extending ACIf could make the following interpretations more automatic. *)
1.283 +
1.284 declare
1.285 fold1_singleton_def[OF Min_def, simp]
1.286 - ACIf.fold1_insert_idem_def[OF ACIf_min Min_def, simp]
1.287 + AC_min.fold1_insert_idem_def[OF Min_def, simp]
1.288 fold1_singleton_def[OF Max_def, simp]
1.289 - ACIf.fold1_insert_idem_def[OF ACIf_max Max_def, simp]
1.290 + AC_max.fold1_insert_idem_def[OF Max_def, simp]
1.291
1.292 text{* Now we instantiate some @{text fold1} properties: *}
1.293
1.294 lemma Min_in [simp]:
1.295 shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
1.296 -using ACf.fold1_in[OF ACf_min]
1.297 +using AC_min.fold1_in
1.298 by(fastsimp simp: Min_def min_def)
1.299
1.300 lemma Max_in [simp]:
1.301 shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
1.302 -using ACf.fold1_in[OF ACf_max]
1.303 +using AC_max.fold1_in
1.304 by(fastsimp simp: Max_def max_def)
1.305
1.306 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
1.307 -by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
1.308 +by(simp add: Min_def AC_min.fold1_belowI)
1.309
1.310 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
1.311 -by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
1.312 +by(simp add: Max_def AC_max.fold1_belowI)
1.313
1.314 lemma Min_ge_iff[simp]:
1.315 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
1.316 -by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min])
1.317 +by(simp add: Min_def AC_min.below_fold1_iff)
1.318
1.319 lemma Max_le_iff[simp]:
1.320 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
1.321 -by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max])
1.322 +by(simp add: Max_def AC_max.below_fold1_iff)
1.323
1.324 lemma Min_le_iff:
1.325 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
1.326 -by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
1.327 +by(simp add: Min_def AC_min.fold1_below_iff)
1.328
1.329 lemma Max_ge_iff:
1.330 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
1.331 -by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
1.332 +by(simp add: Max_def AC_max.fold1_below_iff)
1.333
1.334 lemma Min_le_Max:
1.335 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
1.336 -by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
1.337 +by(simp add: Min_def Max_def Lattice_min_max.Inf_le_Sup)
1.338
1.339 lemma max_Min2_distrib:
1.340 "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
1.341 max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
1.342 -by(simp add: Min_def Distrib_Lattice.sup_Inf2_distrib[OF Distrib_Lattice_min_max])
1.343 +by(simp add: Min_def Lattice_min_max.sup_Inf2_distrib)
1.344
1.345 end