src/Tools/intuitionistic.ML
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (18 months ago)
changeset 67835 c8e4ee2b5482
parent 64556 851ae0e7b09c
permissions -rw-r--r--
tuned imports;
     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 fun remdups_tac ctxt = 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     (ematch_tac ctxt [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    24   end);
    25 
    26 fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
    27 
    28 fun bires_tac ctxt = Tactic.biresolution_from_nets_tac ctxt Context_Rules.orderlist;
    29 
    30 fun safe_step_tac ctxt =
    31   Context_Rules.Swrap ctxt
    32    (eq_assume_tac ORELSE'
    33     bires_tac ctxt true (Context_Rules.netpair_bang ctxt));
    34 
    35 fun unsafe_step_tac ctxt =
    36   Context_Rules.wrap ctxt
    37    (assume_tac ctxt APPEND'
    38     bires_tac ctxt false (Context_Rules.netpair_bang ctxt) APPEND'
    39     bires_tac ctxt 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) =>
    46   if d > lim then no_tac
    47   else
    48     let
    49       val ps = Logic.strip_assums_hyp g;
    50       val c = Logic.strip_assums_concl g;
    51     in
    52       if member (fn ((ps1, c1), (ps2, c2)) =>
    53           c1 aconv c2 andalso
    54           length ps1 = length ps2 andalso
    55           eq_set (op aconv) (ps1, ps2)) gs (ps, c)
    56       then no_tac
    57       else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    58     end);
    59 
    60 in
    61 
    62 fun prover_tac ctxt opt_lim =
    63   SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    64 
    65 end;
    66 
    67 
    68 (* method setup *)
    69 
    70 local
    71 
    72 val introN = "intro";
    73 val elimN = "elim";
    74 val destN = "dest";
    75 
    76 fun modifier name kind kind' att pos =
    77   Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
    78     >> (fn arg => Method.modifier (att arg) pos);
    79 
    80 val modifiers =
    81  [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang \<^here>,
    82   modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest \<^here>,
    83   modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang \<^here>,
    84   modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim \<^here>,
    85   modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang \<^here>,
    86   modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro \<^here>,
    87   Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del \<^here>)];
    88 
    89 in
    90 
    91 fun method_setup name =
    92   Method.setup name
    93     (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
    94       (fn opt_lim => fn ctxt =>
    95         SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
    96     "intuitionistic proof search";
    97 
    98 end;
    99 
   100 end;
   101