DEL_TAC

ASM 系のタクティックの負担軽減の為，不要な仮定を消去する目的で作りました．

for HOL Light

let DEL_TAC n = ASSUM_LIST (fun al-> UNDISCH_THEN ( concl ((el((length al)-1-n)al)) ) (K ALL_TAC) );;

for HOL4

fun DEL_TAC n = ASSUM_LIST (fn al => UNDISCH_THEN ( concl ((el((length al)-n)al)) ) (K ALL_TAC) );

例えば

> val it =
    
    0 <= (b − a) * (b pow n − a pow n) * s * t
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- - e( METIS_TAC [POW_LE, REAL_SUB_LE, REAL_LE_MUL, REAL_LE_TOTAL,  REAL_NEG_MUL2, REAL_NEG_SUB]  );
OK..
metis: r[+0+16]+0+0+0+0+0+0+0+2+0+0+0+0+0+0+2+0+1+0+0+5+1+1+7+2+0+2+1+1+1+0+0+1+2+1+1#

だったものが

> val it =
    
    0 <= (b − a) * (b pow n − a pow n) * s * t
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  s + t = 1
      3.  0 <= a
      4.  0 <= b
      5.  (s * a + t * b) pow n <= s * a pow n + t * b pow n
     : proof
- e( MAP_EVERY DEL_TAC [5, 2] );
OK..
1 subgoal:
> val it =
    
    0 <= (b − a) * (b pow n − a pow n) * s * t
    ------------------------------------
      0.  0 <= s
      1.  0 <= t
      2.  0 <= a
      3.  0 <= b
     : proof
- e( METIS_TAC [POW_LE, REAL_SUB_LE, REAL_LE_MUL, REAL_LE_TOTAL,  REAL_NEG_MUL2, REAL_NEG_SUB]  );
OK..
metis: r[+0+14]+0+0+0+0+0+0+0+2+0+0+0+0+2+0+1+0+0+5+1+1+7+2+2+1+2+1+1+0+2+1+1+1#

になります．リストで番号を指定するときは値の大きい順に．