src/Tools/intuitionistic.ML
author wenzelm
Fri, 30 Jul 2021 23:00:50 +0200
changeset 74088 6d8674ffb962
parent 64556 851ae0e7b09c
permissions -rw-r--r--
clarified signature;
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
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58048
diff changeset
    20
fun remdups_tac ctxt = SUBGOAL (fn (g, i) =>
30165
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))
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58048
diff changeset
    23
    (ematch_tac ctxt [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
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58048
diff changeset
    26
fun REMDUPS tac ctxt = tac ctxt THEN_ALL_NEW remdups_tac ctxt;
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
diff changeset
    27
59164
ff40c53d1af9 proper context for "net" tactics;
wenzelm
parents: 58963
diff changeset
    28
fun bires_tac ctxt = Tactic.biresolution_from_nets_tac ctxt 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'
59164
ff40c53d1af9 proper context for "net" tactics;
wenzelm
parents: 58963
diff changeset
    33
    bires_tac ctxt 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
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58957
diff changeset
    37
   (assume_tac ctxt APPEND'
59164
ff40c53d1af9 proper context for "net" tactics;
wenzelm
parents: 58963
diff changeset
    38
    bires_tac ctxt false (Context_Rules.netpair_bang ctxt) APPEND'
ff40c53d1af9 proper context for "net" tactics;
wenzelm
parents: 58963
diff changeset
    39
    bires_tac ctxt 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 =
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58048
diff changeset
    42
  REPEAT_DETERM1 (REMDUPS safe_step_tac ctxt i) ORELSE
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58048
diff changeset
    43
  REMDUPS unsafe_step_tac ctxt i;
30165
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 =
64556
851ae0e7b09c more symbols;
wenzelm
parents: 59164
diff changeset
    81
 [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang \<^here>,
851ae0e7b09c more symbols;
wenzelm
parents: 59164
diff changeset
    82
  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest \<^here>,
851ae0e7b09c more symbols;
wenzelm
parents: 59164
diff changeset
    83
  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang \<^here>,
851ae0e7b09c more symbols;
wenzelm
parents: 59164
diff changeset
    84
  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim \<^here>,
851ae0e7b09c more symbols;
wenzelm
parents: 59164
diff changeset
    85
  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang \<^here>,
851ae0e7b09c more symbols;
wenzelm
parents: 59164
diff changeset
    86
  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro \<^here>,
851ae0e7b09c more symbols;
wenzelm
parents: 59164
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