# HG changeset patch
# User blanchet
# Date 1272631969 -7200
# Node ID 870dfa6d00ce97c078b62debc02895395c6fc648
# Parent  badb32303d1ea1a9a9358c744a52eaa4a1a15576
eliminate trivial case splits from Isar proofs

diff -r badb32303d1e -r 870dfa6d00ce src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 30 14:52:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 30 14:52:49 2010 +0200
@@ -185,15 +185,15 @@
   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
                                          --| Scan.option ($$ ","))) []
 
-(* It is not clear why some literals are followed by sequences of stars. We
-   ignore them. *)
-fun parse_starred_predicate_term pool =
+(* It is not clear why some literals are followed by sequences of stars and/or
+   pluses. We ignore them. *)
+fun parse_decorated_predicate_term pool =
   parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
 
 fun parse_horn_clause pool =
-  Scan.repeat (parse_starred_predicate_term pool) --| $$ "|" --| $$ "|"
-    -- Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
-    -- Scan.repeat (parse_starred_predicate_term pool)
+  Scan.repeat (parse_decorated_predicate_term pool) --| $$ "|" --| $$ "|"
+    -- Scan.repeat (parse_decorated_predicate_term pool) --| $$ "-" --| $$ ">"
+    -- Scan.repeat (parse_decorated_predicate_term pool)
   >> (fn (([], []), []) => [str_leaf "c_False"]
        | ((clauses1, clauses2), clauses3) =>
          map negate_node (clauses1 @ clauses2) @ clauses3)
@@ -620,6 +620,9 @@
   ByMetis of facts |
   CaseSplit of step list list * facts
 
+fun smart_case_split [] facts = ByMetis facts
+  | smart_case_split proofs facts = CaseSplit (proofs, facts)
+
 val raw_prefix = "X"
 val assum_prefix = "A"
 val fact_prefix = "F"
@@ -645,7 +648,7 @@
                          thm_names frees =
   let
     val lines =
-      atp_proof ^ "$" (* the $ sign is a dummy token *)
+      atp_proof ^ "$" (* the $ sign acts as a sentinel *)
       |> parse_proof pool
       |> decode_lines ctxt
       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
@@ -788,10 +791,10 @@
                   SOME (l, t, proofs, proof_tail) =>
                   Have (case_split_qualifiers proofs @
                         (if null proof_tail then end_qs else []), l, t,
-                        CaseSplit (proofs, facts)) :: proof_tail
+                        smart_case_split proofs facts) :: proof_tail
                 | NONE =>
                   [Have (case_split_qualifiers proofs @ end_qs, no_label,
-                         concl_t, CaseSplit (proofs, facts))],
+                         concl_t, smart_case_split proofs facts)],
                 patches)
              end
            | _ => raise Fail "malformed proof")