src/FOL/IFOL.thy
author wenzelm
Wed Mar 10 10:55:12 1999 +0100 (1999-03-10)
changeset 6340 7d5cbd5819a0
parent 6027 9dd06eeda95c
child 7355 4c43090659ca
permissions -rw-r--r--
HTML output;
clasohm@1268
     1
(*  Title:      FOL/IFOL.thy
lcp@35
     2
    ID:         $Id$
wenzelm@79
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
lcp@35
     4
    Copyright   1993  University of Cambridge
lcp@35
     5
wenzelm@2205
     6
Intuitionistic first-order logic.
lcp@35
     7
*)
lcp@35
     8
wenzelm@79
     9
IFOL = Pure +
clasohm@0
    10
wenzelm@3906
    11
global
wenzelm@3906
    12
wenzelm@79
    13
classes
wenzelm@79
    14
  term < logic
wenzelm@79
    15
wenzelm@79
    16
default
wenzelm@79
    17
  term
clasohm@0
    18
wenzelm@79
    19
types
clasohm@278
    20
  o
clasohm@0
    21
wenzelm@79
    22
arities
wenzelm@79
    23
  o :: logic
clasohm@0
    24
wenzelm@79
    25
wenzelm@79
    26
consts
clasohm@0
    27
clasohm@1322
    28
  Trueprop      :: o => prop                    ("(_)" 5)
clasohm@1322
    29
  True, False   :: o
wenzelm@79
    30
wenzelm@79
    31
  (* Connectives *)
wenzelm@79
    32
clasohm@1322
    33
  "="           :: ['a, 'a] => o                (infixl 50)
lcp@35
    34
clasohm@1322
    35
  Not           :: o => o                       ("~ _" [40] 40)
clasohm@1322
    36
  "&"           :: [o, o] => o                  (infixr 35)
clasohm@1322
    37
  "|"           :: [o, o] => o                  (infixr 30)
clasohm@1322
    38
  "-->"         :: [o, o] => o                  (infixr 25)
clasohm@1322
    39
  "<->"         :: [o, o] => o                  (infixr 25)
wenzelm@79
    40
wenzelm@79
    41
  (* Quantifiers *)
wenzelm@79
    42
clasohm@1322
    43
  All           :: ('a => o) => o               (binder "ALL " 10)
clasohm@1322
    44
  Ex            :: ('a => o) => o               (binder "EX " 10)
clasohm@1322
    45
  Ex1           :: ('a => o) => o               (binder "EX! " 10)
wenzelm@79
    46
clasohm@0
    47
wenzelm@2257
    48
lcp@928
    49
syntax
clasohm@1322
    50
  "~="          :: ['a, 'a] => o                (infixl 50)
lcp@928
    51
lcp@35
    52
translations
wenzelm@79
    53
  "x ~= y"      == "~ (x = y)"
wenzelm@79
    54
wenzelm@2257
    55
syntax (symbols)
wenzelm@2257
    56
  Not           :: o => o                       ("\\<not> _" [40] 40)
wenzelm@2257
    57
  "op &"        :: [o, o] => o                  (infixr "\\<and>" 35)
wenzelm@2257
    58
  "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
wenzelm@2257
    59
  "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
wenzelm@2257
    60
  "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
wenzelm@2367
    61
  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" [0, 10] 10)
wenzelm@2367
    62
  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" [0, 10] 10)
wenzelm@2367
    63
  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
wenzelm@2257
    64
  "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
wenzelm@2205
    65
oheimb@6027
    66
syntax (xsymbols)
oheimb@6027
    67
  "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
oheimb@6027
    68
  "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
lcp@35
    69
wenzelm@6340
    70
syntax (HTML output)
wenzelm@6340
    71
  Not           :: o => o                       ("\\<not> _" [40] 40)
wenzelm@6340
    72
wenzelm@6340
    73
wenzelm@3932
    74
local
wenzelm@3906
    75
clasohm@0
    76
rules
clasohm@0
    77
wenzelm@79
    78
  (* Equality *)
clasohm@0
    79
wenzelm@79
    80
  refl          "a=a"
wenzelm@79
    81
  subst         "[| a=b;  P(a) |] ==> P(b)"
clasohm@0
    82
wenzelm@79
    83
  (* Propositional logic *)
clasohm@0
    84
wenzelm@79
    85
  conjI         "[| P;  Q |] ==> P&Q"
wenzelm@79
    86
  conjunct1     "P&Q ==> P"
wenzelm@79
    87
  conjunct2     "P&Q ==> Q"
clasohm@0
    88
wenzelm@79
    89
  disjI1        "P ==> P|Q"
wenzelm@79
    90
  disjI2        "Q ==> P|Q"
wenzelm@79
    91
  disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
clasohm@0
    92
wenzelm@79
    93
  impI          "(P ==> Q) ==> P-->Q"
wenzelm@79
    94
  mp            "[| P-->Q;  P |] ==> Q"
clasohm@0
    95
wenzelm@79
    96
  FalseE        "False ==> P"
clasohm@0
    97
wenzelm@79
    98
  (* Definitions *)
clasohm@0
    99
wenzelm@79
   100
  True_def      "True  == False-->False"
wenzelm@79
   101
  not_def       "~P    == P-->False"
wenzelm@79
   102
  iff_def       "P<->Q == (P-->Q) & (Q-->P)"
wenzelm@79
   103
wenzelm@79
   104
  (* Unique existence *)
clasohm@0
   105
wenzelm@79
   106
  ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
clasohm@0
   107
wenzelm@79
   108
  (* Quantifiers *)
clasohm@0
   109
wenzelm@3835
   110
  allI          "(!!x. P(x)) ==> (ALL x. P(x))"
wenzelm@3835
   111
  spec          "(ALL x. P(x)) ==> P(x)"
clasohm@0
   112
wenzelm@3835
   113
  exI           "P(x) ==> (EX x. P(x))"
wenzelm@3835
   114
  exE           "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
clasohm@0
   115
clasohm@0
   116
  (* Reflection *)
clasohm@0
   117
wenzelm@79
   118
  eq_reflection   "(x=y)   ==> (x==y)"
wenzelm@79
   119
  iff_reflection  "(P<->Q) ==> (P==Q)"
clasohm@0
   120
wenzelm@4092
   121
wenzelm@4854
   122
setup
wenzelm@4854
   123
  Simplifier.setup
wenzelm@4092
   124
wenzelm@4854
   125
end