author  wenzelm 
Sat, 10 Jul 1999 21:44:26 +0200  
changeset 6966  cfa87aef9ccd 
parent 6113  b321f5aaa5f4 
child 7355  4c43090659ca 
permissions  rwrr 
1459  1 
(* Title: FOL/IFOL.ML 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

1280  6 
Tactics and lemmas for IFOL.thy (intuitionistic firstorder logic) 
0  7 
*) 
8 

779  9 
qed_goalw "TrueI" IFOL.thy [True_def] "True" 
0  10 
(fn _ => [ (REPEAT (ares_tac [impI] 1)) ]); 
11 

12 
(*** Sequentstyle elimination rules for & > and ALL ***) 

13 

779  14 
qed_goal "conjE" IFOL.thy 
0  15 
"[ P&Q; [ P; Q ] ==> R ] ==> R" 
16 
(fn prems=> 

17 
[ (REPEAT (resolve_tac prems 1 

18 
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN 

19 
resolve_tac prems 1))) ]); 

20 

779  21 
qed_goal "impE" IFOL.thy 
0  22 
"[ P>Q; P; Q ==> R ] ==> R" 
23 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 

24 

779  25 
qed_goal "allE" IFOL.thy 
3835  26 
"[ ALL x. P(x); P(x) ==> R ] ==> R" 
0  27 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); 
28 

29 
(*Duplicates the quantifier; for use with eresolve_tac*) 

779  30 
qed_goal "all_dupE" IFOL.thy 
3835  31 
"[ ALL x. P(x); [ P(x); ALL x. P(x) ] ==> R \ 
0  32 
\ ] ==> R" 
33 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); 

34 

35 

36 
(*** Negation rules, which translate between ~P and P>False ***) 

37 

779  38 
qed_goalw "notI" IFOL.thy [not_def] "(P ==> False) ==> ~P" 
0  39 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); 
40 

779  41 
qed_goalw "notE" IFOL.thy [not_def] "[ ~P; P ] ==> R" 
0  42 
(fn prems=> 
43 
[ (resolve_tac [mp RS FalseE] 1), 

44 
(REPEAT (resolve_tac prems 1)) ]); 

45 

1891  46 
qed_goal "rev_notE" IFOL.thy "!!P R. [ P; ~P ] ==> R" 
47 
(fn _ => [REPEAT (ares_tac [notE] 1)]); 

48 

0  49 
(*This is useful with the special implication rules for each kind of P. *) 
779  50 
qed_goal "not_to_imp" IFOL.thy 
0  51 
"[ ~P; (P>False) ==> Q ] ==> Q" 
52 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); 

53 

1002  54 
(* For substitution into an assumption P, reduce Q to P>Q, substitute into 
0  55 
this implication, then apply impI to move P back into the assumptions. 
56 
To specify P use something like 

57 
eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) 

779  58 
qed_goal "rev_mp" IFOL.thy "[ P; P > Q ] ==> Q" 
0  59 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); 
60 

61 
(*Contrapositive of an inference rule*) 

779  62 
qed_goal "contrapos" IFOL.thy "[ ~Q; P==>Q ] ==> ~P" 
0  63 
(fn [major,minor]=> 
64 
[ (rtac (major RS notE RS notI) 1), 

65 
(etac minor 1) ]); 

66 

67 

68 
(*** Modus Ponens Tactics ***) 

69 

70 
(*Finds P>Q and P in the assumptions, replaces implication by Q *) 

71 
fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i; 

72 

73 
(*Like mp_tac but instantiates no variables*) 

74 
fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i; 

75 

76 

77 
(*** Ifandonlyif ***) 

78 

779  79 
qed_goalw "iffI" IFOL.thy [iff_def] 
0  80 
"[ P ==> Q; Q ==> P ] ==> P<>Q" 
81 
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); 

82 

83 

84 
(*Observe use of rewrite_rule to unfold "<>" in metaassumptions (prems) *) 

779  85 
qed_goalw "iffE" IFOL.thy [iff_def] 
0  86 
"[ P <> Q; [ P>Q; Q>P ] ==> R ] ==> R" 
1459  87 
(fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); 
0  88 

89 
(* Destruct rules for <> similar to Modus Ponens *) 

90 

