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: tip2.html   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/ex/Code_Binary_Nat_examples.thy
    Author:     Florian Haftmann, TU Muenchen
*)

section \<open>Simple examples for natural numbers implemented in binary representation.\<close>

theory Code_Binary_Nat_examples
imports Complex_Main "HOL-Library.Code_Binary_Nat"
begin

fun to_n :: "nat \ nat list"
where
  "to_n 0 = []"
| "to_n (Suc 0) = []"
| "to_n (Suc (Suc 0)) = []"
| "to_n (Suc n) = n # to_n n"

definition naive_prime :: "nat \ bool"
where
  "naive_prime n \ n \ 2 \ filter (\m. n mod m = 0) (to_n n) = []"

primrec fac :: "nat \ nat"
where
  "fac 0 = 1"
| "fac (Suc n) = Suc n * fac n"

primrec harmonic :: "nat \ rat"
where
  "harmonic 0 = 0"
| "harmonic (Suc n) = 1 / of_nat (Suc n) + harmonic n"

lemma "harmonic 200 \ 5"
  by eval

lemma "(let (q, r) = quotient_of (harmonic 8) in q div r) \ 2"
  by normalization

lemma "naive_prime 89"
  by eval

lemma "naive_prime 89"
  by normalization

lemma "\ naive_prime 87"
  by eval

lemma "\ naive_prime 87"
  by normalization

lemma "fac 10 > 3000000"
  by eval

lemma "fac 10 > 3000000"
  by normalization

end


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.9Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff