1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Parallel_Example.thy Sun Jul 22 09:56:34 2012 +0200
1.3 @@ -0,0 +1,108 @@
1.4 +header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
1.5 +
1.6 +theory Parallel_Example
1.7 +imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
1.8 +begin
1.9 +
1.10 +subsection {* Compute-intensive examples. *}
1.11 +
1.12 +subsubsection {* Fragments of the harmonic series *}
1.13 +
1.14 +definition harmonic :: "nat \<Rightarrow> rat" where
1.15 + "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
1.16 +
1.17 +
1.18 +subsubsection {* The sieve of Erathostenes *}
1.19 +
1.20 +text {*
1.21 + The attentive reader may relate this ad-hoc implementation to the
1.22 + arithmetic notion of prime numbers as a little exercise.
1.23 +*}
1.24 +
1.25 +primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where
1.26 + "mark _ _ [] = []"
1.27 +| "mark m n (p # ps) = (case n of 0 \<Rightarrow> False # mark m m ps
1.28 + | Suc n \<Rightarrow> p # mark m n ps)"
1.29 +
1.30 +lemma length_mark [simp]:
1.31 + "length (mark m n ps) = length ps"
1.32 + by (induct ps arbitrary: n) (simp_all split: nat.split)
1.33 +
1.34 +function sieve :: "nat \<Rightarrow> bool list \<Rightarrow> bool list" where
1.35 + "sieve m ps = (case dropWhile Not ps
1.36 + of [] \<Rightarrow> ps
1.37 + | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
1.38 +by pat_completeness auto
1.39 +
1.40 +termination -- {* tuning of this proof is left as an exercise to the reader *}
1.41 + apply (relation "measure (length \<circ> snd)")
1.42 + apply rule
1.43 + apply (auto simp add: length_dropWhile_le)
1.44 +proof -
1.45 + fix ps qs q
1.46 + assume "dropWhile Not ps = q # qs"
1.47 + then have "length (q # qs) = length (dropWhile Not ps)" by simp
1.48 + then have "length qs < length (dropWhile Not ps)" by simp
1.49 + moreover have "length (dropWhile Not ps) \<le> length ps"
1.50 + by (simp add: length_dropWhile_le)
1.51 + ultimately show "length qs < length ps" by auto
1.52 +qed
1.53 +
1.54 +primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
1.55 + "natify _ [] = []"
1.56 +| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
1.57 +
1.58 +primrec list_primes where
1.59 + "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
1.60 +
1.61 +
1.62 +subsubsection {* Naive factorisation *}
1.63 +
1.64 +function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
1.65 + "factorise_from k n = (if 1 < k \<and> k \<le> n
1.66 + then
1.67 + let (q, r) = divmod_nat n k
1.68 + in if r = 0 then k # factorise_from k q
1.69 + else factorise_from (Suc k) n
1.70 + else [])"
1.71 +by pat_completeness auto
1.72 +
1.73 +termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *}
1.74 +term measure
1.75 +apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
1.76 +apply (auto simp add: prod_eq_iff)
1.77 +apply (case_tac "k \<le> 2 * q")
1.78 +apply (rule diff_less_mono)
1.79 +apply auto
1.80 +done
1.81 +
1.82 +definition factorise :: "nat \<Rightarrow> nat list" where
1.83 + "factorise n = factorise_from 2 n"
1.84 +
1.85 +
1.86 +subsection {* Concurrent computation via futures *}
1.87 +
1.88 +definition computation_harmonic :: "unit \<Rightarrow> rat" where
1.89 + "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
1.90 +
1.91 +definition computation_primes :: "unit \<Rightarrow> nat list" where
1.92 + "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
1.93 +
1.94 +definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where
1.95 + "computation_future = Debug.timing (STR ''overall computation'')
1.96 + (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
1.97 + in (computation_primes (), Parallel.join c))"
1.98 +
1.99 +value [code] "computation_future ()"
1.100 +
1.101 +definition computation_factorise :: "nat \<Rightarrow> nat list" where
1.102 + "computation_factorise = Debug.timing (STR ''factorise'') factorise"
1.103 +
1.104 +definition computation_parallel :: "unit \<Rightarrow> nat list list" where
1.105 + "computation_parallel _ = Debug.timing (STR ''overall computation'')
1.106 + (Parallel.map computation_factorise) [20000..<20100]"
1.107 +
1.108 +value [code] "computation_parallel ()"
1.109 +
1.110 +end
1.111 +