IOA/example/Multiset.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/example/Multiset.thy	Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,39 @@
+Multiset = Arith + "Lemmas" +
+
+types
+
+  'a multiset
+
+arities
+
+  multiset :: (term) term
+
+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"
+
+rules
+
+delm_empty_def
+  "delm({|},x) = {|}" 
+
+delm_nonempty_def
+  "delm(addm(M,x),y) == if(x=y,M,addm(delm(M,y),x))"
+
+countm_empty_def
+   "countm({|},P) == 0"
+
+countm_nonempty_def
+   "countm(addm(M,x),P) == countm(M,P) + if(P(x), Suc(0), 0)"
+
+count_def
+   "count(M,x) == countm(M, %y.y = x)"
+
+induction
+   "[| P({|}); !!M x. P(M) ==> P(addm(M,x)) |] ==> P(M)"
+
+end