|
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 |