# HG changeset patch
# User nipkow
# Date 1229332742 -3600
# Node ID d2b60c49a7133dcf1afd806109d17d4949820866
# Parent  8f38bf68d42e1923d3b97a297bd9f716ee286359# Parent  476c46e99ada98eddc805ca1781c196fb98d5ee6
merged

diff -r 8f38bf68d42e -r d2b60c49a713 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Dec 15 09:58:45 2008 +0100
+++ b/src/HOL/Divides.thy	Mon Dec 15 10:19:02 2008 +0100
@@ -127,7 +127,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp
diff -r 8f38bf68d42e -r d2b60c49a713 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Dec 15 09:58:45 2008 +0100
+++ b/src/HOL/IsaMakefile	Mon Dec 15 10:19:02 2008 +0100
@@ -777,6 +777,7 @@
   ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
   ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
   ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
+  ex/CodegenSML_Test.thy 						\
   ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
   ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy		\
   ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy	\
diff -r 8f38bf68d42e -r d2b60c49a713 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Dec 15 09:58:45 2008 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Dec 15 10:19:02 2008 +0100
@@ -28,6 +28,10 @@
 lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   unfolding eq_set_def by auto
 
+(* FIXME allow for Stefan's code generator:
+declare set_eq_subset[code unfold]
+*)
+
 lemma [code]:
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..
@@ -35,6 +39,8 @@
 definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   "filter_set P xs = {x\<in>xs. P x}"
 
+declare filter_set_def[symmetric, code unfold] 
+
 
 subsection {* Operations on lists *}
 
@@ -269,5 +275,6 @@
   Ball ("{*Blall*}")
   Bex ("{*Blex*}")
   filter_set ("{*filter*}")
+  fold ("{* foldl o flip *}")
 
 end
diff -r 8f38bf68d42e -r d2b60c49a713 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Dec 15 09:58:45 2008 +0100
+++ b/src/HOL/Real.thy	Mon Dec 15 10:19:02 2008 +0100
@@ -1,5 +1,5 @@
 theory Real
-imports "~~/src/HOL/Real/RealVector"
+imports RComplete "~~/src/HOL/Real/RealVector"
 begin
 
 end
diff -r 8f38bf68d42e -r d2b60c49a713 src/HOL/ex/CodegenSML_Test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodegenSML_Test.thy	Mon Dec 15 10:19:02 2008 +0100
@@ -0,0 +1,54 @@
+(*  Title:      Test file for Stefan Berghofer's SML code generator
+    Author:     Tobias Nipkow, TU Muenchen
+*)
+
+theory CodegenSML_Test
+imports Executable_Set
+begin
+
+lemma "True : {False, True} & False ~: {True}"
+by evaluation
+
+lemma
+"eq_set ({1::nat,2,3,2} \<union> {3,1,2,1}) {2,2,3,1} &
+ eq_set ({1::nat,2,3,2} \<union> {4,1,5,1}) {4,4,5,1,2,3}"
+by evaluation
+
+lemma
+"eq_set ({1::nat,2,3,2} \<inter> {3,1,2,1}) {2,2,3,1} & 
+ eq_set ({1::nat,2,3,2} \<inter> {4,1,5,2}) {2,1,2}"
+by evaluation
+
+lemma
+"eq_set ({1::nat,2,3,2} - {3,1,2,1}) {} & 
+ eq_set ({1::nat,2,3,2} - {4,1,5,2}) {3}"
+by evaluation
+
+lemma
+"eq_set (Union{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} &
+ eq_set (Union{{1::nat,2,3,2}, {4,1,5,1}}) {4,4,5,1,2,3}"
+by evaluation
+
+lemma
+"eq_set (Inter{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} & 
+ eq_set (Inter{{1::nat,2,3,2}, {4,1,5,2}}) {2,1,2}"
+by evaluation
+
+lemma "eq_set ((%x. x+2) ` {1::nat,2,3,2}) {4,5,3,3}"
+by evaluation
+
+lemma
+"(ALL x:{1::nat,2,3,2}. EX y : {4,5,2}. x < y) &
+ (EX x:{1::nat,2,3,2}. ALL y : {4,5,6}. x < y)"
+by evaluation
+
+lemma
+"eq_set {x : {4::nat,7,10}. 2 dvd x } {4,10}"
+by evaluation
+
+lemma
+"fold (op +) (5::int) {3,7,9} = 24 &
+ fold_image (op *) id (2::int) {3,4,5} = 120"
+by evaluation
+
+end