# HG changeset patch
# User blanchet
# Date 1368517743 -7200
# Node ID e5303bd748f22546241ac83cb9265ad6765c1e5c
# Parent  7bab3fb52e3eadd3b404b894e09d054cd9b9ccae
generate valid direct Isar proof also if the facts are contradictory

diff -r 7bab3fb52e3e -r e5303bd748f2 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue May 14 07:09:09 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue May 14 09:49:03 2013 +0200
@@ -276,7 +276,8 @@
   | _ => (raw_prefix ^ ascii_of num, 0)
 
 fun label_of_clause [name] = raw_label_for_name name
-  | label_of_clause c = (space_implode "___" (map (fst o raw_label_for_name) c), 0)
+  | label_of_clause c =
+    (space_implode "___" (map (fst o raw_label_for_name) c), 0)
 
 fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
     if is_fact fact_names ss then
@@ -432,19 +433,21 @@
     fun of_moreover ind = of_indent ind ^ "moreover\n"
     fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
     fun of_obtain qs nr =
-      (if nr>1 orelse (nr=1 andalso member (op=) qs Then)
-        then "ultimately "
-      else if nr=1 orelse member (op=) qs Then
-        then "then "
-        else "") ^ "obtain"
-    fun of_show_have qs = if member (op=) qs Show then "show" else "have"
-    fun of_thus_hence qs = if member (op=) qs Show then "thus" else "hence"
+      (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+         "ultimately "
+       else if nr=1 orelse member (op =) qs Then then
+         "then "
+       else
+         "") ^ "obtain"
+    fun of_show_have qs = if member (op =) qs Show then "show" else "have"
+    fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
     fun of_prove qs nr =
-      if nr>1 orelse (nr=1 andalso member (op=) qs Then)
-        then "ultimately " ^ of_show_have qs
-      else if nr=1 orelse member (op=) qs Then
-        then of_thus_hence qs
-        else of_show_have qs
+      if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+        "ultimately " ^ of_show_have qs
+      else if nr=1 orelse member (op =) qs Then then
+        of_thus_hence qs
+      else
+        of_show_have qs
     fun add_term term (s, ctxt) =
       (s ^ (annotate_types ctxt term
             |> with_vanilla_print_mode (Syntax.string_of_term ctxt)
@@ -490,7 +493,7 @@
       end
     and of_subproofs _ _ _ [] = ""
       | of_subproofs ind ctxt qs subproofs =
-        (if member (op=) qs Then then of_moreover ind else "") ^
+        (if member (op =) qs Then then of_moreover ind else "") ^
         space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
     and add_step_pre ind qs subproofs (s, ctxt) =
       (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
@@ -726,7 +729,15 @@
             val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
             fun skolems_of t =
               Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
-            fun do_steps _ _ accum [] = rev accum
+            fun do_steps outer predecessor accum [] =
+                accum
+                |> (if tainted = [] then
+                      cons (Prove (if outer then [Show] else [], no_label,
+                                   concl_t,
+                                   By_Metis ([], ([the predecessor], []))))
+                    else
+                      I)
+                |> rev
               | do_steps outer _ accum (Have (gamma, c) :: infs) =
                 let
                   val l = label_of_clause c
@@ -736,8 +747,8 @@
                       (fold (add_fact_from_dependencies fact_names)
                             gamma no_facts))
                   fun prove by = Prove (maybe_show outer c [], l, t, by)
-                  fun do_rest lbl step =
-                    do_steps outer (SOME lbl) (step :: accum) infs
+                  fun do_rest l step =
+                    do_steps outer (SOME l) (step :: accum) infs
                 in
                   if is_clause_tainted c then
                     case gamma of
@@ -764,13 +775,14 @@
               | do_steps outer predecessor accum (Cases cases :: infs) =
                 let
                   fun do_case (c, infs) =
-                    do_proof false [] [(label_of_clause c, prop_of_clause c)] infs
+                    do_proof false [] [(label_of_clause c, prop_of_clause c)]
+                             infs
                   val c = succedent_of_cases cases
                   val l = label_of_clause c
                   val t = prop_of_clause c
                   val step =
-                    (Prove (maybe_show outer c [], l, t, By_Metis
-                      (map do_case cases, (the_list predecessor, []))))
+                    Prove (maybe_show outer c [], l, t,
+                      By_Metis (map do_case cases, (the_list predecessor, [])))
                 in
                   do_steps outer (SOME l) (step :: accum) infs
                 end