src/HOL/Set.thy
changeset 42459 38b9f023cc34
parent 42456 13b4b6ba3593
child 43818 fcc5d3ffb6f5
     1.1 --- a/src/HOL/Set.thy	Fri Apr 22 14:53:11 2011 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Apr 22 15:05:04 2011 +0200
     1.3 @@ -76,14 +76,12 @@
     1.4  *}
     1.5  
     1.6  simproc_setup defined_Collect ("{x. P x & Q x}") = {*
     1.7 -  let
     1.8 -    val Collect_perm_tac =
     1.9 -      rtac @{thm Collect_cong} 1 THEN
    1.10 +  fn _ =>
    1.11 +    Quantifier1.rearrange_Collect
    1.12 +     (rtac @{thm Collect_cong} 1 THEN
    1.13        rtac @{thm iffI} 1 THEN
    1.14 -      ALLGOALS (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]);
    1.15 -  in
    1.16 -    fn _ => fn ss => Quantifier1.rearrange_Collect Collect_perm_tac ss o term_of
    1.17 -  end
    1.18 +      ALLGOALS
    1.19 +        (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
    1.20  *}
    1.21  
    1.22  lemmas CollectE = CollectD [elim_format]
    1.23 @@ -331,18 +329,14 @@
    1.24    let
    1.25      val unfold_bex_tac = unfold_tac @{thms Bex_def};
    1.26      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    1.27 -  in
    1.28 -    fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss o term_of
    1.29 -  end
    1.30 +  in fn _ => fn ss => Quantifier1.rearrange_bex (prove_bex_tac ss) ss end
    1.31  *}
    1.32  
    1.33  simproc_setup defined_All ("ALL x:A. P x --> Q x") = {*
    1.34    let
    1.35      val unfold_ball_tac = unfold_tac @{thms Ball_def};
    1.36      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    1.37 -  in
    1.38 -    fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss o term_of
    1.39 -  end
    1.40 +  in fn _ => fn ss => Quantifier1.rearrange_ball (prove_ball_tac ss) ss end
    1.41  *}
    1.42  
    1.43  lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x"