library theories for debugging and parallel computing using code generation towards Isabelle/ML

--- a/src/HOL/IsaMakefile	Sat Jul 21 20:01:16 2012 +0200
+++ b/src/HOL/IsaMakefile	Sun Jul 22 09:56:34 2012 +0200
@@ -452,6 +452,7 @@
   Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
   Library/Continuity.thy						\
   Library/Convex.thy Library/Countable.thy				\
+  Library/Debug.thy							\
   Library/Dlist.thy Library/Eval_Witness.thy				\
   Library/DAList.thy Library/Dlist.thy					\
   Library/Eval_Witness.thy						\
@@ -470,6 +471,7 @@
   Library/Multiset.thy Library/Nat_Bijection.thy			\
   Library/Numeral_Type.thy Library/Old_Recdef.thy			\
   Library/OptionalSugar.thy Library/Order_Relation.thy			\
+  Library/Parallel.thy							\
   Library/Permutation.thy Library/Permutations.thy			\
   Library/Phantom_Type.thy Library/Poly_Deriv.thy			\
   Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
@@ -1034,6 +1036,7 @@
   ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy	\
   ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy			\
   ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy	\
+  ex/Parallel_Example.thy						\
   ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy				\
   ex/Quicksort.thy ex/ROOT.ML						\
   ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Debug.thy	Sun Jul 22 09:56:34 2012 +0200
