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