--- a/src/HOL/Hilbert_Choice.thy Sun May 28 13:57:43 2017 +0200
+++ b/src/HOL/Hilbert_Choice.thy Sun May 28 15:46:26 2017 +0200
@@ -522,92 +522,6 @@
lemma tfl_some: "\<forall>P x. P x \<longrightarrow> P (Eps P)"
by (blast intro: someI)
-(*
-subsection \<open>Greatest value operator\<close>
-
-definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
- where "GreatestM m P \<equiv> SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m x)"
-
-definition Greatest :: "('a::ord \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREATEST " 10)
- where "Greatest \<equiv> GreatestM (\<lambda>x. x)"
-
-syntax
- "_GreatestM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a" ("GREATEST _ WRT _. _" [0, 4, 10] 10)
-translations
- "GREATEST x WRT m. P" \<rightleftharpoons> "CONST GreatestM m (\<lambda>x. P)"
-
-lemma GreatestMI2:
- "P x \<Longrightarrow>
- (\<And>y. P y \<Longrightarrow> m y \<le> m x) \<Longrightarrow>
- (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y \<le> m x \<Longrightarrow> Q x) \<Longrightarrow>
- Q (GreatestM m P)"
- apply (simp add: GreatestM_def)
- apply (rule someI2_ex)
- apply blast
- apply blast
- done
-
-lemma GreatestM_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m x \<le> m k) \<Longrightarrow> m (GREATEST x WRT m. P x) = m k"
- for m :: "_ \<Rightarrow> 'a::order"
- apply (rule GreatestMI2 [where m = m])
- apply assumption
- apply blast
- apply (blast intro!: order_antisym)
- done
-
-lemma Greatest_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> x \<le> k) \<Longrightarrow> (GREATEST x. P x) = k"
- for k :: "'a::order"
- apply (simp add: Greatest_def)
- apply (erule GreatestM_equality)
- apply blast
- done
-
-lemma ex_has_greatest_nat_lemma:
- "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> m y \<le> m x) \<Longrightarrow> \<exists>y. P y \<and> \<not> m y < m k + n"
- for m :: "'a \<Rightarrow> nat"
- by (induct n) (force simp: le_Suc_eq)+
-
-lemma ex_has_greatest_nat:
- "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m x)"
- for m :: "'a \<Rightarrow> nat"
- apply (rule ccontr)
- apply (cut_tac P = P and n = "b - m k" in ex_has_greatest_nat_lemma)
- apply (subgoal_tac [3] "m k \<le> b")
- apply auto
- done
-
-lemma GreatestM_nat_lemma:
- "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> P (GreatestM m P) \<and> (\<forall>y. P y \<longrightarrow> m y \<le> m (GreatestM m P))"
- for m :: "'a \<Rightarrow> nat"
- apply (simp add: GreatestM_def)
- apply (rule someI_ex)
- apply (erule ex_has_greatest_nat)
- apply assumption
- done
-
-lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1]
-
-lemma GreatestM_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m y < b \<Longrightarrow> m x \<le> m (GreatestM m P)"
- for m :: "'a \<Rightarrow> nat"
- by (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
-
-
-text \<open>\<^medskip> Specialization to \<open>GREATEST\<close>.\<close>
-
-lemma GreatestI: "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
- for k :: nat
- unfolding Greatest_def by (rule GreatestM_natI) auto
-
-lemma Greatest_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> x \<le> (GREATEST x. P x)"
- for x :: nat
- unfolding Greatest_def by (rule GreatestM_nat_le) auto
-
-lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
- apply (erule exE)
- apply (rule GreatestI)
- apply assumption+
- done
-*)
subsection \<open>An aside: bounded accessible part\<close>