--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Feb 15 10:13:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Feb 15 10:18:44 2013 +0100
@@ -89,8 +89,7 @@
(* proof references *)
fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = lookup_indices lfs
| refs (Prove (_, _, _, By_Metis (lfs, _))) = lookup_indices lfs
- | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) =
- lookup_indices lfs @ maps (maps refs) cases
+ | refs (Prove (_, _, _, Case_Split cases)) = maps (maps refs) cases
| refs (Prove (_, _, _, Subblock proof)) = maps refs proof
| refs _ = []
val refed_by_vect =
@@ -234,9 +233,9 @@
in fold_map f_m candidates zero_preplay_time end
val compress_subproof =
compress_each_and_collect_time (do_proof false ctxt)
- fun compress (Prove (qs, l, t, Case_Split (cases, facts))) =
+ fun compress (Prove (qs, l, t, Case_Split cases)) =
let val (cases, time) = compress_subproof cases
- in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
+ in (Prove (qs, l, t, Case_Split cases), time) end
| compress (Prove (qs, l, t, Subblock proof)) =
let val ([proof], time) = compress_subproof [proof]
in (Prove (qs, l, t, Subblock proof), time) end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Feb 15 10:13:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Feb 15 10:18:44 2013 +0100
@@ -84,17 +84,15 @@
val facts =
(case byline of
By_Metis fact_names => resolve_fact_names ctxt fact_names
- | Case_Split (cases, fact_names) =>
- resolve_fact_names ctxt fact_names
- @ (case the succedent of
- Assume (_, t) => make_thm t
- | Obtain (_, _, _, t, _) => make_thm t
- | Prove (_, _, t, _) => make_thm t
- | _ => error "preplay error: unexpected succedent of case split")
- :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
- | _ => error "preplay error: malformed case split")
- #> make_thm)
- cases
+ | Case_Split cases =>
+ (case the succedent of
+ Assume (_, t) => make_thm t
+ | Obtain (_, _, _, t, _) => make_thm t
+ | Prove (_, _, t, _) => make_thm t
+ | _ => error "preplay error: unexpected succedent of case split")
+ :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+ | _ => error "preplay error: malformed case split")
+ #> make_thm) cases
| Subblock proof =>
let
val (steps, last_step) = split_last proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 15 10:13:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 15 10:18:44 2013 +0100
@@ -22,7 +22,7 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts |
+ Case_Split of isar_step list list |
Subblock of isar_step list
val string_for_label : label -> string
@@ -46,7 +46,7 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts |
+ Case_Split of isar_step list list |
Subblock of isar_step list
fun string_for_label (s, num) = s ^ string_of_int num
@@ -57,7 +57,7 @@
fun metis_steps_total proof =
fold (fn Obtain _ => Integer.add 1
| Prove (_, _, _, By_Metis _) => Integer.add 1
- | Prove (_, _, _, Case_Split (cases, _)) =>
+ | Prove (_, _, _, Case_Split cases) =>
Integer.add (fold (Integer.add o metis_steps_total) cases 1)
| Prove (_, _, _, Subblock subproof) =>
Integer.add (metis_steps_total subproof + 1)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Feb 15 10:13:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Feb 15 10:18:44 2013 +0100
@@ -501,10 +501,10 @@
do_metis ind "using [[metis_new_skolem]] " facts ^ "\n"
| do_step ind (Prove (qs, l, t, By_Metis facts)) =
do_prove ind qs l t facts
- | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
+ | do_step ind (Prove (qs, l, t, Case_Split proofs)) =
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
proofs) ^
- do_prove ind qs l t facts
+ do_prove ind qs l t ([], [])
| do_step ind (Prove (qs, l, t, Subblock proof)) =
do_block ind proof ^ do_prove ind qs l t ([], [])
and do_steps prefix suffix ind steps =
@@ -531,8 +531,7 @@
| used_labels_of_step (Prove (_, _, _, by)) =
(case by of
By_Metis (ls, _) => ls
- | Case_Split (proofs, (ls, _)) =>
- fold (union (op =) o used_labels_of) proofs ls
+ | Case_Split proofs => fold (union (op =) o used_labels_of) proofs []
| Subblock proof => used_labels_of proof)
| used_labels_of_step _ = []
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
@@ -546,8 +545,7 @@
| do_step (Prove (qs, l, t, by)) =
Prove (qs, do_label l, t,
case by of
- Case_Split (proofs, facts) =>
- Case_Split (map do_proof proofs, facts)
+ Case_Split proofs => Case_Split (map do_proof proofs)
| Subblock proof => Subblock (do_proof proof)
| _ => by)
| do_step step = step
@@ -570,9 +568,8 @@
fun do_byline subst depth nexts by =
case by of
By_Metis facts => By_Metis (do_facts subst facts)
- | Case_Split (proofs, facts) =>
- Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs,
- do_facts subst facts)
+ | Case_Split proofs =>
+ Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs)
| Subblock proof => Subblock (do_proof subst depth nexts proof)
and do_proof _ _ _ [] = []
| do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) =
@@ -623,8 +620,8 @@
Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs))
else
step
- | chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) =
- Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs, facts))
+ | chain_step _ (Prove (qs, l, t, Case_Split proofs)) =
+ Prove (qs, l, t, Case_Split (map (chain_proof NONE) proofs))
| chain_step _ (Prove (qs, l, t, Subblock proof)) =
Prove (qs, l, t, Subblock (chain_proof NONE proof))
| chain_step _ step = step
@@ -750,10 +747,9 @@
Assume (label_of_clause c, prop_of_clause c) ::
map (isar_step_of_direct_inf false) infs
val c = succedent_of_cases cases
- val cases = map do_case cases
in
Prove (maybe_show outer c [Ultimately], label_of_clause c,
- prop_of_clause c, Case_Split (cases, ([], [])))
+ prop_of_clause c, Case_Split (map do_case cases))
end
fun isar_proof_of_direct_proof direct_proof =
direct_proof