src/Provers/hypsubst.ML
 author paulson Tue Nov 12 11:36:44 1996 +0100 (1996-11-12 ago) changeset 2174 0829b7b632c5 parent 2143 093bbe6d333b child 2722 3e07c20b967c permissions -rw-r--r--
Removed a call to polymorphic mem
```     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 the assumption x=t in the rest of the subgoal,
```
```     7 and to delete that assumption.  Original version due to Martin Coen.
```
```     8
```
```     9 This version uses the simplifier, and requires it to be already present.
```
```    10
```
```    11 Test data:
```
```    12
```
```    13 goal thy "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)";
```
```    14 goal thy "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)";
```
```    15 goal thy "!!y. [| ?x=y; P(?x) |] ==> y = a";
```
```    16 goal thy "!!z. [| ?x=y; P(?x) |] ==> y = a";
```
```    17
```
```    18 by (hyp_subst_tac 1);
```
```    19 by (bound_hyp_subst_tac 1);
```
```    20
```
```    21 Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
```
```    22 goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
```
```    23 *)
```
```    24
```
```    25 signature HYPSUBST_DATA =
```
```    26   sig
```
```    27   structure Simplifier : SIMPLIFIER
```
```    28   val dest_eq	       : term -> term*term
```
```    29   val eq_reflection    : thm		   (* a=b ==> a==b *)
```
```    30   val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
```
```    31   val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
```
```    32   val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
```
```    33   val sym	       : thm		   (* a=b ==> b=a *)
```
```    34   end;
```
```    35
```
```    36
```
```    37 signature HYPSUBST =
```
```    38   sig
```
```    39   val bound_hyp_subst_tac    : int -> tactic
```
```    40   val hyp_subst_tac          : int -> tactic
```
```    41     (*exported purely for debugging purposes*)
```
```    42   val gen_hyp_subst_tac      : bool -> int -> tactic
```
```    43   val vars_gen_hyp_subst_tac : bool -> int -> tactic
```
```    44   val eq_var                 : bool -> bool -> term -> int * bool
```
```    45   val inspect_pair           : bool -> bool -> term * term -> bool
```
```    46   val mk_eqs                 : thm -> thm list
```
```    47   val thin_leading_eqs_tac   : bool -> int -> int -> tactic
```
```    48   end;
```
```    49
```
```    50 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
```
```    51 struct
```
```    52
```
```    53 local open Data in
```
```    54
```
```    55 exception EQ_VAR;
```
```    56
```
```    57 fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
```
```    58
```
```    59 local val odot = ord"."
```
```    60 in
```
```    61 (*Simplifier turns Bound variables to dotted Free variables:
```
```    62   change it back (any Bound variable will do)
```
```    63 *)
```
```    64 fun contract t =
```
```    65     case Pattern.eta_contract t of
```
```    66 	Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T)
```
```    67       | t'        => t'
```
```    68 end;
```
```    69
```
```    70 fun has_vars t = maxidx_of_term t <> ~1;
```
```    71
```
```    72 (*If novars then we forbid Vars in the equality.
```
```    73   If bnd then we only look for Bound (or dotted Free) variables to eliminate.
```
```    74   When can we safely delete the equality?
```
```    75     Not if it equates two constants; consider 0=1.
```
```    76     Not if it resembles x=t[x], since substitution does not eliminate x.
```
```    77     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
```
```    78     Not if it involves a variable free in the premises,
```
```    79         but we can't check for this -- hence bnd and bound_hyp_subst_tac
```
```    80   Prefer to eliminate Bound variables if possible.
```
```    81   Result:  true = use as is,  false = reorient first *)
```
```    82 fun inspect_pair bnd novars (t,u) =
```
```    83   case (contract t, contract u) of
```
```    84        (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u
```
```    85 		       then raise Match
```
```    86 		       else true		(*eliminates t*)
```
```    87      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
```
```    88 		       then raise Match
```
```    89 		       else false		(*eliminates u*)
```
```    90      | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
```
```    91 		          novars andalso has_vars u
```
```    92 		       then raise Match
```
```    93 		       else true		(*eliminates t*)
```
```    94      | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
```
```    95 		          novars andalso has_vars t
```
```    96 		       then raise Match
```
```    97 		       else false		(*eliminates u*)
```
```    98      | _ => raise Match;
```
```    99
```
```   100 (*Locates a substitutable variable on the left (resp. right) of an equality
```
```   101    assumption.  Returns the number of intervening assumptions. *)
```
```   102 fun eq_var bnd novars =
```
```   103   let fun eq_var_aux k (Const("all",_) \$ Abs(_,_,t)) = eq_var_aux k t
```
```   104 	| eq_var_aux k (Const("==>",_) \$ A \$ B) =
```
```   105 	      ((k, inspect_pair bnd novars (dest_eq A))
```
```   106 		      (*Exception comes from inspect_pair or dest_eq*)
```
```   107 	       handle Match => eq_var_aux (k+1) B)
```
```   108 	| eq_var_aux k _ = raise EQ_VAR
```
```   109   in  eq_var_aux 0  end;
```
```   110
```
```   111 (*We do not try to delete ALL equality assumptions at once.  But
```
```   112   it is easy to handle several consecutive equality assumptions in a row.
```
```   113   Note that we have to inspect the proof state after doing the rewriting,
```
```   114   since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
```
```   115   must NOT be deleted.  Tactic must rotate or delete m assumptions.
```
```   116 *)
```
```   117 fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
```
```   118     let fun count []      = 0
```
```   119 	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);
```
```   120 			      1 + count Bs)
```
```   121                              handle Match => 0)
```
```   122 	val (_,_,Bi,_) = dest_state(state,i)
```
```   123         val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
```
```   124     in  REPEAT_DETERM_N j     (etac thin_rl i)   THEN
```
```   125         REPEAT_DETERM_N (m-j) (etac revcut_rl i)
```
```   126     end);
```
```   127
```
```   128 (*For the simpset.  Adds ALL suitable equalities, even if not first!
```
```   129   No vars are allowed here, as simpsets are built from meta-assumptions*)
```
```   130 fun mk_eqs th =
```
```   131     [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th)))
```
```   132       then th RS Data.eq_reflection
```
```   133       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
```
```   134     handle Match => [];  (*Exception comes from inspect_pair or dest_eq*)
```
```   135
```
```   136 local open Simplifier
```
```   137 in
```
```   138
```
```   139   val hyp_subst_ss = empty_ss setmksimps mk_eqs
```
```   140
```
```   141   (*Select a suitable equality assumption and substitute throughout the subgoal
```
```   142     Replaces only Bound variables if bnd is true*)
```
```   143   fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
```
```   144 	let val (_,_,Bi,_) = dest_state(state,i)
```
```   145 	    val n = length(Logic.strip_assums_hyp Bi) - 1
```
```   146 	    val (k,_) = eq_var bnd true Bi
```
```   147 	in
```
```   148 	   EVERY [REPEAT_DETERM_N k (etac revcut_rl i),
```
```   149 		  asm_full_simp_tac hyp_subst_ss i,
```
```   150 		  etac thin_rl i,
```
```   151 		  thin_leading_eqs_tac bnd (n-k) i]
```
```   152 	end
```
```   153 	handle THM _ => no_tac | EQ_VAR => no_tac));
```
```   154
```
```   155 end;
```
```   156
```
```   157 val ssubst = standard (sym RS subst);
```
```   158
```
```   159 (*Old version of the tactic above -- slower but the only way
```
```   160   to handle equalities containing Vars.*)
```
```   161 fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
```
```   162       let val (_,_,Bi,_) = dest_state(state,i)
```
```   163 	  val n = length(Logic.strip_assums_hyp Bi) - 1
```
```   164 	  val (k,symopt) = eq_var bnd false Bi
```
```   165       in
```
```   166 	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
```
```   167 		etac revcut_rl i,
```
```   168 		REPEAT_DETERM_N (n-k) (etac rev_mp i),
```
```   169 		etac (if symopt then ssubst else subst) i,
```
```   170 		REPEAT_DETERM_N n (rtac imp_intr i)]
```
```   171       end
```
```   172       handle THM _ => no_tac | EQ_VAR => no_tac));
```
```   173
```
```   174 (*Substitutes for Free or Bound variables*)
```
```   175 val hyp_subst_tac =
```
```   176     gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false;
```
```   177
```
```   178 (*Substitutes for Bound variables only -- this is always safe*)
```
```   179 val bound_hyp_subst_tac =
```
```   180     gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
```
```   181
```
```   182 end
```
```   183 end;
```
```   184
```