author  wenzelm 
Fri, 08 Jan 2021 22:30:32 +0100  
changeset 73110  c87ca43ebd3b 
parent 70880  de2e2382bc0d 
child 74301  ffe269e74bdd 
permissions  rwrr 
1477  1 
(* Title: FOLP/IFOLP.thy 
2 
Author: Martin D Coen, Cambridge University Computer Laboratory 

1142  3 
Copyright 1992 University of Cambridge 
4 
*) 

5 

60770  6 
section \<open>Intuitionistic FirstOrder Logic with Proofs\<close> 
17480  7 

8 
theory IFOLP 

9 
imports Pure 

10 
begin 

0  11 

69605  12 
ML_file \<open>~~/src/Tools/misc_legacy.ML\<close> 
48891  13 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
38800
diff
changeset

14 
setup Pure_Thy.old_appl_syntax_setup 
70880  15 
setup \<open>Proofterm.set_preproc (Proof_Rewrite_Rules.standard_preproc [])\<close> 
26956
1309a6a0a29f
setup PureThy.old_appl_syntax_setup  theory Pure provides regular application syntax by default;
wenzelm
parents:
26480
diff
changeset

16 

55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
52230
diff
changeset

17 
class "term" 
36452  18 
default_sort "term" 
0  19 

17480  20 
typedecl p 
21 
typedecl o 

0  22 

17480  23 
consts 
0  24 
(*** Judgements ***) 
1477  25 
Proof :: "[o,p]=>prop" 
0  26 
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5) 
17480  27 

0  28 
(*** Logical Connectives  Type Formers ***) 
41310  29 
eq :: "['a,'a] => o" (infixl "=" 50) 
17480  30 
True :: "o" 
31 
False :: "o" 

41310  32 
conj :: "[o,o] => o" (infixr "&" 35) 
33 
disj :: "[o,o] => o" (infixr "" 30) 

34 
imp :: "[o,o] => o" (infixr ">" 25) 

0  35 
(*Quantifiers*) 
1477  36 
All :: "('a => o) => o" (binder "ALL " 10) 
37 
Ex :: "('a => o) => o" (binder "EX " 10) 

0  38 
(*Rewriting gadgets*) 
1477  39 
NORM :: "o => o" 
40 
norm :: "'a => 'a" 

0  41 

648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

42 
(*** Proof Term Formers: precedence must exceed 50 ***) 
1477  43 
tt :: "p" 
44 
contr :: "p=>p" 

17480  45 
fst :: "p=>p" 
46 
snd :: "p=>p" 

1477  47 
pair :: "[p,p]=>p" ("(1<_,/_>)") 
48 
split :: "[p, [p,p]=>p] =>p" 

17480  49 
inl :: "p=>p" 
50 
inr :: "p=>p" 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
59529
diff
changeset

51 
"when" :: "[p, p=>p, p=>p]=>p" 
1477  52 
lambda :: "(p => p) => p" (binder "lam " 55) 
41310  53 
App :: "[p,p]=>p" (infixl "`" 60) 
648
e27c9ec2b48b
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
lcp
parents:
283
diff
changeset

54 
alll :: "['a=>p]=>p" (binder "all " 55) 
41310  55 
app :: "[p,'a]=>p" (infixl "^" 55) 
1477  56 
exists :: "['a,p]=>p" ("(1[_,/_])") 
0  57 
xsplit :: "[p,['a,p]=>p]=>p" 
58 
ideq :: "'a=>p" 

59 
idpeel :: "[p,'a=>p]=>p" 

17480  60 
nrm :: p 
61 
NRM :: p 

0  62 

35113  63 
syntax "_Proof" :: "[p,o]=>prop" ("(_ /: _)" [51, 10] 5) 
64 

60770  65 
parse_translation \<open> 
69593  66 
let fun proof_tr [p, P] = Const (\<^const_syntax>\<open>Proof\<close>, dummyT) $ P $ p 
67 
in [(\<^syntax_const>\<open>_Proof\<close>, K proof_tr)] end 

60770  68 
\<close> 
17480  69 

38800  70 
(*show_proofs = true displays the proof terms  they are ENORMOUS*) 
69593  71 
ML \<open>val show_proofs = Attrib.setup_config_bool \<^binding>\<open>show_proofs\<close> (K false)\<close> 
38800  72 

