1 (* Title: FOL/ifol.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Intuitionistic first-order logic |
|
7 *) |
|
8 |
|
9 IFOL = Pure + |
|
10 |
|
11 classes |
|
12 term < logic |
|
13 |
|
14 default |
|
15 term |
|
16 |
|
17 types |
|
18 o |
|
19 |
|
20 arities |
|
21 o :: logic |
|
22 |
|
23 |
|
24 consts |
|
25 |
|
26 Trueprop :: "o => prop" ("(_)" 5) |
|
27 True, False :: "o" |
|
28 |
|
29 (* Connectives *) |
|
30 |
|
31 "=" :: "['a, 'a] => o" (infixl 50) |
|
32 "~=" :: "['a, 'a] => o" ("(_ ~=/ _)" [50, 51] 50) |
|
33 |
|
34 Not :: "o => o" ("~ _" [40] 40) |
|
35 "&" :: "[o, o] => o" (infixr 35) |
|
36 "|" :: "[o, o] => o" (infixr 30) |
|
37 "-->" :: "[o, o] => o" (infixr 25) |
|
38 "<->" :: "[o, o] => o" (infixr 25) |
|
39 |
|
40 (* Quantifiers *) |
|
41 |
|
42 All :: "('a => o) => o" (binder "ALL " 10) |
|
43 Ex :: "('a => o) => o" (binder "EX " 10) |
|
44 Ex1 :: "('a => o) => o" (binder "EX! " 10) |
|
45 |
|
46 |
|
47 translations |
|
48 "x ~= y" == "~ (x = y)" |
|
49 |
|
50 |
|
51 rules |
|
52 |
|
53 (* Equality *) |
|
54 |
|
55 refl "a=a" |
|
56 subst "[| a=b; P(a) |] ==> P(b)" |
|
57 |
|
58 (* Propositional logic *) |
|
59 |
|
60 conjI "[| P; Q |] ==> P&Q" |
|
61 conjunct1 "P&Q ==> P" |
|
62 conjunct2 "P&Q ==> Q" |
|
63 |
|
64 disjI1 "P ==> P|Q" |
|
65 disjI2 "Q ==> P|Q" |
|
66 disjE "[| P|Q; P ==> R; Q ==> R |] ==> R" |
|
67 |
|
68 impI "(P ==> Q) ==> P-->Q" |
|
69 mp "[| P-->Q; P |] ==> Q" |
|
70 |
|
71 FalseE "False ==> P" |
|
72 |
|
73 (* Definitions *) |
|
74 |
|
75 True_def "True == False-->False" |
|
76 not_def "~P == P-->False" |
|
77 iff_def "P<->Q == (P-->Q) & (Q-->P)" |
|
78 |
|
79 (* Unique existence *) |
|
80 |
|
81 ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
|
82 |
|
83 (* Quantifiers *) |
|
84 |
|
85 allI "(!!x. P(x)) ==> (ALL x.P(x))" |
|
86 spec "(ALL x.P(x)) ==> P(x)" |
|
87 |
|
88 exI "P(x) ==> (EX x.P(x))" |
|
89 exE "[| EX x.P(x); !!x. P(x) ==> R |] ==> R" |
|
90 |
|
91 (* Reflection *) |
|
92 |
|
93 eq_reflection "(x=y) ==> (x==y)" |
|
94 iff_reflection "(P<->Q) ==> (P==Q)" |
|
95 |
|
96 end |
|
97 |
|