# HG changeset patch
# User blanchet
# Date 1360919924 -3600
# Node ID 020a6812a204d8f07009d62c9a33d2c0d419697e
# Parent  754127b3af235d7d500ce92b16021e78c569e188
removed dead weight from data structure

diff -r 754127b3af23 -r 020a6812a204 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- 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
diff -r 754127b3af23 -r 020a6812a204 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- 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
diff -r 754127b3af23 -r 020a6812a204 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- 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)
diff -r 754127b3af23 -r 020a6812a204 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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