# HG changeset patch
# User blanchet
# Date 1394793099 -3600
# Node ID 9ee083f9da5b8befc809b5e5118e294b30595383
# Parent  c106ac2ff76dd09e48e0d5d27ef9a2f313bfd5ca
remove '__' skolem suffixes before showing terms to users

diff -r c106ac2ff76d -r 9ee083f9da5b src/HOL/Tools/SMT2/z3_new_isar.ML
--- a/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:15:46 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_isar.ML	Fri Mar 14 11:31:39 2014 +0100
@@ -63,18 +63,21 @@
           end
       end
 
-fun simplify_prop (@{const Not} $ t) = s_not (simplify_prop t)
-  | simplify_prop (@{const conj} $ t $ u) = s_conj (simplify_prop t, simplify_prop u)
-  | simplify_prop (@{const disj} $ t $ u) = s_disj (simplify_prop t, simplify_prop u)
-  | simplify_prop (@{const implies} $ t $ u) = s_imp (simplify_prop t, simplify_prop u)
-  | simplify_prop (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_prop t, simplify_prop u)
-  | simplify_prop (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
+fun simplify_bool (@{const Not} $ t) = s_not (simplify_bool t)
+  | simplify_bool (@{const conj} $ t $ u) = s_conj (simplify_bool t, simplify_bool u)
+  | simplify_bool (@{const disj} $ t $ u) = s_disj (simplify_bool t, simplify_bool u)
+  | simplify_bool (@{const implies} $ t $ u) = s_imp (simplify_bool t, simplify_bool u)
+  | simplify_bool (@{const HOL.eq (bool)} $ t $ u) = s_iff (simplify_bool t, simplify_bool u)
+  | simplify_bool (t as Const (@{const_name HOL.eq}, _) $ u $ v) =
     if u aconv v then @{const True} else t
-  | simplify_prop (t $ u) = simplify_prop t $ simplify_prop u
-  | simplify_prop (Abs (s, T, t)) = Abs (s, T, simplify_prop t)
-  | simplify_prop t = t
+  | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u
+  | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t)
+  | simplify_bool t = t
 
-fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps)
+(* It is not entirely clear why this should be necessary, especially for abstractions variables. *)
+val unskolemize_names =
+  Term.map_abs_vars (perhaps (try Name.dest_skolem))
+  #> Term.map_aterms (perhaps (try (fn Free (s, T) => Free (Name.dest_skolem s, T))))
 
 fun atp_proof_of_z3_proof thy rewrite_rules conjecture_id fact_ids proof =
   let
@@ -99,6 +102,8 @@
         val concl' = concl
           |> Raw_Simplifier.rewrite_term thy rewrite_rules []
           |> Object_Logic.atomize_term thy
+          |> simplify_bool
+          |> unskolemize_names
           |> HOLogic.mk_Trueprop
       in
         (name, role, concl', Z3_New_Proof.string_of_rule rule, map step_name_of prems)
@@ -108,7 +113,6 @@
     |> map step_of
     |> inline_z3_defs []
     |> inline_z3_hypotheses [] []
-    |> map simplify_line
   end
 
 end;