replaced axioms/finalconsts by proper axiomatization;
authorwenzelm
Sun Apr 15 14:31:44 2007 +0200 (2007-04-15)
changeset 226900b08f218f260
parent 22689 b800228434a8
child 22691 290454649b8c
replaced axioms/finalconsts by proper axiomatization;
src/HOL/Hilbert_Choice.thy
src/HOL/ZF/HOLZF.thy
     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"
     2.1 --- a/src/HOL/ZF/HOLZF.thy	Sat Apr 14 23:56:36 2007 +0200
     2.2 +++ b/src/HOL/ZF/HOLZF.thy	Sun Apr 15 14:31:44 2007 +0200
     2.3 @@ -12,12 +12,12 @@
     2.4  
     2.5  typedecl ZF
     2.6  
     2.7 -consts
     2.8 -  Empty :: ZF
     2.9 -  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
    2.10 -  Sum :: "ZF \<Rightarrow> ZF"
    2.11 -  Power :: "ZF \<Rightarrow> ZF"
    2.12 -  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF"
    2.13 +axiomatization
    2.14 +  Empty :: ZF and
    2.15 +  Elem :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" and
    2.16 +  Sum :: "ZF \<Rightarrow> ZF" and
    2.17 +  Power :: "ZF \<Rightarrow> ZF" and
    2.18 +  Repl :: "ZF \<Rightarrow> (ZF \<Rightarrow> ZF) \<Rightarrow> ZF" and
    2.19    Inf :: ZF
    2.20  
    2.21  constdefs
    2.22 @@ -32,9 +32,6 @@
    2.23    subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool"
    2.24    "subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
    2.25  
    2.26 -finalconsts 
    2.27 -  Empty Elem Sum Power Repl Inf
    2.28 -
    2.29  axioms
    2.30    Empty: "Not (Elem x Empty)"
    2.31    Ext: "(x = y) = (! z. Elem z x = Elem z y)"