1268
|
1 |
(* Title: FOL/IFOL.thy
|
35
|
2 |
ID: $Id$
|
79
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
35
|
4 |
Copyright 1993 University of Cambridge
|
|
5 |
|
2205
|
6 |
Intuitionistic first-order logic.
|
35
|
7 |
*)
|
|
8 |
|
79
|
9 |
IFOL = Pure +
|
0
|
10 |
|
3906
|
11 |
global
|
|
12 |
|
79
|
13 |
classes
|
|
14 |
term < logic
|
|
15 |
|
|
16 |
default
|
|
17 |
term
|
0
|
18 |
|
79
|
19 |
types
|
278
|
20 |
o
|
0
|
21 |
|
79
|
22 |
arities
|
|
23 |
o :: logic
|
0
|
24 |
|
79
|
25 |
|
|
26 |
consts
|
0
|
27 |
|
1322
|
28 |
Trueprop :: o => prop ("(_)" 5)
|
|
29 |
True, False :: o
|
79
|
30 |
|
|
31 |
(* Connectives *)
|
|
32 |
|
1322
|
33 |
"=" :: ['a, 'a] => o (infixl 50)
|
35
|
34 |
|
1322
|
35 |
Not :: o => o ("~ _" [40] 40)
|
|
36 |
"&" :: [o, o] => o (infixr 35)
|
|
37 |
"|" :: [o, o] => o (infixr 30)
|
|
38 |
"-->" :: [o, o] => o (infixr 25)
|
|
39 |
"<->" :: [o, o] => o (infixr 25)
|
79
|
40 |
|
|
41 |
(* Quantifiers *)
|
|
42 |
|
1322
|
43 |
All :: ('a => o) => o (binder "ALL " 10)
|
|
44 |
Ex :: ('a => o) => o (binder "EX " 10)
|
|
45 |
Ex1 :: ('a => o) => o (binder "EX! " 10)
|
79
|
46 |
|
0
|
47 |
|
2257
|
48 |
|
928
|
49 |
syntax
|
1322
|
50 |
"~=" :: ['a, 'a] => o (infixl 50)
|
928
|
51 |
|
35
|
52 |
translations
|
79
|
53 |
"x ~= y" == "~ (x = y)"
|
|
54 |
|
2257
|
55 |
syntax (symbols)
|
|
56 |
Not :: o => o ("\\<not> _" [40] 40)
|
|
57 |
"op &" :: [o, o] => o (infixr "\\<and>" 35)
|
|
58 |
"op |" :: [o, o] => o (infixr "\\<or>" 30)
|
|
59 |
"op -->" :: [o, o] => o (infixr "\\<midarrow>\\<rightarrow>" 25)
|
|
60 |
"op <->" :: [o, o] => o (infixr "\\<leftarrow>\\<rightarrow>" 25)
|
2367
|
61 |
"ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)
|
|
62 |
"EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)
|
|
63 |
"EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)
|
2257
|
64 |
"op ~=" :: ['a, 'a] => o (infixl "\\<noteq>" 50)
|
2205
|
65 |
|
35
|
66 |
|
3932
|
67 |
local
|
3906
|
68 |
|
0
|
69 |
rules
|
|
70 |
|
79
|
71 |
(* Equality *)
|
0
|
72 |
|
79
|
73 |
refl "a=a"
|
|
74 |
subst "[| a=b; P(a) |] ==> P(b)"
|
0
|
75 |
|
79
|
76 |
(* Propositional logic *)
|
0
|
77 |
|
79
|
78 |
conjI "[| P; Q |] ==> P&Q"
|
|
79 |
conjunct1 "P&Q ==> P"
|
|
80 |
conjunct2 "P&Q ==> Q"
|
0
|
81 |
|
79
|
82 |
disjI1 "P ==> P|Q"
|
|
83 |
disjI2 "Q ==> P|Q"
|
|
84 |
disjE "[| P|Q; P ==> R; Q ==> R |] ==> R"
|
0
|
85 |
|
79
|
86 |
impI "(P ==> Q) ==> P-->Q"
|
|
87 |
mp "[| P-->Q; P |] ==> Q"
|
0
|
88 |
|
79
|
89 |
FalseE "False ==> P"
|
0
|
90 |
|
79
|
91 |
(* Definitions *)
|
0
|
92 |
|
79
|
93 |
True_def "True == False-->False"
|
|
94 |
not_def "~P == P-->False"
|
|
95 |
iff_def "P<->Q == (P-->Q) & (Q-->P)"
|
|
96 |
|
|
97 |
(* Unique existence *)
|
0
|
98 |
|
79
|
99 |
ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
|
0
|
100 |
|
79
|
101 |
(* Quantifiers *)
|
0
|
102 |
|
3835
|
103 |
allI "(!!x. P(x)) ==> (ALL x. P(x))"
|
|
104 |
spec "(ALL x. P(x)) ==> P(x)"
|
0
|
105 |
|
3835
|
106 |
exI "P(x) ==> (EX x. P(x))"
|
|
107 |
exE "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
|
0
|
108 |
|
|
109 |
(* Reflection *)
|
|
110 |
|
79
|
111 |
eq_reflection "(x=y) ==> (x==y)"
|
|
112 |
iff_reflection "(P<->Q) ==> (P==Q)"
|
0
|
113 |
|
4092
|
114 |
|
4854
|
115 |
setup
|
|
116 |
Simplifier.setup
|
4092
|
117 |
|
4854
|
118 |
end
|