10 val new_skolem_var_prefix : string |
10 val new_skolem_var_prefix : string |
11 val extensionalize_theorem : thm -> thm |
11 val extensionalize_theorem : thm -> thm |
12 val introduce_combinators_in_cterm : cterm -> thm |
12 val introduce_combinators_in_cterm : cterm -> thm |
13 val introduce_combinators_in_theorem : thm -> thm |
13 val introduce_combinators_in_theorem : thm -> thm |
14 val to_definitional_cnf_with_quantifiers : theory -> thm -> thm |
14 val to_definitional_cnf_with_quantifiers : theory -> thm -> thm |
15 val cluster_of_zapped_var_name : string -> (int * int) * bool |
15 val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool |
16 val cnf_axiom : |
16 val cnf_axiom : |
17 Proof.context -> bool -> int -> thm -> (thm * term) option * thm list |
17 Proof.context -> bool -> int -> thm -> (thm * term) option * thm list |
18 val meson_general_tac : Proof.context -> thm list -> int -> tactic |
18 val meson_general_tac : Proof.context -> thm list -> int -> tactic |
19 val setup: theory -> theory |
19 val setup: theory -> theory |
20 end; |
20 end; |
227 val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) |
227 val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th)) |
228 val eqth = eqth RS @{thm eq_reflection} |
228 val eqth = eqth RS @{thm eq_reflection} |
229 val eqth = eqth RS @{thm TruepropI} |
229 val eqth = eqth RS @{thm TruepropI} |
230 in Thm.equal_elim eqth th end |
230 in Thm.equal_elim eqth th end |
231 |
231 |
232 fun zapped_var_name ax_no (cluster_no, skolem) s = |
232 fun zapped_var_name ((ax_no, cluster_no), skolem) index_no s = |
233 (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ |
233 (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^ |
234 "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s |
234 "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ |
|
235 string_of_int index_no ^ "_" ^ s |
235 |
236 |
236 fun cluster_of_zapped_var_name s = |
237 fun cluster_of_zapped_var_name s = |
237 ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)), |
238 let val get_int = the o Int.fromString o nth (space_explode "_" s) in |
238 String.isPrefix new_skolem_var_prefix s) |
239 ((get_int 1, (get_int 2, get_int 3)), |
239 |
240 String.isPrefix new_skolem_var_prefix s) |
240 fun rename_vars_to_be_zapped ax_no = |
241 end |
241 let |
242 |
242 fun aux (cluster as (cluster_no, cluster_skolem)) pos t = |
243 fun zap (cluster as (cluster_no, cluster_skolem)) index_no pos ct = |
243 case t of |
|
244 (t1 as Const (s, _)) $ Abs (s', T, t') => |
|
245 if s = @{const_name all} orelse s = @{const_name All} orelse |
|
246 s = @{const_name Ex} then |
|
247 let |
|
248 val skolem = (pos = (s = @{const_name Ex})) |
|
249 val cluster = |
|
250 if skolem = cluster_skolem then cluster |
|
251 else (cluster_no |> cluster_skolem ? Integer.add 1, skolem) |
|
252 val s' = zapped_var_name ax_no cluster s' |
|
253 in t1 $ Abs (s', T, aux cluster pos t') end |
|
254 else |
|
255 t |
|
256 | (t1 as Const (s, _)) $ t2 $ t3 => |
|
257 if s = @{const_name "==>"} orelse s = @{const_name implies} then |
|
258 t1 $ aux cluster (not pos) t2 $ aux cluster pos t3 |
|
259 else if s = @{const_name conj} orelse s = @{const_name disj} then |
|
260 t1 $ aux cluster pos t2 $ aux cluster pos t3 |
|
261 else |
|
262 t |
|
263 | (t1 as Const (s, _)) $ t2 => |
|
264 if s = @{const_name Trueprop} then t1 $ aux cluster pos t2 |
|
265 else if s = @{const_name Not} then t1 $ aux cluster (not pos) t2 |
|
266 else t |
|
267 | _ => t |
|
268 in aux (0, true) true end |
|
269 |
|
270 fun zap pos ct = |
|
271 ct |
244 ct |
272 |> (case term_of ct of |
245 |> (case term_of ct of |
273 Const (s, _) $ Abs (s', _, _) => |
246 Const (s, _) $ Abs (s', _, _) => |
274 if s = @{const_name all} orelse s = @{const_name All} orelse |
247 if s = @{const_name all} orelse s = @{const_name All} orelse |
275 s = @{const_name Ex} then |
248 s = @{const_name Ex} then |
276 Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos |
249 let |
|
250 val skolem = (pos = (s = @{const_name Ex})) |
|
251 val (cluster, index_no) = |
|
252 if skolem = cluster_skolem then (cluster, index_no) |
|
253 else ((cluster_no ||> cluster_skolem ? Integer.add 1, skolem), 0) |
|
254 in |
|
255 Thm.dest_comb #> snd |
|
256 #> Thm.dest_abs (SOME (zapped_var_name cluster index_no s')) |
|
257 #> snd #> zap cluster (index_no + 1) pos |
|
258 end |
277 else |
259 else |
278 Conv.all_conv |
260 Conv.all_conv |
279 | Const (s, _) $ _ $ _ => |
261 | Const (s, _) $ _ $ _ => |
280 if s = @{const_name "==>"} orelse s = @{const_name implies} then |
262 if s = @{const_name "==>"} orelse s = @{const_name implies} then |
281 Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos) |
263 Conv.combination_conv (Conv.arg_conv (zap cluster index_no (not pos))) |
|
264 (zap cluster index_no pos) |
282 else if s = @{const_name conj} orelse s = @{const_name disj} then |
265 else if s = @{const_name conj} orelse s = @{const_name disj} then |
283 Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos) |
266 Conv.combination_conv (Conv.arg_conv (zap cluster index_no pos)) |
|
267 (zap cluster index_no pos) |
284 else |
268 else |
285 Conv.all_conv |
269 Conv.all_conv |
286 | Const (s, _) $ _ => |
270 | Const (s, _) $ _ => |
287 if s = @{const_name Trueprop} then Conv.arg_conv (zap pos) |
271 if s = @{const_name Trueprop} then |
288 else if s = @{const_name Not} then Conv.arg_conv (zap (not pos)) |
272 Conv.arg_conv (zap cluster index_no pos) |
289 else Conv.all_conv |
273 else if s = @{const_name Not} then |
|
274 Conv.arg_conv (zap cluster index_no (not pos)) |
|
275 else |
|
276 Conv.all_conv |
290 | _ => Conv.all_conv) |
277 | _ => Conv.all_conv) |
291 |
278 |
292 fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths |
279 fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths |
293 |
280 |
294 val no_choice = |
281 val no_choice = |
309 |> extensionalize_theorem |
296 |> extensionalize_theorem |
310 |> Meson.make_nnf ctxt |
297 |> Meson.make_nnf ctxt |
311 in |
298 in |
312 if new_skolemizer then |
299 if new_skolemizer then |
313 let |
300 let |
314 fun rename_bound_vars th = |
|
315 let val t = concl_of th in |
|
316 th |> Thm.rename_boundvars t (rename_vars_to_be_zapped ax_no t) |
|
317 end |
|
318 fun skolemize choice_ths = |
301 fun skolemize choice_ths = |
319 Meson.skolemize_with_choice_thms ctxt choice_ths |
302 Meson.skolemize_with_choice_thms ctxt choice_ths |
320 #> simplify (ss_only @{thms all_simps[symmetric]}) |
303 #> simplify (ss_only @{thms all_simps[symmetric]}) |
321 val pull_out = |
304 val pull_out = |
322 simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) |
305 simplify (ss_only @{thms all_simps[symmetric] ex_simps[symmetric]}) |
323 val (discharger_th, fully_skolemized_th) = |
306 val (discharger_th, fully_skolemized_th) = |
324 if null choice_ths then |
307 if null choice_ths then |
325 th |> rename_bound_vars |> `I |>> pull_out ||> skolemize [no_choice] |
308 th |> `I |>> pull_out ||> skolemize [no_choice] |
326 else |
309 else |
327 th |> skolemize choice_ths |> rename_bound_vars |> `I |
310 th |> skolemize choice_ths |> `I |
328 val t = |
311 val t = |
329 fully_skolemized_th |> cprop_of |
312 fully_skolemized_th |> cprop_of |
330 |> zap true |> Drule.export_without_context |
313 |> zap ((ax_no, 0), true) 0 true |> Drule.export_without_context |
331 |> cprop_of |> Thm.dest_equals |> snd |> term_of |
314 |> cprop_of |> Thm.dest_equals |> snd |> term_of |
332 in |
315 in |
333 if exists_subterm (fn Var ((s, _), _) => |
316 if exists_subterm (fn Var ((s, _), _) => |
334 String.isPrefix new_skolem_var_prefix s |
317 String.isPrefix new_skolem_var_prefix s |
335 | _ => false) t then |
318 | _ => false) t then |