--- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Aug 28 00:40:38 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,123 +0,0 @@
-(* Title: HOL/Tools/SMT2/z3_new_isar.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Z3 proofs as generic ATP proofs for Isar proof reconstruction.
-*)
-
-signature Z3_NEW_ISAR =
-sig
- val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term ->
- (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list ->
- (term, string) ATP_Proof.atp_step list
-end;
-
-structure Z3_New_Isar: Z3_NEW_ISAR =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Proof_Reconstruct
-open SMTLIB2_Isar
-
-val z3_apply_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Apply_Def
-val z3_hypothesis_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Hypothesis
-val z3_intro_def_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Intro_Def
-val z3_lemma_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Lemma
-
-fun inline_z3_defs _ [] = []
- | inline_z3_defs defs ((name, role, t, rule, deps) :: lines) =
- if rule = z3_intro_def_rule then
- let val def = t |> HOLogic.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 add_z3_hypotheses [] = I
- | add_z3_hypotheses hyps =
- HOLogic.dest_Trueprop
- #> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps))
- #> HOLogic.mk_Trueprop
-
-fun inline_z3_hypotheses _ _ [] = []
- | inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) =
- if rule = z3_hypothesis_rule then
- inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps)
- lines
- else
- let val deps' = subtract (op =) hyp_names deps in
- if rule = z3_lemma_rule then
- (name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines
- else
- let
- val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
- val t' = add_z3_hypotheses (map fst add_hyps) t
- val deps' = subtract (op =) hyp_names deps
- val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
- in
- (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines
- end
- end
-
-fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) =
- let val (s', t') = Term.dest_abs abs in
- dest_alls t' |>> cons (s', T)
- end
- | dest_alls t = ([], t)
-
-val reorder_foralls =
- dest_alls
- #>> sort_wrt fst
- #-> fold_rev (Logic.all o Free);
-
-fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
- conjecture_id fact_helper_ids proof =
- let
- val thy = Proof_Context.theory_of ctxt
-
- fun steps_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) =
- let
- val sid = string_of_int id
-
- val concl' = concl
- |> reorder_foralls (* crucial for skolemization steps *)
- |> postprocess_step_conclusion thy rewrite_rules ll_defs
- fun standard_step role =
- ((sid, []), role, concl', Z3_New_Proof.string_of_rule rule,
- map (fn id => (string_of_int id, [])) prems)
- in
- (case rule of
- Z3_New_Proof.Asserted =>
- let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in
- (case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts
- hyp_ts concl_t of
- NONE => []
- | SOME (role0, concl00) =>
- let
- val name0 = (sid ^ "a", ss)
- val concl0 = unskolemize_names concl00
- in
- (if role0 = Axiom then []
- else [(name0, role0, concl0, Z3_New_Proof.string_of_rule rule, [])]) @
- [((sid, []), Plain, concl', Z3_New_Proof.string_of_rule Z3_New_Proof.Rewrite,
- name0 :: normalizing_prems ctxt concl0)]
- end)
- end
- | Z3_New_Proof.Rewrite => [standard_step Lemma]
- | Z3_New_Proof.Rewrite_Star => [standard_step Lemma]
- | Z3_New_Proof.Skolemize => [standard_step Lemma]
- | Z3_New_Proof.Th_Lemma _ => [standard_step Lemma]
- | _ => [standard_step Plain])
- end
- in
- proof
- |> maps steps_of
- |> inline_z3_defs []
- |> inline_z3_hypotheses [] []
- end
-
-end;