# HG changeset patch
# User haftmann
# Date 1206738059 -3600
# Node ID 1f55aef1390374057af9ddc646cff86968ac58fd
# Parent  aedaf65f7a57ceceb302b636cd2b9106a6a9dc2b
only invoke interpret

diff -r aedaf65f7a57 -r 1f55aef13903 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Mar 28 20:08:11 2008 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Mar 28 22:00:59 2008 +0100
@@ -1725,7 +1725,7 @@
 proof (induct rule: finite_induct)
   case empty then show ?case by simp
 next
-  invoke ab_semigroup_mult ["op Un"]
+  interpret ab_semigroup_mult ["op Un"]
     by unfold_locales auto
   case insert 
   then show ?case by simp
@@ -2134,7 +2134,7 @@
   assumes "finite A" "A \<noteq> {}"
   shows "x \<le> fold1 inf A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
 proof -
-  invoke ab_semigroup_idem_mult [inf]
+  interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   show ?thesis using assms by (induct rule: finite_ne_induct) simp_all
 qed
@@ -2146,7 +2146,7 @@
 using assms proof (induct rule: finite_ne_induct)
   case singleton thus ?case by simp
 next
-  invoke ab_semigroup_idem_mult [inf]
+  interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   case (insert x F)
   from insert(5) have "a = x \<or> a \<in> F" by simp
@@ -2220,7 +2220,7 @@
     and "A \<noteq> {}"
   shows "sup x (\<Sqinter>\<^bsub>fin\<^esub>A) = \<Sqinter>\<^bsub>fin\<^esub>{sup x a|a. a \<in> A}"
 proof -
-  invoke ab_semigroup_idem_mult [inf]
+  interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   from assms show ?thesis
     by (simp add: Inf_fin_def image_def
@@ -2235,7 +2235,7 @@
   case singleton thus ?case
     by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
 next
-  invoke ab_semigroup_idem_mult [inf]
+  interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   case (insert x A)
   have finB: "finite {sup x b |b. b \<in> B}"
@@ -2265,7 +2265,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "inf x (\<Squnion>\<^bsub>fin\<^esub>A) = \<Squnion>\<^bsub>fin\<^esub>{inf x a|a. a \<in> A}"
 proof -
-  invoke ab_semigroup_idem_mult [sup]
+  interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   from assms show ?thesis
     by (simp add: Sup_fin_def image_def hom_fold1_commute [where h="inf x", OF inf_sup_distrib1])
@@ -2289,7 +2289,7 @@
     thus ?thesis by(simp add: insert(1) B(1))
   qed
   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
-  invoke ab_semigroup_idem_mult [sup]
+  interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   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)"
     using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
@@ -2318,7 +2318,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Sqinter>\<^bsub>fin\<^esub>A = Inf A"
 proof -
-  invoke ab_semigroup_idem_mult [inf]
+  interpret ab_semigroup_idem_mult [inf]
     by (rule ab_semigroup_idem_mult_inf)
   from assms show ?thesis
   unfolding Inf_fin_def by (induct A set: finite)
@@ -2329,7 +2329,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "\<Squnion>\<^bsub>fin\<^esub>A = Sup A"
 proof -
-  invoke ab_semigroup_idem_mult [sup]
+  interpret ab_semigroup_idem_mult [sup]
     by (rule ab_semigroup_idem_mult_sup)
   from assms show ?thesis
   unfolding Sup_fin_def by (induct A set: finite)
@@ -2378,7 +2378,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x < fold1 min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2389,7 +2389,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "fold1 min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2400,7 +2400,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "fold1 min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
   by (induct rule: finite_ne_induct)
@@ -2413,7 +2413,7 @@
 proof cases
   assume "A = B" thus ?thesis by simp
 next
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   assume "A \<noteq> B"
   have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
@@ -2447,7 +2447,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min (insert x A) = min x (Min A)"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis by (rule fold1_insert_idem_def [OF Min_def])
 qed
@@ -2456,7 +2456,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max (insert x A) = max x (Max A)"
 proof -
-  invoke ab_semigroup_idem_mult [max]
+  interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis by (rule fold1_insert_idem_def [OF Max_def])
 qed
@@ -2465,7 +2465,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<in> A"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms fold1_in show ?thesis by (fastsimp simp: Min_def min_def)
 qed
@@ -2474,7 +2474,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<in> A"
 proof -
