library theories for debugging and parallel computing using code generation towards Isabelle/ML
1 header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
3 theory Parallel_Example
4 imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
7 subsection {* Compute-intensive examples. *}
9 subsubsection {* Fragments of the harmonic series *}
11 definition harmonic :: "nat \<Rightarrow> rat" where
12 "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
15 subsubsection {* The sieve of Erathostenes *}
18 The attentive reader may relate this ad-hoc implementation to the
19 arithmetic notion of prime numbers as a little exercise.
22 primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where
24 | "mark m n (p # ps) = (case n of 0 \<Rightarrow> False # mark m m ps
25 | Suc n \<Rightarrow> p # mark m n ps)"
27 lemma length_mark [simp]:
28 "length (mark m n ps) = length ps"
29 by (induct ps arbitrary: n) (simp_all split: nat.split)
31 function sieve :: "nat \<Rightarrow> bool list \<Rightarrow> bool list" where
32 "sieve m ps = (case dropWhile Not ps
33 of [] \<Rightarrow> ps
34 | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
35 by pat_completeness auto
37 termination -- {* tuning of this proof is left as an exercise to the reader *}
38 apply (relation "measure (length \<circ> snd)")
40 apply (auto simp add: length_dropWhile_le)
43 assume "dropWhile Not ps = q # qs"
44 then have "length (q # qs) = length (dropWhile Not ps)" by simp
45 then have "length qs < length (dropWhile Not ps)" by simp
46 moreover have "length (dropWhile Not ps) \<le> length ps"
47 by (simp add: length_dropWhile_le)
48 ultimately show "length qs < length ps" by auto
51 primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
53 | "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
55 primrec list_primes where
56 "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
59 subsubsection {* Naive factorisation *}
61 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
62 "factorise_from k n = (if 1 < k \<and> k \<le> n
64 let (q, r) = divmod_nat n k
65 in if r = 0 then k # factorise_from k q
66 else factorise_from (Suc k) n
68 by pat_completeness auto
70 termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *}
72 apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
73 apply (auto simp add: prod_eq_iff)
74 apply (case_tac "k \<le> 2 * q")
75 apply (rule diff_less_mono)
79 definition factorise :: "nat \<Rightarrow> nat list" where
80 "factorise n = factorise_from 2 n"
83 subsection {* Concurrent computation via futures *}
85 definition computation_harmonic :: "unit \<Rightarrow> rat" where
86 "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
88 definition computation_primes :: "unit \<Rightarrow> nat list" where
89 "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
91 definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where
92 "computation_future = Debug.timing (STR ''overall computation'')
93 (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
94 in (computation_primes (), Parallel.join c))"
96 value [code] "computation_future ()"
98 definition computation_factorise :: "nat \<Rightarrow> nat list" where
99 "computation_factorise = Debug.timing (STR ''factorise'') factorise"
101 definition computation_parallel :: "unit \<Rightarrow> nat list list" where
102 "computation_parallel _ = Debug.timing (STR ''overall computation'')
103 (Parallel.map computation_factorise) [20000..<20100]"
105 value [code] "computation_parallel ()"