--- a/src/HOLCF/IOA/NTP/Multiset.thy Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.thy Sat Sep 03 16:50:22 2005 +0200
@@ -1,47 +1,47 @@
(* Title: HOL/IOA/NTP/Multiset.thy
ID: $Id$
Author: Tobias Nipkow & Konrad Slind
-
-Axiomatic multisets.
-Should be done as a subtype and moved to a global place.
*)
-Multiset = Lemmas +
+header {* Axiomatic multisets *}
-types
+theory Multiset
+imports Lemmas
+begin
+typedecl
'a multiset
-arities
-
- multiset :: (type) type
-
consts
- "{|}" :: 'a multiset ("{|}")
- addm :: ['a multiset, 'a] => 'a multiset
- delm :: ['a multiset, 'a] => 'a multiset
- countm :: ['a multiset, 'a => bool] => nat
- count :: ['a multiset, 'a] => nat
+ "{|}" :: "'a multiset" ("{|}")
+ addm :: "['a multiset, 'a] => 'a multiset"
+ delm :: "['a multiset, 'a] => 'a multiset"
+ countm :: "['a multiset, 'a => bool] => nat"
+ count :: "['a multiset, 'a] => nat"
-rules
+axioms
-delm_empty_def
- "delm {|} x = {|}"
+delm_empty_def:
+ "delm {|} x = {|}"
-delm_nonempty_def
+delm_nonempty_def:
"delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
-countm_empty_def
+countm_empty_def:
"countm {|} P == 0"
-countm_nonempty_def
+countm_nonempty_def:
"countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
-count_def
+count_def:
"count M x == countm M (%y. y = x)"
-induction
+"induction":
"[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
+ML {* use_text Context.ml_output true
+ ("structure Multiset = struct " ^ legacy_bindings (the_context ()) ^ " end") *}
+ML {* open Multiset *}
+
end