# HG changeset patch
# User bulwahn
# Date 1340632994 -7200
# Node ID f479f36ed2fff30af5666a81d3632a91c8e0aa53
# Parent  fa7c0c659798120eed81003c74acb6e9b530c691
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions;
noting further steps with FIXME

diff -r fa7c0c659798 -r f479f36ed2ff src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 25 16:03:14 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)") =
   {* 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 = []}])
+*}
 
 lemma finite_induct [case_names empty insert, induct set: finite]:
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
diff -r fa7c0c659798 -r f479f36ed2ff src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 16:03:14 2012 +0200
@@ -7,8 +7,10 @@
 
 signature SET_COMPREHENSION_POINTFREE =
 sig
+  val code_simproc : morphism -> simpset -> cterm -> thm option
   val simproc : morphism -> 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 morphism 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
+      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;