src/Provers/hypsubst.ML
author wenzelm
Wed Dec 05 03:13:21 2001 +0100 (2001-12-05 ago)
changeset 12377 c1e3e7d3f469
parent 12262 11ff5f47df6e
child 13604 57bfacbbaeda
permissions -rw-r--r--
'symmetric' attribute moved to Pure/calculation.ML;
     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 method and symmetric attribute.
     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 by (hyp_subst_tac 1);
    22 by (bound_hyp_subst_tac 1);
    23 
    24 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
    25 Goal "P(a) --> (EX y. a=y --> P(f(a)))";
    26 
    27 Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
    28 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    29 by (blast_hyp_subst_tac (ref true) 1);
    30 *)
    31 
    32 signature HYPSUBST_DATA =
    33   sig
    34   structure Simplifier : SIMPLIFIER
    35   val dest_Trueprop    : term -> term
    36   val dest_eq          : term -> term*term*typ
    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 
    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     (*exported purely for debugging purposes*)
    54   val gen_hyp_subst_tac      : bool -> int -> tactic
    55   val vars_gen_hyp_subst_tac : bool -> int -> tactic
    56   val eq_var                 : bool -> bool -> term -> int * bool
    57   val inspect_pair           : bool -> bool -> term * term * typ -> bool
    58   val mk_eqs                 : thm -> thm list
    59   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
    60   val stac		     : thm -> int -> tactic
    61   val hypsubst_setup         : (theory -> theory) list
    62   end;
    63 
    64 
    65 
    66 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    67 struct
    68 
    69 exception EQ_VAR;
    70 
    71 fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
    72 
    73 local val odot = ord"."
    74 in
    75 (*Simplifier turns Bound variables to dotted Free variables:
    76   change it back (any Bound variable will do)
    77 *)
    78 fun contract t =
    79     case Pattern.eta_contract_atom t of
    80         Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
    81       | t'        => t'
    82 end;
    83 
    84 fun has_vars t = maxidx_of_term t <> ~1;
    85 
    86 (*If novars then we forbid Vars in the equality.
    87   If bnd then we only look for Bound (or dotted Free) variables to eliminate.
    88   When can we safely delete the equality?
    89     Not if it equates two constants; consider 0=1.
    90     Not if it resembles x=t[x], since substitution does not eliminate x.
    91     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    92     Not if it involves a variable free in the premises,
    93         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    94   Prefer to eliminate Bound variables if possible.
    95   Result:  true = use as is,  false = reorient first *)
    96 fun inspect_pair bnd novars (t,u,T) =
    97   if novars andalso maxidx_of_typ T <> ~1
    98   then raise Match   (*variables in the type!*)
    99   else
   100   case (contract t, contract u) of
   101        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
   102                        then raise Match
   103                        else true                (*eliminates t*)
   104      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
   105                        then raise Match
   106                        else false               (*eliminates u*)
   107      | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
   108                           novars andalso has_vars u
   109                        then raise Match
   110                        else true                (*eliminates t*)
   111      | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
   112                           novars andalso has_vars t
   113                        then raise Match
   114                        else false               (*eliminates u*)
   115      | _ => raise Match;
   116 
   117 (*Locates a substitutable variable on the left (resp. right) of an equality
   118    assumption.  Returns the number of intervening assumptions. *)
   119 fun eq_var bnd novars =
   120   let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
   121         | eq_var_aux k (Const("==>",_) $ A $ B) =
   122               ((k, inspect_pair bnd novars
   123                     (Data.dest_eq (Data.dest_Trueprop A)))
   124                       (*Exception comes from inspect_pair or dest_eq*)
   125                handle _ => eq_var_aux (k+1) B)
   126         | eq_var_aux k _ = raise EQ_VAR
   127   in  eq_var_aux 0  end;
   128 
   129 (*We do not try to delete ALL equality assumptions at once.  But
   130   it is easy to handle several consecutive equality assumptions in a row.
   131   Note that we have to inspect the proof state after doing the rewriting,
   132   since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
   133   must NOT be deleted.  Tactic must rotate or delete m assumptions.
   134 *)
   135 fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
   136     let fun count []      = 0
   137           | count (A::Bs) = ((inspect_pair bnd true
   138                               (Data.dest_eq (Data.dest_Trueprop A));
   139                               1 + count Bs)
   140                              handle _ => 0)
   141         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
   142     in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
   143     end);
   144 
   145 (*For the simpset.  Adds ALL suitable equalities, even if not first!
   146   No vars are allowed here, as simpsets are built from meta-assumptions*)
   147 fun mk_eqs th =
   148     [ if inspect_pair false false (Data.dest_eq
   149                                    (Data.dest_Trueprop (#prop (rep_thm th))))
   150       then th RS Data.eq_reflection
   151       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
   152     handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
   153 
   154 local open Simplifier
   155 in
   156 
   157   val hyp_subst_ss = empty_ss setmksimps mk_eqs
   158 
   159   (*Select a suitable equality assumption and substitute throughout the subgoal
   160     Replaces only Bound variables if bnd is true*)
   161   fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   162         let val n = length(Logic.strip_assums_hyp Bi) - 1
   163             val (k,_) = eq_var bnd true Bi
   164         in
   165            DETERM (EVERY [rotate_tac k i,
   166                           asm_full_simp_tac hyp_subst_ss i,
   167                           etac thin_rl i,
   168                           thin_leading_eqs_tac bnd (n-k) i])
   169         end
   170         handle THM _ => no_tac | EQ_VAR => no_tac);
   171 
   172 end;
   173 
   174 val ssubst = standard (Data.sym RS Data.subst);
   175 
   176 val imp_intr_tac = rtac Data.imp_intr;
   177 
   178 (*Old version of the tactic above -- slower but the only way
   179   to handle equalities containing Vars.*)
   180 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
   181       let val n = length(Logic.strip_assums_hyp Bi) - 1
   182           val (k,symopt) = eq_var bnd false Bi
   183       in
   184          DETERM
   185            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   186                    rotate_tac 1 i,
   187                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   188                    etac (if symopt then ssubst else Data.subst) i,
   189                    REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   190       end
   191       handle THM _ => no_tac | EQ_VAR => no_tac);
   192 
   193 (*Substitutes for Free or Bound variables*)
   194 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   195         gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
   196 
   197 (*Substitutes for Bound variables only -- this is always safe*)
   198 val bound_hyp_subst_tac =
   199     gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
   200 
   201 
   202 (** Version for Blast_tac.  Hyps that are affected by the substitution are
   203     moved to the front.  Defect: even trivial changes are noticed, such as
   204     substitutions in the arguments of a function Var. **)
   205 
   206 (*final re-reversal of the changed assumptions*)
   207 fun reverse_n_tac 0 i = all_tac
   208   | reverse_n_tac 1 i = rotate_tac ~1 i
   209   | reverse_n_tac n i =
   210       REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   211       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   212 
   213 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   214 fun all_imp_intr_tac hyps i =
   215   let fun imptac (r, [])    st = reverse_n_tac r i st
   216         | imptac (r, hyp::hyps) st =
   217            let val (hyp',_) = List.nth (prems_of st, i-1) |>
   218                               Logic.strip_assums_concl    |>
   219                               Data.dest_Trueprop          |> Data.dest_imp
   220                val (r',tac) = if Pattern.aeconv (hyp,hyp')
   221                               then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   222                               else (*leave affected hyps at end*)
   223                                    (r+1, imp_intr_tac i)
   224            in
   225                case Seq.pull(tac st) of
   226                    None       => Seq.single(st)
   227                  | Some(st',_) => imptac (r',hyps) st'
   228            end handle _ => error "?? in blast_hyp_subst_tac"
   229   in  imptac (0, rev hyps)  end;
   230 
   231 
   232 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   233       let val (k,symopt) = eq_var false false Bi
   234           val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   235           (*omit selected equality, returning other hyps*)
   236           val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   237           val n = length hyps
   238       in
   239          if !trace then tracing "Substituting an equality" else ();
   240          DETERM
   241            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   242                    rotate_tac 1 i,
   243                    REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   244                    etac (if symopt then ssubst else Data.subst) i,
   245                    all_imp_intr_tac hyps i])
   246       end
   247       handle THM _ => no_tac | EQ_VAR => no_tac);
   248 
   249 
   250 (*apply an equality or definition ONCE;
   251   fails unless the substitution has an effect*)
   252 fun stac th =
   253   let val th' = th RS Data.rev_eq_reflection handle THM _ => th
   254   in CHANGED_GOAL (rtac (th' RS ssubst)) end;
   255 
   256 
   257 (* proof methods *)
   258 
   259 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac);
   260 val hyp_subst_meth =
   261   Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac));
   262 
   263 
   264 (* theory setup *)
   265 
   266 val hypsubst_setup =
   267  [Method.add_methods
   268   [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
   269    ("subst", subst_meth, "substitution")]];
   270 
   271 end;