60770  73 
print_translation \<open> 
38800  74 
let 
75 
fun proof_tr' ctxt [P, p] = 

69593  76 
if Config.get ctxt show_proofs then Const (\<^syntax_const>\<open>_Proof\<close>, dummyT) $ p $ P 
38800  77 
else P 
69593  78 
in [(\<^const_syntax>\<open>Proof\<close>, proof_tr')] end 
60770  79 
\<close> 
17480  80 

0  81 

82 
(**** Propositional logic ****) 

83 

84 
(*Equality*) 

85 
(* Like Intensional Equality in MLTT  but proofs distinct from terms *) 

86 

51306  87 
axiomatization where 
88 
ieqI: "ideq(a) : a=a" and 

17480  89 
ieqE: "[ p : a=b; !!x. f(x) : P(x,x) ] ==> idpeel(p,f) : P(a,b)" 
0  90 

91 
(* Truth and Falsity *) 

92 

51306  93 
axiomatization where 
94 
TrueI: "tt : True" and 

17480  95 
FalseE: "a:False ==> contr(a):P" 
0  96 

97 
(* Conjunction *) 

98 

51306  99 
axiomatization where 
100 
conjI: "[ a:P; b:Q ] ==> <a,b> : P&Q" and 

101 
conjunct1: "p:P&Q ==> fst(p):P" and 

17480  102 
conjunct2: "p:P&Q ==> snd(p):Q" 
0  103 

104 
(* Disjunction *) 

105 

51306  106 
axiomatization where 
107 
disjI1: "a:P ==> inl(a):PQ" and 

108 
disjI2: "b:Q ==> inr(b):PQ" and 

17480  109 
disjE: "[ a:PQ; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R 
110 
] ==> when(a,f,g):R" 

0  111 

112 
(* Implication *) 

113 

51306  114 
axiomatization where 
115 
impI: "\<And>P Q f. (!!x. x:P ==> f(x):Q) ==> lam x. f(x):P>Q" and 

116 
mp: "\<And>P Q f. [ f:P>Q; a:P ] ==> f`a:Q" 

0  117 

118 
(*Quantifiers*) 

119 

51306  120 
axiomatization where 
121 
allI: "\<And>P. (!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" and 

122 
spec: "\<And>P f. (f:ALL x. P(x)) ==> f^x : P(x)" 

0  123 

51306  124 
axiomatization where 
125 
exI: "p : P(x) ==> [x,p] : EX x. P(x)" and 

17480  126 
exE: "[ p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R ] ==> xsplit(p,f):R" 
0  127 

128 
(**** Equality between proofs ****) 

129 

51306  130 
axiomatization where 
131 
prefl: "a : P ==> a = a : P" and 

132 
psym: "a = b : P ==> b = a : P" and 

17480  133 
ptrans: "[ a = b : P; b = c : P ] ==> a = c : P" 
0  134 

51306  135 
axiomatization where 
17480  136 
idpeelB: "[ !!x. f(x) : P(x,x) ] ==> idpeel(ideq(a),f) = f(a) : P(a,a)" 
0  137 

51306  138 
axiomatization where 
139 
fstB: "a:P ==> fst(<a,b>) = a : P" and 

140 
sndB: "b:Q ==> snd(<a,b>) = b : Q" and 

17480  141 
pairEC: "p:P&Q ==> p = <fst(p),snd(p)> : P&Q" 
0  142 

51306  143 
axiomatization where 
144 
whenBinl: "[ a:P; !!x. x:P ==> f(x) : Q ] ==> when(inl(a),f,g) = f(a) : Q" and 

145 
whenBinr: "[ b:P; !!x. x:P ==> g(x) : Q ] ==> when(inr(b),f,g) = g(b) : Q" and 

17480  146 
plusEC: "a:PQ ==> when(a,%x. inl(x),%y. inr(y)) = a : PQ" 
0  147 

51306  148 
axiomatization where 
149 
applyB: "[ a:P; !!x. x:P ==> b(x) : Q ] ==> (lam x. b(x)) ` a = b(a) : Q" and 

17480  150 
funEC: "f:P ==> f = lam x. f`x : P" 
0  151 

51306  152 
axiomatization where 
17480  153 
specB: "[ !!x. f(x) : P(x) ] ==> (all x. f(x)) ^ a = f(a) : P(a)" 
0  154 

155 

156 
(**** Definitions ****) 

157 

62147  158 
definition Not :: "o => o" ("~ _" [40] 40) 
159 
where not_def: "~P == P>False" 

160 

161 
definition iff :: "[o,o] => o" (infixr "<>" 25) 

162 
where "P<>Q == (P>Q) & (Q>P)" 

0  163 

164 
(*Unique existence*) 

62147  165 
definition Ex1 :: "('a => o) => o" (binder "EX! " 10) 
166 
where ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 

0  167 

168 
(*Rewriting  special constants to flag normalized terms and formulae*) 

51306  169 
axiomatization where 
170 
norm_eq: "nrm : norm(x) = x" and 

17480  171 
NORM_iff: "NRM : NORM(P) <> P" 
172 

26322  173 
(*** Sequentstyle elimination rules for & > and ALL ***) 
174 

61337  175 
schematic_goal conjE: 
26322  176 
assumes "p:P&Q" 
177 
and "!!x y.[ x:P; y:Q ] ==> f(x,y):R" 

178 
shows "?a:R" 

179 
apply (rule assms(2)) 

180 
apply (rule conjunct1 [OF assms(1)]) 

181 
apply (rule conjunct2 [OF assms(1)]) 

182 
done 

183 

61337  184 
schematic_goal impE: 
26322  185 
assumes "p:P>Q" 
186 
and "q:P" 

187 
and "!!x. x:Q ==> r(x):R" 

188 
shows "?p:R" 

189 
apply (rule assms mp)+ 

190 
done 

191 

61337  192 
schematic_goal allE: 
26322  193 
assumes "p:ALL x. P(x)" 
194 
and "!!y. y:P(x) ==> q(y):R" 

195 
shows "?p:R" 

196 
apply (rule assms spec)+ 

197 
done 

198 

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

61337  200 
schematic_goal all_dupE: 
26322  201 
assumes "p:ALL x. P(x)" 
202 
and "!!y z.[ y:P(x); z:ALL x. P(x) ] ==> q(y,z):R" 

203 
shows "?p:R" 

204 
apply (rule assms spec)+ 

205 
done 

206 

207 

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

209 

61337  210 
schematic_goal notI: 
26322  211 
assumes "!!x. x:P ==> q(x):False" 
212 
shows "?p:~P" 

213 
unfolding not_def 

214 
apply (assumption  rule assms impI)+ 

215 
done 

216 

61337  217 
schematic_goal notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R" 
26322  218 
unfolding not_def 
219 
apply (drule (1) mp) 

220 
apply (erule FalseE) 

221 
done 

222 

223 
(*This is useful with the special implication rules for each kind of P. *) 

61337  224 
schematic_goal not_to_imp: 
26322  225 
assumes "p:~P" 
226 
and "!!x. x:(P>False) ==> q(x):Q" 

227 
shows "?p:Q" 

228 
apply (assumption  rule assms impI notE)+ 

229 
done 

230 

231 
(* For substitution int an assumption P, reduce Q to P>Q, substitute into 

27150  232 
this implication, then apply impI to move P back into the assumptions.*) 
61337  233 
schematic_goal rev_mp: "[ p:P; q:P > Q ] ==> ?p:Q" 
26322  234 
apply (assumption  rule mp)+ 
235 
done 

236 

237 

238 
(*Contrapositive of an inference rule*) 

61337  239 
schematic_goal contrapos: 
26322  240 
assumes major: "p:~Q" 
241 
and minor: "!!y. y:P==>q(y):Q" 

242 
shows "?a:~P" 

243 
apply (rule major [THEN notE, THEN notI]) 

244 
apply (erule minor) 

245 
done 

246 

247 
(** Unique assumption tactic. 

248 
Ignores proof objects. 

249 
Fails unless one assumption is equal and exactly one is unifiable 

250 
**) 

251 

60770  252 
ML \<open> 
26322  253 
local 
69593  254 
fun discard_proof (Const (\<^const_name>\<open>Proof\<close>, _) $ P $ _) = P; 
26322  255 
in 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

256 
fun uniq_assume_tac ctxt = 
26322  257 
SUBGOAL 
258 
(fn (prem,i) => 

259 
let val hyps = map discard_proof (Logic.strip_assums_hyp prem) 

260 
and concl = discard_proof (Logic.strip_assums_concl prem) 

261 
in 

262 
if exists (fn hyp => hyp aconv concl) hyps 

67405
e9ab4ad7bd15
uniform use of Standard ML opinfix  eliminated warnings;
wenzelm
parents:
67399
diff
changeset

263 
then case distinct (op =) (filter (fn hyp => Term.could_unify (hyp, concl)) hyps) of 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

264 
[_] => assume_tac ctxt i 
26322  265 
 _ => no_tac 
266 
else no_tac 

267 
end); 

268 
end; 

60770  269 
\<close> 
26322  270 

271 

272 
(*** Modus Ponens Tactics ***) 

273 

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

60770  275 
ML \<open> 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

276 
fun mp_tac ctxt i = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

277 
eresolve_tac ctxt [@{thm notE}, make_elim @{thm mp}] i THEN assume_tac ctxt i 
60770  278 
\<close> 
59529  279 
method_setup mp = \<open>Scan.succeed (SIMPLE_METHOD' o mp_tac)\<close> 
26322  280 

281 
(*Like mp_tac but instantiates no variables*) 

60770  282 
ML \<open> 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

283 
fun int_uniq_mp_tac ctxt i = 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset

284 
eresolve_tac ctxt [@{thm notE}, @{thm impE}] i THEN uniq_assume_tac ctxt i 
60770  285 
\<close> 
26322  286 

287 

288 
(*** Ifandonlyif ***) 

289 

61337  290 
schematic_goal iffI: 
26322  291 
assumes "!!x. x:P ==> q(x):Q" 
292 
and "!!x. x:Q ==> r(x):P" 

293 
shows "?p:P<>Q" 

294 
unfolding iff_def 

295 
apply (assumption  rule assms conjI impI)+ 

296 
done 

297 

298 

61337  299 
schematic_goal iffE: 
26322  300 
assumes "p:P <> Q" 
301 
and "!!x y.[ x:P>Q; y:Q>P ] ==> q(x,y):R" 

302 
shows "?p:R" 

303 
apply (rule conjE) 

304 
apply (rule assms(1) [unfolded iff_def]) 

305 
apply (rule assms(2)) 

306 
apply assumption+ 

307 
done 

308 

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

310 

61337  311 
schematic_goal iffD1: "[ p:P <> Q; q:P ] ==> ?p:Q" 
26322  312 
unfolding iff_def 
313 
apply (rule conjunct1 [THEN mp], assumption+) 

314 
done 

315 

61337  316 
schematic_goal iffD2: "[ p:P <> Q; q:Q ] ==> ?p:P" 
26322  317 
unfolding iff_def 
318 
apply (rule conjunct2 [THEN mp], assumption+) 

319 
done 

320 

61337  321 
schematic_goal iff_refl: "?p:P <> P" 
26322  322 
apply (rule iffI) 
323 
apply assumption+ 

324 
done 

325 

61337  326 
schematic_goal iff_sym: "p:Q <> P ==> ?p:P <> Q" 
26322  327 
apply (erule iffE) 
328 
apply (rule iffI) 

329 
apply (erule (1) mp)+ 

330 
done 

331 

61337  332 
schematic_goal iff_trans: "[ p:P <> Q; q:Q<> R ] ==> ?p:P <> R" 
26322  333 
apply (rule iffI) 
334 
apply (assumption  erule iffE  erule (1) impE)+ 

335 
done 

336 

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

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

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

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

341 
***) 

342 

61337  343 
schematic_goal ex1I: 
26322  344 
assumes "p:P(a)" 
345 
and "!!x u. u:P(x) ==> f(u) : x=a" 

346 
shows "?p:EX! x. P(x)" 

347 
unfolding ex1_def 

348 
apply (assumption  rule assms exI conjI allI impI)+ 

349 
done 

350 

61337  351 
schematic_goal ex1E: 
26322  352 
assumes "p:EX! x. P(x)" 
353 
and "!!x u v. [ u:P(x); v:ALL y. P(y) > y=x ] ==> f(x,u,v):R" 

354 
shows "?a : R" 

355 
apply (insert assms(1) [unfolded ex1_def]) 

356 
apply (erule exE conjE  assumption  rule assms(1))+ 

29305  357 
apply (erule assms(2), assumption) 
26322  358 
done 
359 

360 

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

362 

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

60770  364 
ML \<open> 
59529  365 
fun iff_tac ctxt prems i = 
366 
resolve_tac ctxt (prems RL [@{thm iffE}]) i THEN 

367 
REPEAT1 (eresolve_tac ctxt [asm_rl, @{thm mp}] i) 

60770  368 
\<close> 
26322  369 

59529  370 
method_setup iff = 
371 
\<open>Attrib.thms >> (fn prems => fn ctxt => SIMPLE_METHOD' (iff_tac ctxt prems))\<close> 

372 

61337  373 
schematic_goal conj_cong: 
26322  374 
assumes "p:P <> P'" 
375 
and "!!x. x:P' ==> q(x):Q <> Q'" 

376 
shows "?p:(P&Q) <> (P'&Q')" 

377 
apply (insert assms(1)) 

59529  378 
apply (assumption  rule iffI conjI  erule iffE conjE mp  iff assms)+ 
26322  379 
done 
380 

61337  381 
schematic_goal disj_cong: 
26322  382 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(PQ) <> (P'Q')" 
59529  383 
apply (erule iffE disjE disjI1 disjI2  assumption  rule iffI  mp)+ 
26322  384 
done 
385 

61337  386 
schematic_goal imp_cong: 
26322  387 
assumes "p:P <> P'" 
388 
and "!!x. x:P' ==> q(x):Q <> Q'" 

389 
shows "?p:(P>Q) <> (P'>Q')" 

390 
apply (insert assms(1)) 

59529  391 
apply (assumption  rule iffI impI  erule iffE  mp  iff assms)+ 
26322  392 
done 
393 

61337  394 
schematic_goal iff_cong: 
26322  395 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(P<>Q) <> (P'<>Q')" 
59529  396 
apply (erule iffE  assumption  rule iffI  mp)+ 
26322  397 
done 
398 

61337  399 
schematic_goal not_cong: 
26322  400 
"p:P <> P' ==> ?p:~P <> ~P'" 
59529  401 
apply (assumption  rule iffI notI  mp  erule iffE notE)+ 
26322  402 
done 
403 

61337  404 
schematic_goal all_cong: 
26322  405 
assumes "!!x. f(x):P(x) <> Q(x)" 
406 
shows "?p:(ALL x. P(x)) <> (ALL x. Q(x))" 

59529  407 
apply (assumption  rule iffI allI  mp  erule allE  iff assms)+ 
26322  408 
done 
409 

61337  410 
schematic_goal ex_cong: 
26322  411 
assumes "!!x. f(x):P(x) <> Q(x)" 
412 
shows "?p:(EX x. P(x)) <> (EX x. Q(x))" 

59529  413 
apply (erule exE  assumption  rule iffI exI  mp  iff assms)+ 
26322  414 
done 
415 

416 
(*NOT PROVED 

56199  417 
ML_Thms.bind_thm ("ex1_cong", prove_goal (the_context ()) 
26322  418 
"(!!x.f(x):P(x) <> Q(x)) ==> ?p:(EX! x.P(x)) <> (EX! x.Q(x))" 
419 
(fn prems => 

420 
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 

421 
ORELSE mp_tac 1 

422 
ORELSE iff_tac prems 1)) ])) 

