src/HOL/Hilbert_Choice.thy
changeset 65952 dec96cb3fbe0
parent 65815 416aa3b00cbe
child 65954 431024edc9cf
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat May 27 22:52:08 2017 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun May 28 08:07:40 2017 +0200
     1.3 @@ -523,64 +523,6 @@
     1.4    by (blast intro: someI)
     1.5  
     1.6  
     1.7 -subsection \<open>Least value operator\<close>
     1.8 -
     1.9 -definition LeastM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"
    1.10 -  where "LeastM m P \<equiv> (SOME x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y))"
    1.11 -
    1.12 -syntax
    1.13 -  "_LeastM" :: "pttrn \<Rightarrow> ('a \<Rightarrow> 'b::ord) \<Rightarrow> bool \<Rightarrow> 'a"  ("LEAST _ WRT _. _" [0, 4, 10] 10)
    1.14 -translations
    1.15 -  "LEAST x WRT m. P" \<rightleftharpoons> "CONST LeastM m (\<lambda>x. P)"
    1.16 -
    1.17 -lemma LeastMI2:
    1.18 -  "P x \<Longrightarrow>
    1.19 -    (\<And>y. P y \<Longrightarrow> m x \<le> m y) \<Longrightarrow>
    1.20 -    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> m x \<le> m y \<Longrightarrow> Q x) \<Longrightarrow>
    1.21 -    Q (LeastM m P)"
    1.22 -  apply (simp add: LeastM_def)
    1.23 -  apply (rule someI2_ex)
    1.24 -   apply blast
    1.25 -  apply blast
    1.26 -  done
    1.27 -
    1.28 -lemma LeastM_equality: "P k \<Longrightarrow> (\<And>x. P x \<Longrightarrow> m k \<le> m x) \<Longrightarrow> m (LEAST x WRT m. P x) = m k"
    1.29 -  for m :: "_ \<Rightarrow> 'a::order"
    1.30 -  apply (rule LeastMI2)
    1.31 -    apply assumption
    1.32 -   apply blast
    1.33 -  apply (blast intro!: order_antisym)
    1.34 -  done
    1.35 -
    1.36 -lemma wf_linord_ex_has_least:
    1.37 -  "wf r \<Longrightarrow> \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>* \<Longrightarrow> P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
    1.38 -  apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
    1.39 -  apply (drule_tac x = "m ` Collect P" in spec)
    1.40 -  apply force
    1.41 -  done
    1.42 -
    1.43 -lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
    1.44 -  for m :: "'a \<Rightarrow> nat"
    1.45 -  apply (simp only: pred_nat_trancl_eq_le [symmetric])
    1.46 -  apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
    1.47 -   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
    1.48 -  apply assumption
    1.49 -  done
    1.50 -
    1.51 -lemma LeastM_nat_lemma: "P k \<Longrightarrow> P (LeastM m P) \<and> (\<forall>y. P y \<longrightarrow> m (LeastM m P) \<le> m y)"
    1.52 -  for m :: "'a \<Rightarrow> nat"
    1.53 -  apply (simp add: LeastM_def)
    1.54 -  apply (rule someI_ex)
    1.55 -  apply (erule ex_has_least_nat)
    1.56 -  done
    1.57 -
    1.58 -lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]
    1.59 -
    1.60 -lemma LeastM_nat_le: "P x \<Longrightarrow> m (LeastM m P) \<le> m x"
    1.61 -  for m :: "'a \<Rightarrow> nat"
    1.62 -  by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
    1.63 -
    1.64 -
    1.65  subsection \<open>Greatest value operator\<close>
    1.66  
    1.67  definition GreatestM :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a"