author | wenzelm |
Sat, 18 Jul 2015 20:54:56 +0200 | |
changeset 60754 | 02924903a6fd |
parent 58880 | 0baae4311a9f |
child 62002 | f1599e98c4d0 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/IOA/NTP/Multiset.thy |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow & Konrad Slind |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
*) |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
|
58880 | 5 |
section {* Axiomatic multisets *} |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
|
17244 | 7 |
theory Multiset |
8 |
imports Lemmas |
|
9 |
begin |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
|
17244 | 11 |
typedecl |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
'a multiset |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
consts |
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
|
41310 | 16 |
emptym :: "'a multiset" ("{|}") |
17244 | 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" |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
|
47026 | 22 |
axiomatization where |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
23 |
|
17244 | 24 |
delm_empty_def: |
47026 | 25 |
"delm {|} x = {|}" and |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
|
17244 | 27 |
delm_nonempty_def: |
47026 | 28 |
"delm (addm M x) y == (if x=y then M else addm (delm M y) x)" and |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
|
17244 | 30 |
countm_empty_def: |
47026 | 31 |
"countm {|} P == 0" and |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
|
17244 | 33 |
countm_nonempty_def: |
47026 | 34 |
"countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" and |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
|
17244 | 36 |
count_def: |
47026 | 37 |
"count M x == countm M (%y. y = x)" and |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
|
17244 | 39 |
"induction": |
47026 | 40 |
"\<And>P M. [| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)" |
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
|
19739 | 42 |
lemma count_empty: |
43 |
"count {|} x = 0" |
|
44 |
by (simp add: Multiset.count_def Multiset.countm_empty_def) |
|
45 |
||
46 |
lemma 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 |
||
50 |
lemma count_leq_addm: "count M y <= count (addm M x) y" |
|
51 |
by (simp add: count_addm_simp) |
|
52 |
||
53 |
lemma count_delm_simp: |
|
54 |
"count (delm M x) y = (if y=x then count M y - 1 else count M y)" |
|
55 |
apply (unfold Multiset.count_def) |
|
56 |
apply (rule_tac M = "M" in Multiset.induction) |
|
57 |
apply (simp (no_asm_simp) add: Multiset.delm_empty_def Multiset.countm_empty_def) |
|
58 |
apply (simp add: Multiset.delm_nonempty_def Multiset.countm_nonempty_def) |
|
59 |
apply safe |
|
60 |
apply simp |
|
61 |
done |
|
62 |
||
63 |
lemma countm_props: "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)" |
|
64 |
apply (rule_tac M = "M" in Multiset.induction) |
|
65 |
apply (simp (no_asm) add: Multiset.countm_empty_def) |
|
66 |
apply (simp (no_asm) add: Multiset.countm_nonempty_def) |
|
67 |
apply auto |
|
68 |
done |
|
69 |
||
70 |
lemma 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 |
||
25161 | 77 |
lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P > 0" |
19739 | 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) |
|
25161 | 80 |
apply (simp add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def) |
19739 | 81 |
done |
82 |
||
83 |
lemma 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) |
|
25161 | 87 |
apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) |
19739 | 88 |
apply auto |
89 |
done |
|
90 |
||
91 |
||
92 |
declare count_addm_simp [simp] count_delm_simp [simp] |
|
93 |
Multiset.countm_empty_def [simp] Multiset.delm_empty_def [simp] count_empty [simp] |
|
17244 | 94 |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
95 |
end |