author | blanchet |
Mon, 16 Dec 2013 09:48:26 +0100 | |
changeset 54764 | 1c9ef5c834e8 |
parent 54761 | 0ef52f40d419 |
child 54765 | b05b0ea06306 |
permissions | -rw-r--r-- |
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50263
diff
changeset
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof.ML |
50263 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
Author: Steffen Juilf Smolka, TU Muenchen |
|
4 |
||
5 |
Basic data structures for representing and basic methods |
|
6 |
for dealing with Isar proof texts. |
|
7 |
*) |
|
8 |
||
50268 | 9 |
signature SLEDGEHAMMER_PROOF = |
50259 | 10 |
sig |
51239 | 11 |
type label = string * int |
52454 | 12 |
type facts = label list * string list (* local & global facts *) |
50268 | 13 |
|
51178 | 14 |
datatype isar_qualifier = Show | Then |
50268 | 15 |
|
52454 | 16 |
datatype isar_proof = |
54700 | 17 |
Proof of (string * typ) list * (label * term) list * isar_step list |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
18 |
and isar_step = |
50268 | 19 |
Let of term * term | |
54700 | 20 |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * |
21 |
(facts * proof_method) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
22 |
and proof_method = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
23 |
MetisM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
24 |
SimpM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
25 |
AutoM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
26 |
FastforceM | |
52629 | 27 |
ForceM | |
28 |
ArithM | |
|
54764 | 29 |
BlastM | |
30 |
MesonM |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
31 |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
32 |
val no_label : label |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
33 |
val no_facts : facts |
50268 | 34 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
35 |
val label_ord : label * label -> order |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
36 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
37 |
val dummy_isar_step : isar_step |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
38 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
39 |
val string_of_label : label -> string |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
40 |
|
54700 | 41 |
val fix_of_proof : isar_proof -> (string * typ) list |
42 |
val assms_of_proof : isar_proof -> (label * term) list |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
43 |
val steps_of_proof : isar_proof -> isar_step list |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
44 |
|
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
45 |
val label_of_step : isar_step -> label option |
52454 | 46 |
val subproofs_of_step : isar_step -> isar_proof list option |
54700 | 47 |
val byline_of_step : isar_step -> (facts * proof_method) option |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
48 |
val proof_method_of_step : isar_step -> proof_method option |
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54700
diff
changeset
|
49 |
val use_metis_new_skolem : isar_step -> bool |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
50 |
|
52454 | 51 |
val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a |
52 |
val fold_isar_steps : |
|
53 |
(isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a |
|
54 |
||
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
55 |
val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
56 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
57 |
val add_proof_steps : isar_step list -> int -> int |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
58 |
|
54534 | 59 |
(** canonical proof labels: 1, 2, 3, ... in postorder **) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
60 |
val canonical_label_ord : (label * label) -> order |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
61 |
val relabel_proof_canonically : isar_proof -> isar_proof |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
62 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
63 |
structure Canonical_Lbl_Tab : TABLE |
54504 | 64 |
end; |
50259 | 65 |
|
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50269
diff
changeset
|
66 |
structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = |
50259 | 67 |
struct |
68 |
||
69 |
type label = string * int |
|
54534 | 70 |
type facts = label list * string list (* local and global facts *) |
50259 | 71 |
|
51178 | 72 |
datatype isar_qualifier = Show | Then |
50259 | 73 |
|
52454 | 74 |
datatype isar_proof = |
54700 | 75 |
Proof of (string * typ) list * (label * term) list * isar_step list |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
76 |
and isar_step = |
50259 | 77 |
Let of term * term | |
54700 | 78 |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * |
79 |
(facts * proof_method) |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
80 |
and proof_method = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
81 |
MetisM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
82 |
SimpM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
83 |
AutoM | |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
84 |
FastforceM | |
52629 | 85 |
ForceM | |
86 |
ArithM | |
|
54764 | 87 |
BlastM | |
88 |
MesonM |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
89 |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
90 |
val no_label = ("", ~1) |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
91 |
val no_facts = ([],[]) |
50259 | 92 |
|
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
93 |
val label_ord = pairself swap #> prod_ord int_ord fast_string_ord |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
94 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
95 |
val dummy_isar_step = Let (Term.dummy, Term.dummy) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
96 |
|
51998
f732a674db1b
renamed Sledgehammer functions with 'for' in their names to 'of'
blanchet
parents:
51239
diff
changeset
|
97 |
fun string_of_label (s, num) = s ^ string_of_int num |
50259 | 98 |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
99 |
fun fix_of_proof (Proof (fix, _, _)) = fix |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
100 |
fun assms_of_proof (Proof (_, assms, _)) = assms |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
101 |
fun steps_of_proof (Proof (_, _, steps)) = steps |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
102 |
|
52454 | 103 |
fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l |
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
104 |
| label_of_step _ = NONE |
51178 | 105 |
|
52454 | 106 |
fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs |
107 |
| subproofs_of_step _ = NONE |
|
108 |
||
109 |
fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline |
|
51179
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
110 |
| byline_of_step _ = NONE |
0d5f8812856f
split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations
smolkas
parents:
51178
diff
changeset
|
111 |
|
54700 | 112 |
fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
113 |
| proof_method_of_step _ = NONE |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
114 |
|
54761
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54700
diff
changeset
|
115 |
fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) = |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54700
diff
changeset
|
116 |
meth = MetisM andalso exists (fn (_, T) => length (binder_types T) > 1) xs |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54700
diff
changeset
|
117 |
| use_metis_new_skolem _ = false |
0ef52f40d419
use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning
blanchet
parents:
54700
diff
changeset
|
118 |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
119 |
fun fold_isar_steps f = fold (fold_isar_step f) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
120 |
and fold_isar_step f step s = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
121 |
fold (steps_of_proof #> fold_isar_steps f) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
122 |
(these (subproofs_of_step step)) s |
52454 | 123 |
|> f step |
124 |
||
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
125 |
fun map_isar_steps f proof = |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
126 |
let |
54700 | 127 |
fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
128 |
and do_step (step as Let _) = f step |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
129 |
| do_step (Prove (qs, xs, l, t, subproofs, by)) = |
54700 | 130 |
f (Prove (qs, xs, l, t, map do_proof subproofs, by)) |
52592
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
131 |
in |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
132 |
do_proof proof |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
133 |
end |
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
134 |
|
8a25b17e3d79
optimize isar-proofs by trying different proof methods
smolkas
parents:
52590
diff
changeset
|
135 |
val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
136 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
137 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
138 |
(** canonical proof labels: 1, 2, 3, ... in post traversal order **) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
139 |
|
52557 | 140 |
fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
141 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
142 |
structure Canonical_Lbl_Tab = Table( |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
143 |
type key = label |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
144 |
val ord = canonical_label_ord) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
145 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
146 |
fun relabel_proof_canonically proof = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
147 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
148 |
fun next_label l (next, subst) = |
54534 | 149 |
let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
150 |
|
54700 | 151 |
fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
152 |
handle Option.Option => |
52627 | 153 |
raise Fail "Sledgehammer_Proof: relabel_proof_canonically" |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
154 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
155 |
fun do_assm (l, t) state = |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
156 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
157 |
val (l, state) = next_label l state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
158 |
in ((l, t), state) end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
159 |
|
54700 | 160 |
fun do_proof (Proof (fix, assms, steps)) state = |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
161 |
let |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
162 |
val (assms, state) = fold_map do_assm assms state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
163 |
val (steps, state) = fold_map do_step steps state |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
164 |
in |
54700 | 165 |
(Proof (fix, assms, steps), state) |
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
166 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
167 |
|
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
168 |
and do_step (step as Let _) state = (step, state) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
169 |
| do_step (Prove (qs, fix, l, t, subproofs, by)) state= |
54534 | 170 |
let |
171 |
val by = do_byline by state |
|
172 |
val (subproofs, state) = fold_map do_proof subproofs state |
|
173 |
val (l, state) = next_label l state |
|
174 |
in |
|
175 |
(Prove (qs, fix, l, t, subproofs, by), state) |
|
176 |
end |
|
52556
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
177 |
in |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
178 |
fst (do_proof proof (0, [])) |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
179 |
end |
c8357085217c
completely rewrote SH compress; added two parameters for experimentation/fine grained control
smolkas
parents:
52454
diff
changeset
|
180 |
|
54504 | 181 |
end; |