# HG changeset patch
# User wenzelm
# Date 1340641278 -7200
# Node ID bf172a5929bbbaaa6aef2aef28bc54918b9ff6e4
# Parent  104e5fccea1290131bfaac6e37ca32b2f98000d2# Parent  d30957198bbb9cf96d720adf1c69fc475f930e20
merged, resolving conflict with 87c831e30f0a;

diff -r 104e5fccea12 -r bf172a5929bb CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Jun 25 16:03:21 2012 +0200
+++ b/CONTRIBUTORS	Mon Jun 25 18:21:18 2012 +0200
@@ -9,6 +9,7 @@
 * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
   Simproc for rewriting set comprehensions into pointfree expressions
 
+
 Contributions to Isabelle2012
 -----------------------------
 
diff -r 104e5fccea12 -r bf172a5929bb src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 25 16:03:21 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 25 18:21:18 2012 +0200
@@ -21,13 +21,13 @@
 use "Tools/set_comprehension_pointfree.ML"
 
 simproc_setup finite_Collect ("finite (Collect P)") =
-  {* Set_Comprehension_Pointfree.simproc *}
+  {* K Set_Comprehension_Pointfree.simproc *}
 
 (* FIXME: move to Set theory*)
 setup {*
   Code_Preproc.map_pre (fn ss => ss addsimprocs
     [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}],
-    proc = Set_Comprehension_Pointfree.code_simproc, identifier = []}])
+    proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
 *}
 
 lemma finite_induct [case_names empty insert, induct set: finite]:
@@ -872,7 +872,7 @@
     case (insert x F) then show ?case apply -
     apply (simp add: subset_insert_iff, clarify)
     apply (subgoal_tac "finite C")
-      prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+      prefer 2 apply (blast dest: finite_subset [rotated])
     apply (subgoal_tac "C = insert x (C - {x})")
       prefer 2 apply blast
     apply (erule ssubst)
@@ -1524,7 +1524,7 @@
   apply - apply (erule finite_induct) apply simp
   apply (simp add: subset_insert_iff, clarify)
   apply (subgoal_tac "finite C")
-  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+  prefer 2 apply (blast dest: finite_subset [rotated])
   apply (subgoal_tac "C = insert x (C - {x})")
   prefer 2 apply blast
   apply (erule ssubst)
diff -r 104e5fccea12 -r bf172a5929bb src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 25 16:03:21 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon Jun 25 18:21:18 2012 +0200
@@ -511,7 +511,7 @@
   hence "path_component (S i) x z" and "path_component (S j) z y"
     using assms by (simp_all add: path_connected_component)
   hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
-    using *(1,3) by (auto elim!: path_component_of_subset [COMP swap_prems_rl])
+    using *(1,3) by (auto elim!: path_component_of_subset [rotated])
   thus "path_component (\<Union>i\<in>A. S i) x y"
     by (rule path_component_trans)
 qed
diff -r 104e5fccea12 -r bf172a5929bb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 16:03:21 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 18:21:18 2012 +0200
@@ -4208,7 +4208,7 @@
 apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
 apply (rule_tac x="r1 \<circ> r2" in exI)
 apply (rule conjI, simp add: subseq_def)
-apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption)
+apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
 apply (drule (1) tendsto_Pair) back
 apply (simp add: o_def)
 done
diff -r 104e5fccea12 -r bf172a5929bb src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 16:03:21 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 18:21:18 2012 +0200
@@ -1,14 +1,14 @@
-(*  Title:      HOL/ex/set_comprehension_pointfree.ML
+(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
     Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
-                Rafal Kolanski, NICTA
+    Author:     Rafal Kolanski, NICTA
 
 Simproc for rewriting set comprehensions to pointfree expressions.
 *)
 
 signature SET_COMPREHENSION_POINTFREE =
 sig
-  val code_simproc : morphism -> simpset -> cterm -> thm option
-  val simproc : morphism -> simpset -> cterm -> thm option
+  val code_simproc : simpset -> cterm -> thm option
+  val simproc : simpset -> cterm -> thm option
   val rewrite_term : term -> term option
   (* FIXME: function conv is not a conversion, i.e. of type cterm -> thm, MAYBE rename *)
   val conv : Proof.context -> term -> thm option
@@ -143,7 +143,7 @@
 
 (* simproc *)
 
-fun base_simproc _ ss redex =
+fun base_simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
     val set_compr = term_of redex
@@ -153,7 +153,7 @@
   end;
 
 (* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
-fun simproc _ ss redex =
+fun simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
     val _ $ set_compr = term_of redex
@@ -163,11 +163,11 @@
          thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
   end;
 
-fun code_simproc morphism ss redex =
+fun code_simproc ss redex =
   let
     val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
   in
-    case base_simproc morphism ss (Thm.rhs_of prep_thm) of
+    case base_simproc ss (Thm.rhs_of prep_thm) of
       SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
         Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)])
     | NONE => NONE
diff -r 104e5fccea12 -r bf172a5929bb src/Provers/classical.ML
--- a/src/Provers/classical.ML	Mon Jun 25 16:03:21 2012 +0200
+++ b/src/Provers/classical.ML	Mon Jun 25 18:21:18 2012 +0200
@@ -907,7 +907,7 @@
 
 (* contradiction method *)
 
-val contradiction = Method.rule [Data.not_elim, Data.not_elim COMP Drule.swap_prems_rl];
+val contradiction = Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim];
 
 
 (* automatic methods *)
diff -r 104e5fccea12 -r bf172a5929bb src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jun 25 16:03:21 2012 +0200
+++ b/src/Pure/drule.ML	Mon Jun 25 18:21:18 2012 +0200
@@ -105,7 +105,6 @@
   val incr_indexes2: thm -> thm -> thm -> thm
   val triv_forall_equality: thm
   val distinct_prems_rl: thm
-  val swap_prems_rl: thm
   val equal_intr_rule: thm
   val equal_elim_rule1: thm
   val equal_elim_rule2: thm
@@ -565,24 +564,6 @@
       (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
   end;
 
-(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
-   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
-   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
-*)
-val swap_prems_rl =
-  let
-    val cmajor = read_prop "PhiA ==> PhiB ==> Psi";
-    val major = Thm.assume cmajor;
-    val cminor1 = read_prop "PhiA";
-    val minor1 = Thm.assume cminor1;
-    val cminor2 = read_prop "PhiB";
-    val minor2 = Thm.assume cminor2;
-  in
-    store_standard_thm_open (Binding.name "swap_prems_rl")
-      (Thm.implies_intr cmajor (Thm.implies_intr cminor2 (Thm.implies_intr cminor1
-        (Thm.implies_elim (Thm.implies_elim major minor1) minor2))))
-  end;
-
 (* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
    ==> PROP ?phi == PROP ?psi
    Introduction rule for == as a meta-theorem.