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