# HG changeset patch
# User nipkow
# Date 1496131415 -7200
# Node ID ca1e636fa7169b8586f89ca125ea53993a100a46
# Parent  d7bc93a467bdf16124444bf4622749999799ebe8
redefined Greatest

diff -r d7bc93a467bd -r ca1e636fa716 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Mon May 29 22:49:52 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue May 30 10:03:35 2017 +0200
@@ -1061,15 +1061,15 @@
     define m where "m = (GREATEST k. k\<le>n \<and> a k \<noteq> 0)"
     have m: "m\<le>n \<and> a m \<noteq> 0"
       unfolding m_def
-      apply (rule GreatestI [where b = "Suc n"])
+      apply (rule GreatestI [where b = n])
       using k apply auto
       done
     have [simp]: "a i = 0" if "m < i" "i \<le> n" for i
-      using Greatest_le [where b = "Suc n" and P = "\<lambda>k. k\<le>n \<and> a k \<noteq> 0"]
+      using Greatest_le [where b = "n" and P = "\<lambda>k. k\<le>n \<and> a k \<noteq> 0"]
       using m_def not_le that by auto
     have "k \<le> m"
       unfolding m_def
-      apply (rule Greatest_le [where b = "Suc n"])
+      apply (rule Greatest_le [where b = "n"])
       using k apply auto
       done
     with k m show ?thesis
diff -r d7bc93a467bd -r ca1e636fa716 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon May 29 22:49:52 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Tue May 30 10:03:35 2017 +0200
@@ -323,8 +323,8 @@
     define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
     assume "\<not>[:c:] dvd b"
     hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
-    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i < Suc (degree b)"
-      by (auto intro: le_degree simp: less_Suc_eq_le)
+    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b"
+      by (auto intro: le_degree)
     have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex[OF A B])
     have "i \<le> m" if "\<not>c dvd coeff b i" for i
       unfolding m_def by (rule Greatest_le[OF that B])
diff -r d7bc93a467bd -r ca1e636fa716 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Mon May 29 22:49:52 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Tue May 30 10:03:35 2017 +0200
@@ -985,7 +985,7 @@
   for f :: "'a \<Rightarrow> nat"
 by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
 
-
+(*
 text \<open>\<^medskip> Specialization to \<open>GREATEST\<close>.\<close>
 
 (* LEAST ? *)
@@ -1012,5 +1012,5 @@
 apply (erule exE)
 apply (erule (1) GreatestI)
 done
-
+*)
 end
diff -r d7bc93a467bd -r ca1e636fa716 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon May 29 22:49:52 2017 +0200
+++ b/src/HOL/Nat.thy	Tue May 30 10:03:35 2017 +0200
@@ -2144,6 +2144,42 @@
 qed
 
 
+subsubsection \<open>Greatest operator\<close>
+
+lemma ex_has_greatest_nat:
+  "P (k::nat) \<Longrightarrow> \<forall>y. P y \<longrightarrow> y \<le> b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y \<le> x)"
+proof (induction "b-k" arbitrary: b k rule: less_induct)
+  case less
+  show ?case
+  proof cases
+    assume "\<exists>n>k. P n"
+    then obtain n where "n>k" "P n" by blast
+    have "n \<le> b" using \<open>P n\<close> less.prems(2) by auto
+    hence "b-n < b-k"
+      by(rule diff_less_mono2[OF \<open>k<n\<close> less_le_trans[OF \<open>k<n\<close>]])
+    from less.hyps[OF this \<open>P n\<close> less.prems(2)]
+    show ?thesis .
+  next
+    assume "\<not> (\<exists>n>k. P n)"
+    hence "\<forall>y. P y \<longrightarrow> y \<le> k" by (auto simp: not_less)
+    thus ?thesis using less.prems(1) by auto
+  qed
+qed
+
+lemma GreatestI: "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
+apply(drule (1) ex_has_greatest_nat)
+using GreatestI2_order by auto
+
+lemma Greatest_le: "\<lbrakk> P(k::nat);  \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> k \<le> (Greatest P)"
+apply(frule (1) ex_has_greatest_nat)
+using GreatestI2_order[where P=P and Q=\<open>\<lambda>x. k \<le> x\<close>] by auto
+
+lemma GreatestI_ex: "\<lbrakk> \<exists>k::nat. P k;  \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
+apply (erule exE)
+apply (erule (1) GreatestI)
+done
+
+
 subsection \<open>Monotonicity of \<open>funpow\<close>\<close>
 
 lemma funpow_increasing: "m \<le> n \<Longrightarrow> mono f \<Longrightarrow> (f ^^ n) \<top> \<le> (f ^^ m) \<top>"
diff -r d7bc93a467bd -r ca1e636fa716 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon May 29 22:49:52 2017 +0200
+++ b/src/HOL/Orderings.thy	Tue May 30 10:03:35 2017 +0200
@@ -301,6 +301,24 @@
 unfolding Least_def by (rule theI2)
   (blast intro: assms antisym)+
 
+text \<open>Greatest value operator\<close>
+
+definition Greatest :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREATEST " 10) where
+"Greatest P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<ge> y))"
+
+lemma GreatestI2_order:
+  "\<lbrakk> P x;
+    \<And>y. P y \<Longrightarrow> x \<ge> y;
+    \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> x \<ge> y \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
+  \<Longrightarrow> Q (Greatest P)"
+unfolding Greatest_def
+by (rule theI2) (blast intro: antisym)+
+
+lemma Greatest_equality:
+  "\<lbrakk> P x;  \<And>y. P y \<Longrightarrow> x \<ge> y \<rbrakk> \<Longrightarrow> Greatest P = x"
+unfolding Greatest_def
+by (rule the_equality) (blast intro: antisym)+
+
 end
 
 lemma ordering_orderI: