src/Tools/intuitionistic.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 33554 4601372337e4
child 36960 01594f816e3a
permissions -rw-r--r--
modernized structure Object_Logic;
     1 (*  Title:      Tools/intuitionistic.ML
     2     Author:     Stefan Berghofer, TU Muenchen
     3 
     4 Simple intuitionistic proof search.
     5 *)
     6 
     7 signature INTUITIONISTIC =
     8 sig
     9   val prover_tac: Proof.context -> int option -> int -> tactic
    10   val method_setup: binding -> theory -> theory
    11 end;
    12 
    13 structure Intuitionistic: INTUITIONISTIC =
    14 struct
    15 
    16 (* main tactic *)
    17 
    18 local
    19 
    20 val remdups_tac = SUBGOAL (fn (g, i) =>
    21   let val prems = Logic.strip_assums_hyp g in
    22     REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    23     (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    24   end);
    25 
    26 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    27 
    28 val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
    29 
    30 fun safe_step_tac ctxt =
    31   Context_Rules.Swrap ctxt
    32    (eq_assume_tac ORELSE'
    33     bires_tac true (Context_Rules.netpair_bang ctxt));
    34 
    35 fun unsafe_step_tac ctxt =
    36   Context_Rules.wrap ctxt
    37    (assume_tac APPEND'
    38     bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
    39     bires_tac false (Context_Rules.netpair ctxt));
    40 
    41 fun step_tac ctxt i =
    42   REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    43   REMDUPS (unsafe_step_tac ctxt) i;
    44 
    45 fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
    46   let
    47     val ps = Logic.strip_assums_hyp g;
    48     val c = Logic.strip_assums_concl g;
    49   in
    50     if member (fn ((ps1, c1), (ps2, c2)) =>
    51         c1 aconv c2 andalso
    52         length ps1 = length ps2 andalso
    53         eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    54     else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    55   end);
    56 
    57 in
    58 
    59 fun prover_tac ctxt opt_lim =
    60   SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    61 
    62 end;
    63 
    64 
    65 (* method setup *)
    66 
    67 local
    68 
    69 val introN = "intro";
    70 val elimN = "elim";
    71 val destN = "dest";
    72 
    73 fun modifier name kind kind' att =
    74   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    75     >> (pair (I: Proof.context -> Proof.context) o att);
    76 
    77 val modifiers =
    78  [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
    79   modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
    80   modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
    81   modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
    82   modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
    83   modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
    84   Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
    85 
    86 in
    87 
    88 fun method_setup name =
    89   Method.setup name
    90     (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
    91       (fn opt_lim => fn ctxt =>
    92         SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
    93     "intuitionistic proof search";
    94 
    95 end;
    96 
    97 end;
    98