products/Sources/formale Sprachen/Isabelle/HOL/ex/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: interval_taylor.prf   Sprache: Isabelle

Original von: Isabelle©
section \<open>A simple example demonstrating parallelism for code generated towards Isabelle/ML\<close>

theory Parallel_Example
imports Complex_Main "HOL-Library.Parallel" "HOL-Library.Debug"
begin

subsection \<open>Compute-intensive examples.\<close>

subsubsection \<open>Fragments of the harmonic series\<close>

definition harmonic :: "nat \ rat" where
  "harmonic n = sum_list (map (\n. 1 / of_nat n) [1..


subsubsection \<open>The sieve of Erathostenes\<close>

text \<open>
  The attentive reader may relate this ad-hoc implementation to the
  arithmetic notion of prime numbers as a little exercise.
\<close>

primrec mark :: "nat \ nat \ bool list \ bool list" where
  "mark _ _ [] = []"
| "mark m n (p # ps) = (case n of 0 \ False # mark m m ps
    | Suc n \<Rightarrow> p # mark m n ps)"

lemma length_mark [simp]:
  "length (mark m n ps) = length ps"
  by (induct ps arbitrary: n) (simp_all split: nat.split)

function sieve :: "nat \ bool list \ bool list" where
  "sieve m ps = (case dropWhile Not ps
   of [] \<Rightarrow> ps
    | p#ps' \ let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
by pat_completeness auto

termination \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
  apply (relation "measure (length \ snd)")
  apply rule
  apply (auto simp add: length_dropWhile_le)
proof -
  fix ps qs q
  assume "dropWhile Not ps = q # qs"
  then have "length (q # qs) = length (dropWhile Not ps)" by simp
  then have "length qs < length (dropWhile Not ps)" by simp
  moreover have "length (dropWhile Not ps) \ length ps"
    by (simp add: length_dropWhile_le)
  ultimately show "length qs < length ps" by auto
qed

primrec natify :: "nat \ bool list \ nat list" where
  "natify _ [] = []"
| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"

primrec list_primes where
  "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"


subsubsection \<open>Naive factorisation\<close>

function factorise_from :: "nat \ nat \ nat list" where
  "factorise_from k n = (if 1 < k \ k \ n
    then
      let (q, r) = Divides.divmod_nat n k 
      in if r = 0 then k # factorise_from k q
        else factorise_from (Suc k) n
    else [])"
by pat_completeness auto

termination factorise_from \<comment> \<open>tuning of this proof is left as an exercise to the reader\<close>
  apply (relation "measure (\(k, n). 2 * n - k)")
    apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
  apply (case_tac "k \ ka * 2")
   apply (auto intro: diff_less_mono)
  done

definition factorise :: "nat \ nat list" where
  "factorise n = factorise_from 2 n"


subsection \<open>Concurrent computation via futures\<close>

definition computation_harmonic :: "unit \ rat" where
  "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"

definition computation_primes :: "unit \ nat list" where
  "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"

definition computation_future :: "unit \ nat list \ rat" where
  "computation_future = Debug.timing (STR ''overall computation'')
   (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic
     in (computation_primes (), Parallel.join c))"

value "computation_future ()"

definition computation_factorise :: "nat \ nat list" where
  "computation_factorise = Debug.timing (STR ''factorise'') factorise"

definition computation_parallel :: "unit \ nat list list" where
  "computation_parallel _ = Debug.timing (STR ''overall computation'')
     (Parallel.map computation_factorise) [20000..<20100]"

value "computation_parallel ()"

end

¤ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff