equal
deleted
inserted
replaced
83 |
83 |
84 lemma countm_done_delm: |
84 lemma countm_done_delm: |
85 "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1" |
85 "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1" |
86 apply (rule_tac M = "M" in Multiset.induction) |
86 apply (rule_tac M = "M" in Multiset.induction) |
87 apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) |
87 apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) |
88 apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) |
88 apply (simp (no_asm_simp) add: neq0_conv count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) |
89 apply auto |
89 apply auto |
90 done |
90 done |
91 |
91 |
92 |
92 |
93 declare count_addm_simp [simp] count_delm_simp [simp] |
93 declare count_addm_simp [simp] count_delm_simp [simp] |