--- a/src/Provers/hypsubst.ML Wed Sep 29 10:05:44 2010 +0200
+++ b/src/Provers/hypsubst.ML Wed Sep 29 11:02:24 2010 +0200
@@ -42,13 +42,10 @@
val subst : thm (* [| a=b; P(a) |] ==> P(b) *)
val sym : thm (* a=b ==> b=a *)
val thin_refl : thm (* [|x=x; PROP W|] ==> PROP W *)
- val prop_subst : thm (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
end;
signature HYPSUBST =
sig
- val single_hyp_subst_tac : int -> int -> tactic
- val single_hyp_meta_subst_tac : int -> int -> tactic
val bound_hyp_subst_tac : int -> tactic
val hyp_subst_tac : int -> tactic
val blast_hyp_subst_tac : bool -> int -> tactic
@@ -61,27 +58,6 @@
exception EQ_VAR;
-val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
- by (unfold prop_def)}
-
-(** Simple version: Just subtitute one hypothesis, specified by index k **)
-fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
- let
- val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
- |> cterm_of (theory_of_cterm csubg)
-
- val rule =
- Thm.lift_rule pat subst_rule (* lift just over parameters *)
- |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
- in
- rotate_tac k i
- THEN Thm.compose_no_flatten false (rule, 1) i
- THEN rotate_tac (~k) i
- end)
-
-val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
-val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
-
fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
(*Simplifier turns Bound variables to special Free variables: