src/Provers/hypsubst.ML
author wenzelm
Wed Apr 04 23:29:33 2007 +0200 (2007-04-04)
changeset 22596 d0d2af4db18f
parent 21588 cd0dc678a205
child 23908 edca7f581c09
permissions -rw-r--r--
rep_thm/cterm/ctyp: removed obsolete sign field;
     1 (*  Title:      Provers/hypsubst.ML
     2     ID:         $Id$
     3     Authors:    Martin D Coen, Tobias Nipkow and Lawrence C Paulson
     4     Copyright   1995  University of Cambridge
     5 
     6 Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "subst".
     7 
     8 Tactic to substitute using (at least) the assumption x=t in the rest
     9 of the subgoal, and to delete (at least) that assumption.  Original
    10 version due to Martin Coen.
    11 
    12 This version uses the simplifier, and requires it to be already present.
    13 
    14 Test data:
    15 
    16 Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
    17 Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
    18 Goal "!!y. [| ?x=y; P(?x) |] ==> y = a";
    19 Goal "!!z. [| ?x=y; P(?x) |] ==> y = a";
    20 
    21 Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)";
    22 
    23 by (bound_hyp_subst_tac 1);
    24 by (hyp_subst_tac 1);
    25 
    26 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
    27 Goal "P(a) --> (EX y. a=y --> P(f(a)))";
    28 
    29 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
    30 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    31 by (blast_hyp_subst_tac (ref true) 1);
    32 *)
    33 
    34 signature HYPSUBST_DATA =
    35 sig
    36   val dest_Trueprop    : term -> term
    37   val dest_eq          : term -> term * term
    38   val dest_imp         : term -> term * term
    39   val eq_reflection    : thm               (* a=b ==> a==b *)
    40   val rev_eq_reflection: thm               (* a==b ==> a=b *)
    41   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    42   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    43   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    44   val sym              : thm               (* a=b ==> b=a *)
    45   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    46 end;
    47 
    48 signature HYPSUBST =
    49 sig
    50   val bound_hyp_subst_tac    : int -> tactic
    51   val hyp_subst_tac          : int -> tactic
    52   val blast_hyp_subst_tac    : bool ref -> int -> tactic
    53   val stac                   : thm -> int -> tactic
    54   val hypsubst_setup         : theory -> theory
    55 end;
    56 
    57 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    58 struct
    59 
    60 exception EQ_VAR;
    61 
    62 fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    63 
    64 (*Simplifier turns Bound variables to special Free variables:
    65   change it back (any Bound variable will do)*)
    66 fun contract t =
    67   (case Pattern.eta_contract_atom t of
    68     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    69   | t' => t');
    70 
    71 val has_vars = Term.exists_subterm Term.is_Var;
    72 val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
    73 
    74 (*If novars then we forbid Vars in the equality.
    75   If bnd then we only look for Bound variables to eliminate.
    76   When can we safely delete the equality?
    77     Not if it equates two constants; consider 0=1.
    78     Not if it resembles x=t[x], since substitution does not eliminate x.
    79     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    80     Not if it involves a variable free in the premises,
    81         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    82   Prefer to eliminate Bound variables if possible.
    83   Result:  true = use as is,  false = reorient first *)
    84 fun inspect_pair bnd novars (t, u) =
    85   if novars andalso (has_tvars t orelse has_tvars u)
    86   then raise Match   (*variables in the type!*)
    87   else
    88   case (contract t, contract u) of
    89        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
    90                        then raise Match
    91                        else true                (*eliminates t*)
    92      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
    93                        then raise Match
    94                        else false               (*eliminates u*)
    95      | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
    96                           novars andalso has_vars u
    97                        then raise Match
    98                        else true                (*eliminates t*)
    99      | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
   100                           novars andalso has_vars t
   101                        then raise Match
   102                        else false               (*eliminates u*)
   103      | _ => raise Match;
   104 
   105 (*Locates a substitutable variable on the left (resp. right) of an equality
   106    assumption.  Returns the number of intervening assumptions. *)
   107 fun eq_var bnd novars =
   108   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
   109         | eq_var_aux k (Const("==>",_) $ A $ B) =
   110               ((k, inspect_pair bnd novars
   111                     (Data.dest_eq (Data.dest_Trueprop A)))
   112                handle TERM _ => eq_var_aux (k+1) B
   113                  | Match => eq_var_aux (k+1) B)
   114         | eq_var_aux k _ = raise EQ_VAR
   115   in  eq_var_aux 0  end;
   116 
   117 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   118   No vars are allowed here, as simpsets are built from meta-assumptions*)
   119 fun mk_eqs bnd th =
   120     [ if inspect_pair bnd false (Data.dest_eq
   121                                    (Data.dest_Trueprop (#prop (rep_thm th))))
   122       then th RS Data.eq_reflection
   123       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
   124     handle TERM _ => [] | Match => [];
   125 
   126 local
   127 in
   128 
   129   (*Select a suitable equality assumption; substitute throughout the subgoal
   130     If bnd is true, then it replaces Bound variables only. *)
   131   fun gen_hyp_subst_tac bnd =
   132     let fun tac i st = SUBGOAL (fn (Bi, _) =>
   133       let
   134         val (k, _) = eq_var bnd true Bi
   135         val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
   136           setmksimps (mk_eqs bnd)
   137       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
   138         etac thin_rl i, rotate_tac (~k) i]
   139       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   140     in REPEAT_DETERM1 o tac end;
   141 
   142 end;
   143 
   144 val ssubst = standard (Data.sym RS Data.subst);
   145 
   146 val imp_intr_tac = rtac Data.imp_intr;
   147 
   148 (*Old version of the tactic above -- slower but the only way
   149   to handle equalities containing Vars.*)
   150 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   151       let val n = length(Logic.strip_assums_hyp Bi) - 1
   152           val (k,symopt) = eq_var bnd false Bi
   153       in
   154          DETERM
   155            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   156                    rotate_tac 1 i,
   157                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   158                    etac (if symopt then ssubst else Data.subst) i,
   159                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   160       end
   161       handle THM _ => no_tac | EQ_VAR => no_tac);
   162 
   163 (*Substitutes for Free or Bound variables*)
   164 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   165         gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
   166 
   167 (*Substitutes for Bound variables only -- this is always safe*)
   168 val bound_hyp_subst_tac =
   169     gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
   170 
   171 
   172 (** Version for Blast_tac.  Hyps that are affected by the substitution are
   173     moved to the front.  Defect: even trivial changes are noticed, such as
   174     substitutions in the arguments of a function Var. **)
   175 
   176 (*final re-reversal of the changed assumptions*)
   177 fun reverse_n_tac 0 i = all_tac
   178   | reverse_n_tac 1 i = rotate_tac ~1 i
   179   | reverse_n_tac n i =
   180       REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   181       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   182 
   183 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   184 fun all_imp_intr_tac hyps i =
   185   let fun imptac (r, [])    st = reverse_n_tac r i st
   186         | imptac (r, hyp::hyps) st =
   187            let val (hyp',_) = List.nth (prems_of st, i-1) |>
   188                               Logic.strip_assums_concl    |>
   189                               Data.dest_Trueprop          |> Data.dest_imp
   190                val (r',tac) = if Pattern.aeconv (hyp,hyp')
   191                               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   192                               else (*leave affected hyps at end*)
   193                                    (r+1, imp_intr_tac i)
   194            in
   195                case Seq.pull(tac st) of
   196                    NONE       => Seq.single(st)
   197                  | SOME(st',_) => imptac (r',hyps) st'
   198            end
   199   in  imptac (0, rev hyps)  end;
   200 
   201 
   202 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   203       let val (k,symopt) = eq_var false false Bi
   204           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   205           (*omit selected equality, returning other hyps*)
   206           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   207           val n = length hyps
   208       in
   209          if !trace then tracing "Substituting an equality" else ();
   210          DETERM
   211            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   212                    rotate_tac 1 i,
   213                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   214                    etac (if symopt then ssubst else Data.subst) i,
   215                    all_imp_intr_tac hyps i])
   216       end
   217       handle THM _ => no_tac | EQ_VAR => no_tac);
   218 
   219 
   220 (*apply an equality or definition ONCE;
   221   fails unless the substitution has an effect*)
   222 fun stac th =
   223   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   224   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   225 
   226 
   227 (* theory setup *)
   228 
   229 val hypsubst_setup =
   230   Method.add_methods
   231     [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
   232         "substitution using an assumption (improper)"),
   233      ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
   234 
   235 end;