author | wenzelm |
Wed, 10 Mar 1999 10:55:12 +0100 | |
changeset 6340 | 7d5cbd5819a0 |
parent 6027 | 9dd06eeda95c |
child 7355 | 4c43090659ca |
permissions | -rw-r--r-- |
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 |
|
6027
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
4854
diff
changeset
|
66 |
syntax (xsymbols) |
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
4854
diff
changeset
|
67 |
"op -->" :: [o, o] => o (infixr "\\<longrightarrow>" 25) |
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
4854
diff
changeset
|
68 |
"op <->" :: [o, o] => o (infixr "\\<longleftrightarrow>" 25) |
35 | 69 |
|
6340 | 70 |
syntax (HTML output) |
71 |
Not :: o => o ("\\<not> _" [40] 40) |
|
72 |
||
73 |
||
3932 | 74 |
local |
3906 | 75 |
|
0 | 76 |
rules |
77 |
||
79 | 78 |
(* Equality *) |
0 | 79 |
|
79 | 80 |
refl "a=a" |
81 |
subst "[| a=b; P(a) |] ==> P(b)" |
|
0 | 82 |
|
79 | 83 |
(* Propositional logic *) |
0 | 84 |
|
79 | 85 |
conjI "[| P; Q |] ==> P&Q" |
86 |
conjunct1 "P&Q ==> P" |
|
87 |
conjunct2 "P&Q ==> Q" |
|
0 | 88 |
|
79 | 89 |
disjI1 "P ==> P|Q" |
90 |
disjI2 "Q ==> P|Q" |
|
91 |
disjE "[| P|Q; P ==> R; Q ==> R |] ==> R" |
|
0 | 92 |
|
79 | 93 |
impI "(P ==> Q) ==> P-->Q" |
94 |
mp "[| P-->Q; P |] ==> Q" |
|
0 | 95 |
|
79 | 96 |
FalseE "False ==> P" |
0 | 97 |
|
79 | 98 |
(* Definitions *) |
0 | 99 |
|
79 | 100 |
True_def "True == False-->False" |
101 |
not_def "~P == P-->False" |
|
102 |
iff_def "P<->Q == (P-->Q) & (Q-->P)" |
|
103 |
||
104 |
(* Unique existence *) |
|
0 | 105 |
|
79 | 106 |
ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
0 | 107 |
|
79 | 108 |
(* Quantifiers *) |
0 | 109 |
|
3835 | 110 |
allI "(!!x. P(x)) ==> (ALL x. P(x))" |
111 |
spec "(ALL x. P(x)) ==> P(x)" |
|
0 | 112 |
|
3835 | 113 |
exI "P(x) ==> (EX x. P(x))" |
114 |
exE "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
|
0 | 115 |
|
116 |
(* Reflection *) |
|
117 |
||
79 | 118 |
eq_reflection "(x=y) ==> (x==y)" |
119 |
iff_reflection "(P<->Q) ==> (P==Q)" |
|
0 | 120 |
|
4092 | 121 |
|
4854 | 122 |
setup |
123 |
Simplifier.setup |
|
4092 | 124 |
|
4854 | 125 |
end |