src/HOL/HOLCF/IOA/NTP/Multiset.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 47026 36dacca8a95c
child 62002 f1599e98c4d0
permissions -rw-r--r--
modernized header;
     1 (*  Title:      HOL/HOLCF/IOA/NTP/Multiset.thy
     2     Author:     Tobias Nipkow & Konrad Slind
     3 *)
     4 
     5 section {* Axiomatic multisets *}
     6 
     7 theory Multiset
     8 imports Lemmas
     9 begin
    10 
    11 typedecl
    12   'a multiset
    13 
    14 consts
    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 
    22 axiomatization where
    23 
    24 delm_empty_def:
    25   "delm {|} x = {|}" and
    26 
    27 delm_nonempty_def:
    28   "delm (addm M x) y == (if x=y then M else addm (delm M y) x)" and
    29 
    30 countm_empty_def:
    31    "countm {|} P == 0" and
    32 
    33 countm_nonempty_def:
    34    "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" and
    35 
    36 count_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 
    42 lemma count_empty: 
    43    "count {|} x = 0"
    44   by (simp add: Multiset.count_def Multiset.countm_empty_def)
    45 
    46 lemma 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 
    50 lemma count_leq_addm: "count M y <= count (addm M x) y"
    51   by (simp add: count_addm_simp)
    52 
    53 lemma count_delm_simp: 
    54      "count (delm M x) y = (if y=x then count M y - 1 else count M y)"
    55 apply (unfold Multiset.count_def)
    56 apply (rule_tac M = "M" in Multiset.induction)
    57 apply (simp (no_asm_simp) add: Multiset.delm_empty_def Multiset.countm_empty_def)
    58 apply (simp add: Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
    59 apply safe
    60 apply simp
    61 done
    62 
    63 lemma countm_props: "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"
    64 apply (rule_tac M = "M" in Multiset.induction)
    65  apply (simp (no_asm) add: Multiset.countm_empty_def)
    66 apply (simp (no_asm) add: Multiset.countm_nonempty_def)
    67 apply auto
    68 done
    69 
    70 lemma 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 
    77 lemma 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 
    83 lemma 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 
    92 declare count_addm_simp [simp] count_delm_simp [simp]
    93   Multiset.countm_empty_def [simp] Multiset.delm_empty_def [simp] count_empty [simp]
    94 
    95 end