src/Tools/intuitionistic.ML
changeset 30165 6ee87f67d9cd
child 30510 4120fc59dd85
equal deleted inserted replaced
30164:9321f7b70450 30165:6ee87f67d9cd
       
     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: bstring -> 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 ContextRules.orderlist;
       
    29 
       
    30 fun safe_step_tac ctxt =
       
    31   ContextRules.Swrap ctxt
       
    32    (eq_assume_tac ORELSE'
       
    33     bires_tac true (ContextRules.netpair_bang ctxt));
       
    34 
       
    35 fun unsafe_step_tac ctxt =
       
    36   ContextRules.wrap ctxt
       
    37    (assume_tac APPEND'
       
    38     bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
       
    39     bires_tac false (ContextRules.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         gen_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 val ruleN = "rule";
       
    73 
       
    74 fun modifier name kind kind' att =
       
    75   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
       
    76     >> (pair (I: Proof.context -> Proof.context) o att);
       
    77 
       
    78 val modifiers =
       
    79  [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
       
    80   modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
       
    81   modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
       
    82   modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
       
    83   modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
       
    84   modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
       
    85   Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
       
    86 
       
    87 val method =
       
    88   Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
       
    89     (fn n => fn prems => fn ctxt => Method.METHOD (fn facts =>
       
    90       HEADGOAL (Method.insert_tac (prems @ facts) THEN'
       
    91       ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
       
    92 
       
    93 in
       
    94 
       
    95 fun method_setup name = Method.add_method (name, method, "intuitionistic proof search");
       
    96 
       
    97 end;
       
    98 
       
    99 end;
       
   100