summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Tue, 31 May 2016 12:24:43 +0200 | |

changeset 63190 | 3e79279c10ca |

parent 63189 | d5974697765b |

child 63191 | 0b7bdb75f451 |

child 63192 | a742d309afa2 |

child 63194 | c3896c385c3e |

added test

src/HOL/Corec_Examples/Tests/Type_Class.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ROOT | file | annotate | diff | comparison | revisions |

--- /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 \<open>Tests Type Class Instances as Friends\<close> + +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 (\<lambda>(x, y). x + y) (sproduct s1 s2)" + +instance .. + +end + +friend_of_corec plus (* :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" *) where + "s1 + s2 = SCons (shd s1 + shd s2) (stl s1 + stl s2)" + sorry + +corec ff :: "('a::plus) stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where + "ff xs ys = SCons (shd xs + shd ys) (ff (stl xs) ys) + SCons (shd xs) (ff xs (stl ys))" + +end