src/Provers/hypsubst.ML
 author krauss Mon Jul 14 17:47:18 2008 +0200 (2008-07-14) changeset 27572 67cd6ed76446 parent 26992 4508f20818af child 27734 dcec1c564f05 permissions -rw-r--r--
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
```     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 ==> PROP prop (x == t ==> 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 = 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.add_methods
```
```   288     [("hypsubst", Method.no_args (Method.SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac)),
```
```   289         "substitution using an assumption (improper)"),
```
```   290      ("simplesubst", Method.thm_args (Method.SIMPLE_METHOD' o stac), "simple substitution")];
```
```   291
```
```   292 end;
```