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