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