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>\<open>Pure.all\<close>,_) $ Abs(_,_,t)) hs = eq_var_aux k t hs 116 | eq_var_aux k (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ 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 142(*Select a suitable equality assumption; substitute throughout the subgoal 143 If bnd is true, then it replaces Bound variables only. *) 144fun gen_hyp_subst_tac ctxt bnd = 145 SUBGOAL (fn (Bi, i) => 146 let 147 val (k, (orient, is_free)) = eq_var bnd true true Bi 148 val hyp_subst_ctxt = empty_simpset ctxt |> Simplifier.set_mksimps (K (mk_eqs bnd)) 149 in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ctxt i, 150 if not is_free then eresolve_tac ctxt [thin_rl] i 151 else if orient then eresolve_tac ctxt [Data.rev_mp] i 152 else eresolve_tac ctxt [Data.sym RS Data.rev_mp] i, 153 rotate_tac (~k) i, 154 if is_free then resolve_tac ctxt [Data.imp_intr] i else all_tac] 155 end handle THM _ => no_tac | EQ_VAR => no_tac) 156 157val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst); 158 159fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) => 160 case try (Logic.strip_assums_hyp #> hd #> 161 Data.dest_Trueprop #> Data.dest_eq #> apply2 Envir.eta_contract) (Thm.term_of cBi) of 162 SOME (t, t') => 163 let 164 val Bi = Thm.term_of cBi; 165 val ps = Logic.strip_params Bi; 166 val U = Term.fastype_of1 (rev (map snd ps), t); 167 val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi); 168 val rl' = Thm.lift_rule cBi rl; 169 val (ixn, T) = dest_Var (Term.head_of (Data.dest_Trueprop 170 (Logic.strip_assums_concl (Thm.prop_of rl')))); 171 val (v1, v2) = Data.dest_eq (Data.dest_Trueprop 172 (Logic.strip_assums_concl (hd (Thm.prems_of rl')))); 173 val (Ts, V) = split_last (Term.binder_types T); 174 val u = 175 fold_rev Term.abs (ps @ [("x", U)]) 176 (case (if b then t else t') of 177 Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) 178 | t => Term.abstract_over (t, Term.incr_boundvars 1 Q)); 179 val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U)); 180 in 181 compose_tac ctxt (true, Drule.instantiate_normalize (instT, 182 map (apsnd (Thm.cterm_of ctxt)) 183 [((ixn, Ts ---> U --> body_type T), u), 184 ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t), 185 ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl', 186 Thm.nprems_of rl) i 187 end 188 | NONE => no_tac); 189 190fun imp_intr_tac ctxt = resolve_tac ctxt [Data.imp_intr]; 191 192fun rev_dup_elim ctxt th = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd; 193fun dup_subst ctxt = rev_dup_elim ctxt ssubst 194 195(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *) 196(* premises containing meta-implications or quantifiers *) 197 198(*Old version of the tactic above -- slower but the only way 199 to handle equalities containing Vars.*) 200fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) => 201 let val n = length(Logic.strip_assums_hyp Bi) - 1 202 val (k, (orient, is_free)) = eq_var bnd false true Bi 203 val rl = if is_free then dup_subst ctxt else ssubst 204 val rl = if orient then rl else Data.sym RS rl 205 in 206 DETERM 207 (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), 208 rotate_tac 1 i, 209 REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i), 210 inst_subst_tac ctxt orient rl i, 211 REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i)]) 212 end 213 handle THM _ => no_tac | EQ_VAR => no_tac); 214 215(*Substitutes for Free or Bound variables, 216 discarding equalities on Bound variables 217 and on Free variables if thin=true*) 218fun hyp_subst_tac_thin thin ctxt = 219 REPEAT_DETERM1 o FIRST' [ematch_tac ctxt [Data.thin_refl], 220 gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false, 221 if thin then thin_free_eq_tac ctxt else K no_tac]; 222 223val hyp_subst_thin = Attrib.setup_config_bool \<^binding>\<open>hypsubst_thin\<close> (K false); 224 225fun hyp_subst_tac ctxt = 226 hyp_subst_tac_thin (Config.get ctxt hyp_subst_thin) ctxt; 227 228(*Substitutes for Bound variables only -- this is always safe*) 229fun bound_hyp_subst_tac ctxt = 230 REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true 231 ORELSE' vars_gen_hyp_subst_tac ctxt true); 232 233(** Version for Blast_tac. Hyps that are affected by the substitution are 234 moved to the front. Defect: even trivial changes are noticed, such as 235 substitutions in the arguments of a function Var. **) 236 237(*final re-reversal of the changed assumptions*) 238fun reverse_n_tac _ 0 i = all_tac 239 | reverse_n_tac _ 1 i = rotate_tac ~1 i 240 | reverse_n_tac ctxt n i = 241 REPEAT_DETERM_N n (rotate_tac ~1 i THEN eresolve_tac ctxt [Data.rev_mp] i) THEN 242 REPEAT_DETERM_N n (imp_intr_tac ctxt i THEN rotate_tac ~1 i); 243 244(*Use imp_intr, comparing the old hyps with the new ones as they come out.*) 245fun all_imp_intr_tac ctxt hyps i = 246 let 247 fun imptac (r, []) st = reverse_n_tac ctxt r i st 248 | imptac (r, hyp::hyps) st = 249 let 250 val (hyp', _) = 251 Thm.term_of (Thm.cprem_of st i) 252 |> Logic.strip_assums_concl 253 |> Data.dest_Trueprop |> Data.dest_imp; 254 val (r', tac) = 255 if Envir.aeconv (hyp, hyp') 256 then (r, imp_intr_tac ctxt i THEN rotate_tac ~1 i) 257 else (*leave affected hyps at end*) (r + 1, imp_intr_tac ctxt i); 258 in 259 (case Seq.pull (tac st) of 260 NONE => Seq.single st 261 | SOME (st', _) => imptac (r', hyps) st') 262 end 263 in imptac (0, rev hyps) end; 264 265 266fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi, i) => 267 let 268 val (k, (symopt, _)) = eq_var false false false Bi 269 val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi) 270 (*omit selected equality, returning other hyps*) 271 val hyps = List.take(hyps0, k) @ List.drop(hyps0, k+1) 272 val n = length hyps 273 in 274 if trace then tracing "Substituting an equality" else (); 275 DETERM 276 (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [Data.rev_mp] i), 277 rotate_tac 1 i, 278 REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [Data.rev_mp] i), 279 inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i, 280 all_imp_intr_tac ctxt hyps i]) 281 end 282 handle THM _ => no_tac | EQ_VAR => no_tac); 283 284(*apply an equality or definition ONCE; 285 fails unless the substitution has an effect*) 286fun stac ctxt th = 287 let val th' = th RS Data.rev_eq_reflection handle THM _ => th 288 in CHANGED_GOAL (resolve_tac ctxt [th' RS ssubst]) end; 289 290 291(* method setup *) 292 293val _ = 294 Theory.setup 295 (Method.setup \<^binding>\<open>hypsubst\<close> 296 (Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o hyp_subst_tac ctxt))) 297 "substitution using an assumption (improper)" #> 298 Method.setup \<^binding>\<open>hypsubst_thin\<close> 299 (Scan.succeed (fn ctxt => SIMPLE_METHOD' 300 (CHANGED_PROP o hyp_subst_tac_thin true ctxt))) 301 "substitution using an assumption, eliminating assumptions" #> 302 Method.setup \<^binding>\<open>simplesubst\<close> 303 (Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (stac ctxt th))) 304 "simple substitution"); 305 306end; 307