src/HOL/ex/Parallel_Example.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61933 cf58b5b794b2
child 63882 018998c00003
permissions -rw-r--r--
bundle lifting_syntax;
     1 section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close>
     2 
     3 theory Parallel_Example
     4 imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
     5 begin
     6 
     7 subsection \<open>Compute-intensive examples.\<close>
     8 
     9 subsubsection \<open>Fragments of the harmonic series\<close>
    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 \<open>The sieve of Erathostenes\<close>
    16 
    17 text \<open>
    18   The attentive reader may relate this ad-hoc implementation to the
    19   arithmetic notion of prime numbers as a little exercise.
    20 \<close>
    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 \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
    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 \<open>Naive factorisation\<close>
    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) = Divides.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 \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
    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 \<open>Concurrent computation via futures\<close>
    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