47 val byline_of_step : isar_step -> (facts * proof_method) option |
41 val byline_of_step : isar_step -> (facts * proof_method) option |
48 val proof_method_of_step : isar_step -> proof_method option |
42 val proof_method_of_step : isar_step -> proof_method option |
49 val use_metis_new_skolem : isar_step -> bool |
43 val use_metis_new_skolem : isar_step -> bool |
50 |
44 |
51 val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a |
45 val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a |
52 val fold_isar_steps : |
46 val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a |
53 (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a |
|
54 |
47 |
55 val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
48 val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof |
56 |
49 |
57 val add_proof_steps : isar_step list -> int -> int |
50 val add_proof_steps : isar_step list -> int -> int |
58 |
51 |
76 and isar_step = |
69 and isar_step = |
77 Let of term * term | |
70 Let of term * term | |
78 Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * |
71 Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list * |
79 (facts * proof_method) |
72 (facts * proof_method) |
80 and proof_method = |
73 and proof_method = |
81 MetisM | |
74 Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method | |
82 SimpM | |
75 Blast_Method | Meson_Method |
83 AutoM | |
|
84 FastforceM | |
|
85 ForceM | |
|
86 ArithM | |
|
87 BlastM | |
|
88 MesonM |
|
89 |
76 |
90 val no_label = ("", ~1) |
77 val no_label = ("", ~1) |
91 val no_facts = ([],[]) |
78 val no_facts = ([],[]) |
92 |
79 |
93 val label_ord = pairself swap #> prod_ord int_ord fast_string_ord |
80 val label_ord = pairself swap #> prod_ord int_ord fast_string_ord |
110 | byline_of_step _ = NONE |
97 | byline_of_step _ = NONE |
111 |
98 |
112 fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method |
99 fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method |
113 | proof_method_of_step _ = NONE |
100 | proof_method_of_step _ = NONE |
114 |
101 |
|
102 (* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see |
|
103 also "atp_proof_reconstruct.ML" concerning Vampire). *) |
115 fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) = |
104 fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) = |
116 meth = MetisM andalso exists (fn (_, T) => length (binder_types T) > 1) xs |
105 meth = Metis_Method andalso exists (fn (_, T) => length (binder_types T) > 1) xs |
117 | use_metis_new_skolem _ = false |
106 | use_metis_new_skolem _ = false |
118 |
107 |
119 fun fold_isar_steps f = fold (fold_isar_step f) |
108 fun fold_isar_steps f = fold (fold_isar_step f) |
120 and fold_isar_step f step s = |
109 and fold_isar_step f step = |
121 fold (steps_of_proof #> fold_isar_steps f) |
110 fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) |
122 (these (subproofs_of_step step)) s |
111 #> f step |
123 |> f step |
|
124 |
112 |
125 fun map_isar_steps f proof = |
113 fun map_isar_steps f = |
126 let |
114 let |
127 fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps) |
115 fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps) |
128 and do_step (step as Let _) = f step |
116 and do_step (step as Let _) = f step |
129 | do_step (Prove (qs, xs, l, t, subproofs, by)) = |
117 | do_step (Prove (qs, xs, l, t, subproofs, by)) = |
130 f (Prove (qs, xs, l, t, map do_proof subproofs, by)) |
118 f (Prove (qs, xs, l, t, map do_proof subproofs, by)) |
131 in |
119 in |
132 do_proof proof |
120 do_proof |
133 end |
121 end |
134 |
122 |
135 val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) |
123 val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I) |
136 |
124 |
137 |
125 |