# HG changeset patch
# User nipkow
# Date 1496145888 -7200
# Node ID 088c79b4015689a886cb170f1b9216d3d772075f
# Parent  3de7464450b045c81b5457c8144f267923fc312d
tuned names

diff -r 3de7464450b0 -r 088c79b40156 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue May 30 11:12:00 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue May 30 14:04:48 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 = n])
+      apply (rule GreatestI_nat [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 = "n" and P = "\<lambda>k. k\<le>n \<and> a k \<noteq> 0"]
+      using Greatest_le_nat [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 = "n"])
+      apply (rule Greatest_le_nat [where b = "n"])
       using k apply auto
       done
     with k m show ?thesis
diff -r 3de7464450b0 -r 088c79b40156 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Tue May 30 11:12:00 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Tue May 30 14:04:48 2017 +0200
@@ -325,9 +325,9 @@
     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 \<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 coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[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])
+      unfolding m_def by (rule Greatest_le_nat[OF that B])
     hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
 
     have "c dvd coeff a i" for i
diff -r 3de7464450b0 -r 088c79b40156 src/HOL/Lattices_Big.thy
--- a/src/HOL/Lattices_Big.thy	Tue May 30 11:12:00 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Tue May 30 14:04:48 2017 +0200
@@ -985,32 +985,4 @@
   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 ? *)
-definition Greatest :: "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "GREATEST " 10)
-where "Greatest \<equiv> arg_max (\<lambda>x. x)"
-
-lemma Greatest_equality:
-  "\<lbrakk> P k;  \<And>x. P x \<Longrightarrow> x \<le> k \<rbrakk> \<Longrightarrow> (Greatest P) = k"
-  for k :: "'a::order"
-apply (simp add: Greatest_def)
-apply (erule arg_max_equality)
-apply blast
-done
-
-lemma GreatestI: "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (Greatest P)"
-  for k :: nat
-unfolding Greatest_def by (rule arg_max_natI) auto
-
-lemma Greatest_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> x \<le> (Greatest P)"
-  for x :: nat
-unfolding Greatest_def by (rule arg_max_nat_le) auto
-
-lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (Greatest P)"
-apply (erule exE)
-apply (erule (1) GreatestI)
-done
-*)
 end
diff -r 3de7464450b0 -r 088c79b40156 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue May 30 11:12:00 2017 +0200
+++ b/src/HOL/Nat.thy	Tue May 30 14:04:48 2017 +0200
@@ -2166,17 +2166,20 @@
   qed
 qed
 
-lemma GreatestI: "\<lbrakk> P(k::nat); \<forall>y. P y \<longrightarrow> y \<le> b \<rbrakk> \<Longrightarrow> P (Greatest P)"
+lemma GreatestI_nat:
+  "\<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)"
+lemma Greatest_le_nat:
+  "\<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)"
+lemma GreatestI_ex_nat:
+  "\<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)
+apply (erule (1) GreatestI_nat)
 done