--- 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
--- 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
--- 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
--- 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