--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jun 26 18:25:13 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jun 26 18:26:00 2013 +0200
@@ -9,21 +9,21 @@
signature SLEDGEHAMMER_PROOF =
sig
type label = string * int
- type facts = label list * string list (* local & global *)
+ type facts = label list * string list (* local & global facts *)
datatype isar_qualifier = Show | Then
datatype fix = Fix of (string * typ) list
datatype assms = Assume of (label * term) list
- datatype isar_proof =
+ datatype isar_proof =
Proof of fix * assms * isar_step list
and isar_step =
Let of term * term |
- (* for |fix|>0, this is an obtain step *)
- Prove of isar_qualifier list * fix * label * term * byline
+ (* for |fix|>0, this is an obtain step; step may contain subproofs *)
+ Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
and byline =
- By_Metis of isar_proof list * facts
+ By_Metis of facts
val no_label : label
val no_facts : facts
@@ -34,8 +34,13 @@
val steps_of_proof : isar_proof -> isar_step list
val label_of_step : isar_step -> label option
+ val subproofs_of_step : isar_step -> isar_proof list option
val byline_of_step : isar_step -> byline option
+ val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
+ val fold_isar_steps :
+ (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
+
val add_metis_steps_top_level : isar_step list -> int -> int
val add_metis_steps : isar_step list -> int -> int
end
@@ -44,21 +49,21 @@
struct
type label = string * int
-type facts = label list * string list
+type facts = label list * string list (* local & global facts *)
datatype isar_qualifier = Show | Then
datatype fix = Fix of (string * typ) list
datatype assms = Assume of (label * term) list
-datatype isar_proof =
+datatype isar_proof =
Proof of fix * assms * isar_step list
and isar_step =
Let of term * term |
- (* for |fix|>0, this is an obtain step *)
- Prove of isar_qualifier list * fix * label * term * byline
+ (* for |fix|>0, this is an obtain step; step may contain subproofs *)
+ Prove of isar_qualifier list * fix * label * term * isar_proof list * byline
and byline =
- By_Metis of isar_proof list * facts
+ By_Metis of facts
val no_label = ("", ~1)
val no_facts = ([],[])
@@ -69,20 +74,26 @@
fun assms_of_proof (Proof (_, assms, _)) = assms
fun steps_of_proof (Proof (_, _, steps)) = steps
-fun label_of_step (Prove (_, _, l, _, _)) = SOME l
+fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
| label_of_step _ = NONE
-fun byline_of_step (Prove (_, _, _, _, byline)) = SOME byline
+fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+ | subproofs_of_step _ = NONE
+
+fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
| byline_of_step _ = NONE
+fun fold_isar_step f step s =
+ fold (steps_of_proof #> fold (fold_isar_step f))
+ (the_default [] (subproofs_of_step step)) s
+ |> f step
+
+fun fold_isar_steps f = fold (fold_isar_step f)
+
val add_metis_steps_top_level =
fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))
-fun add_metis_steps steps =
- fold (byline_of_step
- #> (fn SOME (By_Metis (subproofs, _)) =>
- Integer.add 1 #> add_substeps subproofs
- | _ => I)) steps
-and add_substeps subproofs = fold (steps_of_proof #> add_metis_steps) subproofs
-
+val add_metis_steps =
+ fold_isar_steps
+ (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I))
end