ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
changes
epsilon,arith: many changes
ordinal/succ_mem_succI/E: deleted; use succ_leI/E
nat/nat_0_in_succ: deleted; use nat_0_le
univ/Vset_rankI: deleted; use VsetI
IFOL = Pure +
classes term < logic
default term
types o 0
arities o :: logic
consts
Trueprop :: "o => prop" ("(_)" [0] 5)
True,False :: "o"
(*Connectives*)
"=" :: "['a,'a] => o" (infixl 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)
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