src/Provers/hypsubst.ML
 author nipkow Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago) changeset 13157 4a4599f78f18 parent 12377 c1e3e7d3f469 child 13604 57bfacbbaeda permissions -rw-r--r--
allowed more general split rules to cope with div/mod 2
```     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;
```