src/Provers/hypsubst.ML
changeset 4466 305390f23734
parent 4299 22596d62ce0b
child 9532 36b9bc6eb454
     1.1 --- a/src/Provers/hypsubst.ML	Tue Dec 23 11:37:48 1997 +0100
     1.2 +++ b/src/Provers/hypsubst.ML	Tue Dec 23 11:39:03 1997 +0100
     1.3 @@ -21,25 +21,32 @@
     1.4  
     1.5  Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
     1.6  goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
     1.7 +
     1.8 +goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
     1.9 +\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    1.10 +by (blast_hyp_subst_tac (ref true) 1);
    1.11  *)
    1.12  
    1.13  signature HYPSUBST_DATA =
    1.14    sig
    1.15    structure Simplifier : SIMPLIFIER
    1.16 +  val dest_Trueprop    : term -> term
    1.17    val dest_eq	       : term -> term*term*typ
    1.18 +  val dest_imp	       : term -> term*term
    1.19    val eq_reflection    : thm		   (* a=b ==> a==b *)
    1.20    val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
    1.21    val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    1.22    val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
    1.23    val sym	       : thm		   (* a=b ==> b=a *)
    1.24    val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    1.25 -end;
    1.26 +  end;
    1.27  
    1.28  
    1.29  signature HYPSUBST =
    1.30    sig
    1.31    val bound_hyp_subst_tac    : int -> tactic
    1.32    val hyp_subst_tac          : int -> tactic
    1.33 +  val blast_hyp_subst_tac    : bool ref -> int -> tactic
    1.34      (*exported purely for debugging purposes*)
    1.35    val gen_hyp_subst_tac      : bool -> int -> tactic
    1.36    val vars_gen_hyp_subst_tac : bool -> int -> tactic
    1.37 @@ -54,8 +61,6 @@
    1.38  functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
    1.39  struct
    1.40  
    1.41 -local open Data in
    1.42 -
    1.43  exception EQ_VAR;
    1.44  
    1.45  fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
    1.46 @@ -109,9 +114,10 @@
    1.47  fun eq_var bnd novars =
    1.48    let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    1.49  	| eq_var_aux k (Const("==>",_) $ A $ B) = 
    1.50 -	      ((k, inspect_pair bnd novars (dest_eq A))
    1.51 +	      ((k, inspect_pair bnd novars 
    1.52 +		    (Data.dest_eq (Data.dest_Trueprop A)))
    1.53  		      (*Exception comes from inspect_pair or dest_eq*)
    1.54 -	       handle Match => eq_var_aux (k+1) B)
    1.55 +	       handle _ => eq_var_aux (k+1) B)
    1.56  	| eq_var_aux k _ = raise EQ_VAR
    1.57    in  eq_var_aux 0  end;
    1.58  
    1.59 @@ -123,9 +129,10 @@
    1.60  *)
    1.61  fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
    1.62      let fun count []      = 0
    1.63 -	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
    1.64 +	  | count (A::Bs) = ((inspect_pair bnd true 
    1.65 +			      (Data.dest_eq (Data.dest_Trueprop A));  
    1.66  			      1 + count Bs)
    1.67 -                             handle Match => 0)
    1.68 +                             handle _ => 0)
    1.69          val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
    1.70      in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
    1.71      end);
    1.72 @@ -133,10 +140,11 @@
    1.73  (*For the simpset.  Adds ALL suitable equalities, even if not first!
    1.74    No vars are allowed here, as simpsets are built from meta-assumptions*)
    1.75  fun mk_eqs th = 
    1.76 -    [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th)))
    1.77 +    [ if inspect_pair false false (Data.dest_eq 
    1.78 +				   (Data.dest_Trueprop (#prop (rep_thm th))))
    1.79        then th RS Data.eq_reflection
    1.80        else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
    1.81 -    handle Match => [];  (*Exception comes from inspect_pair or dest_eq*)
    1.82 +    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
    1.83  
    1.84  local open Simplifier 
    1.85  in
    1.86 @@ -158,7 +166,9 @@
    1.87  
    1.88  end;
    1.89  
    1.90 -val ssubst = standard (sym RS subst);
    1.91 +val ssubst = standard (Data.sym RS Data.subst);
    1.92 +
    1.93 +val imp_intr_tac = rtac Data.imp_intr;
    1.94  
    1.95  (*Old version of the tactic above -- slower but the only way
    1.96    to handle equalities containing Vars.*)
    1.97 @@ -167,22 +177,69 @@
    1.98  	  val (k,symopt) = eq_var bnd false Bi
    1.99        in 
   1.100  	 DETERM
   1.101 -           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   1.102 -		   etac revcut_rl i,
   1.103 -		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
   1.104 -		   etac (if symopt then ssubst else subst) i,
   1.105 -		   REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)])
   1.106 +           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   1.107 +		   rotate_tac 1 i,
   1.108 +		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   1.109 +		   etac (if symopt then ssubst else Data.subst) i,
   1.110 +		   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   1.111        end
   1.112        handle THM _ => no_tac | EQ_VAR => no_tac);
   1.113  
   1.114  (*Substitutes for Free or Bound variables*)
   1.115 -val hyp_subst_tac = FIRST' [ematch_tac [thin_refl],
   1.116 +val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   1.117          gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
   1.118  
   1.119  (*Substitutes for Bound variables only -- this is always safe*)
   1.120  val bound_hyp_subst_tac = 
   1.121      gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
   1.122  
   1.123 -end
   1.124 +
   1.125 +(** Version for Blast_tac.  Hyps that are affected by the substitution are 
   1.126 +    moved to the front.  Defect: even trivial changes are noticed, such as
   1.127 +    substitutions in the arguments of a function Var. **)
   1.128 +
   1.129 +(*final re-reversal of the changed assumptions*)
   1.130 +fun reverse_n_tac 0 i = all_tac
   1.131 +  | reverse_n_tac 1 i = rotate_tac ~1 i
   1.132 +  | reverse_n_tac n i = 
   1.133 +      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   1.134 +      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   1.135 +
   1.136 +(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   1.137 +fun all_imp_intr_tac hyps i = 
   1.138 +  let fun imptac (r, [])    st = reverse_n_tac r i st
   1.139 +	| imptac (r, hyp::hyps) st =
   1.140 +	   let val (hyp',_) = List.nth (prems_of st, i-1) |>
   1.141 +			      Logic.strip_assums_concl    |> 
   1.142 +			      Data.dest_Trueprop          |> Data.dest_imp
   1.143 +	       val (r',tac) = if Pattern.aeconv (hyp,hyp')
   1.144 +			      then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   1.145 +			      else (*leave affected hyps at end*)
   1.146 +				   (r+1, imp_intr_tac i) 
   1.147 +	   in
   1.148 +	       case Seq.pull(tac st) of
   1.149 +		   None       => Seq.single(st)
   1.150 +		 | Some(st',_) => imptac (r',hyps) st'
   1.151 +	   end handle _ => error "?? in blast_hyp_subst_tac"
   1.152 +  in  imptac (0, rev hyps)  end;
   1.153 +
   1.154 +
   1.155 +fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   1.156 +      let val (k,symopt) = eq_var false false Bi
   1.157 +	  val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   1.158 +          (*omit selected equality, returning other hyps*)
   1.159 +	  val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   1.160 +	  val n = length hyps
   1.161 +      in 
   1.162 +	 if !trace then writeln "Substituting an equality" else ();
   1.163 +	 DETERM
   1.164 +           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   1.165 +		   rotate_tac 1 i,
   1.166 +		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   1.167 +		   etac (if symopt then ssubst else Data.subst) i,
   1.168 +		   all_imp_intr_tac hyps i])
   1.169 +      end
   1.170 +      handle THM _ => no_tac | EQ_VAR => no_tac);
   1.171 +
   1.172  end;
   1.173