src/HOL/Hilbert_Choice.thy
changeset 11451 8abfb4f7bd02
child 11454 7514e5e21cb8
equal deleted inserted replaced
11450:1b02a6c4032f 11451:8abfb4f7bd02
       
     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 constdefs  
       
    33   inv :: "('a => 'b) => ('b => 'a)"
       
    34     "inv(f::'a=>'b) == % y. @x. f(x)=y"
       
    35 
       
    36   Inv :: "['a set, 'a => 'b] => ('b => 'a)"
       
    37     "Inv A f == (% x. (@ y. y : A & f y = x))"
       
    38 
       
    39 
       
    40 use "Hilbert_Choice_lemmas.ML"
       
    41 
       
    42 
       
    43 (** Least value operator **)
       
    44 
       
    45 constdefs
       
    46   LeastM   :: "['a => 'b::ord, 'a => bool] => 'a"
       
    47               "LeastM m P == @x. P x & (ALL y. P y --> m x <= m y)"
       
    48 
       
    49 syntax
       
    50  "@LeastM" :: "[pttrn, 'a=>'b::ord, bool] => 'a" ("LEAST _ WRT _. _" [0,4,10]10)
       
    51 
       
    52 translations
       
    53                 "LEAST x WRT m. P" == "LeastM m (%x. P)"
       
    54 
       
    55 lemma LeastMI2:
       
    56   "[| P x; !!y. P y ==> m x <= m y;
       
    57            !!x. [| P x; \\<forall>y. P y --> m x \\<le> m y |] ==> Q x |]
       
    58    ==> Q (LeastM m P)";
       
    59 apply (unfold LeastM_def)
       
    60 apply (rule someI2_ex)
       
    61 apply  blast
       
    62 apply blast
       
    63 done
       
    64 
       
    65 lemma LeastM_equality:
       
    66  "[| P k; !!x. P x ==> m k <= m x |] ==> m (LEAST x WRT m. P x) = 
       
    67      (m k::'a::order)";
       
    68 apply (rule LeastMI2)
       
    69 apply   assumption
       
    70 apply  blast
       
    71 apply (blast intro!: order_antisym) 
       
    72 done
       
    73 
       
    74 
       
    75 (** Greatest value operator **)
       
    76 
       
    77 constdefs
       
    78   GreatestM   :: "['a => 'b::ord, 'a => bool] => 'a"
       
    79               "GreatestM m P == @x. P x & (ALL y. P y --> m y <= m x)"
       
    80   
       
    81   Greatest    :: "('a::ord => bool) => 'a"         (binder "GREATEST " 10)
       
    82               "Greatest     == GreatestM (%x. x)"
       
    83 
       
    84 syntax
       
    85  "@GreatestM" :: "[pttrn, 'a=>'b::ord, bool] => 'a"
       
    86                                         ("GREATEST _ WRT _. _" [0,4,10]10)
       
    87 
       
    88 translations
       
    89               "GREATEST x WRT m. P" == "GreatestM m (%x. P)"
       
    90 
       
    91 lemma GreatestMI2:
       
    92      "[| P x;
       
    93 	 !!y. P y ==> m y <= m x;
       
    94          !!x. [| P x; \\<forall>y. P y --> m y \\<le> m x |] ==> Q x |]
       
    95       ==> Q (GreatestM m P)";
       
    96 apply (unfold GreatestM_def)
       
    97 apply (rule someI2_ex)
       
    98 apply  blast
       
    99 apply blast
       
   100 done
       
   101 
       
   102 lemma GreatestM_equality:
       
   103  "[| P k;  !!x. P x ==> m x <= m k |]
       
   104   ==> m (GREATEST x WRT m. P x) = (m k::'a::order)";
       
   105 apply (rule_tac m=m in GreatestMI2)
       
   106 apply   assumption
       
   107 apply  blast
       
   108 apply (blast intro!: order_antisym) 
       
   109 done
       
   110 
       
   111 lemma Greatest_equality:
       
   112   "[| P (k::'a::order); !!x. P x ==> x <= k |] ==> (GREATEST x. P x) = k";
       
   113 apply (unfold Greatest_def)
       
   114 apply (erule GreatestM_equality)
       
   115 apply blast
       
   116 done
       
   117 
       
   118 lemma ex_has_greatest_nat_lemma:
       
   119      "[|P k;  ALL x. P x --> (EX y. P y & ~ ((m y::nat) <= m x))|]  
       
   120       ==> EX y. P y & ~ (m y < m k + n)"
       
   121 apply (induct_tac "n")
       
   122 apply force
       
   123 (*ind step*)
       
   124 apply (force simp add: le_Suc_eq)
       
   125 done
       
   126 
       
   127 lemma ex_has_greatest_nat: "[|P k;  ! y. P y --> m y < b|]  
       
   128       ==> ? x. P x & (! y. P y --> (m y::nat) <= m x)"
       
   129 apply (rule ccontr)
       
   130 apply (cut_tac P = "P" and n = "b - m k" in ex_has_greatest_nat_lemma)
       
   131 apply (subgoal_tac [3] "m k <= b")
       
   132 apply auto
       
   133 done
       
   134 
       
   135 lemma GreatestM_nat_lemma: 
       
   136      "[|P k;  ! y. P y --> m y < b|]  
       
   137       ==> P (GreatestM m P) & (!y. P y --> (m y::nat) <= m (GreatestM m P))"
       
   138 apply (unfold GreatestM_def)
       
   139 apply (rule someI_ex)
       
   140 apply (erule ex_has_greatest_nat)
       
   141 apply assumption
       
   142 done
       
   143 
       
   144 lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
       
   145 
       
   146 lemma GreatestM_nat_le: "[|P x;  ! y. P y --> m y < b|]  
       
   147       ==> (m x::nat) <= m (GreatestM m P)"
       
   148 apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec]) 
       
   149 done
       
   150 
       
   151 (** Specialization to GREATEST **)
       
   152 
       
   153 lemma GreatestI: 
       
   154      "[|P (k::nat);  ! y. P y --> y < b|] ==> P (GREATEST x. P x)"
       
   155 
       
   156 apply (unfold Greatest_def)
       
   157 apply (rule GreatestM_natI)
       
   158 apply auto
       
   159 done
       
   160 
       
   161 lemma Greatest_le: 
       
   162      "[|P x;  ! y. P y --> y < b|] ==> (x::nat) <= (GREATEST x. P x)"
       
   163 apply (unfold Greatest_def)
       
   164 apply (rule GreatestM_nat_le)
       
   165 apply auto
       
   166 done
       
   167 
       
   168 
       
   169 ML {*
       
   170 val LeastMI2 = thm "LeastMI2";
       
   171 val LeastM_equality = thm "LeastM_equality";
       
   172 val GreatestM_def = thm "GreatestM_def";
       
   173 val GreatestMI2 = thm "GreatestMI2";
       
   174 val GreatestM_equality = thm "GreatestM_equality";
       
   175 val Greatest_def = thm "Greatest_def";
       
   176 val Greatest_equality = thm "Greatest_equality";
       
   177 val GreatestM_natI = thm "GreatestM_natI";
       
   178 val GreatestM_nat_le = thm "GreatestM_nat_le";
       
   179 val GreatestI = thm "GreatestI";
       
   180 val Greatest_le = thm "Greatest_le";
       
   181 *}
       
   182 
       
   183 use "meson_lemmas.ML"
       
   184 use "Tools/meson.ML"
       
   185 setup meson_setup
       
   186 
       
   187 end