author  wenzelm 
Tue, 13 Sep 2005 22:19:23 +0200  
changeset 17339  ab97ccef124a 
parent 17276  3bb24e8b2cb2 
child 17591  33d409318266 
permissions  rwrr 
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 firstorder logic *} 
35  7 

15481  8 
theory IFOL 
9 
imports Pure 

16417  10 
uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") 
15481  11 
begin 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

12 

0  13 

11677  14 
subsection {* Syntax and axiomatic basis *} 
15 

3906  16 
global 
17 

14854  18 
classes "term" 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

19 
defaultsort "term" 
0  20 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

21 
typedecl o 
79  22 

11747  23 
judgment 
24 
Trueprop :: "o => prop" ("(_)" 5) 

0  25 

11747  26 
consts 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

27 
True :: o 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

28 
False :: o 
79  29 

30 
(* Connectives *) 

31 

17276  32 
"op =" :: "['a, 'a] => o" (infixl "=" 50) 
35  33 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

34 
Not :: "o => o" ("~ _" [40] 40) 
17276  35 
"op &" :: "[o, o] => o" (infixr "&" 35) 
36 
"op " :: "[o, o] => o" (infixr "" 30) 

37 
"op >" :: "[o, o] => o" (infixr ">" 25) 

38 
"op <>" :: "[o, o] => o" (infixr "<>" 25) 

79  39 

40 
(* Quantifiers *) 

41 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

42 
All :: "('a => o) => o" (binder "ALL " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

43 
Ex :: "('a => o) => o" (binder "EX " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

44 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  45 

0  46 

928  47 
syntax 
12662  48 
"_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) 
35  49 
translations 
79  50 
"x ~= y" == "~ (x = y)" 
51 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12019
diff
changeset

52 
syntax (xsymbols) 
11677  53 
Not :: "o => o" ("\<not> _" [40] 40) 
54 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 

55 
"op " :: "[o, o] => o" (infixr "\<or>" 30) 

56 
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) 

57 
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) 

58 
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) 

12662  59 
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 
11677  60 
"op >" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) 
61 
"op <>" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) 

35  62 

6340  63 
syntax (HTML output) 
11677  64 
Not :: "o => o" ("\<not> _" [40] 40) 
14565  65 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 
66 
"op " :: "[o, o] => o" (infixr "\<or>" 30) 

67 
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) 

68 
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) 

69 
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) 

70 
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 

6340  71 

72 

3932  73 
local 
3906  74 

14236  75 
finalconsts 
76 
False All Ex 

77 
"op =" 

78 
"op &" 

79 
"op " 

80 
"op >" 

81 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

82 
axioms 
0  83 

79  84 
(* Equality *) 
0  85 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

86 
refl: "a=a" 
0  87 

79  88 
(* Propositional logic *) 
0  89 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

90 
conjI: "[ P; Q ] ==> P&Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

91 
conjunct1: "P&Q ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

92 
conjunct2: "P&Q ==> Q" 
0  93 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

94 
disjI1: "P ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

95 
disjI2: "Q ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

96 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  97 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

98 
impI: "(P ==> Q) ==> P>Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

99 
mp: "[ P>Q; P ] ==> Q" 
0  100 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

101 
FalseE: "False ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

102 

79  103 
(* Quantifiers *) 
0  104 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

105 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

106 
spec: "(ALL x. P(x)) ==> P(x)" 
0  107 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

108 
exI: "P(x) ==> (EX x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

109 
exE: "[ EX x. P(x); !!x. P(x) ==> R ] ==> R" 
0  110 

111 
(* Reflection *) 

112 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

113 
eq_reflection: "(x=y) ==> (x==y)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

114 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  115 

4092  116 

15377  117 
text{*Thanks to Stephan Merz*} 
118 
theorem subst: 

119 
assumes eq: "a = b" and p: "P(a)" 

120 
shows "P(b)" 

121 
proof  

122 
from eq have meta: "a \<equiv> b" 

123 
by (rule eq_reflection) 

124 
from p show ?thesis 

125 
by (unfold meta) 

126 
qed 

127 

128 

14236  129 
defs 
130 
(* Definitions *) 

131 

132 
True_def: "True == False>False" 

133 
not_def: "~P == P>False" 

134 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

135 

136 
(* Unique existence *) 

137 

138 
ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) > y=x)" 

139 

13779  140 

11677  141 
subsection {* Lemmas and proof tools *} 
142 

9886  143 
use "IFOL_lemmas.ML" 
11734  144 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

145 
use "fologic.ML" 
9886  146 
use "hypsubstdata.ML" 
147 
setup hypsubst_setup 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

