src/Tools/intuitionistic.ML
changeset 33369 470a7b233ee5
parent 33038 8f9594c31de4
child 33554 4601372337e4
equal deleted inserted replaced
33368:b1cf34f1855c 33369:470a7b233ee5
    23     (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    23     (Tactic.ematch_tac [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 = tac THEN_ALL_NEW remdups_tac;
    27 
    27 
    28 val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.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   ContextRules.Swrap ctxt
    31   Context_Rules.Swrap ctxt
    32    (eq_assume_tac ORELSE'
    32    (eq_assume_tac ORELSE'
    33     bires_tac true (ContextRules.netpair_bang ctxt));
    33     bires_tac true (Context_Rules.netpair_bang ctxt));
    34 
    34 
    35 fun unsafe_step_tac ctxt =
    35 fun unsafe_step_tac ctxt =
    36   ContextRules.wrap ctxt
    36   Context_Rules.wrap ctxt
    37    (assume_tac APPEND'
    37    (assume_tac APPEND'
    38     bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
    38     bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
    39     bires_tac false (ContextRules.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 
    73 fun modifier name kind kind' att =
    73 fun modifier name kind kind' att =
    74   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    74   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    75     >> (pair (I: Proof.context -> Proof.context) o att);
    75     >> (pair (I: Proof.context -> Proof.context) o att);
    76 
    76 
    77 val modifiers =
    77 val modifiers =
    78  [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
    78  [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
    79   modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
    79   modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
    80   modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
    80   modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
    81   modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
    81   modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
    82   modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
    82   modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
    83   modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    83   modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
    84   Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    84   Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
    85 
    85 
    86 in
    86 in
    87 
    87 
    88 fun method_setup name =
    88 fun method_setup name =
    89   Method.setup name
    89   Method.setup name