# HG changeset patch
# User blanchet
# Date 1386977205 -28800
# Node ID 6db5fbc0243633254d9196e626243ff01569f567
# Parent  05c9f3d84ba35588bca846727c0d76f8bf5f1f17
better handling of Z3 proof blocks

diff -r 05c9f3d84ba3 -r 6db5fbc02436 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Dec 13 22:54:39 2013 +0800
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Dec 14 07:26:45 2013 +0800
@@ -47,6 +47,21 @@
 
 open String_Redirect
 
+fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
+
+val e_skolemize_rule = "skolemize"
+val vampire_skolemisation_rule = "skolemisation"
+(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
+val z3_skolemize_rule = "skolemize"
+val z3_hypothesis_rule = "hypothesis"
+val z3_lemma_rule = "lemma"
+val z3_intro_def_rule = "intro-def"
+val z3_apply_def_rule = "apply-def"
+
+val is_skolemize_rule =
+  member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+
 fun raw_label_of_num num = (num, 0)
 
 fun label_of_clause [(num, _)] = raw_label_of_num num
@@ -60,42 +75,38 @@
 fun replace_dependencies_in_line p (name, role, t, rule, deps) =
   (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
 
+fun inline_z3_defs _ [] = []
+  | inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) =
+    if rule = z3_intro_def_rule then
+      let val def = t |> maybe_dest_Trueprop |> HOLogic.dest_eq |> swap in
+        inline_z3_defs (insert (op =) def defs)
+          (map (replace_dependencies_in_line (name, [])) lines)
+      end
+    else if rule = z3_apply_def_rule then
+      inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
+    else
+      (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
+
+fun inline_z3_hypotheses lines = lines
+
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
    clsarity). *)
 fun is_only_type_information t = t aconv @{term True}
 
-fun is_same_inference (role, t) (_, role', t', _, _) =
-  (t |> role = Conjecture ? s_not) aconv (t' |> role' = Conjecture ? s_not)
-
-fun is_False t = t aconv @{term False} orelse t aconv @{prop False}
-
-fun truncate_at_false [] = []
-  | truncate_at_false ((line as (_, role, t, _, _)) :: lines) =
-    line :: (if role <> Conjecture andalso is_False t then [] else truncate_at_false lines)
-
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
-fun add_line (name as (_, ss), role, t, rule, []) lines =
+fun add_line (line as (name as (_, ss), role, t, rule, [])) lines =
     (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
        internal facts or definitions. *)
     if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
        role = Hypothesis then
-      (name, role, t, rule, []) :: lines
+      line :: lines
     else if role = Axiom then
       (* Facts are not proof lines. *)
       lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
     else
       map (replace_dependencies_in_line (name, [])) lines
-  | add_line (line as (name, role, t, _, _)) lines =
-    (* Type information will be deleted later; skip repetition test. *)
-    if is_only_type_information t then
-      line :: lines
-    else
-      (* Is there a repetition? If so, replace later line by earlier one. *)
-      (case take_prefix (not o is_same_inference (role, t)) lines of
-        (_, []) => line :: lines
-      | (pre, (name', _, _, _, _) :: post) =>
-        line :: pre @ map (replace_dependencies_in_line (name', [name])) post)
+  | add_line line lines = line :: lines
 
 (* Recursively delete empty lines (type information) from the proof. *)
 fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
@@ -104,19 +115,13 @@
 and delete_dependency name lines =
   fold_rev add_nontrivial_line (map (replace_dependencies_in_line (name, [])) lines) []
 
-val e_skolemize_rule = "skolemize"
-val vampire_skolemisation_rule = "skolemisation"
-
-val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
-
 fun add_desired_lines res [] = rev res
   | add_desired_lines res ((name as (_, ss), role, t, rule, deps) :: lines) =
     if role <> Plain orelse is_skolemize_rule rule orelse
        (* the last line must be kept *)
        null lines orelse
-       (not (is_only_type_information t) andalso
-        null (Term.add_tvars t []) andalso
-        length deps >= 2 andalso
+       (not (is_only_type_information t) andalso null (Term.add_tvars t [])
+        andalso length deps >= 2 andalso
         (* don't keep next to last line, which usually results in a trivial step *)
         not (can the_single lines)) then
       add_desired_lines ((name, role, t, rule, deps) :: res) lines
@@ -205,9 +210,6 @@
     and chain_proofs proofs = map (chain_proof) proofs
   in chain_proof end
 
-fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
-val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
-
 type isar_params =
   bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
   thm
@@ -232,7 +234,8 @@
       let
         val atp_proof =
           atp_proof
-          |> truncate_at_false
+          |> inline_z3_defs []
+          |> inline_z3_hypotheses
           |> rpair [] |-> fold_rev add_line
           |> rpair [] |-> fold_rev add_nontrivial_line
           |> add_desired_lines []