boehmes@36887
|
1 |
(* Title: HOL/SMT/Tools/z3_proof_tools.ML
|
boehmes@36887
|
2 |
Author: Sascha Boehme, TU Muenchen
|
boehmes@36887
|
3 |
|
boehmes@36887
|
4 |
Helper functions required for Z3 proof reconstruction.
|
boehmes@36887
|
5 |
*)
|
boehmes@36887
|
6 |
|
boehmes@36887
|
7 |
signature Z3_PROOF_TOOLS =
|
boehmes@36887
|
8 |
sig
|
boehmes@36887
|
9 |
(* accessing and modifying terms *)
|
boehmes@36887
|
10 |
val term_of: cterm -> term
|
boehmes@36887
|
11 |
val prop_of: thm -> term
|
boehmes@36887
|
12 |
val mk_prop: cterm -> cterm
|
boehmes@36887
|
13 |
val as_meta_eq: cterm -> cterm
|
boehmes@36887
|
14 |
|
boehmes@36887
|
15 |
(* theorem nets *)
|
boehmes@36887
|
16 |
val thm_net_of: thm list -> thm Net.net
|
boehmes@36887
|
17 |
val net_instance: thm Net.net -> cterm -> thm option
|
boehmes@36887
|
18 |
|
boehmes@36887
|
19 |
(* proof combinators *)
|
boehmes@36887
|
20 |
val under_assumption: (thm -> thm) -> cterm -> thm
|
boehmes@36887
|
21 |
val with_conv: conv -> (cterm -> thm) -> cterm -> thm
|
boehmes@36887
|
22 |
val discharge: thm -> thm -> thm
|
boehmes@36887
|
23 |
val varify: string list -> thm -> thm
|
boehmes@36887
|
24 |
val unfold_eqs: Proof.context -> thm list -> conv
|
boehmes@36887
|
25 |
val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
|
boehmes@36887
|
26 |
val by_tac: (int -> tactic) -> cterm -> thm
|
boehmes@36888
|
27 |
val make_hyp_def: thm -> Proof.context -> thm * Proof.context
|
boehmes@36887
|
28 |
val by_abstraction: Proof.context -> thm list -> (Proof.context -> cterm ->
|
boehmes@36887
|
29 |
thm) -> cterm -> thm
|
boehmes@36887
|
30 |
|
boehmes@36887
|
31 |
(* a faster COMP *)
|
boehmes@36887
|
32 |
type compose_data
|
boehmes@36887
|
33 |
val precompose: (cterm -> cterm list) -> thm -> compose_data
|
boehmes@36887
|
34 |
val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
|
boehmes@36887
|
35 |
val compose: compose_data -> thm -> thm
|
boehmes@36887
|
36 |
|
boehmes@36887
|
37 |
(* unfolding of 'distinct' *)
|
boehmes@36887
|
38 |
val unfold_distinct_conv: conv
|
boehmes@36887
|
39 |
|
boehmes@36887
|
40 |
(* simpset *)
|
boehmes@36887
|
41 |
val make_simpset: Proof.context -> thm list -> simpset
|
boehmes@36887
|
42 |
end
|
boehmes@36887
|
43 |
|
boehmes@36887
|
44 |
structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
|
boehmes@36887
|
45 |
struct
|
boehmes@36887
|
46 |
|
boehmes@36887
|
47 |
|
boehmes@36887
|
48 |
|
boehmes@36887
|
49 |
(* accessing terms *)
|
boehmes@36887
|
50 |
|
boehmes@36887
|
51 |
val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
|
boehmes@36887
|
52 |
|
boehmes@36887
|
53 |
fun term_of ct = dest_prop (Thm.term_of ct)
|
boehmes@36887
|
54 |
fun prop_of thm = dest_prop (Thm.prop_of thm)
|
boehmes@36887
|
55 |
|
boehmes@36887
|
56 |
val mk_prop = Thm.capply @{cterm Trueprop}
|
boehmes@36887
|
57 |
|
boehmes@36887
|
58 |
val (eqT, eq) = `(hd o Thm.dest_ctyp o Thm.ctyp_of_term) @{cpat "op =="}
|
boehmes@36887
|
59 |
fun mk_meta_eq_cterm ct cu =
|
boehmes@36887
|
60 |
let val inst = ([(eqT, Thm.ctyp_of_term ct)], [])
|
boehmes@36887
|
61 |
in Thm.mk_binop (Thm.instantiate_cterm inst eq) ct cu end
|
boehmes@36887
|
62 |
|
boehmes@36887
|
63 |
fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
|
boehmes@36887
|
64 |
|
boehmes@36887
|
65 |
|
boehmes@36887
|
66 |
|
boehmes@36887
|
67 |
(* theorem nets *)
|
boehmes@36887
|
68 |
|
boehmes@36887
|
69 |
fun thm_net_of thms =
|
boehmes@36887
|
70 |
let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
|
boehmes@36887
|
71 |
in fold insert thms Net.empty end
|
boehmes@36887
|
72 |
|
boehmes@36887
|
73 |
fun maybe_instantiate ct thm =
|
boehmes@36887
|
74 |
try Thm.first_order_match (Thm.cprop_of thm, ct)
|
boehmes@36887
|
75 |
|> Option.map (fn inst => Thm.instantiate inst thm)
|
boehmes@36887
|
76 |
|
boehmes@36887
|
77 |
fun first_of thms ct = get_first (maybe_instantiate ct) thms
|
boehmes@36887
|
78 |
fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
|
boehmes@36887
|
79 |
|
boehmes@36887
|
80 |
|
boehmes@36887
|
81 |
|
boehmes@36887
|
82 |
(* proof combinators *)
|
boehmes@36887
|
83 |
|
boehmes@36887
|
84 |
fun under_assumption f ct =
|
boehmes@36887
|
85 |
let val ct' = mk_prop ct
|
boehmes@36887
|
86 |
in Thm.implies_intr ct' (f (Thm.assume ct')) end
|
boehmes@36887
|
87 |
|
boehmes@36887
|
88 |
fun with_conv conv prove ct =
|
boehmes@36887
|
89 |
let val eq = Thm.symmetric (conv ct)
|
boehmes@36887
|
90 |
in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
|
boehmes@36887
|
91 |
|
boehmes@36887
|
92 |
fun discharge p pq = Thm.implies_elim pq p
|
boehmes@36887
|
93 |
|
boehmes@36887
|
94 |
fun varify vars = Drule.generalize ([], vars)
|
boehmes@36887
|
95 |
|
boehmes@36887
|
96 |
fun unfold_eqs _ [] = Conv.all_conv
|
boehmes@36887
|
97 |
| unfold_eqs ctxt eqs =
|
boehmes@36887
|
98 |
More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
|
boehmes@36887
|
99 |
|
boehmes@36887
|
100 |
fun match_instantiate f ct thm =
|
boehmes@36887
|
101 |
Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
|
boehmes@36887
|
102 |
|
boehmes@36887
|
103 |
fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
|
boehmes@36887
|
104 |
|
boehmes@36887
|
105 |
(* |- c x == t x ==> P (c x) ~~> c == t |- P (c x) *)
|
boehmes@36888
|
106 |
fun make_hyp_def thm ctxt =
|
boehmes@36887
|
107 |
let
|
boehmes@36887
|
108 |
val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
|
boehmes@36887
|
109 |
val (cf, cvs) = Drule.strip_comb lhs
|
boehmes@36887
|
110 |
val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
|
boehmes@36887
|
111 |
fun apply cv th =
|
boehmes@36887
|
112 |
Thm.combination th (Thm.reflexive cv)
|
boehmes@36887
|
113 |
|> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
|
boehmes@36888
|
114 |
in
|
boehmes@36888
|
115 |
yield_singleton Assumption.add_assumes eq ctxt
|
boehmes@36888
|
116 |
|>> Thm.implies_elim thm o fold apply cvs
|
boehmes@36888
|
117 |
end
|
boehmes@36887
|
118 |
|
boehmes@36887
|
119 |
|
boehmes@36887
|
120 |
|
boehmes@36887
|
121 |
(* abstraction *)
|
boehmes@36887
|
122 |
|
boehmes@36887
|
123 |
local
|
boehmes@36887
|
124 |
|
boehmes@36887
|
125 |
fun typ_of ct = #T (Thm.rep_cterm ct)
|
boehmes@36887
|
126 |
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
|
boehmes@36887
|
127 |
|
boehmes@36887
|
128 |
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
|
boehmes@36887
|
129 |
|
boehmes@36887
|
130 |
fun context_of (ctxt, _, _, _) = ctxt
|
boehmes@36887
|
131 |
|
boehmes@36887
|
132 |
fun replace (cv, ct) = Thm.forall_elim ct o Thm.forall_intr cv
|
boehmes@36887
|
133 |
|
boehmes@36887
|
134 |
fun abs_instantiate (_, tab, _, beta_norm) =
|
boehmes@36887
|
135 |
fold replace (map snd (Termtab.dest tab)) #>
|
boehmes@36887
|
136 |
beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
|
boehmes@36887
|
137 |
|
boehmes@36887
|
138 |
fun generalize cvs =
|
boehmes@36887
|
139 |
let
|
boehmes@36887
|
140 |
val no_name = ""
|
boehmes@36887
|
141 |
|
boehmes@36887
|
142 |
fun dest (Free (n, _)) = n
|
boehmes@36887
|
143 |
| dest _ = no_name
|
boehmes@36887
|
144 |
|
boehmes@36887
|
145 |
fun gen vs (t as Free (n, _)) =
|
boehmes@36887
|
146 |
let val i = find_index (equal n) vs
|
boehmes@36887
|
147 |
in
|
boehmes@36887
|
148 |
if i >= 0 then insert (op aconvc) (nth cvs i) #> pair (Bound i)
|
boehmes@36887
|
149 |
else pair t
|
boehmes@36887
|
150 |
end
|
boehmes@36887
|
151 |
| gen vs (t $ u) = gen vs t ##>> gen vs u #>> (op $)
|
boehmes@36887
|
152 |
| gen vs (Abs (n, T, t)) =
|
boehmes@36887
|
153 |
gen (no_name :: vs) t #>> (fn u => Abs (n, T, u))
|
boehmes@36887
|
154 |
| gen _ t = pair t
|
boehmes@36887
|
155 |
|
boehmes@36887
|
156 |
in (fn ct => gen (map (dest o Thm.term_of) cvs) (Thm.term_of ct) []) end
|
boehmes@36887
|
157 |
|
boehmes@36887
|
158 |
fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) =
|
boehmes@36887
|
159 |
let val (t, cvs') = generalize cvs ct
|
boehmes@36887
|
160 |
in
|
boehmes@36887
|
161 |
(case Termtab.lookup tab t of
|
boehmes@36887
|
162 |
SOME (cv, _) => (cv, cx)
|
boehmes@36887
|
163 |
| NONE =>
|
boehmes@36887
|
164 |
let
|
boehmes@36887
|
165 |
val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
|
boehmes@36887
|
166 |
val cv = certify ctxt (Free (n, map typ_of cvs' ---> typ_of ct))
|
boehmes@36887
|
167 |
val cv' = Drule.list_comb (cv, cvs')
|
boehmes@36887
|
168 |
val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
|
boehmes@36887
|
169 |
val beta_norm' = beta_norm orelse not (null cvs')
|
boehmes@36887
|
170 |
in (cv', (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
|
boehmes@36887
|
171 |
end
|
boehmes@36887
|
172 |
|
boehmes@36887
|
173 |
fun abs_arg f cvs ct =
|
boehmes@36887
|
174 |
let val (cf, cu) = Thm.dest_comb ct
|
boehmes@36887
|
175 |
in f cvs cu #>> Thm.capply cf end
|
boehmes@36887
|
176 |
|
boehmes@36887
|
177 |
fun abs_comb f g cvs ct =
|
boehmes@36887
|
178 |
let val (cf, cu) = Thm.dest_comb ct
|
boehmes@36887
|
179 |
in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
|
boehmes@36887
|
180 |
|
boehmes@36887
|
181 |
fun abs_list f g cvs ct =
|
boehmes@36887
|
182 |
(case Thm.term_of ct of
|
boehmes@36887
|
183 |
Const (@{const_name Nil}, _) => pair ct
|
boehmes@36887
|
184 |
| Const (@{const_name Cons}, _) $ _ $ _ =>
|
boehmes@36887
|
185 |
abs_comb (abs_arg f) (abs_list f g) cvs ct
|
boehmes@36887
|
186 |
| _ => g cvs ct)
|
boehmes@36887
|
187 |
|
boehmes@36887
|
188 |
fun abs_abs f cvs ct =
|
boehmes@36887
|
189 |
let val (cv, cu) = Thm.dest_abs NONE ct
|
boehmes@36887
|
190 |
in f (cv :: cvs) cu #>> Thm.cabs cv end
|
boehmes@36887
|
191 |
|
boehmes@36887
|
192 |
val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
|
boehmes@36887
|
193 |
val is_arithT = (fn @{typ int} => true | @{typ real} => true | _ => false)
|
boehmes@36887
|
194 |
fun is_number t =
|
boehmes@36887
|
195 |
(case try HOLogic.dest_number t of
|
boehmes@36887
|
196 |
SOME (T, _) => is_arithT T
|
boehmes@36887
|
197 |
| NONE => false)
|
boehmes@36887
|
198 |
|
boehmes@36887
|
199 |
val abstract =
|
boehmes@36887
|
200 |
let (* FIXME: provide an option to avoid abstraction of If/distinct/All/Ex *)
|
boehmes@36887
|
201 |
fun abstr1 cvs ct = abs_arg abstr cvs ct
|
boehmes@36887
|
202 |
and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
|
boehmes@36887
|
203 |
and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
|
boehmes@36887
|
204 |
and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
|
boehmes@36887
|
205 |
|
boehmes@36887
|
206 |
and abstr cvs ct =
|
boehmes@36887
|
207 |
(case Thm.term_of ct of
|
boehmes@36887
|
208 |
@{term Trueprop} $ _ => abstr1 cvs ct
|
boehmes@36887
|
209 |
| @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
210 |
| @{term True} => pair ct
|
boehmes@36887
|
211 |
| @{term False} => pair ct
|
boehmes@36887
|
212 |
| @{term Not} $ _ => abstr1 cvs ct
|
boehmes@36887
|
213 |
| @{term "op &"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
214 |
| @{term "op |"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
215 |
| @{term "op -->"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
216 |
| Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
217 |
| Const (@{const_name distinct}, _) $ _ =>
|
boehmes@36887
|
218 |
abs_arg (abs_list abstr fresh_abstraction) cvs ct
|
boehmes@36887
|
219 |
| Const (@{const_name If}, _) $ _ $ _ $ _ => abstr3 cvs ct
|
boehmes@36887
|
220 |
| Const (@{const_name All}, _) $ _ => abstr_abs cvs ct
|
boehmes@36887
|
221 |
| Const (@{const_name Ex}, _) $ _ => abstr_abs cvs ct
|
boehmes@36887
|
222 |
| @{term "uminus :: int => _"} $ _ => abstr1 cvs ct
|
boehmes@36887
|
223 |
| @{term "uminus :: real => _"} $ _ => abstr1 cvs ct
|
boehmes@36887
|
224 |
| @{term "op + :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
225 |
| @{term "op + :: real => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
226 |
| @{term "op - :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
227 |
| @{term "op - :: real => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
228 |
| @{term "op * :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
229 |
| @{term "op * :: real => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
230 |
| @{term "op div :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
231 |
| @{term "op mod :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
232 |
| @{term "op / :: real => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
233 |
| @{term "op < :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
234 |
| @{term "op < :: real => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
235 |
| @{term "op <= :: int => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
236 |
| @{term "op <= :: real => _"} $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
237 |
| Const (@{const_name apply}, _) $ _ $ _ => abstr2 cvs ct
|
boehmes@36887
|
238 |
| Const (@{const_name fun_upd}, _) $ _ $ _ $ _ => abstr3 cvs ct
|
boehmes@36887
|
239 |
| t =>
|
boehmes@36887
|
240 |
if is_atomic t orelse is_number t then pair ct
|
boehmes@36887
|
241 |
else fresh_abstraction cvs ct)
|
boehmes@36887
|
242 |
in abstr [] end
|
boehmes@36887
|
243 |
|
boehmes@36887
|
244 |
fun with_prems thms f ct =
|
boehmes@36887
|
245 |
fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
|
boehmes@36887
|
246 |
|> f
|
boehmes@36887
|
247 |
|> fold (fn prem => fn th => Thm.implies_elim th prem) thms
|
boehmes@36887
|
248 |
|
boehmes@36887
|
249 |
in
|
boehmes@36887
|
250 |
|
boehmes@36887
|
251 |
fun by_abstraction ctxt thms prove = with_prems thms (fn ct =>
|
boehmes@36887
|
252 |
let val (cu, cx) = abstract ct (abs_context ctxt)
|
boehmes@36887
|
253 |
in abs_instantiate cx (prove (context_of cx) cu) end)
|
boehmes@36887
|
254 |
|
boehmes@36887
|
255 |
end
|
boehmes@36887
|
256 |
|
boehmes@36887
|
257 |
|
boehmes@36887
|
258 |
|
boehmes@36887
|
259 |
(* a faster COMP *)
|
boehmes@36887
|
260 |
|
boehmes@36887
|
261 |
type compose_data = cterm list * (cterm -> cterm list) * thm
|
boehmes@36887
|
262 |
|
boehmes@36887
|
263 |
fun list2 (x, y) = [x, y]
|
boehmes@36887
|
264 |
|
boehmes@36887
|
265 |
fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
|
boehmes@36887
|
266 |
fun precompose2 f rule = precompose (list2 o f) rule
|
boehmes@36887
|
267 |
|
boehmes@36887
|
268 |
fun compose (cvs, f, rule) thm =
|
boehmes@36887
|
269 |
discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
|
boehmes@36887
|
270 |
|
boehmes@36887
|
271 |
|
boehmes@36887
|
272 |
|
boehmes@36887
|
273 |
(* unfolding of 'distinct' *)
|
boehmes@36887
|
274 |
|
boehmes@36887
|
275 |
local
|
boehmes@36887
|
276 |
val set1 = @{lemma "x ~: set [] == ~False" by simp}
|
boehmes@36887
|
277 |
val set2 = @{lemma "x ~: set [x] == False" by simp}
|
boehmes@36887
|
278 |
val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
|
boehmes@36887
|
279 |
val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
|
boehmes@36887
|
280 |
val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
|
boehmes@36887
|
281 |
|
boehmes@36887
|
282 |
fun set_conv ct =
|
boehmes@36887
|
283 |
(More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
|
boehmes@36887
|
284 |
(Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
|
boehmes@36887
|
285 |
|
boehmes@36887
|
286 |
val dist1 = @{lemma "distinct [] == ~False" by simp}
|
boehmes@36887
|
287 |
val dist2 = @{lemma "distinct [x] == ~False" by simp}
|
boehmes@36887
|
288 |
val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
|
boehmes@36887
|
289 |
by simp}
|
boehmes@36887
|
290 |
|
boehmes@36887
|
291 |
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
|
boehmes@36887
|
292 |
in
|
boehmes@36887
|
293 |
fun unfold_distinct_conv ct =
|
boehmes@36887
|
294 |
(More_Conv.rewrs_conv [dist1, dist2] else_conv
|
boehmes@36887
|
295 |
(Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
|
boehmes@36887
|
296 |
end
|
boehmes@36887
|
297 |
|
boehmes@36887
|
298 |
|
boehmes@36887
|
299 |
|
boehmes@36887
|
300 |
(* simpset *)
|
boehmes@36887
|
301 |
|
boehmes@36887
|
302 |
local
|
boehmes@36887
|
303 |
val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
|
boehmes@36887
|
304 |
val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
|
boehmes@36887
|
305 |
val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
|
boehmes@36887
|
306 |
val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
|
boehmes@36887
|
307 |
|
boehmes@36887
|
308 |
fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
|
boehmes@36887
|
309 |
fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
|
boehmes@36887
|
310 |
| dest_binop t = raise TERM ("dest_binop", [t])
|
boehmes@36887
|
311 |
|
boehmes@36887
|
312 |
fun prove_antisym_le ss t =
|
boehmes@36887
|
313 |
let
|
boehmes@36887
|
314 |
val (le, r, s) = dest_binop t
|
boehmes@36887
|
315 |
val less = Const (@{const_name less}, Term.fastype_of le)
|
boehmes@36887
|
316 |
val prems = Simplifier.prems_of_ss ss
|
boehmes@36887
|
317 |
in
|
boehmes@36887
|
318 |
(case find_first (eq_prop (le $ s $ r)) prems of
|
boehmes@36887
|
319 |
NONE =>
|
boehmes@36887
|
320 |
find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
|
boehmes@36887
|
321 |
|> Option.map (fn thm => thm RS antisym_less1)
|
boehmes@36887
|
322 |
| SOME thm => SOME (thm RS antisym_le1))
|
boehmes@36887
|
323 |
end
|
boehmes@36887
|
324 |
handle THM _ => NONE
|
boehmes@36887
|
325 |
|
boehmes@36887
|
326 |
fun prove_antisym_less ss t =
|
boehmes@36887
|
327 |
let
|
boehmes@36887
|
328 |
val (less, r, s) = dest_binop (HOLogic.dest_not t)
|
boehmes@36887
|
329 |
val le = Const (@{const_name less_eq}, Term.fastype_of less)
|
boehmes@36887
|
330 |
val prems = prems_of_ss ss
|
boehmes@36887
|
331 |
in
|
boehmes@36887
|
332 |
(case find_first (eq_prop (le $ r $ s)) prems of
|
boehmes@36887
|
333 |
NONE =>
|
boehmes@36887
|
334 |
find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
|
boehmes@36887
|
335 |
|> Option.map (fn thm => thm RS antisym_less2)
|
boehmes@36887
|
336 |
| SOME thm => SOME (thm RS antisym_le2))
|
boehmes@36887
|
337 |
end
|
boehmes@36887
|
338 |
handle THM _ => NONE
|
boehmes@36887
|
339 |
in
|
boehmes@36887
|
340 |
|
boehmes@36887
|
341 |
fun make_simpset ctxt rules = Simplifier.context ctxt (HOL_ss
|
boehmes@36888
|
342 |
addsimps @{thms field_simps}
|
boehmes@36887
|
343 |
addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
|
boehmes@36887
|
344 |
addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
|
boehmes@36887
|
345 |
addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
|
boehmes@36887
|
346 |
addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
|
boehmes@36887
|
347 |
addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
|
boehmes@36887
|
348 |
addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
|
boehmes@36887
|
349 |
addsimps @{thms array_rules}
|
boehmes@36887
|
350 |
addsimprocs [
|
boehmes@36887
|
351 |
Simplifier.simproc @{theory} "fast_int_arith" [
|
boehmes@36887
|
352 |
"(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
|
boehmes@36887
|
353 |
Simplifier.simproc @{theory} "fast_real_arith" [
|
boehmes@36887
|
354 |
"(m::real) < n", "(m::real) <= n", "(m::real) = n"]
|
boehmes@36887
|
355 |
(K Lin_Arith.simproc),
|
boehmes@36887
|
356 |
Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
|
boehmes@36887
|
357 |
(K prove_antisym_le),
|
boehmes@36887
|
358 |
Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
|
boehmes@36887
|
359 |
(K prove_antisym_less)]
|
boehmes@36887
|
360 |
addsimps rules)
|
boehmes@36887
|
361 |
|
boehmes@36887
|
362 |
end
|
boehmes@36887
|
363 |
|
boehmes@36887
|
364 |
end
|