diff -r fd510875fb71 -r d12da312eff4 src/FOLP/IFOLP.ML --- a/src/FOLP/IFOLP.ML Mon Jan 29 13:56:41 1996 +0100 +++ b/src/FOLP/IFOLP.ML Mon Jan 29 13:58:15 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: FOLP/IFOLP.ML +(* Title: FOLP/IFOLP.ML ID: \$Id\$ - Author: Martin D Coen, Cambridge University Computer Laboratory + Author: Martin D Coen, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs) @@ -140,9 +140,9 @@ let val hyps = map discard_proof (Logic.strip_assums_hyp prem) and concl = discard_proof (Logic.strip_assums_concl prem) in - if exists (fn hyp => hyp aconv concl) hyps - then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of - [_] => assume_tac i + if exists (fn hyp => hyp aconv concl) hyps + then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of + [_] => assume_tac i | _ => no_tac else no_tac end); @@ -168,7 +168,7 @@ (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) val iffE = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R" - (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]); + (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); (* Destruct rules for <-> similar to Modus Ponens *) @@ -241,14 +241,14 @@ (fn prems => [ (cut_facts_tac prems 1), (REPEAT (ares_tac [iffI,impI] 1 - ORELSE eresolve_tac [iffE] 1 + ORELSE etac iffE 1 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); val iff_cong = prove_goal IFOLP.thy "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" (fn prems => [ (cut_facts_tac prems 1), - (REPEAT (eresolve_tac [iffE] 1 + (REPEAT (etac iffE 1 ORELSE ares_tac [iffI] 1 ORELSE mp_tac 1)) ]); @@ -265,12 +265,12 @@ (fn prems => [ (REPEAT (ares_tac [iffI,allI] 1 ORELSE mp_tac 1 - ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]); + ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); val ex_cong = prove_goal IFOLP.thy "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))" (fn prems => - [ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1 + [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); @@ -320,7 +320,7 @@ "[| p:a=b |] ==> ?d:t(a)=t(b)" (fn prems=> [ (resolve_tac (prems RL [ssubst]) 1), - (resolve_tac [refl] 1) ]); + (rtac refl 1) ]); val subst_context2 = prove_goal IFOLP.thy "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)" @@ -333,23 +333,23 @@ [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); (*Useful with eresolve_tac for proving equalties from known equalities. - a = b - | | - c = d *) + a = b + | | + c = d *) val box_equals = prove_goal IFOLP.thy "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d" (fn prems=> - [ (resolve_tac [trans] 1), - (resolve_tac [trans] 1), - (resolve_tac [sym] 1), + [ (rtac trans 1), + (rtac trans 1), + (rtac sym 1), (REPEAT (resolve_tac prems 1)) ]); (*Dual of box_equals: for proving equalities backwards*) val simp_equals = prove_goal IFOLP.thy "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b" (fn prems=> - [ (resolve_tac [trans] 1), - (resolve_tac [trans] 1), + [ (rtac trans 1), + (rtac trans 1), (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); (** Congruence rules for predicate letters **) @@ -379,9 +379,9 @@ val pred_congs = flat (map (fn c => - map (fn th => read_instantiate [("P",c)] th) - [pred1_cong,pred2_cong,pred3_cong]) - (explode"PQRS")); + map (fn th => read_instantiate [("P",c)] th) + [pred1_cong,pred2_cong,pred3_cong]) + (explode"PQRS")); (*special case for the equality predicate!*) val eq_cong = read_instantiate [("P","op =")] pred2_cong;