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.25 -interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
    1.26 +class_interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
    1.27    proof qed (auto intro: add_assoc add_commute)
    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])