src/Provers/hypsubst.ML
author wenzelm
Sat Oct 17 00:52:37 2009 +0200 (2009-10-17)
changeset 32957 675c0c7e6a37
parent 30515 bca05b17b618
child 35021 c839a4c670c6
permissions -rw-r--r--
explicitly qualify Drule.standard;
     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 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   val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
    47 end;
    48 
    49 signature HYPSUBST =
    50 sig
    51   val single_hyp_subst_tac   : int -> int -> tactic
    52   val single_hyp_meta_subst_tac : int -> int -> tactic
    53   val bound_hyp_subst_tac    : int -> tactic
    54   val hyp_subst_tac          : int -> tactic
    55   val blast_hyp_subst_tac    : bool -> int -> tactic
    56   val stac                   : thm -> int -> tactic
    57   val hypsubst_setup         : theory -> theory
    58 end;
    59 
    60 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    61 struct
    62 
    63 exception EQ_VAR;
    64 
    65 val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
    66   by (unfold prop_def)}
    67 
    68 (** Simple version: Just subtitute one hypothesis, specified by index k **)
    69 fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
    70  let 
    71    val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
    72              |> cterm_of (theory_of_cterm csubg)
    73 
    74    val rule =
    75        Thm.lift_rule pat subst_rule (* lift just over parameters *)
    76        |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
    77  in
    78    rotate_tac k i
    79    THEN Thm.compose_no_flatten false (rule, 1) i
    80    THEN rotate_tac (~k) i
    81  end)
    82 
    83 val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
    84 val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
    85 
    86 fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    87 
    88 (*Simplifier turns Bound variables to special Free variables:
    89   change it back (any Bound variable will do)*)
    90 fun contract t =
    91   (case Envir.eta_contract t of
    92     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    93   | t' => t');
    94 
    95 val has_vars = Term.exists_subterm Term.is_Var;
    96 val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
    97 
    98 (*If novars then we forbid Vars in the equality.
    99   If bnd then we only look for Bound variables to eliminate.
   100   When can we safely delete the equality?
   101     Not if it equates two constants; consider 0=1.
   102     Not if it resembles x=t[x], since substitution does not eliminate x.
   103     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
   104     Not if it involves a variable free in the premises,
   105         but we can't check for this -- hence bnd and bound_hyp_subst_tac
   106   Prefer to eliminate Bound variables if possible.
   107   Result:  true = use as is,  false = reorient first *)
   108 fun inspect_pair bnd novars (t, u) =
   109   if novars andalso (has_tvars t orelse has_tvars u)
   110   then raise Match   (*variables in the type!*)
   111   else
   112   case (contract t, contract u) of
   113        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
   114                        then raise Match
   115                        else true                (*eliminates t*)
   116      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
   117                        then raise Match
   118                        else false               (*eliminates u*)
   119      | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
   120                           novars andalso has_vars u
   121                        then raise Match
   122                        else true                (*eliminates t*)
   123      | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
   124                           novars andalso has_vars t
   125                        then raise Match
   126                        else false               (*eliminates u*)
   127      | _ => raise Match;
   128 
   129 (*Locates a substitutable variable on the left (resp. right) of an equality
   130    assumption.  Returns the number of intervening assumptions. *)
   131 fun eq_var bnd novars =
   132   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
   133         | eq_var_aux k (Const("==>",_) $ A $ B) =
   134               ((k, inspect_pair bnd novars
   135                     (Data.dest_eq (Data.dest_Trueprop A)))
   136                handle TERM _ => eq_var_aux (k+1) B
   137                  | Match => eq_var_aux (k+1) B)
   138         | eq_var_aux k _ = raise EQ_VAR
   139   in  eq_var_aux 0  end;
   140 
   141 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   142   No vars are allowed here, as simpsets are built from meta-assumptions*)
   143 fun mk_eqs bnd th =
   144     [ if inspect_pair bnd false (Data.dest_eq
   145                                    (Data.dest_Trueprop (#prop (rep_thm th))))
   146       then th RS Data.eq_reflection
   147       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
   148     handle TERM _ => [] | Match => [];
   149 
   150 local
   151 in
   152 
   153   (*Select a suitable equality assumption; substitute throughout the subgoal
   154     If bnd is true, then it replaces Bound variables only. *)
   155   fun gen_hyp_subst_tac bnd =
   156     let fun tac i st = SUBGOAL (fn (Bi, _) =>
   157       let
   158         val (k, _) = eq_var bnd true Bi
   159         val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
   160           setmksimps (mk_eqs bnd)
   161       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
   162         etac thin_rl i, rotate_tac (~k) i]
   163       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   164     in REPEAT_DETERM1 o tac end;
   165 
   166 end;
   167 
   168 val ssubst = Drule.standard (Data.sym RS Data.subst);
   169 
   170 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   171   case try (Logic.strip_assums_hyp #> hd #>
   172       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   173     SOME (t, t') =>
   174       let
   175         val Bi = Thm.term_of cBi;
   176         val ps = Logic.strip_params Bi;
   177         val U = Term.fastype_of1 (rev (map snd ps), t);
   178         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
   179         val rl' = Thm.lift_rule cBi rl;
   180         val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
   181           (Logic.strip_assums_concl (Thm.prop_of rl')));
   182         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
   183           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
   184         val (Ts, V) = split_last (Term.binder_types T);
   185         val u = list_abs (ps @ [("x", U)], case (if b then t else t') of
   186             Bound j => subst_bounds (map Bound
   187               ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   188           | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   189         val thy = Thm.theory_of_thm rl';
   190         val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
   191       in compose_tac (true, Drule.instantiate (instT,
   192         map (pairself (cterm_of thy))
   193           [(Var (ixn, Ts ---> U --> body_type T), u),
   194            (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)),
   195            (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl',
   196         nprems_of rl) i
   197       end
   198   | NONE => no_tac);
   199 
   200 val imp_intr_tac = rtac Data.imp_intr;
   201 
   202 (* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *)
   203 (* premises containing meta-implications or quantifiers                *)
   204 
   205 (*Old version of the tactic above -- slower but the only way
   206   to handle equalities containing Vars.*)
   207 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   208       let val n = length(Logic.strip_assums_hyp Bi) - 1
   209           val (k,symopt) = eq_var bnd false Bi
   210       in
   211          DETERM
   212            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   213                    rotate_tac 1 i,
   214                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   215                    inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   216                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   217       end
   218       handle THM _ => no_tac | EQ_VAR => no_tac);
   219 
   220 (*Substitutes for Free or Bound variables*)
   221 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   222         gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
   223 
   224 (*Substitutes for Bound variables only -- this is always safe*)
   225 val bound_hyp_subst_tac =
   226     gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
   227 
   228 
   229 (** Version for Blast_tac.  Hyps that are affected by the substitution are
   230     moved to the front.  Defect: even trivial changes are noticed, such as
   231     substitutions in the arguments of a function Var. **)
   232 
   233 (*final re-reversal of the changed assumptions*)
   234 fun reverse_n_tac 0 i = all_tac
   235   | reverse_n_tac 1 i = rotate_tac ~1 i
   236   | reverse_n_tac n i =
   237       REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   238       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   239 
   240 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   241 fun all_imp_intr_tac hyps i =
   242   let fun imptac (r, [])    st = reverse_n_tac r i st
   243         | imptac (r, hyp::hyps) st =
   244            let val (hyp',_) = List.nth (prems_of st, i-1) |>
   245                               Logic.strip_assums_concl    |>
   246                               Data.dest_Trueprop          |> Data.dest_imp
   247                val (r',tac) = if Pattern.aeconv (hyp,hyp')
   248                               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   249                               else (*leave affected hyps at end*)
   250                                    (r+1, imp_intr_tac i)
   251            in
   252                case Seq.pull(tac st) of
   253                    NONE       => Seq.single(st)
   254                  | SOME(st',_) => imptac (r',hyps) st'
   255            end
   256   in  imptac (0, rev hyps)  end;
   257 
   258 
   259 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   260       let val (k,symopt) = eq_var false false Bi
   261           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   262           (*omit selected equality, returning other hyps*)
   263           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   264           val n = length hyps
   265       in
   266          if trace then tracing "Substituting an equality" else ();
   267          DETERM
   268            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   269                    rotate_tac 1 i,
   270                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   271                    inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   272                    all_imp_intr_tac hyps i])
   273       end
   274       handle THM _ => no_tac | EQ_VAR => no_tac);
   275 
   276 
   277 (*apply an equality or definition ONCE;
   278   fails unless the substitution has an effect*)
   279 fun stac th =
   280   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   281   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   282 
   283 
   284 (* theory setup *)
   285 
   286 val hypsubst_setup =
   287   Method.setup @{binding hypsubst}
   288     (Scan.succeed (K (SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac))))
   289     "substitution using an assumption (improper)" #>
   290   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   291     "simple substitution";
   292 
   293 end;