# HG changeset patch
# User blanchet
# Date 1272484769 -7200
# Node ID cc42df660808e6f41d82a6c6622e872b06962361
# Parent  f8da913b6c3a366634d68a902cbd9243cb7644a3
improve unskolemization

diff -r f8da913b6c3a -r cc42df660808 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 18:11:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Apr 28 21:59:29 2010 +0200
@@ -42,7 +42,14 @@
 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
 
+(* Hack: Could return false positives (e.g., a user happens to declare a
+   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+  Long_Name.base_name
+  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
+val index_in_shape = find_index o exists o curry (op =)
 
 fun ugly_name NONE s = s
   | ugly_name (SOME the_pool) s =
@@ -51,15 +58,13 @@
     | NONE => s
 
 fun smart_lambda v t =
-    Abs (case v of
-           Const (s, _) =>
-           List.last (space_explode skolem_infix (Long_Name.base_name s))
-         | Var ((s, _), _) => s
-         | Free (s, _) => s
-         | _ => "", fastype_of v, abstract_over (v, t))
-
+  Abs (case v of
+         Const (s, _) =>
+         List.last (space_explode skolem_infix (Long_Name.base_name s))
+       | Var ((s, _), _) => s
+       | Free (s, _) => s
+       | _ => "", fastype_of v, abstract_over (v, t))
 fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ smart_lambda v t
 
 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
   Definition of 'a * 'b * 'c |
@@ -381,19 +386,22 @@
         | tmsubst (t as Bound _) = t
         | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
         | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
-  in not (Vartab.is_empty vt) ? tmsubst end;
+  in not (Vartab.is_empty vt) ? tmsubst end
+
+fun unskolemize_term t =
+  fold forall_of (Term.add_consts t []
+                 |> filter (is_skolem_const_name o fst) |> map Const) t
 
 (* Interpret a list of syntax trees as a clause, given by "real" literals and
    sort constraints. "vt" holds the initial sort constraints, from the
    conjecture clauses. *)
 fun clause_of_nodes ctxt vt us =
-  let val (vt, dt) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
-    dt |> repair_sorts vt
+  let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
+    t |> repair_sorts vt
   end
 fun check_clause ctxt =
   TypeInfer.constrain HOLogic.boolT
   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-fun checked_clause_of_nodes ctxt = check_clause ctxt oo clause_of_nodes ctxt
 
 (** Global sort constraints on TFrees (from tfree_tcs) are positive unit
     clauses. **)
@@ -420,22 +428,25 @@
 
 fun decode_line vt (Definition (num, u, us)) ctxt =
     let
-      val cl1 = clause_of_nodes ctxt vt [u]
-      val vars = snd (strip_comb cl1)
+      val t1 = clause_of_nodes ctxt vt [u]
+      val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val cl2 = clause_of_nodes ctxt vt us
-      val (cl1, cl2) =
-        HOLogic.eq_const HOLogic.typeT $ cl1 $ cl2
+      val t2 = clause_of_nodes ctxt vt us
+      val (t1, t2) =
+        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
     in
-      (Definition (num, cl1, cl2),
-       fold Variable.declare_term (maps OldTerm.term_frees [cl1, cl2]) ctxt)
+      (Definition (num, t1, t2),
+       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
   | decode_line vt (Inference (num, us, deps)) ctxt =
-    let val cl = us |> clause_of_nodes ctxt vt |> check_clause ctxt in
-      (Inference (num, cl, deps),
-       fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+    let
+      val t = us |> clause_of_nodes ctxt vt |> unskolemize_term
+                 |> check_clause ctxt
+    in
+      (Inference (num, t, deps),
+       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     end
 fun decode_lines ctxt lines =
   let
@@ -457,9 +468,10 @@
 
 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   only in type information.*)
-fun add_line _ (line as Definition _) lines = line :: lines
-  | add_line thm_names (Inference (num, t, [])) lines =
-    (* No dependencies: axiom or conjecture clause *)
+fun add_line _ _ (line as Definition _) lines = line :: lines
+  | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
+    (* No dependencies: axiom, conjecture clause, or internal axioms
+       (Vampire). *)
     if is_axiom_clause_number thm_names num then
       (* Axioms are not proof lines. *)
       if is_only_type_information t then
@@ -469,9 +481,11 @@
         (_, []) => lines (*no repetition of proof line*)
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
-    else
+    else if index_in_shape num conjecture_shape >= 0 then
       Inference (num, t, []) :: lines
-  | add_line _ (Inference (num, t, deps)) lines =
+    else
+      lines
+  | add_line _ _ (Inference (num, t, deps)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
       Inference (num, t, deps) :: lines
@@ -492,6 +506,7 @@
 and delete_dep num lines =
   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
 
+(* FIXME: this seems not to have worked and is obsolete anyway *)
 fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
   | is_bad_free _ = false
 
@@ -596,13 +611,14 @@
           forall_vars t,
           Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
 
-fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
+fun proof_from_atp_proof pool ctxt shrink_factor atp_proof conjecture_shape
+                         thm_names frees =
   let
     val lines =
       atp_proof ^ "$" (* the $ sign is a dummy token *)
       |> parse_proof pool
       |> decode_lines ctxt
-      |> rpair [] |-> fold_rev (add_line thm_names)
+      |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
       |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
       |> snd
@@ -662,22 +678,20 @@
   | 1 => [Then]
   | _ => [Ultimately]
 
-val index_in_shape = find_index o exists o curry (op =)
-
 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
   let
     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
-    fun find_hyp (_, j) = nth hyp_ts (index_in_shape j conjecture_shape)
+    fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
     fun first_pass ([], contra) = ([], contra)
       | first_pass ((step as Fix _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
       | first_pass ((step as Let _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
-      | first_pass ((step as Assume (l, t)) :: proof, contra) =
+      | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
         if member (op =) concl_ls l then
           first_pass (proof, contra ||> cons step)
         else
-          first_pass (proof, contra) |>> cons (Assume (l, find_hyp l))
+          first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
       | first_pass ((step as Have (qs, l, t, Facts (ls, ss))) :: proof,
                     contra) =
         if exists (member (op =) (fst contra)) ls then
@@ -773,21 +787,6 @@
     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   in do_proof end
 
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
-   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
-  Long_Name.base_name
-  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-fun unskolemize_term t =
-  fold exists_of (Term.add_consts t []
-                  |> filter (is_skolem_const_name o fst) |> map Const) t
-
-fun unskolemize_step (Have (qs, l, t, by)) =
-    Have (qs, l, unskolemize_term t, by)
-  | unskolemize_step step = step
-
 val then_chain_proof =
   let
     fun aux _ [] = []
@@ -866,7 +865,7 @@
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
-    fun do_raw_label (s, j) = s ^ string_of_int j
+    fun do_raw_label (s, num) = s ^ string_of_int num
     fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
     fun do_have qs =
       (if member (op =) qs Moreover then "moreover " else "") ^
@@ -921,11 +920,10 @@
     val (one_line_proof, lemma_names) =
       metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
     fun isar_proof_for () =
-      case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names
-                                frees
+      case proof_from_atp_proof pool ctxt shrink_factor atp_proof
+                                conjecture_shape thm_names frees
            |> redirect_proof thy conjecture_shape hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof
-           |> map unskolemize_step
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof