src/HOL/HOL.thy
changeset 7238 36e58620ffc8
parent 7220 da6f387ca482
child 7357 d0e16da40ea2
     1.1 --- a/src/HOL/HOL.thy	Tue Aug 17 22:11:05 1999 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Aug 17 22:13:23 1999 +0200
     1.3 @@ -40,9 +40,9 @@
     1.4    (* Binders *)
     1.5  
     1.6    Eps           :: ('a => bool) => 'a
     1.7 -  All           :: ('a => bool) => bool             (binder "! " 10)
     1.8 -  Ex            :: ('a => bool) => bool             (binder "? " 10)
     1.9 -  Ex1           :: ('a => bool) => bool             (binder "?! " 10)
    1.10 +  All           :: ('a => bool) => bool             (binder "ALL " 10)
    1.11 +  Ex            :: ('a => bool) => bool             (binder "EX " 10)
    1.12 +  Ex1           :: ('a => bool) => bool             (binder "EX! " 10)
    1.13    Let           :: ['a, 'a => 'b] => 'b
    1.14  
    1.15    (* Infixes *)
    1.16 @@ -75,6 +75,7 @@
    1.17    (*See Nat.thy for "^"*)
    1.18  
    1.19  
    1.20 +
    1.21  (** Additional concrete syntax **)
    1.22  
    1.23  nonterminals
    1.24 @@ -82,16 +83,8 @@
    1.25    case_syn  cases_syn
    1.26  
    1.27  syntax
    1.28 -
    1.29    "~="          :: ['a, 'a] => bool                 (infixl 50)
    1.30 -
    1.31 -  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
    1.32 -
    1.33 -  (* Alternative Quantifiers *)
    1.34 -
    1.35 -  "*All"        :: [idts, bool] => bool             ("(3ALL _./ _)" [0, 10] 10)
    1.36 -  "*Ex"         :: [idts, bool] => bool             ("(3EX _./ _)" [0, 10] 10)
    1.37 -  "*Ex1"        :: [idts, bool] => bool             ("(3EX! _./ _)" [0, 10] 10)
    1.38 +  "_Eps"        :: [pttrn, bool] => 'a              ("(3SOME _./ _)" [0, 10] 10)
    1.39  
    1.40    (* Let expressions *)
    1.41  
    1.42 @@ -108,11 +101,8 @@
    1.43    "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ | _")
    1.44  
    1.45  translations
    1.46 -  "x ~= y"      == "~ (x = y)"
    1.47 -  "@ x. b"      == "Eps (%x. b)"
    1.48 -  "ALL xs. P"   => "! xs. P"
    1.49 -  "EX xs. P"    => "? xs. P"
    1.50 -  "EX! xs. P"   => "?! xs. P"
    1.51 +  "x ~= y"                == "~ (x = y)"
    1.52 +  "SOME x. P"             == "Eps (%x. P)"
    1.53    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.54    "let x = a in e"        == "Let a (%x. e)"
    1.55  
    1.56 @@ -127,18 +117,15 @@
    1.57    "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.58    "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
    1.59    "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
    1.60 -  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
    1.61 -  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.62 -  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.63 -  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.64 +  "_Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
    1.65 +  "ALL "        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.66 +  "EX "         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.67 +  "EX! "        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.68    "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
    1.69  (*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
    1.70  
    1.71  syntax (symbols output)
    1.72    "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
    1.73 -  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
    1.74 -  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
    1.75 -  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.76  
    1.77  syntax (xsymbols)
    1.78    "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
    1.79 @@ -146,6 +133,13 @@
    1.80  syntax (HTML output)
    1.81    Not           :: bool => bool                     ("\\<not> _" [40] 40)
    1.82  
    1.83 +syntax (HOL)
    1.84 +  "_Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
    1.85 +  "ALL "        :: [idts, bool] => bool             ("(3! _./ _)" [0, 10] 10)
    1.86 +  "EX "         :: [idts, bool] => bool             ("(3? _./ _)" [0, 10] 10)
    1.87 +  "EX! "        :: [idts, bool] => bool             ("(3?! _./ _)" [0, 10] 10)
    1.88 +
    1.89 +
    1.90  
    1.91  (** Rules and definitions **)
    1.92  
    1.93 @@ -205,24 +199,3 @@
    1.94  
    1.95  
    1.96  end
    1.97 -
    1.98 -
    1.99 -ML
   1.100 -
   1.101 -
   1.102 -(** Choice between the HOL and Isabelle style of quantifiers **)
   1.103 -
   1.104 -val HOL_quantifiers = ref true;
   1.105 -
   1.106 -fun alt_ast_tr' (name, alt_name) =
   1.107 -  let
   1.108 -    fun ast_tr' (*name*) args =
   1.109 -      if ! HOL_quantifiers then raise Match
   1.110 -      else Syntax.mk_appl (Syntax.Constant alt_name) args;
   1.111 -  in
   1.112 -    (name, ast_tr')
   1.113 -  end;
   1.114 -
   1.115 -
   1.116 -val print_ast_translation =
   1.117 -  map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];