only invoke interpret
authorhaftmann
Fri Mar 28 22:00:59 2008 +0100 (2008-03-28)
changeset 264651f55aef13903
parent 26464 aedaf65f7a57
child 26466 5d6b3a808131
only invoke interpret
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Mar 28 20:08:11 2008 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri Mar 28 22:00:59 2008 +0100
     1.3 @@ -1725,7 +1725,7 @@
     1.4  proof (induct rule: finite_induct)
     1.5    case empty then show ?case by simp
     1.6  next
     1.7 -  invoke ab_semigroup_mult ["op Un"]
     1.8 +  interpret ab_semigroup_mult ["op Un"]
     1.9      by unfold_locales auto
    1.10    case insert 
    1.11    then show ?case by simp
    1.12 @@ -2134,7 +2134,7 @@
    1.13    assumes "finite A" "A \<noteq> {}"
    1.14    shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
    1.15  proof -
    1.16 -  invoke ab_semigroup_idem_mult [inf]
    1.17 +  interpret ab_semigroup_idem_mult [inf]
    1.18      by (rule ab_semigroup_idem_mult_inf)
    1.19    show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
    1.20  qed
    1.21 @@ -2146,7 +2146,7 @@
    1.22  using assms proof (induct rule: finite_ne_induct)
    1.23    case singleton thus ?case by simp
    1.24  next
    1.25 -  invoke ab_semigroup_idem_mult [inf]
    1.26 +  interpret ab_semigroup_idem_mult [inf]
    1.27      by (rule ab_semigroup_idem_mult_inf)
    1.28    case (insert x F)
    1.29    from insert(5) have "a = x \<or> a \<in> F" by simp
    1.30 @@ -2220,7 +2220,7 @@
    1.31      and "A \<noteq> {}"
    1.32    shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
    1.33  proof -
    1.34 -  invoke ab_semigroup_idem_mult [inf]
    1.35 +  interpret ab_semigroup_idem_mult [inf]
    1.36      by (rule ab_semigroup_idem_mult_inf)
    1.37    from assms show ?thesis
    1.38      by (simp add: Inf_fin_def image_def
    1.39 @@ -2235,7 +2235,7 @@
    1.40    case singleton thus ?case
    1.41      by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
    1.42  next
    1.43 -  invoke ab_semigroup_idem_mult [inf]
    1.44 +  interpret ab_semigroup_idem_mult [inf]
    1.45      by (rule ab_semigroup_idem_mult_inf)
    1.46    case (insert x A)
    1.47    have finB: "finite {sup x b |b. b \<in> B}"
    1.48 @@ -2265,7 +2265,7 @@
    1.49    assumes "finite A" and "A \<noteq> {}"
    1.50    shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
    1.51  proof -
    1.52 -  invoke ab_semigroup_idem_mult [sup]
    1.53 +  interpret ab_semigroup_idem_mult [sup]
    1.54      by (rule ab_semigroup_idem_mult_sup)
    1.55    from assms show ?thesis
    1.56      by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
    1.57 @@ -2289,7 +2289,7 @@
    1.58      thus ?thesis by(simp add: insert(1) B(1))
    1.59    qed
    1.60    have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
    1.61 -  invoke ab_semigroup_idem_mult [sup]
    1.62 +  interpret ab_semigroup_idem_mult [sup]
    1.63      by (rule ab_semigroup_idem_mult_sup)
    1.64    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.65      using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
    1.66 @@ -2318,7 +2318,7 @@
    1.67    assumes "finite A" and "A \<noteq> {}"
    1.68    shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
    1.69  proof -
    1.70 -  invoke ab_semigroup_idem_mult [inf]
    1.71 +  interpret ab_semigroup_idem_mult [inf]
    1.72      by (rule ab_semigroup_idem_mult_inf)
    1.73    from assms show ?thesis
    1.74    unfolding Inf_fin_def by (induct A set: finite)
    1.75 @@ -2329,7 +2329,7 @@
    1.76    assumes "finite A" and "A \<noteq> {}"
    1.77    shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
    1.78  proof -
    1.79 -  invoke ab_semigroup_idem_mult [sup]
    1.80 +  interpret ab_semigroup_idem_mult [sup]
    1.81      by (rule ab_semigroup_idem_mult_sup)
    1.82    from assms show ?thesis
    1.83    unfolding Sup_fin_def by (induct A set: finite)
    1.84 @@ -2378,7 +2378,7 @@
    1.85    assumes "finite A" and "A \<noteq> {}"
    1.86    shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
    1.87  proof -
    1.88 -  invoke ab_semigroup_idem_mult [min]
    1.89 +  interpret ab_semigroup_idem_mult [min]
    1.90      by (rule ab_semigroup_idem_mult_min)
    1.91    from assms show ?thesis
    1.92    by (induct rule: finite_ne_induct)
    1.93 @@ -2389,7 +2389,7 @@
    1.94    assumes "finite A" and "A \<noteq> {}"
    1.95    shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
    1.96  proof -
    1.97 -  invoke ab_semigroup_idem_mult [min]
    1.98 +  interpret ab_semigroup_idem_mult [min]
    1.99      by (rule ab_semigroup_idem_mult_min)
   1.100    from assms show ?thesis
   1.101    by (induct rule: finite_ne_induct)
   1.102 @@ -2400,7 +2400,7 @@
   1.103    assumes "finite A" and "A \<noteq> {}"
   1.104    shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   1.105  proof -
   1.106 -  invoke ab_semigroup_idem_mult [min]
   1.107 +  interpret ab_semigroup_idem_mult [min]
   1.108      by (rule ab_semigroup_idem_mult_min)
   1.109    from assms show ?thesis
   1.110    by (induct rule: finite_ne_induct)
   1.111 @@ -2413,7 +2413,7 @@
   1.112  proof cases
   1.113    assume "A = B" thus ?thesis by simp
   1.114  next
   1.115 -  invoke ab_semigroup_idem_mult [min]
   1.116 +  interpret ab_semigroup_idem_mult [min]
   1.117      by (rule ab_semigroup_idem_mult_min)
   1.118    assume "A \<noteq> B"
   1.119    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   1.120 @@ -2447,7 +2447,7 @@
   1.121    assumes "finite A" and "A \<noteq> {}"
   1.122    shows "Min (insert x A) = min x (Min A)"
   1.123  proof -
   1.124 -  invoke ab_semigroup_idem_mult [min]
   1.125 +  interpret ab_semigroup_idem_mult [min]
   1.126      by (rule ab_semigroup_idem_mult_min)
   1.127    from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
   1.128  qed
   1.129 @@ -2456,7 +2456,7 @@
   1.130    assumes "finite A" and "A \<noteq> {}"
   1.131    shows "Max (insert x A) = max x (Max A)"
   1.132  proof -
   1.133 -  invoke ab_semigroup_idem_mult [max]
   1.134 +  interpret ab_semigroup_idem_mult [max]
   1.135      by (rule ab_semigroup_idem_mult_max)
   1.136    from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
   1.137  qed
   1.138 @@ -2465,7 +2465,7 @@
   1.139    assumes "finite A" and "A \<noteq> {}"
   1.140    shows "Min A \<in> A"
   1.141  proof -
   1.142 -  invoke ab_semigroup_idem_mult [min]
   1.143 +  interpret ab_semigroup_idem_mult [min]
   1.144      by (rule ab_semigroup_idem_mult_min)
   1.145    from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
   1.146  qed
   1.147 @@ -2474,7 +2474,7 @@
   1.148    assumes "finite A" and "A \<noteq> {}"
   1.149    shows "Max A \<in> A"
   1.150  proof -
   1.151 -  invoke ab_semigroup_idem_mult [max]
   1.152 +  interpret ab_semigroup_idem_mult [max]
   1.153      by (rule ab_semigroup_idem_mult_max)
   1.154    from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
   1.155  qed
   1.156 @@ -2483,7 +2483,7 @@
   1.157    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   1.158    shows "Min (A \<union> B) = min (Min A) (Min B)"
   1.159  proof -
   1.160 -  invoke ab_semigroup_idem_mult [min]
   1.161 +  interpret ab_semigroup_idem_mult [min]
   1.162      by (rule ab_semigroup_idem_mult_min)
   1.163    from assms show ?thesis
   1.164      by (simp add: Min_def fold1_Un2)
   1.165 @@ -2493,7 +2493,7 @@
   1.166    assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   1.167    shows "Max (A \<union> B) = max (Max A) (Max B)"
   1.168  proof -
   1.169 -  invoke ab_semigroup_idem_mult [max]
   1.170 +  interpret ab_semigroup_idem_mult [max]
   1.171      by (rule ab_semigroup_idem_mult_max)
   1.172    from assms show ?thesis
   1.173      by (simp add: Max_def fold1_Un2)
   1.174 @@ -2504,7 +2504,7 @@
   1.175      and "finite N" and "N \<noteq> {}"
   1.176    shows "h (Min N) = Min (h ` N)"
   1.177  proof -
   1.178 -  invoke ab_semigroup_idem_mult [min]
   1.179 +  interpret ab_semigroup_idem_mult [min]
   1.180      by (rule ab_semigroup_idem_mult_min)
   1.181    from assms show ?thesis
   1.182      by (simp add: Min_def hom_fold1_commute)
   1.183 @@ -2515,7 +2515,7 @@
   1.184      and "finite N" and "N \<noteq> {}"
   1.185    shows "h (Max N) = Max (h ` N)"
   1.186  proof -
   1.187 -  invoke ab_semigroup_idem_mult [max]
   1.188 +  interpret ab_semigroup_idem_mult [max]
   1.189      by (rule ab_semigroup_idem_mult_max)
   1.190    from assms show ?thesis
   1.191      by (simp add: Max_def hom_fold1_commute [of h])
   1.192 @@ -2525,7 +2525,7 @@
   1.193    assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
   1.194    shows "Min A \<le> x"
   1.195  proof -
   1.196 -  invoke lower_semilattice [_ _ min]
   1.197 +  interpret lower_semilattice ["op \<le>" "op <" min]
   1.198      by (rule min_lattice)
   1.199    from assms show ?thesis by (simp add: Min_def fold1_belowI)
   1.200  qed
   1.201 @@ -2534,7 +2534,7 @@
   1.202    assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
   1.203    shows "x \<le> Max A"
   1.204  proof -
   1.205 -  invoke lower_semilattice [_ _ max]
   1.206 +  invoke lower_semilattice ["op \<ge>" "op >" max]
   1.207      by (rule max_lattice)
   1.208    from assms show ?thesis by (simp add: Max_def fold1_belowI)
   1.209  qed
   1.210 @@ -2543,7 +2543,7 @@
   1.211    assumes "finite A" and "A \<noteq> {}"
   1.212    shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   1.213  proof -
   1.214 -  invoke lower_semilattice [_ _ min]
   1.215 +  interpret lower_semilattice ["op \<le>" "op <" min]
   1.216      by (rule min_lattice)
   1.217    from assms show ?thesis by (simp add: Min_def below_fold1_iff)
   1.218  qed
   1.219 @@ -2552,7 +2552,7 @@
   1.220    assumes "finite A" and "A \<noteq> {}"
   1.221    shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   1.222  proof -
   1.223 -  invoke lower_semilattice [_ _ max]
   1.224 +  invoke lower_semilattice ["op \<ge>" "op >" max]
   1.225      by (rule max_lattice)
   1.226    from assms show ?thesis by (simp add: Max_def below_fold1_iff)
   1.227  qed
   1.228 @@ -2561,7 +2561,7 @@
   1.229    assumes "finite A" and "A \<noteq> {}"
   1.230    shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   1.231  proof -
   1.232 -  invoke lower_semilattice [_ _ min]
   1.233 +  interpret lower_semilattice ["op \<le>" "op <" min]
   1.234      by (rule min_lattice)
   1.235    from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
   1.236  qed
   1.237 @@ -2571,7 +2571,7 @@
   1.238    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   1.239  proof -
   1.240    note Max = Max_def
   1.241 -  invoke linorder ["op \<ge>" "op >"]
   1.242 +  interpret linorder ["op \<ge>" "op >"]
   1.243      by (rule dual_linorder)
   1.244    from assms show ?thesis
   1.245      by (simp add: Max strict_below_fold1_iff [folded dual_max])
   1.246 @@ -2581,7 +2581,7 @@
   1.247    assumes "finite A" and "A \<noteq> {}"
   1.248    shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   1.249  proof -
   1.250 -  invoke lower_semilattice [_ _ min]
   1.251 +  interpret lower_semilattice ["op \<le>" "op <" min]
   1.252      by (rule min_lattice)
   1.253    from assms show ?thesis
   1.254      by (simp add: Min_def fold1_below_iff)
   1.255 @@ -2592,7 +2592,7 @@
   1.256    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   1.257  proof -
   1.258    note Max = Max_def
   1.259 -  invoke linorder ["op \<ge>" "op >"]
   1.260 +  interpret linorder ["op \<ge>" "op >"]
   1.261      by (rule dual_linorder)
   1.262    from assms show ?thesis
   1.263      by (simp add: Max fold1_below_iff [folded dual_max])
   1.264 @@ -2602,7 +2602,7 @@
   1.265    assumes "finite A" and "A \<noteq> {}"
   1.266    shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   1.267  proof -
   1.268 -  invoke lower_semilattice [_ _ min]
   1.269 +  interpret lower_semilattice ["op \<le>" "op <" min]
   1.270      by (rule min_lattice)
   1.271    from assms show ?thesis
   1.272      by (simp add: Min_def fold1_strict_below_iff)
   1.273 @@ -2613,7 +2613,7 @@
   1.274    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   1.275  proof -
   1.276    note Max = Max_def
   1.277 -  invoke linorder ["op \<ge>" "op >"]
   1.278 +  interpret linorder ["op \<ge>" "op >"]
   1.279      by (rule dual_linorder)
   1.280    from assms show ?thesis
   1.281      by (simp add: Max fold1_strict_below_iff [folded dual_max])
   1.282 @@ -2623,7 +2623,7 @@
   1.283    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   1.284    shows "Min N \<le> Min M"
   1.285  proof -
   1.286 -  invoke distrib_lattice ["op \<le>" "op <" min max]
   1.287 +  interpret distrib_lattice ["op \<le>" "op <" min max]
   1.288      by (rule distrib_lattice_min_max)
   1.289    from assms show ?thesis by (simp add: Min_def fold1_antimono)
   1.290  qed
   1.291 @@ -2633,7 +2633,7 @@
   1.292    shows "Max M \<le> Max N"
   1.293  proof -
   1.294    note Max = Max_def
   1.295 -  invoke linorder ["op \<ge>" "op >"]
   1.296 +  interpret linorder ["op \<ge>" "op >"]
   1.297      by (rule dual_linorder)
   1.298    from assms show ?thesis
   1.299      by (simp add: Max fold1_antimono [folded dual_max])