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
```     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
```