author  wenzelm 
Mon, 22 Jun 1998 17:13:09 +0200  
changeset 5068  fb28eaa07e01 
parent 4833  2e53109d4bc8 
child 5132  24f992a25adc 
permissions  rwrr 
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 

5068  10 
Goalw [Multiset.count_def, Multiset.countm_empty_def] 
3073
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 

5068  15 
Goal 
3073
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 
4833  18 
[Multiset.count_def,Multiset.countm_nonempty_def]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

19 
qed "count_addm_simp"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

20 

5068  21 
Goal "count M y <= count (addm M x) y"; 
4833  22 
by (simp_tac (simpset() addsimps [count_addm_simp]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

23 
qed "count_leq_addm"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

24 

5068  25 
Goalw [Multiset.count_def] 
4710  26 
"count (delm M x) y = (if y=x then count M y  1 else count M y)"; 
4833  27 
by (res_inst_tac [("M","M")] Multiset.induction 1); 
28 
by (asm_simp_tac (simpset() 

29 
addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1); 

30 
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

31 
addsimps [Multiset.delm_nonempty_def, 
4833  32 
Multiset.countm_nonempty_def]) 1); 
33 
by Safe_tac; 

34 
by (Asm_full_simp_tac 1); 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

35 
qed "count_delm_simp"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

36 

5068  37 
Goal "!!M. (!x. P(x) > Q(x)) ==> (countm M P <= countm M Q)"; 
4681  38 
by (res_inst_tac [("M","M")] Multiset.induction 1); 
39 
by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1); 

40 
by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1); 

41 
auto(); 

3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

42 
qed "countm_props"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

43 

5068  44 
Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

45 
by (res_inst_tac [("M","M")] Multiset.induction 1); 
4098  46 
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

47 
Multiset.countm_empty_def]) 1); 
4098  48 
by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def, 
4833  49 
Multiset.delm_nonempty_def]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

50 
qed "countm_spurious_delm"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

51 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

52 

5068  53 
Goal "!!P. P(x) ==> 0<count M x > 0<countm M P"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

54 
by (res_inst_tac [("M","M")] Multiset.induction 1); 
4098  55 
by (simp_tac (simpset() addsimps 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

56 
[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

57 
Multiset.countm_empty_def]) 1); 
4098  58 
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

59 
[Multiset.count_def,Multiset.delm_nonempty_def, 
4833  60 
Multiset.countm_nonempty_def]) 1); 
4681  61 
qed_spec_mp "pos_count_imp_pos_countm"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

62 

5068  63 
Goal 
4710  64 
"!!P. P(x) ==> 0<count M x > countm (delm M x) P = countm M P  1"; 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

65 
by (res_inst_tac [("M","M")] Multiset.induction 1); 
4098  66 
by (simp_tac (simpset() addsimps 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

67 
[Multiset.delm_empty_def, 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

68 
Multiset.countm_empty_def]) 1); 
4098  69 
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

70 
[eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def, 
4833  71 
Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1); 
3073
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

72 
qed "countm_done_delm"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

73 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

74 

88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

75 
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

76 
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

77 
count_empty]; 