src/HOL/Extraction/Pigeonhole.thy
changeset 20837 099877d83d2b
parent 20593 5af400cc64d5
child 20933 3f999b73f6d5
--- a/src/HOL/Extraction/Pigeonhole.thy	Mon Oct 02 23:00:52 2006 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Mon Oct 02 23:00:53 2006 +0200
@@ -285,9 +285,6 @@
 consts_code
   arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
 
-code_const "arbitrary \<Colon> nat \<times> nat"
-  (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
-
 code_module PH
 contains
   test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
@@ -304,4 +301,32 @@
 
 ML "PH.pigeonhole 8 (PH.sel [0,1,2,3,4,5,6,3,7,8])"
 
+definition
+  arbitrary_nat :: "nat \<times> nat"
+  "arbitrary_nat = arbitrary"
+
+lemma [code func]:
+  "arbitrary_nat = arbitrary_nat" ..
+
+declare arbitrary_nat_def [symmetric, code inline]
+
+code_const arbitrary_nat
+  (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
+
+definition
+  "test n = pigeonhole n (\<lambda>m. m - 1)"
+  "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
+
+code_gen test test' "op !" (SML -)
+
+ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
+ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
+ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
+ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
+ML "timeit (fn () => ROOT.Pigeonhole.test 25)"
+ML "timeit (fn () => ROOT.Pigeonhole.test' 25)"
+ML "timeit (fn () => ROOT.Pigeonhole.test 500)"
+
+ML "ROOT.Pigeonhole.pigeonhole 8 (ROOT.List.nth [0,1,2,3,4,5,6,3,7,8])"
+
 end