author  mueller 
Wed, 30 Apr 1997 11:25:31 +0200  
changeset 3073  88366253a09a 
child 4098  71e05eb27fb6 
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 

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)"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

17 
by (asm_simp_tac (!simpset addsimps 
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"; 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

23 
by (simp_tac (!simpset addsimps [count_addm_simp] 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

30 
by (asm_simp_tac (!simpset 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

33 
by (asm_full_simp_tac (!simpset 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

37 
by (safe_tac (!claset)); 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

43 
by (simp_tac (!simpset addsimps [Multiset.countm_empty_def]) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

44 
by (simp_tac (!simpset addsimps[Multiset.countm_nonempty_def]) 1); 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

46 
by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq] 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

52 
by (simp_tac (!simpset addsimps [Multiset.delm_empty_def, 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

53 
Multiset.countm_empty_def]) 1); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

54 
by (asm_simp_tac (!simpset addsimps[Multiset.countm_nonempty_def, 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

62 
by (simp_tac (!simpset addsimps 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

65 
by (asm_simp_tac (!simpset addsimps 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

74 
by (simp_tac (!simpset addsimps 
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); 
88366253a09a
Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff
changeset

77 
by (asm_simp_tac (!simpset addsimps 
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]; 