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