src/ZF/pair.thy
changeset 42455 6702c984bf5a
parent 41777 1f7cbe39d425
child 42456 13b4b6ba3593
     1.1 --- a/src/ZF/pair.thy	Fri Apr 22 13:07:47 2011 +0200
     1.2 +++ b/src/ZF/pair.thy	Fri Apr 22 13:58:13 2011 +0200
     1.3 @@ -7,7 +7,29 @@
     1.4  header{*Ordered Pairs*}
     1.5  
     1.6  theory pair imports upair
     1.7 -uses "simpdata.ML" begin
     1.8 +uses "simpdata.ML"
     1.9 +begin
    1.10 +
    1.11 +simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
    1.12 +  let
    1.13 +    val unfold_bex_tac = unfold_tac @{thms Bex_def};
    1.14 +    fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.15 +  in
    1.16 +    fn _ => fn ss => fn ct =>
    1.17 +      Quantifier1.rearrange_bex prove_bex_tac (theory_of_cterm ct) ss (term_of ct)
    1.18 +  end
    1.19 +*}
    1.20 +
    1.21 +simproc_setup defined_Ball ("ALL x:A. P(x) --> Q(x)") = {*
    1.22 +  let
    1.23 +    val unfold_ball_tac = unfold_tac @{thms Ball_def};
    1.24 +    fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.25 +  in
    1.26 +    fn _ => fn ss => fn ct =>
    1.27 +      Quantifier1.rearrange_ball prove_ball_tac (theory_of_cterm ct) ss (term_of ct)
    1.28 +  end
    1.29 +*}
    1.30 +
    1.31  
    1.32  (** Lemmas for showing that <a,b> uniquely determines a and b **)
    1.33