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"
```