author  wenzelm 
Thu, 29 Sep 2005 00:58:55 +0200  
changeset 17702  ea88ddeafabe 
parent 17591  33d409318266 
child 18481  b75ce99617c7 
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" 
17702  19 
final_consts term_class 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

20 
defaultsort "term" 
0  21 

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

22 
typedecl o 
79  23 

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

0  26 

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

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

29 
False :: o 
79  30 

31 
(* Connectives *) 

32 

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

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

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

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

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

79  40 

41 
(* Quantifiers *) 

42 

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

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

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

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

0  47 

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

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

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

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

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

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

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

12662  60 
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 
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) 
14565  66 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 
67 
"op " :: "[o, o] => o" (infixr "\<or>" 30) 

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

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

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

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

6340  72 

73 

3932  74 
local 
3906  75 

14236  76 
finalconsts 
77 
False All Ex 

78 
"op =" 

79 
"op &" 

80 
"op " 

81 
"op >" 

82 

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

83 
axioms 
0  84 

79  85 
(* Equality *) 
0  86 

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

87 
refl: "a=a" 
0  88 

79  89 
(* Propositional logic *) 
0  90 

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

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

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

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

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

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

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

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

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

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

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

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

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

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 

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

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

121 
shows "P(b)" 

122 
proof  

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

124 
by (rule eq_reflection) 

125 
from p show ?thesis 

126 
by (unfold meta) 

127 
qed 

128 

129 

14236  130 
defs 
131 
(* Definitions *) 

132 

133 
True_def: "True == False>False" 

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

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

136 

137 
(* Unique existence *) 

138 

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

140 

13779  141 

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

9886  144 
use "IFOL_lemmas.ML" 
11734  145 

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

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

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

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

150 

4092  151 

12875  152 
subsection {* Intuitionistic Reasoning *} 
12368  153 

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

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

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

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

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

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

164 

165 
lemma allE': 

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

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

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

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

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

172 
qed 

173 

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

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

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

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

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

180 
with 1 show R by (rule notE) 

181 
qed 

182 

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

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

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

186 
and [Pure.intro] = exI disjI2 disjI1 

187 

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

12349  190 
*} 
191 

192 

12368  193 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  194 
by iprover 
12368  195 

196 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

198 

199 

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

202 
apply (erule sym)+ 

203 
done 

204 

205 

11677  206 
subsection {* Atomizing metalevel rules *} 
207 

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

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

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

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

223 
thus B by (rule mp) 

224 
qed 

225 

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

230 
next 

231 
assume "x = y" 

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

233 
qed 

234 

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

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

240 
next 

241 
fix C 

242 
assume "A & B" 

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

244 
thus "PROP C" 

245 
proof this 

246 
show A by (rule conjunct1) 

247 
show B by (rule conjunct2) 

248 
qed 

249 
qed 

250 

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

11848  253 

254 
subsection {* Calculational rules *} 

255 

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

257 
by (rule ssubst) 

258 

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

260 
by (rule subst) 

261 

262 
text {* 

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

264 
*} 

265 

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

269 
rev_mp 

270 
mp 

271 
trans 

272 

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

275 
nonterminals letbinds letbind 

276 

277 
constdefs 

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

281 
syntax 

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

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

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

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

286 

287 
translations 

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

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

290 

291 

292 
lemma LetI: 

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

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

295 
apply (unfold Let_def) 

296 
apply (rule refl [THEN prem]) 

297 
done 

298 

299 
ML 

300 
{* 

301 
val Let_def = thm "Let_def"; 

302 
val LetI = thm "LetI"; 

303 
*} 

304 

4854  305 
end 