26 |
26 |
27 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = |
27 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = |
28 struct |
28 struct |
29 |
29 |
30 local open Data in |
30 local open Data in |
31 |
|
32 fun REPEATN 0 tac = all_tac |
|
33 | REPEATN n tac = Tactic(fn state => |
|
34 tapply(tac THEN REPEATN (n-1) tac, state)); |
|
35 |
31 |
36 exception EQ_VAR; |
32 exception EQ_VAR; |
37 |
33 |
38 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
34 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
39 |
35 |
71 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
67 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => |
72 let val (_,_,Bi,_) = dest_state(state,i) |
68 let val (_,_,Bi,_) = dest_state(state,i) |
73 val n = length(Logic.strip_assums_hyp Bi) - 1 |
69 val n = length(Logic.strip_assums_hyp Bi) - 1 |
74 val (k,symopt) = eq_var bnd Bi |
70 val (k,symopt) = eq_var bnd Bi |
75 in |
71 in |
76 EVERY [REPEATN k (etac rev_mp i), |
72 EVERY [REPEAT_DETERM_N k (etac rev_mp i), |
77 etac revcut_rl i, |
73 etac revcut_rl i, |
78 REPEATN (n-k) (etac rev_mp i), |
74 REPEAT_DETERM_N (n-k) (etac rev_mp i), |
79 etac (symopt RS subst) i, |
75 etac (symopt RS subst) i, |
80 REPEATN n (rtac imp_intr i)] |
76 REPEAT_DETERM_N n (rtac imp_intr i)] |
81 end |
77 end |
82 handle THM _ => no_tac | EQ_VAR => no_tac)); |
78 handle THM _ => no_tac | EQ_VAR => no_tac)); |
83 |
79 |
84 (*Substitutes for Free or Bound variables*) |
80 (*Substitutes for Free or Bound variables*) |
85 val hyp_subst_tac = gen_hyp_subst_tac false; |
81 val hyp_subst_tac = gen_hyp_subst_tac false; |