author | wenzelm |
Thu, 04 Oct 2001 15:28:00 +0200 | |
changeset 11677 | ee12f18599e5 |
parent 9886 | 897d6602cbfb |
child 11734 | 7a21bf539412 |
permissions | -rw-r--r-- |
1268 | 1 |
(* Title: FOL/IFOL.thy |
35 | 2 |
ID: $Id$ |
11677 | 3 |
Author: Lawrence C Paulson and Markus Wenzel |
4 |
*) |
|
35 | 5 |
|
11677 | 6 |
header {* Intuitionistic first-order logic *} |
35 | 7 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
8 |
theory IFOL = Pure |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
9 |
files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"): |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
10 |
|
0 | 11 |
|
11677 | 12 |
subsection {* Syntax and axiomatic basis *} |
13 |
||
3906 | 14 |
global |
15 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
16 |
classes "term" < logic |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
17 |
defaultsort "term" |
0 | 18 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
19 |
typedecl o |
79 | 20 |
|
21 |
consts |
|
0 | 22 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
23 |
Trueprop :: "o => prop" ("(_)" 5) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
24 |
True :: o |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
25 |
False :: o |
79 | 26 |
|
27 |
(* Connectives *) |
|
28 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
29 |
"=" :: "['a, 'a] => o" (infixl 50) |
35 | 30 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
31 |
Not :: "o => o" ("~ _" [40] 40) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
32 |
& :: "[o, o] => o" (infixr 35) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
33 |
"|" :: "[o, o] => o" (infixr 30) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
34 |
--> :: "[o, o] => o" (infixr 25) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
35 |
<-> :: "[o, o] => o" (infixr 25) |
79 | 36 |
|
37 |
(* Quantifiers *) |
|
38 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
39 |
All :: "('a => o) => o" (binder "ALL " 10) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
40 |
Ex :: "('a => o) => o" (binder "EX " 10) |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
41 |
Ex1 :: "('a => o) => o" (binder "EX! " 10) |
79 | 42 |
|
0 | 43 |
|
928 | 44 |
syntax |
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
45 |
"~=" :: "['a, 'a] => o" (infixl 50) |
35 | 46 |
translations |
79 | 47 |
"x ~= y" == "~ (x = y)" |
48 |
||
2257 | 49 |
syntax (symbols) |
11677 | 50 |
Not :: "o => o" ("\<not> _" [40] 40) |
51 |
"op &" :: "[o, o] => o" (infixr "\<and>" 35) |
|
52 |
"op |" :: "[o, o] => o" (infixr "\<or>" 30) |
|
53 |
"op -->" :: "[o, o] => o" (infixr "\<midarrow>\<rightarrow>" 25) |
|
54 |
"op <->" :: "[o, o] => o" (infixr "\<leftarrow>\<rightarrow>" 25) |
|
55 |
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
|
56 |
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
|
57 |
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
58 |
"op ~=" :: "['a, 'a] => o" (infixl "\<noteq>" 50) |
|
2205 | 59 |
|
6027
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
4854
diff
changeset
|
60 |
syntax (xsymbols) |
11677 | 61 |
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
62 |
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
|
35 | 63 |
|
6340 | 64 |
syntax (HTML output) |
11677 | 65 |
Not :: "o => o" ("\<not> _" [40] 40) |
6340 | 66 |
|
67 |
||
3932 | 68 |
local |
3906 | 69 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
70 |
axioms |
0 | 71 |
|
79 | 72 |
(* Equality *) |
0 | 73 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
74 |
refl: "a=a" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
75 |
subst: "[| a=b; P(a) |] ==> P(b)" |
0 | 76 |
|
79 | 77 |
(* Propositional logic *) |
0 | 78 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
79 |
conjI: "[| P; Q |] ==> P&Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
80 |
conjunct1: "P&Q ==> P" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
81 |
conjunct2: "P&Q ==> Q" |
0 | 82 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
83 |
disjI1: "P ==> P|Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
84 |
disjI2: "Q ==> P|Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
85 |
disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" |
0 | 86 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
87 |
impI: "(P ==> Q) ==> P-->Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
88 |
mp: "[| P-->Q; P |] ==> Q" |
0 | 89 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
90 |
FalseE: "False ==> P" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
91 |
|
0 | 92 |
|
79 | 93 |
(* Definitions *) |
0 | 94 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
95 |
True_def: "True == False-->False" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
96 |
not_def: "~P == P-->False" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
97 |
iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
79 | 98 |
|
99 |
(* Unique existence *) |
|
0 | 100 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
101 |
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
102 |
|
0 | 103 |
|
79 | 104 |
(* Quantifiers *) |
0 | 105 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
106 |
allI: "(!!x. P(x)) ==> (ALL x. P(x))" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
107 |
spec: "(ALL x. P(x)) ==> P(x)" |
0 | 108 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
109 |
exI: "P(x) ==> (EX x. P(x))" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
110 |
exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
0 | 111 |
|
112 |
(* Reflection *) |
|
113 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
114 |
eq_reflection: "(x=y) ==> (x==y)" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
115 |
iff_reflection: "(P<->Q) ==> (P==Q)" |
0 | 116 |
|
4092 | 117 |
|
11677 | 118 |
subsection {* Lemmas and proof tools *} |
119 |
||
9886 | 120 |
setup Simplifier.setup |
121 |
use "IFOL_lemmas.ML" |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
122 |
use "fologic.ML" |
9886 | 123 |
use "hypsubstdata.ML" |
124 |
setup hypsubst_setup |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
125 |
use "intprover.ML" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
126 |
|
4092 | 127 |
|
11677 | 128 |
subsection {* Atomizing meta-level rules *} |
129 |
||
130 |
lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
|
131 |
proof (rule equal_intr_rule) |
|
132 |
assume "!!x. P(x)" |
|
133 |
show "ALL x. P(x)" by (rule allI) |
|
134 |
next |
|
135 |
assume "ALL x. P(x)" |
|
136 |
thus "!!x. P(x)" by (rule allE) |
|
137 |
qed |
|
138 |
||
139 |
lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)" |
|
140 |
proof (rule equal_intr_rule) |
|
141 |
assume r: "A ==> B" |
|
142 |
show "A --> B" by (rule impI) (rule r) |
|
143 |
next |
|
144 |
assume "A --> B" and A |
|
145 |
thus B by (rule mp) |
|
146 |
qed |
|
147 |
||
148 |
lemma atomize_eq: "(x == y) == Trueprop (x = y)" |
|
149 |
proof (rule equal_intr_rule) |
|
150 |
assume "x == y" |
|
151 |
show "x = y" by (unfold prems) (rule refl) |
|
152 |
next |
|
153 |
assume "x = y" |
|
154 |
thus "x == y" by (rule eq_reflection) |
|
155 |
qed |
|
156 |
||
157 |
lemmas atomize = atomize_all atomize_imp |
|
158 |
lemmas atomize' = atomize atomize_eq |
|
159 |
||
4854 | 160 |
end |