423 
*) 

424 

425 
(*** Equality rules ***) 

426 

427 
lemmas refl = ieqI 

428 

61337  429 
schematic_goal subst: 
26322  430 
assumes prem1: "p:a=b" 
431 
and prem2: "q:P(a)" 

432 
shows "?p : P(b)" 

433 
apply (rule prem2 [THEN rev_mp]) 

434 
apply (rule prem1 [THEN ieqE]) 

435 
apply (rule impI) 

436 
apply assumption 

437 
done 

438 

61337  439 
schematic_goal sym: "q:a=b ==> ?c:b=a" 
26322  440 
apply (erule subst) 
441 
apply (rule refl) 

442 
done 

443 

61337  444 
schematic_goal trans: "[ p:a=b; q:b=c ] ==> ?d:a=c" 
26322  445 
apply (erule (1) subst) 
446 
done 

447 

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

61337  449 
schematic_goal not_sym: "p:~ b=a ==> ?q:~ a=b" 
26322  450 
apply (erule contrapos) 
451 
apply (erule sym) 

452 
done 

453 

61337  454 
schematic_goal ssubst: "p:b=a \<Longrightarrow> q:P(a) \<Longrightarrow> ?p:P(b)" 
45594  455 
apply (drule sym) 
456 
apply (erule subst) 

