src/HOL/Corec_Examples/Paper_Examples.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66453 cc19f7ca2ed6
child 67051 e7e54a0b9197
permissions -rw-r--r--
tuned;
blanchet@62734
     1
(*  Title:      HOL/Corec_Examples/Paper_Examples.thy
blanchet@62734
     2
    Author:     Andreas Lochbihler, ETH Zuerich
blanchet@62734
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@62734
     4
    Copyright   2016
blanchet@62734
     5
blanchet@63406
     6
Small examples from the paper "Friends with Benefits".
blanchet@62734
     7
*)
blanchet@62734
     8
blanchet@63406
     9
section \<open>Small Examples from the Paper ``Friends with Benefits''\<close>
blanchet@62734
    10
blanchet@62734
    11
theory Paper_Examples
wenzelm@66453
    12
imports "HOL-Library.BNF_Corec" "HOL-Library.FSet" Complex_Main
blanchet@62734
    13
begin
blanchet@62734
    14
blanchet@63406
    15
section \<open>Examples from the introduction\<close>
blanchet@62734
    16
blanchet@63406
    17
codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") (infixr "\<lhd>" 65)
blanchet@62734
    18
blanchet@63406
    19
corec "natsFrom" :: "nat \<Rightarrow> nat stream" where
blanchet@63406
    20
  "natsFrom n = n \<lhd> natsFrom (n + 1)"
blanchet@62734
    21
blanchet@63408
    22
corec (friend) add1 :: "nat stream \<Rightarrow> nat stream"
blanchet@63468
    23
where "add1 ns = (shd ns + 1) \<lhd> add1 (stl ns)"
blanchet@62734
    24
blanchet@63406
    25
corec natsFrom' :: "nat \<Rightarrow> nat stream" where
blanchet@63408
    26
  "natsFrom' n = n \<lhd> add1 (natsFrom' n)"
blanchet@62734
    27
blanchet@63406
    28
section \<open>Examples from section 3\<close>
blanchet@62734
    29
blanchet@63406
    30
text \<open>We curry the example functions in this section because infix syntax works only for curried functions.\<close>
blanchet@62734
    31
blanchet@62734
    32
corec (friend) Plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>" 67) where
blanchet@63406
    33
  "x\<^sub>1 \<oplus> x\<^sub>2 = (shd x\<^sub>1 + shd x\<^sub>2) \<lhd> (stl x\<^sub>1 \<oplus> stl x\<^sub>2)"
blanchet@62734
    34
blanchet@63406
    35
section \<open>Examples from section 4\<close>
blanchet@62734
    36
blanchet@63408
    37
codatatype 'a llist = LNil | LCons 'a "'a llist"
blanchet@63408
    38
blanchet@63408
    39
corec collatz :: "nat \<Rightarrow> nat llist" where
blanchet@63408
    40
  "collatz n = (if n \<le> 1 then LNil
blanchet@63408
    41
     else if even n then collatz (n div 2)
blanchet@63408
    42
     else LCons n (collatz (3 * n + 1)))"
blanchet@62734
    43
blanchet@63406
    44
datatype 'a nelist = NEList (hd:'a) (tl:"'a list")
blanchet@63406
    45
blanchet@63408
    46
primrec (transfer) snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a nelist" (infix "\<rhd>" 64) where
blanchet@63406
    47
 "[] \<rhd> a = NEList a []"
blanchet@63406
    48
|"(b # bs) \<rhd> a = NEList b (bs @ [a])"
blanchet@63406
    49
blanchet@63406
    50
corec (friend) inter :: "nat stream nelist \<Rightarrow> nat stream" where
blanchet@63408
    51
"inter xss = shd (hd xss) \<lhd> inter (tl xss \<rhd> stl (hd xss))"
blanchet@63406
    52
blanchet@63408
    53
corec (friend) inter' :: "nat stream nelist \<Rightarrow> nat stream" where
blanchet@63408
    54
"inter' xss = (case hd xss of x \<lhd> xs \<Rightarrow> x \<lhd> inter' (tl xss \<rhd> xs))"
blanchet@63406
    55
blanchet@63406
    56
corec zero :: "nat stream" where "zero = 0 \<lhd> zero"
blanchet@63406
    57
blanchet@63406
    58
section \<open>Examples from Blanchette et al. (ICFP 2015)\<close>
blanchet@63406
    59
