src/Provers/hypsubst.ML
changeset 704 b71b6be59354
parent 680 f9e24455bbd1
child 1011 5c9654e2e3de
equal deleted inserted replaced
703:3a5cd2883581 704:b71b6be59354
    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;