457 
apply assumption 

458 
done 

26322  459 

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

61337  461 
schematic_goal ex1_equalsE: "[ p:EX! x. P(x); q:P(a); r:P(b) ] ==> ?d:a=b" 
26322  462 
apply (erule ex1E) 
463 
apply (rule trans) 

464 
apply (rule_tac [2] sym) 

465 
apply (assumption  erule spec [THEN mp])+ 

466 
done 

467 

468 
(** Polymorphic congruence rules **) 

469 

61337  470 
schematic_goal subst_context: "[ p:a=b ] ==> ?d:t(a)=t(b)" 
26322  471 
apply (erule ssubst) 
472 
apply (rule refl) 

473 
done 

474 

61337  475 
schematic_goal subst_context2: "[ p:a=b; q:c=d ] ==> ?p:t(a,c)=t(b,d)" 
26322  476 
apply (erule ssubst)+ 
477 
apply (rule refl) 

478 
done 

479 

61337  480 
schematic_goal subst_context3: "[ p:a=b; q:c=d; r:e=f ] ==> ?p:t(a,c,e)=t(b,d,f)" 
26322  481 
apply (erule ssubst)+ 
482 
apply (rule refl) 

483 
done 

484 

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

486 
a = b 

487 
  

488 
c = d *) 

