src/HOL/Hilbert_Choice.thy
 changeset 22690 0b08f218f260 parent 21999 0cf192e489e2 child 23433 c2c10abd2a1e
```     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Apr 14 23:56:36 2007 +0200
1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Apr 15 14:31:44 2007 +0200
1.3 @@ -13,8 +13,10 @@
1.4
1.5  subsection {* Hilbert's epsilon *}
1.6
1.7 -consts
1.8 -  Eps           :: "('a => bool) => 'a"
1.9 +axiomatization
1.10 +  Eps :: "('a => bool) => 'a"
1.11 +where
1.12 +  someI: "P x ==> P (Eps P)"
1.13
1.14  syntax (epsilon)
1.15    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
1.16 @@ -23,21 +25,15 @@
1.17  syntax
1.18    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
1.19  translations
1.20 -  "SOME x. P" == "Eps (%x. P)"
1.21 +  "SOME x. P" == "CONST Eps (%x. P)"
1.22
1.23  print_translation {*
1.24  (* to avoid eta-contraction of body *)
1.25 -[("Eps", fn [Abs abs] =>
1.26 +[(@{const_syntax Eps}, fn [Abs abs] =>
1.27       let val (x,t) = atomic_abs_tr' abs
1.28       in Syntax.const "_Eps" \$ x \$ t end)]
1.29  *}
1.30
1.31 -axioms
1.32 -  someI: "P (x::'a) ==> P (SOME x. P x)"
1.33 -finalconsts
1.34 -  Eps
1.35 -
1.36 -
1.37  constdefs
1.38    inv :: "('a => 'b) => ('b => 'a)"
1.39    "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
```