src/HOL/HOL.thy
author nipkow
Tue May 09 22:10:08 1995 +0200 (1995-05-09)
changeset 1114 c8dfb56a7e95
parent 1068 e0f2dffab506
child 1232 454eb424c223
permissions -rw-r--r--
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
clasohm@923
     1
(*  Title:      HOL/HOL.thy
clasohm@923
     2
    ID:         $Id$
clasohm@923
     3
    Author:     Tobias Nipkow
clasohm@923
     4
    Copyright   1993  University of Cambridge
clasohm@923
     5
clasohm@923
     6
Higher-Order Logic
clasohm@923
     7
*)
clasohm@923
     8
clasohm@923
     9
HOL = CPure +
clasohm@923
    10
clasohm@923
    11
classes
clasohm@923
    12
  term < logic
clasohm@923
    13
clasohm@923
    14
axclass
clasohm@923
    15
  plus < term
clasohm@923
    16
clasohm@923
    17
axclass
clasohm@923
    18
  minus < term
clasohm@923
    19
clasohm@923
    20
axclass
clasohm@923
    21
  times < term
clasohm@923
    22
clasohm@923
    23
default
clasohm@923
    24
  term
clasohm@923
    25
clasohm@923
    26
types
clasohm@923
    27
  bool
clasohm@923
    28
clasohm@923
    29
arities
clasohm@923
    30
  fun :: (term, term) term
clasohm@923
    31
  bool :: term
clasohm@923
    32
clasohm@923
    33
clasohm@923
    34
consts
clasohm@923
    35
clasohm@923
    36
  (* Constants *)
clasohm@923
    37
clasohm@923
    38
  Trueprop      :: "bool => prop"                     ("(_)" 5)
clasohm@923
    39
  not           :: "bool => bool"                     ("~ _" [40] 40)
clasohm@923
    40
  True, False   :: "bool"
clasohm@965
    41
  If            :: "[bool, 'a, 'a] => 'a"   ("(if (_)/ then (_)/ else (_))" 10)
clasohm@923
    42
  Inv           :: "('a => 'b) => ('b => 'a)"
clasohm@923
    43
clasohm@923
    44
  (* Binders *)
clasohm@923
    45
nipkow@1068
    46
  Eps           :: "('a => bool) => 'a"
clasohm@923
    47
  All           :: "('a => bool) => bool"             (binder "! " 10)
clasohm@923
    48
  Ex            :: "('a => bool) => bool"             (binder "? " 10)
clasohm@923
    49
  Ex1           :: "('a => bool) => bool"             (binder "?! " 10)
clasohm@923
    50
  Let           :: "['a, 'a => 'b] => 'b"
clasohm@923
    51
clasohm@923
    52
  (* Infixes *)
clasohm@923
    53
clasohm@923
    54
  o             :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixr 50)
clasohm@923
    55
  "="           :: "['a, 'a] => bool"                 (infixl 50)
clasohm@923
    56
  "&"           :: "[bool, bool] => bool"             (infixr 35)
clasohm@923
    57
  "|"           :: "[bool, bool] => bool"             (infixr 30)
clasohm@923
    58
  "-->"         :: "[bool, bool] => bool"             (infixr 25)
clasohm@923
    59
clasohm@923
    60
  (* Overloaded Constants *)
clasohm@923
    61
clasohm@923
    62
  "+"           :: "['a::plus, 'a] => 'a"             (infixl 65)
clasohm@923
    63
  "-"           :: "['a::minus, 'a] => 'a"            (infixl 65)
clasohm@923
    64
  "*"           :: "['a::times, 'a] => 'a"            (infixl 70)
clasohm@923
    65
clasohm@923
    66
clasohm@923
    67
types
clasohm@923
    68
  letbinds  letbind
clasohm@923
    69
  case_syn  cases_syn
clasohm@923
    70
clasohm@923
    71
syntax
clasohm@923
    72
clasohm@923
    73
  "~="          :: "['a, 'a] => bool"                 (infixl 50)
clasohm@923
    74
nipkow@1068
    75
  "@Eps"        :: "[pttrn,bool] => 'a"               ("(3@ _./ _)" 10)
nipkow@1068
    76
clasohm@923
    77
  (* Alternative Quantifiers *)
clasohm@923
    78
clasohm@923
    79
  "*All"        :: "[idts, bool] => bool"             ("(3ALL _./ _)" 10)
clasohm@923
    80
  "*Ex"         :: "[idts, bool] => bool"             ("(3EX _./ _)" 10)
