Installation of new simplfier. Previously appeared to set up the old
simplifier to rewrite with the partial ordering [=, something not possible
with the new simplifier. But such rewriting appears not to have actually
been used, and there were few complications. In terms.ML setloop was used
to avoid infinite rewriting with the letrec rule. Congruence rules were
deleted, and an occasional SIMP_TAC had to become asm_simp_tac.
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