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