src/Tools/intuitionistic.ML
changeset 58957 c9e744ea8a38
parent 58048 aa6296d09e0e
child 58963 26bf09b95dda
equal deleted inserted replaced
58956:a816aa3ff391 58957:c9e744ea8a38
    15 
    15 
    16 (* main tactic *)
    16 (* main tactic *)
    17 
    17 
    18 local
    18 local
    19 
    19 
    20 val remdups_tac = SUBGOAL (fn (g, i) =>
    20 fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
    21   let val prems = Logic.strip_assums_hyp g in
    21   let val prems = Logic.strip_assums_hyp g in
    22     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    22     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    23     (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    23     (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    24   end);
    24   end);
    25 
    25 
    26 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    26 fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
    27 
    27 
    28 val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
    28 val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
    29 
    29 
    30 fun safe_step_tac ctxt =
    30 fun safe_step_tac ctxt =
    31   Context_Rules.Swrap ctxt
    31   Context_Rules.Swrap ctxt
    37    (assume_tac APPEND'
    37    (assume_tac APPEND'
    38     bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
    38     bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
    39     bires_tac false (Context_Rules.netpair ctxt));
    39     bires_tac false (Context_Rules.netpair ctxt));
    40 
    40 
    41 fun step_tac ctxt i =
    41 fun step_tac ctxt i =
    42   REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    42   REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
    43   REMDUPS (unsafe_step_tac ctxt) i;
    43   REMDUPS unsafe_step_tac ctxt i;
    44 
    44 
    45 fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
    45 fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
    46   if d > lim then no_tac
    46   if d > lim then no_tac
    47   else
    47   else
    48     let
    48     let