61337  489 
schematic_goal box_equals: "[ p:a=b; q:a=c; r:b=d ] ==> ?p:c=d" 
26322  490 
apply (rule trans) 
491 
apply (rule trans) 

492 
apply (rule sym) 

493 
apply assumption+ 

494 
done 

495 

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

61337  497 
schematic_goal simp_equals: "[ p:a=c; q:b=d; r:c=d ] ==> ?p:a=b" 
26322  498 
apply (rule trans) 
499 
apply (rule trans) 

500 
apply (assumption  rule sym)+ 

501 
done 

502 

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

504 

61337  505 
schematic_goal pred1_cong: "p:a=a' ==> ?p:P(a) <> P(a')" 
26322  506 
apply (rule iffI) 
60770  507 
apply (tactic \<open> 
69593  508 
DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE eresolve_tac \<^context> [@{thm subst}, @{thm ssubst}] 1)\<close>) 
26322  509 
done 
510 

61337  511 
schematic_goal pred2_cong: "[ p:a=a'; q:b=b' ] ==> ?p:P(a,b) <> P(a',b')" 
26322  512 
apply (rule iffI) 
60770  513 
apply (tactic \<open> 
69593  514 
DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE eresolve_tac \<^context> [@{thm subst}, @{thm ssubst}] 1)\<close>) 
26322  515 
done 
516 

