1(* Title: HOL/Corec_Examples/Tests/Type_Class.thy 2 Author: Andreas Lochbihler, ETH Zuerich 3 Author: Jasmin Blanchette, Inria, LORIA, MPII 4 Copyright 2016 5 6Tests type class instances as friends. 7*) 8 9section \<open>Tests Type Class Instances as Friends\<close> 10 11theory Type_Class 12imports "HOL-Library.BNF_Corec" "HOL-Library.Stream" 13begin 14 15instantiation stream :: (plus) plus 16begin 17 18definition plus_stream where "plus_stream s1 s2 = smap (\<lambda>(x, y). x + y) (sproduct s1 s2)" 19 20instance .. 21 22end 23 24friend_of_corec plus (* :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" *) where 25 "s1 + s2 = SCons (shd s1 + shd s2) (stl s1 + stl s2)" 26 sorry 27 28corec ff :: "('a::plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 29 "ff xs ys = SCons (shd xs + shd ys) (ff (stl xs) ys) + SCons (shd xs) (ff xs (stl ys))" 30 31end 32