Theory Paper_Examples

(*  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 ‹Small Examples from the Paper ``Friends with Benefits''›

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

section ‹Examples from the introduction›

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 ‹Examples from section 3›

text ‹We curry the example functions in this section because infix syntax works only for curried functions.›

corec (friend) Plus :: "nat stream ⇒ nat stream ⇒ nat stream" (infix "⊕" 67) where
  "x1 ⊕ x2 = (shd x1 + shd x2) ⊲ (stl x1 ⊕ stl x2)"

section ‹Examples from section 4›

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 ‹Examples from Blanchette et al. (ICFP 2015)›

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 (λ(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 ∧ n > 1) ∨ coprime m n then n ⊲ 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