|
1 (* Title: Tools/intuitionistic.ML |
|
2 Author: Stefan Berghofer, TU Muenchen |
|
3 |
|
4 Simple intuitionistic proof search. |
|
5 *) |
|
6 |
|
7 signature INTUITIONISTIC = |
|
8 sig |
|
9 val prover_tac: Proof.context -> int option -> int -> tactic |
|
10 val method_setup: bstring -> theory -> theory |
|
11 end; |
|
12 |
|
13 structure Intuitionistic: INTUITIONISTIC = |
|
14 struct |
|
15 |
|
16 (* main tactic *) |
|
17 |
|
18 local |
|
19 |
|
20 val remdups_tac = SUBGOAL (fn (g, i) => |
|
21 let val prems = Logic.strip_assums_hyp g in |
|
22 REPEAT_DETERM_N (length prems - length (distinct op aconv prems)) |
|
23 (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i) |
|
24 end); |
|
25 |
|
26 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac; |
|
27 |
|
28 val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist; |
|
29 |
|
30 fun safe_step_tac ctxt = |
|
31 ContextRules.Swrap ctxt |
|
32 (eq_assume_tac ORELSE' |
|
33 bires_tac true (ContextRules.netpair_bang ctxt)); |
|
34 |
|
35 fun unsafe_step_tac ctxt = |
|
36 ContextRules.wrap ctxt |
|
37 (assume_tac APPEND' |
|
38 bires_tac false (ContextRules.netpair_bang ctxt) APPEND' |
|
39 bires_tac false (ContextRules.netpair ctxt)); |
|
40 |
|
41 fun step_tac ctxt i = |
|
42 REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE |
|
43 REMDUPS (unsafe_step_tac ctxt) i; |
|
44 |
|
45 fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else |
|
46 let |
|
47 val ps = Logic.strip_assums_hyp g; |
|
48 val c = Logic.strip_assums_concl g; |
|
49 in |
|
50 if member (fn ((ps1, c1), (ps2, c2)) => |
|
51 c1 aconv c2 andalso |
|
52 length ps1 = length ps2 andalso |
|
53 gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac |
|
54 else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i |
|
55 end); |
|
56 |
|
57 in |
|
58 |
|
59 fun prover_tac ctxt opt_lim = |
|
60 SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1); |
|
61 |
|
62 end; |
|
63 |
|
64 |
|
65 (* method setup *) |
|
66 |
|
67 local |
|
68 |
|
69 val introN = "intro"; |
|
70 val elimN = "elim"; |
|
71 val destN = "dest"; |
|
72 val ruleN = "rule"; |
|
73 |
|
74 fun modifier name kind kind' att = |
|
75 Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME) |
|
76 >> (pair (I: Proof.context -> Proof.context) o att); |
|
77 |
|
78 val modifiers = |
|
79 [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang, |
|
80 modifier destN Args.colon (Scan.succeed ()) ContextRules.dest, |
|
81 modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang, |
|
82 modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim, |
|
83 modifier introN Args.bang_colon Args.bang ContextRules.intro_bang, |
|
84 modifier introN Args.colon (Scan.succeed ()) ContextRules.intro, |
|
85 Args.del -- Args.colon >> K (I, ContextRules.rule_del)]; |
|
86 |
|
87 val method = |
|
88 Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat)) |
|
89 (fn n => fn prems => fn ctxt => Method.METHOD (fn facts => |
|
90 HEADGOAL (Method.insert_tac (prems @ facts) THEN' |
|
91 ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n))); |
|
92 |
|
93 in |
|
94 |
|
95 fun method_setup name = Method.add_method (name, method, "intuitionistic proof search"); |
|
96 |
|
97 end; |
|
98 |
|
99 end; |
|
100 |