Quelle Paper_Examples.thy Sprache: Isabelle

(*  Title:      HOL/Corec_Examples/Paper_Examples.thy
    Author:     Andreas Lochbihler, ETH Zuerich
    Author:     Andrei Popescu, TU Muenchen
    Copyright   2016

Small examples from the paper "Friends with Benefits".
*)

section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>

theory Paper_Examples
imports "HOL-Library.BNF_Corec" "HOL-Library.FSet" Complex_Main
begin

section \<open>Examples from the introduction\<close>

codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") (infixr \<open>\<lhd>\<close> 65)

corec "natsFrom" :: "nat \ nat stream" where
  "natsFrom n = n \ natsFrom (n + 1)"

corec (friend) add1 :: "nat stream \ nat stream"
where "add1 ns = (shd ns + 1) \ add1 (stl ns)"

corec natsFrom' :: "nat \ nat stream" where
  "natsFrom' n = n \ add1 (natsFrom' n)"

section \<open>Examples from section 3\<close>

text \<open>We curry the example functions in this section because infix syntax works only for curried functions.\<close>

corec (friend) Plus :: "nat stream \ nat stream \ nat stream" (infix \\\ 67) where
  "x\<^sub>1 \ x\<^sub>2 = (shd x\<^sub>1 + shd x\<^sub>2) \ (stl x\<^sub>1 \ stl x\<^sub>2)"

section \<open>Examples from section 4\<close>

codatatype 'a llist = LNil | LCons 'a "'a llist"

corec collatz :: "nat \ nat llist" where
  "collatz n = (if n \ 1 then LNil
     else if even n then collatz (n div 2)
     else LCons n (collatz (3 * n + 1)))"

datatype 'a nelist = NEList (hd:'a) (tl:"'a list")

primrec (transfer) snoc :: "'a list \ 'a \ 'a nelist" (infix \\\ 64) where
"[] \ a = NEList a []"
|"(b # bs) \ a = NEList b (bs @ [a])"

corec (friend) inter :: "nat stream nelist \ nat stream" where
"inter xss = shd (hd xss) \ inter (tl xss \ stl (hd xss))"

corec (friend) inter' :: "nat stream nelist \ nat stream" where
"inter' xss = (case hd xss of x \ xs \ x \ inter' (tl xss \ xs))"

corec zero :: "nat stream" where "zero = 0 \ zero"

section \<open>Examples from Blanchette et al. (ICFP 2015)\<close>

corec oneTwos :: "nat stream" where "oneTwos = 1 \ 2 \ oneTwos"

corec everyOther :: "'a stream \ 'a stream"
where "everyOther xs = shd xs \ everyOther (stl (stl xs))"

corec fibA :: "nat stream"
where "fibA = 0 \ (1 \ fibA \ fibA)"

corec fibB :: "nat stream"
where "fibB = (0 \ 1 \ fibB) \ (0 \ fibB)"

corec (friend) times :: "nat stream \ nat stream \ nat stream" (infix \\\ 69)
where "xs \ ys = (shd xs * shd ys) \ xs \ stl ys \ stl xs \ ys"

corec (friend) exp :: "nat stream \ nat stream"
where "exp xs = 2 ^ shd xs \ (stl xs \ exp xs)"

corec facA :: "nat stream"
where "facA = (1 \ facA) \ (1 \ facA)"

corec facB :: "nat stream"
where "facB = exp (0 \ facB)"

corec (friend) sfsup :: "nat stream fset \ nat stream"
where "sfsup X = Sup (fset (fimage shd X)) \ sfsup (fimage stl X)"

codatatype tree = Node (val: nat) (sub: "tree list")

corec (friend) tplus :: "tree \ tree \ tree"
where "tplus t u = Node (val t + val u) (map (\(t', u'). tplus t' u') (zip (sub t) (sub u)))"

corec (friend) ttimes :: "tree \ tree \ tree"
where "ttimes t u = Node (val t * val u)
  (map (\<lambda>(t, u). tplus (ttimes t u) (ttimes t u)) (zip (sub t) (sub u)))"

corecursive primes :: "nat \ nat \ nat stream"
where "primes m n =
  (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
apply (relation "measure (\(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
   apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
   apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
  done

corec facC :: "nat \ nat \ nat \ nat stream"
where "facC n a i = (if i = 0 then a \ facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"

corec catalan :: "nat \ nat stream"
where "catalan n = (if n > 0 then catalan (n - 1) \ (0 \ catalan (n + 1)) else 1 \ catalan 1)"

corec (friend) heart :: "nat stream \ nat stream \ nat stream" (infix \\\ 65)
where "xs \ ys = SCons (shd xs * shd ys) ((((xs \ stl ys) \ (stl xs \ ys)) \ ys) \ ys)"

corec (friend) g :: "'a stream \ 'a stream"
where "g xs = shd xs \ g (g (stl xs))"

end

quality100%

¤ Dauer der Verarbeitung: 0.11 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.