# HG changeset patch # User berghofe # Date 1210150788 -7200 # Node ID 7c3757fccf0e4848952b72cfbf6b47d89f6668c3 # Parent 46b90bbc370dd913612659495bd315e220f379aa Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification. diff -r 46b90bbc370d -r 7c3757fccf0e src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Wed May 07 10:59:47 2008 +0200 +++ b/src/Provers/hypsubst.ML Wed May 07 10:59:48 2008 +0200 @@ -64,7 +64,7 @@ (*Simplifier turns Bound variables to special Free variables: change it back (any Bound variable will do)*) fun contract t = - (case Pattern.eta_contract_atom t of + (case Envir.eta_contract t of Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T) | t' => t'); @@ -143,8 +143,39 @@ val ssubst = standard (Data.sym RS Data.subst); +fun inst_subst_tac b rl = SUBGOAL (fn (Bi, i) => fn st => + case try (Logic.strip_assums_hyp #> hd #> + Data.dest_Trueprop #> Data.dest_eq #> pairself contract) Bi of + SOME (t, t') => + let + val ps = Logic.strip_params Bi; + val U = fastype_of1 (rev (map snd ps), t); + val Q = Data.dest_Trueprop (Logic.strip_assums_concl Bi); + val rl' = Thm.lift_rule (nth (cprems_of st) (i - 1)) rl; + val Var (ixn, T) = head_of (Data.dest_Trueprop + (Logic.strip_assums_concl (prop_of rl'))); + val (v1, v2) = Data.dest_eq (Data.dest_Trueprop + (Logic.strip_assums_concl (hd (prems_of rl')))); + val (Ts, V) = split_last (binder_types T); + val u = list_abs (ps @ [("x", U)], case (if b then t else t') of + Bound j => subst_bounds (map Bound + ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q) + | t => abstract_over (t, incr_boundvars 1 Q)); + val thy = theory_of_thm rl' + in compose_tac (true, instantiate ([(ctyp_of thy V, ctyp_of thy U)], + map (pairself (cterm_of thy)) + [(Var (ixn, Ts ---> U --> body_type T), u), + (Var (fst (dest_Var (head_of v1)), Ts ---> U), list_abs (ps, t)), + (Var (fst (dest_Var (head_of v2)), Ts ---> U), list_abs (ps, t'))]) rl', + nprems_of rl) i st + end + | NONE => Seq.empty); + val imp_intr_tac = rtac Data.imp_intr; +(* FIXME: "etac Data.rev_mp i" will not behave as expected if goal has *) +(* premises containing meta-implications or quantifiers *) + (*Old version of the tactic above -- slower but the only way to handle equalities containing Vars.*) fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => @@ -155,7 +186,7 @@ (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), rotate_tac 1 i, REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), - etac (if symopt then ssubst else Data.subst) i, + inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)]) end handle THM _ => no_tac | EQ_VAR => no_tac); @@ -211,7 +242,7 @@ (EVERY [REPEAT_DETERM_N k (etac Data.rev_mp i), rotate_tac 1 i, REPEAT_DETERM_N (n-k) (etac Data.rev_mp i), - etac (if symopt then ssubst else Data.subst) i, + inst_subst_tac symopt (if symopt then ssubst else Data.subst) i, all_imp_intr_tac hyps i]) end handle THM _ => no_tac | EQ_VAR => no_tac);