src/HOL/ex/Parallel_Example.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56927 4044a7d1720f
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
haftmann@48427
     1
header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
haftmann@48427
     2
haftmann@48427
     3
theory Parallel_Example
haftmann@48427
     4
imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
haftmann@48427
     5
begin
haftmann@48427
     6
haftmann@48427
     7
subsection {* Compute-intensive examples. *}
haftmann@48427
     8
haftmann@48427
     9
subsubsection {* Fragments of the harmonic series *}
haftmann@48427
    10
haftmann@48427
    11
definition harmonic :: "nat \<Rightarrow> rat" where
haftmann@48427
    12
  "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
haftmann@48427
    13
haftmann@48427
    14
haftmann@48427
    15
subsubsection {* The sieve of Erathostenes *}
haftmann@48427
    16
haftmann@48427
    17
text {*
haftmann@48427
    18
  The attentive reader may relate this ad-hoc implementation to the
haftmann@48427
    19
  arithmetic notion of prime numbers as a little exercise.
haftmann@48427
    20
*}
haftmann@48427
    21
haftmann@48427
    22
primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where
haftmann@48427
    23
  "mark _ _ [] = []"
haftmann@48427
    24
| "mark m n (p # ps) = (case n of 0 \<Rightarrow> False # mark m m ps
haftmann@48427
    25
    | Suc n \<Rightarrow> p # mark m n ps)"
haftmann@48427
    26
haftmann@48427
    27
lemma length_mark [simp]:
haftmann@48427
    28
  "length (mark m n ps) = length ps"
haftmann@48427
    29
  by (induct ps arbitrary: n) (simp_all split: nat.split)
haftmann@48427
    30
haftmann@48427
    31
function sieve :: "nat \<Rightarrow> bool list \<Rightarrow> bool list" where
haftmann@48427
    32
  "sieve m ps = (case dropWhile Not ps
haftmann@48427
    33
   of [] \<Rightarrow> ps
haftmann@48427
    34
    | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
haftmann@48427
    35
by pat_completeness auto
haftmann@48427
    36
haftmann@48427
    37
termination -- {* tuning of this proof is left as an exercise to the reader *}
haftmann@48427
    38
  apply (relation "measure (length \<circ> snd)")
haftmann@48427
    39
  apply rule
haftmann@48427
    40
  apply (auto simp add: length_dropWhile_le)
haftmann@48427
    41
proof -
haftmann@48427
    42
  fix ps qs q
haftmann@48427
    43
  assume "dropWhile Not ps = q # qs"
haftmann@48427
    44
  then have "length (q # qs) = length (dropWhile Not ps)" by simp
haftmann@48427
    45
  then have "length qs < length (dropWhile Not ps)" by simp
haftmann@48427
    46
  moreover have "length (dropWhile Not ps) \<le> length ps"
haftmann@48427
    47
    by (simp add: length_dropWhile_le)
haftmann@48427
    48
  ultimately show "length qs < length ps" by auto
haftmann@48427
    49
qed
haftmann@48427
    50
haftmann@48427
    51
primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
haftmann@48427
    52
  "natify _ [] = []"
haftmann@48427
    53
| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
haftmann@48427
    54
haftmann@48427
    55
primrec list_primes where
haftmann@48427
    56
  "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
haftmann@48427
    57
haftmann@48427
    58
haftmann@48427
    59
subsubsection {* Naive factorisation *}
haftmann@48427
    60
haftmann@48427
    61
function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
haftmann@48427
    62
  "factorise_from k n = (if 1 < k \<and> k \<le> n
haftmann@48427
    63
    then
haftmann@48427
    64
      let (q, r) = divmod_nat n k 
haftmann@48427
    65
      in if r = 0 then k # factorise_from k q
haftmann@48427
    66
        else factorise_from (Suc k) n
haftmann@48427
    67
    else [])" 
haftmann@48427
    68
by pat_completeness auto
haftmann@48427
    69
haftmann@48427
    70
termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *}
haftmann@48427
    71
term measure
haftmann@48427
    72
apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
haftmann@48427
    73
apply (auto simp add: prod_eq_iff)
haftmann@48427
    74
apply (case_tac "k \<le> 2 * q")
haftmann@48427
    75
apply (rule diff_less_mono)
haftmann@48427
    76
apply auto
haftmann@48427
    77
done
haftmann@48427
    78
haftmann@48427
    79
definition factorise :: "nat \<Rightarrow> nat list" where
haftmann@48427
    80
  "factorise n = factorise_from 2 n"
haftmann@48427
    81
haftmann@48427
    82
haftmann@48427
    83
subsection {* Concurrent computation via futures *}
haftmann@48427
    84
haftmann@48427
    85
definition computation_harmonic :: "unit \<Rightarrow> rat" where
haftmann@48427
    86
  "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
haftmann@48427
    87
haftmann@48427
    88
definition computation_primes :: "unit \<Rightarrow> nat list" where
haftmann@48427
    89
  "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
haftmann@48427
    90
haftmann@48427
    91
definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where
haftmann@48427
    92
  "computation_future = Debug.timing (STR ''overall computation'')
haftmann@48427
    93
   (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
haftmann@48427
    94
     in (computation_primes (), Parallel.join c))"
haftmann@48427
    95
haftmann@56927
    96
value "computation_future ()"
haftmann@48427
    97
haftmann@48427
    98
definition computation_factorise :: "nat \<Rightarrow> nat list" where
haftmann@48427
    99
  "computation_factorise = Debug.timing (STR ''factorise'') factorise"
haftmann@48427
   100
haftmann@48427
   101
definition computation_parallel :: "unit \<Rightarrow> nat list list" where
haftmann@48427
   102
  "computation_parallel _ = Debug.timing (STR ''overall computation'')
haftmann@48427
   103
     (Parallel.map computation_factorise) [20000..<20100]"
haftmann@48427
   104
haftmann@56927
   105
value "computation_parallel ()"
haftmann@48427
   106
haftmann@48427
   107
end
haftmann@48427
   108