59 |
59 |
60 val map_facts_of_byline : (facts -> facts) -> byline -> byline |
60 val map_facts_of_byline : (facts -> facts) -> byline -> byline |
61 |
61 |
62 val add_proof_steps : isar_step list -> int -> int |
62 val add_proof_steps : isar_step list -> int -> int |
63 |
63 |
64 (** canonical proof labels: 1, 2, 3, ... in post traversal order **) |
64 (** canonical proof labels: 1, 2, 3, ... in postorder **) |
65 val canonical_label_ord : (label * label) -> order |
65 val canonical_label_ord : (label * label) -> order |
66 val relabel_proof_canonically : isar_proof -> isar_proof |
66 val relabel_proof_canonically : isar_proof -> isar_proof |
67 |
67 |
68 structure Canonical_Lbl_Tab : TABLE |
68 structure Canonical_Lbl_Tab : TABLE |
69 |
69 |
71 |
71 |
72 structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = |
72 structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = |
73 struct |
73 struct |
74 |
74 |
75 type label = string * int |
75 type label = string * int |
76 type facts = label list * string list (* local & global facts *) |
76 type facts = label list * string list (* local and global facts *) |
77 |
77 |
78 datatype isar_qualifier = Show | Then |
78 datatype isar_qualifier = Show | Then |
79 |
79 |
80 datatype fix = Fix of (string * typ) list |
80 datatype fix = Fix of (string * typ) list |
81 datatype assms = Assume of (label * term) list |
81 datatype assms = Assume of (label * term) list |
158 type key = label |
158 type key = label |
159 val ord = canonical_label_ord) |
159 val ord = canonical_label_ord) |
160 |
160 |
161 fun relabel_proof_canonically proof = |
161 fun relabel_proof_canonically proof = |
162 let |
162 let |
163 val lbl = pair "" |
|
164 |
|
165 fun next_label l (next, subst) = |
163 fun next_label l (next, subst) = |
166 (lbl next, (next + 1, (l, lbl next) :: subst)) |
164 let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end |
167 |
165 |
168 fun do_byline by (_, subst) = |
166 fun do_byline by (_, subst) = |
169 by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the))) |
167 by |> map_facts_of_byline (apfst (map (AList.lookup (op =) subst #> the))) |
170 handle Option.Option => |
168 handle Option.Option => |
171 raise Fail "Sledgehammer_Proof: relabel_proof_canonically" |
169 raise Fail "Sledgehammer_Proof: relabel_proof_canonically" |
183 (Proof (fix, Assume assms, steps), state) |
181 (Proof (fix, Assume assms, steps), state) |
184 end |
182 end |
185 |
183 |
186 and do_step (step as Let _) state = (step, state) |
184 and do_step (step as Let _) state = (step, state) |
187 | do_step (Prove (qs, fix, l, t, subproofs, by)) state= |
185 | do_step (Prove (qs, fix, l, t, subproofs, by)) state= |
188 let |
186 let |
189 val by = do_byline by state |
187 val by = do_byline by state |
190 val (subproofs, state) = fold_map do_proof subproofs state |
188 val (subproofs, state) = fold_map do_proof subproofs state |
191 val (l, state) = next_label l state |
189 val (l, state) = next_label l state |
192 in |
190 in |
193 (Prove (qs, fix, l, t, subproofs, by), state) |
191 (Prove (qs, fix, l, t, subproofs, by), state) |
194 end |
192 end |
195 in |
193 in |
196 fst (do_proof proof (0, [])) |
194 fst (do_proof proof (0, [])) |
197 end |
195 end |
198 |
196 |
199 end; |
197 end; |