src/Tools/intuitionistic.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 58048 aa6296d09e0e
child 58957 c9e744ea8a38
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
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))
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 36960
diff changeset
    23
    (ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
30165
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
55627
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    45
fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    46
  if d > lim then no_tac
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    47
  else
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    48
    let
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    49
      val ps = Logic.strip_assums_hyp g;
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    50
      val c = Logic.strip_assums_concl g;
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    51
    in
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    52
      if member (fn ((ps1, c1), (ps2, c2)) =>
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    53
          c1 aconv c2 andalso
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    54
          length ps1 = length ps2 andalso
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    55
          eq_set (op aconv) (ps1, ps2)) gs (ps, c)
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    56
      then no_tac
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    57
      else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
95c8ef02f04b tuned whitespace;
wenzelm
parents: 54742
diff changeset
    58
    end);
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    59
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    60
in
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
fun prover_tac ctxt opt_lim =
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    63
  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
    64
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    65
end;
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
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    68
(* method setup *)
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    69
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    70
local
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    71
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    72
val introN = "intro";
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    73
val elimN = "elim";
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    74
val destN = "dest";
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    75
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    76
fun modifier name kind kind' att pos =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 35625
diff changeset
    77
  Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    78
    >> (fn arg => Method.modifier (att arg) pos);
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    79
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    80
val modifiers =
58048
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    81
 [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here},
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    82
  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here},
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    83
  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here},
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    84
  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here},
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    85
  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here},
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    86
  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here},
aa6296d09e0e more explicit Method.modifier with reported position;
wenzelm
parents: 55627
diff changeset
    87
  Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})];
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    88
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    89
in
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    90
31299
0c5baf034d0e modernized method setup;
wenzelm
parents: 30510
diff changeset
    91
fun method_setup name =
0c5baf034d0e modernized method setup;
wenzelm
parents: 30510
diff changeset
    92
  Method.setup name
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 35625
diff changeset
    93
    (Scan.lift (Scan.option Parse.nat) --| Method.sections modifiers >>
33554
4601372337e4 eliminated some unused/obsolete Args.bang_facts;
wenzelm
parents: 33369
diff changeset
    94
      (fn opt_lim => fn ctxt =>
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    95
        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac ctxt THEN' prover_tac ctxt opt_lim)))
31299
0c5baf034d0e modernized method setup;
wenzelm
parents: 30510
diff changeset
    96
    "intuitionistic proof search";
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    97
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    98
end;
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    99
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
   100
end;
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
   101