148 
use "intprover.ML" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

149 

4092  150 

12875  151 
subsection {* Intuitionistic Reasoning *} 
12368  152 

12349  153 
lemma impE': 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

154 
assumes 1: "P > Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

155 
and 2: "Q ==> R" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

156 
and 3: "P > Q ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

157 
shows R 
12349  158 
proof  
159 
from 3 and 1 have P . 

12368  160 
with 1 have Q by (rule impE) 
12349  161 
with 2 show R . 
162 
qed 

163 

164 
lemma allE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

165 
assumes 1: "ALL x. P(x)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

166 
and 2: "P(x) ==> ALL x. P(x) ==> Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

167 
shows Q 
12349  168 
proof  
169 
from 1 have "P(x)" by (rule spec) 

170 
from this and 1 show Q by (rule 2) 

171 
qed 

172 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

173 
lemma notE': 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

174 
assumes 1: "~ P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

175 
and 2: "~ P ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

176 
shows R 
12349  177 
proof  
178 
from 2 and 1 have P . 

179 
with 1 show R by (rule notE) 

180 
qed 

181 

182 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 

183 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

184 
and [Pure.elim 2] = allE notE' impE' 

185 
and [Pure.intro] = exI disjI2 disjI1 

186 

16121  187 
setup {* 
188 
[ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)] 

12349  189 
*} 
190 

191 

12368  192 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
193 
by rules 

194 

195 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

196 
and [Pure.elim?] = iffD1 iffD2 impE 

197 

198 

13435  199 
lemma eq_commute: "a=b <> b=a" 
200 
apply (rule iffI) 

201 
apply (erule sym)+ 

202 
done 

203 

204 

11677  205 
subsection {* Atomizing metalevel rules *} 
206 

11747  207 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  208 
proof 
11677  209 
assume "!!x. P(x)" 
12368  210 
show "ALL x. P(x)" .. 
11677  211 
next 
212 
assume "ALL x. P(x)" 

12368  213 
thus "!!x. P(x)" .. 
11677  214 
qed 
215 

11747  216 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  217 
proof 
12368  218 
assume "A ==> B" 
219 
thus "A > B" .. 

11677  220 
next 
221 
assume "A > B" and A 

222 
thus B by (rule mp) 

223 
qed 

224 

11747  225 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  226 
proof 
11677  227 
assume "x == y" 
228 
show "x = y" by (unfold prems) (rule refl) 

229 
next 

230 
assume "x = y" 

231 
thus "x == y" by (rule eq_reflection) 

232 
qed 

233 

12875  234 
lemma atomize_conj [atomize]: 
235 
"(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 

11976  236 
proof 
11953  237 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
238 
show "A & B" by (rule conjI) 

239 
next 

240 
fix C 

241 
assume "A & B" 

242 
assume "A ==> B ==> PROP C" 

243 
thus "PROP C" 

244 
proof this 

245 
show A by (rule conjunct1) 

246 
show B by (rule conjunct2) 

247 
qed 

248 
qed 

249 

12368  250 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
11771  251 

11848  252 

253 
subsection {* Calculational rules *} 

254 

255 
lemma forw_subst: "a = b ==> P(b) ==> P(a)" 

256 
by (rule ssubst) 

257 

258 
lemma back_subst: "P(a) ==> a = b ==> P(b)" 

259 
by (rule subst) 

260 

261 
text {* 

262 
Note that this list of rules is in reverse order of priorities. 

263 
*} 

264 

12019  265 
lemmas basic_trans_rules [trans] = 
11848  266 
forw_subst 
267 
back_subst 

268 
rev_mp 

269 
mp 

270 
trans 

271 

13779  272 
subsection {* ``Let'' declarations *} 
273 

274 
nonterminals letbinds letbind 

275 

276 
constdefs 

14854  277 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  278 
"Let(s, f) == f(s)" 
279 

280 
syntax 

281 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 

282 
"" :: "letbind => letbinds" ("_") 

283 
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") 

284 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) 

285 

286 
translations 

287 
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" 

288 
"let x = a in e" == "Let(a, %x. e)" 

289 

290 

291 
lemma LetI: 

292 
assumes prem: "(!!x. x=t ==> P(u(x)))" 

293 
shows "P(let x=t in u(x))" 

294 
apply (unfold Let_def) 

295 
apply (rule refl [THEN prem]) 

296 
done 

297 

298 
ML 

299 
{* 

300 
val Let_def = thm "Let_def"; 

301 
val LetI = thm "LetI"; 

302 
*} 

303 

4854  304 
end 