equal
deleted
inserted
replaced
366 *} |
366 *} |
367 |
367 |
368 text {* Setting up the one-point-rule simproc *} |
368 text {* Setting up the one-point-rule simproc *} |
369 |
369 |
370 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {* |
370 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {* |
371 let |
371 fn _ => Quantifier1.rearrange_bex |
372 val unfold_rex_tac = unfold_tac @{thms rex_def}; |
372 (fn ctxt => |
373 fun prove_rex_tac ctxt = unfold_rex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac; |
373 unfold_tac ctxt @{thms rex_def} THEN |
374 in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_rex_tac ctxt) ctxt end |
374 Quantifier1.prove_one_point_ex_tac) |
375 *} |
375 *} |
376 |
376 |
377 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {* |
377 simproc_setup defined_rall ("\<forall>x[M]. P(x) \<longrightarrow> Q(x)") = {* |
378 let |
378 fn _ => Quantifier1.rearrange_ball |
379 val unfold_rall_tac = unfold_tac @{thms rall_def}; |
379 (fn ctxt => |
380 fun prove_rall_tac ctxt = unfold_rall_tac ctxt THEN Quantifier1.prove_one_point_all_tac; |
380 unfold_tac ctxt @{thms rall_def} THEN |
381 in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_rall_tac ctxt) ctxt end |
381 Quantifier1.prove_one_point_all_tac) |
382 *} |
382 *} |
383 |
383 |
384 end |
384 end |