src/FOL/IFOL.thy
author clasohm
Thu Mar 17 11:24:31 1994 +0100 (1994-03-17)
changeset 278 523518f44286
parent 79 74e68ed3b4fd
child 928 cb31a4e97f75
permissions -rw-r--r--
adapted type definition to new syntax
     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   "~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)
    33 
    34   Not           :: "o => o"                     ("~ _" [40] 40)
    35   "&"           :: "[o, o] => o"                (infixr 35)
    36   "|"           :: "[o, o] => o"                (infixr 30)
    37   "-->"         :: "[o, o] => o"                (infixr 25)
    38   "<->"         :: "[o, o] => o"                (infixr 25)
    39 
    40   (* Quantifiers *)
    41 
    42   All           :: "('a => o) => o"             (binder "ALL " 10)
    43   Ex            :: "('a => o) => o"             (binder "EX " 10)
    44   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    45 
    46 
    47 translations
    48   "x ~= y"      == "~ (x = y)"
    49 
    50 
    51 rules
    52 
    53   (* Equality *)
    54 
    55   refl          "a=a"
    56   subst         "[| a=b;  P(a) |] ==> P(b)"
    57 
    58   (* Propositional logic *)
    59 
    60   conjI         "[| P;  Q |] ==> P&Q"
    61   conjunct1     "P&Q ==> P"
    62   conjunct2     "P&Q ==> Q"
    63 
    64   disjI1        "P ==> P|Q"
    65   disjI2        "Q ==> P|Q"
    66   disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    67 
    68   impI          "(P ==> Q) ==> P-->Q"
    69   mp            "[| P-->Q;  P |] ==> Q"
    70 
    71   FalseE        "False ==> P"
    72 
    73   (* Definitions *)
    74 
    75   True_def      "True  == False-->False"
    76   not_def       "~P    == P-->False"
    77   iff_def       "P<->Q == (P-->Q) & (Q-->P)"
    78 
    79   (* Unique existence *)
    80 
    81   ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    82 
    83   (* Quantifiers *)
    84 
    85   allI          "(!!x. P(x)) ==> (ALL x.P(x))"
    86   spec          "(ALL x.P(x)) ==> P(x)"
    87 
    88   exI           "P(x) ==> (EX x.P(x))"
    89   exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"
    90 
    91   (* Reflection *)
    92 
    93   eq_reflection   "(x=y)   ==> (x==y)"
    94   iff_reflection  "(P<->Q) ==> (P==Q)"
    95 
    96 end
    97