src/Sequents/modal.ML
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 69593 3dda49e08b9d
equal deleted inserted replaced
59580:cbc38731d42f 59582:0fbed69ff081
    67 fun fres_unsafe_tac ctxt = fresolve_tac ctxt Modal_Rule.unsafe_rls THEN' aside_tac ctxt;
    67 fun fres_unsafe_tac ctxt = fresolve_tac ctxt Modal_Rule.unsafe_rls THEN' aside_tac ctxt;
    68 fun fres_bound_tac ctxt = fresolve_tac ctxt Modal_Rule.bound_rls;
    68 fun fres_bound_tac ctxt = fresolve_tac ctxt Modal_Rule.bound_rls;
    69 
    69 
    70 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
    70 fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
    71                                     else tf(i) THEN tac(i-1)
    71                                     else tf(i) THEN tac(i-1)
    72                     in fn st => tac (nprems_of st) st end;
    72                     in fn st => tac (Thm.nprems_of st) st end;
    73 
    73 
    74 (* Depth first search bounded by d *)
    74 (* Depth first search bounded by d *)
    75 fun solven_tac ctxt d n st = st |>
    75 fun solven_tac ctxt d n st = st |>
    76  (if d < 0 then no_tac
    76  (if d < 0 then no_tac
    77   else if nprems_of st = 0 then all_tac
    77   else if Thm.nprems_of st = 0 then all_tac
    78   else (DETERM(fres_safe_tac ctxt n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE
    78   else (DETERM(fres_safe_tac ctxt n) THEN UPTOGOAL n (solven_tac ctxt d)) ORELSE
    79            ((fres_unsafe_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt d)) APPEND
    79            ((fres_unsafe_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt d)) APPEND
    80              (fres_bound_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt (d - 1)))));
    80              (fres_bound_tac ctxt n  THEN UPTOGOAL n (solven_tac ctxt (d - 1)))));
    81 
    81 
    82 fun solve_tac ctxt d =
    82 fun solve_tac ctxt d =