# HG changeset patch # User blanchet # Date 1464690283 -7200 # Node ID 3e79279c10ca0032d9173bed0edec29aa4bc7274 # Parent d5974697765bb20fcfb4c6b167988748b03f046e added test diff -r d5974697765b -r 3e79279c10ca src/HOL/Corec_Examples/Tests/Type_Class.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Corec_Examples/Tests/Type_Class.thy Tue May 31 12:24:43 2016 +0200 @@ -0,0 +1,31 @@ +(* Title: HOL/Corec_Examples/Tests/Type_Class.thy + Author: Andreas Lochbihler, ETH Zuerich + Author: Jasmin Blanchette, Inria, LORIA, MPII + Copyright 2016 + +Tests type class instances as friends. +*) + +section \Tests Type Class Instances as Friends\ + +theory Type_Class +imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream" +begin + +instantiation stream :: (plus) plus +begin + +definition plus_stream where "plus_stream s1 s2 = smap (\(x, y). x + y) (sproduct s1 s2)" + +instance .. + +end + +friend_of_corec plus (* :: "'a stream \ 'a stream \ 'a stream" *) where + "s1 + s2 = SCons (shd s1 + shd s2) (stl s1 + stl s2)" + sorry + +corec ff :: "('a::plus) stream \ 'a stream \ 'a stream" where + "ff xs ys = SCons (shd xs + shd ys) (ff (stl xs) ys) + SCons (shd xs) (ff xs (stl ys))" + +end diff -r d5974697765b -r 3e79279c10ca src/HOL/ROOT --- a/src/HOL/ROOT Tue May 31 11:54:45 2016 +0200 +++ b/src/HOL/ROOT Tue May 31 12:24:43 2016 +0200 @@ -832,6 +832,7 @@ "Tests/Small_Concrete" "Tests/Stream_Friends" "Tests/TLList_Friends" + "Tests/Type_Class" session "HOL-Word" (main) in Word = HOL + theories Word