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