1.1 --- a/CONTRIBUTORS	Mon Jun 25 16:03:21 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Jun 25 18:21:18 2012 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
     1.5    Simproc for rewriting set comprehensions into pointfree expressions
     1.6  
     1.7 +
     1.8  Contributions to Isabelle2012
     1.9  -----------------------------
    1.10  

     2.1 --- a/src/HOL/Finite_Set.thy	Mon Jun 25 16:03:21 2012 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Mon Jun 25 18:21:18 2012 +0200
     2.3 @@ -21,13 +21,13 @@
     2.4  use "Tools/set_comprehension_pointfree.ML"
     2.5  
     2.6  simproc_setup finite_Collect ("finite (Collect P)") =
     2.7 -  {* Set_Comprehension_Pointfree.simproc *}
     2.8 +  {* K Set_Comprehension_Pointfree.simproc *}
     2.9  
    2.10  (* FIXME: move to Set theory*)
    2.11  setup {*
    2.12    Code_Preproc.map_pre (fn ss => ss addsimprocs
    2.13      [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
    2.14 -    proc = Set_Comprehension_Pointfree.code_simproc, identifier = []}])
    2.15 +    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
    2.16  *}
    2.17  
    2.18  lemma finite_induct [case_names empty insert, induct set: finite]:
    2.19 @@ -872,7 +872,7 @@
    2.20      case (insert x F) then show ?case apply -
    2.21      apply (simp add: subset_insert_iff, clarify)
    2.22      apply (subgoal_tac "finite C")
    2.23 -      prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
    2.24 +      prefer 2 apply (blast dest: finite_subset [rotated])
    2.25      apply (subgoal_tac "C = insert x (C - {x})")
    2.26        prefer 2 apply blast
    2.27      apply (erule ssubst)
    2.28 @@ -1524,7 +1524,7 @@
    2.29    apply - apply (erule finite_induct) apply simp
    2.30    apply (simp add: subset_insert_iff, clarify)
    2.31    apply (subgoal_tac "finite C")
    2.32 -  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
    2.33 +  prefer 2 apply (blast dest: finite_subset [rotated])
    2.34    apply (subgoal_tac "C = insert x (C - {x})")
    2.35    prefer 2 apply blast
    2.36    apply (erule ssubst)

     3.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 25 16:03:21 2012 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 25 18:21:18 2012 +0200
     3.3 @@ -511,7 +511,7 @@
     3.4    hence "path_component (S i) x z" and "path_component (S j) z y"
     3.5      using assms by (simp_all add: path_connected_component)
     3.6    hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
     3.7 -    using *(1,3) by (auto elim!: path_component_of_subset [COMP swap_prems_rl])
     3.8 +    using *(1,3) by (auto elim!: path_component_of_subset [rotated])
     3.9    thus "path_component (\<Union>i\<in>A. S i) x y"
    3.10      by (rule path_component_trans)
    3.11  qed

     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 16:03:21 2012 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 18:21:18 2012 +0200
     4.3 @@ -4208,7 +4208,7 @@
     4.4  apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
     4.5  apply (rule_tac x="r1 \<circ> r2" in exI)
     4.6  apply (rule conjI, simp add: subseq_def)
     4.7 -apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption)
     4.8 +apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
     4.9  apply (drule (1) tendsto_Pair) back
    4.10  apply (simp add: o_def)
    4.11  done

     5.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 16:03:21 2012 +0200
     5.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 18:21:18 2012 +0200
     5.3 @@ -1,14 +1,14 @@
     5.4 -(*  Title:      HOL/ex/set_comprehension_pointfree.ML
     5.5 +(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
     5.6      Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
     5.7 -                Rafal Kolanski, NICTA
     5.8 +    Author:     Rafal Kolanski, NICTA
     5.9  
    5.10  Simproc for rewriting set comprehensions to pointfree expressions.
    5.11  *)
    5.12  
    5.13  signature SET_COMPREHENSION_POINTFREE =
    5.14  sig
    5.15 -  val code_simproc : morphism -> simpset -> cterm -> thm option
    5.16 -  val simproc : morphism -> simpset -> cterm -> thm option
    5.17 +  val code_simproc : simpset -> cterm -> thm option
    5.18 +  val simproc : simpset -> cterm -> thm option
    5.19    val rewrite_term : term -> term option
    5.20    (* FIXME: function conv is not a conversion, i.e. of type cterm -> thm, MAYBE rename *)
    5.21    val conv : Proof.context -> term -> thm option
    5.22 @@ -143,7 +143,7 @@
    5.23  
    5.24  (* simproc *)
    5.25  
    5.26 -fun base_simproc _ ss redex =
    5.27 +fun base_simproc ss redex =
    5.28    let
    5.29      val ctxt = Simplifier.the_context ss
    5.30      val set_compr = term_of redex
    5.31 @@ -153,7 +153,7 @@
    5.32    end;
    5.33  
    5.34  (* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
    5.35 -fun simproc _ ss redex =
    5.36 +fun simproc ss redex =
    5.37    let
    5.38      val ctxt = Simplifier.the_context ss
    5.39      val _ $ set_compr = term_of redex
    5.40 @@ -163,11 +163,11 @@
    5.41           thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
    5.42    end;
    5.43  
    5.44 -fun code_simproc morphism ss redex =
    5.45 +fun code_simproc ss redex =
    5.46    let
    5.47      val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
    5.48    in
    5.49 -    case base_simproc morphism ss (Thm.rhs_of prep_thm) of
    5.50 +    case base_simproc ss (Thm.rhs_of prep_thm) of
    5.51        SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
    5.52          Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)])
    5.53      | NONE => NONE

     6.1 --- a/src/Provers/classical.ML	Mon Jun 25 16:03:21 2012 +0200
     6.2 +++ b/src/Provers/classical.ML	Mon Jun 25 18:21:18 2012 +0200
     6.3 @@ -907,7 +907,7 @@
     6.4  
     6.5  (* contradiction method *)
     6.6  
     6.7 -val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
     6.8 +val contradiction = Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim];
     6.9  
    6.10  
    6.11  (* automatic methods *)

     7.1 --- a/src/Pure/drule.ML	Mon Jun 25 16:03:21 2012 +0200
     7.2 +++ b/src/Pure/drule.ML	Mon Jun 25 18:21:18 2012 +0200
     7.3 @@ -105,7 +105,6 @@
     7.4    val incr_indexes2: thm -> thm -> thm -> thm
     7.5    val triv_forall_equality: thm
     7.6    val distinct_prems_rl: thm
     7.7 -  val swap_prems_rl: thm
     7.8    val equal_intr_rule: thm
     7.9    val equal_elim_rule1: thm
    7.10    val equal_elim_rule2: thm
    7.11 @@ -565,24 +564,6 @@
    7.12        (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
    7.13    end;
    7.14  
    7.15 -(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
    7.16 -   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
    7.17 -   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
    7.18 -*)
    7.19 -val swap_prems_rl =
    7.20 -  let
    7.21 -    val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
    7.22 -    val major = Thm.assume cmajor;
    7.23 -    val cminor1 = read_prop "PhiA";
    7.24 -    val minor1 = Thm.assume cminor1;
    7.25 -    val cminor2 = read_prop "PhiB";
    7.26 -    val minor2 = Thm.assume cminor2;
    7.27 -  in
    7.28 -    store_standard_thm_open (Binding.name "swap_prems_rl")
    7.29 -      (Thm.implies_intr cmajor (Thm.implies_intr cminor2 (Thm.implies_intr cminor1
    7.30 -        (Thm.implies_elim (Thm.implies_elim major minor1) minor2))))
    7.31 -  end;
    7.32 -
    7.33  (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
    7.34     ==> PROP ?phi == PROP ?psi
    7.35     Introduction rule for == as a meta-theorem.