src/HOL/Hilbert_Choice.thy
author wenzelm
Wed Aug 29 21:17:24 2001 +0200 (2001-08-29)
changeset 11506 244a02a2968b
parent 11454 7514e5e21cb8
child 12023 d982f98e0f0d
permissions -rw-r--r--
avoid ML bindings;
     1 (*  Title:      HOL/Hilbert_Choice.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   2001  University of Cambridge
     5 
     6 Hilbert's epsilon-operator and everything to do with the Axiom of Choice
     7 *)
     8 
     9 theory Hilbert_Choice = NatArith
    10 files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
    11 
    12 consts
    13   Eps           :: "('a => bool) => 'a"
    14 
    15 
    16 syntax (input)
    17   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\<epsilon>_./ _)" [0, 10] 10)
    18 
    19 syntax (HOL)
    20   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
    21 
    22 syntax
    23   "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
    24 
    25 translations
    26   "SOME x. P"             == "Eps (%x. P)"
    27 
    28 axioms  
    29   someI:        "P (x::'a) ==> P (SOME x. P x)"
    30 
    31 
    32 (*used in TFL*)
    33 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    34   by (blast intro: someI)
    35 
    36 
    37 constdefs  
    38   inv :: "('a => 'b) => ('b => 'a)"
    39     "inv(f::'a=>'b) == % y. @x. f(x)=y"
    40 
    41   Inv :: "['a set, 'a => 'b] => ('b => 'a)"
    42     "Inv A f == (% x. (@ y. y : A & f y = x))"
    43 
    44 
    45 use "Hilbert_Choice_lemmas.ML"
    46 
    47 
    48 (** Least value operator **)
    49 
    50 constdefs
    51   LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
    52               "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
    53 
    54 syntax
    55  "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
    56 
    57 translations
    58                 "LEAST x WRT m. P" == "LeastM m (%x. P)"
    59 
    60 lemma LeastMI2:
    61   "[| P x; !!y. P y ==> m x <= m y;
    62            !!x. [| P x; \<forall>y. P y --> m x \<le> m y |] ==> Q x |]
    63    ==> Q (LeastM m P)";
    64 apply (unfold LeastM_def)
    65 apply (rule someI2_ex)
    66 apply  blast
    67 apply blast
    68 done
    69 
    70 lemma LeastM_equality:
    71  "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
    72      (m k::'a::order)";
    73 apply (rule LeastMI2)
    74 apply   assumption
    75 apply  blast
    76 apply (blast intro!: order_antisym) 
    77 done
    78 
    79 lemma wf_linord_ex_has_least:
    80      "[|wf r;  ALL x y. ((x,y):r^+) = ((y,x)~:r^*);  P k|]  \
    81 \     ==> EX x. P x & (!y. P y --> (m x,m y):r^*)" 
    82 apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
    83 apply (drule_tac x = "m`Collect P" in spec)
    84 apply force
    85 done
    86 
    87 (* successor of obsolete nonempty_has_least *)
    88 lemma ex_has_least_nat:
    89      "P k ==> EX x. P x & (ALL y. P y --> m x <= (m y::nat))"
    90 apply (simp only: pred_nat_trancl_eq_le [symmetric])
    91 apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
    92 apply (simp (no_asm) add: less_eq not_le_iff_less pred_nat_trancl_eq_le)
    93 apply assumption
    94 done
    95 
    96 lemma LeastM_nat_lemma: 
    97   "P k ==> P (LeastM m P) & (ALL y. P y --> m (LeastM m P) <= (m y::nat))"
    98 apply (unfold LeastM_def)
    99 apply (rule someI_ex)
   100 apply (erule ex_has_least_nat)
   101 done
   102 
   103 lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
   104 
   105 lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
   106 apply (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
   107 apply assumption
   108 apply assumption
   109 done
   110 
   111 
   112 (** Greatest value operator **)
   113 
   114 constdefs
   115   GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
   116               "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
   117   
   118   Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
   119               "Greatest     == GreatestM (%x. x)"
   120 
   121 syntax
   122  "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
   123                                         ("GREATEST _ WRT _. _" [0,4,10]10)
   124 
   125 translations
   126               "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
   127 
   128 lemma GreatestMI2:
   129      "[| P x;
   130 	 !!y. P y ==> m y <= m x;
   131          !!x. [| P x; \<forall>y. P y --> m y \<le> m x |] ==> Q x |]
   132       ==> Q (GreatestM m P)";
   133 apply (unfold GreatestM_def)
   134 apply (rule someI2_ex)
   135 apply  blast
   136 apply blast
   137 done
   138 
   139 lemma GreatestM_equality:
   140  "[| P k;  !!x. P x ==> m x <= m k |]
   141   ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
   142 apply (rule_tac m=m in GreatestMI2)
   143 apply   assumption
   144 apply  blast
   145 apply (blast intro!: order_antisym) 
   146 done
   147 
   148 lemma Greatest_equality:
   149   "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
   150 apply (unfold Greatest_def)
   151 apply (erule GreatestM_equality)
   152 apply blast
   153 done
   154 
   155 lemma ex_has_greatest_nat_lemma:
   156      "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]  
   157       ==> EX y. P y & ~ (m y < m k + n)"
   158 apply (induct_tac "n")
   159 apply force
   160 (*ind step*)
   161 apply (force simp add: le_Suc_eq)
   162 done
   163 
   164 lemma ex_has_greatest_nat: "[|P k;  ! y. P y --> m y < b|]  
   165       ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
   166 apply (rule ccontr)
   167 apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
   168 apply (subgoal_tac [3] "m k <= b")
   169 apply auto
   170 done
   171 
   172 lemma GreatestM_nat_lemma: 
   173      "[|P k;  ! y. P y --> m y < b|]  
   174       ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
   175 apply (unfold GreatestM_def)
   176 apply (rule someI_ex)
   177 apply (erule ex_has_greatest_nat)
   178 apply assumption
   179 done
   180 
   181 lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
   182 
   183 lemma GreatestM_nat_le: "[|P x;  ! y. P y --> m y < b|]  
   184       ==> (m x::nat) <= m (GreatestM m P)"
   185 apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
   186 done
   187 
   188 (** Specialization to GREATEST **)
   189 
   190 lemma GreatestI: 
   191      "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
   192 
   193 apply (unfold Greatest_def)
   194 apply (rule GreatestM_natI)
   195 apply auto
   196 done
   197 
   198 lemma Greatest_le: 
   199      "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
   200 apply (unfold Greatest_def)
   201 apply (rule GreatestM_nat_le)
   202 apply auto
   203 done
   204 
   205 
   206 use "meson_lemmas.ML"
   207 use "Tools/meson.ML"
   208 setup meson_setup
   209 
   210 end