merged, resolving conflict with 87c831e30f0a;

--- a/src/HOL/Enum.thy	Mon Jun 25 17:50:05 2012 +0200
+++ b/src/HOL/Enum.thy	Mon Jun 25 18:21:18 2012 +0200
@@ -784,10 +784,14 @@
 
 subsection {* Further operations on finite types *}
 
-lemma [code]:
+lemma Collect_code[code]:
   "Collect P = set (filter P enum)"
 by (auto simp add: enum_UNIV)
 
+lemma [code]:
+  "Id = image (%x. (x, x)) (set Enum.enum)"
+by (auto intro: imageI in_enum)
+
 lemma tranclp_unfold [code, no_atp]:
   "tranclp r a b \<equiv> (a, b) \<in> trancl {(x, y). r x y}"
 by (simp add: trancl_def)

--- a/src/HOL/Finite_Set.thy	Mon Jun 25 17:50:05 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 25 18:21:18 2012 +0200
@@ -17,11 +17,18 @@
     emptyI [simp, intro!]: "finite {}"
   | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)"
 
+(* FIXME: move to Set theory *)
 use "Tools/set_comprehension_pointfree.ML"
 
 simproc_setup finite_Collect ("finite (Collect P)") =
   {* 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 = K Set_Comprehension_Pointfree.code_simproc, identifier = []}])
+*}
 
 lemma finite_induct [case_names empty insert, induct set: finite]:
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}

--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 17:50:05 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 18:21:18 2012 +0200
@@ -7,8 +7,10 @@
 
 signature SET_COMPREHENSION_POINTFREE =
 sig
+  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
 end
 
@@ -141,6 +143,16 @@
 
 (* simproc *)
 
+fun base_simproc ss redex =
+  let
+    val ctxt = Simplifier.the_context ss
+    val set_compr = term_of redex
+  in
+    conv ctxt set_compr
+    |> Option.map (fn thm => thm RS @{thm eq_reflection})
+  end;
+
+(* FIXME: turn into generic simproc for many predicates, i.e., remove hard-coded finite! *)
 fun simproc ss redex =
   let
     val ctxt = Simplifier.the_context ss
@@ -151,5 +163,15 @@
          thm RS @{thm arg_cong[of _ _ finite]} RS @{thm eq_reflection})
   end;
 
+fun code_simproc ss redex =
+  let
+    val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
+  in
+    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
+  end;
+
 end;