7 *) |
7 *) |
8 |
8 |
9 signature SLEDGEHAMMER_PROOF = |
9 signature SLEDGEHAMMER_PROOF = |
10 sig |
10 sig |
11 type label = string * int |
11 type label = string * int |
12 type facts = label list * string list |
12 type facts = label list * string list (* local & global *) |
13 |
13 |
14 datatype isar_qualifier = Show | Then |
14 datatype isar_qualifier = Show | Then |
15 |
15 |
16 datatype fix = Fix of (string * typ) list |
16 datatype fix = Fix of (string * typ) list |
17 datatype assms = Assume of (label * term) list |
17 datatype assms = Assume of (label * term) list |
66 fun string_of_label (s, num) = s ^ string_of_int num |
66 fun string_of_label (s, num) = s ^ string_of_int num |
67 |
67 |
68 fun fix_of_proof (Proof (fix, _, _)) = fix |
68 fun fix_of_proof (Proof (fix, _, _)) = fix |
69 fun assms_of_proof (Proof (_, assms, _)) = assms |
69 fun assms_of_proof (Proof (_, assms, _)) = assms |
70 fun steps_of_proof (Proof (_, _, steps)) = steps |
70 fun steps_of_proof (Proof (_, _, steps)) = steps |
71 (*fun map_steps_of_proof f (Proof (fix, assms, steps)) = |
|
72 Proof(fix, assms, f steps)*) |
|
73 |
71 |
74 fun label_of_step (Obtain (_, _, l, _, _)) = SOME l |
72 fun label_of_step (Obtain (_, _, l, _, _)) = SOME l |
75 | label_of_step (Prove (_, l, _, _)) = SOME l |
73 | label_of_step (Prove (_, l, _, _)) = SOME l |
76 | label_of_step _ = NONE |
74 | label_of_step _ = NONE |
77 |
75 |