src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -133,6 +133,56 @@
   end;
 
 fun preprocess_term t thy = error "preprocess_pred_term: to implement" 
-  
-  
+
+fun is_Abs (Abs _) = true
+  | is_Abs _       = false
+
+fun flat_higher_order_arguments (intross, thy) =
+  let
+    fun process constname atom (new_defs, thy) =
+      let
+        val (pred, args) = strip_comb atom
+        val abs_args = filter is_Abs args
+        fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
+          let
+            val _ = tracing ("Introduce new constant for " ^
+              Syntax.string_of_term_global thy abs_arg)
+            val vars = map Var (Term.add_vars abs_arg [])
+            val abs_arg' = Logic.unvarify abs_arg
+            val frees = map Free (Term.add_frees abs_arg' [])
+            val constname = Name.variant []
+              ((Long_Name.base_name constname) ^ "_hoaux")
+            val full_constname = Sign.full_bname thy constname
+            val constT = map fastype_of frees ---> (fastype_of abs_arg')
+            val const = Const (full_constname, constT)
+            val lhs = list_comb (const, frees)
+            val def = Logic.mk_equals (lhs, abs_arg')
+            val _ = tracing (Syntax.string_of_term_global thy def)
+            val ([definition], thy') = thy
+              |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+              |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+            
+          in
+            (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
+          end
+        | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
+
+      val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
+            (*        val _ = if not (null abs_args) then error "Found some abs argument" else ()*)
+      in
+        (list_comb (pred, args'), (new_defs', thy'))
+      end
+    fun flat_intro intro (new_defs, thy) =
+      let
+        val constname = "dummy"
+        val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
+        val th = setmp quick_and_dirty true (SkipProof.make_thm thy) intro_ts
+      in
+        (th, (new_defs, thy))
+      end
+    val (intross', (new_defs, thy')) = fold_map (fold_map flat_intro) intross ([], thy)
+  in
+    (intross', (new_defs, thy'))
+  end
+
 end;