blanchet@63406
    60
corec oneTwos :: "nat stream" where "oneTwos = 1 \<lhd> 2 \<lhd> oneTwos"
blanchet@63406
    61
blanchet@63406
    62
corec everyOther :: "'a stream \<Rightarrow> 'a stream"
blanchet@63406
    63
where "everyOther xs = shd xs \<lhd> everyOther (stl (stl xs))"
blanchet@63406
    64
blanchet@63406
    65
corec fibA :: "nat stream"
blanchet@63406
    66
where "fibA = 0 \<lhd> (1 \<lhd> fibA \<oplus> fibA)"
blanchet@63406
    67
blanchet@63406
    68
corec fibB :: "nat stream"
blanchet@63406
    69
where "fibB = (0 \<lhd> 1 \<lhd> fibB) \<oplus> (0 \<lhd> fibB)"
blanchet@63406
    70
blanchet@63406
    71
corec (friend) times :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<otimes>" 69)
blanchet@63406
    72
where "xs \<otimes> ys = (shd xs * shd ys) \<lhd> xs \<otimes> stl ys \<oplus> stl xs \<otimes> ys"
blanchet@63406
    73
blanchet@63406
    74
corec (friend) exp :: "nat stream \<Rightarrow> nat stream"
blanchet@63406
    75
where "exp xs = 2 ^ shd xs \<lhd> (stl xs \<otimes> exp xs)"
blanchet@63406
    76
blanchet@63406
    77
corec facA :: "nat stream"
blanchet@63406
    78
where "facA = (1 \<lhd> facA) \<otimes> (1 \<lhd> facA)"
blanchet@63406
    79
blanchet@63406
    80
corec facB :: "nat stream"
blanchet@63406
    81
where "facB = exp (0 \<lhd> facB)"
blanchet@63406
    82
blanchet@63406
    83
corec (friend) sfsup :: "nat stream fset \<Rightarrow> nat stream"
blanchet@63406
    84
where "sfsup X = Sup (fset (fimage shd X)) \<lhd> sfsup (fimage stl X)"
blanchet@63406
    85
blanchet@63406
    86
codatatype tree = Node (val: nat) (sub: "tree list")
blanchet@63406
    87
blanchet@63406
    88
corec (friend) tplus :: "tree \<Rightarrow> tree \<Rightarrow> tree"
blanchet@63406
    89
where "tplus t u = Node (val t + val u) (map (\<lambda>(t', u'). tplus t' u') (zip (sub t) (sub u)))"
blanchet@63406
    90
blanchet@63406
    91
corec (friend) ttimes :: "tree \<Rightarrow> tree \<Rightarrow> tree"
blanchet@63408
    92
where "ttimes t u = Node (val t * val u)
blanchet@63408
    93
  (map (\<lambda>(t, u). tplus (ttimes t u) (ttimes t u)) (zip (sub t) (sub u)))"
blanchet@63406
    94
blanchet@63406
    95
corecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream"
blanchet@63406
    96
where "primes m n =
blanchet@63406
    97
  (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
blanchet@63406
    98
apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
blanchet@63406
    99
apply (auto simp: mod_Suc intro: Suc_lessI )
blanchet@63406
   100
apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
blanchet@63406
   101
by (metis diff_less_mono2 lessI mod_less_divisor)
blanchet@63406
   102
blanchet@63406
   103
corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
blanchet@63406
   104
where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
blanchet@63406
   105
blanchet@63406
   106
corec catalan :: "nat \<Rightarrow> nat stream"
blanchet@63406
   107
where "catalan n = (if n > 0 then catalan (n - 1) \<oplus> (0 \<lhd> catalan (n + 1)) else 1 \<lhd> catalan 1)"
blanchet@63406
   108
blanchet@63406
   109
corec (friend) heart :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<heartsuit>" 65)
blanchet@63406
   110
where "xs \<heartsuit> ys = SCons (shd xs * shd ys) ((((xs \<heartsuit> stl ys) \<oplus> (stl xs \<otimes> ys)) \<heartsuit> ys) \<otimes> ys)"
blanchet@63406
   111
blanchet@63406
   112
corec (friend) g :: "'a stream \<Rightarrow> 'a stream"
blanchet@63406
   113
where "g xs = shd xs \<lhd> g (g (stl xs))"
blanchet@63406
   114
blanchet@62734
   115
end