src/HOL/Hilbert_Choice.thy

 
 text \<open>A dynamically-scoped fact for TFL\<close>
 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>
 
 text \<open>Finite monotone eventually stable sequences\<close>