src/HOL/ex/Parallel_Example.thy
 author wenzelm Mon Aug 31 21:28:08 2015 +0200 (2015-08-31) changeset 61070 b72a990adfe2 parent 58889 5b7a9633cfa8 child 61343 5b5656a63bd6 permissions -rw-r--r--
prefer symbols;
```     1 section {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
```
```     2
```
```     3 theory Parallel_Example
```
```     4 imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
```
```     5 begin
```
```     6
```
```     7 subsection {* Compute-intensive examples. *}
```
```     8
```
```     9 subsubsection {* Fragments of the harmonic series *}
```
```    10
```
```    11 definition harmonic :: "nat \<Rightarrow> rat" where
```
```    12   "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
```
```    13
```
```    14
```
```    15 subsubsection {* The sieve of Erathostenes *}
```
```    16
```
```    17 text {*
```
```    18   The attentive reader may relate this ad-hoc implementation to the
```
```    19   arithmetic notion of prime numbers as a little exercise.
```
```    20 *}
```
```    21
```
```    22 primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where
```
```    23   "mark _ _ [] = []"
```
```    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)"
```
```    26
```
```    27 lemma length_mark [simp]:
```
```    28   "length (mark m n ps) = length ps"
```
```    29   by (induct ps arbitrary: n) (simp_all split: nat.split)
```
```    30
```
```    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
```
```    36
```
```    37 termination -- {* tuning of this proof is left as an exercise to the reader *}
```
```    38   apply (relation "measure (length \<circ> snd)")
```
```    39   apply rule
```
```    40   apply (auto simp add: length_dropWhile_le)
```
```    41 proof -
```
```    42   fix ps qs q
```
```    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
```
```    49 qed
```
```    50
```
```    51 primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
```
```    52   "natify _ [] = []"
```
```    53 | "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
```
```    54
```
```    55 primrec list_primes where
```
```    56   "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
```
```    57
```
```    58
```
```    59 subsubsection {* Naive factorisation *}
```
```    60
```
```    61 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
```
```    62   "factorise_from k n = (if 1 < k \<and> k \<le> n
```
```    63     then
```
```    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
```
```    67     else [])"
```
```    68 by pat_completeness auto
```
```    69
```
```    70 termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *}
```
```    71 term measure
```
```    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)
```
```    76 apply auto
```
```    77 done
```
```    78
```
```    79 definition factorise :: "nat \<Rightarrow> nat list" where
```
```    80   "factorise n = factorise_from 2 n"
```
```    81
```
```    82
```
```    83 subsection {* Concurrent computation via futures *}
```
```    84
```
```    85 definition computation_harmonic :: "unit \<Rightarrow> rat" where
```
```    86   "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
```
```    87
```
```    88 definition computation_primes :: "unit \<Rightarrow> nat list" where
```
```    89   "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
```
```    90
```
```    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))"
```
```    95
```
```    96 value "computation_future ()"
```
```    97
```
```    98 definition computation_factorise :: "nat \<Rightarrow> nat list" where
```
```    99   "computation_factorise = Debug.timing (STR ''factorise'') factorise"
```
```   100
```
```   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]"
```
```   104
```
```   105 value "computation_parallel ()"
```
```   106
```
```   107 end
```
```   108
```