equal
deleted
inserted
replaced
|
1 signature SLEDGEHAMMER_ISAR = |
|
2 sig |
|
3 val annotate_types : Proof.context -> term -> term |
|
4 end |
|
5 |
|
6 structure Sledgehammer_Isar_Reconstruct (* : SLEDGEHAMMER_Isar *) = |
|
7 struct |
|
8 |
|
9 type label = string * int |
|
10 type facts = label list * string list |
|
11 |
|
12 datatype isar_qualifier = Show | Then | Moreover | Ultimately |
|
13 |
|
14 datatype isar_step = |
|
15 Fix of (string * typ) list | |
|
16 Let of term * term | |
|
17 Assume of label * term | |
|
18 Prove of isar_qualifier list * label * term * byline |
|
19 and byline = |
|
20 By_Metis of facts | |
|
21 Case_Split of isar_step list list * facts |
|
22 |
|
23 fun string_for_label (s, num) = s ^ string_of_int num |
|
24 |
|
25 fun thms_of_name ctxt name = |
|
26 let |
|
27 val lex = Keyword.get_lexicons |
|
28 val get = maps (Proof_Context.get_fact ctxt o fst) |
|
29 in |
|
30 Source.of_string name |
|
31 |> Symbol.source |
|
32 |> Token.source {do_recover = SOME false} lex Position.start |
|
33 |> Token.source_proper |
|
34 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
|
35 |> Source.exhaust |
|
36 end |
|
37 |
|
38 val inc = curry op+ |
|
39 fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0 |
|
40 fun metis_steps_recursive proof = |
|
41 fold (fn Prove (_,_,_, By_Metis _) => inc 1 |
|
42 | Prove (_,_,_, Case_Split (cases, _)) => |
|
43 inc (fold (inc o metis_steps_recursive) cases 1) |
|
44 | _ => I) proof 0 |
|
45 |
|
46 end |