src/Provers/hypsubst.ML
 author wenzelm Thu Jul 27 11:44:29 2000 +0200 (2000-07-27 ago) changeset 9449 2f814053a6cc parent 4466 305390f23734 child 9532 36b9bc6eb454 permissions -rw-r--r--
intro_elim_tac: bimatch_from;
```     1 (*  Title: 	Provers/hypsubst
```
```     2     ID:         \$Id\$
```
```     3     Authors: 	Martin D Coen, Tobias Nipkow and Lawrence C Paulson
```
```     4     Copyright   1995  University of Cambridge
```
```     5
```
```     6 Tactic to substitute using (at least) the assumption x=t in the rest of the
```
```     7 subgoal, and to delete (at least) that assumption.
```
```     8 Original version due to Martin Coen.
```
```     9
```
```    10 This version uses the simplifier, and requires it to be already present.
```
```    11
```
```    12 Test data:
```
```    13
```
```    14 goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
```
```    15 goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
```
```    16 goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a";
```
```    17 goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a";
```
```    18
```
```    19 by (hyp_subst_tac 1);
```
```    20 by (bound_hyp_subst_tac 1);
```
```    21
```
```    22 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
```
```    23 goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
```
```    24
```
```    25 goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
```
```    26 \                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
```
```    27 by (blast_hyp_subst_tac (ref true) 1);
```
```    28 *)
```
```    29
```
```    30 signature HYPSUBST_DATA =
```
```    31   sig
```
```    32   structure Simplifier : SIMPLIFIER
```
```    33   val dest_Trueprop    : term -> term
```
```    34   val dest_eq	       : term -> term*term*typ
```
```    35   val dest_imp	       : term -> term*term
```
```    36   val eq_reflection    : thm		   (* a=b ==> a==b *)
```
```    37   val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
```
```    38   val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
```
```    39   val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
```
```    40   val sym	       : thm		   (* a=b ==> b=a *)
```
```    41   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
```
```    42   end;
```
```    43
```
```    44
```
```    45 signature HYPSUBST =
```
```    46   sig
```
```    47   val bound_hyp_subst_tac    : int -> tactic
```
```    48   val hyp_subst_tac          : int -> tactic
```
```    49   val blast_hyp_subst_tac    : bool ref -> int -> tactic
```
```    50     (*exported purely for debugging purposes*)
```
```    51   val gen_hyp_subst_tac      : bool -> int -> tactic
```
```    52   val vars_gen_hyp_subst_tac : bool -> int -> tactic
```
```    53   val eq_var                 : bool -> bool -> term -> int * bool
```
```    54   val inspect_pair           : bool -> bool -> term * term * typ -> bool
```
```    55   val mk_eqs                 : thm -> thm list
```
```    56   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
```
```    57   end;
```
```    58
```
```    59
```
```    60
```
```    61 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
```
```    62 struct
```
```    63
```
```    64 exception EQ_VAR;
```
```    65
```
```    66 fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
```
```    67
```
```    68 local val odot = ord"."
```
```    69 in
```
```    70 (*Simplifier turns Bound variables to dotted Free variables:
```
```    71   change it back (any Bound variable will do)
```
```    72 *)
```
```    73 fun contract t =
```
```    74     case Pattern.eta_contract_atom t of
```
```    75 	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
```
```    76       | t'        => t'
```
```    77 end;
```
```    78
```
```    79 fun has_vars t = maxidx_of_term t <> ~1;
```
```    80
```
```    81 (*If novars then we forbid Vars in the equality.
```
```    82   If bnd then we only look for Bound (or dotted Free) variables to eliminate.
```
```    83   When can we safely delete the equality?
```
```    84     Not if it equates two constants; consider 0=1.
```
```    85     Not if it resembles x=t[x], since substitution does not eliminate x.
```
```    86     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
```
```    87     Not if it involves a variable free in the premises,
```
```    88         but we can't check for this -- hence bnd and bound_hyp_subst_tac
```
```    89   Prefer to eliminate Bound variables if possible.
```
```    90   Result:  true = use as is,  false = reorient first *)
```
```    91 fun inspect_pair bnd novars (t,u,T) =
```
```    92   if novars andalso maxidx_of_typ T <> ~1
```
```    93   then raise Match   (*variables in the type!*)
```
```    94   else
```
```    95   case (contract t, contract u) of
```
```    96        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
```
```    97 		       then raise Match
```
```    98 		       else true		(*eliminates t*)
```
```    99      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
```
```   100 		       then raise Match
```
```   101 		       else false		(*eliminates u*)
```
```   102      | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
```
```   103 		          novars andalso has_vars u
```
```   104 		       then raise Match
```
```   105 		       else true		(*eliminates t*)
```
```   106      | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
```
```   107 		          novars andalso has_vars t
```
```   108 		       then raise Match
```
```   109 		       else false		(*eliminates u*)
```
```   110      | _ => raise Match;
```
```   111
```
```   112 (*Locates a substitutable variable on the left (resp. right) of an equality
```
```   113    assumption.  Returns the number of intervening assumptions. *)
```
```   114 fun eq_var bnd novars =
```
```   115   let fun eq_var_aux k (Const("all",_) \$ Abs(_,_,t)) = eq_var_aux k t
```
```   116 	| eq_var_aux k (Const("==>",_) \$ A \$ B) =
```
```   117 	      ((k, inspect_pair bnd novars
```
```   118 		    (Data.dest_eq (Data.dest_Trueprop A)))
```
```   119 		      (*Exception comes from inspect_pair or dest_eq*)
```
```   120 	       handle _ => eq_var_aux (k+1) B)
```
```   121 	| eq_var_aux k _ = raise EQ_VAR
```
```   122   in  eq_var_aux 0  end;
```
```   123
```
```   124 (*We do not try to delete ALL equality assumptions at once.  But
```
```   125   it is easy to handle several consecutive equality assumptions in a row.
```
```   126   Note that we have to inspect the proof state after doing the rewriting,
```
```   127   since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
```
```   128   must NOT be deleted.  Tactic must rotate or delete m assumptions.
```
```   129 *)
```
```   130 fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
```
```   131     let fun count []      = 0
```
```   132 	  | count (A::Bs) = ((inspect_pair bnd true
```
```   133 			      (Data.dest_eq (Data.dest_Trueprop A));
```
```   134 			      1 + count Bs)
```
```   135                              handle _ => 0)
```
```   136         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
```
```   137     in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
```
```   138     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 th =
```
```   143     [ if inspect_pair false false (Data.dest_eq
```
```   144 				   (Data.dest_Trueprop (#prop (rep_thm th))))
```
```   145       then th RS Data.eq_reflection
```
```   146       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
```
```   147     handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
```
```   148
```
```   149 local open Simplifier
```
```   150 in
```
```   151
```
```   152   val hyp_subst_ss = empty_ss setmksimps mk_eqs
```
```   153
```
```   154   (*Select a suitable equality assumption and substitute throughout the subgoal
```
```   155     Replaces only Bound variables if bnd is true*)
```
```   156   fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
```
```   157 	let val n = length(Logic.strip_assums_hyp Bi) - 1
```
```   158 	    val (k,_) = eq_var bnd true Bi
```
```   159 	in
```
```   160 	   DETERM (EVERY [rotate_tac k i,
```
```   161 			  asm_full_simp_tac hyp_subst_ss i,
```
```   162 			  etac thin_rl i,
```
```   163 			  thin_leading_eqs_tac bnd (n-k) i])
```
```   164 	end
```
```   165 	handle THM _ => no_tac | EQ_VAR => no_tac);
```
```   166
```
```   167 end;
```
```   168
```
```   169 val ssubst = standard (Data.sym RS Data.subst);
```
```   170
```
```   171 val imp_intr_tac = rtac Data.imp_intr;
```
```   172
```
```   173 (*Old version of the tactic above -- slower but the only way
```
```   174   to handle equalities containing Vars.*)
```
```   175 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
```
```   176       let val n = length(Logic.strip_assums_hyp Bi) - 1
```
```   177 	  val (k,symopt) = eq_var bnd false Bi
```
```   178       in
```
```   179 	 DETERM
```
```   180            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
```
```   181 		   rotate_tac 1 i,
```
```   182 		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
```
```   183 		   etac (if symopt then ssubst else Data.subst) i,
```
```   184 		   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
```
```   185       end
```
```   186       handle THM _ => no_tac | EQ_VAR => no_tac);
```
```   187
```
```   188 (*Substitutes for Free or Bound variables*)
```
```   189 val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
```
```   190         gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
```
```   191
```
```   192 (*Substitutes for Bound variables only -- this is always safe*)
```
```   193 val bound_hyp_subst_tac =
```
```   194     gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
```
```   195
```
```   196
```
```   197 (** Version for Blast_tac.  Hyps that are affected by the substitution are
```
```   198     moved to the front.  Defect: even trivial changes are noticed, such as
```
```   199     substitutions in the arguments of a function Var. **)
```
```   200
```
```   201 (*final re-reversal of the changed assumptions*)
```
```   202 fun reverse_n_tac 0 i = all_tac
```
```   203   | reverse_n_tac 1 i = rotate_tac ~1 i
```
```   204   | reverse_n_tac n i =
```
```   205       REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
```
```   206       REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
```
```   207
```
```   208 (*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
```
```   209 fun all_imp_intr_tac hyps i =
```
```   210   let fun imptac (r, [])    st = reverse_n_tac r i st
```
```   211 	| imptac (r, hyp::hyps) st =
```
```   212 	   let val (hyp',_) = List.nth (prems_of st, i-1) |>
```
```   213 			      Logic.strip_assums_concl    |>
```
```   214 			      Data.dest_Trueprop          |> Data.dest_imp
```
```   215 	       val (r',tac) = if Pattern.aeconv (hyp,hyp')
```
```   216 			      then (r, imp_intr_tac i THEN rotate_tac ~1 i)
```
```   217 			      else (*leave affected hyps at end*)
```
```   218 				   (r+1, imp_intr_tac i)
```
```   219 	   in
```
```   220 	       case Seq.pull(tac st) of
```
```   221 		   None       => Seq.single(st)
```
```   222 		 | Some(st',_) => imptac (r',hyps) st'
```
```   223 	   end handle _ => error "?? in blast_hyp_subst_tac"
```
```   224   in  imptac (0, rev hyps)  end;
```
```   225
```
```   226
```
```   227 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
```
```   228       let val (k,symopt) = eq_var false false Bi
```
```   229 	  val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
```
```   230           (*omit selected equality, returning other hyps*)
```
```   231 	  val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
```
```   232 	  val n = length hyps
```
```   233       in
```
```   234 	 if !trace then writeln "Substituting an equality" else ();
```
```   235 	 DETERM
```
```   236            (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
```
```   237 		   rotate_tac 1 i,
```
```   238 		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
```
```   239 		   etac (if symopt then ssubst else Data.subst) i,
```
```   240 		   all_imp_intr_tac hyps i])
```
```   241       end
```
```   242       handle THM _ => no_tac | EQ_VAR => no_tac);
```
```   243
```
```   244 end;
```
```   245
```