equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/MultisetOrder |
1 (* Title: HOL/Induct/MultisetOrder.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
5 |
6 Multisets are partially ordered |
6 Multisets are partially ordered. |
7 *) |
7 *) |
8 |
8 |
9 MultisetOrder = Multiset + |
9 theory MultisetOrder = Multiset: |
10 |
10 |
11 instance multiset :: (order) order |
11 instance multiset :: (order) order |
12 (mult_le_refl,mult_le_trans,mult_le_antisym,mult_less_le) |
12 apply intro_classes |
|
13 apply (rule mult_le_refl) |
|
14 apply (erule mult_le_trans) |
|
15 apply assumption |
|
16 apply (erule mult_le_antisym) |
|
17 apply assumption |
|
18 apply (rule mult_less_le) |
|
19 done |
13 |
20 |
14 instance multiset :: (term) plus_ac0 (union_commute,union_assoc) {|Auto_tac|} |
21 instance multiset :: ("term") plus_ac0 |
|
22 apply intro_classes |
|
23 apply (rule union_commute) |
|
24 apply (rule union_assoc) |
|
25 apply simp |
|
26 done |
|
27 |
15 end |
28 end |