src/FOL/IFOL.thy
 author clasohm Thu, 17 Mar 1994 11:24:31 +0100 changeset 278 523518f44286 parent 79 74e68ed3b4fd child 928 cb31a4e97f75 permissions -rw-r--r--
adapted type definition to new syntax
```
(*  Title:      FOL/ifol.thy
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright   1993  University of Cambridge

Intuitionistic first-order logic
*)

IFOL = Pure +

classes
term < logic

default
term

types
o

arities
o :: logic

consts

Trueprop      :: "o => prop"                  ("(_)" 5)
True, False   :: "o"

(* Connectives *)

"="           :: "['a, 'a] => o"              (infixl 50)
"~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)

Not           :: "o => o"                     ("~ _" [40] 40)
"&"           :: "[o, o] => o"                (infixr 35)
"|"           :: "[o, o] => o"                (infixr 30)
"-->"         :: "[o, o] => o"                (infixr 25)
"<->"         :: "[o, o] => o"                (infixr 25)

(* Quantifiers *)

All           :: "('a => o) => o"             (binder "ALL " 10)
Ex            :: "('a => o) => o"             (binder "EX " 10)
Ex1           :: "('a => o) => o"             (binder "EX! " 10)

translations
"x ~= y"      == "~ (x = y)"

rules

(* Equality *)

refl          "a=a"
subst         "[| a=b;  P(a) |] ==> P(b)"

(* Propositional logic *)

conjI         "[| P;  Q |] ==> P&Q"
conjunct1     "P&Q ==> P"
conjunct2     "P&Q ==> Q"

disjI1        "P ==> P|Q"
disjI2        "Q ==> P|Q"
disjE         "[| P|Q;  P ==> R;  Q ==> R |] ==> R"

impI          "(P ==> Q) ==> P-->Q"
mp            "[| P-->Q;  P |] ==> Q"

FalseE        "False ==> P"

(* Definitions *)

True_def      "True  == False-->False"
not_def       "~P    == P-->False"
iff_def       "P<->Q == (P-->Q) & (Q-->P)"

(* Unique existence *)

ex1_def       "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"

(* Quantifiers *)

allI          "(!!x. P(x)) ==> (ALL x.P(x))"
spec          "(ALL x.P(x)) ==> P(x)"

exI           "P(x) ==> (EX x.P(x))"
exE           "[| EX x.P(x);  !!x. P(x) ==> R |] ==> R"

(* Reflection *)

eq_reflection   "(x=y)   ==> (x==y)"
iff_reflection  "(P<->Q) ==> (P==Q)"

end

```