10Sduke(* Title: HOL/Corec_Examples/Paper_Examples.thy 213268Srehn Author: Andreas Lochbihler, ETH Zuerich 30Sduke Author: Andrei Popescu, TU Muenchen 40Sduke Copyright 2016 50Sduke 60SdukeSmall examples from the paper "Friends with Benefits". 70Sduke*) 80Sduke 90Sdukesection \<open>Small Examples from the Paper ``Friends with Benefits''\<close> 100Sduke 110Sduketheory Paper_Examples 120Sdukeimports "HOL-Library.BNF_Corec" "HOL-Library.FSet" Complex_Main 130Sdukebegin 140Sduke 150Sdukesection \<open>Examples from the introduction\<close> 160Sduke 170Sdukecodatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") (infixr "\<lhd>" 65) 180Sduke 191472Strimscorec "natsFrom" :: "nat \<Rightarrow> nat stream" where 201472Strims "natsFrom n = n \<lhd> natsFrom (n + 1)" 211472Strims 220Sdukecorec (friend) add1 :: "nat stream \<Rightarrow> nat stream" 230Sdukewhere "add1 ns = (shd ns + 1) \<lhd> add1 (stl ns)" 240Sduke 251879Sstefankcorec natsFrom' :: "nat \<Rightarrow> nat stream" where 263883Stwisti "natsFrom' n = n \<lhd> add1 (natsFrom' n)" 271879Sstefank 281879Sstefanksection \<open>Examples from section 3\<close> 291879Sstefank 309685Smikaeltext \<open>We curry the example functions in this section because infix syntax works only for curried functions.\<close> 311879Sstefank 321879Sstefankcorec (friend) Plus :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<oplus>" 67) where 331879Sstefank "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)" 341879Sstefank 351879Sstefanksection \<open>Examples from section 4\<close> 361879Sstefank 371879Sstefankcodatatype 'a llist = LNil | LCons 'a "'a llist" 381879Sstefank 391879Sstefankcorec collatz :: "nat \<Rightarrow> nat llist" where 401879Sstefank "collatz n = (if n \<le> 1 then LNil 411879Sstefank else if even n then collatz (n div 2) 421879Sstefank else LCons n (collatz (3 * n + 1)))" 431879Sstefank 441879Sstefankdatatype 'a nelist = NEList (hd:'a) (tl:"'a list") 451879Sstefank 461879Sstefankprimrec (transfer) snoc :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a nelist" (infix "\<rhd>" 64) where 471879Sstefank "[] \<rhd> a = NEList a []" 481879Sstefank|"(b # bs) \<rhd> a = NEList b (bs @ [a])" 491879Sstefank 503864Sstefankcorec (friend) inter :: "nat stream nelist \<Rightarrow> nat stream" where 511879Sstefank"inter xss = shd (hd xss) \<lhd> inter (tl xss \<rhd> stl (hd xss))" 525853Szgu 5313249Sstefankcorec (friend) inter' :: "nat stream nelist \<Rightarrow> nat stream" where 541879Sstefank"inter' xss = (case hd xss of x \<lhd> xs \<Rightarrow> x \<lhd> inter' (tl xss \<rhd> xs))" 551879Sstefank 560Sdukecorec zero :: "nat stream" where "zero = 0 \<lhd> zero" 570Sduke 580Sdukesection \<open>Examples from Blanchette et al. (ICFP 2015)\<close> 590Sduke 600Sdukecorec oneTwos :: "nat stream" where "oneTwos = 1 \<lhd> 2 \<lhd> oneTwos" 610Sduke 620Sdukecorec everyOther :: "'a stream \<Rightarrow> 'a stream" 630Sdukewhere "everyOther xs = shd xs \<lhd> everyOther (stl (stl xs))" 640Sduke 650Sdukecorec fibA :: "nat stream" 660Sdukewhere "fibA = 0 \<lhd> (1 \<lhd> fibA \<oplus> fibA)" 670Sduke 680Sdukecorec fibB :: "nat stream" 690Sdukewhere "fibB = (0 \<lhd> 1 \<lhd> fibB) \<oplus> (0 \<lhd> fibB)" 700Sduke 710Sdukecorec (friend) times :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<otimes>" 69) 720Sdukewhere "xs \<otimes> ys = (shd xs * shd ys) \<lhd> xs \<otimes> stl ys \<oplus> stl xs \<otimes> ys" 730Sduke 740Sdukecorec (friend) exp :: "nat stream \<Rightarrow> nat stream" 750Sdukewhere "exp xs = 2 ^ shd xs \<lhd> (stl xs \<otimes> exp xs)" 760Sduke 7713076Smikaelcorec facA :: "nat stream" 780Sdukewhere "facA = (1 \<lhd> facA) \<otimes> (1 \<lhd> facA)" 7913076Smikael 800Sdukecorec facB :: "nat stream" 810Sdukewhere "facB = exp (0 \<lhd> facB)" 820Sduke 830Sdukecorec (friend) sfsup :: "nat stream fset \<Rightarrow> nat stream" 840Sdukewhere "sfsup X = Sup (fset (fimage shd X)) \<lhd> sfsup (fimage stl X)" 850Sduke 860Sdukecodatatype tree = Node (val: nat) (sub: "tree list") 870Sduke 880Sdukecorec (friend) tplus :: "tree \<Rightarrow> tree \<Rightarrow> tree" 890Sdukewhere "tplus t u = Node (val t + val u) (map (\<lambda>(t', u'). tplus t' u') (zip (sub t) (sub u)))" 900Sduke 910Sdukecorec (friend) ttimes :: "tree \<Rightarrow> tree \<Rightarrow> tree" 920Sdukewhere "ttimes t u = Node (val t * val u) 930Sduke (map (\<lambda>(t, u). tplus (ttimes t u) (ttimes t u)) (zip (sub t) (sub u)))" 940Sduke 950Sdukecorecursive primes :: "nat \<Rightarrow> nat \<Rightarrow> nat stream" 9650Sdcubedwhere "primes m n = 9750Sdcubed (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))" 9850Sdcubedapply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)") 9950Sdcubed apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE) 1004795Ssimonis apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel) 1014795Ssimonis done 1024795Ssimonis 1034795Ssimoniscorec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream" 10450Sdcubedwhere "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))" 1050Sduke 1060Sdukecorec catalan :: "nat \<Rightarrow> nat stream" 10750Sdcubedwhere "catalan n = (if n > 0 then catalan (n - 1) \<oplus> (0 \<lhd> catalan (n + 1)) else 1 \<lhd> catalan 1)" 1080Sduke 1090Sdukecorec (friend) heart :: "nat stream \<Rightarrow> nat stream \<Rightarrow> nat stream" (infix "\<heartsuit>" 65) 1100Sdukewhere "xs \<heartsuit> ys = SCons (shd xs * shd ys) ((((xs \<heartsuit> stl ys) \<oplus> (stl xs \<otimes> ys)) \<heartsuit> ys) \<otimes> ys)" 1110Sduke 1120Sdukecorec (friend) g :: "'a stream \<Rightarrow> 'a stream" 1130Sdukewhere "g xs = shd xs \<lhd> g (g (stl xs))" 1140Sduke 1150Sdukeend 1160Sduke