# HG changeset patch
# User ballarin
# Date 1113832431 -7200
# Node ID 6472d4942992297a68de4a9d376b3b05b2d549b5
# Parent  250df939a1de0f9bc9dd2219a5bfec2e04776a1d
Cleaned up, now uses interpretation.

diff -r 250df939a1de -r 6472d4942992 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Apr 18 10:36:05 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Apr 18 15:53:51 2005 +0200
@@ -509,21 +509,30 @@
 
 lemmas (in ACIf) ACI = AC idem idem2
 
-text{* Instantiation of locales: *}
+text{* Interpretation of locales: *}
+
+interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
+by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
 
+interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
+  apply -
+   apply (fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
+  apply (fastsimp intro: ACe_axioms.intro mult_assoc ab_semigroup_mult.mult_commute)
+  done
+
+(*
 lemma ACf_add: "ACf (op + :: 'a::comm_monoid_add \<Rightarrow> 'a \<Rightarrow> 'a)"
 by(fastsimp intro: ACf.intro add_assoc add_commute)
 
 lemma ACe_add: "ACe (op +) (0::'a::comm_monoid_add)"
 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_add)
 
-
 lemma ACf_mult: "ACf (op * :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> 'a)"
 by(fast intro: ACf.intro mult_assoc ab_semigroup_mult.mult_commute)
 
-lemma ACe_mult: "ACe (op *) (1::'a::comm_monoid_mult)"
+lemma ACe_mult: "ACe (op * ) (1::'a::comm_monoid_mult)"
 by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
-
+*)
 
 subsubsection{*From @{term foldSet} to @{term fold}*}
 
@@ -878,14 +887,14 @@
 
 lemma setsum_insert [simp]:
     "finite F ==> a \<notin> F ==> setsum f (insert a F) = f a + setsum f F"
-  by (simp add: setsum_def ACf.fold_insert [OF ACf_add])
+  by (simp add: setsum_def)
 
 lemma setsum_infinite [simp]: "~ finite A ==> setsum f A = 0"
   by (simp add: setsum_def)
 
 lemma setsum_reindex:
      "inj_on f B ==> setsum h (f ` B) = setsum (h \<circ> f) B"
-by(auto simp add: setsum_def ACf.fold_reindex[OF ACf_add] dest!:finite_imageD)
+by(auto simp add: setsum_def AC_add.fold_reindex dest!:finite_imageD)
 
 lemma setsum_reindex_id:
      "inj_on f B ==> setsum f B = setsum id (f ` B)"
@@ -893,7 +902,7 @@
 
 lemma setsum_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setsum f A = setsum g B"
-by(fastsimp simp: setsum_def intro: ACf.fold_cong[OF ACf_add])
+by(fastsimp simp: setsum_def intro: AC_add.fold_cong)
 
 lemma setsum_cong2: "\<lbrakk>\<And>x. x \<in> A \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> setsum f A = setsum g A";
   by (rule setsum_cong[OF refl], auto);
@@ -905,7 +914,7 @@
 
 lemma setsum_0[simp]: "setsum (%i. 0) A = 0"
 apply (clarsimp simp: setsum_def)
-apply (erule finite_induct, auto simp:ACf.fold_insert [OF ACf_add])
+apply (erule finite_induct, auto)
 done
 
 lemma setsum_0': "ALL a:A. f a = 0 ==> setsum f A = 0"
@@ -914,7 +923,7 @@
 lemma setsum_Un_Int: "finite A ==> finite B ==>
   setsum g (A Un B) + setsum g (A Int B) = setsum g A + setsum g B"
   -- {* The reversed orientation looks more natural, but LOOPS as a simprule! *}
-by(simp add: setsum_def ACe.fold_Un_Int[OF ACe_add,symmetric])
+by(simp add: setsum_def AC_add.fold_Un_Int [symmetric])
 
 lemma setsum_Un_disjoint: "finite A ==> finite B
   ==> A Int B = {} ==> setsum g (A Un B) = setsum g A + setsum g B"