779  91 
qed_goalw "iffD1" IFOL.thy [iff_def] "[ P <> Q; P ] ==> Q" 
0  92 
(fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 
93 

779  94 
qed_goalw "iffD2" IFOL.thy [iff_def] "[ P <> Q; Q ] ==> P" 
0  95 
(fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 
96 

4462  97 
qed_goal "rev_iffD1" IFOL.thy "!!P. [ P; P <> Q ] ==> Q" 
98 
(fn _ => [etac iffD1 1, assume_tac 1]); 

99 

100 
qed_goal "rev_iffD2" IFOL.thy "!!P. [ Q; P <> Q ] ==> P" 

101 
(fn _ => [etac iffD2 1, assume_tac 1]); 

102 

779  103 
qed_goal "iff_refl" IFOL.thy "P <> P" 
0  104 
(fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); 
105 

779  106 
qed_goal "iff_sym" IFOL.thy "Q <> P ==> P <> Q" 
0  107 
(fn [major] => 
108 
[ (rtac (major RS iffE) 1), 

109 
(rtac iffI 1), 

110 
(REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); 

111 

779  112 
qed_goal "iff_trans" IFOL.thy 
0  113 
"!!P Q R. [ P <> Q; Q<> R ] ==> P <> R" 
114 
(fn _ => 

115 
[ (rtac iffI 1), 

116 
(REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); 

117 

118 

119 
(*** Unique existence. NOTE THAT the following 2 quantifications 

120 
EX!x such that [EX!y such that P(x,y)] (sequential) 

121 
EX!x,y such that P(x,y) (simultaneous) 

122 
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. 

123 
***) 

124 

779  125 
qed_goalw "ex1I" IFOL.thy [ex1_def] 
0  126 
"[ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x)" 
127 
(fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); 

128 

2843  129 
(*Sometimes easier to use: the premises have no shared variables. Safe!*) 
779  130 
qed_goal "ex_ex1I" IFOL.thy 
3835  131 
"[ EX x. P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> EX! x. P(x)" 
12
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

132 
(fn [ex,eq] => [ (rtac (ex RS exE) 1), 
1459  133 
(REPEAT (ares_tac [ex1I,eq] 1)) ]); 
12
f17d542276b6
Added ex_ex1I: new introduction rule for the EX! quantifier.
lcp
parents:
0
diff
changeset

134 

779  135 
qed_goalw "ex1E" IFOL.thy [ex1_def] 
3835  136 
"[ EX! x. P(x); !!x. [ P(x); ALL y. P(y) > y=x ] ==> R ] ==> R" 
0  137 
(fn prems => 
138 
[ (cut_facts_tac prems 1), 

139 
(REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); 

140 

141 

142 
(*** <> congruence rules for simplification ***) 

143 

144 
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) 

145 
fun iff_tac prems i = 

146 
resolve_tac (prems RL [iffE]) i THEN 

147 
REPEAT1 (eresolve_tac [asm_rl,mp] i); 

148 

779  149 
qed_goal "conj_cong" IFOL.thy 
0  150 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P&Q) <> (P'&Q')" 
151 
(fn prems => 

152 
[ (cut_facts_tac prems 1), 

153 
(REPEAT (ares_tac [iffI,conjI] 1 

154 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

155 
ORELSE iff_tac prems 1)) ]); 

156 

793  157 
(*Reversed congruence rule! Used in ZF/Order*) 
158 
qed_goal "conj_cong2" IFOL.thy 

159 
"[ P <> P'; P' ==> Q <> Q' ] ==> (Q&P) <> (Q'&P')" 

160 
(fn prems => 

161 
[ (cut_facts_tac prems 1), 

162 
(REPEAT (ares_tac [iffI,conjI] 1 

163 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

164 
ORELSE iff_tac prems 1)) ]); 

165 

779  166 
qed_goal "disj_cong" IFOL.thy 
0  167 
"[ P <> P'; Q <> Q' ] ==> (PQ) <> (P'Q')" 
168 
(fn prems => 

169 
[ (cut_facts_tac prems 1), 

170 
(REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 

171 
ORELSE ares_tac [iffI] 1 

172 
ORELSE mp_tac 1)) ]); 

173 

779  174 
qed_goal "imp_cong" IFOL.thy 
0  175 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P>Q) <> (P'>Q')" 
176 
(fn prems => 

177 
[ (cut_facts_tac prems 1), 

178 
(REPEAT (ares_tac [iffI,impI] 1 

1459  179 
ORELSE etac iffE 1 
0  180 
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); 
181 

779  182 
qed_goal "iff_cong" IFOL.thy 
0  183 
"[ P <> P'; Q <> Q' ] ==> (P<>Q) <> (P'<>Q')" 
184 
(fn prems => 

185 
[ (cut_facts_tac prems 1), 

1459  186 
(REPEAT (etac iffE 1 
0  187 
ORELSE ares_tac [iffI] 1 
188 
ORELSE mp_tac 1)) ]); 

189 

779  190 
qed_goal "not_cong" IFOL.thy 
0  191 
"P <> P' ==> ~P <> ~P'" 
192 
(fn prems => 

193 
[ (cut_facts_tac prems 1), 

194 
(REPEAT (ares_tac [iffI,notI] 1 

195 
ORELSE mp_tac 1 

196 
ORELSE eresolve_tac [iffE,notE] 1)) ]); 

197 

779  198 
qed_goal "all_cong" IFOL.thy 
3835  199 
"(!!x. P(x) <> Q(x)) ==> (ALL x. P(x)) <> (ALL x. Q(x))" 
0  200 
(fn prems => 
201 
[ (REPEAT (ares_tac [iffI,allI] 1 

202 
ORELSE mp_tac 1 

1459  203 
ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); 
0  204 

779  205 
qed_goal "ex_cong" IFOL.thy 
3835  206 
"(!!x. P(x) <> Q(x)) ==> (EX x. P(x)) <> (EX x. Q(x))" 
0  207 
(fn prems => 
1459  208 
[ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 
0  209 
ORELSE mp_tac 1 
210 
ORELSE iff_tac prems 1)) ]); 

211 

779  212 
qed_goal "ex1_cong" IFOL.thy 
3835  213 
"(!!x. P(x) <> Q(x)) ==> (EX! x. P(x)) <> (EX! x. Q(x))" 
0  214 
(fn prems => 
215 
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 

216 
ORELSE mp_tac 1 

217 
ORELSE iff_tac prems 1)) ]); 

218 

219 
(*** Equality rules ***) 

220 

779  221 
qed_goal "sym" IFOL.thy "a=b ==> b=a" 
0  222 
(fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); 
223 

779  224 
qed_goal "trans" IFOL.thy "[ a=b; b=c ] ==> a=c" 
0  225 
(fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); 
226 

227 
(** ~ b=a ==> ~ a=b **) 

228 
val [not_sym] = compose(sym,2,contrapos); 

229 

5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

230 

01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

231 
(* Two theorms for rewriting only one instance of a definition: 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

232 
the first for definitions of formulae and the second for terms *) 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

233 

01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

234 
val prems = goal IFOL.thy "(A == B) ==> A <> B"; 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

235 
by (rewrite_goals_tac prems); 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

236 
by (rtac iff_refl 1); 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

237 
qed "def_imp_iff"; 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

238 

01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

239 
val prems = goal IFOL.thy "(A == B) ==> A = B"; 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

240 
by (rewrite_goals_tac prems); 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

241 
by (rtac refl 1); 
6113  242 
qed "meta_eq_to_obj_eq"; 
243 

5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

244 

2037  245 
(*Substitution: rule and tactic*) 
246 
bind_thm ("ssubst", sym RS subst); 

5139
013ea0f023e3
stac now uses CHANGED_GOAL and correctly fails when it has no useful effect,
paulson
parents:
4462
diff
changeset

247 

5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

248 
(*Apply an equality or definition ONCE. 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

249 
Fails unless the substitution has an effect*) 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

250 
fun stac th = 
6966  251 
let val th' = th RS meta_eq_to_obj_eq handle THM _ => th 
5309
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

252 
in CHANGED_GOAL (rtac (th' RS ssubst)) 
01c2b317da88
stac now handles definitions as well as equalities
paulson
parents:
5139
diff
changeset

253 
end; 
0  254 

255 
(*A special case of ex1E that would otherwise need quantifier expansion*) 

779  256 
qed_goal "ex1_equalsE" IFOL.thy 
3835  257 
"[ EX! x. P(x); P(a); P(b) ] ==> a=b" 
0  258 
(fn prems => 
259 
[ (cut_facts_tac prems 1), 

260 
(etac ex1E 1), 

261 
(rtac trans 1), 

262 
(rtac sym 2), 

263 
(REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); 

264 

265 
(** Polymorphic congruence rules **) 

266 

779  267 
qed_goal "subst_context" IFOL.thy 
0  268 
"[ a=b ] ==> t(a)=t(b)" 
269 
(fn prems=> 

270 
[ (resolve_tac (prems RL [ssubst]) 1), 

1459  271 
(rtac refl 1) ]); 
0  272 

779  273 
qed_goal "subst_context2" IFOL.thy 
0  274 
"[ a=b; c=d ] ==> t(a,c)=t(b,d)" 
275 
(fn prems=> 

276 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); 

277 

779  278 
qed_goal "subst_context3" IFOL.thy 
0  279 
"[ a=b; c=d; e=f ] ==> t(a,c,e)=t(b,d,f)" 
280 
(fn prems=> 

281 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); 

282 

283 
(*Useful with eresolve_tac for proving equalties from known equalities. 

1459  284 
a = b 
285 
  

286 
c = d *) 

779  287 
qed_goal "box_equals" IFOL.thy 
0  288 
"[ a=b; a=c; b=d ] ==> c=d" 
289 
(fn prems=> 

1459  290 
[ (rtac trans 1), 
291 
(rtac trans 1), 

292 
(rtac sym 1), 

0  293 
(REPEAT (resolve_tac prems 1)) ]); 
294 

295 
(*Dual of box_equals: for proving equalities backwards*) 

779  296 
qed_goal "simp_equals" IFOL.thy 
0  297 
"[ a=c; b=d; c=d ] ==> a=b" 
298 
(fn prems=> 

1459  299 
[ (rtac trans 1), 
300 
(rtac trans 1), 

0  301 
(REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); 
302 

303 
(** Congruence rules for predicate letters **) 

304 

779  305 
qed_goal "pred1_cong" IFOL.thy 
0  306 
"a=a' ==> P(a) <> P(a')" 
307 
(fn prems => 

308 
[ (cut_facts_tac prems 1), 

309 
(rtac iffI 1), 

310 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

311 

779  312 
qed_goal "pred2_cong" IFOL.thy 
0  313 
"[ a=a'; b=b' ] ==> P(a,b) <> P(a',b')" 
314 
(fn prems => 

315 
[ (cut_facts_tac prems 1), 

316 
(rtac iffI 1), 

317 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

318 

779  319 
qed_goal "pred3_cong" IFOL.thy 
0  320 
"[ a=a'; b=b'; c=c' ] ==> P(a,b,c) <> P(a',b',c')" 
321 
(fn prems => 

322 
[ (cut_facts_tac prems 1), 

323 
(rtac iffI 1), 

324 
(DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); 

325 

326 
(*special cases for free variables P, Q, R, S  up to 3 arguments*) 

327 

328 
val pred_congs = 

329 
flat (map (fn c => 

1459  330 
map (fn th => read_instantiate [("P",c)] th) 
331 
[pred1_cong,pred2_cong,pred3_cong]) 

332 
(explode"PQRS")); 

0  333 

334 
(*special case for the equality predicate!*) 

335 
val eq_cong = read_instantiate [("P","op =")] pred2_cong; 

336 

337 

338 
(*** Simplifications of assumed implications. 

339 
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE 

340 
used with mp_tac (restricted to atomic formulae) is COMPLETE for 

341 
intuitionistic propositional logic. See 

342 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

343 
(preprint, University of St Andrews, 1991) ***) 

344 

779  345 
qed_goal "conj_impE" IFOL.thy 
0  346 
"[ (P&Q)>S; P>(Q>S) ==> R ] ==> R" 
347 
(fn major::prems=> 

348 
[ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); 

349 

779  350 
qed_goal "disj_impE" IFOL.thy 
0  351 
"[ (PQ)>S; [ P>S; Q>S ] ==> R ] ==> R" 
352 
(fn major::prems=> 

353 
[ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); 

354 

355 
(*Simplifies the implication. Classical version is stronger. 

356 
Still UNSAFE since Q must be provable  backtracking needed. *) 

779  357 
qed_goal "imp_impE" IFOL.thy 
0  358 
"[ (P>Q)>S; [ P; Q>S ] ==> Q; S ==> R ] ==> R" 
359 
(fn major::prems=> 

360 
[ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); 

361 

362 
(*Simplifies the implication. Classical version is stronger. 

363 
Still UNSAFE since ~P must be provable  backtracking needed. *) 

779  364 
qed_goal "not_impE" IFOL.thy 
0  365 
"[ ~P > S; P ==> False; S ==> R ] ==> R" 
366 
(fn major::prems=> 

367 
[ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); 

368 

369 
(*Simplifies the implication. UNSAFE. *) 

779  370 
qed_goal "iff_impE" IFOL.thy 
0  371 
"[ (P<>Q)>S; [ P; Q>S ] ==> Q; [ Q; P>S ] ==> P; \ 
372 
\ S ==> R ] ==> R" 

373 
(fn major::prems=> 

374 
[ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); 

375 

376 
(*What if (ALL x.~~P(x)) > ~~(ALL x.P(x)) is an assumption? UNSAFE*) 

779  377 
qed_goal "all_impE" IFOL.thy 
3835  378 
"[ (ALL x. P(x))>S; !!x. P(x); S ==> R ] ==> R" 
0  379 
(fn major::prems=> 
380 
[ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); 

381 

382 
(*Unsafe: (EX x.P(x))>S is equivalent to ALL x.P(x)>S. *) 

779  383 
qed_goal "ex_impE" IFOL.thy 
3835  384 
"[ (EX x. P(x))>S; P(x)>S ==> R ] ==> R" 
0  385 
(fn major::prems=> 
386 
[ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); 

821  387 

1608  388 
(*** Courtesy of Krzysztof Grabczewski ***) 
389 

821  390 
val major::prems = goal IFOL.thy "[ PQ; P==>R; Q==>S ] ==> RS"; 
1459  391 
by (rtac (major RS disjE) 1); 
821  392 
by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1)); 
393 
qed "disj_imp_disj"; 

1608  394 

3722
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

395 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

396 
(** strip ALL and > from proved goal while preserving ALLbound var names **) 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

397 

6113  398 
fun make_new_spec rl = 
399 
(* Use a crazy name to avoid forall_intr failing because of 

400 
duplicate variable name *) 

401 
let val myspec = read_instantiate [("P","?wlzickd")] rl 

402 
val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec; 

403 
val cvx = cterm_of (#sign(rep_thm myspec)) vx 

404 
in (vxT, forall_intr cvx myspec) end; 

405 

3722
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

406 
local 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

407 

6113  408 
val (specT, spec') = make_new_spec spec 
3722
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

409 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

410 
in 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

411 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

412 
fun RSspec th = 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

413 
(case concl_of th of 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

414 
_ $ (Const("All",_) $ Abs(a,_,_)) => 
6113  415 
let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT)) 
416 
in th RS forall_elim ca spec' end 

3722
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

417 
 _ => raise THM("RSspec",0,[th])); 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

418 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

419 
fun RSmp th = 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

420 
(case concl_of th of 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

421 
_ $ (Const("op >",_)$_$_) => th RS mp 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

422 
 _ => raise THM("RSmp",0,[th])); 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

423 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

424 
fun normalize_thm funs = 
6113  425 
let fun trans [] th = th 
426 
 trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th 

427 
in trans funs end; 

3722
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

428 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

429 
fun qed_spec_mp name = 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

430 
let val thm = normalize_thm [RSspec,RSmp] (result()) 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

431 
in bind_thm(name, thm) end; 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

432 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

433 
fun qed_goal_spec_mp name thy s p = 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

434 
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p)); 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

435 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

436 
fun qed_goalw_spec_mp name thy defs s p = 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

437 
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p)); 
24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

438 

24af9e73451e
qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
paulson
parents:
2843
diff
changeset

439 
end; 
5888  440 

441 

442 
(* attributes *) 

443 

444 
local 

445 

6090  446 
fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; 
5888  447 

448 
in 

449 

450 
val attrib_setup = 

451 
[Attrib.add_attributes 

452 
[("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]]; 

453 

454 
end; 