1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Dec 13 22:54:39 2013 +0800
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Dec 14 07:26:45 2013 +0800
1.3 @@ -47,6 +47,21 @@
1.4
1.5 open String_Redirect
1.6
1.7 +fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
1.8 +val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
1.9 +
1.10 +val e_skolemize_rule = "skolemize"
1.11 +val vampire_skolemisation_rule = "skolemisation"
1.12 +(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
1.13 +val z3_skolemize_rule = "skolemize"
1.14 +val z3_hypothesis_rule = "hypothesis"
1.15 +val z3_lemma_rule = "lemma"
1.16 +val z3_intro_def_rule = "intro-def"
1.17 +val z3_apply_def_rule = "apply-def"
1.18 +
1.19 +val is_skolemize_rule =
1.20 + member (op =) [e_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
1.21 +
1.22 fun raw_label_of_num num = (num, 0)
1.23
1.24 fun label_of_clause [(num, _)] = raw_label_of_num num
1.25 @@ -60,42 +75,38 @@
1.26 fun replace_dependencies_in_line p (name, role, t, rule, deps) =
1.27 (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps [])
1.28
1.29 +fun inline_z3_defs _ [] = []
1.30 + | inline_z3_defs defs ((line as (name, role, t, rule, deps)) :: lines) =
1.31 + if rule = z3_intro_def_rule then
1.32 + let val def = t |> maybe_dest_Trueprop |> HOLogic.dest_eq |> swap in
1.33 + inline_z3_defs (insert (op =) def defs)
1.34 + (map (replace_dependencies_in_line (name, [])) lines)
1.35 + end
1.36 + else if rule = z3_apply_def_rule then
1.37 + inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines)
1.38 + else
1.39 + (name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines
1.40 +
1.41 +fun inline_z3_hypotheses lines = lines
1.42 +
1.43 (* No "real" literals means only type information (tfree_tcs, clsrel, or
1.44 clsarity). *)
1.45 fun is_only_type_information t = t aconv @{term True}
1.46
1.47 -fun is_same_inference (role, t) (_, role', t', _, _) =
1.48 - (t |> role = Conjecture ? s_not) aconv (t' |> role' = Conjecture ? s_not)
1.49 -
1.50 -fun is_False t = t aconv @{term False} orelse t aconv @{prop False}
1.51 -
1.52 -fun truncate_at_false [] = []
1.53 - | truncate_at_false ((line as (_, role, t, _, _)) :: lines) =
1.54 - line :: (if role <> Conjecture andalso is_False t then [] else truncate_at_false lines)
1.55 -
1.56 (* Discard facts; consolidate adjacent lines that prove the same formula, since
1.57 they differ only in type information.*)
1.58 -fun add_line (name as (_, ss), role, t, rule, []) lines =
1.59 +fun add_line (line as (name as (_, ss), role, t, rule, [])) lines =
1.60 (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire)
1.61 internal facts or definitions. *)
1.62 if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
1.63 role = Hypothesis then
1.64 - (name, role, t, rule, []) :: lines
1.65 + line :: lines
1.66 else if role = Axiom then
1.67 (* Facts are not proof lines. *)
1.68 lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
1.69 else
1.70 map (replace_dependencies_in_line (name, [])) lines
1.71 - | add_line (line as (name, role, t, _, _)) lines =
1.72 - (* Type information will be deleted later; skip repetition test. *)
1.73 - if is_only_type_information t then
1.74 - line :: lines
1.75 - else
1.76 - (* Is there a repetition? If so, replace later line by earlier one. *)
1.77 - (case take_prefix (not o is_same_inference (role, t)) lines of
1.78 - (_, []) => line :: lines
1.79 - | (pre, (name', _, _, _, _) :: post) =>
1.80 - line :: pre @ map (replace_dependencies_in_line (name', [name])) post)
1.81 + | add_line line lines = line :: lines
1.82
1.83 (* Recursively delete empty lines (type information) from the proof. *)
1.84 fun add_nontrivial_line (line as (name, _, t, _, [])) lines =
1.85 @@ -104,19 +115,13 @@
1.86 and delete_dependency name lines =
1.87 fold_rev add_nontrivial_line (map (replace_dependencies_in_line (name, [])) lines) []
1.88
1.89 -val e_skolemize_rule = "skolemize"
1.90 -val vampire_skolemisation_rule = "skolemisation"
1.91 -
1.92 -val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule]
1.93 -
1.94 fun add_desired_lines res [] = rev res
1.95 | add_desired_lines res ((name as (_, ss), role, t, rule, deps) :: lines) =
1.96 if role <> Plain orelse is_skolemize_rule rule orelse
1.97 (* the last line must be kept *)
1.98 null lines orelse
1.99 - (not (is_only_type_information t) andalso
1.100 - null (Term.add_tvars t []) andalso
1.101 - length deps >= 2 andalso
1.102 + (not (is_only_type_information t) andalso null (Term.add_tvars t [])
1.103 + andalso length deps >= 2 andalso
1.104 (* don't keep next to last line, which usually results in a trivial step *)
1.105 not (can the_single lines)) then
1.106 add_desired_lines ((name, role, t, rule, deps) :: res) lines
1.107 @@ -205,9 +210,6 @@
1.108 and chain_proofs proofs = map (chain_proof) proofs
1.109 in chain_proof end
1.110
1.111 -fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
1.112 -val maybe_dest_Trueprop = perhaps (try HOLogic.dest_Trueprop)
1.113 -
1.114 type isar_params =
1.115 bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
1.116 thm
1.117 @@ -232,7 +234,8 @@
1.118 let
1.119 val atp_proof =
1.120 atp_proof
1.121 - |> truncate_at_false
1.122 + |> inline_z3_defs []
1.123 + |> inline_z3_hypotheses
1.124 |> rpair [] |-> fold_rev add_line
1.125 |> rpair [] |-> fold_rev add_nontrivial_line
1.126 |> add_desired_lines []