@@ -926,7 +935,7 @@
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
-by(simp add: setsum_def ACe.fold_UN_disjoint[OF ACe_add] cong: setsum_cong)
+by(simp add: setsum_def AC_add.fold_UN_disjoint cong: setsum_cong)
 
 text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
 directly 0, and @{term "Union C"} is also infinite, hence the lhs is also 0.*}
@@ -945,7 +954,7 @@
 lemma setsum_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) =
     (\<Sum>z\<in>(SIGMA x:A. B x). f (fst z) (snd z))"
-by(simp add:setsum_def ACe.fold_Sigma[OF ACe_add] split_def cong:setsum_cong)
+by(simp add:setsum_def AC_add.fold_Sigma split_def cong:setsum_cong)
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setsum_cartesian_product: 
@@ -960,7 +969,7 @@
 done
 
 lemma setsum_addf: "setsum (%x. f x + g x) A = (setsum f A + setsum g A)"
-by(simp add:setsum_def ACe.fold_distrib[OF ACe_add])
+by(simp add:setsum_def AC_add.fold_distrib)
 
 
 subsubsection {* Properties in more restricted classes of structures *}
@@ -1241,21 +1250,21 @@
 
 lemma setprod_insert [simp]: "[| finite A; a \<notin> A |] ==>
     setprod f (insert a A) = f a * setprod f A"
-by (simp add: setprod_def ACf.fold_insert [OF ACf_mult])
+by (simp add: setprod_def)
 
 lemma setprod_infinite [simp]: "~ finite A ==> setprod f A = 1"
   by (simp add: setprod_def)
 
 lemma setprod_reindex:
      "inj_on f B ==> setprod h (f ` B) = setprod (h \<circ> f) B"
-by(auto simp: setprod_def ACf.fold_reindex[OF ACf_mult] dest!:finite_imageD)
+by(auto simp: setprod_def AC_mult.fold_reindex dest!:finite_imageD)
 
 lemma setprod_reindex_id: "inj_on f B ==> setprod f B = setprod id (f ` B)"
 by (auto simp add: setprod_reindex)
 
 lemma setprod_cong:
   "A = B ==> (!!x. x:B ==> f x = g x) ==> setprod f A = setprod g B"
