src/FOL/IFOL.thy
author clasohm
Thu Oct 05 14:45:54 1995 +0100 (1995-10-05)
changeset 1268 f6ef556b3ede
parent 928 cb31a4e97f75
child 1322 9b3d3362a048
permissions -rw-r--r--
corrected title
     1 (*  Title:      FOL/IFOL.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 Intuitionistic first-order logic
     7 *)
     8 
     9 IFOL = Pure +
    10 
    11 classes
    12   term < logic
    13 
    14 default
    15   term
    16 
    17 types
    18   o
    19 
    20 arities
    21   o :: logic
    22 
    23 
    24 consts
    25 
    26   Trueprop      :: "o => prop"                  ("(_)" 5)
    27   True, False   :: "o"
    28 
    29   (* Connectives *)
    30 
    31   "="           :: "['a, 'a] => o"              (infixl 50)
    32 
    33   Not           :: "o => o"                     ("~ _" [40] 40)
    34   "&"           :: "[o, o] => o"                (infixr 35)
    35   "|"           :: "[o, o] => o"                (infixr 30)
    36   "-->"         :: "[o, o] => o"                (infixr 25)
    37   "<->"         :: "[o, o] => o"                (infixr 25)
    38 
    39   (* Quantifiers *)
    40 
    41   All           :: "('a => o) => o"             (binder "ALL " 10)
    42   Ex            :: "('a => o) => o"             (binder "EX " 10)
    43   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    44 
    45 
    46 syntax
    47   "~="          :: "['a, 'a] => o"              (infixl 50)
    48 
    49 translations
    50   "x ~= y"      == "~ (x = y)"
    51 
    52 
    53 rules
    54 
    55   (* Equality *)
    56 
    57   refl          "a=a"
    58   subst         "[| a=b;  P(a) |] ==> P(b)"
    59 
    60   (* Propositional logic *)
    61 
    62   conjI         "[| P;  Q |] ==> P&Q"
    63   conjunct1     "P&Q ==> P"
    64   conjunct2     "P&Q ==> Q"
    65 
    66   disjI1        "P ==> P|Q"
    67   disjI2        "Q ==> P|Q"
    68   disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    69 
    70   impI          "(P ==> Q) ==> P-->Q"
    71   mp            "[| P-->Q;  P |] ==> Q"
    72 
    73   FalseE        "False ==> P"
    74 
    75   (* Definitions *)
    76 
    77   True_def      "True  == False-->False"
    78   not_def       "~P    == P-->False"
    79   iff_def       "P<->Q == (P-->Q) & (Q-->P)"
    80 
    81   (* Unique existence *)
    82 
    83   ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    84 
    85   (* Quantifiers *)
    86 
    87   allI          "(!!x. P(x)) ==> (ALL x.P(x))"
    88   spec          "(ALL x.P(x)) ==> P(x)"
    89 
    90   exI           "P(x) ==> (EX x.P(x))"
    91   exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
    92 
    93   (* Reflection *)
    94 
    95   eq_reflection   "(x=y)   ==> (x==y)"
    96   iff_reflection  "(P<->Q) ==> (P==Q)"
    97 
    98 end
    99