1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Multiset.v,v 1.9.2.1 2004/07/16 19:31:17 herbelin Exp $ i*)
37 include "Sets/Permut.ma".
40 Set Implicit Arguments.
48 cic:/Coq/Sets/Multiset/multiset_defs/A.var
52 cic:/Coq/Sets/Multiset/multiset_defs/eqA.var
56 cic:/Coq/Sets/Multiset/multiset_defs/Aeq_dec.var
59 inline procedural "cic:/Coq/Sets/Multiset/multiset.ind".
61 inline procedural "cic:/Coq/Sets/Multiset/EmptyBag.con" as definition.
63 inline procedural "cic:/Coq/Sets/Multiset/SingletonBag.con" as definition.
65 inline procedural "cic:/Coq/Sets/Multiset/multiplicity.con" as definition.
67 (*#* multiset equality *)
69 inline procedural "cic:/Coq/Sets/Multiset/meq.con" as definition.
72 Hint Unfold meq multiplicity.
75 inline procedural "cic:/Coq/Sets/Multiset/meq_refl.con" as lemma.
78 Hint Resolve meq_refl.
81 inline procedural "cic:/Coq/Sets/Multiset/meq_trans.con" as lemma.
83 inline procedural "cic:/Coq/Sets/Multiset/meq_sym.con" as lemma.
86 Hint Immediate meq_sym.
89 (*#* multiset union *)
91 inline procedural "cic:/Coq/Sets/Multiset/munion.con" as definition.
93 inline procedural "cic:/Coq/Sets/Multiset/munion_empty_left.con" as lemma.
96 Hint Resolve munion_empty_left.
99 inline procedural "cic:/Coq/Sets/Multiset/munion_empty_right.con" as lemma.
101 include "Arith/Plus.ma".
103 (* comm. and ass. of plus *)
105 inline procedural "cic:/Coq/Sets/Multiset/munion_comm.con" as lemma.
108 Hint Resolve munion_comm.
111 inline procedural "cic:/Coq/Sets/Multiset/munion_ass.con" as lemma.
114 Hint Resolve munion_ass.
117 inline procedural "cic:/Coq/Sets/Multiset/meq_left.con" as lemma.
120 Hint Resolve meq_left.
123 inline procedural "cic:/Coq/Sets/Multiset/meq_right.con" as lemma.
126 Hint Resolve meq_right.
129 (*#* Here we should make multiset an abstract datatype, by hiding [Bag],
130 [munion], [multiplicity]; all further properties are proved abstractly *)
132 inline procedural "cic:/Coq/Sets/Multiset/munion_rotate.con" as lemma.
134 inline procedural "cic:/Coq/Sets/Multiset/meq_congr.con" as lemma.
136 inline procedural "cic:/Coq/Sets/Multiset/munion_perm_left.con" as lemma.
138 inline procedural "cic:/Coq/Sets/Multiset/multiset_twist1.con" as lemma.
140 inline procedural "cic:/Coq/Sets/Multiset/multiset_twist2.con" as lemma.
142 (*#* specific for treesort *)
144 inline procedural "cic:/Coq/Sets/Multiset/treesort_twist1.con" as lemma.
146 inline procedural "cic:/Coq/Sets/Multiset/treesort_twist2.con" as lemma.
148 (*i theory of minter to do similarly
150 (* multiset intersection *)
151 Definition minter := [m1,m2:multiset]
152 (Bag [a:A](min (multiplicity m1 a)(multiplicity m2 a))).
160 Unset Implicit Arguments.
164 Hint Unfold meq multiplicity: v62 datatypes.
168 Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
169 munion_empty_left: v62 datatypes.
173 Hint Immediate meq_sym: v62 datatypes.