src/FOLP/IFOLP.ML
changeset 9263 53e09e592278
parent 3836 f1a1817659e6
child 15570 8d8c70b41bab
equal deleted inserted replaced
9262:8baf94ddb345 9263:53e09e592278
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     3     Author:     Martin D Coen, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
     6 Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs)
     7 *)
     7 *)
     8 
       
     9 open IFOLP;
       
    10 
       
    11 signature IFOLP_LEMMAS = 
       
    12   sig
       
    13   val allE: thm
       
    14   val all_cong: thm
       
    15   val all_dupE: thm
       
    16   val all_impE: thm
       
    17   val box_equals: thm
       
    18   val conjE: thm
       
    19   val conj_cong: thm
       
    20   val conj_impE: thm
       
    21   val contrapos: thm
       
    22   val disj_cong: thm
       
    23   val disj_impE: thm
       
    24   val eq_cong: thm
       
    25   val ex1I: thm
       
    26   val ex1E: thm
       
    27   val ex1_equalsE: thm
       
    28 (*  val ex1_cong: thm****)
       
    29   val ex_cong: thm
       
    30   val ex_impE: thm
       
    31   val iffD1: thm
       
    32   val iffD2: thm
       
    33   val iffE: thm
       
    34   val iffI: thm
       
    35   val iff_cong: thm
       
    36   val iff_impE: thm
       
    37   val iff_refl: thm
       
    38   val iff_sym: thm
       
    39   val iff_trans: thm
       
    40   val impE: thm
       
    41   val imp_cong: thm
       
    42   val imp_impE: thm
       
    43   val mp_tac: int -> tactic
       
    44   val notE: thm
       
    45   val notI: thm
       
    46   val not_cong: thm
       
    47   val not_impE: thm
       
    48   val not_sym: thm
       
    49   val not_to_imp: thm
       
    50   val pred1_cong: thm
       
    51   val pred2_cong: thm
       
    52   val pred3_cong: thm
       
    53   val pred_congs: thm list
       
    54   val refl: thm
       
    55   val rev_mp: thm
       
    56   val simp_equals: thm
       
    57   val subst: thm
       
    58   val ssubst: thm
       
    59   val subst_context: thm
       
    60   val subst_context2: thm
       
    61   val subst_context3: thm
       
    62   val sym: thm
       
    63   val trans: thm
       
    64   val TrueI: thm
       
    65   val uniq_assume_tac: int -> tactic
       
    66   val uniq_mp_tac: int -> tactic
       
    67   end;
       
    68 
       
    69 
       
    70 structure IFOLP_Lemmas : IFOLP_LEMMAS =
       
    71 struct
       
    72 
       
    73 val TrueI = TrueI;
       
    74 
       
    75 (*** Sequent-style elimination rules for & --> and ALL ***)
     8 (*** Sequent-style elimination rules for & --> and ALL ***)
    76 
     9 
    77 val conjE = prove_goal IFOLP.thy 
    10 val prems= Goal 
    78     "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R"
    11     "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R";
    79  (fn prems=>
    12 by (REPEAT (resolve_tac prems 1
    80   [ (REPEAT (resolve_tac prems 1
    13    ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ;
    81       ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN
    14 qed "conjE";
    82               resolve_tac prems 1))) ]);
    15 
    83 
    16 val prems= Goal 
    84 val impE = prove_goal IFOLP.thy 
    17     "[| 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"
    18 by (REPEAT (resolve_tac (prems@[mp]) 1)) ;
    86  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    19 qed "impE";
    87 
    20 
    88 val allE = prove_goal IFOLP.thy 
    21 val prems= Goal 
    89     "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"
    22     "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R";
    90  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    23 by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
       
    24 qed "allE";
    91 
    25 
    92 (*Duplicates the quantifier; for use with eresolve_tac*)
    26 (*Duplicates the quantifier; for use with eresolve_tac*)
    93 val all_dupE = prove_goal IFOLP.thy 
    27 val prems= Goal 
    94     "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
    28     "[| p:ALL x. P(x);  !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \
    95 \    |] ==> ?p:R"
    29 \    |] ==> ?p:R";
    96  (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);
    30 by (REPEAT (resolve_tac (prems@[spec]) 1)) ;
       
    31 qed "all_dupE";
    97 
    32 
    98 
    33 
    99 (*** Negation rules, which translate between ~P and P-->False ***)
    34 (*** Negation rules, which translate between ~P and P-->False ***)
   100 
    35 
   101 val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
    36 val notI = prove_goalw IFOLP.thy [not_def]  "(!!x. x:P ==> q(x):False) ==> ?p:~P"
   105  (fn prems=>
    40  (fn prems=>
   106   [ (resolve_tac [mp RS FalseE] 1),
    41   [ (resolve_tac [mp RS FalseE] 1),
   107     (REPEAT (resolve_tac prems 1)) ]);
    42     (REPEAT (resolve_tac prems 1)) ]);
   108 
    43 
   109 (*This is useful with the special implication rules for each kind of P. *)
    44 (*This is useful with the special implication rules for each kind of P. *)
   110 val not_to_imp = prove_goal IFOLP.thy 
    45 val prems= Goal 
   111     "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"
    46     "[| p:~P;  !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q";
   112  (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);
    47 by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;
       
    48 qed "not_to_imp";
   113 
    49 
   114 
    50 
   115 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into
    51 (* 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.
    52    this implication, then apply impI to move P back into the assumptions.
   117    To specify P use something like
    53    To specify P use something like
   118       eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
    54       eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
   119 val rev_mp = prove_goal IFOLP.thy "[| p:P;  q:P --> Q |] ==> ?p:Q"
    55 Goal "[| p:P;  q:P --> Q |] ==> ?p:Q";
   120  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
    56 by (REPEAT (ares_tac [mp] 1)) ;
       
    57 qed "rev_mp";
   121 
    58 
   122 
    59 
   123 (*Contrapositive of an inference rule*)
    60 (*Contrapositive of an inference rule*)
   124 val contrapos = prove_goal IFOLP.thy "[| p:~Q;  !!y. y:P==>q(y):Q |] ==> ?a:~P"
    61 val [major,minor]= Goal "[| p:~Q;  !!y. y:P==>q(y):Q |] ==> ?a:~P";
   125  (fn [major,minor]=> 
    62 by (rtac (major RS notE RS notI) 1);
   126   [ (rtac (major RS notE RS notI) 1), 
    63 by (etac minor 1) ;
   127     (etac minor 1) ]);
    64 qed "contrapos";
   128 
    65 
   129 (** Unique assumption tactic.
    66 (** Unique assumption tactic.
   130     Ignores proof objects.
    67     Ignores proof objects.
   131     Fails unless one assumption is equal and exactly one is unifiable 
    68     Fails unless one assumption is equal and exactly one is unifiable 
   132 **)
    69 **)
   153 
    90 
   154 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
    91 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   155 fun mp_tac i = eresolve_tac [notE,make_elim mp] i  THEN  assume_tac i;
    92 fun mp_tac i = eresolve_tac [notE,make_elim mp] i  THEN  assume_tac i;
   156 
    93 
   157 (*Like mp_tac but instantiates no variables*)
    94 (*Like mp_tac but instantiates no variables*)
   158 fun uniq_mp_tac i = eresolve_tac [notE,impE] i  THEN  uniq_assume_tac i;
    95 fun int_uniq_mp_tac i = eresolve_tac [notE,impE] i  THEN  uniq_assume_tac i;
   159 
    96 
   160 
    97 
   161 (*** If-and-only-if ***)
    98 (*** If-and-only-if ***)
   162 
    99 
   163 val iffI = prove_goalw IFOLP.thy [iff_def]
   100 val iffI = prove_goalw IFOLP.thy [iff_def]
   176  (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   113  (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   177 
   114 
   178 val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
   115 val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q;  q:Q |] ==> ?p:P"
   179  (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   116  (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);
   180 
   117 
   181 val iff_refl = prove_goal IFOLP.thy "?p:P <-> P"
   118 Goal "?p:P <-> P";
   182  (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]);
   119 by (REPEAT (ares_tac [iffI] 1)) ;
   183 
   120 qed "iff_refl";
   184 val iff_sym = prove_goal IFOLP.thy "p:Q <-> P ==> ?p:P <-> Q"
   121 
   185  (fn [major] =>
   122 Goal "p:Q <-> P ==> ?p:P <-> Q";
   186   [ (rtac (major RS iffE) 1),
   123 by (etac iffE 1);
   187     (rtac iffI 1),
   124 by (rtac iffI 1);
   188     (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]);
   125 by (REPEAT (eresolve_tac [asm_rl,mp] 1)) ;
   189 
   126 qed "iff_sym";
   190 val iff_trans = prove_goal IFOLP.thy "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R"
   127 
   191  (fn prems =>
   128 Goal "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R";
   192   [ (cut_facts_tac prems 1),
   129 by (rtac iffI 1);
   193     (rtac iffI 1),
   130 by (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ;
   194     (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]);
   131 qed "iff_trans";
   195 
   132 
   196 
   133 
   197 (*** Unique existence.  NOTE THAT the following 2 quantifications
   134 (*** Unique existence.  NOTE THAT the following 2 quantifications
   198    EX!x such that [EX!y such that P(x,y)]     (sequential)
   135    EX!x such that [EX!y such that P(x,y)]     (sequential)
   199    EX!x,y such that P(x,y)                    (simultaneous)
   136    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.
   137  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   201 ***)
   138 ***)
   202 
   139 
   203 val ex1I = prove_goalw IFOLP.thy [ex1_def]
   140 val prems = goalw IFOLP.thy [ex1_def]
   204     "[| p:P(a);  !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"
   141     "[| 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)) ]);
   142 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;
   206 
   143 qed "ex1I";
   207 val ex1E = prove_goalw IFOLP.thy [ex1_def]
   144 
       
   145 val prems = goalw IFOLP.thy [ex1_def]
   208     "[| p:EX! x. P(x);  \
   146     "[| p:EX! x. P(x);  \
   209 \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
   147 \       !!x u v. [| u:P(x);  v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\
   210 \    ?a : R"
   148 \    ?a : R";
   211  (fn prems =>
   149 by (cut_facts_tac prems 1);
   212   [ (cut_facts_tac prems 1),
   150 by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ;
   213     (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]);
   151 qed "ex1E";
   214 
   152 
   215 
   153 
   216 (*** <-> congruence rules for simplification ***)
   154 (*** <-> congruence rules for simplification ***)
   217 
   155 
   218 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   156 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   289 
   227 
   290 val subst = prove_goal IFOLP.thy "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
   228 val subst = prove_goal IFOLP.thy "[| p:a=b;  q:P(a) |] ==> ?p : P(b)"
   291  (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1), 
   229  (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1), 
   292                         rtac impI 1, atac 1 ]);
   230                         rtac impI 1, atac 1 ]);
   293 
   231 
   294 val sym = prove_goal IFOLP.thy "q:a=b ==> ?c:b=a"
   232 Goal "q:a=b ==> ?c:b=a";
   295  (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]);
   233 by (etac subst 1);
   296 
   234 by (rtac refl 1) ;
   297 val trans = prove_goal IFOLP.thy "[| p:a=b;  q:b=c |] ==> ?d:a=c"
   235 qed "sym";
   298  (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);
   236 
       
   237 Goal "[| p:a=b;  q:b=c |] ==> ?d:a=c";
       
   238 by (etac subst 1 THEN assume_tac 1); 
       
   239 qed "trans";
   299 
   240 
   300 (** ~ b=a ==> ~ a=b **)
   241 (** ~ b=a ==> ~ a=b **)
   301 val not_sym = prove_goal IFOLP.thy "p:~ b=a ==> ?q:~ a=b"
   242 Goal "p:~ b=a ==> ?q:~ a=b";
   302  (fn [prem] => [ (rtac (prem RS contrapos) 1), (etac sym 1) ]);
   243 by (etac contrapos 1);
       
   244 by (etac sym 1) ;
       
   245 qed "not_sym";
   303 
   246 
   304 (*calling "standard" reduces maxidx to 0*)
   247 (*calling "standard" reduces maxidx to 0*)
   305 val ssubst = standard (sym RS subst);
   248 val ssubst = standard (sym RS subst);
   306 
   249 
   307 (*A special case of ex1E that would otherwise need quantifier expansion*)
   250 (*A special case of ex1E that would otherwise need quantifier expansion*)
   308 val ex1_equalsE = prove_goal IFOLP.thy
   251 Goal "[| 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"
   252 by (etac ex1E 1);
   310  (fn prems =>
   253 by (rtac trans 1);
   311   [ (cut_facts_tac prems 1),
   254 by (rtac sym 2);
   312     (etac ex1E 1),
   255 by (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ;
   313     (rtac trans 1),
   256 qed "ex1_equalsE";
   314     (rtac sym 2),
       
   315     (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]);
       
   316 
   257 
   317 (** Polymorphic congruence rules **)
   258 (** Polymorphic congruence rules **)
   318 
   259 
   319 val subst_context = prove_goal IFOLP.thy 
   260 Goal "[| p:a=b |]  ==>  ?d:t(a)=t(b)";
   320    "[| p:a=b |]  ==>  ?d:t(a)=t(b)"
   261 by (etac ssubst 1);
   321  (fn prems=>
   262 by (rtac refl 1) ;
   322   [ (resolve_tac (prems RL [ssubst]) 1),
   263 qed "subst_context";
   323     (rtac refl 1) ]);
   264 
   324 
   265 Goal "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)";
   325 val subst_context2 = prove_goal IFOLP.thy 
   266 by (REPEAT (etac ssubst 1)); 
   326    "[| p:a=b;  q:c=d |]  ==>  ?p:t(a,c)=t(b,d)"
   267 by (rtac refl 1) ;
   327  (fn prems=>
   268 qed "subst_context2";
   328   [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
   269 
   329 
   270 Goal "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)";
   330 val subst_context3 = prove_goal IFOLP.thy 
   271 by (REPEAT (etac ssubst 1)); 
   331    "[| p:a=b;  q:c=d;  r:e=f |]  ==>  ?p:t(a,c,e)=t(b,d,f)"
   272 by (rtac refl 1) ;
   332  (fn prems=>
   273 qed "subst_context3";
   333   [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);
       
   334 
   274 
   335 (*Useful with eresolve_tac for proving equalties from known equalities.
   275 (*Useful with eresolve_tac for proving equalties from known equalities.
   336         a = b
   276         a = b
   337         |   |
   277         |   |
   338         c = d   *)
   278         c = d   *)
   339 val box_equals = prove_goal IFOLP.thy
   279 Goal "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d";
   340     "[| p:a=b;  q:a=c;  r:b=d |] ==> ?p:c=d"  
   280 by (rtac trans 1);
   341  (fn prems=>
   281 by (rtac trans 1);
   342   [ (rtac trans 1),
   282 by (rtac sym 1);
   343     (rtac trans 1),
   283 by (REPEAT (assume_tac 1)) ;
   344     (rtac sym 1),
   284 qed "box_equals";
   345     (REPEAT (resolve_tac prems 1)) ]);
       
   346 
   285 
   347 (*Dual of box_equals: for proving equalities backwards*)
   286 (*Dual of box_equals: for proving equalities backwards*)
   348 val simp_equals = prove_goal IFOLP.thy
   287 Goal "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b";
   349     "[| p:a=c;  q:b=d;  r:c=d |] ==> ?p:a=b"  
   288 by (rtac trans 1);
   350  (fn prems=>
   289 by (rtac trans 1);
   351   [ (rtac trans 1),
   290 by (REPEAT (eresolve_tac [asm_rl, sym] 1)) ;
   352     (rtac trans 1),
   291 qed "simp_equals";
   353     (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);
       
   354 
   292 
   355 (** Congruence rules for predicate letters **)
   293 (** Congruence rules for predicate letters **)
   356 
   294 
   357 val pred1_cong = prove_goal IFOLP.thy
   295 Goal "p:a=a' ==> ?p:P(a) <-> P(a')";
   358     "p:a=a' ==> ?p:P(a) <-> P(a')"
   296 by (rtac iffI 1);
   359  (fn prems =>
   297 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
   360   [ (cut_facts_tac prems 1),
   298 qed "pred1_cong";
   361     (rtac iffI 1),
   299 
   362     (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   300 Goal "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')";
   363 
   301 by (rtac iffI 1);
   364 val pred2_cong = prove_goal IFOLP.thy
   302 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
   365     "[| p:a=a';  q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')"
   303 qed "pred2_cong";
   366  (fn prems =>
   304 
   367   [ (cut_facts_tac prems 1),
   305 Goal "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')";
   368     (rtac iffI 1),
   306 by (rtac iffI 1);
   369     (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
   307 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ;
   370 
   308 qed "pred3_cong";
   371 val pred3_cong = prove_goal IFOLP.thy
       
   372     "[| p:a=a';  q:b=b';  r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')"
       
   373  (fn prems =>
       
   374   [ (cut_facts_tac prems 1),
       
   375     (rtac iffI 1),
       
   376     (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]);
       
   377 
   309 
   378 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   310 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   379 
   311 
   380 val pred_congs = 
   312 val pred_congs = 
   381     flat (map (fn c => 
   313     flat (map (fn c => 
   392      used with mp_tac (restricted to atomic formulae) is COMPLETE for 
   324      used with mp_tac (restricted to atomic formulae) is COMPLETE for 
   393      intuitionistic propositional logic.  See
   325      intuitionistic propositional logic.  See
   394    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   326    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   395     (preprint, University of St Andrews, 1991)  ***)
   327     (preprint, University of St Andrews, 1991)  ***)
   396 
   328 
   397 val conj_impE = prove_goal IFOLP.thy 
   329 val major::prems= Goal 
   398     "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"
   330     "[| p:(P&Q)-->S;  !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R";
   399  (fn major::prems=>
   331 by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ;
   400   [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]);
   332 qed "conj_impE";
   401 
   333 
   402 val disj_impE = prove_goal IFOLP.thy 
   334 val major::prems= Goal 
   403     "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R"
   335     "[| p:(P|Q)-->S;  !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R";
   404  (fn major::prems=>
   336 by (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)) ]);
   337 qed "disj_impE";
   406 
   338 
   407 (*Simplifies the implication.  Classical version is stronger. 
   339 (*Simplifies the implication.  Classical version is stronger. 
   408   Still UNSAFE since Q must be provable -- backtracking needed.  *)
   340   Still UNSAFE since Q must be provable -- backtracking needed.  *)
   409 val imp_impE = prove_goal IFOLP.thy 
   341 val major::prems= Goal 
   410     "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
   342     "[| p:(P-->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  !!x. x:S ==> r(x):R |] ==> \
   411 \    ?p:R"
   343 \    ?p:R";
   412  (fn major::prems=>
   344 by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ;
   413   [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]);
   345 qed "imp_impE";
   414 
   346 
   415 (*Simplifies the implication.  Classical version is stronger. 
   347 (*Simplifies the implication.  Classical version is stronger. 
   416   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   348   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   417 val not_impE = prove_goal IFOLP.thy
   349 val major::prems= Goal
   418     "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R"
   350     "[| p:~P --> S;  !!y. y:P ==> q(y):False;  !!y. y:S ==> r(y):R |] ==> ?p:R";
   419  (fn major::prems=>
   351 by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ;
   420   [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]);
   352 qed "not_impE";
   421 
   353 
   422 (*Simplifies the implication.   UNSAFE.  *)
   354 (*Simplifies the implication.   UNSAFE.  *)
   423 val iff_impE = prove_goal IFOLP.thy 
   355 val major::prems= Goal 
   424     "[| p:(P<->Q)-->S;  !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q;  \
   356     "[| 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"
   357 \       !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P;  !!x. x:S ==> s(x):R |] ==> ?p:R";
   426  (fn major::prems=>
   358 by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ;
   427   [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]);
   359 qed "iff_impE";
   428 
   360 
   429 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   361 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   430 val all_impE = prove_goal IFOLP.thy 
   362 val major::prems= Goal 
   431     "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R"
   363     "[| p:(ALL x. P(x))-->S;  !!x. q:P(x);  !!y. y:S ==> r(y):R |] ==> ?p:R";
   432  (fn major::prems=>
   364 by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ;
   433   [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]);
   365 qed "all_impE";
   434 
   366 
   435 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   367 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   436 val ex_impE = prove_goal IFOLP.thy 
   368 val major::prems= Goal 
   437     "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"
   369     "[| p:(EX x. P(x))-->S;  !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R";
   438  (fn major::prems=>
   370 by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ;
   439   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   371 qed "ex_impE";
   440 
       
   441 end;
       
   442 
       
   443 open IFOLP_Lemmas;
       
   444