single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
authorkrauss
Mon Jul 14 17:47:18 2008 +0200 (2008-07-14)
changeset 2757267cd6ed76446
parent 27571 69f3981c8ed4
child 27573 10ba0d7d94e0
single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp
src/FOL/hypsubstdata.ML
src/HOL/HOL.thy
src/Provers/hypsubst.ML
     1.1 --- a/src/FOL/hypsubstdata.ML	Mon Jul 14 17:02:55 2008 +0200
     1.2 +++ b/src/FOL/hypsubstdata.ML	Mon Jul 14 17:47:18 2008 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4    val subst = thm "subst"
     1.5    val sym = thm "sym"
     1.6    val thin_refl = thm "thin_refl"
     1.7 +  val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
     1.8 +                     by (unfold prop_def) (drule eq_reflection, unfold)}
     1.9  end;
    1.10  
    1.11  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     2.1 --- a/src/HOL/HOL.thy	Mon Jul 14 17:02:55 2008 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Jul 14 17:47:18 2008 +0200
     2.3 @@ -918,6 +918,8 @@
     2.4    val subst = @{thm subst}
     2.5    val sym = @{thm sym}
     2.6    val thin_refl = @{thm thin_refl};
     2.7 +  val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)"
     2.8 +                     by (unfold prop_def) (drule eq_reflection, unfold)}
     2.9  end);
    2.10  open Hypsubst;
    2.11  
     3.1 --- a/src/Provers/hypsubst.ML	Mon Jul 14 17:02:55 2008 +0200
     3.2 +++ b/src/Provers/hypsubst.ML	Mon Jul 14 17:47:18 2008 +0200
     3.3 @@ -43,10 +43,13 @@
     3.4    val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
     3.5    val sym              : thm               (* a=b ==> b=a *)
     3.6    val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
     3.7 +  val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
     3.8  end;
     3.9  
    3.10  signature HYPSUBST =
    3.11  sig
    3.12 +  val single_hyp_subst_tac   : int -> int -> tactic
    3.13 +  val single_hyp_meta_subst_tac : int -> int -> tactic
    3.14    val bound_hyp_subst_tac    : int -> tactic
    3.15    val hyp_subst_tac          : int -> tactic
    3.16    val blast_hyp_subst_tac    : bool -> int -> tactic
    3.17 @@ -59,6 +62,27 @@
    3.18  
    3.19  exception EQ_VAR;
    3.20  
    3.21 +val meta_subst = @{lemma "PROP P t ==> PROP prop (x == t ==> PROP P x)"
    3.22 +  by (unfold prop_def)}
    3.23 +
    3.24 +(** Simple version: Just subtitute one hypothesis, specified by index k **)
    3.25 +fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
    3.26 + let 
    3.27 +   val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
    3.28 +             |> cterm_of (theory_of_cterm csubg)
    3.29 +
    3.30 +   val rule =
    3.31 +       Thm.lift_rule pat subst_rule (* lift just over parameters *)
    3.32 +       |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
    3.33 + in
    3.34 +   rotate_tac k i
    3.35 +   THEN Thm.compose_no_flatten false (rule, 1) i
    3.36 +   THEN rotate_tac (~k) i
    3.37 + end)
    3.38 +
    3.39 +val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
    3.40 +val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
    3.41 +
    3.42  fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    3.43  
    3.44  (*Simplifier turns Bound variables to special Free variables: