--- 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
--- 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])
--- 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
--- 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>"
--- 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: