src/HOL/Hilbert_Choice.thy
 author wenzelm Sat Nov 03 01:33:54 2001 +0100 (2001-11-03) changeset 12023 d982f98e0f0d parent 11506 244a02a2968b child 12298 b344486c33e2 permissions -rw-r--r--
tuned;
```     1 (*  Title:      HOL/Hilbert_Choice.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson
```
```     4     Copyright   2001  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
```
```     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
```