# HG changeset patch
# User huffman
# Date 1267061879 28800
# Node ID 593c184977a4cf215872d31351975e8ebc88670f
# Parent  73f645fdd4fff01f7a5806169a08c7c28cfed7c4
add function beta_of_def

diff -r 73f645fdd4ff -r 593c184977a4 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Feb 24 16:15:03 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Wed Feb 24 17:37:59 2010 -0800
@@ -228,11 +228,32 @@
     ((consts, def_thms), thy)
   end;
 
-(*** argument preprocessing ***)
+
+(************** generating beta reduction rules from definitions **************)
 
-type arg = (bool * binding option * typ) * string;
-
-
+local
+  fun arglist (Const _ $ Abs (s, T, t)) =
+      let
+        val arg = Free (s, T);
+        val (args, body) = arglist (subst_bound (arg, t));
+      in (arg :: args, body) end
+    | arglist t = ([], t);
+in
+  fun beta_of_def thy def_thm =
+      let
+        val (con, lam) = Logic.dest_equals (concl_of def_thm);
+        val (args, rhs) = arglist lam;
+        val lhs = Library.foldl mk_capply (con, args);
+        val goal = mk_equals (lhs, rhs);
+        val cs = ContProc.cont_thms lam;
+        val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs;
+        val tac =
+            rewrite_goals_tac (def_thm::betas)
+            THEN rtac reflexive_thm 1;
+      in
+        Goal.prove_global thy [] [] goal (K tac)
+      end;
+end;
 
 (******************************* main function ********************************)
 
@@ -265,6 +286,8 @@
         define_consts (map2 mk_def cons' rhss) thy
       end;
 
+    val con_beta_thms = map (beta_of_def thy) con_def_thms;
+
     (* TODO: re-enable this *)
     (* val thy = Sign.parent_path thy; *)