src/HOL/HOL.thy
changeset 7357 d0e16da40ea2
parent 7238 36e58620ffc8
child 7369 2d2110cda81e
     1.1 --- a/src/HOL/HOL.thy	Wed Aug 25 20:46:40 1999 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 25 20:49:02 1999 +0200
     1.3 @@ -6,72 +6,63 @@
     1.4  Higher-Order Logic.
     1.5  *)
     1.6  
     1.7 -HOL = CPure +
     1.8 +theory HOL = CPure
     1.9 +files ("HOL_lemmas.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML"):
    1.10  
    1.11  
    1.12  (** Core syntax **)
    1.13  
    1.14  global
    1.15  
    1.16 -classes
    1.17 -  term < logic
    1.18 +classes "term" < logic
    1.19 +defaultsort "term"
    1.20  
    1.21 -default
    1.22 -  term
    1.23 -
    1.24 -types
    1.25 -  bool
    1.26 +typedecl bool
    1.27  
    1.28  arities
    1.29 -  fun :: (term, term) term
    1.30 -  bool :: term
    1.31 +  bool :: "term"
    1.32 +  fun :: ("term", "term") "term"
    1.33  
    1.34  
    1.35  consts
    1.36  
    1.37    (* Constants *)
    1.38  
    1.39 -  Trueprop      :: bool => prop                     ("(_)" 5)
    1.40 -  Not           :: bool => bool                     ("~ _" [40] 40)
    1.41 -  True, False   :: bool
    1.42 -  If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    1.43 +  Trueprop      :: "bool => prop"                   ("(_)" 5)
    1.44 +  Not           :: "bool => bool"                   ("~ _" [40] 40)
    1.45 +  True          :: bool
    1.46 +  False         :: bool
    1.47 +  If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)
    1.48    arbitrary     :: 'a
    1.49  
    1.50    (* Binders *)
    1.51  
    1.52 -  Eps           :: ('a => bool) => 'a
    1.53 -  All           :: ('a => bool) => bool             (binder "ALL " 10)
    1.54 -  Ex            :: ('a => bool) => bool             (binder "EX " 10)
    1.55 -  Ex1           :: ('a => bool) => bool             (binder "EX! " 10)
    1.56 -  Let           :: ['a, 'a => 'b] => 'b
    1.57 +  Eps           :: "('a => bool) => 'a"
    1.58 +  All           :: "('a => bool) => bool"           (binder "ALL " 10)
    1.59 +  Ex            :: "('a => bool) => bool"           (binder "EX " 10)
    1.60 +  Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
    1.61 +  Let           :: "['a, 'a => 'b] => 'b"
    1.62  
    1.63    (* Infixes *)
    1.64  
    1.65 -  "="           :: ['a, 'a] => bool                 (infixl 50)
    1.66 -  "&"           :: [bool, bool] => bool             (infixr 35)
    1.67 -  "|"           :: [bool, bool] => bool             (infixr 30)
    1.68 -  "-->"         :: [bool, bool] => bool             (infixr 25)
    1.69 +  "="           :: "['a, 'a] => bool"               (infixl 50)
    1.70 +  &             :: "[bool, bool] => bool"           (infixr 35)
    1.71 +  "|"           :: "[bool, bool] => bool"           (infixr 30)
    1.72 +  -->           :: "[bool, bool] => bool"           (infixr 25)
    1.73  
    1.74  
    1.75  (* Overloaded Constants *)
    1.76  
    1.77 -axclass
    1.78 -  plus < term
    1.79 -
    1.80 -axclass
    1.81 -  minus < term
    1.82 -
    1.83 -axclass
    1.84 -  times < term
    1.85 -
    1.86 -axclass
    1.87 -  power < term
    1.88 +axclass plus < "term"
    1.89 +axclass minus < "term"
    1.90 +axclass times < "term"
    1.91 +axclass power < "term"
    1.92  
    1.93  consts
    1.94 -  "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
    1.95 -  "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    1.96 -  uminus        :: ['a::minus] => 'a                ("- _" [81] 80)
    1.97 -  "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.98 +  "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    1.99 +  -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   1.100 +  uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
   1.101 +  "*"           :: "['a::times, 'a] => 'a"          (infixl 70)
   1.102    (*See Nat.thy for "^"*)
   1.103  
   1.104  
   1.105 @@ -83,22 +74,22 @@
   1.106    case_syn  cases_syn
   1.107  
   1.108  syntax
   1.109 -  "~="          :: ['a, 'a] => bool                 (infixl 50)
   1.110 -  "_Eps"        :: [pttrn, bool] => 'a              ("(3SOME _./ _)" [0, 10] 10)
   1.111 +  ~=            :: "['a, 'a] => bool"                    (infixl 50)
   1.112 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3SOME _./ _)" [0, 10] 10)
   1.113  
   1.114    (* Let expressions *)
   1.115  
   1.116 -  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
   1.117 -  ""            :: letbind => letbinds              ("_")
   1.118 -  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
   1.119 -  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
   1.120 +  "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
   1.121 +  ""            :: "letbind => letbinds"                 ("_")
   1.122 +  "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
   1.123 +  "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" 10)
   1.124  
   1.125    (* Case expressions *)
   1.126  
   1.127 -  "@case"       :: ['a, cases_syn] => 'b            ("(case _ of/ _)" 10)
   1.128 -  "@case1"      :: ['a, 'b] => case_syn             ("(2_ =>/ _)" 10)
   1.129 -  ""            :: case_syn => cases_syn            ("_")
   1.130 -  "@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ | _")
   1.131 +  "@case"       :: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
   1.132 +  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
   1.133 +  ""            :: "case_syn => cases_syn"               ("_")
   1.134 +  "@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
   1.135  
   1.136  translations
   1.137    "x ~= y"                == "~ (x = y)"
   1.138 @@ -107,37 +98,37 @@
   1.139    "let x = a in e"        == "Let a (%x. e)"
   1.140  
   1.141  syntax ("" output)
   1.142 -  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
   1.143 -  "op ~="       :: ['a, 'a] => bool                 ("(_ ~=/ _)" [51, 51] 50)
   1.144 +  "op ="        :: "['a, 'a] => bool"                    ("(_ =/ _)" [51, 51] 50)
   1.145 +  "op ~="       :: "['a, 'a] => bool"                    ("(_ ~=/ _)" [51, 51] 50)
   1.146  
   1.147  syntax (symbols)
   1.148 -  Not           :: bool => bool                     ("\\<not> _" [40] 40)
   1.149 -  "op &"        :: [bool, bool] => bool             (infixr "\\<and>" 35)
   1.150 -  "op |"        :: [bool, bool] => bool             (infixr "\\<or>" 30)
   1.151 -  "op -->"      :: [bool, bool] => bool             (infixr "\\<midarrow>\\<rightarrow>" 25)
   1.152 -  "op o"        :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl "\\<circ>" 55)
   1.153 -  "op ~="       :: ['a, 'a] => bool                 (infixl "\\<noteq>" 50)
   1.154 -  "_Eps"        :: [pttrn, bool] => 'a              ("(3\\<epsilon>_./ _)" [0, 10] 10)
   1.155 -  "ALL "        :: [idts, bool] => bool             ("(3\\<forall>_./ _)" [0, 10] 10)
   1.156 -  "EX "         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
   1.157 -  "EX! "        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
   1.158 -  "@case1"      :: ['a, 'b] => case_syn             ("(2_ \\<Rightarrow>/ _)" 10)
   1.159 -(*"@case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ \\<orelse> _")*)
   1.160 +  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
   1.161 +  "op &"        :: "[bool, bool] => bool"                (infixr "\\<and>" 35)
   1.162 +  "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
   1.163 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
   1.164 +  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
   1.165 +  "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
   1.166 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
   1.167 +  "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
   1.168 +  "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
   1.169 +  "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
   1.170 +  "@case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
   1.171 +(*"@case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
   1.172  
   1.173  syntax (symbols output)
   1.174 -  "op ~="       :: ['a, 'a] => bool                 ("(_ \\<noteq>/ _)" [51, 51] 50)
   1.175 +  "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)
   1.176  
   1.177  syntax (xsymbols)
   1.178 -  "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
   1.179 +  "op -->"      :: "[bool, bool] => bool"                (infixr "\\<longrightarrow>" 25)
   1.180  
   1.181  syntax (HTML output)
   1.182 -  Not           :: bool => bool                     ("\\<not> _" [40] 40)
   1.183 +  Not           :: "bool => bool"                        ("\\<not> _" [40] 40)
   1.184  
   1.185  syntax (HOL)
   1.186 -  "_Eps"        :: [pttrn, bool] => 'a              ("(3@ _./ _)" [0, 10] 10)
   1.187 -  "ALL "        :: [idts, bool] => bool             ("(3! _./ _)" [0, 10] 10)
   1.188 -  "EX "         :: [idts, bool] => bool             ("(3? _./ _)" [0, 10] 10)
   1.189 -  "EX! "        :: [idts, bool] => bool             ("(3?! _./ _)" [0, 10] 10)
   1.190 +  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3@ _./ _)" [0, 10] 10)
   1.191 +  "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
   1.192 +  "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
   1.193 +  "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)
   1.194  
   1.195  
   1.196  
   1.197 @@ -145,57 +136,59 @@
   1.198  
   1.199  local
   1.200  
   1.201 -rules
   1.202 +axioms
   1.203  
   1.204 -  eq_reflection "(x=y) ==> (x==y)"
   1.205 +  eq_reflection: "(x=y) ==> (x==y)"
   1.206  
   1.207    (* Basic Rules *)
   1.208  
   1.209 -  refl          "t = (t::'a)"
   1.210 -  subst         "[| s = t; P(s) |] ==> P(t::'a)"
   1.211 +  refl:         "t = (t::'a)"
   1.212 +  subst:        "[| s = t; P(s) |] ==> P(t::'a)"
   1.213  
   1.214    (*Extensionality is built into the meta-logic, and this rule expresses
   1.215      a related property.  It is an eta-expanded version of the traditional
   1.216      rule, and similar to the ABS rule of HOL.*)
   1.217 -  ext           "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
   1.218 +  ext:          "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
   1.219  
   1.220 -  selectI       "P (x::'a) ==> P (@x. P x)"
   1.221 +  selectI:      "P (x::'a) ==> P (@x. P x)"
   1.222  
   1.223 -  impI          "(P ==> Q) ==> P-->Q"
   1.224 -  mp            "[| P-->Q;  P |] ==> Q"
   1.225 +  impI:         "(P ==> Q) ==> P-->Q"
   1.226 +  mp:           "[| P-->Q;  P |] ==> Q"
   1.227  
   1.228  defs
   1.229  
   1.230 -  True_def      "True      == ((%x::bool. x) = (%x. x))"
   1.231 -  All_def       "All(P)    == (P = (%x. True))"
   1.232 -  Ex_def        "Ex(P)     == P(@x. P(x))"
   1.233 -  False_def     "False     == (!P. P)"
   1.234 -  not_def       "~ P       == P-->False"
   1.235 -  and_def       "P & Q     == !R. (P-->Q-->R) --> R"
   1.236 -  or_def        "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
   1.237 -  Ex1_def       "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"
   1.238 +  True_def:     "True      == ((%x::bool. x) = (%x. x))"
   1.239 +  All_def:      "All(P)    == (P = (%x. True))"
   1.240 +  Ex_def:       "Ex(P)     == P(@x. P(x))"
   1.241 +  False_def:    "False     == (!P. P)"
   1.242 +  not_def:      "~ P       == P-->False"
   1.243 +  and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
   1.244 +  or_def:       "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
   1.245 +  Ex1_def:      "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"
   1.246  
   1.247 -rules
   1.248 +axioms
   1.249    (* Axioms *)
   1.250  
   1.251 -  iff           "(P-->Q) --> (Q-->P) --> (P=Q)"
   1.252 -  True_or_False "(P=True) | (P=False)"
   1.253 +  iff:          "(P-->Q) --> (Q-->P) --> (P=Q)"
   1.254 +  True_or_False:  "(P=True) | (P=False)"
   1.255  
   1.256  defs
   1.257    (*misc definitions*)
   1.258 -  Let_def       "Let s f == f(s)"
   1.259 -  if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   1.260 +  Let_def:      "Let s f == f(s)"
   1.261 +  if_def:       "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
   1.262  
   1.263    (*arbitrary is completely unspecified, but is made to appear as a
   1.264      definition syntactically*)
   1.265 -  arbitrary_def "False ==> arbitrary == (@x. False)"
   1.266 +  arbitrary_def:  "False ==> arbitrary == (@x. False)"
   1.267  
   1.268  
   1.269  
   1.270 -(** initial HOL theory setup **)
   1.271 +(* theory and package setup *)
   1.272  
   1.273 -setup Simplifier.setup
   1.274 -setup ClasetThyData.setup
   1.275 +use "HOL_lemmas.ML"	setup attrib_setup
   1.276 +use "cladata.ML"	setup Classical.setup setup clasetup
   1.277 +use "blastdata.ML"	setup Blast.setup
   1.278 +use "simpdata.ML"	setup Simplifier.setup setup simpsetup setup Clasimp.setup
   1.279  
   1.280  
   1.281  end