5 |
5 |
6 Axiomatic multisets. |
6 Axiomatic multisets. |
7 Should be done as a subtype and moved to a global place. |
7 Should be done as a subtype and moved to a global place. |
8 *) |
8 *) |
9 |
9 |
10 goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def] |
10 Goalw [Multiset.count_def, Multiset.countm_empty_def] |
11 "count {|} x = 0"; |
11 "count {|} x = 0"; |
12 by (rtac refl 1); |
12 by (rtac refl 1); |
13 qed "count_empty"; |
13 qed "count_empty"; |
14 |
14 |
15 goal Multiset.thy |
15 Goal |
16 "count (addm M x) y = (if y=x then Suc(count M y) else count M y)"; |
16 "count (addm M x) y = (if y=x then Suc(count M y) else count M y)"; |
17 by (asm_simp_tac (simpset() addsimps |
17 by (asm_simp_tac (simpset() addsimps |
18 [Multiset.count_def,Multiset.countm_nonempty_def]) 1); |
18 [Multiset.count_def,Multiset.countm_nonempty_def]) 1); |
19 qed "count_addm_simp"; |
19 qed "count_addm_simp"; |
20 |
20 |
21 goal Multiset.thy "count M y <= count (addm M x) y"; |
21 Goal "count M y <= count (addm M x) y"; |
22 by (simp_tac (simpset() addsimps [count_addm_simp]) 1); |
22 by (simp_tac (simpset() addsimps [count_addm_simp]) 1); |
23 qed "count_leq_addm"; |
23 qed "count_leq_addm"; |
24 |
24 |
25 goalw Multiset.thy [Multiset.count_def] |
25 Goalw [Multiset.count_def] |
26 "count (delm M x) y = (if y=x then count M y - 1 else count M y)"; |
26 "count (delm M x) y = (if y=x then count M y - 1 else count M y)"; |
27 by (res_inst_tac [("M","M")] Multiset.induction 1); |
27 by (res_inst_tac [("M","M")] Multiset.induction 1); |
28 by (asm_simp_tac (simpset() |
28 by (asm_simp_tac (simpset() |
29 addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1); |
29 addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1); |
30 by (asm_full_simp_tac (simpset() |
30 by (asm_full_simp_tac (simpset() |
32 Multiset.countm_nonempty_def]) 1); |
32 Multiset.countm_nonempty_def]) 1); |
33 by Safe_tac; |
33 by Safe_tac; |
34 by (Asm_full_simp_tac 1); |
34 by (Asm_full_simp_tac 1); |
35 qed "count_delm_simp"; |
35 qed "count_delm_simp"; |
36 |
36 |
37 goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"; |
37 Goal "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"; |
38 by (res_inst_tac [("M","M")] Multiset.induction 1); |
38 by (res_inst_tac [("M","M")] Multiset.induction 1); |
39 by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1); |
39 by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1); |
40 by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1); |
40 by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1); |
41 auto(); |
41 auto(); |
42 qed "countm_props"; |
42 qed "countm_props"; |
43 |
43 |
44 goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"; |
44 Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"; |
45 by (res_inst_tac [("M","M")] Multiset.induction 1); |
45 by (res_inst_tac [("M","M")] Multiset.induction 1); |
46 by (simp_tac (simpset() addsimps [Multiset.delm_empty_def, |
46 by (simp_tac (simpset() addsimps [Multiset.delm_empty_def, |
47 Multiset.countm_empty_def]) 1); |
47 Multiset.countm_empty_def]) 1); |
48 by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def, |
48 by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def, |
49 Multiset.delm_nonempty_def]) 1); |
49 Multiset.delm_nonempty_def]) 1); |
50 qed "countm_spurious_delm"; |
50 qed "countm_spurious_delm"; |
51 |
51 |
52 |
52 |
53 goal Multiset.thy "!!P. P(x) ==> 0<count M x --> 0<countm M P"; |
53 Goal "!!P. P(x) ==> 0<count M x --> 0<countm M P"; |
54 by (res_inst_tac [("M","M")] Multiset.induction 1); |
54 by (res_inst_tac [("M","M")] Multiset.induction 1); |
55 by (simp_tac (simpset() addsimps |
55 by (simp_tac (simpset() addsimps |
56 [Multiset.delm_empty_def,Multiset.count_def, |
56 [Multiset.delm_empty_def,Multiset.count_def, |
57 Multiset.countm_empty_def]) 1); |
57 Multiset.countm_empty_def]) 1); |
58 by (asm_simp_tac (simpset() addsimps |
58 by (asm_simp_tac (simpset() addsimps |
59 [Multiset.count_def,Multiset.delm_nonempty_def, |
59 [Multiset.count_def,Multiset.delm_nonempty_def, |
60 Multiset.countm_nonempty_def]) 1); |
60 Multiset.countm_nonempty_def]) 1); |
61 qed_spec_mp "pos_count_imp_pos_countm"; |
61 qed_spec_mp "pos_count_imp_pos_countm"; |
62 |
62 |
63 goal Multiset.thy |
63 Goal |
64 "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1"; |
64 "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1"; |
65 by (res_inst_tac [("M","M")] Multiset.induction 1); |
65 by (res_inst_tac [("M","M")] Multiset.induction 1); |
66 by (simp_tac (simpset() addsimps |
66 by (simp_tac (simpset() addsimps |
67 [Multiset.delm_empty_def, |
67 [Multiset.delm_empty_def, |
68 Multiset.countm_empty_def]) 1); |
68 Multiset.countm_empty_def]) 1); |