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