src/Provers/hypsubst.ML
 author paulson Tue Jul 22 11:12:55 1997 +0200 (1997-07-22 ago) changeset 3537 79ac9b475621 parent 2750 fe3799355b5e child 4179 cc4b6791d5dc permissions -rw-r--r--
Removal of the tactical STATE
 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 lcp@1011 28 val dest_eq : term -> term*term 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 lcp@1011 45 val inspect_pair : bool -> bool -> term * term -> 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 *) lcp@1011 84 fun inspect_pair bnd novars (t,u) = lcp@1011 85 case (contract t, contract u) of lcp@1011 86 (Bound i, _) => if loose(i,u) orelse novars andalso has_vars u lcp@1011 87 then raise Match lcp@1011 88 else true (*eliminates t*) lcp@1011 89 | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t lcp@1011 90 then raise Match lcp@1011 91 else false (*eliminates u*) lcp@1011 92 | (Free _, _) => if bnd orelse Logic.occs(t,u) orelse lcp@1011 93 novars andalso has_vars u lcp@1011 94 then raise Match lcp@1011 95 else true (*eliminates t*) lcp@1011 96 | (_, Free _) => if bnd orelse Logic.occs(u,t) orelse lcp@1011 97 novars andalso has_vars t lcp@1011 98 then raise Match lcp@1011 99 else false (*eliminates u*) clasohm@0 100 | _ => raise Match; clasohm@0 101 lcp@680 102 (*Locates a substitutable variable on the left (resp. right) of an equality lcp@1011 103 assumption. Returns the number of intervening assumptions. *) lcp@1011 104 fun eq_var bnd novars = lcp@680 105 let fun eq_var_aux k (Const("all",_) \$ Abs(_,_,t)) = eq_var_aux k t lcp@680 106 | eq_var_aux k (Const("==>",_) \$ A \$ B) = lcp@1011 107 ((k, inspect_pair bnd novars (dest_eq A)) lcp@1011 108 (*Exception comes from inspect_pair or dest_eq*) lcp@680 109 handle Match => eq_var_aux (k+1) B) lcp@680 110 | eq_var_aux k _ = raise EQ_VAR lcp@680 111 in eq_var_aux 0 end; clasohm@0 112 lcp@1011 113 (*We do not try to delete ALL equality assumptions at once. But lcp@1011 114 it is easy to handle several consecutive equality assumptions in a row. lcp@1011 115 Note that we have to inspect the proof state after doing the rewriting, lcp@1011 116 since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality lcp@1011 117 must NOT be deleted. Tactic must rotate or delete m assumptions. lcp@1011 118 *) paulson@3537 119 fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => lcp@1011 120 let fun count [] = 0 lcp@1011 121 | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); lcp@1011 122 1 + count Bs) lcp@1011 123 handle Match => 0) paulson@2143 124 val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) paulson@2722 125 in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i lcp@1011 126 end); lcp@1011 127 lcp@1011 128 (*For the simpset. Adds ALL suitable equalities, even if not first! lcp@1011 129 No vars are allowed here, as simpsets are built from meta-assumptions*) lcp@1011 130 fun mk_eqs th = lcp@1011 131 [ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) lcp@1011 132 then th RS Data.eq_reflection lcp@1011 133 else symmetric(th RS Data.eq_reflection) (*reorient*) ] lcp@1011 134 handle Match => []; (*Exception comes from inspect_pair or dest_eq*) lcp@1011 135 lcp@1011 136 local open Simplifier lcp@1011 137 in lcp@1011 138 lcp@1011 139 val hyp_subst_ss = empty_ss setmksimps mk_eqs lcp@1011 140 lcp@1011 141 (*Select a suitable equality assumption and substitute throughout the subgoal lcp@1011 142 Replaces only Bound variables if bnd is true*) paulson@3537 143 fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => paulson@3537 144 let val n = length(Logic.strip_assums_hyp Bi) - 1 lcp@1011 145 val (k,_) = eq_var bnd true Bi lcp@1011 146 in paulson@3537 147 DETERM (EVERY [rotate_tac k i, paulson@3537 148 asm_full_simp_tac hyp_subst_ss i, paulson@3537 149 etac thin_rl i, paulson@3537 150 thin_leading_eqs_tac bnd (n-k) i]) lcp@1011 151 end paulson@3537 152 handle THM _ => no_tac | EQ_VAR => no_tac); lcp@1011 153 lcp@1011 154 end; lcp@1011 155 lcp@1011 156 val ssubst = standard (sym RS subst); lcp@1011 157 lcp@1011 158 (*Old version of the tactic above -- slower but the only way lcp@1011 159 to handle equalities containing Vars.*) paulson@3537 160 fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => paulson@3537 161 let val n = length(Logic.strip_assums_hyp Bi) - 1 lcp@1011 162 val (k,symopt) = eq_var bnd false Bi lcp@680 163 in paulson@3537 164 DETERM paulson@3537 165 (EVERY [REPEAT_DETERM_N k (etac rev_mp i), paulson@3537 166 etac revcut_rl i, paulson@3537 167 REPEAT_DETERM_N (n-k) (etac rev_mp i), paulson@3537 168 etac (if symopt then ssubst else subst) i, paulson@3537 169 REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) clasohm@0 170 end paulson@3537 171 handle THM _ => no_tac | EQ_VAR => no_tac); clasohm@0 172 clasohm@0 173 (*Substitutes for Free or Bound variables*) lcp@1011 174 val hyp_subst_tac = lcp@1011 175 gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; clasohm@0 176 clasohm@0 177 (*Substitutes for Bound variables only -- this is always safe*) lcp@1011 178 val bound_hyp_subst_tac = lcp@1011 179 gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; clasohm@0 180 clasohm@0 181 end clasohm@0 182 end; clasohm@0 183