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