src/HOL/Finite_Set.thy
 changeset 29223 e09c53289830 parent 29025 8c8859c0d734 child 29509 1ff0f3f08a7b
```     1.1 --- a/src/HOL/Finite_Set.thy	Wed Dec 10 17:19:25 2008 +0100
1.2 +++ b/src/HOL/Finite_Set.thy	Thu Dec 11 18:30:26 2008 +0100
1.3 @@ -750,7 +750,7 @@
1.4  assumes "finite A" and "a \<notin> A"
1.5  shows "fold_image times g z (insert a A) = g a * (fold_image times g z A)"
1.6  proof -
1.7 -  interpret I: fun_left_comm ["%x y. (g x) * y"]
1.8 +  interpret I: fun_left_comm "%x y. (g x) * y"
1.9      by unfold_locales (simp add: mult_ac)
1.10    show ?thesis using assms by(simp add:fold_image_def I.fold_insert)
1.11  qed
1.12 @@ -798,7 +798,7 @@
1.13      and hyp: "\<And>x y. h (g x y) = times x (h y)"
1.14    shows "h (fold g j w A) = fold times j (h w) A"
1.15  proof -
1.16 -  interpret ab_semigroup_mult [g] by fact
1.17 +  class_interpret ab_semigroup_mult [g] by fact
1.18    show ?thesis using fin hyp by (induct set: finite) simp_all
1.19  qed
1.20  *)
1.21 @@ -873,7 +873,7 @@
1.22
1.23  subsection {* Generalized summation over a set *}
1.24
1.28
1.29  definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
1.30 @@ -1760,7 +1760,7 @@
1.31  proof (induct rule: finite_induct)
1.32    case empty then show ?case by simp
1.33  next
1.34 -  interpret ab_semigroup_mult ["op Un"]
1.35 +  class_interpret ab_semigroup_mult ["op Un"]
1.36      proof qed auto
1.37    case insert
1.38    then show ?case by simp
1.39 @@ -1943,7 +1943,7 @@
1.40  assumes fold: "fold_graph times (b::'a) A y" and "b \<notin> A"
1.41  shows "fold_graph times z (insert b A) (z * y)"
1.42  proof -
1.43 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
1.44 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
1.45  from assms show ?thesis
1.46  proof (induct rule: fold_graph.induct)
1.47    case emptyI thus ?case by (force simp add: fold_insert_aux mult_commute)
1.48 @@ -1983,7 +1983,7 @@
1.49  lemma fold1_eq_fold:
1.50  assumes "finite A" "a \<notin> A" shows "fold1 times (insert a A) = fold times a A"
1.51  proof -
1.52 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
1.53 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
1.54    from assms show ?thesis
1.55  apply (simp add: fold1_def fold_def)
1.56  apply (rule the_equality)
1.57 @@ -2010,7 +2010,7 @@
1.58    assumes nonempty: "A \<noteq> {}" and A: "finite A" "x \<notin> A"
1.59    shows "fold1 times (insert x A) = x * fold1 times A"
1.60  proof -
1.61 -  interpret fun_left_comm ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"] by (rule fun_left_comm)
1.62 +  interpret fun_left_comm "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a" by (rule fun_left_comm)
1.63    from nonempty obtain a A' where "A = insert a A' & a ~: A'"
1.64      by (auto simp add: nonempty_iff)
1.65    with A show ?thesis
1.66 @@ -2033,7 +2033,7 @@
1.67    assumes nonempty: "A \<noteq> {}" and A: "finite A"
1.68    shows "fold1 times (insert x A) = x * fold1 times A"
1.69  proof -
1.70 -  interpret fun_left_comm_idem ["op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"]
1.71 +  interpret fun_left_comm_idem "op *::'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.72      by (rule fun_left_comm_idem)
1.73    from nonempty obtain a A' where A': "A = insert a A' & a ~: A'"
1.74      by (auto simp add: nonempty_iff)
1.75 @@ -2198,7 +2198,7 @@
1.76    assumes "finite A" "A \<noteq> {}"
1.77    shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
1.78  proof -
1.79 -  interpret ab_semigroup_idem_mult [inf]
1.80 +  class_interpret ab_semigroup_idem_mult [inf]
1.81      by (rule ab_semigroup_idem_mult_inf)
1.82    show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
1.83  qed
1.84 @@ -2213,7 +2213,7 @@
1.85    proof (induct rule: finite_ne_induct)
1.86      case singleton thus ?case by simp
1.87    next
1.88 -    interpret ab_semigroup_idem_mult [inf]
1.89 +    class_interpret ab_semigroup_idem_mult [inf]
1.90        by (rule ab_semigroup_idem_mult_inf)
1.91      case (insert x F)
1.92      from insert(5) have "a = x \<or> a \<in> F" by simp
1.93 @@ -2288,7 +2288,7 @@
1.94      and "A \<noteq> {}"
1.95    shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
1.96  proof -
1.97 -  interpret ab_semigroup_idem_mult [inf]
1.98 +  class_interpret ab_semigroup_idem_mult [inf]
1.99      by (rule ab_semigroup_idem_mult_inf)
1.100    from assms show ?thesis
1.101      by (simp add: Inf_fin_def image_def
1.102 @@ -2303,7 +2303,7 @@
1.103    case singleton thus ?case
1.104      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
1.105  next
1.106 -  interpret ab_semigroup_idem_mult [inf]
1.107 +  class_interpret ab_semigroup_idem_mult [inf]
1.108      by (rule ab_semigroup_idem_mult_inf)
1.109    case (insert x A)
1.110    have finB: "finite {sup x b |b. b \<in> B}"
1.111 @@ -2333,7 +2333,7 @@
1.112    assumes "finite A" and "A \<noteq> {}"
1.113    shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
1.114  proof -
1.115 -  interpret ab_semigroup_idem_mult [sup]
1.116 +  class_interpret ab_semigroup_idem_mult [sup]
1.117      by (rule ab_semigroup_idem_mult_sup)
1.118    from assms show ?thesis
1.119      by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
1.120 @@ -2357,7 +2357,7 @@
1.121      thus ?thesis by(simp add: insert(1) B(1))
1.122    qed
1.123    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
1.124 -  interpret ab_semigroup_idem_mult [sup]
1.125 +  class_interpret ab_semigroup_idem_mult [sup]
1.126      by (rule ab_semigroup_idem_mult_sup)
1.127    have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
1.128      using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
1.129 @@ -2386,7 +2386,7 @@
1.130    assumes "finite A" and "A \<noteq> {}"
1.131    shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
1.132  proof -
1.133 -  interpret ab_semigroup_idem_mult [inf]
1.134 +  class_interpret ab_semigroup_idem_mult [inf]
1.135      by (rule ab_semigroup_idem_mult_inf)
1.136    from assms show ?thesis
1.137    unfolding Inf_fin_def by (induct A set: finite)
1.138 @@ -2397,7 +2397,7 @@
1.139    assumes "finite A" and "A \<noteq> {}"
1.140    shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
1.141  proof -
1.142 -  interpret ab_semigroup_idem_mult [sup]
1.143 +  class_interpret ab_semigroup_idem_mult [sup]
1.144      by (rule ab_semigroup_idem_mult_sup)
1.145    from assms show ?thesis
1.146    unfolding Sup_fin_def by (induct A set: finite)
1.147 @@ -2446,7 +2446,7 @@
1.148    assumes "finite A" and "A \<noteq> {}"
1.149    shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
1.150  proof -
1.151 -  interpret ab_semigroup_idem_mult [min]
1.152 +  class_interpret ab_semigroup_idem_mult [min]
1.153      by (rule ab_semigroup_idem_mult_min)
1.154    from assms show ?thesis
1.155    by (induct rule: finite_ne_induct)
1.156 @@ -2457,7 +2457,7 @@
1.157    assumes "finite A" and "A \<noteq> {}"
1.158    shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
1.159  proof -
1.160 -  interpret ab_semigroup_idem_mult [min]
1.161 +  class_interpret ab_semigroup_idem_mult [min]
1.162      by (rule ab_semigroup_idem_mult_min)
1.163    from assms show ?thesis
1.164    by (induct rule: finite_ne_induct)
1.165 @@ -2468,7 +2468,7 @@
1.166    assumes "finite A" and "A \<noteq> {}"
1.167    shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
1.168  proof -
1.169 -  interpret ab_semigroup_idem_mult [min]
1.170 +  class_interpret ab_semigroup_idem_mult [min]
1.171      by (rule ab_semigroup_idem_mult_min)
1.172    from assms show ?thesis
1.173    by (induct rule: finite_ne_induct)
1.174 @@ -2481,7 +2481,7 @@
1.175  proof cases
1.176    assume "A = B" thus ?thesis by simp
1.177  next
1.178 -  interpret ab_semigroup_idem_mult [min]
1.179 +  class_interpret ab_semigroup_idem_mult [min]
1.180      by (rule ab_semigroup_idem_mult_min)
1.181    assume "A \<noteq> B"
1.182    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
1.183 @@ -2515,7 +2515,7 @@
1.184    assumes "finite A" and "A \<noteq> {}"
1.185    shows "Min (insert x A) = min x (Min A)"
1.186  proof -
1.187 -  interpret ab_semigroup_idem_mult [min]
1.188 +  class_interpret ab_semigroup_idem_mult [min]
1.189      by (rule ab_semigroup_idem_mult_min)
1.190    from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
1.191  qed
1.192 @@ -2524,7 +2524,7 @@
1.193    assumes "finite A" and "A \<noteq> {}"
1.194    shows "Max (insert x A) = max x (Max A)"
1.195  proof -
1.196 -  interpret ab_semigroup_idem_mult [max]
1.197 +  class_interpret ab_semigroup_idem_mult [max]
1.198      by (rule ab_semigroup_idem_mult_max)
1.199    from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
1.200  qed
1.201 @@ -2533,7 +2533,7 @@
1.202    assumes "finite A" and "A \<noteq> {}"
1.203    shows "Min A \<in> A"
1.204  proof -
1.205 -  interpret ab_semigroup_idem_mult [min]
1.206 +  class_interpret ab_semigroup_idem_mult [min]
1.207      by (rule ab_semigroup_idem_mult_min)
1.208    from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
1.209  qed
1.210 @@ -2542,7 +2542,7 @@
1.211    assumes "finite A" and "A \<noteq> {}"
1.212    shows "Max A \<in> A"
1.213  proof -
1.214 -  interpret ab_semigroup_idem_mult [max]
1.215 +  class_interpret ab_semigroup_idem_mult [max]
1.216      by (rule ab_semigroup_idem_mult_max)
1.217    from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
1.218  qed
1.219 @@ -2551,7 +2551,7 @@
1.220    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
1.221    shows "Min (A \<union> B) = min (Min A) (Min B)"
1.222  proof -
1.223 -  interpret ab_semigroup_idem_mult [min]
1.224 +  class_interpret ab_semigroup_idem_mult [min]
1.225      by (rule ab_semigroup_idem_mult_min)
1.226    from assms show ?thesis
1.227      by (simp add: Min_def fold1_Un2)
1.228 @@ -2561,7 +2561,7 @@
1.229    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
1.230    shows "Max (A \<union> B) = max (Max A) (Max B)"
1.231  proof -
1.232 -  interpret ab_semigroup_idem_mult [max]
1.233 +  class_interpret ab_semigroup_idem_mult [max]
1.234      by (rule ab_semigroup_idem_mult_max)
1.235    from assms show ?thesis
1.236      by (simp add: Max_def fold1_Un2)
1.237 @@ -2572,7 +2572,7 @@
1.238      and "finite N" and "N \<noteq> {}"
1.239    shows "h (Min N) = Min (h ` N)"
1.240  proof -
1.241 -  interpret ab_semigroup_idem_mult [min]
1.242 +  class_interpret ab_semigroup_idem_mult [min]
1.243      by (rule ab_semigroup_idem_mult_min)
1.244    from assms show ?thesis
1.245      by (simp add: Min_def hom_fold1_commute)
1.246 @@ -2583,7 +2583,7 @@
1.247      and "finite N" and "N \<noteq> {}"
1.248    shows "h (Max N) = Max (h ` N)"
1.249  proof -
1.250 -  interpret ab_semigroup_idem_mult [max]
1.251 +  class_interpret ab_semigroup_idem_mult [max]
1.252      by (rule ab_semigroup_idem_mult_max)
1.253    from assms show ?thesis
1.254      by (simp add: Max_def hom_fold1_commute [of h])
1.255 @@ -2593,7 +2593,7 @@
1.256    assumes "finite A" and "x \<in> A"
1.257    shows "Min A \<le> x"
1.258  proof -
1.259 -  interpret lower_semilattice ["op \<le>" "op <" min]
1.260 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
1.261      by (rule min_lattice)
1.262    from assms show ?thesis by (simp add: Min_def fold1_belowI)
1.263  qed
1.264 @@ -2611,7 +2611,7 @@
1.265    assumes "finite A" and "A \<noteq> {}"
1.266    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
1.267  proof -
1.268 -  interpret lower_semilattice ["op \<le>" "op <" min]
1.269 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
1.270      by (rule min_lattice)
1.271    from assms show ?thesis by (simp add: Min_def below_fold1_iff)
1.272  qed
1.273 @@ -2629,7 +2629,7 @@
1.274    assumes "finite A" and "A \<noteq> {}"
1.275    shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
1.276  proof -
1.277 -  interpret lower_semilattice ["op \<le>" "op <" min]
1.278 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
1.279      by (rule min_lattice)
1.280    from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
1.281  qed
1.282 @@ -2639,7 +2639,7 @@
1.283    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
1.284  proof -
1.285    note Max = Max_def
1.286 -  interpret linorder ["op \<ge>" "op >"]
1.287 +  class_interpret linorder ["op \<ge>" "op >"]
1.288      by (rule dual_linorder)
1.289    from assms show ?thesis
1.290      by (simp add: Max strict_below_fold1_iff [folded dual_max])
1.291 @@ -2649,7 +2649,7 @@
1.292    assumes "finite A" and "A \<noteq> {}"
1.293    shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
1.294  proof -
1.295 -  interpret lower_semilattice ["op \<le>" "op <" min]
1.296 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
1.297      by (rule min_lattice)
1.298    from assms show ?thesis
1.299      by (simp add: Min_def fold1_below_iff)
1.300 @@ -2660,7 +2660,7 @@
1.301    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
1.302  proof -
1.303    note Max = Max_def
1.304 -  interpret linorder ["op \<ge>" "op >"]
1.305 +  class_interpret linorder ["op \<ge>" "op >"]
1.306      by (rule dual_linorder)
1.307    from assms show ?thesis
1.308      by (simp add: Max fold1_below_iff [folded dual_max])
1.309 @@ -2670,7 +2670,7 @@
1.310    assumes "finite A" and "A \<noteq> {}"
1.311    shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
1.312  proof -
1.313 -  interpret lower_semilattice ["op \<le>" "op <" min]
1.314 +  class_interpret lower_semilattice ["op \<le>" "op <" min]
1.315      by (rule min_lattice)
1.316    from assms show ?thesis
1.317      by (simp add: Min_def fold1_strict_below_iff)
1.318 @@ -2681,7 +2681,7 @@
1.319    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
1.320  proof -
1.321    note Max = Max_def
1.322 -  interpret linorder ["op \<ge>" "op >"]
1.323 +  class_interpret linorder ["op \<ge>" "op >"]
1.324      by (rule dual_linorder)
1.325    from assms show ?thesis
1.326      by (simp add: Max fold1_strict_below_iff [folded dual_max])
1.327 @@ -2691,7 +2691,7 @@
1.328    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
1.329    shows "Min N \<le> Min M"
1.330  proof -
1.331 -  interpret distrib_lattice ["op \<le>" "op <" min max]
1.332 +  class_interpret distrib_lattice ["op \<le>" "op <" min max]
1.333      by (rule distrib_lattice_min_max)
1.334    from assms show ?thesis by (simp add: Min_def fold1_antimono)
1.335  qed
1.336 @@ -2701,7 +2701,7 @@
1.337    shows "Max M \<le> Max N"
1.338  proof -
1.339    note Max = Max_def
1.340 -  interpret linorder ["op \<ge>" "op >"]
1.341 +  class_interpret linorder ["op \<ge>" "op >"]
1.342      by (rule dual_linorder)
1.343    from assms show ?thesis
1.344      by (simp add: Max fold1_antimono [folded dual_max])
```