added symbols syntax;
authorwenzelm
Wed Nov 27 16:51:15 1996 +0100 (1996-11-27)
changeset 2260b59781f2b809
parent 2259 e6d738f2b9a9
child 2261 d926157c0a6a
added symbols syntax;
src/HOL/HOL.thy
src/HOL/Prod.thy
     1.1 --- a/src/HOL/HOL.thy	Wed Nov 27 16:48:19 1996 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Nov 27 16:51:15 1996 +0100
     1.3 @@ -3,23 +3,17 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -Higher-Order Logic
     1.8 +Higher-Order Logic.
     1.9  *)
    1.10  
    1.11  HOL = CPure +
    1.12  
    1.13 +
    1.14 +(** Core syntax **)
    1.15 +
    1.16  classes
    1.17    term < logic
    1.18  
    1.19 -axclass
    1.20 -  plus < term
    1.21 -
    1.22 -axclass
    1.23 -  minus < term
    1.24 -
    1.25 -axclass
    1.26 -  times < term
    1.27 -
    1.28  default
    1.29    term
    1.30  
    1.31 @@ -57,13 +51,27 @@
    1.32    "|"           :: [bool, bool] => bool             (infixr 30)
    1.33    "-->"         :: [bool, bool] => bool             (infixr 25)
    1.34  
    1.35 -  (* Overloaded Constants *)
    1.36 +
    1.37 +(* Overloaded Constants *)
    1.38 +
    1.39 +axclass
    1.40 +  plus < term
    1.41  
    1.42 +axclass
    1.43 +  minus < term
    1.44 +
    1.45 +axclass
    1.46 +  times < term
    1.47 +
    1.48 +consts
    1.49    "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
    1.50    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    1.51    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.52  
    1.53  
    1.54 +
    1.55 +(** Additional concrete syntax **)
    1.56 +
    1.57  types
    1.58    letbinds  letbind
    1.59    case_syn  cases_syn
    1.60 @@ -72,7 +80,7 @@
    1.61  
    1.62    "~="          :: ['a, 'a] => bool                 (infixl 50)
    1.63  
    1.64 -  "@Eps"        :: [pttrn,bool] => 'a               ("(3@ _./ _)" 10)
    1.65 +  "@Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" 10)
    1.66  
    1.67    (* Alternative Quantifiers *)
    1.68  
    1.69 @@ -96,13 +104,34 @@
    1.70  
    1.71  translations
    1.72    "x ~= y"      == "~ (x = y)"
    1.73 -  "@ x.b"       == "Eps(%x.b)"
    1.74 +  "@ x.b"       == "Eps (%x. b)"
    1.75    "ALL xs. P"   => "! xs. P"
    1.76    "EX xs. P"    => "? xs. P"
    1.77    "EX! xs. P"   => "?! xs. P"
    1.78    "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
    1.79    "let x = a in e"        == "Let a (%x. e)"
    1.80  
    1.81 +
    1.82 +syntax (symbols)
    1.83 +  not           :: bool => bool                     ("\\<not> _" [40] 40)
    1.84 +  "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
    1.85 +  "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
    1.86 +  "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
    1.87 +  "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
    1.88 +  "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
    1.89 +  "@Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" 10)
    1.90 +  "! "          :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
    1.91 +  "? "          :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
    1.92 +  "?! "         :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
    1.93 +  "*All"        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" 10)
    1.94 +  "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" 10)
    1.95 +  "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" 10)
    1.96 +  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<mapsto>/ _)" 10)
    1.97 +
    1.98 +
    1.99 +
   1.100 +(** Rules and definitions **)
   1.101 +
   1.102  rules
   1.103  
   1.104    eq_reflection "(x=y) ==> (x==y)"
   1.105 @@ -147,6 +176,7 @@
   1.106  
   1.107  end
   1.108  
   1.109 +
   1.110  ML
   1.111  
   1.112  (** Choice between the HOL and Isabelle style of quantifiers **)
   1.113 @@ -168,6 +198,3 @@
   1.114  
   1.115  (* start 8bit 2 *)
   1.116  (* end 8bit 2 *)
   1.117 -
   1.118 -
   1.119 -
     2.1 --- a/src/HOL/Prod.thy	Wed Nov 27 16:48:19 1996 +0100
     2.2 +++ b/src/HOL/Prod.thy	Wed Nov 27 16:51:15 1996 +0100
     2.3 @@ -9,7 +9,8 @@
     2.4  
     2.5  Prod = Fun + equalities +
     2.6  
     2.7 -(** Products **)
     2.8 +
     2.9 +(** products **)
    2.10  
    2.11  (* type definition *)
    2.12  
    2.13 @@ -21,6 +22,9 @@
    2.14    ('a, 'b) "*"          (infixr 20)
    2.15      = "{f. ? a b. f = Pair_Rep (a::'a) (b::'b)}"
    2.16  
    2.17 +syntax (symbols)
    2.18 +  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
    2.19 +
    2.20  
    2.21  (* abstract constants and syntax *)
    2.22  
    2.23 @@ -32,30 +36,37 @@
    2.24    Pair          :: "['a, 'b] => 'a * 'b"
    2.25    Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
    2.26  
    2.27 -(** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
    2.28 +
    2.29 +(* patterns -- extends pre-defined type "pttrn" used in abstractions *)
    2.30 +
    2.31  types pttrns
    2.32  
    2.33  syntax
    2.34 -  "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
    2.35 +  "@Tuple"      :: "['a, args] => 'a * 'b"      ("(1'(_,/ _'))")
    2.36  
    2.37 -  "@pttrn"  :: [pttrn,pttrns] => pttrn              ("'(_,/_')")
    2.38 -  ""        ::  pttrn         => pttrns             ("_")
    2.39 -  "@pttrns" :: [pttrn,pttrns] => pttrns             ("_,/_")
    2.40 +  "@pttrn"      :: [pttrn, pttrns] => pttrn     ("'(_,/_')")
    2.41 +  ""            :: pttrn => pttrns              ("_")
    2.42 +  "@pttrns"     :: [pttrn, pttrns] => pttrns    ("_,/_")
    2.43  
    2.44 -  "@Sigma"  :: "[idt,'a set,'b set] => ('a * 'b)set"
    2.45 -               ("(3SIGMA _:_./ _)" 10)
    2.46 -  "@Times"  :: "['a set, 'a => 'b set] => ('a * 'b) set"
    2.47 -               ("_ Times _" [81,80] 80)
    2.48 +  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3SIGMA _:_./ _)" 10)
    2.49 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
    2.50  
    2.51  translations
    2.52    "(x, y, z)"   == "(x, (y, z))"
    2.53    "(x, y)"      == "Pair x y"
    2.54  
    2.55 -  "%(x,y,zs).b"   == "split(%x (y,zs).b)"
    2.56 -  "%(x,y).b"      == "split(%x y.b)"
    2.57 +  "%(x,y,zs).b" == "split(%x (y,zs).b)"
    2.58 +  "%(x,y).b"    == "split(%x y.b)"
    2.59 +
    2.60 +  "SIGMA x:A.B" => "Sigma A (%x.B)"
    2.61 +  "A Times B"   => "Sigma A (_K B)"
    2.62  
    2.63 -  "SIGMA x:A. B"  =>  "Sigma A (%x.B)"
    2.64 -  "A Times B"     =>  "Sigma A (_K B)"
    2.65 +syntax (symbols)
    2.66 +  "@Sigma"      :: "[idt, 'a set, 'b set] => ('a * 'b) set"     ("(3\\<Sigma> _\\<in>_./ _)" 10)
    2.67 +  "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ \\<times> _" [81, 80] 80)
    2.68 +
    2.69 +
    2.70 +(* definitions *)
    2.71  
    2.72  defs
    2.73    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    2.74 @@ -65,7 +76,9 @@
    2.75    prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    2.76    Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    2.77  
    2.78 -(** Unit **)
    2.79 +
    2.80 +
    2.81 +(** unit **)
    2.82  
    2.83  typedef (Unit)
    2.84    unit = "{p. p = True}"