author  paulson 
Thu, 16 Oct 2003 10:31:40 +0200  
changeset 14236  c73d62ce9d1c 
parent 13779  2a34dc5cf79e 
child 14565  c6dc17aab88a 
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 

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 

11747  21 
judgment 
22 
Trueprop :: "o => prop" ("(_)" 5) 

0  23 

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

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

26 
False :: o 
79  27 

28 
(* Connectives *) 

29 

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

30 
"=" :: "['a, 'a] => o" (infixl 50) 
35  31 

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

32 
Not :: "o => o" ("~ _" [40] 40) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

33 
& :: "[o, o] => o" (infixr 35) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

34 
"" :: "[o, o] => o" (infixr 30) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

35 
> :: "[o, o] => o" (infixr 25) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

36 
<> :: "[o, o] => o" (infixr 25) 
79  37 

38 
(* Quantifiers *) 

39 

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

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

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

42 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  43 

0  44 

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

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

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

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

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

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

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

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

35  60 

6340  61 
syntax (HTML output) 
11677  62 
Not :: "o => o" ("\<not> _" [40] 40) 
6340  63 

64 

3932  65 
local 
3906  66 

14236  67 
finalconsts 
68 
False All Ex 

69 
"op =" 

70 
"op &" 

71 
"op " 

72 
"op >" 

73 

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

74 
axioms 
0  75 

79  76 
(* Equality *) 
0  77 

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

78 
refl: "a=a" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

79 
subst: "[ a=b; P(a) ] ==> P(b)" 
0  80 

79  81 
(* Propositional logic *) 
0  82 

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

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

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

85 
conjunct2: "P&Q ==> Q" 
0  86 

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

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

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

89 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  90 

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

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

92 
mp: "[ P>Q; P ] ==> Q" 
0  93 

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

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

95 

79  96 
(* Quantifiers *) 
0  97 

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

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

99 
spec: "(ALL x. P(x)) ==> P(x)" 
0  100 

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

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

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

104 
(* Reflection *) 

105 

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

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

107 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  108 

4092  109 

14236  110 
defs 
111 
(* Definitions *) 

112 

113 
True_def: "True == False>False" 

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

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

116 

117 
(* Unique existence *) 

118 

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

120 

13779  121 

11677  122 
subsection {* Lemmas and proof tools *} 
123 

9886  124 
setup Simplifier.setup 
125 
use "IFOL_lemmas.ML" 

11734  126 

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

127 
use "fologic.ML" 
9886  128 
use "hypsubstdata.ML" 
129 
setup hypsubst_setup 

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

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

131 

4092  132 

12875  133 
subsection {* Intuitionistic Reasoning *} 
12368  134 

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

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

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

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

139 
shows R 
12349  140 
proof  
141 
from 3 and 1 have P . 

12368  142 
with 1 have Q by (rule impE) 
12349  143 
with 2 show R . 
144 
qed 

145 

146 
lemma allE': 

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

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

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

149 
shows Q 
12349  150 
proof  
151 
from 1 have "P(x)" by (rule spec) 

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

153 
qed 

154 

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

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

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

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

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

161 
with 1 show R by (rule notE) 

162 
qed 

163 

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

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

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

167 
and [Pure.intro] = exI disjI2 disjI1 

168 

169 
ML_setup {* 

12352  170 
Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)); 
12349  171 
*} 
172 

173 

12368  174 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
175 
by rules 

176 

177 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

179 

180 

13435  181 
lemma eq_commute: "a=b <> b=a" 
182 
apply (rule iffI) 

183 
apply (erule sym)+ 

184 
done 

185 

186 

11677  187 
subsection {* Atomizing metalevel rules *} 
188 

11747  189 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  190 
proof 
11677  191 
assume "!!x. P(x)" 
12368  192 
show "ALL x. P(x)" .. 
11677  193 
next 
194 
assume "ALL x. P(x)" 

12368  195 
thus "!!x. P(x)" .. 
11677  196 
qed 
197 

11747  198 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  199 
proof 
12368  200 
assume "A ==> B" 
201 
thus "A > B" .. 

11677  202 
next 
203 
assume "A > B" and A 

204 
thus B by (rule mp) 

205 
qed 

206 

11747  207 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  208 
proof 
11677  209 
assume "x == y" 
210 
show "x = y" by (unfold prems) (rule refl) 

211 
next 

212 
assume "x = y" 

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

214 
qed 

215 

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

11976  218 
proof 
11953  219 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
220 
show "A & B" by (rule conjI) 

221 
next 

222 
fix C 

223 
assume "A & B" 

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

225 
thus "PROP C" 

226 
proof this 

227 
show A by (rule conjunct1) 

228 
show B by (rule conjunct2) 

229 
qed 

230 
qed 

231 

12368  232 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
11771  233 

11848  234 

235 
subsection {* Calculational rules *} 

236 

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

238 
by (rule ssubst) 

239 

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

241 
by (rule subst) 

242 

243 
text {* 

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

245 
*} 

246 

12019  247 
lemmas basic_trans_rules [trans] = 
11848  248 
forw_subst 
249 
back_subst 

250 
rev_mp 

251 
mp 

252 
trans 

253 

13779  254 

255 

256 
subsection {* ``Let'' declarations *} 

257 

258 
nonterminals letbinds letbind 

259 

260 
constdefs 

261 
Let :: "['a::logic, 'a => 'b] => ('b::logic)" 

262 
"Let(s, f) == f(s)" 

263 

264 
syntax 

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

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

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

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

269 

270 
translations 

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

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

273 

274 

275 
lemma LetI: 

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

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

278 
apply (unfold Let_def) 

279 
apply (rule refl [THEN prem]) 

280 
done 

281 

282 
ML 

283 
{* 

284 
val Let_def = thm "Let_def"; 

285 
val LetI = thm "LetI"; 

286 
*} 

287 

4854  288 
end 