# HG changeset patch
# User nipkow
# Date 1114010358 -7200
# Node ID 6744bba5561d5c5739aeb32edea2de59406de0aa
# Parent  aed221aff64299e14c1a3817f9b9662a5ed4ee77
Used locale interpretations everywhere.

diff -r aed221aff642 -r 6744bba5561d src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Apr 20 16:03:17 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 20 17:19:18 2005 +0200
@@ -516,23 +516,10 @@
 
 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)
+   apply (fast intro: ACf.intro mult_assoc mult_commute)
+  apply (fastsimp intro: ACe_axioms.intro mult_assoc 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)"
-by(fastsimp intro: ACe.intro ACe_axioms.intro ACf_mult)
-*)
 
 subsubsection{*From @{term foldSet} to @{term fold}*}
 
@@ -2149,7 +2136,7 @@
 
 subsubsection{* Fold laws in lattices *}
 
-lemma (in Lattice) Inf_le_Sup: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
+lemma (in Lattice) Inf_le_Sup[simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Squnion>A"
 apply(unfold Sup_def Inf_def)
 apply(subgoal_tac "EX a. a:A")
 prefer 2 apply blast
@@ -2159,13 +2146,13 @@
 apply(erule (2) ACIfSL.fold1_belowI[OF ACIfSL_sup])
 done
 
-lemma (in Lattice) sup_Inf_absorb:
+lemma (in Lattice) sup_Inf_absorb[simp]:
   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<squnion> \<Sqinter>A) = a"
 apply(subst sup_commute)
 apply(simp add:Inf_def sup_absorb ACIfSL.fold1_belowI[OF ACIfSL_inf])
 done
 
-lemma (in Lattice) inf_Sup_absorb:
+lemma (in Lattice) inf_Sup_absorb[simp]:
   "\<lbrakk> finite A; A \<noteq> {}; a \<in> A \<rbrakk> \<Longrightarrow> (a \<sqinter> \<Squnion>A) = a"
 by(simp add:Sup_def inf_absorb ACIfSL.fold1_belowI[OF ACIfSL_sup])
 
@@ -2260,51 +2247,41 @@
 apply(auto simp:max_def)
 done
 
-interpretation AC_min [rule del]: ACIfSL ["min:: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
+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
 
-interpretation AC_min [rule del]: ACIfSLlin ["min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "op \<le>"]
+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
 
-interpretation AC_max [rule del]: ACIfSL ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
+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
 
-interpretation AC_max [rule del]: ACIfSLlin ["max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "%x y. y\<le>x"]
+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 [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])
+interpretation min_max [rule del]:
+  Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
+apply -
+apply(rule Min_def)
+apply(rule Max_def)
 done
 
-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)
-apply(rule lower_semilattice.axioms[OF lower_semilattice_lin_min])
-apply(rule upper_semilattice.axioms[OF upper_semilattice_lin_max])
-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)
+interpretation min_max [rule del]:
+  Distrib_Lattice ["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max" "Min" "Max"]
+.
 
 text {* Classical rules from the locales are deleted in the above
   interpretations, since they interfere with the claset setup for
@@ -2356,13 +2333,4 @@
   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> (x \<le> Max A) = (\<exists>a\<in>A. x \<le> a)"
 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_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 Lattice_min_max.sup_Inf2_distrib)
-
 end
diff -r aed221aff642 -r 6744bba5561d src/HOL/Orderings.ML
--- a/src/HOL/Orderings.ML	Wed Apr 20 16:03:17 2005 +0200
+++ b/src/HOL/Orderings.ML	Wed Apr 20 17:19:18 2005 +0200
@@ -39,9 +39,7 @@
 val le_maxI1 = thm "le_maxI1";
 val le_maxI2 = thm "le_maxI2";
 val less_max_iff_disj = thm "less_max_iff_disj";
-val max_le_iff_conj = thm "max_le_iff_conj";
 val max_less_iff_conj = thm "max_less_iff_conj";
-val le_min_iff_conj = thm "le_min_iff_conj";
 val min_less_iff_conj = thm "min_less_iff_conj";
 val min_le_iff_disj = thm "min_le_iff_disj";
 val min_less_iff_disj = thm "min_less_iff_disj";
diff -r aed221aff642 -r 6744bba5561d src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Apr 20 16:03:17 2005 +0200
+++ b/src/HOL/Orderings.thy	Wed Apr 20 17:19:18 2005 +0200
@@ -93,8 +93,8 @@
 
 text{* Connection to locale: *}
 
-lemma partial_order_order:
- "partial_order (op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool)"
+interpretation order[rule del]:
+  partial_order["op \<le> :: 'a::order \<Rightarrow> 'a \<Rightarrow> bool"]
 apply(rule partial_order.intro)
 apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
 done
@@ -226,6 +226,16 @@
 axclass linorder < order
   linorder_linear: "x <= y | y <= x"
 
+(* Could (should?) follow automatically from the interpretation of
+   partial_order by class order. rule del is needed because two copies
+   of refl with classes order and linorder confuse blast (and are pointless)*)
+interpretation order[rule del]:
+  partial_order["op \<le> :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> bool"]
+apply(rule partial_order.intro)
+apply(rule order_refl, erule (1) order_trans, erule (1) order_antisym)
+done
+
+
 lemma linorder_less_linear: "!!x::'a::linorder. x<y | x=y | y<x"
   apply (simp add: order_less_le)
   apply (insert linorder_linear, blast)
