1(* Title: Provers/hypsubst.ML 2 Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson 3 Copyright 1995 University of Cambridge 4 5Basic equational reasoning: hyp_subst_tac and methods "hypsubst", "simplesubst". 6 7Tactic to substitute using (at least) the assumption x=t in the rest 8of the subgoal, and to delete (at least) that assumption. Original 9version due to Martin Coen. 10 11This version uses the simplifier, and requires it to be already present. 12 13Test data: 14 15Goal "!!x.[| Q(x,y,z); y=x; a=x; z=y; P(y) |] ==> P(z)"; 16Goal "!!x.[| Q(x,y,z); z=f(x); x=z |] ==> P(z)"; 17Goal "!!y. [| ?x=y; P(?x) |] ==> y = a"; 18Goal "!!z. [| ?x=y; P(?x) |] ==> y = a"; 19 20Goal "!!x a. [| x = f(b); g(a) = b |] ==> P(x)"; 21 22by (bound_hyp_subst_tac 1); 23by (hyp_subst_tac 1); 24 25Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) 26Goal "P(a) --> (EX y. a=y --> P(f(a)))"; 27 28Goal "!!x. [| Q(x,h1); P(a,h2); R(x,y,h3); R(y,z,h4); x=f(y); \ 29\ P(x,h5); P(y,h6); K(x,h7) |] ==> Q(x,c)"; 30by (blast_hyp_subst_tac true 1); 31*) 32 33signature HYPSUBST_DATA = 34sig 35 val dest_Trueprop : term -> term 36 val dest_eq : term -> term * term 37 val dest_imp : term -> term * term 38 val eq_reflection : thm (* a=b ==> a==b *) 39 val rev_eq_reflection: thm (* a==b ==> a=b *) 40 val imp_intr : thm (* (P ==> Q) ==> P-->Q *) 41 val rev_mp : thm (* [| P; P-->Q |] ==> Q *) 42 val subst : thm (* [| a=b; P(a) |] ==> P(b) *) 43 val sym : thm (* a=b ==> b=a *) 44 val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *) 45end; 46 47signature HYPSUBST = 48sig 49 val bound_hyp_subst_tac : Proof.context -> int -> tactic 50 val hyp_subst_tac_thin : bool -> Proof.context -> int -> tactic 51 val hyp_subst_thin : bool Config.T 52 val hyp_subst_tac : Proof.context -> int -> tactic 53 val blast_hyp_subst_tac : Proof.context -> bool -> int -> tactic 54 val stac : Proof.context -> thm -> int -> tactic 55end; 56 57functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST = 58struct 59 60exception EQ_VAR; 61 62(*Simplifier turns Bound variables to special Free variables: 63 change it back (any Bound variable will do)*) 64fun inspect_contract t = 65 (case Envir.eta_contract t of 66 Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T) 67 | t' => t'); 68 69val has_vars = Term.exists_subterm Term.is_Var; 70val has_tvars = Term.exists_type (Term.exists_subtype Term.is_TVar); 71 72(*If novars then we forbid Vars in the equality. 73 If bnd then we only look for Bound 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; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P 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 also returns var to substitute, relevant if it is Free *) 83fun inspect_pair bnd novars (t, u) = 84 if novars andalso (has_tvars t orelse has_tvars u) 85 then raise Match (*variables in the type!*) 86 else 87 (case apply2 inspect_contract (t, u) of 88 (Bound i, _) => 89 if loose_bvar1 (u, i) orelse novars andalso has_vars u 90 then raise Match 91 else (true, Bound i) (*eliminates t*) 92 | (_, Bound i) => 93 if loose_bvar1 (t, i) orelse novars andalso has_vars t 94 then raise Match 95 else (false, Bound i) (*eliminates u*) 96 | (t' as Free _, _) => 97 if bnd orelse Logic.occs (t', u) orelse novars andalso has_vars u 98 then raise Match 99 else (true, t') (*eliminates t*) 100 | (_, u' as Free _) => 101 if bnd orelse Logic.occs (u', t) orelse novars andalso has_vars t 102 then raise Match 103 else (false, u') (*eliminates u*) 104 | _ => raise Match); 105 106(*Locates a substitutable variable on the left (resp. right) of an equality 107 assumption. Returns the number of intervening assumptions. *) 108fun eq_var bnd novars check_frees t = 109 let 110 fun check_free ts (orient, Free f) 111 = if not check_frees orelse not orient 112 orelse exists (curry Logic.occs (Free f)) ts 113 then (orient, true) else raise Match 114 | check_free ts (orient, _) = (orient, false) 115 fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) hs = eq_var_aux k t hs 116 | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) hs = 117 ((k, check_free (B :: hs) (inspect_pair bnd novars 118 (Data.dest_eq (Data.dest_Trueprop A)))) 119 handle TERM _ => eq_var_aux (k+1) B (A :: hs) 120 | Match => eq_var_aux (k+1) B (A :: hs)) 121 | eq_var_aux k _ _ = raise EQ_VAR 122 123 in eq_var_aux 0 t [] end; 124 125fun thin_free_eq_tac ctxt = SUBGOAL (fn (t, i) => 126 let 127 val (k, _) = eq_var false false false t 128 val ok = (eq_var false false true t |> fst) > k handle EQ_VAR => true 129 in 130 if ok then EVERY [rotate_tac k i, eresolve_tac ctxt [thin_rl] i, rotate_tac (~k) i] 131 else no_tac 132 end handle EQ_VAR => no_tac) 133 134(*For the simpset. Adds ALL suitable equalities, even if not first! 135 No vars are allowed here, as simpsets are built from meta-assumptions*) 136fun mk_eqs bnd th = 137 [ if inspect_pair bnd false (Data.dest_eq (Data.dest_Trueprop (Thm.prop_of th))) |> fst 138 then th RS Data.eq_reflection 139 else Thm.symmetric(th RS Data.eq_reflection) (*reorient*) ] 140 handle TERM _ => [] | Match => []; 141 142fun bool2s true = "true" | bool2s false = "false" 143 144local 145in 146 147 (*Select a suitable equality assumption; substitute throughout the subgoal 148 If bnd is true, then it replaces Bound variables only. *) 149 fun gen_hyp_subst_tac ctxt bnd = 150 SUBGOAL (fn (Bi, i) => 151 let 152 val (k, (orient, is_free)) = eq_var bnd true true Bi 153 val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd)) 154 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, 155 if not is_free then eresolve_tac ctxt [thin_rl] i 156 else if orient then eresolve_tac ctxt [Data.rev_mp] i 157 else eresolve_tac ctxt [Data.sym RS Data.rev_mp] i, 158 rotate_tac (~k) i, 159 if is_free then resolve_tac ctxt [Data.imp_intr] i else all_tac] 160 end handle THM _ => no_tac | EQ_VAR => no_tac) 161 162end; 163 164val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst); 165 166fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) => 167 case try (Logic.strip_assums_hyp #> hd #> 168 Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_contract) (Thm.term_of cBi) of 169 SOME (t, t') => 170 let 171 val Bi = Thm.term_of cBi; 172 val ps = Logic.strip_params Bi; 173 val U = Term.fastype_of1 (rev (map snd ps), t); 174 val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi); 175 val rl' = Thm.lift_rule cBi rl; 176 val Var (ixn, T) = Term.head_of (Data.dest_Trueprop 177 (Logic.strip_assums_concl (Thm.prop_of rl'))); 178 val (v1, v2) = Data.dest_eq (Data.dest_Trueprop 179 (Logic.strip_assums_concl (hd (Thm.prems_of rl')))); 180 val (Ts, V) = split_last (Term.binder_types T); 181 val u = 182 fold_rev Term.abs (ps @ [("x", U)]) 183 (case (if b then t else t') of 184 Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) 185 | t => Term.abstract_over (t, Term.incr_boundvars 1 Q)); 186 val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); 187 in 188 compose_tac ctxt (true, Drule.instantiate_normalize (instT, 189 map (apsnd (Thm.cterm_of ctxt)) 190 [((ixn, Ts ---> U --> body_type T), u), 191 ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), 192 ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', 193 Thm.nprems_of rl) i 194 end 195 | NONE => no_tac); 196 197fun imp_intr_tac ctxt = resolve_tac ctxt [Data.imp_intr]; 198 199fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd; 200fun dup_subst ctxt = rev_dup_elim ctxt ssubst 201 202(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *) 203(* premises containing meta-implications or quantifiers *) 204 205(*Old version of the tactic above -- slower but the only way 206 to handle equalities containing Vars.*) 207fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) => 208 let val n = length(Logic.strip_assums_hyp Bi) - 1 209 val (k, (orient, is_free)) = eq_var bnd false true Bi 210 val rl = if is_free then dup_subst ctxt else ssubst 211 val rl = if orient then rl else Data.sym RS rl 212 in 213 DETERM 214 (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), 215 rotate_tac 1 i, 216 REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i), 217 inst_subst_tac ctxt orient rl i, 218 REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i)]) 219 end 220 handle THM _ => no_tac | EQ_VAR => no_tac); 221 222(*Substitutes for Free or Bound variables, 223 discarding equalities on Bound variables 224 and on Free variables if thin=true*) 225fun hyp_subst_tac_thin thin ctxt = 226 REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl], 227 gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false, 228 if thin then thin_free_eq_tac ctxt else K no_tac]; 229 230val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false); 231 232fun hyp_subst_tac ctxt = 233 hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt; 234 235(*Substitutes for Bound variables only -- this is always safe*) 236fun bound_hyp_subst_tac ctxt = 237 REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true 238 ORELSE' vars_gen_hyp_subst_tac ctxt true); 239 240(** Version for Blast_tac. Hyps that are affected by the substitution are 241 moved to the front. Defect: even trivial changes are noticed, such as 242 substitutions in the arguments of a function Var. **) 243 244(*final re-reversal of the changed assumptions*) 245fun reverse_n_tac _ 0 i = all_tac 246 | reverse_n_tac _ 1 i = rotate_tac ~1 i 247 | reverse_n_tac ctxt n i = 248 REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac ctxt [Data.rev_mp] i) THEN 249 REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i); 250 251(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) 252fun all_imp_intr_tac ctxt hyps i = 253 let 254 fun imptac (r, []) st = reverse_n_tac ctxt r i st 255 | imptac (r, hyp::hyps) st = 256 let 257 val (hyp', _) = 258 Thm.term_of (Thm.cprem_of st i) 259 |> Logic.strip_assums_concl 260 |> Data.dest_Trueprop |> Data.dest_imp; 261 val (r', tac) = 262 if Envir.aeconv (hyp, hyp') 263 then (r, imp_intr_tac ctxt i THEN rotate_tac ~1 i) 264 else (*leave affected hyps at end*) (r + 1, imp_intr_tac ctxt i); 265 in 266 (case Seq.pull (tac st) of 267 NONE => Seq.single st 268 | SOME (st', _) => imptac (r', hyps) st') 269 end 270 in imptac (0, rev hyps) end; 271 272 273fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi, i) => 274 let 275 val (k, (symopt, _)) = eq_var false false false Bi 276 val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) 277 (*omit selected equality, returning other hyps*) 278 val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) 279 val n = length hyps 280 in 281 if trace then tracing "Substituting an equality" else (); 282 DETERM 283 (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), 284 rotate_tac 1 i, 285 REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i), 286 inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i, 287 all_imp_intr_tac ctxt hyps i]) 288 end 289 handle THM _ => no_tac | EQ_VAR => no_tac); 290 291(*apply an equality or definition ONCE; 292 fails unless the substitution has an effect*) 293fun stac ctxt th = 294 let val th' = th RS Data.rev_eq_reflection handle THM _ => th 295 in CHANGED_GOAL (resolve_tac ctxt [th' RS ssubst]) end; 296 297 298(* method setup *) 299 300val _ = 301 Theory.setup 302 (Method.setup @{binding hypsubst} 303 (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt))) 304 "substitution using an assumption (improper)" #> 305 Method.setup @{binding hypsubst_thin} 306 (Scan.succeed (fn ctxt => SIMPLE_METHOD' 307 (CHANGED_PROP o hyp_subst_tac_thin true ctxt))) 308 "substitution using an assumption, eliminating assumptions" #> 309 Method.setup @{binding simplesubst} 310 (Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th))) 311 "simple substitution"); 312 313end; 314