src/Provers/hypsubst.ML
changeset 27572 67cd6ed76446
parent 26992 4508f20818af
child 27734 dcec1c564f05
     1.1 --- a/src/Provers/hypsubst.ML	Mon Jul 14 17:02:55 2008 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Mon Jul 14 17:47:18 2008 +0200
     1.3 @@ -43,10 +43,13 @@
     1.4    val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
     1.5    val sym              : thm               (* a=b ==> b=a *)
     1.6    val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
     1.7 +  val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
     1.8  end;
     1.9  
    1.10  signature HYPSUBST =
    1.11  sig
    1.12 +  val single_hyp_subst_tac   : int -> int -> tactic
    1.13 +  val single_hyp_meta_subst_tac : int -> int -> tactic
    1.14    val bound_hyp_subst_tac    : int -> tactic
    1.15    val hyp_subst_tac          : int -> tactic
    1.16    val blast_hyp_subst_tac    : bool -> int -> tactic
    1.17 @@ -59,6 +62,27 @@
    1.18  
    1.19  exception EQ_VAR;
    1.20  
    1.21 +val meta_subst = @{lemma "PROP P t ==> PROP prop (x == t ==> PROP P x)"
    1.22 +  by (unfold prop_def)}
    1.23 +
    1.24 +(** Simple version: Just subtitute one hypothesis, specified by index k **)
    1.25 +fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
    1.26 + let 
    1.27 +   val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
    1.28 +             |> cterm_of (theory_of_cterm csubg)
    1.29 +
    1.30 +   val rule =
    1.31 +       Thm.lift_rule pat subst_rule (* lift just over parameters *)
    1.32 +       |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
    1.33 + in
    1.34 +   rotate_tac k i
    1.35 +   THEN Thm.compose_no_flatten false (rule, 1) i
    1.36 +   THEN rotate_tac (~k) i
    1.37 + end)
    1.38 +
    1.39 +val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
    1.40 +val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
    1.41 +
    1.42  fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    1.43  
    1.44  (*Simplifier turns Bound variables to special Free variables: