diff -r f04b33ce250f -r a4dc62a46ee4 IOA/example/Multiset.thy --- a/IOA/example/Multiset.thy Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* Title: HOL/IOA/example/Multiset.thy - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -Axiomatic multisets. -Should be done as a subtype and moved to a global place. -*) - -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