|
7626
|
1 |
(* Title: HOL/BCV/Plus.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
|
|
|
6 |
Supremum operation on various domains.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Plus = Orders +
|
|
|
10 |
|
|
|
11 |
instance option :: (plus)plus
|
|
|
12 |
instance list :: (plus)plus
|
|
|
13 |
instance "*" :: (plus,plus)plus
|
|
|
14 |
|
|
|
15 |
consts list_plus :: "('a::plus)list => 'a list => 'a list"
|
|
|
16 |
primrec
|
|
|
17 |
"list_plus [] ys = ys"
|
|
|
18 |
"list_plus (x#xs) ys = (case ys of [] => x#xs | z#zs => (x+z)#list_plus xs zs)"
|
|
|
19 |
defs
|
|
|
20 |
plus_option "o1 + o2 == case o1 of None => o2
|
|
|
21 |
| Some x => (case o2 of None => o1
|
|
|
22 |
| Some y => Some(x+y))"
|
|
|
23 |
plus_list "op + == list_plus"
|
|
|
24 |
plus_prod "op + == %(a,b) (c,d). (a+c,b+d)"
|
|
|
25 |
|
|
|
26 |
end
|