-by(fastsimp simp: setprod_def intro: ACf.fold_cong[OF ACf_mult])
+by(fastsimp simp: setprod_def intro: AC_mult.fold_cong)
 
 lemma setprod_reindex_cong: "inj_on f A ==>
     B = f ` A ==> g = h \<circ> f ==> setprod h B = setprod g A"
@@ -1275,7 +1284,7 @@
 
 lemma setprod_Un_Int: "finite A ==> finite B
     ==> setprod g (A Un B) * setprod g (A Int B) = setprod g A * setprod g B"
-by(simp add: setprod_def ACe.fold_Un_Int[OF ACe_mult,symmetric])
+by(simp add: setprod_def AC_mult.fold_Un_Int[symmetric])
 
 lemma setprod_Un_disjoint: "finite A ==> finite B
   ==> A Int B = {} ==> setprod g (A Un B) = setprod g A * setprod g B"
@@ -1285,7 +1294,7 @@
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
-by(simp add: setprod_def ACe.fold_UN_disjoint[OF ACe_mult] cong: setprod_cong)
+by(simp add: setprod_def AC_mult.fold_UN_disjoint cong: setprod_cong)
 
 lemma setprod_Union_disjoint:
   "[| (ALL A:C. finite A);
@@ -1300,7 +1309,7 @@
 lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
     (\<Prod>x:A. (\<Prod>y: B x. f x y)) =
     (\<Prod>z:(SIGMA x:A. B x). f (fst z) (snd z))"
-by(simp add:setprod_def ACe.fold_Sigma[OF ACe_mult] split_def cong:setprod_cong)
+by(simp add:setprod_def AC_mult.fold_Sigma split_def cong:setprod_cong)
 
 text{*Here we can eliminate the finiteness assumptions, by cases.*}
 lemma setprod_cartesian_product: 
@@ -1316,7 +1325,7 @@
 
 lemma setprod_timesf:
      "setprod (%x. f x * g x) A = (setprod f A * setprod g A)"
-by(simp add:setprod_def ACe.fold_distrib[OF ACe_mult])
+by(simp add:setprod_def AC_mult.fold_distrib)
 
 
 subsubsection {* Properties in more restricted classes of structures *}
@@ -1434,7 +1443,7 @@
 
 lemma card_insert_disjoint [simp]:
   "finite A ==> x \<notin> A ==> card (insert x A) = Suc(card A)"
-by(simp add: card_def ACf.fold_insert[OF ACf_add])
+by(simp add: card_def)
 
 lemma card_insert_if:
     "finite A ==> card (insert x A) = (if x:A then card A else Suc(card(A)))"
@@ -2231,70 +2240,54 @@
 text{* Before we can do anything, we need to show that @{text min} and
 @{text max} are ACI and the ordering is linear: *}
 
-lemma ACf_min: "ACf(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
+interpretation AC_min [rule del]: ACf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACf.intro)
 apply(auto simp:min_def)
 done
 
-lemma ACIf_min: "ACIf(min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
-apply(rule ACIf.intro[OF ACf_min])
+interpretation AC_min [rule del]: ACIf ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACIf_axioms.intro)
 apply(auto simp:min_def)
 done
 
-lemma ACf_max: "ACf(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
+interpretation AC_max [rule del]: ACf ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACf.intro)
 apply(auto simp:max_def)
 done
 
-lemma ACIf_max: "ACIf(max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
-apply(rule ACIf.intro[OF ACf_max])
+interpretation AC_max [rule del]: ACIf ["max:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
 apply(rule ACIf_axioms.intro)
 apply(auto simp:max_def)
 done
 
-lemma ACIfSL_min: "ACIfSL(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
-apply(rule ACIfSL.intro)
-apply(rule ACf_min)
-apply(rule ACIf.axioms[OF ACIf_min])
+interpretation AC_min [rule del]: ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
 apply(rule ACIfSL_axioms.intro)
 apply(auto simp:min_def)
 done
 
-lemma ACIfSLlin_min: "ACIfSLlin(min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (op \<le>)"
-apply(rule ACIfSLlin.intro)
-apply(rule ACf_min)
-apply(rule ACIf.axioms[OF ACIf_min])
-apply(rule ACIfSL.axioms[OF ACIfSL_min])
+interpretation AC_min [rule del]: ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
 apply(rule ACIfSLlin_axioms.intro)
 apply(auto simp:min_def)
 done
 
-lemma ACIfSL_max: "ACIfSL(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
-apply(rule ACIfSL.intro)
-apply(rule ACf_max)
-apply(rule ACIf.axioms[OF ACIf_max])
+interpretation AC_max [rule del]: ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
 apply(rule ACIfSL_axioms.intro)
 apply(auto simp:max_def)
 done
 
-lemma ACIfSLlin_max: "ACIfSLlin(max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) (%x y. y\<le>x)"
-apply(rule ACIfSLlin.intro)
-apply(rule ACf_max)
-apply(rule ACIf.axioms[OF ACIf_max])
-apply(rule ACIfSL.axioms[OF ACIfSL_max])
+interpretation AC_max [rule del]: ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
 apply(rule ACIfSLlin_axioms.intro)
 apply(auto simp:max_def)
 done
 
-lemma Lattice_min_max: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
+lemma Lattice_min_max [rule del]: "Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
 apply(rule Lattice.intro)
 apply(rule partial_order_order)
 apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
 apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
 done
 
-lemma Distrib_Lattice_min_max:
+lemma Distrib_Lattice_min_max [rule del]:
  "Distrib_Lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
 apply(rule Distrib_Lattice.intro)
 apply(rule partial_order_order)
@@ -2303,56 +2296,73 @@
 apply(rule distrib_lattice.axioms[OF distrib_lattice_min_max])
 done
 
+interpretation Lattice_min_max [rule del]:
+  Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
+using Lattice_min_max
+by (auto dest: Lattice.axioms)
+
+interpretation Lattice_min_max [rule del]:
+  Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
+using Distrib_Lattice_min_max
+by (fast dest: Distrib_Lattice.axioms)
+
+text {* Classical rules from the locales are deleted in the above
+  interpretations, since they interfere with the claset setup for
+  {text "op \<le>"}. *)
+
 text{* Now we instantiate the recursion equations and declare them
 simplification rules: *}
 
+(* Making Min (resp. Max) a defined parameter of a locale suitably
+  extending ACIf could make the following interpretations more automatic. *)
+
 declare
   fold1_singleton_def[OF Min_def, simp]
-  ACIf.fold1_insert_idem_def[OF ACIf_min Min_def, simp]
+  AC_min.fold1_insert_idem_def[OF Min_def, simp]
   fold1_singleton_def[OF Max_def, simp]
-  ACIf.fold1_insert_idem_def[OF ACIf_max Max_def, simp]
+  AC_max.fold1_insert_idem_def[OF Max_def, simp]
 
 text{* Now we instantiate some @{text fold1} properties: *}
 
 lemma Min_in [simp]:
   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Min A \<in> A"
-using ACf.fold1_in[OF ACf_min]
+using AC_min.fold1_in
 by(fastsimp simp: Min_def min_def)
 
 lemma Max_in [simp]:
   shows "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> Max A \<in> A"
-using ACf.fold1_in[OF ACf_max]
+using AC_max.fold1_in
 by(fastsimp simp: Max_def max_def)
 
 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> x"
-by(simp add: Min_def ACIfSL.fold1_belowI[OF ACIfSL_min])
+by(simp add: Min_def AC_min.fold1_belowI)
 
 lemma Max_ge [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> x \<le> Max A"
-by(simp add: Max_def ACIfSL.fold1_belowI[OF ACIfSL_max])
+by(simp add: Max_def AC_max.fold1_belowI)
 
 lemma Min_ge_iff[simp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Min A) = (\<forall>a\<in>A. x \<le> a)"
-by(simp add: Min_def ACIfSL.below_fold1_iff[OF ACIfSL_min])
+by(simp add: Min_def AC_min.below_fold1_iff)
 
 lemma Max_le_iff[simp]:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Max A \<le> x) = (\<forall>a\<in>A. a \<le> x)"
-by(simp add: Max_def ACIfSL.below_fold1_iff[OF ACIfSL_max])
+by(simp add: Max_def AC_max.below_fold1_iff)
 
 lemma Min_le_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (Min A \<le> x) = (\<exists>a\<in>A. a \<le> x)"
-by(simp add: Min_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_min])
+by(simp add: Min_def AC_min.fold1_below_iff)
 
 lemma Max_ge_iff:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
-by(simp add: Max_def ACIfSLlin.fold1_below_iff[OF ACIfSLlin_max])
+by(simp add: Max_def AC_max.fold1_below_iff)
 
 lemma Min_le_Max:
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A \<le> Max A"
-by(simp add: Min_def Max_def Lattice.Inf_le_Sup[OF Lattice_min_max])
+by(simp add: Min_def Max_def Lattice_min_max.Inf_le_Sup)
 
 lemma max_Min2_distrib:
   "\<lbrakk> finite A; A \<noteq> {}; finite B; B \<noteq> {} \<rbrakk> \<Longrightarrow>
   max (Min A) (Min B) = Min{ max a b |a b. a \<in> A \<and> b \<in> B}"
-by(simp add: Min_def Distrib_Lattice.sup_Inf2_distrib[OF Distrib_Lattice_min_max])
+by(simp add: Min_def Lattice_min_max.sup_Inf2_distrib)
 
 end