61337  517 
schematic_goal pred3_cong: "[ p:a=a'; q:b=b'; r:c=c' ] ==> ?p:P(a,b,c) <> P(a',b',c')" 
26322  518 
apply (rule iffI) 
60770  519 
apply (tactic \<open> 
69593  520 
DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE eresolve_tac \<^context> [@{thm subst}, @{thm ssubst}] 1)\<close>) 
26322  521 
done 
522 

27152
192954a9a549
changed pred_congs: merely cover pred1_cong pred2_cong pred3_cong;
wenzelm
parents:
27150
diff
changeset

523 
lemmas pred_congs = pred1_cong pred2_cong pred3_cong 
26322  524 

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

67399  526 
lemmas eq_cong = pred2_cong [where P = "(=)"] 
26322  527 

528 

529 
(*** Simplifications of assumed implications. 

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

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

532 
intuitionistic propositional logic. See 

533 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

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

535 

61337  536 
schematic_goal conj_impE: 
26322  537 
assumes major: "p:(P&Q)>S" 
538 
and minor: "!!x. x:P>(Q>S) ==> q(x):R" 

539 
shows "?p:R" 

540 
apply (assumption  rule conjI impI major [THEN mp] minor)+ 

541 
done 

542 

61337  543 
schematic_goal disj_impE: 
26322  544 
assumes major: "p:(PQ)>S" 
545 
and minor: "!!x y.[ x:P>S; y:Q>S ] ==> q(x,y):R" 

546 
shows "?p:R" 

69593  547 
apply (tactic \<open>DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE 
548 
resolve_tac \<^context> [@{thm disjI1}, @{thm disjI2}, @{thm impI}, 

60770  549 
@{thm major} RS @{thm mp}, @{thm minor}] 1)\<close>) 
26322  550 
done 
551 

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

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

