src/Provers/hypsubst.ML
changeset 27572 67cd6ed76446
parent 26992 4508f20818af
child 27734 dcec1c564f05
equal deleted inserted replaced
27571:69f3981c8ed4 27572:67cd6ed76446
    41   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    41   val imp_intr         : thm               (* (P ==> Q) ==> P-->Q *)
    42   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    42   val rev_mp           : thm               (* [| P;  P-->Q |] ==> Q *)
    43   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    43   val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
    44   val sym              : thm               (* a=b ==> b=a *)
    44   val sym              : thm               (* a=b ==> b=a *)
    45   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
    45   val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
       
    46   val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
    46 end;
    47 end;
    47 
    48 
    48 signature HYPSUBST =
    49 signature HYPSUBST =
    49 sig
    50 sig
       
    51   val single_hyp_subst_tac   : int -> int -> tactic
       
    52   val single_hyp_meta_subst_tac : int -> int -> tactic
    50   val bound_hyp_subst_tac    : int -> tactic
    53   val bound_hyp_subst_tac    : int -> tactic
    51   val hyp_subst_tac          : int -> tactic
    54   val hyp_subst_tac          : int -> tactic
    52   val blast_hyp_subst_tac    : bool -> int -> tactic
    55   val blast_hyp_subst_tac    : bool -> int -> tactic
    53   val stac                   : thm -> int -> tactic
    56   val stac                   : thm -> int -> tactic
    54   val hypsubst_setup         : theory -> theory
    57   val hypsubst_setup         : theory -> theory
    56 
    59 
    57 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    60 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    58 struct
    61 struct
    59 
    62 
    60 exception EQ_VAR;
    63 exception EQ_VAR;
       
    64 
       
    65 val meta_subst = @{lemma "PROP P t ==> PROP prop (x == t ==> PROP P x)"
       
    66   by (unfold prop_def)}
       
    67 
       
    68 (** Simple version: Just subtitute one hypothesis, specified by index k **)
       
    69 fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
       
    70  let 
       
    71    val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
       
    72              |> cterm_of (theory_of_cterm csubg)
       
    73 
       
    74    val rule =
       
    75        Thm.lift_rule pat subst_rule (* lift just over parameters *)
       
    76        |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
       
    77  in
       
    78    rotate_tac k i
       
    79    THEN Thm.compose_no_flatten false (rule, 1) i
       
    80    THEN rotate_tac (~k) i
       
    81  end)
       
    82 
       
    83 val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
       
    84 val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
    61 
    85 
    62 fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    86 fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    63 
    87 
    64 (*Simplifier turns Bound variables to special Free variables:
    88 (*Simplifier turns Bound variables to special Free variables:
    65   change it back (any Bound variable will do)*)
    89   change it back (any Bound variable will do)*)