@@ -0,0 +1,40 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Debugging facilities for code generated towards Isabelle/ML *}
+
+theory Debug
+imports Main
+begin
+
+definition trace :: "String.literal \<Rightarrow> unit" where
+  [simp]: "trace s = ()"
+
+definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
+  [simp]: "tracing s = id"
+
+lemma [code]:
+  "tracing s = (let u = trace s in id)"
+  by simp
+
+definition flush :: "'a \<Rightarrow> unit" where
+  [simp]: "flush x = ()"
+
+definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
+  [simp]: "flushing x = id"
+
+lemma [code, code_unfold]:
+  "flushing x = (let u = flush x in id)"
+  by simp
+
+definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
+  [simp]: "timing s f x = f x"
+
+code_const trace and flush and timing
+  (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
+
+code_reserved Eval Output PolyML Timing
+
+hide_const (open) trace tracing flush flushing timing
+
+end
+

--- a/src/HOL/Library/Library.thy	Sat Jul 21 20:01:16 2012 +0200
+++ b/src/HOL/Library/Library.thy	Sun Jul 22 09:56:34 2012 +0200
@@ -12,6 +12,7 @@
   ContNotDenum
   Convex
   Countable
+  Debug
   Dlist
   Eval_Witness
   Extended_Nat
@@ -37,6 +38,7 @@
   Old_Recdef
   OptionalSugar
   Option_ord
+  Parallel
   Permutation
   Permutations
   Poly_Deriv

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Parallel.thy	Sun Jul 22 09:56:34 2012 +0200
@@ -0,0 +1,67 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Futures and parallel lists for code generated towards Isabelle/ML *}
+
+theory Parallel
+imports Main
+begin
+
+subsection {* Futures *}
+
+datatype 'a future = fork "unit \<Rightarrow> 'a"
+
+primrec join :: "'a future \<Rightarrow> 'a" where
+  "join (fork f) = f ()"
+
+lemma future_eqI [intro!]:
+  assumes "join f = join g"
+  shows "f = g"
+  using assms by (cases f, cases g) (simp add: ext)
+
+code_type future
+  (Eval "_ future")
+
+code_const fork
+  (Eval "Future.fork")
+
+code_const join
+  (Eval "Future.join")
+
+code_reserved Eval Future future
+
+
+subsection {* Parallel lists *}
+
+definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
+  [simp]: "map = List.map"
+
+definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "forall = list_all"
+
+lemma forall_all [simp]:
+  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
+  by (simp add: forall_def list_all_iff)
+
+definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "exists = list_ex"
+
+lemma exists_ex [simp]:
+  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
+  by (simp add: exists_def list_ex_iff)
+
+code_const map
+  (Eval "Par'_List.map")
+
+code_const forall
+  (Eval "Par'_List.forall")
+
+code_const exists
+  (Eval "Par'_List.exists")
+
+code_reserved Eval Par_List
+
+
+hide_const (open) fork join map exists forall
+
+end
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Parallel_Example.thy	Sun Jul 22 09:56:34 2012 +0200
@@ -0,0 +1,108 @@
+header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
+
+theory Parallel_Example
+imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
+begin
+
+subsection {* Compute-intensive examples. *}
+
+subsubsection {* Fragments of the harmonic series *}
+
+definition harmonic :: "nat \<Rightarrow> rat" where
+  "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
+
+
+subsubsection {* The sieve of Erathostenes *}
+
+text {*
+  The attentive reader may relate this ad-hoc implementation to the
+  arithmetic notion of prime numbers as a little exercise.
+*}
+
+primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where
+  "mark _ _ [] = []"
+| "mark m n (p # ps) = (case n of 0 \<Rightarrow> False # mark m m ps
+    | Suc n \<Rightarrow> p # mark m n ps)"
+
+lemma length_mark [simp]:
+  "length (mark m n ps) = length ps"
+  by (induct ps arbitrary: n) (simp_all split: nat.split)
+
+function sieve :: "nat \<Rightarrow> bool list \<Rightarrow> bool list" where
+  "sieve m ps = (case dropWhile Not ps
+   of [] \<Rightarrow> ps
+    | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
+by pat_completeness auto
+
+termination -- {* tuning of this proof is left as an exercise to the reader *}
+  apply (relation "measure (length \<circ> snd)")
+  apply rule
+  apply (auto simp add: length_dropWhile_le)
+proof -
+  fix ps qs q
+  assume "dropWhile Not ps = q # qs"
+  then have "length (q # qs) = length (dropWhile Not ps)" by simp
+  then have "length qs < length (dropWhile Not ps)" by simp
+  moreover have "length (dropWhile Not ps) \<le> length ps"
+    by (simp add: length_dropWhile_le)
+  ultimately show "length qs < length ps" by auto
+qed
+
+primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
+  "natify _ [] = []"
+| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
+
+primrec list_primes where
+  "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
+
+
+subsubsection {* Naive factorisation *}
+
+function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
+  "factorise_from k n = (if 1 < k \<and> k \<le> n
+    then
+      let (q, r) = divmod_nat n k 
+      in if r = 0 then k # factorise_from k q
+        else factorise_from (Suc k) n
+    else [])" 
+by pat_completeness auto
+
+termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *}
+term measure
+apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
+apply (auto simp add: prod_eq_iff)
+apply (case_tac "k \<le> 2 * q")
+apply (rule diff_less_mono)
+apply auto
+done
+
+definition factorise :: "nat \<Rightarrow> nat list" where
+  "factorise n = factorise_from 2 n"
+
+
+subsection {* Concurrent computation via futures *}
+
+definition computation_harmonic :: "unit \<Rightarrow> rat" where
+  "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
+
+definition computation_primes :: "unit \<Rightarrow> nat list" where
+  "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
+
+definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where
+  "computation_future = Debug.timing (STR ''overall computation'')
+   (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
+     in (computation_primes (), Parallel.join c))"
+
+value [code] "computation_future ()"
+
+definition computation_factorise :: "nat \<Rightarrow> nat list" where
+  "computation_factorise = Debug.timing (STR ''factorise'') factorise"
+
+definition computation_parallel :: "unit \<Rightarrow> nat list list" where
+  "computation_parallel _ = Debug.timing (STR ''overall computation'')
+     (Parallel.map computation_factorise) [20000..<20100]"
+
+value [code] "computation_parallel ()"
+
+end
+

--- a/src/HOL/ex/ROOT.ML	Sat Jul 21 20:01:16 2012 +0200
+++ b/src/HOL/ex/ROOT.ML	Sun Jul 22 09:56:34 2012 +0200
@@ -73,7 +73,8 @@
   "Simproc_Tests",
   "Executable_Relation",
   "FinFunPred",
-  "Set_Comprehension_Pointfree_Tests"
+  "Set_Comprehension_Pointfree_Tests",
+  "Parallel_Example"
 ];
 
 use_thy "SVC_Oracle";