author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 52732  b4da1f2ec73f 
child 54742  7a86358a3c0b 
permissions  rwrr 
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  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  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  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  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  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  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  38 
bires_tac false (Context_Rules.netpair_bang ctxt) APPEND' 
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  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 = 
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35625
diff
changeset

74 
Args.$$$ name  (kind >> K NONE  kind'  Parse.nat  Args.colon >> SOME) 
30165
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  78 
[modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang, 
79 
modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest, 

80 
modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang, 

81 
modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim, 

82 
modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang, 

83 
modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro, 

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  88 
fun method_setup name = 
89 
Method.setup name 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
35625
diff
changeset

90 
(Scan.lift (Scan.option Parse.nat)  Method.sections modifiers >> 
33554  91 
(fn opt_lim => fn ctxt => 
35625  92 
SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim))) 
31299  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 