1(* Title: HOL/HOLCF/IOA/NTP/Multiset.thy 2 Author: Tobias Nipkow & Konrad Slind 3*) 4 5section \<open>Axiomatic multisets\<close> 6 7theory Multiset 8imports Lemmas 9begin 10 11typedecl 12 'a multiset 13 14consts 15 16 emptym :: "'a multiset" ("{|}") 17 addm :: "['a multiset, 'a] => 'a multiset" 18 delm :: "['a multiset, 'a] => 'a multiset" 19 countm :: "['a multiset, 'a => bool] => nat" 20 count :: "['a multiset, 'a] => nat" 21 22axiomatization where 23 24delm_empty_def: 25 "delm {|} x = {|}" and 26 27delm_nonempty_def: 28 "delm (addm M x) y == (if x=y then M else addm (delm M y) x)" and 29 30countm_empty_def: 31 "countm {|} P == 0" and 32 33countm_nonempty_def: 34 "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" and 35 36count_def: 37 "count M x == countm M (%y. y = x)" and 38 39"induction": 40 "\<And>P M. [| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)" 41 42lemma count_empty: 43 "count {|} x = 0" 44 by (simp add: Multiset.count_def Multiset.countm_empty_def) 45 46lemma count_addm_simp: 47 "count (addm M x) y = (if y=x then Suc(count M y) else count M y)" 48 by (simp add: Multiset.count_def Multiset.countm_nonempty_def) 49 50lemma count_leq_addm: "count M y <= count (addm M x) y" 51 by (simp add: count_addm_simp) 52 53lemma count_delm_simp: 54 "count (delm M x) y = (if y=x then count M y - 1 else count M y)" 55apply (unfold Multiset.count_def) 56apply (rule_tac M = "M" in Multiset.induction) 57apply (simp (no_asm_simp) add: Multiset.delm_empty_def Multiset.countm_empty_def) 58apply (simp add: Multiset.delm_nonempty_def Multiset.countm_nonempty_def) 59apply safe 60apply simp 61done 62 63lemma countm_props: "\<And>M. (\<forall>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (countm M P \<le> countm M Q)" 64apply (rule_tac M = "M" in Multiset.induction) 65 apply (simp (no_asm) add: Multiset.countm_empty_def) 66apply (simp (no_asm) add: Multiset.countm_nonempty_def) 67apply auto 68done 69 70lemma countm_spurious_delm: "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P" 71 apply (rule_tac M = "M" in Multiset.induction) 72 apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) 73 apply (simp (no_asm_simp) add: Multiset.countm_nonempty_def Multiset.delm_nonempty_def) 74 done 75 76 77lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P > 0" 78 apply (rule_tac M = "M" in Multiset.induction) 79 apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def) 80 apply (simp add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def) 81 done 82 83lemma countm_done_delm: 84 "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1" 85 apply (rule_tac M = "M" in Multiset.induction) 86 apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def) 87 apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm) 88 apply auto 89 done 90 91 92declare count_addm_simp [simp] count_delm_simp [simp] 93 Multiset.countm_empty_def [simp] Multiset.delm_empty_def [simp] count_empty [simp] 94 95end 96