11 uses ("Tools/meson.ML") ("Tools/specification_package.ML") |
11 uses ("Tools/meson.ML") ("Tools/specification_package.ML") |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Hilbert's epsilon *} |
14 subsection {* Hilbert's epsilon *} |
15 |
15 |
16 consts |
16 axiomatization |
17 Eps :: "('a => bool) => 'a" |
17 Eps :: "('a => bool) => 'a" |
|
18 where |
|
19 someI: "P x ==> P (Eps P)" |
18 |
20 |
19 syntax (epsilon) |
21 syntax (epsilon) |
20 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
22 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
21 syntax (HOL) |
23 syntax (HOL) |
22 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
24 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
23 syntax |
25 syntax |
24 "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) |
26 "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) |
25 translations |
27 translations |
26 "SOME x. P" == "Eps (%x. P)" |
28 "SOME x. P" == "CONST Eps (%x. P)" |
27 |
29 |
28 print_translation {* |
30 print_translation {* |
29 (* to avoid eta-contraction of body *) |
31 (* to avoid eta-contraction of body *) |
30 [("Eps", fn [Abs abs] => |
32 [(@{const_syntax Eps}, fn [Abs abs] => |
31 let val (x,t) = atomic_abs_tr' abs |
33 let val (x,t) = atomic_abs_tr' abs |
32 in Syntax.const "_Eps" $ x $ t end)] |
34 in Syntax.const "_Eps" $ x $ t end)] |
33 *} |
35 *} |
34 |
|
35 axioms |
|
36 someI: "P (x::'a) ==> P (SOME x. P x)" |
|
37 finalconsts |
|
38 Eps |
|
39 |
|
40 |
36 |
41 constdefs |
37 constdefs |
42 inv :: "('a => 'b) => ('b => 'a)" |
38 inv :: "('a => 'b) => ('b => 'a)" |
43 "inv(f :: 'a => 'b) == %y. SOME x. f x = y" |
39 "inv(f :: 'a => 'b) == %y. SOME x. f x = y" |
44 |
40 |