Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
authorpaulson
Tue Dec 23 11:39:03 1997 +0100 (1997-12-23 ago)
changeset 4466305390f23734
parent 4465 7ba65fe66c73
child 4467 bd05e2a28602
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
src/FOL/ROOT.ML
src/FOL/cladata.ML
src/FOL/fologic.ML
src/HOL/cladata.ML
src/HOL/hologic.ML
src/Provers/blast.ML
src/Provers/hypsubst.ML
     1.1 --- a/src/FOL/ROOT.ML	Tue Dec 23 11:37:48 1997 +0100
     1.2 +++ b/src/FOL/ROOT.ML	Tue Dec 23 11:39:03 1997 +0100
     1.3 @@ -28,9 +28,10 @@
     1.4  structure Hypsubst_Data =
     1.5    struct
     1.6    structure Simplifier = Simplifier
     1.7 -    (*Take apart an equality judgement; otherwise raise Match!*)
     1.8 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
     1.9 -	(t, u, domain_type T)
    1.10 +    (*These destructors  Match!*)
    1.11 +  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
    1.12 +  val dest_Trueprop = FOLogic.dest_Trueprop
    1.13 +  val dest_imp = FOLogic.dest_imp
    1.14    val eq_reflection = eq_reflection
    1.15    val imp_intr = impI
    1.16    val rev_mp = rev_mp
     2.1 --- a/src/FOL/cladata.ML	Tue Dec 23 11:37:48 1997 +0100
     2.2 +++ b/src/FOL/cladata.ML	Tue Dec 23 11:39:03 1997 +0100
     2.3 @@ -54,7 +54,7 @@
     2.4    val ccontr	= ccontr
     2.5    val contr_tac = Cla.contr_tac
     2.6    val dup_intr	= Cla.dup_intr
     2.7 -  val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
     2.8 +  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     2.9    val claset	= Cla.claset
    2.10    val rep_claset = Cla.rep_claset
    2.11    end;
     3.1 --- a/src/FOL/fologic.ML	Tue Dec 23 11:37:48 1997 +0100
     3.2 +++ b/src/FOL/fologic.ML	Tue Dec 23 11:39:03 1997 +0100
     3.3 @@ -10,6 +10,7 @@
     3.4    val oT: typ
     3.5    val mk_Trueprop: term -> term
     3.6    val dest_Trueprop: term -> term
     3.7 +  val dest_imp	       : term -> term*term
     3.8    val conj: term
     3.9    val disj: term
    3.10    val imp: term
    3.11 @@ -40,6 +41,9 @@
    3.12  and disj = Const("op |", [oT,oT]--->oT)
    3.13  and imp = Const("op -->", [oT,oT]--->oT);
    3.14  
    3.15 +fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
    3.16 +  | dest_imp  t = raise TERM ("dest_imp", [t]);
    3.17 +
    3.18  fun eq_const T = Const ("op =", [T, T] ---> oT);
    3.19  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    3.20  
     4.1 --- a/src/HOL/cladata.ML	Tue Dec 23 11:37:48 1997 +0100
     4.2 +++ b/src/HOL/cladata.ML	Tue Dec 23 11:39:03 1997 +0100
     4.3 @@ -14,8 +14,9 @@
     4.4    struct
     4.5    structure Simplifier = Simplifier
     4.6    (*Take apart an equality judgement; otherwise raise Match!*)
     4.7 -  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
     4.8 -	(t, u, domain_type T)
     4.9 +  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
    4.10 +  val dest_Trueprop = HOLogic.dest_Trueprop
    4.11 +  val dest_imp = HOLogic.dest_imp
    4.12    val eq_reflection = eq_reflection
    4.13    val imp_intr = impI
    4.14    val rev_mp = rev_mp
    4.15 @@ -72,7 +73,7 @@
    4.16    val ccontr	= ccontr
    4.17    val contr_tac = Classical.contr_tac
    4.18    val dup_intr	= Classical.dup_intr
    4.19 -  val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
    4.20 +  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    4.21    val claset	= Classical.claset
    4.22    val rep_claset = Classical.rep_claset
    4.23    end;
     5.1 --- a/src/HOL/hologic.ML	Tue Dec 23 11:37:48 1997 +0100
     5.2 +++ b/src/HOL/hologic.ML	Tue Dec 23 11:39:03 1997 +0100
     5.3 @@ -18,6 +18,7 @@
     5.4    val conj: term
     5.5    val disj: term
     5.6    val imp: term
     5.7 +  val dest_imp	       : term -> term*term
     5.8    val eq_const: typ -> term
     5.9    val all_const: typ -> term
    5.10    val exists_const: typ -> term
    5.11 @@ -73,6 +74,9 @@
    5.12  and disj = Const ("op |", [boolT, boolT] ---> boolT)
    5.13  and imp = Const ("op -->", [boolT, boolT] ---> boolT);
    5.14  
    5.15 +fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
    5.16 +  | dest_imp  t = raise TERM ("dest_imp", [t]);
    5.17 +
    5.18  fun eq_const T = Const ("op =", [T, T] ---> boolT);
    5.19  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    5.20  
     6.1 --- a/src/Provers/blast.ML	Tue Dec 23 11:37:48 1997 +0100
     6.2 +++ b/src/Provers/blast.ML	Tue Dec 23 11:39:03 1997 +0100
     6.3 @@ -58,7 +58,7 @@
     6.4    val ccontr		: thm		
     6.5    val contr_tac 	: int -> tactic
     6.6    val dup_intr		: thm -> thm
     6.7 -  val vars_gen_hyp_subst_tac : bool -> int -> tactic
     6.8 +  val hyp_subst_tac     : bool ref -> int -> tactic
     6.9    val claset		: unit -> claset
    6.10    val rep_claset	: 
    6.11        claset -> {safeIs: thm list, safeEs: thm list, 
    6.12 @@ -731,26 +731,31 @@
    6.13    let val (t,u) = orientGoal(dest_eq G)
    6.14        val subst = subst_atomic (t,u)
    6.15        fun subst2(G,md) = (subst G, md)
    6.16 -      (*substitute throughout Haz list; move affected ones to Safe part*)
    6.17 -      fun subHazs ([], Gs, nHs)         = (Gs,nHs)
    6.18 -	| subHazs ((H,md)::Hs, Gs, nHs) =
    6.19 -	    let val nH = subst H
    6.20 -	    in  if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs)
    6.21 -		              else subHazs (Hs, (nH,md)::Gs, nHs)
    6.22 +      (*substitute throughout list; extract affected formulae*)
    6.23 +      fun subForm ((G,md), (changed, pairs)) =
    6.24 +	    let val nG = subst G
    6.25 +	    in  if nG aconv G then (changed, (G,md)::pairs)
    6.26 +		              else ((nG,md)::changed, pairs)
    6.27              end
    6.28 -      val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs
    6.29 -      (*substitute throughout literals; move affected ones to Safe part*)
    6.30 -      fun subLits ([], [], nlits) =          (pairs', nlits, vars, lim)
    6.31 -	| subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim)
    6.32 -	| subLits (lit::lits, Gs, nlits) =
    6.33 +      (*substitute throughout "stack frame"; extract affected formulae*)
    6.34 +      fun subFrame ((Gs,Hs), (changed, frames)) =
    6.35 +	    let val (changed', Gs') = foldr subForm (Gs, (changed, []))
    6.36 +                val (changed'', Hs') = foldr subForm (Hs, (changed', []))
    6.37 +            in  (changed'', (Gs',Hs')::frames)  end
    6.38 +      (*substitute throughout literals; extract affected ones*)
    6.39 +      fun subLit (lit, (changed, nlits)) =
    6.40  	    let val nlit = subst lit
    6.41 -	    in  if nlit aconv lit then subLits (lits, Gs, nlit::nlits)
    6.42 -		                  else subLits (lits, (nlit,true)::Gs, nlits)
    6.43 +	    in  if nlit aconv lit then (changed, nlit::nlits)
    6.44 +		                  else ((nlit,true)::changed, nlits)
    6.45              end
    6.46 +      val (changed, lits') = foldr subLit (lits, ([], []))
    6.47 +      val (changed', pairs') = foldr subFrame (pairs, (changed, []))
    6.48    in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
    6.49  			      " for " ^ traceTerm sign t ^ " in branch" )
    6.50        else ();
    6.51 -      subLits (rev lits, [], [])  
    6.52 +      ((changed',[])::pairs',	(*affected formulas, and others*)
    6.53 +       lits',			(*unaffected literals*)
    6.54 +       vars, lim)
    6.55    end;
    6.56  
    6.57  
    6.58 @@ -1007,7 +1012,7 @@
    6.59  	  in tracing sign brs0; 
    6.60  	     if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
    6.61  	     else
    6.62 -	     prv (Data.vars_gen_hyp_subst_tac false  ::  tacs, 
    6.63 +	     prv (Data.hyp_subst_tac trace :: tacs, 
    6.64  		  brs0::trs,  choices,
    6.65  		  equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs)
    6.66  	     handle DEST_EQ =>   closeF lits
    6.67 @@ -1015,16 +1020,18 @@
    6.68  	        handle CLOSEF => deeper rules
    6.69  		  handle NEWBRANCHES => 
    6.70  		   (case netMkRules G vars hazList of
    6.71 -		       [] => (*no plausible haz rules: move G to literals*)
    6.72 -			   prv (tacs, brs0::trs, choices,
    6.73 -				((br,haz)::pairs, addLit(G,lits), vars, lim)
    6.74 -				::brs)
    6.75 +		       [] => (*there are no plausible haz rules*)
    6.76 +			   (traceMsg "moving goal to literals";
    6.77 +			    prv (tacs, brs0::trs, choices,
    6.78 +				 ((br,haz)::pairs, addLit(G,lits), vars, lim)
    6.79 +				 ::brs))
    6.80  		    | _ => (*G admits some haz rules: try later*)
    6.81 -			   prv (if isGoal G then negOfGoal_tac :: tacs
    6.82 -				else tacs, 
    6.83 -				brs0::trs,  choices,
    6.84 -				((br, haz@[(negOfGoal G, md)])::pairs,
    6.85 -				 lits, vars, lim)  ::  brs))
    6.86 +			   (traceMsg "moving goal to haz list";
    6.87 +			    prv (if isGoal G then negOfGoal_tac :: tacs
    6.88 +				 else tacs, 
    6.89 +				     brs0::trs,  choices,
    6.90 +				     ((br, haz@[(negOfGoal G, md)])::pairs,
    6.91 +				      lits, vars, lim)  ::  brs)))
    6.92  	  end
    6.93         | prv (tacs, trs, choices, 
    6.94  	      (([],haz)::(Gs,haz')::pairs, lits, vars, lim) :: brs) =
     7.1 --- a/src/Provers/hypsubst.ML	Tue Dec 23 11:37:48 1997 +0100
     7.2 +++ b/src/Provers/hypsubst.ML	Tue Dec 23 11:39:03 1997 +0100
     7.3 @@ -21,25 +21,32 @@
     7.4  
     7.5  Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a))
     7.6  goal thy "P(a) --> (EX y. a=y --> P(f(a)))";
     7.7 +
     7.8 +goal thy "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \
     7.9 +\                 P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)";
    7.10 +by (blast_hyp_subst_tac (ref true) 1);
    7.11  *)
    7.12  
    7.13  signature HYPSUBST_DATA =
    7.14    sig
    7.15    structure Simplifier : SIMPLIFIER
    7.16 +  val dest_Trueprop    : term -> term
    7.17    val dest_eq	       : term -> term*term*typ
    7.18 +  val dest_imp	       : term -> term*term
    7.19    val eq_reflection    : thm		   (* a=b ==> a==b *)
    7.20    val imp_intr	       : thm		   (* (P ==> Q) ==> P-->Q *)
    7.21    val rev_mp	       : thm		   (* [| P;  P-->Q |] ==> Q *)
    7.22    val subst	       : thm		   (* [| a=b;  P(a) |] ==> P(b) *)
    7.23    val sym	       : thm		   (* a=b ==> b=a *)
    7.24    val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    7.25 -end;
    7.26 +  end;
    7.27  
    7.28  
    7.29  signature HYPSUBST =
    7.30    sig
    7.31    val bound_hyp_subst_tac    : int -> tactic
    7.32    val hyp_subst_tac          : int -> tactic
    7.33 +  val blast_hyp_subst_tac    : bool ref -> int -> tactic
    7.34      (*exported purely for debugging purposes*)
    7.35    val gen_hyp_subst_tac      : bool -> int -> tactic
    7.36    val vars_gen_hyp_subst_tac : bool -> int -> tactic
    7.37 @@ -54,8 +61,6 @@
    7.38  functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
    7.39  struct
    7.40  
    7.41 -local open Data in
    7.42 -
    7.43  exception EQ_VAR;
    7.44  
    7.45  fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
    7.46 @@ -109,9 +114,10 @@
    7.47  fun eq_var bnd novars =
    7.48    let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    7.49  	| eq_var_aux k (Const("==>",_) $ A $ B) = 
    7.50 -	      ((k, inspect_pair bnd novars (dest_eq A))
    7.51 +	      ((k, inspect_pair bnd novars 
    7.52 +		    (Data.dest_eq (Data.dest_Trueprop A)))
    7.53  		      (*Exception comes from inspect_pair or dest_eq*)
    7.54 -	       handle Match => eq_var_aux (k+1) B)
    7.55 +	       handle _ => eq_var_aux (k+1) B)
    7.56  	| eq_var_aux k _ = raise EQ_VAR
    7.57    in  eq_var_aux 0  end;
    7.58  
    7.59 @@ -123,9 +129,10 @@
    7.60  *)
    7.61  fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
    7.62      let fun count []      = 0
    7.63 -	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
    7.64 +	  | count (A::Bs) = ((inspect_pair bnd true 
    7.65 +			      (Data.dest_eq (Data.dest_Trueprop A));  
    7.66  			      1 + count Bs)
    7.67 -                             handle Match => 0)
    7.68 +                             handle _ => 0)
    7.69          val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
    7.70      in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
    7.71      end);
    7.72 @@ -133,10 +140,11 @@
    7.73  (*For the simpset.  Adds ALL suitable equalities, even if not first!
    7.74    No vars are allowed here, as simpsets are built from meta-assumptions*)
    7.75  fun mk_eqs th = 
    7.76 -    [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th)))
    7.77 +    [ if inspect_pair false false (Data.dest_eq 
    7.78 +				   (Data.dest_Trueprop (#prop (rep_thm th))))
    7.79        then th RS Data.eq_reflection
    7.80        else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
    7.81 -    handle Match => [];  (*Exception comes from inspect_pair or dest_eq*)
    7.82 +    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
    7.83  
    7.84  local open Simplifier 
    7.85  in
    7.86 @@ -158,7 +166,9 @@
    7.87  
    7.88  end;
    7.89  
    7.90 -val ssubst = standard (sym RS subst);
    7.91 +val ssubst = standard (Data.sym RS Data.subst);
    7.92 +
    7.93 +val imp_intr_tac = rtac Data.imp_intr;
    7.94  
    7.95  (*Old version of the tactic above -- slower but the only way
    7.96    to handle equalities containing Vars.*)
    7.97 @@ -167,22 +177,69 @@
    7.98  	  val (k,symopt) = eq_var bnd false Bi
    7.99        in 
   7.100  	 DETERM
   7.101 -           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
   7.102 -		   etac revcut_rl i,
   7.103 -		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
   7.104 -		   etac (if symopt then ssubst else subst) i,
   7.105 -		   REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)])
   7.106 +           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   7.107 +		   rotate_tac 1 i,
   7.108 +		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   7.109 +		   etac (if symopt then ssubst else Data.subst) i,
   7.110 +		   REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
   7.111        end
   7.112        handle THM _ => no_tac | EQ_VAR => no_tac);
   7.113  
   7.114  (*Substitutes for Free or Bound variables*)
   7.115 -val hyp_subst_tac = FIRST' [ematch_tac [thin_refl],
   7.116 +val hyp_subst_tac = FIRST' [ematch_tac [Data.thin_refl],
   7.117          gen_hyp_subst_tac false, vars_gen_hyp_subst_tac false];
   7.118  
   7.119  (*Substitutes for Bound variables only -- this is always safe*)
   7.120  val bound_hyp_subst_tac = 
   7.121      gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true;
   7.122  
   7.123 -end
   7.124 +
   7.125 +(** Version for Blast_tac.  Hyps that are affected by the substitution are 
   7.126 +    moved to the front.  Defect: even trivial changes are noticed, such as
   7.127 +    substitutions in the arguments of a function Var. **)
   7.128 +
   7.129 +(*final re-reversal of the changed assumptions*)
   7.130 +fun reverse_n_tac 0 i = all_tac
   7.131 +  | reverse_n_tac 1 i = rotate_tac ~1 i
   7.132 +  | reverse_n_tac n i = 
   7.133 +      REPEAT_DETERM_N n (rotate_tac ~1 i THEN etac Data.rev_mp i) THEN
   7.134 +      REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i);
   7.135 +
   7.136 +(*Use imp_intr, comparing the old hyps with the new ones as they come out.*)
   7.137 +fun all_imp_intr_tac hyps i = 
   7.138 +  let fun imptac (r, [])    st = reverse_n_tac r i st
   7.139 +	| imptac (r, hyp::hyps) st =
   7.140 +	   let val (hyp',_) = List.nth (prems_of st, i-1) |>
   7.141 +			      Logic.strip_assums_concl    |> 
   7.142 +			      Data.dest_Trueprop          |> Data.dest_imp
   7.143 +	       val (r',tac) = if Pattern.aeconv (hyp,hyp')
   7.144 +			      then (r, imp_intr_tac i THEN rotate_tac ~1 i)
   7.145 +			      else (*leave affected hyps at end*)
   7.146 +				   (r+1, imp_intr_tac i) 
   7.147 +	   in
   7.148 +	       case Seq.pull(tac st) of
   7.149 +		   None       => Seq.single(st)
   7.150 +		 | Some(st',_) => imptac (r',hyps) st'
   7.151 +	   end handle _ => error "?? in blast_hyp_subst_tac"
   7.152 +  in  imptac (0, rev hyps)  end;
   7.153 +
   7.154 +
   7.155 +fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
   7.156 +      let val (k,symopt) = eq_var false false Bi
   7.157 +	  val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
   7.158 +          (*omit selected equality, returning other hyps*)
   7.159 +	  val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1)
   7.160 +	  val n = length hyps
   7.161 +      in 
   7.162 +	 if !trace then writeln "Substituting an equality" else ();
   7.163 +	 DETERM
   7.164 +           (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i),
   7.165 +		   rotate_tac 1 i,
   7.166 +		   REPEAT_DETERM_N (n-k) (etac Data.rev_mp i),
   7.167 +		   etac (if symopt then ssubst else Data.subst) i,
   7.168 +		   all_imp_intr_tac hyps i])
   7.169 +      end
   7.170 +      handle THM _ => no_tac | EQ_VAR => no_tac);
   7.171 +
   7.172  end;
   7.173