61337  554 
schematic_goal imp_impE: 
26322  555 
assumes major: "p:(P>Q)>S" 
556 
and r1: "!!x y.[ x:P; y:Q>S ] ==> q(x,y):Q" 

557 
and r2: "!!x. x:S ==> r(x):R" 

558 
shows "?p:R" 

559 
apply (assumption  rule impI major [THEN mp] r1 r2)+ 

560 
done 

561 

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

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

61337  564 
schematic_goal not_impE: 
26322  565 
assumes major: "p:~P > S" 
566 
and r1: "!!y. y:P ==> q(y):False" 

567 
and r2: "!!y. y:S ==> r(y):R" 

568 
shows "?p:R" 

569 
apply (assumption  rule notI impI major [THEN mp] r1 r2)+ 

570 
done 

571 

572 
(*Simplifies the implication. UNSAFE. *) 

61337  573 
schematic_goal iff_impE: 
26322  574 
assumes major: "p:(P<>Q)>S" 
575 
and r1: "!!x y.[ x:P; y:Q>S ] ==> q(x,y):Q" 

576 
and r2: "!!x y.[ x:Q; y:P>S ] ==> r(x,y):P" 

577 
and r3: "!!x. x:S ==> s(x):R" 

578 
shows "?p:R" 

579 
apply (assumption  rule iffI impI major [THEN mp] r1 r2 r3)+ 

580 
done 

581 

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

61337  583 
schematic_goal all_impE: 
26322  584 
assumes major: "p:(ALL x. P(x))>S" 
585 
and r1: "!!x. q:P(x)" 

586 
and r2: "!!y. y:S ==> r(y):R" 

587 
shows "?p:R" 

588 
apply (assumption  rule allI impI major [THEN mp] r1 r2)+ 

589 
done 

590 

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

61337  592 
schematic_goal ex_impE: 
26322  593 
assumes major: "p:(EX x. P(x))>S" 
594 
and r: "!!y. y:P(a)>S ==> q(y):R" 

595 
shows "?p:R" 

596 
apply (assumption  rule exI impI major [THEN mp] r)+ 

597 
done 

598 

599 

61337  600 
schematic_goal rev_cut_eq: 
26322  601 
assumes "p:a=b" 
602 
and "!!x. x:a=b ==> f(x):R" 

603 
shows "?p:R" 

604 
apply (rule assms)+ 

605 
done 

606 

607 
lemma thin_refl: "!!X. [p:x=x; PROP W] ==> PROP W" . 

608 

69605  609 
ML_file \<open>hypsubst.ML\<close> 
26322  610 

60770  611 
ML \<open> 
42799  612 
structure Hypsubst = Hypsubst 
613 
( 

26322  614 
(*Take apart an equality judgement; otherwise raise Match!*) 
69593  615 
fun dest_eq (Const (\<^const_name>\<open>Proof\<close>, _) $ 
616 
(Const (\<^const_name>\<open>eq\<close>, _) $ t $ u) $ _) = (t, u); 

26322  617 

618 
val imp_intr = @{thm impI} 

619 

620 
(*etac rev_cut_eq moves an equality to be the last premise. *) 

621 
val rev_cut_eq = @{thm rev_cut_eq} 

622 

623 
val rev_mp = @{thm rev_mp} 

624 
val subst = @{thm subst} 

625 
val sym = @{thm sym} 

626 
val thin_refl = @{thm thin_refl} 

42799  627 
); 
26322  628 
open Hypsubst; 
60770  629 
\<close> 
26322  630 

