author | wenzelm |
Wed, 04 Oct 2017 12:00:53 +0200 | |
changeset 66787 | 64b47495676d |
parent 66298 | 5ff9fe3fee66 |
child 67149 | e61557884799 |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/smt_normalize.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 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
4 |
Normalization steps on theorems required by SMT solvers. |
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 SMT_NORMALIZE = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
8 |
sig |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
9 |
val drop_fact_warning: Proof.context -> thm -> unit |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
10 |
val atomize_conv: Proof.context -> conv |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
11 |
|
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
12 |
val special_quant_table: (string * thm) list |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
13 |
val case_bool_entry: string * thm |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
14 |
val abs_min_max_table: (string * thm) list |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
15 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
16 |
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
58061 | 17 |
val add_extra_norm: SMT_Util.class * extra_norm -> Context.generic -> Context.generic |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
18 |
val normalize: Proof.context -> thm list -> (int * thm) list |
57229 | 19 |
end; |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
20 |
|
58061 | 21 |
structure SMT_Normalize: SMT_NORMALIZE = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
22 |
struct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
23 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
24 |
fun drop_fact_warning ctxt = |
58061 | 25 |
SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o |
61268 | 26 |
Thm.string_of_thm ctxt) |
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 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
29 |
(* general theorem normalizations *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
30 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
31 |
(** instantiate elimination rules **) |
57230 | 32 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
33 |
local |
59632 | 34 |
val (cpfalse, cfalse) = `SMT_Util.mk_cprop (Thm.cterm_of @{context} @{const False}) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
35 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
36 |
fun inst f ct thm = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
37 |
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm)) |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59632
diff
changeset
|
38 |
in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
39 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
40 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
41 |
fun instantiate_elim thm = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
42 |
(case Thm.concl_of thm of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
43 |
@{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
44 |
| Var _ => inst I cpfalse thm |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
45 |
| _ => thm) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
46 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
47 |
end |
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 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
50 |
(** normalize definitions **) |
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 |
fun norm_def thm = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
53 |
(case Thm.prop_of thm of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
54 |
@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
55 |
norm_def (thm RS @{thm fun_cong}) |
56245 | 56 |
| Const (@{const_name Pure.eq}, _) $ _ $ Abs _ => norm_def (thm RS @{thm meta_eq_to_obj_eq}) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
57 |
| _ => thm) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
58 |
|
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 |
(** atomization **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
61 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
62 |
fun atomize_conv ctxt ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
63 |
(case Thm.term_of ct of |
56245 | 64 |
@{const Pure.imp} $ _ $ _ => |
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56100
diff
changeset
|
65 |
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp} |
56245 | 66 |
| Const (@{const_name Pure.eq}, _) $ _ $ _ => |
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56100
diff
changeset
|
67 |
Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq} |
56245 | 68 |
| Const (@{const_name Pure.all}, _) $ Abs _ => |
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56100
diff
changeset
|
69 |
Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
70 |
| _ => Conv.all_conv) ct |
61033
fd7fe96ca7b9
generate proper error instead of exception if goal cannot be atomized
blanchet
parents:
60642
diff
changeset
|
71 |
handle CTERM _ => Conv.all_conv ct |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
72 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
73 |
val setup_atomize = |
58061 | 74 |
fold SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp}, @{const_name Pure.eq}, |
56245 | 75 |
@{const_name Pure.all}, @{const_name Trueprop}] |
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 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
78 |
(** unfold special quantifiers **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
79 |
|
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
80 |
val special_quant_table = [ |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
81 |
(@{const_name Ex1}, @{thm Ex1_def_raw}), |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
82 |
(@{const_name Ball}, @{thm Ball_def_raw}), |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
83 |
(@{const_name Bex}, @{thm Bex_def_raw})] |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
84 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
85 |
local |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
86 |
fun special_quant (Const (n, _)) = AList.lookup (op =) special_quant_table n |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
87 |
| special_quant _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
88 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
89 |
fun special_quant_conv _ ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
90 |
(case special_quant (Thm.term_of ct) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
91 |
SOME thm => Conv.rewr_conv thm |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
92 |
| NONE => Conv.all_conv) ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
93 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
94 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
95 |
fun unfold_special_quants_conv ctxt = |
58061 | 96 |
SMT_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
97 |
|
58061 | 98 |
val setup_unfolded_quants = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) special_quant_table |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
99 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
100 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
101 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
102 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
103 |
(** trigger inference **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
104 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
105 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
106 |
(*** check trigger syntax ***) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
107 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
108 |
fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
109 |
| dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
110 |
| dest_trigger _ = NONE |
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 |
fun eq_list [] = false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
113 |
| eq_list (b :: bs) = forall (equal b) bs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
114 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
115 |
fun proper_trigger t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
116 |
t |
58061 | 117 |
|> these o try SMT_Util.dest_symb_list |
118 |
|> map (map_filter dest_trigger o these o try SMT_Util.dest_symb_list) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
119 |
|> (fn [] => false | bss => forall eq_list bss) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
120 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
121 |
fun proper_quant inside f t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
122 |
(case t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
123 |
Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
124 |
| Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
125 |
| @{const trigger} $ p $ u => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
126 |
(if inside then f p else false) andalso proper_quant false f u |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
127 |
| Abs (_, _, u) => proper_quant false f u |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
128 |
| u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
129 |
| _ => true) |
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 |
fun check_trigger_error ctxt t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
132 |
error ("SMT triggers must only occur under quantifier and multipatterns " ^ |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
133 |
"must have the same kind: " ^ Syntax.string_of_term ctxt t) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
134 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
135 |
fun check_trigger_conv ctxt ct = |
58061 | 136 |
if proper_quant false proper_trigger (SMT_Util.term_of ct) then Conv.all_conv ct |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
137 |
else check_trigger_error ctxt (Thm.term_of ct) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
138 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
139 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
140 |
(*** infer simple triggers ***) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
141 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
142 |
fun dest_cond_eq ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
143 |
(case Thm.term_of ct of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
144 |
Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
145 |
| @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
146 |
| _ => raise CTERM ("no equation", [ct])) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
147 |
|
58132 | 148 |
fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
149 |
| get_constrs _ _ = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
150 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
151 |
fun is_constr thy (n, T) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
152 |
let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
153 |
in can (the o find_first match o get_constrs thy o Term.body_type) T end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
154 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
155 |
fun is_constr_pat thy t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
156 |
(case Term.strip_comb t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
157 |
(Free _, []) => true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
158 |
| (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
159 |
| _ => false) |
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 |
fun is_simp_lhs ctxt t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
162 |
(case Term.strip_comb t of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
163 |
(Const c, ts as _ :: _) => |
58061 | 164 |
not (SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
165 |
forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
166 |
| _ => false) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
167 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
168 |
fun has_all_vars vs t = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
169 |
subset (op aconv) (vs, map Free (Term.add_frees t [])) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
170 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
171 |
fun minimal_pats vs ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
172 |
if has_all_vars vs (Thm.term_of ct) then |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
173 |
(case Thm.term_of ct of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
174 |
_ $ _ => |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58132
diff
changeset
|
175 |
(case apply2 (minimal_pats vs) (Thm.dest_comb ct) of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
176 |
([], []) => [[ct]] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
177 |
| (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss') |
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 |
else [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
180 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
181 |
fun proper_mpat _ _ _ [] = false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
182 |
| proper_mpat thy gen u cts = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
183 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
184 |
val tps = (op ~~) (`gen (map Thm.term_of cts)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
185 |
fun some_match u = tps |> exists (fn (t', t) => |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
186 |
Pattern.matches thy (t', u) andalso not (t aconv u)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
187 |
in not (Term.exists_subterm some_match u) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
188 |
|
58061 | 189 |
val pat = SMT_Util.mk_const_pat @{theory} @{const_name pat} SMT_Util.destT1 |
190 |
fun mk_pat ct = Thm.apply (SMT_Util.instT' ct pat) ct |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
191 |
|
57230 | 192 |
fun mk_clist T = |
59632 | 193 |
apply2 (Thm.cterm_of @{context}) (SMT_Util.symb_cons_const T, SMT_Util.symb_nil_const T) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
194 |
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil |
57230 | 195 |
val mk_pat_list = mk_list (mk_clist @{typ pattern}) |
196 |
val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"}) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
197 |
fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
198 |
|
57230 | 199 |
val trigger_eq = mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
200 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
201 |
fun insert_trigger_conv [] ct = Conv.all_conv ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
202 |
| insert_trigger_conv ctss ct = |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59632
diff
changeset
|
203 |
let |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59632
diff
changeset
|
204 |
val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59632
diff
changeset
|
205 |
val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)] |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59632
diff
changeset
|
206 |
in Thm.instantiate ([], inst) trigger_eq end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
207 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
208 |
fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
209 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
210 |
val (lhs, rhs) = dest_cond_eq ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
211 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
212 |
val vs = map Thm.term_of cvs |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
213 |
val thy = Proof_Context.theory_of ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
214 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
215 |
fun get_mpats ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
216 |
if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
217 |
else [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
218 |
val gen = Variable.export_terms ctxt outer_ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
219 |
val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
220 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
221 |
in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
222 |
|
57230 | 223 |
fun has_trigger (@{const trigger} $ _ $ _) = true |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
224 |
| has_trigger _ = false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
225 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
226 |
fun try_trigger_conv cv ct = |
58061 | 227 |
if SMT_Util.under_quant has_trigger (SMT_Util.term_of ct) then Conv.all_conv ct |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
228 |
else Conv.try_conv cv ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
229 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
230 |
fun infer_trigger_conv ctxt = |
58061 | 231 |
if Config.get ctxt SMT_Config.infer_triggers then |
232 |
try_trigger_conv (SMT_Util.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
233 |
else Conv.all_conv |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
234 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
235 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
236 |
fun trigger_conv ctxt = |
58061 | 237 |
SMT_Util.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
238 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
239 |
val setup_trigger = |
58061 | 240 |
fold SMT_Builtin.add_builtin_fun_ext'' |
57230 | 241 |
[@{const_name pat}, @{const_name nopat}, @{const_name trigger}] |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
242 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
243 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
244 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
245 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
246 |
(** combined general normalizations **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
247 |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
248 |
fun gen_normalize1_conv ctxt = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
249 |
atomize_conv ctxt then_conv |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
250 |
unfold_special_quants_conv ctxt then_conv |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
251 |
Thm.beta_conversion true then_conv |
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
252 |
trigger_conv ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
253 |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
254 |
fun gen_normalize1 ctxt = |
56107 | 255 |
instantiate_elim #> |
256 |
norm_def #> |
|
257 |
Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion) #> |
|
258 |
Drule.forall_intr_vars #> |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
259 |
Conv.fconv_rule (gen_normalize1_conv ctxt) #> |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
260 |
(* Z3 4.3.1 silently normalizes "P --> Q --> R" to "P & Q --> R" *) |
56107 | 261 |
Raw_Simplifier.rewrite_rule ctxt @{thms HOL.imp_conjL[symmetric, THEN eq_reflection]} |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
262 |
|
57165
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
263 |
fun gen_norm1_safe ctxt (i, thm) = |
7b1bf424ec5f
removed SMT weights -- their impact was very inconclusive anyway
blanchet
parents:
56981
diff
changeset
|
264 |
(case try (gen_normalize1 ctxt) thm of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
265 |
SOME thm' => SOME (i, thm') |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
266 |
| NONE => (drop_fact_warning ctxt thm; NONE)) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
267 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
268 |
fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
269 |
|
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 |
(* unfolding of definitions and theory-specific rewritings *) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
272 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
273 |
fun expand_head_conv cv ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
274 |
(case Thm.term_of ct of |
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 |
Conv.fun_conv (expand_head_conv cv) then_conv |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
277 |
Conv.try_conv (Thm.beta_conversion false) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
278 |
| _ => cv) ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
279 |
|
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 |
(** rewrite bool case expressions as if expressions **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
282 |
|
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
283 |
val case_bool_entry = (@{const_name "bool.case_bool"}, @{thm case_bool_if}) |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
284 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
285 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
286 |
fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
287 |
| is_case_bool _ = false |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
288 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
289 |
fun unfold_conv _ = |
58061 | 290 |
SMT_Util.if_true_conv (is_case_bool o Term.head_of) |
56103
6689512f3710
move lemmas to theory file, towards textual proof reconstruction
blanchet
parents:
56100
diff
changeset
|
291 |
(expand_head_conv (Conv.rewr_conv @{thm case_bool_if})) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
292 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
293 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
294 |
fun rewrite_case_bool_conv ctxt = |
58061 | 295 |
SMT_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
296 |
|
58061 | 297 |
val setup_case_bool = SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"} |
56078
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 |
end |
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 |
(** unfold abs, min and max **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
303 |
|
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
304 |
val abs_min_max_table = [ |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
305 |
(@{const_name min}, @{thm min_def_raw}), |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
306 |
(@{const_name max}, @{thm max_def_raw}), |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
307 |
(@{const_name abs}, @{thm abs_if_raw})] |
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
308 |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
309 |
local |
56100 | 310 |
fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) = |
56981
3ef45ce002b5
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
blanchet
parents:
56245
diff
changeset
|
311 |
(case AList.lookup (op =) abs_min_max_table n of |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
312 |
NONE => NONE |
58061 | 313 |
| SOME thm => if SMT_Builtin.is_builtin_typ_ext ctxt T then SOME thm else NONE) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
314 |
| abs_min_max _ _ = NONE |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
315 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
316 |
fun unfold_amm_conv ctxt ct = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
317 |
(case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
318 |
SOME thm => expand_head_conv (Conv.rewr_conv thm) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
319 |
| NONE => Conv.all_conv) ct |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
320 |
in |
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 unfold_abs_min_max_conv ctxt = |
58061 | 323 |
SMT_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt) |
57230 | 324 |
|
58061 | 325 |
val setup_abs_min_max = fold (SMT_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
326 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
327 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
328 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
329 |
|
66298 | 330 |
(** embedding of standard natural number operations into integer operations **) |
331 |
||
332 |
local |
|
333 |
val nat_embedding = @{thms nat_int' int_nat_nneg int_nat_neg} |
|
334 |
||
335 |
val simple_nat_ops = [ |
|
336 |
@{const less (nat)}, @{const less_eq (nat)}, |
|
337 |
@{const Suc}, @{const plus (nat)}, @{const minus (nat)}] |
|
338 |
||
339 |
val mult_nat_ops = |
|
340 |
[@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}] |
|
341 |
||
342 |
val nat_ops = simple_nat_ops @ mult_nat_ops |
|
343 |
||
344 |
val nat_consts = nat_ops @ [@{const numeral (nat)}, |
|
345 |
@{const zero_class.zero (nat)}, @{const one_class.one (nat)}] |
|
346 |
||
347 |
val nat_int_coercions = [@{const of_nat (int)}, @{const nat}] |
|
348 |
||
349 |
val builtin_nat_ops = nat_int_coercions @ simple_nat_ops |
|
350 |
||
351 |
val is_nat_const = member (op aconv) nat_consts |
|
352 |
||
353 |
fun is_nat_const' @{const of_nat (int)} = true |
|
354 |
| is_nat_const' t = is_nat_const t |
|
355 |
||
356 |
val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int |
|
357 |
nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int |
|
358 |
nat_div_as_int nat_mod_as_int} |
|
359 |
||
360 |
val ints = map mk_meta_eq @{thms of_nat_0 of_nat_1 int_Suc int_plus int_minus of_nat_mult zdiv_int |
|
361 |
zmod_int} |
|
362 |
val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp} |
|
363 |
||
364 |
fun mk_number_eq ctxt i lhs = |
|
365 |
let |
|
366 |
val eq = SMT_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i) |
|
367 |
val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms of_nat_numeral} |
|
368 |
val tac = HEADGOAL (Simplifier.simp_tac ctxt') |
|
369 |
in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end |
|
370 |
||
371 |
fun ite_conv cv1 cv2 = |
|
372 |
Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2 |
|
373 |
||
374 |
fun int_conv ctxt ct = |
|
375 |
(case Thm.term_of ct of |
|
376 |
@{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) => |
|
377 |
Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct) |
|
378 |
| @{const of_nat (int)} $ _ => |
|
379 |
(Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv |
|
380 |
(Conv.rewr_conv int_if then_conv |
|
381 |
ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv |
|
382 |
Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt |
|
383 |
| _ => Conv.no_conv) ct |
|
384 |
||
385 |
and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt |
|
386 |
||
387 |
and expand_conv ctxt = |
|
388 |
SMT_Util.if_conv (is_nat_const o Term.head_of) |
|
389 |
(expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt) |
|
390 |
||
391 |
and nat_conv ctxt = SMT_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt) |
|
392 |
||
393 |
val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions) |
|
394 |
in |
|
395 |
||
396 |
val nat_as_int_conv = nat_conv |
|
397 |
||
398 |
fun add_nat_embedding thms = |
|
399 |
if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding) else (thms, []) |
|
400 |
||
401 |
val setup_nat_as_int = |
|
402 |
SMT_Builtin.add_builtin_typ_ext (@{typ nat}, |
|
403 |
fn ctxt => K (Config.get ctxt SMT_Config.nat_as_int)) #> |
|
404 |
fold (SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops |
|
405 |
||
406 |
end |
|
407 |
||
408 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
409 |
(** normalize numerals **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
410 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
411 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
412 |
(* |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
413 |
rewrite Numeral1 into 1 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
414 |
rewrite - 0 into 0 |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
415 |
*) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
416 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
417 |
fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
418 |
true |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
419 |
| is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
420 |
true |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57230
diff
changeset
|
421 |
| is_irregular_number _ = false |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
422 |
|
58061 | 423 |
fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
424 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
425 |
val proper_num_ss = |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57230
diff
changeset
|
426 |
simpset_of (put_simpset HOL_ss @{context} addsimps @{thms Num.numeral_One minus_zero}) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
427 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
428 |
fun norm_num_conv ctxt = |
58061 | 429 |
SMT_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) |
56090 | 430 |
Conv.no_conv |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
431 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
432 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
433 |
fun normalize_numerals_conv ctxt = |
58061 | 434 |
SMT_Util.if_exists_conv (is_strange_number ctxt) (Conv.top_sweep_conv norm_num_conv ctxt) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
435 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
436 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
437 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
438 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
439 |
(** combined unfoldings and rewritings **) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
440 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
441 |
fun burrow_ids f ithms = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
442 |
let |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
443 |
val (is, thms) = split_list ithms |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
444 |
val (thms', extra_thms) = f thms |
56106 | 445 |
in (is ~~ thms') @ map (pair ~1) extra_thms end |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
446 |
|
66298 | 447 |
fun unfold_conv ctxt = |
448 |
rewrite_case_bool_conv ctxt then_conv |
|
449 |
unfold_abs_min_max_conv ctxt then_conv |
|
450 |
(if Config.get ctxt SMT_Config.nat_as_int then nat_as_int_conv ctxt |
|
451 |
else Conv.all_conv) then_conv |
|
452 |
Thm.beta_conversion true |
|
453 |
||
454 |
fun unfold_polymorph ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt))) |
|
455 |
fun unfold_monomorph ctxt = |
|
456 |
map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) |
|
457 |
#> Config.get ctxt SMT_Config.nat_as_int ? burrow_ids add_nat_embedding |
|
458 |
||
459 |
||
460 |
(* overall normalization *) |
|
461 |
||
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
462 |
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
463 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
464 |
structure Extra_Norms = Generic_Data |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
465 |
( |
58061 | 466 |
type T = extra_norm SMT_Util.dict |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
467 |
val empty = [] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
468 |
val extend = I |
58061 | 469 |
fun merge data = SMT_Util.dict_merge fst data |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
470 |
) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
471 |
|
58061 | 472 |
fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT_Util.dict_update (cs, norm)) |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
473 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
474 |
fun apply_extra_norms ctxt ithms = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
475 |
let |
58061 | 476 |
val cs = SMT_Config.solver_class_of ctxt |
477 |
val es = SMT_Util.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
478 |
in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
479 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
480 |
local |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
481 |
val ignored = member (op =) [@{const_name All}, @{const_name Ex}, |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
482 |
@{const_name Let}, @{const_name If}, @{const_name HOL.eq}] |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
483 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
484 |
val schematic_consts_of = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
485 |
let |
57230 | 486 |
fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
487 |
| collect (t $ u) = collect t #> collect u |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
488 |
| collect (Abs (_, _, t)) = collect t |
57230 | 489 |
| collect (t as Const (n, _)) = |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
490 |
if not (ignored n) then Monomorph.add_schematic_consts_of t else I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
491 |
| collect _ = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
492 |
and collect_trigger t = |
58061 | 493 |
let val dest = these o try SMT_Util.dest_symb_list |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
494 |
in fold (fold collect_pat o dest) (dest t) end |
57230 | 495 |
and collect_pat (Const (@{const_name pat}, _) $ t) = collect t |
496 |
| collect_pat (Const (@{const_name nopat}, _) $ t) = collect t |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
497 |
| collect_pat _ = I |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
498 |
in (fn t => collect t Symtab.empty) end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
499 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
500 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
501 |
fun monomorph ctxt xthms = |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
502 |
let val (xs, thms) = split_list xthms |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
503 |
in |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
504 |
map (pair 1) thms |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
505 |
|> Monomorph.monomorph schematic_consts_of ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
506 |
|> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
507 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
508 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
509 |
end |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
510 |
|
56106 | 511 |
fun normalize ctxt wthms = |
512 |
wthms |
|
513 |
|> map_index I |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
514 |
|> gen_normalize ctxt |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57230
diff
changeset
|
515 |
|> unfold_polymorph ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
516 |
|> monomorph ctxt |
57696
fb71c6f100f8
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
blanchet
parents:
57230
diff
changeset
|
517 |
|> unfold_monomorph ctxt |
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
518 |
|> apply_extra_norms ctxt |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
519 |
|
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
520 |
val _ = Theory.setup (Context.theory_map ( |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
521 |
setup_atomize #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
522 |
setup_unfolded_quants #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
523 |
setup_trigger #> |
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
524 |
setup_case_bool #> |
66298 | 525 |
setup_abs_min_max #> |
526 |
setup_nat_as_int)) |
|
56078
624faeda77b5
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet
parents:
diff
changeset
|
527 |
|
57229 | 528 |
end; |