|
(* 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 "\" 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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
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.
|
