20 Obtain of |
20 Obtain of |
21 isar_qualifier list * (string * typ) list * label * term * byline | |
21 isar_qualifier list * (string * typ) list * label * term * byline | |
22 Prove of isar_qualifier list * label * term * byline |
22 Prove of isar_qualifier list * label * term * byline |
23 and byline = |
23 and byline = |
24 By_Metis of facts | |
24 By_Metis of facts | |
25 Case_Split of isar_step list list * facts | |
25 Case_Split of isar_step list list | |
26 Subblock of isar_step list |
26 Subblock of isar_step list |
27 |
27 |
28 val string_for_label : label -> string |
28 val string_for_label : label -> string |
29 val metis_steps_top_level : isar_step list -> int |
29 val metis_steps_top_level : isar_step list -> int |
30 val metis_steps_total : isar_step list -> int |
30 val metis_steps_total : isar_step list -> int |
44 Assume of label * term | |
44 Assume of label * term | |
45 Obtain of isar_qualifier list * (string * typ) list * label * term * byline | |
45 Obtain of isar_qualifier list * (string * typ) list * label * term * byline | |
46 Prove of isar_qualifier list * label * term * byline |
46 Prove of isar_qualifier list * label * term * byline |
47 and byline = |
47 and byline = |
48 By_Metis of facts | |
48 By_Metis of facts | |
49 Case_Split of isar_step list list * facts | |
49 Case_Split of isar_step list list | |
50 Subblock of isar_step list |
50 Subblock of isar_step list |
51 |
51 |
52 fun string_for_label (s, num) = s ^ string_of_int num |
52 fun string_for_label (s, num) = s ^ string_of_int num |
53 |
53 |
54 fun metis_steps_top_level proof = |
54 fun metis_steps_top_level proof = |
55 fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) |
55 fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) |
56 proof 0 |
56 proof 0 |
57 fun metis_steps_total proof = |
57 fun metis_steps_total proof = |
58 fold (fn Obtain _ => Integer.add 1 |
58 fold (fn Obtain _ => Integer.add 1 |
59 | Prove (_, _, _, By_Metis _) => Integer.add 1 |
59 | Prove (_, _, _, By_Metis _) => Integer.add 1 |
60 | Prove (_, _, _, Case_Split (cases, _)) => |
60 | Prove (_, _, _, Case_Split cases) => |
61 Integer.add (fold (Integer.add o metis_steps_total) cases 1) |
61 Integer.add (fold (Integer.add o metis_steps_total) cases 1) |
62 | Prove (_, _, _, Subblock subproof) => |
62 | Prove (_, _, _, Subblock subproof) => |
63 Integer.add (metis_steps_total subproof + 1) |
63 Integer.add (metis_steps_total subproof + 1) |
64 | _ => I) proof 0 |
64 | _ => I) proof 0 |
65 |
65 |