69605  631 
ML_file \<open>intprover.ML\<close> 
26322  632 

633 

634 
(*** Rewrite rules ***) 

635 

61337  636 
schematic_goal conj_rews: 
26322  637 
"?p1 : P & True <> P" 
638 
"?p2 : True & P <> P" 

639 
"?p3 : P & False <> False" 

640 
"?p4 : False & P <> False" 

641 
"?p5 : P & P <> P" 

642 
"?p6 : P & ~P <> False" 

643 
"?p7 : ~P & P <> False" 

644 
"?p8 : (P & Q) & R <> P & (Q & R)" 

69593  645 
apply (tactic \<open>fn st => IntPr.fast_tac \<^context> 1 st\<close>)+ 
26322  646 
done 
647 

61337  648 
schematic_goal disj_rews: 
26322  649 
"?p1 : P  True <> True" 
650 
"?p2 : True  P <> True" 

651 
"?p3 : P  False <> P" 

652 
"?p4 : False  P <> P" 

653 
"?p5 : P  P <> P" 

654 
"?p6 : (P  Q)  R <> P  (Q  R)" 

69593  655 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  656 
done 
657 

61337  658 
schematic_goal not_rews: 
26322  659 
"?p1 : ~ False <> True" 
660 
"?p2 : ~ True <> False" 

69593  661 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  662 
done 
663 

61337  664 
schematic_goal imp_rews: 
26322  665 
"?p1 : (P > False) <> ~P" 
666 
"?p2 : (P > True) <> True" 

667 
"?p3 : (False > P) <> True" 

668 
"?p4 : (True > P) <> P" 

669 
"?p5 : (P > P) <> True" 

670 
"?p6 : (P > ~P) <> ~P" 

69593  671 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  672 
done 
673 

61337  674 
schematic_goal iff_rews: 
26322  675 
"?p1 : (True <> P) <> P" 
676 
"?p2 : (P <> True) <> P" 

677 
"?p3 : (P <> P) <> True" 

678 
"?p4 : (False <> P) <> ~P" 

679 
"?p5 : (P <> False) <> ~P" 

69593  680 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  681 
done 
682 

61337  683 
schematic_goal quant_rews: 
26322  684 
"?p1 : (ALL x. P) <> P" 
685 
"?p2 : (EX x. P) <> P" 

69593  686 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  687 
done 
688 

689 
(*These are NOT supplied by default!*) 

61337  690 
schematic_goal distrib_rews1: 
26322  691 
"?p1 : ~(PQ) <> ~P & ~Q" 
692 
"?p2 : P & (Q  R) <> P&Q  P&R" 

693 
"?p3 : (Q  R) & P <> Q&P  R&P" 

694 
"?p4 : (P  Q > R) <> (P > R) & (Q > R)" 

69593  695 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  696 
done 
697 

61337  698 
schematic_goal distrib_rews2: 
26322  699 
"?p1 : ~(EX x. NORM(P(x))) <> (ALL x. ~NORM(P(x)))" 
700 
"?p2 : ((EX x. NORM(P(x))) > Q) <> (ALL x. NORM(P(x)) > Q)" 

701 
"?p3 : (EX x. NORM(P(x))) & NORM(Q) <> (EX x. NORM(P(x)) & NORM(Q))" 

702 
"?p4 : NORM(Q) & (EX x. NORM(P(x))) <> (EX x. NORM(Q) & NORM(P(x)))" 

69593  703 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>)+ 
26322  704 
done 
705 

706 
lemmas distrib_rews = distrib_rews1 distrib_rews2 

707 

61337  708 
schematic_goal P_Imp_P_iff_T: "p:P ==> ?p:(P <> True)" 
69593  709 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>) 
26322  710 
done 
711 

61337  712 
schematic_goal not_P_imp_P_iff_F: "p:~P ==> ?p:(P <> False)" 
69593  713 
apply (tactic \<open>IntPr.fast_tac \<^context> 1\<close>) 
26322  714 
done 
0  715 

716 
end 