src/HOL/Tools/Predicate_Compile/pred_compile_set.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML	Wed Sep 23 16:20:12 2009 +0200
@@ -0,0 +1,51 @@
+(* Author: Lukas Bulwahn, TU Muenchen
+
+Preprocessing sets to predicates
+*)
+
+signature PRED_COMPILE_SET =
+sig
+(*
+  val preprocess_intro : thm -> theory -> thm * theory
+  val preprocess_clause : term -> theory -> term * theory
+*)
+  val unfold_set_notation : thm -> thm;
+end;
+
+structure Pred_Compile_Set : PRED_COMPILE_SET =
+struct
+(*FIXME: unfolding Ball in pretty adhoc here *)
+val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, @{thm Ball_def}]
+
+val unfold_set_notation = Simplifier.rewrite_rule unfold_set_lemmas
+
+(*
+fun find_set_theorems ctxt cname =
+  let
+    val _ = cname 
+*)
+
+(*
+fun preprocess_term t ctxt =
+  case t of
+    Const ("op :", _) $ x $ A => 
+      case strip_comb A of
+        (Const (cname, T), params) =>
+          let 
+            val _ = find_set_theorems
+          in
+            (t, ctxt)
+          end
+      | _ => (t, ctxt)  
+  | _ => (t, ctxt)
+*) 
+(*
+fun preprocess_intro th thy =
+  let
+    val cnames = find_heads_of_prems
+    val set_cname = filter (has_set_definition
+    val _ = define_preds
+    val _ = prep_pred_def
+  in
+*)
+end;