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"