src/FOL/IFOL.thy
author wenzelm
Wed Nov 27 16:42:48 1996 +0100 (1996-11-27)
changeset 2257 c8154379738c
parent 2205 c5a7c72746ac
child 2367 eba760ebe315
permissions -rw-r--r--
symbol names changes;
     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 
    47 syntax
    48   "~="          :: ['a, 'a] => o                (infixl 50)
    49 
    50 translations
    51   "x ~= y"      == "~ (x = y)"
    52 
    53 syntax (symbols)
    54   Not           :: o => o                       ("\\<not> _" [40] 40)
    55   "op &"        :: [o, o] => o                  (infixr "\\<and>" 35)
    56   "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
    57   "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
    58   "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
    59   "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" 10)
    60   "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" 10)
    61   "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" 10)
    62   "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
    63 
    64 
    65 rules
    66 
    67   (* Equality *)
    68 
    69   refl          "a=a"
    70   subst         "[| a=b;  P(a) |] ==> P(b)"
    71 
    72   (* Propositional logic *)
    73 
    74   conjI         "[| P;  Q |] ==> P&Q"
    75   conjunct1     "P&Q ==> P"
    76   conjunct2     "P&Q ==> Q"
    77 
    78   disjI1        "P ==> P|Q"
    79   disjI2        "Q ==> P|Q"
    80   disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    81 
    82   impI          "(P ==> Q) ==> P-->Q"
    83   mp            "[| P-->Q;  P |] ==> Q"
    84 
    85   FalseE        "False ==> P"
    86 
    87   (* Definitions *)
    88 
    89   True_def      "True  == False-->False"
    90   not_def       "~P    == P-->False"
    91   iff_def       "P<->Q == (P-->Q) & (Q-->P)"
    92 
    93   (* Unique existence *)
    94 
    95   ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    96 
    97   (* Quantifiers *)
    98 
    99   allI          "(!!x. P(x)) ==> (ALL x.P(x))"
   100   spec          "(ALL x.P(x)) ==> P(x)"
   101 
   102   exI           "P(x) ==> (EX x.P(x))"
   103   exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
   104 
   105   (* Reflection *)
   106 
   107   eq_reflection   "(x=y)   ==> (x==y)"
   108   iff_reflection  "(P<->Q) ==> (P==Q)"
   109 
   110 end
   111