|
0
|
1 |
IFOL = Pure +
|
|
|
2 |
|
|
|
3 |
classes term < logic
|
|
|
4 |
|
|
|
5 |
default term
|
|
|
6 |
|
|
|
7 |
types o 0
|
|
|
8 |
|
|
|
9 |
arities o :: logic
|
|
|
10 |
|
|
|
11 |
consts
|
|
|
12 |
Trueprop :: "o => prop" ("(_)" [0] 5)
|
|
|
13 |
True,False :: "o"
|
|
|
14 |
(*Connectives*)
|
|
|
15 |
"=" :: "['a,'a] => o" (infixl 50)
|
|
|
16 |
Not :: "o => o" ("~ _" [40] 40)
|
|
|
17 |
"&" :: "[o,o] => o" (infixr 35)
|
|
|
18 |
"|" :: "[o,o] => o" (infixr 30)
|
|
|
19 |
"-->" :: "[o,o] => o" (infixr 25)
|
|
|
20 |
"<->" :: "[o,o] => o" (infixr 25)
|
|
|
21 |
(*Quantifiers*)
|
|
|
22 |
All :: "('a => o) => o" (binder "ALL " 10)
|
|
|
23 |
Ex :: "('a => o) => o" (binder "EX " 10)
|
|
|
24 |
Ex1 :: "('a => o) => o" (binder "EX! " 10)
|
|
|
25 |
|
|
|
26 |
rules
|
|
|
27 |
|
|
|
28 |
(*Equality*)
|
|
|
29 |
|
|
|
30 |
refl "a=a"
|
|
|
31 |
subst "[| a=b; P(a) |] ==> P(b)"
|
|
|
32 |
|
|
|
33 |
(*Propositional logic*)
|
|
|
34 |
|
|
|
35 |
conjI "[| P; Q |] ==> P&Q"
|
|
|
36 |
conjunct1 "P&Q ==> P"
|
|
|
37 |
conjunct2 "P&Q ==> Q"
|
|
|
38 |
|
|
|
39 |
disjI1 "P ==> P|Q"
|
|
|
40 |
disjI2 "Q ==> P|Q"
|
|
|
41 |
disjE "[| P|Q; P ==> R; Q ==> R |] ==> R"
|
|
|
42 |
|
|
|
43 |
impI "(P ==> Q) ==> P-->Q"
|
|
|
44 |
mp "[| P-->Q; P |] ==> Q"
|
|
|
45 |
|
|
|
46 |
FalseE "False ==> P"
|
|
|
47 |
|
|
|
48 |
(*Definitions*)
|
|
|
49 |
|
|
|
50 |
True_def "True == False-->False"
|
|
|
51 |
not_def "~P == P-->False"
|
|
|
52 |
iff_def "P<->Q == (P-->Q) & (Q-->P)"
|
|
|
53 |
|
|
|
54 |
(*Unique existence*)
|
|
|
55 |
ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
|
|
|
56 |
|
|
|
57 |
(*Quantifiers*)
|
|
|
58 |
|
|
|
59 |
allI "(!!x. P(x)) ==> (ALL x.P(x))"
|
|
|
60 |
spec "(ALL x.P(x)) ==> P(x)"
|
|
|
61 |
|
|
|
62 |
exI "P(x) ==> (EX x.P(x))"
|
|
|
63 |
exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R"
|
|
|
64 |
|
|
|
65 |
(* Reflection *)
|
|
|
66 |
|
|
|
67 |
eq_reflection "(x=y) ==> (x==y)"
|
|
|
68 |
iff_reflection "(P<->Q) ==> (P==Q)"
|
|
|
69 |
|
|
|
70 |
end
|