-  invoke ab_semigroup_idem_mult [max]
+  interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms fold1_in [of A] show ?thesis by (fastsimp simp: Max_def max_def)
 qed
@@ -2483,7 +2483,7 @@
   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   shows "Min (A \<union> B) = min (Min A) (Min B)"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
     by (simp add: Min_def fold1_Un2)
@@ -2493,7 +2493,7 @@
   assumes "finite A" and "A \<noteq> {}" and "finite B" and "B \<noteq> {}"
   shows "Max (A \<union> B) = max (Max A) (Max B)"
 proof -
-  invoke ab_semigroup_idem_mult [max]
+  interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis
     by (simp add: Max_def fold1_Un2)
@@ -2504,7 +2504,7 @@
     and "finite N" and "N \<noteq> {}"
   shows "h (Min N) = Min (h ` N)"
 proof -
-  invoke ab_semigroup_idem_mult [min]
+  interpret ab_semigroup_idem_mult [min]
     by (rule ab_semigroup_idem_mult_min)
   from assms show ?thesis
     by (simp add: Min_def hom_fold1_commute)
@@ -2515,7 +2515,7 @@
     and "finite N" and "N \<noteq> {}"
   shows "h (Max N) = Max (h ` N)"
 proof -
-  invoke ab_semigroup_idem_mult [max]
+  interpret ab_semigroup_idem_mult [max]
     by (rule ab_semigroup_idem_mult_max)
   from assms show ?thesis
     by (simp add: Max_def hom_fold1_commute [of h])
@@ -2525,7 +2525,7 @@
   assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
   shows "Min A \<le> x"
 proof -
-  invoke lower_semilattice [_ _ min]
+  interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def fold1_belowI)
 qed
@@ -2534,7 +2534,7 @@
   assumes "finite A" and "A \<noteq> {}" and "x \<in> A"
   shows "x \<le> Max A"
 proof -
-  invoke lower_semilattice [_ _ max]
+  invoke lower_semilattice ["op \<ge>" "op >" max]
     by (rule max_lattice)
   from assms show ?thesis by (simp add: Max_def fold1_belowI)
 qed
@@ -2543,7 +2543,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
 proof -
-  invoke lower_semilattice [_ _ min]
+  interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def below_fold1_iff)
 qed
@@ -2552,7 +2552,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
 proof -
-  invoke lower_semilattice [_ _ max]
+  invoke lower_semilattice ["op \<ge>" "op >" max]
     by (rule max_lattice)
   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
 qed
@@ -2561,7 +2561,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
 proof -
-  invoke lower_semilattice [_ _ min]
+  interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis by (simp add: Min_def strict_below_fold1_iff)
 qed
@@ -2571,7 +2571,7 @@
   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
 proof -
   note Max = Max_def
-  invoke linorder ["op \<ge>" "op >"]
+  interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max strict_below_fold1_iff [folded dual_max])
@@ -2581,7 +2581,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
 proof -
-  invoke lower_semilattice [_ _ min]
+  interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis
     by (simp add: Min_def fold1_below_iff)
@@ -2592,7 +2592,7 @@
   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
 proof -
   note Max = Max_def
-  invoke linorder ["op \<ge>" "op >"]
+  interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_below_iff [folded dual_max])
@@ -2602,7 +2602,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
 proof -
-  invoke lower_semilattice [_ _ min]
+  interpret lower_semilattice ["op \<le>" "op <" min]
     by (rule min_lattice)
   from assms show ?thesis
     by (simp add: Min_def fold1_strict_below_iff)
@@ -2613,7 +2613,7 @@
   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
 proof -
   note Max = Max_def
-  invoke linorder ["op \<ge>" "op >"]
+  interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_strict_below_iff [folded dual_max])
@@ -2623,7 +2623,7 @@
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Min N \<le> Min M"
 proof -
-  invoke distrib_lattice ["op \<le>" "op <" min max]
+  interpret distrib_lattice ["op \<le>" "op <" min max]
     by (rule distrib_lattice_min_max)
   from assms show ?thesis by (simp add: Min_def fold1_antimono)
 qed
@@ -2633,7 +2633,7 @@
   shows "Max M \<le> Max N"
 proof -
   note Max = Max_def
-  invoke linorder ["op \<ge>" "op >"]
+  interpret linorder ["op \<ge>" "op >"]
     by (rule dual_linorder)
   from assms show ?thesis
     by (simp add: Max fold1_antimono [folded dual_max])