src/FOLP/hypsubst.ML
changeset 3537 79ac9b475621
parent 2728 df3a269b6f34
child 26830 7b7139f961bd
equal deleted inserted replaced
3536:8fb4150e2ad3 3537:79ac9b475621
    65         | eq_var_aux k _ = raise EQ_VAR
    65         | eq_var_aux k _ = raise EQ_VAR
    66   in  eq_var_aux 0  end;
    66   in  eq_var_aux 0  end;
    67 
    67 
    68 (*Select a suitable equality assumption and substitute throughout the subgoal
    68 (*Select a suitable equality assumption and substitute throughout the subgoal
    69   Replaces only Bound variables if bnd is true*)
    69   Replaces only Bound variables if bnd is true*)
    70 fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    70 fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    71       let val (_,_,Bi,_) = dest_state(state,i)
    71       let val n = length(Logic.strip_assums_hyp Bi) - 1
    72           val n = length(Logic.strip_assums_hyp Bi) - 1
       
    73           val (k,symopt) = eq_var bnd Bi
    72           val (k,symopt) = eq_var bnd Bi
    74       in 
    73       in 
    75          EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    74          DETERM
    76                 etac revcut_rl i,
    75            (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    77                 REPEAT_DETERM_N (n-k) (etac rev_mp i),
    76 		   etac revcut_rl i,
    78                 etac (symopt RS subst) i,
    77 		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    79                 REPEAT_DETERM_N n (rtac imp_intr i)]
    78 		   etac (symopt RS subst) i,
       
    79 		   REPEAT_DETERM_N n (rtac imp_intr i)])
    80       end
    80       end
    81       handle THM _ => no_tac | EQ_VAR => no_tac));
    81       handle THM _ => no_tac | EQ_VAR => no_tac);
    82 
    82 
    83 (*Substitutes for Free or Bound variables*)
    83 (*Substitutes for Free or Bound variables*)
    84 val hyp_subst_tac = gen_hyp_subst_tac false;
    84 val hyp_subst_tac = gen_hyp_subst_tac false;
    85 
    85 
    86 (*Substitutes for Bound variables only -- this is always safe*)
    86 (*Substitutes for Bound variables only -- this is always safe*)