src/Provers/hypsubst.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 52131 366fa32ee2a3
child 57492 74bf65a1910a
permissions -rw-r--r--
more qualified names;
     1 (*  Title:      Provers/hypsubst.ML
     2     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     3     Copyright   1995  University of Cambridge
     4 
     5 Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst".
     6 
     7 Tactic to substitute using (at least) the assumption x=t in the rest
     8 of the subgoal, and to delete (at least) that assumption.  Original
     9 version due to Martin Coen.
    10 
    11 This version uses the simplifier, and requires it to be already present.
    12 
    13 Test data:
    14 
    15 Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
    16 Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
    17 Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
    18 Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
    19 
    20 Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)";
    21 
    22 by (bound_hyp_subst_tac 1);
    23 by (hyp_subst_tac 1);
    24 
    25 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
    26 Goal "P(a) --> (EX y. a=y --> P(f(a)))";
    27 
    28 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
    29 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    30 by (blast_hyp_subst_tac true 1);
    31 *)
    32 
    33 signature HYPSUBST_DATA =
    34 sig
    35   val dest_Trueprop    : term -> term
    36   val dest_eq          : term -> term * term
    37   val dest_imp         : term -> term * term
    38   val eq_reflection    : thm               (* a=b ==> a==b *)
    39   val rev_eq_reflection: thm               (* a==b ==> a=b *)
    40   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    41   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    42   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    43   val sym              : thm               (* a=b ==> b=a *)
    44   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    45 end;
    46 
    47 signature HYPSUBST =
    48 sig
    49   val bound_hyp_subst_tac    : Proof.context -> int -> tactic
    50   val hyp_subst_tac          : Proof.context -> int -> tactic
    51   val blast_hyp_subst_tac    : bool -> int -> tactic
    52   val stac                   : thm -> int -> tactic
    53   val hypsubst_setup         : theory -> theory
    54 end;
    55 
    56 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    57 struct
    58 
    59 exception EQ_VAR;
    60 
    61 (*Simplifier turns Bound variables to special Free variables:
    62   change it back (any Bound variable will do)*)
    63 fun contract t =
    64   (case Envir.eta_contract t of
    65     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    66   | t' => t');
    67 
    68 val has_vars = Term.exists_subterm Term.is_Var;
    69 val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
    70 
    71 (*If novars then we forbid Vars in the equality.
    72   If bnd then we only look for Bound variables to eliminate.
    73   When can we safely delete the equality?
    74     Not if it equates two constants; consider 0=1.
    75     Not if it resembles x=t[x], since substitution does not eliminate x.
    76     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    77     Not if it involves a variable free in the premises,
    78         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    79   Prefer to eliminate Bound variables if possible.
    80   Result:  true = use as is,  false = reorient first *)
    81 fun inspect_pair bnd novars (t, u) =
    82   if novars andalso (has_tvars t orelse has_tvars u)
    83   then raise Match   (*variables in the type!*)
    84   else
    85     (case (contract t, contract u) of
    86       (Bound i, _) =>
    87         if loose_bvar1 (u, i) orelse novars andalso has_vars u
    88         then raise Match
    89         else true                (*eliminates t*)
    90     | (_, Bound i) =>
    91         if loose_bvar1 (t, i) orelse novars andalso has_vars t
    92         then raise Match
    93         else false               (*eliminates u*)
    94     | (t' as Free _, _) =>
    95         if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
    96         then raise Match
    97         else true                (*eliminates t*)
    98     | (_, u' as Free _) =>
    99         if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
   100         then raise Match
   101         else false               (*eliminates u*)
   102     | _ => raise Match);
   103 
   104 (*Locates a substitutable variable on the left (resp. right) of an equality
   105    assumption.  Returns the number of intervening assumptions. *)
   106 fun eq_var bnd novars =
   107   let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
   108         | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
   109               ((k, inspect_pair bnd novars
   110                     (Data.dest_eq (Data.dest_Trueprop A)))
   111                handle TERM _ => eq_var_aux (k+1) B
   112                  | Match => eq_var_aux (k+1) B)
   113         | eq_var_aux k _ = raise EQ_VAR
   114   in  eq_var_aux 0  end;
   115 
   116 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   117   No vars are allowed here, as simpsets are built from meta-assumptions*)
   118 fun mk_eqs bnd th =
   119     [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th)))
   120       then th RS Data.eq_reflection
   121       else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
   122     handle TERM _ => [] | Match => [];
   123 
   124 local
   125 in
   126 
   127   (*Select a suitable equality assumption; substitute throughout the subgoal
   128     If bnd is true, then it replaces Bound variables only. *)
   129   fun gen_hyp_subst_tac ctxt bnd =
   130     let fun tac i st = SUBGOAL (fn (Bi, _) =>
   131       let
   132         val (k, _) = eq_var bnd true Bi
   133         val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
   134       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
   135         etac thin_rl i, rotate_tac (~k) i]
   136       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   137     in REPEAT_DETERM1 o tac end;
   138 
   139 end;
   140 
   141 val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
   142 
   143 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   144   case try (Logic.strip_assums_hyp #> hd #>
   145       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   146     SOME (t, t') =>
   147       let
   148         val Bi = Thm.term_of cBi;
   149         val ps = Logic.strip_params Bi;
   150         val U = Term.fastype_of1 (rev (map snd ps), t);
   151         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
   152         val rl' = Thm.lift_rule cBi rl;
   153         val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
   154           (Logic.strip_assums_concl (Thm.prop_of rl')));
   155         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
   156           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
   157         val (Ts, V) = split_last (Term.binder_types T);
   158         val u =
   159           fold_rev Term.abs (ps @ [("x", U)])
   160             (case (if b then t else t') of
   161               Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   162             | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   163         val thy = Thm.theory_of_thm rl';
   164         val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
   165       in
   166         compose_tac (true, Drule.instantiate_normalize (instT,
   167           map (pairself (cterm_of thy))
   168             [(Var (ixn, Ts ---> U --> body_type T), u),
   169              (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   170              (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   171           nprems_of rl) i
   172       end
   173   | NONE => no_tac);
   174 
   175 val imp_intr_tac = rtac Data.imp_intr;
   176 
   177 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
   178 (* premises containing meta-implications or quantifiers                *)
   179 
   180 (*Old version of the tactic above -- slower but the only way
   181   to handle equalities containing Vars.*)
   182 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   183       let val n = length(Logic.strip_assums_hyp Bi) - 1
   184           val (k,symopt) = eq_var bnd false Bi
   185       in
   186          DETERM
   187            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   188                    rotate_tac 1 i,
   189                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   190                    inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   191                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   192       end
   193       handle THM _ => no_tac | EQ_VAR => no_tac);
   194 
   195 (*Substitutes for Free or Bound variables*)
   196 fun hyp_subst_tac ctxt =
   197   FIRST' [ematch_tac [Data.thin_refl],
   198     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false];
   199 
   200 (*Substitutes for Bound variables only -- this is always safe*)
   201 fun bound_hyp_subst_tac ctxt =
   202   gen_hyp_subst_tac ctxt true ORELSE' vars_gen_hyp_subst_tac true;
   203 
   204 
   205 (** Version for Blast_tac.  Hyps that are affected by the substitution are
   206     moved to the front.  Defect: even trivial changes are noticed, such as
   207     substitutions in the arguments of a function Var. **)
   208 
   209 (*final re-reversal of the changed assumptions*)
   210 fun reverse_n_tac 0 i = all_tac
   211   | reverse_n_tac 1 i = rotate_tac ~1 i
   212   | reverse_n_tac n i =
   213       REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   214       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   215 
   216 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   217 fun all_imp_intr_tac hyps i =
   218   let
   219     fun imptac (r, []) st = reverse_n_tac r i st
   220       | imptac (r, hyp::hyps) st =
   221           let
   222             val (hyp', _) =
   223               term_of (Thm.cprem_of st i)
   224               |> Logic.strip_assums_concl
   225               |> Data.dest_Trueprop |> Data.dest_imp;
   226             val (r', tac) =
   227               if Envir.aeconv (hyp, hyp')
   228               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   229               else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
   230           in
   231             (case Seq.pull (tac st) of
   232               NONE => Seq.single st
   233             | SOME (st', _) => imptac (r', hyps) st')
   234           end
   235   in imptac (0, rev hyps) end;
   236 
   237 
   238 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   239       let val (k,symopt) = eq_var false false Bi
   240           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   241           (*omit selected equality, returning other hyps*)
   242           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   243           val n = length hyps
   244       in
   245          if trace then tracing "Substituting an equality" else ();
   246          DETERM
   247            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   248                    rotate_tac 1 i,
   249                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   250                    inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   251                    all_imp_intr_tac hyps i])
   252       end
   253       handle THM _ => no_tac | EQ_VAR => no_tac);
   254 
   255 
   256 (*apply an equality or definition ONCE;
   257   fails unless the substitution has an effect*)
   258 fun stac th =
   259   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   260   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   261 
   262 
   263 (* theory setup *)
   264 
   265 val hypsubst_setup =
   266   Method.setup @{binding hypsubst}
   267     (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   268     "substitution using an assumption (improper)" #>
   269   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   270     "simple substitution";
   271 
   272 end;