clasohm@923
    81
  "*Ex1"        :: "[idts, bool] => bool"             ("(3EX! _./ _)" 10)
clasohm@923
    82
clasohm@923
    83
  (* Let expressions *)
clasohm@923
    84
nipkow@1068
    85
  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
clasohm@923
    86
  ""            :: "letbind => letbinds"              ("_")
clasohm@923
    87
  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
clasohm@923
    88
  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
clasohm@923
    89
clasohm@923
    90
  (* Case expressions *)
clasohm@923
    91
clasohm@923
    92
  "@case"       :: "['a, cases_syn] => 'b"            ("(case _ of/ _)" 10)
clasohm@923
    93
  "@case1"      :: "['a, 'b] => case_syn"             ("(2_ =>/ _)" 10)
clasohm@923
    94
  ""            :: "case_syn => cases_syn"            ("_")
clasohm@923
    95
  "@case2"      :: "[case_syn, cases_syn] => cases_syn"   ("_/ | _")
clasohm@923
    96
clasohm@923
    97
translations
clasohm@923
    98
  "x ~= y"      == "~ (x = y)"
nipkow@1068
    99
  "@ x.b"       == "Eps(%x.b)"
clasohm@923
   100
  "ALL xs. P"   => "! xs. P"
clasohm@923
   101
  "EX xs. P"    => "? xs. P"
clasohm@923
   102
  "EX! xs. P"   => "?! xs. P"
clasohm@923
   103
  "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
nipkow@1114
   104
  "let x = a in e"        == "Let a (%x. e)"
clasohm@923
   105
clasohm@923
   106
rules
clasohm@923
   107
clasohm@923
   108
  eq_reflection "(x=y) ==> (x==y)"
clasohm@923
   109
clasohm@923
   110
  (* Basic Rules *)
clasohm@923
   111
clasohm@923
   112
  refl          "t = (t::'a)"
clasohm@923
   113
  subst         "[| s = t; P(s) |] ==> P(t::'a)"
clasohm@923
   114
  ext           "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
clasohm@923
   115
  selectI       "P(x::'a) ==> P(@x.P(x))"
clasohm@923
   116
clasohm@923
   117
  impI          "(P ==> Q) ==> P-->Q"
clasohm@923
   118
  mp            "[| P-->Q;  P |] ==> Q"
clasohm@923
   119
clasohm@923
   120
defs
clasohm@923
   121
clasohm@923
   122
  True_def      "True      == ((%x::bool.x)=(%x.x))"
clasohm@923
   123
  All_def       "All(P)    == (P = (%x.True))"
clasohm@923
   124
  Ex_def        "Ex(P)     == P(@x.P(x))"
clasohm@923
   125
  False_def     "False     == (!P.P)"
clasohm@923
   126
  not_def       "~ P       == P-->False"
clasohm@923
   127
  and_def       "P & Q     == !R. (P-->Q-->R) --> R"
clasohm@923
   128
  or_def        "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
clasohm@923
   129
  Ex1_def       "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"
clasohm@923
   130
clasohm@923
   131
rules
clasohm@923
   132
  (* Axioms *)
clasohm@923
   133
clasohm@923
   134
  iff           "(P-->Q) --> (Q-->P) --> (P=Q)"
clasohm@923
   135
  True_or_False "(P=True) | (P=False)"
clasohm@923
   136
clasohm@923
   137
defs
clasohm@923
   138
  (* Misc Definitions *)
clasohm@923
   139
clasohm@923
   140
  Let_def       "Let s f == f(s)"
clasohm@923
   141
  Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
clasohm@923
   142
  o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
nipkow@973
   143
  if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
clasohm@923
   144
clasohm@923
   145
end
clasohm@923
   146
clasohm@923
   147
clasohm@923
   148
ML
clasohm@923
   149
clasohm@923
   150
(** Choice between the HOL and Isabelle style of quantifiers **)
clasohm@923
   151
clasohm@923
   152
val HOL_quantifiers = ref true;
clasohm@923
   153
clasohm@923
   154
fun alt_ast_tr' (name, alt_name) =
clasohm@923
   155
  let
clasohm@923
   156
    fun ast_tr' (*name*) args =
clasohm@923
   157
      if ! HOL_quantifiers then raise Match
clasohm@923
   158
      else Syntax.mk_appl (Syntax.Constant alt_name) args;
clasohm@923
   159
  in
clasohm@923
   160
    (name, ast_tr')
clasohm@923
   161
  end;
clasohm@923
   162
clasohm@923
   163
clasohm@923
   164
val print_ast_translation =
clasohm@923
   165
  map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];