src/FOLP/IFOLP.ML
changeset 3836 f1a1817659e6
parent 1459 d12da312eff4
child 9263 53e09e592278
equal deleted inserted replaced
3835:9a5a4e123859 3836:f1a1817659e6
    80   [ (REPEAT (resolve_tac prems 1
    80   [ (REPEAT (resolve_tac prems 1
    81       ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN
    81       ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN
    82               resolve_tac prems 1))) ]);
    82               resolve_tac prems 1))) ]);
    83 
    83 
    84 val impE = prove_goal IFOLP.thy 
    84 val impE = prove_goal IFOLP.thy 
    85     "[| p:P-->Q;  q:P;  !!x.x:Q ==> r(x):R |] ==> ?p:R"
    85     "[| p:P-->Q;  q:P;  !!x. x:Q ==> r(x):R |] ==> ?p:R"
    86  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    86  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    87 
    87 
    88 val allE = prove_goal IFOLP.thy 
    88 val allE = prove_goal IFOLP.thy 
    89     "[| p:ALL x.P(x); !!y.y:P(x) ==> q(y):R |] ==> ?p:R"
    89     "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"
    90  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    90  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    91 
    91 
    92 (*Duplicates the quantifier; for use with eresolve_tac*)
    92 (*Duplicates the quantifier; for use with eresolve_tac*)
    93 val all_dupE = prove_goal IFOLP.thy 
    93 val all_dupE = prove_goal IFOLP.thy 
    94     "[| p:ALL x.P(x);  !!y z.[| y:P(x); z:ALL x.P(x) |] ==> q(y,z):R \
    94     "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
    95 \    |] ==> ?p:R"
    95 \    |] ==> ?p:R"
    96  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    96  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    97 
    97 
    98 
    98 
    99 (*** Negation rules, which translate between ~P and P-->False ***)
    99 (*** Negation rules, which translate between ~P and P-->False ***)
   100 
   100 
   101 val notI = prove_goalw IFOLP.thy [not_def]  "(!!x.x:P ==> q(x):False) ==> ?p:~P"
   101 val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
   102  (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
   102  (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);
   103 
   103 
   104 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
   104 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P;  q:P |] ==> ?p:R"
   105  (fn prems=>
   105  (fn prems=>
   106   [ (resolve_tac [mp RS FalseE] 1),
   106   [ (resolve_tac [mp RS FalseE] 1),
   107     (REPEAT (resolve_tac prems 1)) ]);
   107     (REPEAT (resolve_tac prems 1)) ]);
   108 
   108 
   109 (*This is useful with the special implication rules for each kind of P. *)
   109 (*This is useful with the special implication rules for each kind of P. *)
   110 val not_to_imp = prove_goal IFOLP.thy 
   110 val not_to_imp = prove_goal IFOLP.thy 
   111     "[| p:~P;  !!x.x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
   111     "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
   112  (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
   112  (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
   113 
   113 
   114 
   114 
   115 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
   115 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
   116    this implication, then apply impI to move P back into the assumptions.
   116    this implication, then apply impI to move P back into the assumptions.
   119 val rev_mp = prove_goal IFOLP.thy "[| p:P;  q:P --> Q |] ==> ?p:Q"
   119 val rev_mp = prove_goal IFOLP.thy "[| p:P;  q:P --> Q |] ==> ?p:Q"
   120  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   120  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   121 
   121 
   122 
   122 
   123 (*Contrapositive of an inference rule*)
   123 (*Contrapositive of an inference rule*)
   124 val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y.y:P==>q(y):Q |] ==> ?a:~P"
   124 val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y. y:P==>q(y):Q |] ==> ?a:~P"
   125  (fn [major,minor]=> 
   125  (fn [major,minor]=> 
   126   [ (rtac (major RS notE RS notI) 1), 
   126   [ (rtac (major RS notE RS notI) 1), 
   127     (etac minor 1) ]);
   127     (etac minor 1) ]);
   128 
   128 
   129 (** Unique assumption tactic.
   129 (** Unique assumption tactic.
   159 
   159 
   160 
   160 
   161 (*** If-and-only-if ***)
   161 (*** If-and-only-if ***)
   162 
   162 
   163 val iffI = prove_goalw IFOLP.thy [iff_def]
   163 val iffI = prove_goalw IFOLP.thy [iff_def]
   164    "[| !!x.x:P ==> q(x):Q;  !!x.x:Q ==> r(x):P |] ==> ?p:P<->Q"
   164    "[| !!x. x:P ==> q(x):Q;  !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q"
   165  (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
   165  (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);
   166 
   166 
   167 
   167 
   168 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   168 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   169 val iffE = prove_goalw IFOLP.thy [iff_def]
   169 val iffE = prove_goalw IFOLP.thy [iff_def]
   199    EX!x,y such that P(x,y)                    (simultaneous)
   199    EX!x,y such that P(x,y)                    (simultaneous)
   200  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   200  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   201 ***)
   201 ***)
   202 
   202 
   203 val ex1I = prove_goalw IFOLP.thy [ex1_def]
   203 val ex1I = prove_goalw IFOLP.thy [ex1_def]
   204     "[| p:P(a);  !!x u.u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
   204     "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
   205  (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
   205  (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
   206 
   206 
   207 val ex1E = prove_goalw IFOLP.thy [ex1_def]
   207 val ex1E = prove_goalw IFOLP.thy [ex1_def]
   208     "[| p:EX! x.P(x);  \
   208     "[| p:EX! x. P(x);  \
   209 \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
   209 \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
   210 \    ?a : R"
   210 \    ?a : R"
   211  (fn prems =>
   211  (fn prems =>
   212   [ (cut_facts_tac prems 1),
   212   [ (cut_facts_tac prems 1),
   213     (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
   213     (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
   219 fun iff_tac prems i =
   219 fun iff_tac prems i =
   220     resolve_tac (prems RL [iffE]) i THEN
   220     resolve_tac (prems RL [iffE]) i THEN
   221     REPEAT1 (eresolve_tac [asm_rl,mp] i);
   221     REPEAT1 (eresolve_tac [asm_rl,mp] i);
   222 
   222 
   223 val conj_cong = prove_goal IFOLP.thy 
   223 val conj_cong = prove_goal IFOLP.thy 
   224     "[| p:P <-> P';  !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
   224     "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')"
   225  (fn prems =>
   225  (fn prems =>
   226   [ (cut_facts_tac prems 1),
   226   [ (cut_facts_tac prems 1),
   227     (REPEAT  (ares_tac [iffI,conjI] 1
   227     (REPEAT  (ares_tac [iffI,conjI] 1
   228       ORELSE  eresolve_tac [iffE,conjE,mp] 1
   228       ORELSE  eresolve_tac [iffE,conjE,mp] 1
   229       ORELSE  iff_tac prems 1)) ]);
   229       ORELSE  iff_tac prems 1)) ]);
   235     (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
   235     (REPEAT  (eresolve_tac [iffE,disjE,disjI1,disjI2] 1
   236       ORELSE  ares_tac [iffI] 1
   236       ORELSE  ares_tac [iffI] 1
   237       ORELSE  mp_tac 1)) ]);
   237       ORELSE  mp_tac 1)) ]);
   238 
   238 
   239 val imp_cong = prove_goal IFOLP.thy 
   239 val imp_cong = prove_goal IFOLP.thy 
   240     "[| p:P <-> P';  !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
   240     "[| p:P <-> P';  !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')"
   241  (fn prems =>
   241  (fn prems =>
   242   [ (cut_facts_tac prems 1),
   242   [ (cut_facts_tac prems 1),
   243     (REPEAT   (ares_tac [iffI,impI] 1
   243     (REPEAT   (ares_tac [iffI,impI] 1
   244       ORELSE  etac iffE 1
   244       ORELSE  etac iffE 1
   245       ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   245       ORELSE  mp_tac 1 ORELSE iff_tac prems 1)) ]);
   259     (REPEAT   (ares_tac [iffI,notI] 1
   259     (REPEAT   (ares_tac [iffI,notI] 1
   260       ORELSE  mp_tac 1
   260       ORELSE  mp_tac 1
   261       ORELSE  eresolve_tac [iffE,notE] 1)) ]);
   261       ORELSE  eresolve_tac [iffE,notE] 1)) ]);
   262 
   262 
   263 val all_cong = prove_goal IFOLP.thy 
   263 val all_cong = prove_goal IFOLP.thy 
   264     "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(ALL x.P(x)) <-> (ALL x.Q(x))"
   264     "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))"
   265  (fn prems =>
   265  (fn prems =>
   266   [ (REPEAT   (ares_tac [iffI,allI] 1
   266   [ (REPEAT   (ares_tac [iffI,allI] 1
   267       ORELSE   mp_tac 1
   267       ORELSE   mp_tac 1
   268       ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   268       ORELSE   etac allE 1 ORELSE iff_tac prems 1)) ]);
   269 
   269 
   270 val ex_cong = prove_goal IFOLP.thy 
   270 val ex_cong = prove_goal IFOLP.thy 
   271     "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))"
   271     "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))"
   272  (fn prems =>
   272  (fn prems =>
   273   [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   273   [ (REPEAT   (etac exE 1 ORELSE ares_tac [iffI,exI] 1
   274       ORELSE   mp_tac 1
   274       ORELSE   mp_tac 1
   275       ORELSE   iff_tac prems 1)) ]);
   275       ORELSE   iff_tac prems 1)) ]);
   276 
   276 
   304 (*calling "standard" reduces maxidx to 0*)
   304 (*calling "standard" reduces maxidx to 0*)
   305 val ssubst = standard (sym RS subst);
   305 val ssubst = standard (sym RS subst);
   306 
   306 
   307 (*A special case of ex1E that would otherwise need quantifier expansion*)
   307 (*A special case of ex1E that would otherwise need quantifier expansion*)
   308 val ex1_equalsE = prove_goal IFOLP.thy
   308 val ex1_equalsE = prove_goal IFOLP.thy
   309     "[| p:EX! x.P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   309     "[| p:EX! x. P(x);  q:P(a);  r:P(b) |] ==> ?d:a=b"
   310  (fn prems =>
   310  (fn prems =>
   311   [ (cut_facts_tac prems 1),
   311   [ (cut_facts_tac prems 1),
   312     (etac ex1E 1),
   312     (etac ex1E 1),
   313     (rtac trans 1),
   313     (rtac trans 1),
   314     (rtac sym 2),
   314     (rtac sym 2),
   393      intuitionistic propositional logic.  See
   393      intuitionistic propositional logic.  See
   394    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   394    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   395     (preprint, University of St Andrews, 1991)  ***)
   395     (preprint, University of St Andrews, 1991)  ***)
   396 
   396 
   397 val conj_impE = prove_goal IFOLP.thy 
   397 val conj_impE = prove_goal IFOLP.thy 
   398     "[| p:(P&Q)-->S;  !!x.x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
   398     "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
   399  (fn major::prems=>
   399  (fn major::prems=>
   400   [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   400   [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   401 
   401 
   402 val disj_impE = prove_goal IFOLP.thy 
   402 val disj_impE = prove_goal IFOLP.thy 
   403     "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R"
   403     "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R"
   405   [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]);
   405   [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]);
   406 
   406 
   407 (*Simplifies the implication.  Classical version is stronger. 
   407 (*Simplifies the implication.  Classical version is stronger. 
   408   Still UNSAFE since Q must be provable -- backtracking needed.  *)
   408   Still UNSAFE since Q must be provable -- backtracking needed.  *)
   409 val imp_impE = prove_goal IFOLP.thy 
   409 val imp_impE = prove_goal IFOLP.thy 
   410     "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x.x:S ==> r(x):R |] ==> \
   410     "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
   411 \    ?p:R"
   411 \    ?p:R"
   412  (fn major::prems=>
   412  (fn major::prems=>
   413   [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   413   [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   414 
   414 
   415 (*Simplifies the implication.  Classical version is stronger. 
   415 (*Simplifies the implication.  Classical version is stronger. 
   416   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   416   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   417 val not_impE = prove_goal IFOLP.thy
   417 val not_impE = prove_goal IFOLP.thy
   418     "[| p:~P --> S;  !!y.y:P ==> q(y):False;  !!y.y:S ==> r(y):R |] ==> ?p:R"
   418     "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R"
   419  (fn major::prems=>
   419  (fn major::prems=>
   420   [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   420   [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   421 
   421 
   422 (*Simplifies the implication.   UNSAFE.  *)
   422 (*Simplifies the implication.   UNSAFE.  *)
   423 val iff_impE = prove_goal IFOLP.thy 
   423 val iff_impE = prove_goal IFOLP.thy 
   424     "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
   424     "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
   425 \       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x.x:S ==> s(x):R |] ==> ?p:R"
   425 \       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R"
   426  (fn major::prems=>
   426  (fn major::prems=>
   427   [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   427   [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   428 
   428 
   429 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   429 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   430 val all_impE = prove_goal IFOLP.thy 
   430 val all_impE = prove_goal IFOLP.thy 
   431     "[| p:(ALL x.P(x))-->S;  !!x.q:P(x);  !!y.y:S ==> r(y):R |] ==> ?p:R"
   431     "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R"
   432  (fn major::prems=>
   432  (fn major::prems=>
   433   [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   433   [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   434 
   434 
   435 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   435 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   436 val ex_impE = prove_goal IFOLP.thy 
   436 val ex_impE = prove_goal IFOLP.thy 
   437     "[| p:(EX x.P(x))-->S;  !!y.y:P(a)-->S ==> q(y):R |] ==> ?p:R"
   437     "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"
   438  (fn major::prems=>
   438  (fn major::prems=>
   439   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   439   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   440 
   440 
   441 end;
   441 end;
   442 
   442