author | wenzelm |
Thu, 13 Aug 2015 11:05:19 +0200 | |
changeset 60924 | 610794dff23c |
parent 59013 | f319054e8dff |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/z3_isar.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Z3 proofs as generic ATP proofs for Isar proof reconstruction. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
|
58061 | 7 |
signature Z3_ISAR = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
sig |
57541 | 9 |
val atp_proof_of_z3_proof: Proof.context -> term list -> thm list -> term list -> term -> |
58061 | 10 |
(string * term) list -> int list -> int -> (int * string) list -> Z3_Proof.z3_step list -> |
57159 | 11 |
(term, string) ATP_Proof.atp_step list |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
end; |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
|
58061 | 14 |
structure Z3_Isar: Z3_ISAR = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
open ATP_Util |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
open ATP_Problem |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
open ATP_Proof |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
open ATP_Proof_Reconstruct |
58061 | 21 |
open SMTLIB_Isar |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
|
58061 | 23 |
val z3_apply_def_rule = Z3_Proof.string_of_rule Z3_Proof.Apply_Def |
24 |
val z3_hypothesis_rule = Z3_Proof.string_of_rule Z3_Proof.Hypothesis |
|
25 |
val z3_intro_def_rule = Z3_Proof.string_of_rule Z3_Proof.Intro_Def |
|
26 |
val z3_lemma_rule = Z3_Proof.string_of_rule Z3_Proof.Lemma |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
28 |
fun inline_z3_defs _ [] = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
| inline_z3_defs defs ((name, role, t, rule, deps) :: lines) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
if rule = z3_intro_def_rule then |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
let val def = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> swap in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
32 |
inline_z3_defs (insert (op =) def defs) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
(map (replace_dependencies_in_line (name, [])) lines) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
34 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
else if rule = z3_apply_def_rule then |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
inline_z3_defs defs (map (replace_dependencies_in_line (name, [])) lines) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
37 |
else |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
38 |
(name, role, Term.subst_atomic defs t, rule, deps) :: inline_z3_defs defs lines |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
39 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
40 |
fun add_z3_hypotheses [] = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
41 |
| add_z3_hypotheses hyps = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
42 |
HOLogic.dest_Trueprop |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
#> curry s_imp (Library.foldr1 s_conj (map HOLogic.dest_Trueprop hyps)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
#> HOLogic.mk_Trueprop |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
fun inline_z3_hypotheses _ _ [] = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
| inline_z3_hypotheses hyp_names hyps ((name, role, t, rule, deps) :: lines) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
if rule = z3_hypothesis_rule then |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
inline_z3_hypotheses (name :: hyp_names) (AList.map_default (op =) (t, []) (cons name) hyps) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
lines |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
51 |
else |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
52 |
let val deps' = subtract (op =) hyp_names deps in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
if rule = z3_lemma_rule then |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
54 |
(name, role, t, rule, deps') :: inline_z3_hypotheses hyp_names hyps lines |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
55 |
else |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
56 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
57 |
val add_hyps = filter_out (null o inter (op =) deps o snd) hyps |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
val t' = add_z3_hypotheses (map fst add_hyps) t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
59 |
val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
(name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
|
57749 | 65 |
fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) = |
66 |
let val (s', t') = Term.dest_abs abs in |
|
67 |
dest_alls t' |>> cons (s', T) |
|
68 |
end |
|
69 |
| dest_alls t = ([], t) |
|
70 |
||
71 |
val reorder_foralls = |
|
72 |
dest_alls |
|
60924
610794dff23c
tuned signature, in accordance to sortBy in Scala;
wenzelm
parents:
59013
diff
changeset
|
73 |
#>> sort_by fst |
57749 | 74 |
#-> fold_rev (Logic.all o Free); |
75 |
||
57541 | 76 |
fun atp_proof_of_z3_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids |
77 |
conjecture_id fact_helper_ids proof = |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
let |
58061 | 79 |
fun steps_of (Z3_Proof.Z3_Step {id, rule, prems, concl, ...}) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
80 |
let |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56981
diff
changeset
|
81 |
val sid = string_of_int id |
56128 | 82 |
|
57749 | 83 |
val concl' = concl |
84 |
|> reorder_foralls (* crucial for skolemization steps *) |
|
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
85 |
|> postprocess_step_conclusion ctxt rewrite_rules ll_defs |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56855
diff
changeset
|
86 |
fun standard_step role = |
58061 | 87 |
((sid, []), role, concl', Z3_Proof.string_of_rule rule, |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56981
diff
changeset
|
88 |
map (fn id => (string_of_int id, [])) prems) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
89 |
in |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56855
diff
changeset
|
90 |
(case rule of |
58061 | 91 |
Z3_Proof.Asserted => |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57705
diff
changeset
|
92 |
let val ss = the_list (AList.lookup (op =) fact_helper_ids id) in |
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57705
diff
changeset
|
93 |
(case distinguish_conjecture_and_hypothesis ss id conjecture_id prem_ids fact_helper_ts |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57749
diff
changeset
|
94 |
hyp_ts concl_t of |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57705
diff
changeset
|
95 |
NONE => [] |
57745 | 96 |
| SOME (role0, concl00) => |
97 |
let |
|
98 |
val name0 = (sid ^ "a", ss) |
|
58064
e9ab6f4c650b
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
blanchet
parents:
58061
diff
changeset
|
99 |
val concl0 = unskolemize_names ctxt concl00 |
57745 | 100 |
in |
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57705
diff
changeset
|
101 |
(if role0 = Axiom then [] |
58061 | 102 |
else [(name0, role0, concl0, Z3_Proof.string_of_rule rule, [])]) @ |
103 |
[((sid, []), Plain, concl', Z3_Proof.string_of_rule Z3_Proof.Rewrite, |
|
57730
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57705
diff
changeset
|
104 |
name0 :: normalizing_prems ctxt concl0)] |
d39815cdb7ba
remove lambda-lifting related assumptions from generated Isar proofs
blanchet
parents:
57705
diff
changeset
|
105 |
end) |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56855
diff
changeset
|
106 |
end |
58061 | 107 |
| Z3_Proof.Rewrite => [standard_step Lemma] |
108 |
| Z3_Proof.Rewrite_Star => [standard_step Lemma] |
|
109 |
| Z3_Proof.Skolemize => [standard_step Lemma] |
|
110 |
| Z3_Proof.Th_Lemma _ => [standard_step Lemma] |
|
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56855
diff
changeset
|
111 |
| _ => [standard_step Plain]) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
112 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
113 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
proof |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56855
diff
changeset
|
115 |
|> maps steps_of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
|> inline_z3_defs [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
|> inline_z3_hypotheses [] [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
119 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
end; |