src/FOLP/IFOLP.ML
 changeset 17480 fd19f77dcf60 parent 15570 8d8c70b41bab child 18977 f24c416a4814
```--- a/src/FOLP/IFOLP.ML	Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/IFOLP.ML	Sun Sep 18 14:25:48 2005 +0200
@@ -2,29 +2,28 @@
ID:         \$Id\$
Author:     Martin D Coen, Cambridge University Computer Laboratory
Copyright   1992  University of Cambridge
+*)

-Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
-*)
(*** Sequent-style elimination rules for & --> and ALL ***)

-val prems= Goal
+val prems= Goal
"[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R";
by (REPEAT (resolve_tac prems 1
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ;
qed "conjE";

-val prems= Goal
+val prems= Goal
"[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R";
by (REPEAT (resolve_tac (prems@[mp]) 1)) ;
qed "impE";

-val prems= Goal
+val prems= Goal
"[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R";
by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
qed "allE";

(*Duplicates the quantifier; for use with eresolve_tac*)
-val prems= Goal
+val prems= Goal
"[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
\    |] ==> ?p:R";
by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
@@ -33,16 +32,16 @@

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

-val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
+val notI = prove_goalw (the_context ()) [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);

-val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
+val notE = prove_goalw (the_context ()) [not_def] "[| p:~P;  q:P |] ==> ?p:R"
(fn prems=>
[ (resolve_tac [mp RS FalseE] 1),
(REPEAT (resolve_tac prems 1)) ]);

(*This is useful with the special implication rules for each kind of P. *)
-val prems= Goal
+val prems= Goal
"[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q";
by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;
qed "not_to_imp";
@@ -65,7 +64,7 @@

(** Unique assumption tactic.
Ignores proof objects.
-    Fails unless one assumption is equal and exactly one is unifiable
+    Fails unless one assumption is equal and exactly one is unifiable
**)

local
@@ -76,7 +75,7 @@
(fn (prem,i) =>
let val hyps = map discard_proof (Logic.strip_assums_hyp prem)
and concl = discard_proof (Logic.strip_assums_concl prem)
-      in
+      in
if exists (fn hyp => hyp aconv concl) hyps
then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
[_] => assume_tac i
@@ -97,22 +96,22 @@

(*** If-and-only-if ***)

-val iffI = prove_goalw IFOLP.thy [iff_def]
+val iffI = prove_goalw (the_context ()) [iff_def]
"[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);

(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
-val iffE = prove_goalw IFOLP.thy [iff_def]
+val iffE = prove_goalw (the_context ()) [iff_def]
"[| p:P <-> Q;  !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R"
(fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);

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

-val iffD1 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
+val iffD1 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:P |] ==> ?p:Q"
(fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);

-val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
+val iffD2 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
(fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);

Goal "?p:P <-> P";
@@ -137,12 +136,12 @@
do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
***)

-val prems = goalw IFOLP.thy [ex1_def]
+val prems = goalw (the_context ()) [ex1_def]
"[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)";
by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
qed "ex1I";

-val prems = goalw IFOLP.thy [ex1_def]
+val prems = goalw (the_context ()) [ex1_def]
"[| p:EX! x. P(x);  \
\       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
\    ?a : R";
@@ -158,7 +157,7 @@
resolve_tac (prems RL [iffE]) i THEN
REPEAT1 (eresolve_tac [asm_rl,mp] i);

-val conj_cong = prove_goal IFOLP.thy
+val conj_cong = prove_goal (the_context ())
"[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -166,7 +165,7 @@
ORELSE  eresolve_tac [iffE,conjE,mp] 1
ORELSE  iff_tac prems 1)) ]);

-val disj_cong = prove_goal IFOLP.thy
+val disj_cong = prove_goal (the_context ())
"[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -174,7 +173,7 @@
ORELSE  ares_tac [iffI] 1
ORELSE  mp_tac 1)) ]);

-val imp_cong = prove_goal IFOLP.thy
+val imp_cong = prove_goal (the_context ())
"[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -182,7 +181,7 @@
ORELSE  etac iffE 1
ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);

-val iff_cong = prove_goal IFOLP.thy
+val iff_cong = prove_goal (the_context ())
"[| p:P <-> P';  q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -190,7 +189,7 @@
ORELSE  ares_tac [iffI] 1
ORELSE  mp_tac 1)) ]);

-val not_cong = prove_goal IFOLP.thy
+val not_cong = prove_goal (the_context ())
"p:P <-> P' ==> ?p:~P <-> ~P'"
(fn prems =>
[ (cut_facts_tac prems 1),
@@ -198,14 +197,14 @@
ORELSE  mp_tac 1
ORELSE  eresolve_tac [iffE,notE] 1)) ]);

-val all_cong = prove_goal IFOLP.thy
+val all_cong = prove_goal (the_context ())
"(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
(fn prems =>
[ (REPEAT   (ares_tac [iffI,allI] 1
ORELSE   mp_tac 1
ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);

-val ex_cong = prove_goal IFOLP.thy
+val ex_cong = prove_goal (the_context ())
"(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
(fn prems =>
[ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
@@ -213,7 +212,7 @@
ORELSE   iff_tac prems 1)) ]);

(*NOT PROVED
-val ex1_cong = prove_goal IFOLP.thy
+val ex1_cong = prove_goal (the_context ())
"(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
(fn prems =>
[ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1
@@ -225,8 +224,8 @@

val refl = ieqI;

-val subst = prove_goal IFOLP.thy "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
- (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
+val subst = prove_goal (the_context ()) "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
+ (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),
rtac impI 1, atac 1 ]);

Goal "q:a=b ==> ?c:b=a";
@@ -235,7 +234,7 @@
qed "sym";

Goal "[| p:a=b;  q:b=c |] ==> ?d:a=c";
-by (etac subst 1 THEN assume_tac 1);
+by (etac subst 1 THEN assume_tac 1);
qed "trans";

(** ~ b=a ==> ~ a=b **)
@@ -263,12 +262,12 @@
qed "subst_context";

Goal "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)";
-by (REPEAT (etac ssubst 1));
+by (REPEAT (etac ssubst 1));
by (rtac refl 1) ;
qed "subst_context2";

Goal "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)";
-by (REPEAT (etac ssubst 1));
+by (REPEAT (etac ssubst 1));
by (rtac refl 1) ;
qed "subst_context3";

@@ -309,8 +308,8 @@

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

-val pred_congs =
-    List.concat (map (fn c =>
+val pred_congs =
+    List.concat (map (fn c =>
map (fn th => read_instantiate [("P",c)] th)
[pred1_cong,pred2_cong,pred3_cong])
(explode"PQRS"));
@@ -321,30 +320,30 @@

(*** Simplifications of assumed implications.
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
-     used with mp_tac (restricted to atomic formulae) is COMPLETE for
+     used with mp_tac (restricted to atomic formulae) is COMPLETE for
intuitionistic propositional logic.  See
R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
(preprint, University of St Andrews, 1991)  ***)

-val major::prems= Goal
+val major::prems= Goal
"[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R";
by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ;
qed "conj_impE";

-val major::prems= Goal
+val major::prems= Goal
"[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R";
by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ;
qed "disj_impE";

-(*Simplifies the implication.  Classical version is stronger.
+(*Simplifies the implication.  Classical version is stronger.
Still UNSAFE since Q must be provable -- backtracking needed.  *)
-val major::prems= Goal
+val major::prems= Goal
"[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
\    ?p:R";
by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ;
qed "imp_impE";

-(*Simplifies the implication.  Classical version is stronger.
+(*Simplifies the implication.  Classical version is stronger.
Still UNSAFE since ~P must be provable -- backtracking needed.  *)
val major::prems= Goal
"[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R";
@@ -352,20 +351,20 @@
qed "not_impE";

(*Simplifies the implication.   UNSAFE.  *)
-val major::prems= Goal
+val major::prems= Goal
"[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
\       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R";
by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ;
qed "iff_impE";

(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
-val major::prems= Goal
+val major::prems= Goal
"[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R";
by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ;
qed "all_impE";

(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
-val major::prems= Goal
+val major::prems= Goal
"[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R";
by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ;
qed "ex_impE";```