@@ -388,39 +398,30 @@
 
 text{* Instantiate locales: *}
 
-lemma lower_semilattice_lin_min:
-  "lower_semilattice(op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
-apply(rule lower_semilattice.intro)
-apply(rule partial_order_order)
+interpretation min_max [rule del]:
+  lower_semilattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+apply -
 apply(rule lower_semilattice_axioms.intro)
 apply(simp add:min_def linorder_not_le order_less_imp_le)
 apply(simp add:min_def linorder_not_le order_less_imp_le)
 apply(simp add:min_def linorder_not_le order_less_imp_le)
 done
 
-lemma upper_semilattice_lin_max:
-  "upper_semilattice(op \<le>) (max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a)"
-apply(rule upper_semilattice.intro)
-apply(rule partial_order_order)
+interpretation min_max [rule del]:
+  upper_semilattice["op \<le>" "max :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a"]
+apply -
 apply(rule upper_semilattice_axioms.intro)
 apply(simp add: max_def linorder_not_le order_less_imp_le)
 apply(simp add: max_def linorder_not_le order_less_imp_le)
 apply(simp add: max_def linorder_not_le order_less_imp_le)
 done
 
-lemma lattice_min_max: "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
+interpretation min_max [rule del]:
+  lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
+.
 
-lemma distrib_lattice_min_max:
- "distrib_lattice (op \<le>) (min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a) max"
-apply(rule distrib_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])
+interpretation min_max [rule del]:
+  distrib_lattice["op \<le>" "min :: 'a::linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
 apply(rule distrib_lattice_axioms.intro)
 apply(rule_tac x=x and y=y in linorder_le_cases)
 apply(rule_tac x=x and y=z in linorder_le_cases)
@@ -445,12 +446,8 @@
   apply (blast intro: order_trans)
   done
 
-lemma le_maxI1: "(x::'a::linorder) <= max x y"
-by(rule upper_semilattice.sup_ge1[OF upper_semilattice_lin_max])
-
-lemma le_maxI2: "(y::'a::linorder) <= max x y"
-    -- {* CANNOT use with @{text "[intro!]"} because blast will give PROOF FAILED. *}
-by(rule upper_semilattice.sup_ge2[OF upper_semilattice_lin_max])
+lemmas le_maxI1 = min_max.sup_ge1
+lemmas le_maxI2 = min_max.sup_ge2
 
 lemma less_max_iff_disj: "!!z::'a::linorder. (z < max x y) = (z < x | z < y)"
   apply (simp add: max_def order_le_less)
@@ -458,22 +455,18 @@
   apply (blast intro: order_less_trans)
   done
 
-lemma max_le_iff_conj [simp]:
-    "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)"
-by (rule upper_semilattice.above_sup_conv[OF upper_semilattice_lin_max])
-
 lemma max_less_iff_conj [simp]:
     "!!z::'a::linorder. (max x y < z) = (x < z & y < z)"
   apply (simp add: order_le_less max_def)
   apply (insert linorder_less_linear)
   apply (blast intro: order_less_trans)
   done
-
+(*
 lemma le_min_iff_conj [simp]:
     "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)"
     -- {* @{text "[iff]"} screws up a @{text blast} in MiniML *}
 by (rule lower_semilattice.below_inf_conv[OF lower_semilattice_lin_min])
-
+*)
 lemma min_less_iff_conj [simp]:
     "!!z::'a::linorder. (z < min x y) = (z < x & z < y)"
   apply (simp add: order_le_less min_def)
@@ -492,24 +485,24 @@
   apply (insert linorder_less_linear)
   apply (blast intro: order_less_trans)
   done
-
+(*
 lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
 by (rule upper_semilattice.sup_assoc[OF upper_semilattice_lin_max])
 
 lemma max_commute: "!!x::'a::linorder. max x y = max y x"
 by (rule upper_semilattice.sup_commute[OF upper_semilattice_lin_max])
-
-lemmas max_ac = max_assoc max_commute
-                mk_left_commute[of max,OF max_assoc max_commute]
-
+*)
+lemmas max_ac = min_max.sup_assoc min_max.sup_commute
+               mk_left_commute[of max,OF min_max.sup_assoc min_max.sup_commute]
+(*
 lemma min_assoc: "!!x::'a::linorder. min (min x y) z = min x (min y z)"
 by (rule lower_semilattice.inf_assoc[OF lower_semilattice_lin_min])
 
 lemma min_commute: "!!x::'a::linorder. min x y = min y x"
 by (rule lower_semilattice.inf_commute[OF lower_semilattice_lin_min])
-
-lemmas min_ac = min_assoc min_commute
-                mk_left_commute[of min,OF min_assoc min_commute]
+*)
+lemmas min_ac = min_max.inf_assoc min_max.inf_commute
+               mk_left_commute[of min,OF min_max.inf_assoc min_max.inf_commute]
 
 lemma split_min:
     "P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"