equal
deleted
inserted
replaced
1 (* Title: HOL/IOA/example/Multiset.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow & Konrad Slind |
|
4 Copyright 1994 TU Muenchen |
|
5 |
|
6 Axiomatic multisets. |
|
7 Should be done as a subtype and moved to a global place. |
|
8 *) |
|
9 |
|
10 Multiset = Arith + "Lemmas" + |
|
11 |
|
12 types |
|
13 |
|
14 'a multiset |
|
15 |
|
16 arities |
|
17 |
|
18 multiset :: (term) term |
|
19 |
|
20 consts |
|
21 |
|
22 "{|}" :: "'a multiset" ("{|}") |
|
23 addm :: "['a multiset, 'a] => 'a multiset" |
|
24 delm :: "['a multiset, 'a] => 'a multiset" |
|
25 countm :: "['a multiset, 'a => bool] => nat" |
|
26 count :: "['a multiset, 'a] => nat" |
|
27 |
|
28 rules |
|
29 |
|
30 delm_empty_def |
|
31 "delm({|},x) = {|}" |
|
32 |
|
33 delm_nonempty_def |
|
34 "delm(addm(M,x),y) == if(x=y,M,addm(delm(M,y),x))" |
|
35 |
|
36 countm_empty_def |
|
37 "countm({|},P) == 0" |
|
38 |
|
39 countm_nonempty_def |
|
40 "countm(addm(M,x),P) == countm(M,P) + if(P(x), Suc(0), 0)" |
|
41 |
|
42 count_def |
|
43 "count(M,x) == countm(M, %y.y = x)" |
|
44 |
|
45 induction |
|
46 "[| P({|}); !!M x. P(M) ==> P(addm(M,x)) |] ==> P(M)" |
|
47 |
|
48 end |
|