1(*  Title:      HOL/HOLCF/IOA/NTP/Multiset.thy
2    Author:     Tobias Nipkow & Konrad Slind
3*)
4
5section \<open>Axiomatic multisets\<close>
6
7theory Multiset
8imports Lemmas
9begin
10
11typedecl
12  'a multiset
13
14consts
15
16  emptym :: "'a multiset"                        ("{|}")
17  addm   :: "['a multiset, 'a] => 'a multiset"
18  delm   :: "['a multiset, 'a] => 'a multiset"
19  countm :: "['a multiset, 'a => bool] => nat"
20  count  :: "['a multiset, 'a] => nat"
21
22axiomatization where
23
24delm_empty_def:
25  "delm {|} x = {|}" and
26
27delm_nonempty_def:
28  "delm (addm M x) y == (if x=y then M else addm (delm M y) x)" and
29
30countm_empty_def:
31   "countm {|} P == 0" and
32
33countm_nonempty_def:
34   "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" and
35
36count_def:
37   "count M x == countm M (%y. y = x)" and
38
39"induction":
40   "\<And>P M. [| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
41
42lemma count_empty: 
43   "count {|} x = 0"
44  by (simp add: Multiset.count_def Multiset.countm_empty_def)
45
46lemma count_addm_simp: 
47     "count (addm M x) y = (if y=x then Suc(count M y) else count M y)"
48  by (simp add: Multiset.count_def Multiset.countm_nonempty_def)
49
50lemma count_leq_addm: "count M y <= count (addm M x) y"
51  by (simp add: count_addm_simp)
52
53lemma count_delm_simp: 
54     "count (delm M x) y = (if y=x then count M y - 1 else count M y)"
55apply (unfold Multiset.count_def)
56apply (rule_tac M = "M" in Multiset.induction)
57apply (simp (no_asm_simp) add: Multiset.delm_empty_def Multiset.countm_empty_def)
58apply (simp add: Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
59apply safe
60apply simp
61done
62
63lemma countm_props: "\<And>M. (\<forall>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (countm M P \<le> countm M Q)"
64apply (rule_tac M = "M" in Multiset.induction)
65 apply (simp (no_asm) add: Multiset.countm_empty_def)
66apply (simp (no_asm) add: Multiset.countm_nonempty_def)
67apply auto
68done
69
70lemma countm_spurious_delm: "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"
71  apply (rule_tac M = "M" in Multiset.induction)
72  apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def)
73  apply (simp (no_asm_simp) add: Multiset.countm_nonempty_def Multiset.delm_nonempty_def)
74  done
75
76
77lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P > 0"
78  apply (rule_tac M = "M" in Multiset.induction)
79  apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def)
80  apply (simp add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
81  done
82
83lemma countm_done_delm: 
84   "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1"
85  apply (rule_tac M = "M" in Multiset.induction)
86  apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def)
87  apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
88  apply auto
89  done
90
91
92declare count_addm_simp [simp] count_delm_simp [simp]
93  Multiset.countm_empty_def [simp] Multiset.delm_empty_def [simp] count_empty [simp]
94
95end
96