author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 69204 | d5ab1636660b |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/z3_replay_methods.ML |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
5 |
Proof methods for replaying Z3 proofs. |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
6 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
7 |
|
58061 | 8 |
signature Z3_REPLAY_METHODS = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
sig |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
11 |
(*methods for Z3 proof rules*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
12 |
type z3_method = Proof.context -> thm list -> term -> thm |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
13 |
val true_axiom: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
14 |
val mp: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
15 |
val refl: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
val symm: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
17 |
val trans: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
18 |
val cong: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
19 |
val quant_intro: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
val distrib: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
21 |
val and_elim: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
val not_or_elim: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
val rewrite: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
val rewrite_star: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
25 |
val pull_quant: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
26 |
val push_quant: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
27 |
val elim_unused: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
28 |
val dest_eq_res: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
val quant_inst: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
val lemma: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
val unit_res: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
32 |
val iff_true: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
val iff_false: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
34 |
val comm: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
val def_axiom: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
val apply_def: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
37 |
val iff_oeq: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
38 |
val nnf_pos: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
39 |
val nnf_neg: z3_method |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
40 |
val mp_oeq: z3_method |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
41 |
val arith_th_lemma: z3_method |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
42 |
val th_lemma: string -> z3_method |
58061 | 43 |
val method_for: Z3_Proof.z3_rule -> z3_method |
57229 | 44 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
|
58061 | 46 |
structure Z3_Replay_Methods: Z3_REPLAY_METHODS = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
48 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
49 |
type z3_method = Proof.context -> thm list -> term -> thm |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
51 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
52 |
(* utility functions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
54 |
fun replay_error ctxt msg rule thms t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
55 |
SMT_Replay_Methods.replay_error ctxt msg (Z3_Proof.string_of_rule rule) thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
56 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
57 |
fun replay_rule_error ctxt rule thms t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
58 |
SMT_Replay_Methods.replay_rule_error ctxt (Z3_Proof.string_of_rule rule) thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
59 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
60 |
fun trace_goal ctxt rule thms t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
61 |
SMT_Replay_Methods.trace_goal ctxt (Z3_Proof.string_of_rule rule) thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
|
69593 | 63 |
fun as_prop (t as Const (\<^const_name>\<open>Trueprop\<close>, _) $ _) = t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
64 |
| as_prop t = HOLogic.mk_Trueprop t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
65 |
|
69593 | 66 |
fun dest_prop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
67 |
| dest_prop t = t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
68 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
69 |
fun dest_thm thm = dest_prop (Thm.concl_of thm) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
70 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
71 |
fun prop_tac ctxt prems = |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61466
diff
changeset
|
72 |
Method.insert_tac ctxt prems |
56816
2f3756ccba41
use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents:
56090
diff
changeset
|
73 |
THEN' SUBGOAL (fn (prop, i) => |
2f3756ccba41
use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents:
56090
diff
changeset
|
74 |
if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i |
2f3756ccba41
use internal proof-producing SAT solver for more efficient SMT proof replay
boehmes
parents:
56090
diff
changeset
|
75 |
else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
76 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
77 |
fun quant_tac ctxt = Blast.blast_tac ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
79 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
80 |
fun apply_rule ctxt t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
81 |
(case Z3_Replay_Rules.apply ctxt (SMT_Replay_Methods.certify_prop ctxt t) of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
82 |
SOME thm => thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
83 |
| NONE => raise Fail "apply_rule") |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
84 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
86 |
(*theory-lemma*) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
87 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
88 |
fun arith_th_lemma_tac ctxt prems = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
89 |
Method.insert_tac ctxt prems |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
90 |
THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def}) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
91 |
THEN' Arith_Data.arith_tac ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
92 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
93 |
fun arith_th_lemma ctxt thms t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
94 |
SMT_Replay_Methods.prove_abstract ctxt thms t arith_th_lemma_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
95 |
fold_map (SMT_Replay_Methods.abstract_arith ctxt o dest_thm) thms ##>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
96 |
SMT_Replay_Methods.abstract_arith ctxt (dest_prop t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
98 |
val _ = Theory.setup (Context.theory_map ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
99 |
SMT_Replay_Methods.add_th_lemma_method ("arith", arith_th_lemma))) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
100 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
101 |
fun th_lemma name ctxt thms = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
102 |
(case Symtab.lookup (SMT_Replay_Methods.get_th_lemma_method ctxt) name of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
103 |
SOME method => method ctxt thms |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
104 |
| NONE => replay_error ctxt "Bad theory" (Z3_Proof.Th_Lemma name) thms) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
106 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
(* truth axiom *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
fun true_axiom _ _ _ = @{thm TrueI} |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
111 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
112 |
(* modus ponens *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
113 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
114 |
fun mp _ [p, p_eq_q] _ = SMT_Replay_Methods.discharge 1 [p_eq_q, p] iffD1 |
58061 | 115 |
| mp ctxt thms t = replay_rule_error ctxt Z3_Proof.Modus_Ponens thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
117 |
val mp_oeq = mp |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
118 |
|
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 |
(* reflexivity *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
122 |
fun refl ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
124 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
(* symmetry *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
fun symm _ [thm] _ = thm RS @{thm sym} |
58061 | 128 |
| symm ctxt thms t = replay_rule_error ctxt Z3_Proof.Reflexivity thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
130 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
131 |
(* transitivity *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
132 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans})) |
58061 | 134 |
| trans ctxt thms t = replay_rule_error ctxt Z3_Proof.Transitivity thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
136 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
(* congruence *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
139 |
fun cong ctxt thms = SMT_Replay_Methods.try_provers ctxt |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
140 |
(Z3_Proof.string_of_rule Z3_Proof.Monotonicity) [ |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
141 |
("basic", SMT_Replay_Methods.cong_basic ctxt thms), |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
142 |
("full", SMT_Replay_Methods.cong_full ctxt thms)] thms |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
145 |
(* quantifier introduction *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
147 |
val quant_intro_rules = @{lemma |
67091 | 148 |
"(\<And>x. P x = Q x) ==> (\<forall>x. P x) = (\<forall>x. Q x)" |
149 |
"(\<And>x. P x = Q x) ==> (\<exists>x. P x) = (\<exists>x. Q x)" |
|
150 |
"(!!x. (\<not> P x) = Q x) \<Longrightarrow> (\<not>(\<exists>x. P x)) = (\<forall>x. Q x)" |
|
151 |
"(\<And>x. (\<not> P x) = Q x) ==> (\<not>(\<forall>x. P x)) = (\<exists>x. Q x)" |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
by fast+} |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
153 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
fun quant_intro ctxt [thm] t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
155 |
SMT_Replay_Methods.prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac ctxt (thm :: quant_intro_rules)))) |
58061 | 156 |
| quant_intro ctxt thms t = replay_rule_error ctxt Z3_Proof.Quant_Intro thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
159 |
(* distributivity of conjunctions and disjunctions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
160 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
161 |
(* TODO: there are no tests with this proof rule *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
162 |
fun distrib ctxt _ t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
163 |
SMT_Replay_Methods.prove_abstract' ctxt t prop_tac |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
164 |
(SMT_Replay_Methods.abstract_prop (dest_prop t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
165 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
166 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
167 |
(* elimination of conjunctions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
168 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
169 |
fun and_elim ctxt [thm] t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
170 |
SMT_Replay_Methods.prove_abstract ctxt [thm] t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
171 |
SMT_Replay_Methods.abstract_lit (dest_prop t) ##>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
172 |
SMT_Replay_Methods.abstract_conj (dest_thm thm) #>> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
apfst single o swap) |
58061 | 174 |
| and_elim ctxt thms t = replay_rule_error ctxt Z3_Proof.And_Elim thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
175 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
176 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
177 |
(* elimination of negated disjunctions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
178 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
179 |
fun not_or_elim ctxt [thm] t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
180 |
SMT_Replay_Methods.prove_abstract ctxt [thm] t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
181 |
SMT_Replay_Methods.abstract_lit (dest_prop t) ##>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
182 |
SMT_Replay_Methods.abstract_not SMT_Replay_Methods.abstract_disj (dest_thm thm) #>> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
apfst single o swap) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
184 |
| not_or_elim ctxt thms t = |
58061 | 185 |
replay_rule_error ctxt Z3_Proof.Not_Or_Elim thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
186 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
187 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
188 |
(* rewriting *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
189 |
|
57144
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
190 |
local |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
191 |
|
69593 | 192 |
fun dest_all (Const (\<^const_name>\<open>HOL.All\<close>, _) $ Abs (_, T, t)) nctxt = |
57144
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
193 |
let |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
194 |
val (n, nctxt') = Name.variant "" nctxt |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
195 |
val f = Free (n, T) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
196 |
val t' = Term.subst_bound (f, t) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
197 |
in dest_all t' nctxt' |>> cons f end |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
198 |
| dest_all t _ = ([], t) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
199 |
|
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
200 |
fun dest_alls t = |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
201 |
let |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
202 |
val nctxt = Name.make_context (Term.add_free_names t []) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
203 |
val (lhs, rhs) = HOLogic.dest_eq (dest_prop t) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
204 |
val (ls, lhs') = dest_all lhs nctxt |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
205 |
val (rs, rhs') = dest_all rhs nctxt |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
206 |
in |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
207 |
if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs'))) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
208 |
else NONE |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
209 |
end |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
210 |
|
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
211 |
fun forall_intr ctxt t thm = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59617
diff
changeset
|
212 |
let val ct = Thm.cterm_of ctxt t |
57144
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
213 |
in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
214 |
|
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
215 |
in |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
216 |
|
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
217 |
fun focus_eq f ctxt t = |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
218 |
(case dest_alls t of |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
219 |
NONE => f ctxt t |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
220 |
| SOME (vs, t') => fold (forall_intr ctxt) vs (f ctxt t')) |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
221 |
|
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
222 |
end |
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
223 |
|
69593 | 224 |
fun abstract_eq f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2) = |
57144
1d12e22e7caf
more complete proof replay for Z3: support universally quantified rewrite steps
boehmes
parents:
56816
diff
changeset
|
225 |
f t1 ##>> f t2 #>> HOLogic.mk_eq |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
226 |
| abstract_eq _ t = SMT_Replay_Methods.abstract_term t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
227 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
228 |
fun prove_prop_rewrite ctxt t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
229 |
SMT_Replay_Methods.prove_abstract' ctxt t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
230 |
abstract_eq SMT_Replay_Methods.abstract_prop (dest_prop t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
231 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
232 |
fun arith_rewrite_tac ctxt _ = |
66692 | 233 |
let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in |
234 |
(TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac |
|
235 |
ORELSE' backup_tac |
|
236 |
end |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
237 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
238 |
fun prove_arith_rewrite ctxt t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
239 |
SMT_Replay_Methods.prove_abstract' ctxt t arith_rewrite_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
240 |
abstract_eq (SMT_Replay_Methods.abstract_arith ctxt) (dest_prop t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
241 |
|
58140
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
242 |
val lift_ite_thm = @{thm HOL.if_distrib} RS @{thm eq_reflection} |
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
243 |
|
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
244 |
fun ternary_conv cv = Conv.combination_conv (Conv.binop_conv cv) cv |
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
245 |
|
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
246 |
fun if_context_conv ctxt ct = |
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
247 |
(case Thm.term_of ct of |
69593 | 248 |
Const (\<^const_name>\<open>HOL.If\<close>, _) $ _ $ _ $ _ => |
58140
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
249 |
ternary_conv (if_context_conv ctxt) |
69593 | 250 |
| _ $ (Const (\<^const_name>\<open>HOL.If\<close>, _) $ _ $ _ $ _) => |
58140
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
251 |
Conv.rewr_conv lift_ite_thm then_conv ternary_conv (if_context_conv ctxt) |
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
252 |
| _ => Conv.sub_conv (Conv.top_sweep_conv if_context_conv) ctxt) ct |
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
253 |
|
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
254 |
fun lift_ite_rewrite ctxt t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
255 |
SMT_Replay_Methods.prove ctxt t (fn ctxt => |
58140
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
256 |
CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt))) |
60752 | 257 |
THEN' resolve_tac ctxt @{thms refl}) |
58140
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
258 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
259 |
fun prove_conj_disj_perm ctxt t = SMT_Replay_Methods.prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac |
59381
de4218223e00
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
boehmes
parents:
58957
diff
changeset
|
260 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
261 |
fun rewrite ctxt _ = SMT_Replay_Methods.try_provers ctxt |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
262 |
(Z3_Proof.string_of_rule Z3_Proof.Rewrite) [ |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
263 |
("rules", apply_rule ctxt), |
59381
de4218223e00
more efficient Z3 proof reconstruction for rewrite steps with conjunctions and disjunctions, similar to Old_SMT
boehmes
parents:
58957
diff
changeset
|
264 |
("conj_disj_perm", prove_conj_disj_perm ctxt), |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
265 |
("prop_rewrite", prove_prop_rewrite ctxt), |
58140
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
266 |
("arith_rewrite", focus_eq prove_arith_rewrite ctxt), |
b4aa77aef6a8
replay Z3 rewrite steps that lift if-then-else expressions
boehmes
parents:
58061
diff
changeset
|
267 |
("if_rewrite", lift_ite_rewrite ctxt)] [] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
268 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
269 |
fun rewrite_star ctxt = rewrite ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
270 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
271 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
272 |
(* pulling quantifiers *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
273 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
274 |
fun pull_quant ctxt _ t = SMT_Replay_Methods.prove ctxt t quant_tac |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
275 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
276 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
277 |
(* pushing quantifiers *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
278 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
279 |
fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
280 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
281 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
282 |
(* elimination of unused bound variables *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
283 |
|
67091 | 284 |
val elim_all = @{lemma "P = Q \<Longrightarrow> (\<forall>x. P) = Q" by fast} |
285 |
val elim_ex = @{lemma "P = Q \<Longrightarrow> (\<exists>x. P) = Q" by fast} |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
286 |
|
58957 | 287 |
fun elim_unused_tac ctxt i st = ( |
288 |
match_tac ctxt [@{thm refl}] |
|
289 |
ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
290 |
ORELSE' ( |
58957 | 291 |
match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}] |
292 |
THEN' elim_unused_tac ctxt)) i st |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
293 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
294 |
fun elim_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t elim_unused_tac |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
295 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
296 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
297 |
(* destructive equality resolution *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
298 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
299 |
fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
300 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
301 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
302 |
(* quantifier instantiation *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
303 |
|
67091 | 304 |
val quant_inst_rule = @{lemma "\<not>P x \<or> Q ==> \<not>(\<forall>x. P x) \<or> Q" by fast} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
305 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
306 |
fun quant_inst ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => |
60752 | 307 |
REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule]) |
308 |
THEN' resolve_tac ctxt @{thms excluded_middle}) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
309 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
310 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
311 |
(* propositional lemma *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
312 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
313 |
exception LEMMA of unit |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
314 |
|
67091 | 315 |
val intro_hyp_rule1 = @{lemma "(\<not>P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" by fast} |
316 |
val intro_hyp_rule2 = @{lemma "(P \<Longrightarrow> Q) \<Longrightarrow> \<not>P \<or> Q" by fast} |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
317 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
318 |
fun norm_lemma thm = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
319 |
(thm COMP_INCR intro_hyp_rule1) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
320 |
handle THM _ => thm COMP_INCR intro_hyp_rule2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
321 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
322 |
fun negated_prop (@{const HOL.Not} $ t) = HOLogic.mk_Trueprop t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
323 |
| negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
324 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
325 |
fun intro_hyps tab (t as @{const HOL.disj} $ t1 $ t2) cx = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
326 |
lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
327 |
| intro_hyps tab t cx = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
328 |
lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
329 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
330 |
and lookup_intro_hyps tab t f (cx as (thm, terms)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
331 |
(case Termtab.lookup tab (negated_prop t) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
332 |
NONE => f cx |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
333 |
| SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
334 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
335 |
fun lemma ctxt (thms as [thm]) t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
336 |
(let |
60949 | 337 |
val tab = Termtab.make (map (`Thm.term_of) (Thm.chyps_of thm)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
338 |
val (thm', terms) = intro_hyps tab (dest_prop t) (thm, []) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
339 |
in |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
340 |
SMT_Replay_Methods.prove_abstract ctxt [thm'] t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
341 |
fold (snd oo SMT_Replay_Methods.abstract_lit) terms #> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
342 |
SMT_Replay_Methods.abstract_disj (dest_thm thm') #>> single ##>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
343 |
SMT_Replay_Methods.abstract_disj (dest_prop t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
344 |
end |
58061 | 345 |
handle LEMMA () => replay_error ctxt "Bad proof state" Z3_Proof.Lemma thms t) |
346 |
| lemma ctxt thms t = replay_rule_error ctxt Z3_Proof.Lemma thms t |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
347 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
348 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
349 |
(* unit resolution *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
350 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
351 |
fun unit_res ctxt thms t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
352 |
SMT_Replay_Methods.prove_abstract ctxt thms t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
353 |
fold_map (SMT_Replay_Methods.abstract_unit o dest_thm) thms ##>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
354 |
SMT_Replay_Methods.abstract_unit (dest_prop t) #>> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
355 |
(fn (prems, concl) => (prems, concl))) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
356 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
357 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
358 |
(* iff-true *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
359 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
360 |
val iff_true_rule = @{lemma "P ==> P = True" by fast} |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
361 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
362 |
fun iff_true _ [thm] _ = thm RS iff_true_rule |
58061 | 363 |
| iff_true ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_True thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
364 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
365 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
366 |
(* iff-false *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
367 |
|
67091 | 368 |
val iff_false_rule = @{lemma "\<not>P \<Longrightarrow> P = False" by fast} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
369 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
370 |
fun iff_false _ [thm] _ = thm RS iff_false_rule |
58061 | 371 |
| iff_false ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_False thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
372 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
373 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
374 |
(* commutativity *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
375 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
376 |
fun comm ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm eq_commute} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
377 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
378 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
379 |
(* definitional axioms *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
380 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
381 |
fun def_axiom_disj ctxt t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
382 |
(case dest_prop t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
383 |
@{const HOL.disj} $ u1 $ u2 => |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
384 |
SMT_Replay_Methods.prove_abstract' ctxt t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
385 |
SMT_Replay_Methods.abstract_prop u2 ##>> SMT_Replay_Methods.abstract_prop u1 #>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
386 |
HOLogic.mk_disj o swap) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
387 |
| u => SMT_Replay_Methods.prove_abstract' ctxt t prop_tac (SMT_Replay_Methods.abstract_prop u)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
388 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
389 |
fun def_axiom ctxt _ = SMT_Replay_Methods.try_provers ctxt |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
390 |
(Z3_Proof.string_of_rule Z3_Proof.Def_Axiom) [ |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
391 |
("rules", apply_rule ctxt), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
392 |
("disj", def_axiom_disj ctxt)] [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
393 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
394 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
395 |
(* application of definitions *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
396 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
397 |
fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *) |
58061 | 398 |
| apply_def ctxt thms t = replay_rule_error ctxt Z3_Proof.Apply_Def thms t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
399 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
400 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
401 |
(* iff-oeq *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
402 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
403 |
fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
404 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
405 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
406 |
(* negation normal form *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
407 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
408 |
fun nnf_prop ctxt thms t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
409 |
SMT_Replay_Methods.prove_abstract ctxt thms t prop_tac ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
410 |
fold_map (SMT_Replay_Methods.abstract_prop o dest_thm) thms ##>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
411 |
SMT_Replay_Methods.abstract_prop (dest_prop t)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
412 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
67091
diff
changeset
|
413 |
fun nnf ctxt rule thms = SMT_Replay_Methods.try_provers ctxt (Z3_Proof.string_of_rule rule) [ |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
414 |
("prop", nnf_prop ctxt thms), |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
415 |
("quant", quant_intro ctxt [hd thms])] thms |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
416 |
|
58061 | 417 |
fun nnf_pos ctxt = nnf ctxt Z3_Proof.Nnf_Pos |
418 |
fun nnf_neg ctxt = nnf ctxt Z3_Proof.Nnf_Neg |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
419 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
420 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
421 |
(* mapping of rules to methods *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
422 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
423 |
fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
424 |
fun assumed rule ctxt = replay_error ctxt "Assumed" rule |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
425 |
|
58061 | 426 |
fun choose Z3_Proof.True_Axiom = true_axiom |
427 |
| choose (r as Z3_Proof.Asserted) = assumed r |
|
428 |
| choose (r as Z3_Proof.Goal) = assumed r |
|
429 |
| choose Z3_Proof.Modus_Ponens = mp |
|
430 |
| choose Z3_Proof.Reflexivity = refl |
|
431 |
| choose Z3_Proof.Symmetry = symm |
|
432 |
| choose Z3_Proof.Transitivity = trans |
|
433 |
| choose (r as Z3_Proof.Transitivity_Star) = unsupported r |
|
434 |
| choose Z3_Proof.Monotonicity = cong |
|
435 |
| choose Z3_Proof.Quant_Intro = quant_intro |
|
436 |
| choose Z3_Proof.Distributivity = distrib |
|
437 |
| choose Z3_Proof.And_Elim = and_elim |
|
438 |
| choose Z3_Proof.Not_Or_Elim = not_or_elim |
|
439 |
| choose Z3_Proof.Rewrite = rewrite |
|
440 |
| choose Z3_Proof.Rewrite_Star = rewrite_star |
|
441 |
| choose Z3_Proof.Pull_Quant = pull_quant |
|
442 |
| choose (r as Z3_Proof.Pull_Quant_Star) = unsupported r |
|
443 |
| choose Z3_Proof.Push_Quant = push_quant |
|
444 |
| choose Z3_Proof.Elim_Unused_Vars = elim_unused |
|
445 |
| choose Z3_Proof.Dest_Eq_Res = dest_eq_res |
|
446 |
| choose Z3_Proof.Quant_Inst = quant_inst |
|
447 |
| choose (r as Z3_Proof.Hypothesis) = assumed r |
|
448 |
| choose Z3_Proof.Lemma = lemma |
|
449 |
| choose Z3_Proof.Unit_Resolution = unit_res |
|
450 |
| choose Z3_Proof.Iff_True = iff_true |
|
451 |
| choose Z3_Proof.Iff_False = iff_false |
|
452 |
| choose Z3_Proof.Commutativity = comm |
|
453 |
| choose Z3_Proof.Def_Axiom = def_axiom |
|
454 |
| choose (r as Z3_Proof.Intro_Def) = assumed r |
|
455 |
| choose Z3_Proof.Apply_Def = apply_def |
|
456 |
| choose Z3_Proof.Iff_Oeq = iff_oeq |
|
457 |
| choose Z3_Proof.Nnf_Pos = nnf_pos |
|
458 |
| choose Z3_Proof.Nnf_Neg = nnf_neg |
|
459 |
| choose (r as Z3_Proof.Nnf_Star) = unsupported r |
|
460 |
| choose (r as Z3_Proof.Cnf_Star) = unsupported r |
|
461 |
| choose (r as Z3_Proof.Skolemize) = assumed r |
|
462 |
| choose Z3_Proof.Modus_Ponens_Oeq = mp_oeq |
|
463 |
| choose (Z3_Proof.Th_Lemma name) = th_lemma name |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
464 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
465 |
fun with_tracing rule method ctxt thms t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
466 |
let val _ = trace_goal ctxt rule thms t |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
467 |
in method ctxt thms t end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
468 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
469 |
fun method_for rule = with_tracing rule (choose rule) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
470 |
|
57229 | 471 |
end; |