src/FOLP/IFOLP.thy
 author wenzelm Sat Mar 29 19:14:00 2008 +0100 (2008-03-29) changeset 26480 544cef16045b parent 26322 eaf634e975fa child 26956 1309a6a0a29f permissions -rw-r--r--
replaced 'ML_setup' by 'ML';
1 (*  Title:      FOLP/IFOLP.thy
2     ID:         \$Id\$
3     Author:     Martin D Coen, Cambridge University Computer Laboratory
4     Copyright   1992  University of Cambridge
5 *)
7 header {* Intuitionistic First-Order Logic with Proofs *}
9 theory IFOLP
10 imports Pure
11 uses ("hypsubst.ML") ("intprover.ML")
12 begin
14 global
16 classes "term"
17 defaultsort "term"
19 typedecl p
20 typedecl o
22 consts
23       (*** Judgements ***)
24  "@Proof"       ::   "[p,o]=>prop"      ("(_ /: _)" [51,10] 5)
25  Proof          ::   "[o,p]=>prop"
26  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
28       (*** Logical Connectives -- Type Formers ***)
29  "="            ::      "['a,'a] => o"  (infixl 50)
30  True           ::      "o"
31  False          ::      "o"
32  Not            ::      "o => o"        ("~ _"  40)
33  "&"            ::      "[o,o] => o"    (infixr 35)
34  "|"            ::      "[o,o] => o"    (infixr 30)
35  "-->"          ::      "[o,o] => o"    (infixr 25)
36  "<->"          ::      "[o,o] => o"    (infixr 25)
37       (*Quantifiers*)
38  All            ::      "('a => o) => o"        (binder "ALL " 10)
39  Ex             ::      "('a => o) => o"        (binder "EX " 10)
40  Ex1            ::      "('a => o) => o"        (binder "EX! " 10)
42  NORM           ::      "o => o"
43  norm           ::      "'a => 'a"
45       (*** Proof Term Formers: precedence must exceed 50 ***)
46  tt             :: "p"
47  contr          :: "p=>p"
48  fst            :: "p=>p"
49  snd            :: "p=>p"
50  pair           :: "[p,p]=>p"           ("(1<_,/_>)")
51  split          :: "[p, [p,p]=>p] =>p"
52  inl            :: "p=>p"
53  inr            :: "p=>p"
54  when           :: "[p, p=>p, p=>p]=>p"
55  lambda         :: "(p => p) => p"      (binder "lam " 55)
56  "`"            :: "[p,p]=>p"           (infixl 60)
57  alll           :: "['a=>p]=>p"         (binder "all " 55)
58  "^"            :: "[p,'a]=>p"          (infixl 55)
59  exists         :: "['a,p]=>p"          ("(1[_,/_])")
60  xsplit         :: "[p,['a,p]=>p]=>p"
61  ideq           :: "'a=>p"
62  idpeel         :: "[p,'a=>p]=>p"
63  nrm            :: p
64  NRM            :: p
66 local
68 ML {*
70 (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
71 val show_proofs = ref false;
73 fun proof_tr [p,P] = Const (@{const_name Proof}, dummyT) \$ P \$ p;
75 fun proof_tr' [P,p] =
76     if !show_proofs then Const("@Proof",dummyT) \$ p \$ P
77     else P  (*this case discards the proof term*);
78 *}
80 parse_translation {* [("@Proof", proof_tr)] *}
81 print_translation {* [("Proof", proof_tr')] *}
83 axioms
85 (**** Propositional logic ****)
87 (*Equality*)
88 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
90 ieqI:      "ideq(a) : a=a"
91 ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
93 (* Truth and Falsity *)
95 TrueI:     "tt : True"
96 FalseE:    "a:False ==> contr(a):P"
98 (* Conjunction *)
100 conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
101 conjunct1: "p:P&Q ==> fst(p):P"
102 conjunct2: "p:P&Q ==> snd(p):Q"
104 (* Disjunction *)
106 disjI1:    "a:P ==> inl(a):P|Q"
107 disjI2:    "b:Q ==> inr(b):P|Q"
108 disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
109            |] ==> when(a,f,g):R"
111 (* Implication *)
113 impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
114 mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
116 (*Quantifiers*)
118 allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
119 spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
121 exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
122 exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
124 (**** Equality between proofs ****)
126 prefl:     "a : P ==> a = a : P"
127 psym:      "a = b : P ==> b = a : P"
128 ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
130 idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
132 fstB:      "a:P ==> fst(<a,b>) = a : P"
133 sndB:      "b:Q ==> snd(<a,b>) = b : Q"
134 pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
136 whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
137 whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
138 plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
140 applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
141 funEC:      "f:P ==> f = lam x. f`x : P"
143 specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
146 (**** Definitions ****)
148 not_def:              "~P == P-->False"
149 iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
151 (*Unique existence*)
152 ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
154 (*Rewriting -- special constants to flag normalized terms and formulae*)
155 norm_eq: "nrm : norm(x) = x"
156 NORM_iff:        "NRM : NORM(P) <-> P"
158 (*** Sequent-style elimination rules for & --> and ALL ***)
160 lemma conjE:
161   assumes "p:P&Q"
162     and "!!x y.[| x:P; y:Q |] ==> f(x,y):R"
163   shows "?a:R"
164   apply (rule assms(2))
165    apply (rule conjunct1 [OF assms(1)])
166   apply (rule conjunct2 [OF assms(1)])
167   done
169 lemma impE:
170   assumes "p:P-->Q"
171     and "q:P"
172     and "!!x. x:Q ==> r(x):R"
173   shows "?p:R"
174   apply (rule assms mp)+
175   done
177 lemma allE:
178   assumes "p:ALL x. P(x)"
179     and "!!y. y:P(x) ==> q(y):R"
180   shows "?p:R"
181   apply (rule assms spec)+
182   done
184 (*Duplicates the quantifier; for use with eresolve_tac*)
185 lemma all_dupE:
186   assumes "p:ALL x. P(x)"
187     and "!!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R"
188   shows "?p:R"
189   apply (rule assms spec)+
190   done
193 (*** Negation rules, which translate between ~P and P-->False ***)
195 lemma notI:
196   assumes "!!x. x:P ==> q(x):False"
197   shows "?p:~P"
198   unfolding not_def
199   apply (assumption | rule assms impI)+
200   done
202 lemma notE: "p:~P \<Longrightarrow> q:P \<Longrightarrow> ?p:R"
203   unfolding not_def
204   apply (drule (1) mp)
205   apply (erule FalseE)
206   done
208 (*This is useful with the special implication rules for each kind of P. *)
209 lemma not_to_imp:
210   assumes "p:~P"
211     and "!!x. x:(P-->False) ==> q(x):Q"
212   shows "?p:Q"
213   apply (assumption | rule assms impI notE)+
214   done
216 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
217    this implication, then apply impI to move P back into the assumptions.
218    To specify P use something like
219       eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
220 lemma rev_mp: "[| p:P;  q:P --> Q |] ==> ?p:Q"
221   apply (assumption | rule mp)+
222   done
225 (*Contrapositive of an inference rule*)
226 lemma contrapos:
227   assumes major: "p:~Q"
228     and minor: "!!y. y:P==>q(y):Q"
229   shows "?a:~P"
230   apply (rule major [THEN notE, THEN notI])
231   apply (erule minor)
232   done
234 (** Unique assumption tactic.
235     Ignores proof objects.
236     Fails unless one assumption is equal and exactly one is unifiable
237 **)
239 ML {*
240 local
241   fun discard_proof (Const (@{const_name Proof}, _) \$ P \$ _) = P;
242 in
243 val uniq_assume_tac =
244   SUBGOAL
245     (fn (prem,i) =>
246       let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
247           and concl = discard_proof (Logic.strip_assums_concl prem)
248       in
249           if exists (fn hyp => hyp aconv concl) hyps
250           then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
251                    [_] => assume_tac i
252                  |  _  => no_tac
253           else no_tac
254       end);
255 end;
256 *}
259 (*** Modus Ponens Tactics ***)
261 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
262 ML {*
263   fun mp_tac i = eresolve_tac [@{thm notE}, make_elim @{thm mp}] i  THEN  assume_tac i
264 *}
266 (*Like mp_tac but instantiates no variables*)
267 ML {*
268   fun int_uniq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  uniq_assume_tac i
269 *}
272 (*** If-and-only-if ***)
274 lemma iffI:
275   assumes "!!x. x:P ==> q(x):Q"
276     and "!!x. x:Q ==> r(x):P"
277   shows "?p:P<->Q"
278   unfolding iff_def
279   apply (assumption | rule assms conjI impI)+
280   done
283 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
285 lemma iffE:
286   assumes "p:P <-> Q"
287     and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
288   shows "?p:R"
289   apply (rule conjE)
290    apply (rule assms(1) [unfolded iff_def])
291   apply (rule assms(2))
292    apply assumption+
293   done
295 (* Destruct rules for <-> similar to Modus Ponens *)
297 lemma iffD1: "[| p:P <-> Q; q:P |] ==> ?p:Q"
298   unfolding iff_def
299   apply (rule conjunct1 [THEN mp], assumption+)
300   done
302 lemma iffD2: "[| p:P <-> Q; q:Q |] ==> ?p:P"
303   unfolding iff_def
304   apply (rule conjunct2 [THEN mp], assumption+)
305   done
307 lemma iff_refl: "?p:P <-> P"
308   apply (rule iffI)
309    apply assumption+
310   done
312 lemma iff_sym: "p:Q <-> P ==> ?p:P <-> Q"
313   apply (erule iffE)
314   apply (rule iffI)
315    apply (erule (1) mp)+
316   done
318 lemma iff_trans: "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
319   apply (rule iffI)
320    apply (assumption | erule iffE | erule (1) impE)+
321   done
323 (*** Unique existence.  NOTE THAT the following 2 quantifications
324    EX!x such that [EX!y such that P(x,y)]     (sequential)
325    EX!x,y such that P(x,y)                    (simultaneous)
326  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
327 ***)
329 lemma ex1I:
330   assumes "p:P(a)"
331     and "!!x u. u:P(x) ==> f(u) : x=a"
332   shows "?p:EX! x. P(x)"
333   unfolding ex1_def
334   apply (assumption | rule assms exI conjI allI impI)+
335   done
337 lemma ex1E:
338   assumes "p:EX! x. P(x)"
339     and "!!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R"
340   shows "?a : R"
341   apply (insert assms(1) [unfolded ex1_def])
342   apply (erule exE conjE | assumption | rule assms(1))+
343   done
346 (*** <-> congruence rules for simplification ***)
348 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
349 ML {*
350 fun iff_tac prems i =
351     resolve_tac (prems RL [@{thm iffE}]) i THEN
352     REPEAT1 (eresolve_tac [asm_rl, @{thm mp}] i)
353 *}
355 lemma conj_cong:
356   assumes "p:P <-> P'"
357     and "!!x. x:P' ==> q(x):Q <-> Q'"
358   shows "?p:(P&Q) <-> (P'&Q')"
359   apply (insert assms(1))
360   apply (assumption | rule iffI conjI |
361     erule iffE conjE mp | tactic {* iff_tac @{thms assms} 1 *})+
362   done
364 lemma disj_cong:
365   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
366   apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | tactic {* mp_tac 1 *})+
367   done
369 lemma imp_cong:
370   assumes "p:P <-> P'"
371     and "!!x. x:P' ==> q(x):Q <-> Q'"
372   shows "?p:(P-->Q) <-> (P'-->Q')"
373   apply (insert assms(1))
374   apply (assumption | rule iffI impI | erule iffE | tactic {* mp_tac 1 *} |
375     tactic {* iff_tac @{thms assms} 1 *})+
376   done
378 lemma iff_cong:
379   "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
380   apply (erule iffE | assumption | rule iffI | tactic {* mp_tac 1 *})+
381   done
383 lemma not_cong:
384   "p:P <-> P' ==> ?p:~P <-> ~P'"
385   apply (assumption | rule iffI notI | tactic {* mp_tac 1 *} | erule iffE notE)+
386   done
388 lemma all_cong:
389   assumes "!!x. f(x):P(x) <-> Q(x)"
390   shows "?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
391   apply (assumption | rule iffI allI | tactic {* mp_tac 1 *} | erule allE |
392     tactic {* iff_tac @{thms assms} 1 *})+
393   done
395 lemma ex_cong:
396   assumes "!!x. f(x):P(x) <-> Q(x)"
397   shows "?p:(EX x. P(x)) <-> (EX x. Q(x))"
398   apply (erule exE | assumption | rule iffI exI | tactic {* mp_tac 1 *} |
399     tactic {* iff_tac @{thms assms} 1 *})+
400   done
402 (*NOT PROVED
403 bind_thm ("ex1_cong", prove_goal (the_context ())
404     "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
405  (fn prems =>
406   [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
407       ORELSE   mp_tac 1
408       ORELSE   iff_tac prems 1)) ]))
409 *)
411 (*** Equality rules ***)
413 lemmas refl = ieqI
415 lemma subst:
416   assumes prem1: "p:a=b"
417     and prem2: "q:P(a)"
418   shows "?p : P(b)"
419   apply (rule prem2 [THEN rev_mp])
420   apply (rule prem1 [THEN ieqE])
421   apply (rule impI)
422   apply assumption
423   done
425 lemma sym: "q:a=b ==> ?c:b=a"
426   apply (erule subst)
427   apply (rule refl)
428   done
430 lemma trans: "[| p:a=b;  q:b=c |] ==> ?d:a=c"
431   apply (erule (1) subst)
432   done
434 (** ~ b=a ==> ~ a=b **)
435 lemma not_sym: "p:~ b=a ==> ?q:~ a=b"
436   apply (erule contrapos)
437   apply (erule sym)
438   done
440 (*calling "standard" reduces maxidx to 0*)
441 lemmas ssubst = sym [THEN subst, standard]
443 (*A special case of ex1E that would otherwise need quantifier expansion*)
444 lemma ex1_equalsE: "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
445   apply (erule ex1E)
446   apply (rule trans)
447    apply (rule_tac  sym)
448    apply (assumption | erule spec [THEN mp])+
449   done
451 (** Polymorphic congruence rules **)
453 lemma subst_context: "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
454   apply (erule ssubst)
455   apply (rule refl)
456   done
458 lemma subst_context2: "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
459   apply (erule ssubst)+
460   apply (rule refl)
461   done
463 lemma subst_context3: "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
464   apply (erule ssubst)+
465   apply (rule refl)
466   done
468 (*Useful with eresolve_tac for proving equalties from known equalities.
469         a = b
470         |   |
471         c = d   *)
472 lemma box_equals: "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"
473   apply (rule trans)
474    apply (rule trans)
475     apply (rule sym)
476     apply assumption+
477   done
479 (*Dual of box_equals: for proving equalities backwards*)
480 lemma simp_equals: "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"
481   apply (rule trans)
482    apply (rule trans)
483     apply (assumption | rule sym)+
484   done
486 (** Congruence rules for predicate letters **)
488 lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')"
489   apply (rule iffI)
490    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
491   done
493 lemma pred2_cong: "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
494   apply (rule iffI)
495    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
496   done
498 lemma pred3_cong: "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
499   apply (rule iffI)
500    apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE eresolve_tac [@{thm subst}, @{thm ssubst}] 1) *})
501   done
503 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
505 ML {*
506   bind_thms ("pred_congs",
507     flat (map (fn c =>
508                map (fn th => read_instantiate [("P",c)] th)
509                    [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
510                (explode"PQRS")))
511 *}
513 (*special case for the equality predicate!*)
514 lemmas eq_cong = pred2_cong [where P = "op =", standard]
517 (*** Simplifications of assumed implications.
518      Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
519      used with mp_tac (restricted to atomic formulae) is COMPLETE for
520      intuitionistic propositional logic.  See
521    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
522     (preprint, University of St Andrews, 1991)  ***)
524 lemma conj_impE:
525   assumes major: "p:(P&Q)-->S"
526     and minor: "!!x. x:P-->(Q-->S) ==> q(x):R"
527   shows "?p:R"
528   apply (assumption | rule conjI impI major [THEN mp] minor)+
529   done
531 lemma disj_impE:
532   assumes major: "p:(P|Q)-->S"
533     and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R"
534   shows "?p:R"
535   apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE
536       resolve_tac [@{thm disjI1}, @{thm disjI2}, @{thm impI},
537         @{thm major} RS @{thm mp}, @{thm minor}] 1) *})
538   done
540 (*Simplifies the implication.  Classical version is stronger.
541   Still UNSAFE since Q must be provable -- backtracking needed.  *)
542 lemma imp_impE:
543   assumes major: "p:(P-->Q)-->S"
544     and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
545     and r2: "!!x. x:S ==> r(x):R"
546   shows "?p:R"
547   apply (assumption | rule impI major [THEN mp] r1 r2)+
548   done
550 (*Simplifies the implication.  Classical version is stronger.
551   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
552 lemma not_impE:
553   assumes major: "p:~P --> S"
554     and r1: "!!y. y:P ==> q(y):False"
555     and r2: "!!y. y:S ==> r(y):R"
556   shows "?p:R"
557   apply (assumption | rule notI impI major [THEN mp] r1 r2)+
558   done
560 (*Simplifies the implication.   UNSAFE.  *)
561 lemma iff_impE:
562   assumes major: "p:(P<->Q)-->S"
563     and r1: "!!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q"
564     and r2: "!!x y.[| x:Q; y:P-->S |] ==> r(x,y):P"
565     and r3: "!!x. x:S ==> s(x):R"
566   shows "?p:R"
567   apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
568   done
570 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
571 lemma all_impE:
572   assumes major: "p:(ALL x. P(x))-->S"
573     and r1: "!!x. q:P(x)"
574     and r2: "!!y. y:S ==> r(y):R"
575   shows "?p:R"
576   apply (assumption | rule allI impI major [THEN mp] r1 r2)+
577   done
579 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
580 lemma ex_impE:
581   assumes major: "p:(EX x. P(x))-->S"
582     and r: "!!y. y:P(a)-->S ==> q(y):R"
583   shows "?p:R"
584   apply (assumption | rule exI impI major [THEN mp] r)+
585   done
588 lemma rev_cut_eq:
589   assumes "p:a=b"
590     and "!!x. x:a=b ==> f(x):R"
591   shows "?p:R"
592   apply (rule assms)+
593   done
595 lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" .
597 use "hypsubst.ML"
599 ML {*
601 (*** Applying HypsubstFun to generate hyp_subst_tac ***)
603 structure Hypsubst_Data =
604 struct
605   (*Take apart an equality judgement; otherwise raise Match!*)
606   fun dest_eq (Const (@{const_name Proof}, _) \$
607     (Const (@{const_name "op ="}, _)  \$ t \$ u) \$ _) = (t, u);
609   val imp_intr = @{thm impI}
611   (*etac rev_cut_eq moves an equality to be the last premise. *)
612   val rev_cut_eq = @{thm rev_cut_eq}
614   val rev_mp = @{thm rev_mp}
615   val subst = @{thm subst}
616   val sym = @{thm sym}
617   val thin_refl = @{thm thin_refl}
618 end;
620 structure Hypsubst = HypsubstFun(Hypsubst_Data);
621 open Hypsubst;
622 *}
624 use "intprover.ML"
627 (*** Rewrite rules ***)
629 lemma conj_rews:
630   "?p1 : P & True <-> P"
631   "?p2 : True & P <-> P"
632   "?p3 : P & False <-> False"
633   "?p4 : False & P <-> False"
634   "?p5 : P & P <-> P"
635   "?p6 : P & ~P <-> False"
636   "?p7 : ~P & P <-> False"
637   "?p8 : (P & Q) & R <-> P & (Q & R)"
638   apply (tactic {* fn st => IntPr.fast_tac 1 st *})+
639   done
641 lemma disj_rews:
642   "?p1 : P | True <-> True"
643   "?p2 : True | P <-> True"
644   "?p3 : P | False <-> P"
645   "?p4 : False | P <-> P"
646   "?p5 : P | P <-> P"
647   "?p6 : (P | Q) | R <-> P | (Q | R)"
648   apply (tactic {* IntPr.fast_tac 1 *})+
649   done
651 lemma not_rews:
652   "?p1 : ~ False <-> True"
653   "?p2 : ~ True <-> False"
654   apply (tactic {* IntPr.fast_tac 1 *})+
655   done
657 lemma imp_rews:
658   "?p1 : (P --> False) <-> ~P"
659   "?p2 : (P --> True) <-> True"
660   "?p3 : (False --> P) <-> True"
661   "?p4 : (True --> P) <-> P"
662   "?p5 : (P --> P) <-> True"
663   "?p6 : (P --> ~P) <-> ~P"
664   apply (tactic {* IntPr.fast_tac 1 *})+
665   done
667 lemma iff_rews:
668   "?p1 : (True <-> P) <-> P"
669   "?p2 : (P <-> True) <-> P"
670   "?p3 : (P <-> P) <-> True"
671   "?p4 : (False <-> P) <-> ~P"
672   "?p5 : (P <-> False) <-> ~P"
673   apply (tactic {* IntPr.fast_tac 1 *})+
674   done
676 lemma quant_rews:
677   "?p1 : (ALL x. P) <-> P"
678   "?p2 : (EX x. P) <-> P"
679   apply (tactic {* IntPr.fast_tac 1 *})+
680   done
682 (*These are NOT supplied by default!*)
683 lemma distrib_rews1:
684   "?p1 : ~(P|Q) <-> ~P & ~Q"
685   "?p2 : P & (Q | R) <-> P&Q | P&R"
686   "?p3 : (Q | R) & P <-> Q&P | R&P"
687   "?p4 : (P | Q --> R) <-> (P --> R) & (Q --> R)"
688   apply (tactic {* IntPr.fast_tac 1 *})+
689   done
691 lemma distrib_rews2:
692   "?p1 : ~(EX x. NORM(P(x))) <-> (ALL x. ~NORM(P(x)))"
693   "?p2 : ((EX x. NORM(P(x))) --> Q) <-> (ALL x. NORM(P(x)) --> Q)"
694   "?p3 : (EX x. NORM(P(x))) & NORM(Q) <-> (EX x. NORM(P(x)) & NORM(Q))"
695   "?p4 : NORM(Q) & (EX x. NORM(P(x))) <-> (EX x. NORM(Q) & NORM(P(x)))"
696   apply (tactic {* IntPr.fast_tac 1 *})+
697   done
699 lemmas distrib_rews = distrib_rews1 distrib_rews2
701 lemma P_Imp_P_iff_T: "p:P ==> ?p:(P <-> True)"
702   apply (tactic {* IntPr.fast_tac 1 *})
703   done
705 lemma not_P_imp_P_iff_F: "p:~P ==> ?p:(P <-> False)"
706   apply (tactic {* IntPr.fast_tac 1 *})
707   done
709 end