Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/ex/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle Parallel_Example.thy Sprache: Isabelle

section ‹A simple example demonstrating parallelism for code generated towards Isabelle/ML›

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

subsection ‹Compute-intensive examples.›

subsubsection ‹Fragments of the harmonic series›

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

subsubsection ‹The sieve of Erathostenes›

text ‹
  The attentive reader may relate this ad-hoc implementation to the
  arithmetic notion of prime numbers as a little exercise.
›

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 ==> 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 [] ==> ps
    | p#ps' \ let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
by pat_completeness auto

termination 🍋 ‹tuning of this proof is left as an exercise to the reader›
  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 qs < length (dropWhile Not ps)"
    by simp
  also have "length (dropWhile Not ps) \ length ps"
    by (simp add: length_dropWhile_le)
  finally show "length qs < length ps" .
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 ‹Naive factorisation›

function factorise_from :: "nat \ nat \ nat list" where
  "factorise_from k n = (if 1 < k \ k \ n
    then
      let (q, r) = Euclidean_Rings.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 🍋 ‹tuning of this proof is left as an exercise to the reader›
  apply (relation "measure (\(k, n). 2 * n - k)")
  apply (auto simp add: Euclidean_Rings.divmod_nat_def algebra_simps elim!: dvdE)
  subgoal for m n
    apply (cases "m \ n * 2")
     apply (auto intro: diff_less_mono)
    done
  done

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

subsection ‹Concurrent computation via futures›

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'')
   (λ() ==> 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

Messung V0.5

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.