src/Provers/hypsubst.ML
author wenzelm
Thu Oct 30 16:55:29 2014 +0100 (2014-10-30)
changeset 58838 59203adfc33f
parent 58826 2ed2eaabe3df
child 58950 d07464875dd4
permissions -rw-r--r--
eliminated aliases;
     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_thin     : bool -> Proof.context -> int -> tactic
    51   val hyp_subst_thin         : bool Config.T
    52   val hyp_subst_tac          : Proof.context -> int -> tactic
    53   val blast_hyp_subst_tac    : bool -> int -> tactic
    54   val stac                   : thm -> int -> tactic
    55 end;
    56 
    57 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    58 struct
    59 
    60 exception EQ_VAR;
    61 
    62 (*Simplifier turns Bound variables to special Free variables:
    63   change it back (any Bound variable will do)*)
    64 fun contract t =
    65   (case Envir.eta_contract t of
    66     Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
    67   | t' => t');
    68 
    69 val has_vars = Term.exists_subterm Term.is_Var;
    70 val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar);
    71 
    72 (*If novars then we forbid Vars in the equality.
    73   If bnd then we only look for Bound variables to eliminate.
    74   When can we safely delete the equality?
    75     Not if it equates two constants; consider 0=1.
    76     Not if it resembles x=t[x], since substitution does not eliminate x.
    77     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    78     Not if it involves a variable free in the premises,
    79         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    80   Prefer to eliminate Bound variables if possible.
    81   Result:  true = use as is,  false = reorient first
    82     also returns var to substitute, relevant if it is Free *)
    83 fun inspect_pair bnd novars (t, u) =
    84   if novars andalso (has_tvars t orelse has_tvars u)
    85   then raise Match   (*variables in the type!*)
    86   else
    87     (case (contract t, contract u) of
    88       (Bound i, _) =>
    89         if loose_bvar1 (u, i) orelse novars andalso has_vars u
    90         then raise Match
    91         else (true, Bound i)                (*eliminates t*)
    92     | (_, Bound i) =>
    93         if loose_bvar1 (t, i) orelse novars andalso has_vars t
    94         then raise Match
    95         else (false, Bound i)               (*eliminates u*)
    96     | (t' as Free _, _) =>
    97         if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u
    98         then raise Match
    99         else (true, t')                (*eliminates t*)
   100     | (_, u' as Free _) =>
   101         if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t
   102         then raise Match
   103         else (false, u')               (*eliminates u*)
   104     | _ => raise Match);
   105 
   106 (*Locates a substitutable variable on the left (resp. right) of an equality
   107    assumption.  Returns the number of intervening assumptions. *)
   108 fun eq_var bnd novars check_frees t =
   109   let
   110     fun check_free ts (orient, Free f)
   111       = if not check_frees orelse not orient
   112             orelse exists (curry Logic.occs (Free f)) ts
   113         then (orient, true) else raise Match
   114       | check_free ts (orient, _) = (orient, false)
   115     fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs
   116       | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs =
   117               ((k, check_free (B :: hs) (inspect_pair bnd novars
   118                     (Data.dest_eq (Data.dest_Trueprop A))))
   119                handle TERM _ => eq_var_aux (k+1) B (A :: hs)
   120                  | Match => eq_var_aux (k+1) B (A :: hs))
   121       | eq_var_aux k _ _ = raise EQ_VAR
   122 
   123   in  eq_var_aux 0 t [] end;
   124 
   125 val thin_free_eq_tac = SUBGOAL (fn (t, i) => let
   126      val (k, _) = eq_var false false false t
   127      val ok = (eq_var false false true t |> fst) > k
   128         handle EQ_VAR => true
   129    in if ok then EVERY [rotate_tac k i, eresolve_tac [thin_rl] i, rotate_tac (~k) i]
   130     else no_tac
   131    end handle EQ_VAR => no_tac)
   132 
   133 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   134   No vars are allowed here, as simpsets are built from meta-assumptions*)
   135 fun mk_eqs bnd th =
   136     [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst
   137       then th RS Data.eq_reflection
   138       else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ]
   139     handle TERM _ => [] | Match => [];
   140 
   141 fun bool2s true = "true" | bool2s false = "false"
   142 
   143 local
   144 in
   145 
   146   (*Select a suitable equality assumption; substitute throughout the subgoal
   147     If bnd is true, then it replaces Bound variables only. *)
   148   fun gen_hyp_subst_tac ctxt bnd =
   149     SUBGOAL (fn (Bi, i) =>
   150       let
   151         val (k, (orient, is_free)) = eq_var bnd true true Bi
   152         val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd))
   153       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i,
   154         if not is_free then eresolve_tac [thin_rl] i
   155           else if orient then eresolve_tac [Data.rev_mp] i
   156           else eresolve_tac [Data.sym RS Data.rev_mp] i,
   157         rotate_tac (~k) i,
   158         if is_free then resolve_tac [Data.imp_intr] i else all_tac]
   159       end handle THM _ => no_tac | EQ_VAR => no_tac)
   160 
   161 end;
   162 
   163 val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
   164 
   165 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   166   case try (Logic.strip_assums_hyp #> hd #>
   167       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   168     SOME (t, t') =>
   169       let
   170         val Bi = Thm.term_of cBi;
   171         val ps = Logic.strip_params Bi;
   172         val U = Term.fastype_of1 (rev (map snd ps), t);
   173         val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi);
   174         val rl' = Thm.lift_rule cBi rl;
   175         val Var (ixn, T) = Term.head_of (Data.dest_Trueprop
   176           (Logic.strip_assums_concl (Thm.prop_of rl')));
   177         val (v1, v2) = Data.dest_eq (Data.dest_Trueprop
   178           (Logic.strip_assums_concl (hd (Thm.prems_of rl'))));
   179         val (Ts, V) = split_last (Term.binder_types T);
   180         val u =
   181           fold_rev Term.abs (ps @ [("x", U)])
   182             (case (if b then t else t') of
   183               Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
   184             | t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
   185         val thy = Thm.theory_of_thm rl';
   186         val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
   187       in
   188         compose_tac (true, Drule.instantiate_normalize (instT,
   189           map (pairself (cterm_of thy))
   190             [(Var (ixn, Ts ---> U --> body_type T), u),
   191              (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
   192              (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
   193           nprems_of rl) i
   194       end
   195   | NONE => no_tac);
   196 
   197 val imp_intr_tac = resolve_tac [Data.imp_intr];
   198 
   199 fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
   200 val dup_subst = rev_dup_elim ssubst
   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, (orient, is_free)) = eq_var bnd false true Bi
   210           val rl = if is_free then dup_subst else ssubst
   211           val rl = if orient then rl else Data.sym RS rl
   212       in
   213          DETERM
   214            (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
   215                    rotate_tac 1 i,
   216                    REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
   217                    inst_subst_tac orient rl i,
   218                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   219       end
   220       handle THM _ => no_tac | EQ_VAR => no_tac);
   221 
   222 (*Substitutes for Free or Bound variables,
   223   discarding equalities on Bound variables
   224   and on Free variables if thin=true*)
   225 fun hyp_subst_tac_thin thin ctxt =
   226   REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
   227     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
   228     if thin then thin_free_eq_tac else K no_tac];
   229 
   230 val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
   231 
   232 fun hyp_subst_tac ctxt =
   233   hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt;
   234 
   235 (*Substitutes for Bound variables only -- this is always safe*)
   236 fun bound_hyp_subst_tac ctxt =
   237   REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
   238     ORELSE' vars_gen_hyp_subst_tac true);
   239 
   240 (** Version for Blast_tac.  Hyps that are affected by the substitution are
   241     moved to the front.  Defect: even trivial changes are noticed, such as
   242     substitutions in the arguments of a function Var. **)
   243 
   244 (*final re-reversal of the changed assumptions*)
   245 fun reverse_n_tac 0 i = all_tac
   246   | reverse_n_tac 1 i = rotate_tac ~1 i
   247   | reverse_n_tac n i =
   248       REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac [Data.rev_mp] i) THEN
   249       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   250 
   251 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   252 fun all_imp_intr_tac hyps i =
   253   let
   254     fun imptac (r, []) st = reverse_n_tac r i st
   255       | imptac (r, hyp::hyps) st =
   256           let
   257             val (hyp', _) =
   258               term_of (Thm.cprem_of st i)
   259               |> Logic.strip_assums_concl
   260               |> Data.dest_Trueprop |> Data.dest_imp;
   261             val (r', tac) =
   262               if Envir.aeconv (hyp, hyp')
   263               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   264               else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
   265           in
   266             (case Seq.pull (tac st) of
   267               NONE => Seq.single st
   268             | SOME (st', _) => imptac (r', hyps) st')
   269           end
   270   in imptac (0, rev hyps) end;
   271 
   272 
   273 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   274       let val (k, (symopt, _)) = eq_var false false false Bi
   275           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   276           (*omit selected equality, returning other hyps*)
   277           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   278           val n = length hyps
   279       in
   280          if trace then tracing "Substituting an equality" else ();
   281          DETERM
   282            (EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
   283                    rotate_tac 1 i,
   284                    REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
   285                    inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
   286                    all_imp_intr_tac hyps i])
   287       end
   288       handle THM _ => no_tac | EQ_VAR => no_tac);
   289 
   290 (*apply an equality or definition ONCE;
   291   fails unless the substitution has an effect*)
   292 fun stac th =
   293   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   294   in CHANGED_GOAL (resolve_tac [th' RS ssubst]) end;
   295 
   296 
   297 (* method setup *)
   298 
   299 val _ =
   300   Theory.setup
   301    (Method.setup @{binding hypsubst}
   302       (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt)))
   303       "substitution using an assumption (improper)" #>
   304     Method.setup @{binding hypsubst_thin}
   305       (Scan.succeed (fn ctxt => SIMPLE_METHOD'
   306           (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
   307       "substitution using an assumption, eliminating assumptions" #>
   308     Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
   309       "simple substitution");
   310 
   311 end;