src/HOL/HOLCF/IOA/NTP/Multiset.thy
changeset 47026 36dacca8a95c
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Mar 19 21:49:52 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Mon Mar 19 21:52:09 2012 +0100
     1.3 @@ -19,25 +19,25 @@
     1.4    countm :: "['a multiset, 'a => bool] => nat"
     1.5    count  :: "['a multiset, 'a] => nat"
     1.6  
     1.7 -axioms
     1.8 +axiomatization where
     1.9  
    1.10  delm_empty_def:
    1.11 -  "delm {|} x = {|}"
    1.12 +  "delm {|} x = {|}" and
    1.13  
    1.14  delm_nonempty_def:
    1.15 -  "delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
    1.16 +  "delm (addm M x) y == (if x=y then M else addm (delm M y) x)" and
    1.17  
    1.18  countm_empty_def:
    1.19 -   "countm {|} P == 0"
    1.20 +   "countm {|} P == 0" and
    1.21  
    1.22  countm_nonempty_def:
    1.23 -   "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
    1.24 +   "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" and
    1.25  
    1.26  count_def:
    1.27 -   "count M x == countm M (%y. y = x)"
    1.28 +   "count M x == countm M (%y. y = x)" and
    1.29  
    1.30  "induction":
    1.31 -   "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
    1.32 +   "\<And>P M. [| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
    1.33  
    1.34  lemma count_empty: 
    1.35     "count {|} x = 0"