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