# HG changeset patch
# User paulson
# Date 992069044 -7200
# Node ID 7b2dbfb5cc3d772dcbe0f8158b20b480c74ed6a2
# Parent  b42287eb20cfbe39a904c4c074237ac49d8d8043
addition of the GREATEST quantifier

diff -r b42287eb20cf -r 7b2dbfb5cc3d src/HOL/NatArith.ML
--- a/src/HOL/NatArith.ML	Sat Jun 09 08:43:38 2001 +0200
+++ b/src/HOL/NatArith.ML	Sat Jun 09 08:44:04 2001 +0200
@@ -133,3 +133,56 @@
 Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
 	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
 
+
+
+(** GREATEST theorems for type "nat": not dual to LEAST, since there is
+    no greatest natural number.  [The LEAST proofs are in Nat.ML, but the
+    GREATEST proofs require more infrastructure.] **)
+
+Goal "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|] \
+\     ==> EX y. P y & ~ (m y < m k + n)";
+by (induct_tac "n" 1);
+by (Force_tac 1); 
+(*ind step*)
+by (force_tac (claset(), simpset() addsimps [le_Suc_eq]) 1); 
+qed "ex_has_greatest_nat_lemma";
+
+Goal "[|P k;  ! y. P y --> m y < b|] \
+\     ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)";
+by (rtac ccontr 1); 
+by (cut_inst_tac [("P","P"),("n","b - m k")] ex_has_greatest_nat_lemma 1);
+by (subgoal_tac "m k <= b" 3);
+by Auto_tac;  
+qed "ex_has_greatest_nat";
+
+Goalw [GreatestM_def]
+     "[|P k;  ! y. P y --> m y < b|] \
+\     ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))";
+by (rtac someI_ex 1);
+by (etac ex_has_greatest_nat 1);
+by (assume_tac 1); 
+qed "GreatestM_nat_lemma";
+
+bind_thm ("GreatestM_natI", GreatestM_nat_lemma RS conjunct1);
+
+Goal "[|P x;  ! y. P y --> m y < b|] \
+\     ==> (m x::nat) <= m (GreatestM m P)";
+by (blast_tac (claset() addDs [GreatestM_nat_lemma RS conjunct2 RS spec]) 1);
+qed "GreatestM_nat_le";
+
+(** Specialization to GREATEST **)
+
+Goalw [Greatest_def]
+     "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)";
+by (rtac GreatestM_natI 1); 
+by Auto_tac;  
+qed "GreatestI";
+
+Goalw [Greatest_def]
+     "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)";
+by (rtac GreatestM_nat_le 1); 
+by Auto_tac;  
+qed "GreatestM_nat_le";
+
+(*No analogue of not_less_Least or Least_Suc yet, since it isn't used much*)
+
diff -r b42287eb20cf -r 7b2dbfb5cc3d src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Sat Jun 09 08:43:38 2001 +0200
+++ b/src/HOL/Ord.thy	Sat Jun 09 08:44:04 2001 +0200
@@ -75,6 +75,9 @@
 apply (simp add: max_def)
 done
 
+
+(** Least value operator **)
+
 constdefs
   LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
               "LeastM m P == @x. P x & (!y. P y --> m x <= m y)"
@@ -96,6 +99,34 @@
 done
 
 
+(** Greatest value operator **)
+
+constdefs
+  GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
+              "GreatestM m P == @x. P x & (!y. P y --> m y <= m x)"
+  
+  Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
+              "Greatest     == GreatestM (%x. x)"
+
+syntax
+ "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
+                                        ("GREATEST _ WRT _. _" [0,4,10]10)
+
+translations
+              "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
+
+lemma GreatestMI2:
+     "[| P x;
+	 !!y. P y ==> m y <= m x;
+         !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
+      ==> Q (GreatestM m P)";
+apply (unfold GreatestM_def)
+apply (rule someI2_ex)
+apply  blast
+apply blast
+done
+
+
 section "Orders"
 
 axclass order < ord
@@ -201,6 +232,22 @@
 apply blast
 done
 
+lemma GreatestM_equality:
+ "[| P k;  !!x. P x ==> m x <= m k |]
+  ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
+apply (rule_tac m=m in GreatestMI2)
+apply   assumption
+apply  blast
+apply (blast intro!: order_antisym) 
+done
+
+lemma Greatest_equality:
+  "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
+apply (unfold Greatest_def)
+apply (erule GreatestM_equality)
+apply blast
+done
+
 
 section "Linear/Total Orders"
 
@@ -367,6 +414,11 @@
 val LeastM_equality = thm "LeastM_equality";
 val Least_def = thm "Least_def";
 val Least_equality = thm "Least_equality";
+val GreatestM_def = thm "GreatestM_def";
+val GreatestMI2 = thm "GreatestMI2";
+val GreatestM_equality = thm "GreatestM_equality";
+val Greatest_def = thm "Greatest_def";
+val Greatest_equality = thm "Greatest_equality";
 val min_leastR = thm "min_leastR";
 val max_leastR = thm "max_leastR";
 val order_eq_refl = thm "order_eq_refl";