9 begin |
9 begin |
10 |
10 |
11 ML_file "simpdata.ML" |
11 ML_file "simpdata.ML" |
12 |
12 |
13 setup {* |
13 setup {* |
14 Simplifier.map_simpset_global |
14 map_theory_simpset |
15 (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) |
15 (Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)) |
16 #> Simplifier.add_cong @{thm if_weak_cong}) |
16 #> Simplifier.add_cong @{thm if_weak_cong}) |
17 *} |
17 *} |
18 |
18 |
19 ML {* val ZF_ss = @{simpset} *} |
19 ML {* val ZF_ss = simpset_of @{context} *} |
20 |
20 |
21 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {* |
21 simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = {* |
22 let |
22 let |
23 val unfold_bex_tac = unfold_tac @{thms Bex_def}; |
23 val unfold_bex_tac = unfold_tac @{thms Bex_def}; |
24 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; |
24 fun prove_bex_tac ctxt = unfold_bex_tac ctxt THEN Quantifier1.prove_one_point_ex_tac; |
25 in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end |
25 in fn _ => fn ctxt => Quantifier1.rearrange_bex (prove_bex_tac ctxt) ctxt end |
26 *} |
26 *} |
27 |
27 |
28 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {* |
28 simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = {* |
29 let |
29 let |
30 val unfold_ball_tac = unfold_tac @{thms Ball_def}; |
30 val unfold_ball_tac = unfold_tac @{thms Ball_def}; |
31 fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; |
31 fun prove_ball_tac ctxt = unfold_ball_tac ctxt THEN Quantifier1.prove_one_point_all_tac; |
32 in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end |
32 in fn _ => fn ctxt => Quantifier1.rearrange_ball (prove_ball_tac ctxt) ctxt end |
33 *} |
33 *} |
34 |
34 |
35 |
35 |
36 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
36 (** Lemmas for showing that <a,b> uniquely determines a and b **) |
37 |
37 |