| author | wenzelm |
| Mon, 03 Nov 1997 14:06:27 +0100 | |
| changeset 4098 | 71e05eb27fb6 |
| parent 3073 | 88366253a09a |
| child 4377 | 2cba48b0f1c4 |
| permissions | -rw-r--r-- |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/IOA/NTP/Multiset.ML |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow & Konrad Slind |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
4 |
Copyright 1994 TU Muenchen |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
5 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
6 |
Axiomatic multisets. |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
7 |
Should be done as a subtype and moved to a global place. |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
8 |
*) |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
9 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
10 |
goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
11 |
"count {|} x = 0";
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
12 |
by (rtac refl 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
13 |
qed "count_empty"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
14 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
15 |
goal Multiset.thy |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
16 |
"count (addm M x) y = (if y=x then Suc(count M y) else count M y)"; |
| 4098 | 17 |
by (asm_simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
18 |
[Multiset.count_def,Multiset.countm_nonempty_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
19 |
setloop (split_tac [expand_if])) 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
20 |
qed "count_addm_simp"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
21 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
22 |
goal Multiset.thy "count M y <= count (addm M x) y"; |
| 4098 | 23 |
by (simp_tac (simpset() addsimps [count_addm_simp] |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
24 |
setloop (split_tac [expand_if])) 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
25 |
qed "count_leq_addm"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
26 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
27 |
goalw Multiset.thy [Multiset.count_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
28 |
"count (delm M x) y = (if y=x then pred(count M y) else count M y)"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
29 |
by (res_inst_tac [("M","M")] Multiset.induction 1);
|
| 4098 | 30 |
by (asm_simp_tac (simpset() |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
31 |
addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
32 |
setloop (split_tac [expand_if])) 1); |
| 4098 | 33 |
by (asm_full_simp_tac (simpset() |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
34 |
addsimps [Multiset.delm_nonempty_def, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
35 |
Multiset.countm_nonempty_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
36 |
setloop (split_tac [expand_if])) 1); |
| 4098 | 37 |
by (safe_tac (claset())); |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
38 |
by (Asm_full_simp_tac 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
39 |
qed "count_delm_simp"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
40 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
41 |
goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
42 |
by (res_inst_tac [("M","M")] Multiset.induction 1);
|
| 4098 | 43 |
by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1); |
44 |
by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1); |
|
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
45 |
by (etac (less_eq_add_cong RS mp RS mp) 1); |
| 4098 | 46 |
by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq] |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
47 |
setloop (split_tac [expand_if])) 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
48 |
qed "countm_props"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
49 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
50 |
goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
51 |
by (res_inst_tac [("M","M")] Multiset.induction 1);
|
| 4098 | 52 |
by (simp_tac (simpset() addsimps [Multiset.delm_empty_def, |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
53 |
Multiset.countm_empty_def]) 1); |
| 4098 | 54 |
by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def, |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
55 |
Multiset.delm_nonempty_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
56 |
setloop (split_tac [expand_if])) 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
57 |
qed "countm_spurious_delm"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
58 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
59 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
60 |
goal Multiset.thy "!!P. P(x) ==> 0<count M x --> 0<countm M P"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
61 |
by (res_inst_tac [("M","M")] Multiset.induction 1);
|
| 4098 | 62 |
by (simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
63 |
[Multiset.delm_empty_def,Multiset.count_def, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
64 |
Multiset.countm_empty_def]) 1); |
| 4098 | 65 |
by (asm_simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
66 |
[Multiset.count_def,Multiset.delm_nonempty_def, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
67 |
Multiset.countm_nonempty_def] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
68 |
setloop (split_tac [expand_if])) 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
69 |
val pos_count_imp_pos_countm = store_thm("pos_count_imp_pos_countm", standard(result() RS mp));
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
70 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
71 |
goal Multiset.thy |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
72 |
"!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
73 |
by (res_inst_tac [("M","M")] Multiset.induction 1);
|
| 4098 | 74 |
by (simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
75 |
[Multiset.delm_empty_def, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
76 |
Multiset.countm_empty_def]) 1); |
| 4098 | 77 |
by (asm_simp_tac (simpset() addsimps |
|
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
78 |
[eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
79 |
Multiset.countm_nonempty_def,pos_count_imp_pos_countm, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
80 |
suc_pred_id] |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
81 |
setloop (split_tac [expand_if])) 1); |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
82 |
qed "countm_done_delm"; |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
83 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
84 |
|
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
85 |
Addsimps [count_addm_simp, count_delm_simp, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
86 |
Multiset.countm_empty_def, Multiset.delm_empty_def, |
|
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset
|
87 |
count_empty]; |