1.1 --- a/src/HOL/IsaMakefile	Sat Jul 21 20:01:16 2012 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sun Jul 22 09:56:34 2012 +0200
     1.3 @@ -452,6 +452,7 @@
     1.4    Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
     1.5    Library/Continuity.thy						\
     1.6    Library/Convex.thy Library/Countable.thy				\
     1.7 +  Library/Debug.thy							\
     1.8    Library/Dlist.thy Library/Eval_Witness.thy				\
     1.9    Library/DAList.thy Library/Dlist.thy					\
    1.10    Library/Eval_Witness.thy						\
    1.11 @@ -470,6 +471,7 @@
    1.12    Library/Multiset.thy Library/Nat_Bijection.thy			\
    1.13    Library/Numeral_Type.thy Library/Old_Recdef.thy			\
    1.14    Library/OptionalSugar.thy Library/Order_Relation.thy			\
    1.15 +  Library/Parallel.thy							\
    1.16    Library/Permutation.thy Library/Permutations.thy			\
    1.17    Library/Phantom_Type.thy Library/Poly_Deriv.thy			\
    1.18    Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
    1.19 @@ -1034,6 +1036,7 @@
    1.20    ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy	\
    1.21    ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy			\
    1.22    ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy	\
    1.23 +  ex/Parallel_Example.thy						\
    1.24    ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy				\
    1.25    ex/Quicksort.thy ex/ROOT.ML						\
    1.26    ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Debug.thy	Sun Jul 22 09:56:34 2012 +0200
     2.3 @@ -0,0 +1,40 @@
     2.4 +(* Author: Florian Haftmann, TU Muenchen *)
     2.5 +
     2.6 +header {* Debugging facilities for code generated towards Isabelle/ML *}
     2.7 +
     2.8 +theory Debug
     2.9 +imports Main
    2.10 +begin
    2.11 +
    2.12 +definition trace :: "String.literal \<Rightarrow> unit" where
    2.13 +  [simp]: "trace s = ()"
    2.14 +
    2.15 +definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
    2.16 +  [simp]: "tracing s = id"
    2.17 +
    2.18 +lemma [code]:
    2.19 +  "tracing s = (let u = trace s in id)"
    2.20 +  by simp
    2.21 +
    2.22 +definition flush :: "'a \<Rightarrow> unit" where
    2.23 +  [simp]: "flush x = ()"
    2.24 +
    2.25 +definition flushing :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" where
    2.26 +  [simp]: "flushing x = id"
    2.27 +
    2.28 +lemma [code, code_unfold]:
    2.29 +  "flushing x = (let u = flush x in id)"
    2.30 +  by simp
    2.31 +
    2.32 +definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    2.33 +  [simp]: "timing s f x = f x"
    2.34 +
    2.35 +code_const trace and flush and timing
    2.36 +  (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
    2.37 +
    2.38 +code_reserved Eval Output PolyML Timing
    2.39 +
    2.40 +hide_const (open) trace tracing flush flushing timing
    2.41 +
    2.42 +end
    2.43 +

     3.1 --- a/src/HOL/Library/Library.thy	Sat Jul 21 20:01:16 2012 +0200
     3.2 +++ b/src/HOL/Library/Library.thy	Sun Jul 22 09:56:34 2012 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4    ContNotDenum
     3.5    Convex
     3.6    Countable
     3.7 +  Debug
     3.8    Dlist
     3.9    Eval_Witness
    3.10    Extended_Nat
    3.11 @@ -37,6 +38,7 @@
    3.12    Old_Recdef
    3.13    OptionalSugar
    3.14    Option_ord
    3.15 +  Parallel
    3.16    Permutation
    3.17    Permutations
    3.18    Poly_Deriv

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Parallel.thy	Sun Jul 22 09:56:34 2012 +0200
     4.3 @@ -0,0 +1,67 @@
     4.4 +(* Author: Florian Haftmann, TU Muenchen *)
     4.5 +
     4.6 +header {* Futures and parallel lists for code generated towards Isabelle/ML *}
     4.7 +
     4.8 +theory Parallel
     4.9 +imports Main
    4.10 +begin
    4.11 +
    4.12 +subsection {* Futures *}
    4.13 +
    4.14 +datatype 'a future = fork "unit \<Rightarrow> 'a"
    4.15 +
    4.16 +primrec join :: "'a future \<Rightarrow> 'a" where
    4.17 +  "join (fork f) = f ()"
    4.18 +
    4.19 +lemma future_eqI [intro!]:
    4.20 +  assumes "join f = join g"
    4.21 +  shows "f = g"
    4.22 +  using assms by (cases f, cases g) (simp add: ext)
    4.23 +
    4.24 +code_type future
    4.25 +  (Eval "_ future")
    4.26 +
    4.27 +code_const fork
    4.28 +  (Eval "Future.fork")
    4.29 +
    4.30 +code_const join
    4.31 +  (Eval "Future.join")
    4.32 +
    4.33 +code_reserved Eval Future future
    4.34 +
    4.35 +
    4.36 +subsection {* Parallel lists *}
    4.37 +
    4.38 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    4.39 +  [simp]: "map = List.map"
    4.40 +
    4.41 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    4.42 +  "forall = list_all"
    4.43 +
    4.44 +lemma forall_all [simp]:
    4.45 +  "forall P xs \<longleftrightarrow> (\<forall>x\<in>set xs. P x)"
    4.46 +  by (simp add: forall_def list_all_iff)
    4.47 +
    4.48 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
    4.49 +  "exists = list_ex"
    4.50 +
    4.51 +lemma exists_ex [simp]:
    4.52 +  "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
    4.53 +  by (simp add: exists_def list_ex_iff)
    4.54 +
    4.55 +code_const map
    4.56 +  (Eval "Par'_List.map")
    4.57 +
    4.58 +code_const forall
    4.59 +  (Eval "Par'_List.forall")
    4.60 +
    4.61 +code_const exists
    4.62 +  (Eval "Par'_List.exists")
    4.63 +
    4.64 +code_reserved Eval Par_List
    4.65 +
    4.66 +
    4.67 +hide_const (open) fork join map exists forall
    4.68 +
    4.69 +end
    4.70 +

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/ex/Parallel_Example.thy	Sun Jul 22 09:56:34 2012 +0200
     5.3 @@ -0,0 +1,108 @@
     5.4 +header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *}
     5.5 +
     5.6 +theory Parallel_Example
     5.7 +imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug"
     5.8 +begin
     5.9 +
    5.10 +subsection {* Compute-intensive examples. *}
    5.11 +
    5.12 +subsubsection {* Fragments of the harmonic series *}
    5.13 +
    5.14 +definition harmonic :: "nat \<Rightarrow> rat" where
    5.15 +  "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])"
    5.16 +
    5.17 +
    5.18 +subsubsection {* The sieve of Erathostenes *}
    5.19 +
    5.20 +text {*
    5.21 +  The attentive reader may relate this ad-hoc implementation to the
    5.22 +  arithmetic notion of prime numbers as a little exercise.
    5.23 +*}
    5.24 +
    5.25 +primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where
    5.26 +  "mark _ _ [] = []"
    5.27 +| "mark m n (p # ps) = (case n of 0 \<Rightarrow> False # mark m m ps
    5.28 +    | Suc n \<Rightarrow> p # mark m n ps)"
    5.29 +
    5.30 +lemma length_mark [simp]:
    5.31 +  "length (mark m n ps) = length ps"
    5.32 +  by (induct ps arbitrary: n) (simp_all split: nat.split)
    5.33 +
    5.34 +function sieve :: "nat \<Rightarrow> bool list \<Rightarrow> bool list" where
    5.35 +  "sieve m ps = (case dropWhile Not ps
    5.36 +   of [] \<Rightarrow> ps
    5.37 +    | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
    5.38 +by pat_completeness auto
    5.39 +
    5.40 +termination -- {* tuning of this proof is left as an exercise to the reader *}
    5.41 +  apply (relation "measure (length \<circ> snd)")
    5.42 +  apply rule
    5.43 +  apply (auto simp add: length_dropWhile_le)
    5.44 +proof -
    5.45 +  fix ps qs q
    5.46 +  assume "dropWhile Not ps = q # qs"
    5.47 +  then have "length (q # qs) = length (dropWhile Not ps)" by simp
    5.48 +  then have "length qs < length (dropWhile Not ps)" by simp
    5.49 +  moreover have "length (dropWhile Not ps) \<le> length ps"
    5.50 +    by (simp add: length_dropWhile_le)
    5.51 +  ultimately show "length qs < length ps" by auto
    5.52 +qed
    5.53 +
    5.54 +primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where
    5.55 +  "natify _ [] = []"
    5.56 +| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
    5.57 +
    5.58 +primrec list_primes where
    5.59 +  "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
    5.60 +
    5.61 +
    5.62 +subsubsection {* Naive factorisation *}
    5.63 +
    5.64 +function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
    5.65 +  "factorise_from k n = (if 1 < k \<and> k \<le> n
    5.66 +    then
    5.67 +      let (q, r) = divmod_nat n k 
    5.68 +      in if r = 0 then k # factorise_from k q
    5.69 +        else factorise_from (Suc k) n
    5.70 +    else [])" 
    5.71 +by pat_completeness auto
    5.72 +
    5.73 +termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *}
    5.74 +term measure
    5.75 +apply (relation "measure (\<lambda>(k, n). 2 * n - k)")
    5.76 +apply (auto simp add: prod_eq_iff)
    5.77 +apply (case_tac "k \<le> 2 * q")
    5.78 +apply (rule diff_less_mono)
    5.79 +apply auto
    5.80 +done
    5.81 +
    5.82 +definition factorise :: "nat \<Rightarrow> nat list" where
    5.83 +  "factorise n = factorise_from 2 n"
    5.84 +
    5.85 +
    5.86 +subsection {* Concurrent computation via futures *}
    5.87 +
    5.88 +definition computation_harmonic :: "unit \<Rightarrow> rat" where
    5.89 +  "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
    5.90 +
    5.91 +definition computation_primes :: "unit \<Rightarrow> nat list" where
    5.92 +  "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
    5.93 +
    5.94 +definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where
    5.95 +  "computation_future = Debug.timing (STR ''overall computation'')
    5.96 +   (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
    5.97 +     in (computation_primes (), Parallel.join c))"
    5.98 +
    5.99 +value [code] "computation_future ()"
   5.100 +
   5.101 +definition computation_factorise :: "nat \<Rightarrow> nat list" where
   5.102 +  "computation_factorise = Debug.timing (STR ''factorise'') factorise"
   5.103 +
   5.104 +definition computation_parallel :: "unit \<Rightarrow> nat list list" where
   5.105 +  "computation_parallel _ = Debug.timing (STR ''overall computation'')
   5.106 +     (Parallel.map computation_factorise) [20000..<20100]"
   5.107 +
   5.108 +value [code] "computation_parallel ()"
   5.109 +
   5.110 +end
   5.111 +

     6.1 --- a/src/HOL/ex/ROOT.ML	Sat Jul 21 20:01:16 2012 +0200
     6.2 +++ b/src/HOL/ex/ROOT.ML	Sun Jul 22 09:56:34 2012 +0200
     6.3 @@ -73,7 +73,8 @@
     6.4    "Simproc_Tests",
     6.5    "Executable_Relation",
     6.6    "FinFunPred",
     6.7 -  "Set_Comprehension_Pointfree_Tests"
     6.8 +  "Set_Comprehension_Pointfree_Tests",
     6.9 +  "Parallel_Example"
    6.10  ];
    6.11  
    6.12  use_thy "SVC_Oracle";