Added Mi and Max on sets, hid Min and Pls on numerals.

--- a/src/HOL/Finite_Set.thy	Fri Aug 09 11:22:18 2002 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Aug 12 17:48:15 2002 +0200
@@ -116,7 +116,7 @@
   apply blast
   done
 
-lemma finite_imageI: "finite F ==> finite (h ` F)"
+lemma finite_imageI[simp]: "finite F ==> finite (h ` F)"
   -- {* The image of a finite set is finite. *}
   by (induct set: Finites) simp_all
 
@@ -882,6 +882,87 @@
   apply (simp add: Ball_def)
   done
 
+subsubsection{* Min and Max of finite linearly ordered sets *}
+
+text{* Seemed easier to define directly than via fold. *}
+
+lemma ex_Max: fixes S :: "('a::linorder)set"
+  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. s \<le> m"
+using fin
+proof (induct)
+  case empty thus ?case by simp
+next
+  case (insert S x)
+  show ?case
+  proof (cases)
+    assume "S = {}" thus ?thesis by simp
+  next
+    assume nonempty: "S \<noteq> {}"
+    then obtain m where m: "m\<in>S" "\<forall>s\<in>S. s \<le> m" using insert by blast
+    show ?thesis
+    proof (cases)
+      assume "x \<le> m" thus ?thesis using m by blast
+    next
+      assume "\<not> x \<le> m" thus ?thesis using m
+	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
+    qed
+  qed
+qed
+
+lemma ex_Min: fixes S :: "('a::linorder)set"
+  assumes fin: "finite S" shows "S \<noteq> {} \<Longrightarrow> \<exists>m\<in>S. \<forall>s \<in> S. m \<le> s"
+using fin
+proof (induct)
+  case empty thus ?case by simp
+next
+  case (insert S x)
+  show ?case
+  proof (cases)
+    assume "S = {}" thus ?thesis by simp
+  next
+    assume nonempty: "S \<noteq> {}"
+    then obtain m where m: "m\<in>S" "\<forall>s\<in>S. m \<le> s" using insert by blast
+    show ?thesis
+    proof (cases)
+      assume "m \<le> x" thus ?thesis using m by blast
+    next
+      assume "\<not> m \<le> x" thus ?thesis using m
+	by(simp add:linorder_not_le order_less_le)(blast intro: order_trans)
+    qed
+  qed
+qed
+
+constdefs
+ Min :: "('a::linorder)set \<Rightarrow> 'a"
+"Min S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. m \<le> s)"
+
+ Max :: "('a::linorder)set \<Rightarrow> 'a"
+"Max S  \<equiv>  THE m. m \<in> S \<and> (\<forall>s \<in> S. s \<le> m)"
+
+lemma Min[simp]: assumes a: "finite S" "S \<noteq> {}"
+                 shows "Min S \<in> S \<and> (\<forall>s \<in> S. Min S \<le> s)" (is "?P(Min S)")
+proof (unfold Min_def, rule theI')
+  show "\<exists>!m. ?P m"
+  proof (rule ex_ex1I)
+    show "\<exists>m. ?P m" using ex_Min[OF a] by blast
+  next
+    fix m1 m2 assume "?P m1" "?P m2"
+    thus "m1 = m2" by (blast dest:order_antisym)
+  qed
+qed
+
+lemma Max[simp]: assumes a: "finite S" "S \<noteq> {}"
+                 shows "Max S \<in> S \<and> (\<forall>s \<in> S. s \<le> Max S)" (is "?P(Max S)")
+proof (unfold Max_def, rule theI')
+  show "\<exists>!m. ?P m"
+  proof (rule ex_ex1I)
+    show "\<exists>m. ?P m" using ex_Max[OF a] by blast
+  next
+    fix m1 m2 assume "?P m1" "?P m2"
+    thus "m1 = m2" by (blast dest:order_antisym)
+  qed
+qed
+
 
 text {*
   \medskip Basic theorem about @{text "choose"}.  By Florian

--- a/src/HOL/Numeral.thy	Fri Aug 09 11:22:18 2002 +0200
+++ b/src/HOL/Numeral.thy	Mon Aug 12 17:48:15 2002 +0200
@@ -8,6 +8,11 @@
 theory Numeral = Datatype
 files "Tools/numeral_syntax.ML":
 
+(* The constructors Pls/Min are hidden in numeral_syntax.ML.
+   Only qualified access bin.Pls/Min is allowed.
+   Should also hide Bit, but that means one cannot use BIT anymore.
+*)
+
 datatype
   bin = Pls
       | Min
@@ -25,8 +30,8 @@
   Numeral1 :: 'a
 
 translations
-  "Numeral0" == "number_of Pls"
-  "Numeral1" == "number_of (Pls BIT True)"
+  "Numeral0" == "number_of bin.Pls"
+  "Numeral1" == "number_of (bin.Pls BIT True)"
 
 
 setup NumeralSyntax.setup