1.1 --- a/src/HOLCF/IOA/NTP/Multiset.thy	Sat Nov 27 14:34:54 2010 -0800
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,95 +0,0 @@
     1.4 -(*  Title:      HOL/IOA/NTP/Multiset.thy
     1.5 -    Author:     Tobias Nipkow & Konrad Slind
     1.6 -*)
     1.7 -
     1.8 -header {* Axiomatic multisets *}
     1.9 -
    1.10 -theory Multiset
    1.11 -imports Lemmas
    1.12 -begin
    1.13 -
    1.14 -typedecl
    1.15 -  'a multiset
    1.16 -
    1.17 -consts
    1.18 -
    1.19 -  "{|}"  :: "'a multiset"                        ("{|}")
    1.20 -  addm   :: "['a multiset, 'a] => 'a multiset"
    1.21 -  delm   :: "['a multiset, 'a] => 'a multiset"
    1.22 -  countm :: "['a multiset, 'a => bool] => nat"
    1.23 -  count  :: "['a multiset, 'a] => nat"
    1.24 -
    1.25 -axioms
    1.26 -
    1.27 -delm_empty_def:
    1.28 -  "delm {|} x = {|}"
    1.29 -
    1.30 -delm_nonempty_def:
    1.31 -  "delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
    1.32 -
    1.33 -countm_empty_def:
    1.34 -   "countm {|} P == 0"
    1.35 -
    1.36 -countm_nonempty_def:
    1.37 -   "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
    1.38 -
    1.39 -count_def:
    1.40 -   "count M x == countm M (%y. y = x)"
    1.41 -
    1.42 -"induction":
    1.43 -   "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
    1.44 -
    1.45 -lemma count_empty: 
    1.46 -   "count {|} x = 0"
    1.47 -  by (simp add: Multiset.count_def Multiset.countm_empty_def)
    1.48 -
    1.49 -lemma count_addm_simp: 
    1.50 -     "count (addm M x) y = (if y=x then Suc(count M y) else count M y)"
    1.51 -  by (simp add: Multiset.count_def Multiset.countm_nonempty_def)
    1.52 -
    1.53 -lemma count_leq_addm: "count M y <= count (addm M x) y"
    1.54 -  by (simp add: count_addm_simp)
    1.55 -
    1.56 -lemma count_delm_simp: 
    1.57 -     "count (delm M x) y = (if y=x then count M y - 1 else count M y)"
    1.58 -apply (unfold Multiset.count_def)
    1.59 -apply (rule_tac M = "M" in Multiset.induction)
    1.60 -apply (simp (no_asm_simp) add: Multiset.delm_empty_def Multiset.countm_empty_def)
    1.61 -apply (simp add: Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
    1.62 -apply safe
    1.63 -apply simp
    1.64 -done
    1.65 -
    1.66 -lemma countm_props: "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)"
    1.67 -apply (rule_tac M = "M" in Multiset.induction)
    1.68 - apply (simp (no_asm) add: Multiset.countm_empty_def)
    1.69 -apply (simp (no_asm) add: Multiset.countm_nonempty_def)
    1.70 -apply auto
    1.71 -done
    1.72 -
    1.73 -lemma countm_spurious_delm: "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P"
    1.74 -  apply (rule_tac M = "M" in Multiset.induction)
    1.75 -  apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def)
    1.76 -  apply (simp (no_asm_simp) add: Multiset.countm_nonempty_def Multiset.delm_nonempty_def)
    1.77 -  done
    1.78 -
    1.79 -
    1.80 -lemma pos_count_imp_pos_countm [rule_format (no_asm)]: "!!P. P(x) ==> 0<count M x --> countm M P > 0"
    1.81 -  apply (rule_tac M = "M" in Multiset.induction)
    1.82 -  apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.count_def Multiset.countm_empty_def)
    1.83 -  apply (simp add: Multiset.count_def Multiset.delm_nonempty_def Multiset.countm_nonempty_def)
    1.84 -  done
    1.85 -
    1.86 -lemma countm_done_delm: 
    1.87 -   "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1"
    1.88 -  apply (rule_tac M = "M" in Multiset.induction)
    1.89 -  apply (simp (no_asm) add: Multiset.delm_empty_def Multiset.countm_empty_def)
    1.90 -  apply (simp (no_asm_simp) add: count_addm_simp Multiset.delm_nonempty_def Multiset.countm_nonempty_def pos_count_imp_pos_countm)
    1.91 -  apply auto
    1.92 -  done
    1.93 -
    1.94 -
    1.95 -declare count_addm_simp [simp] count_delm_simp [simp]
    1.96 -  Multiset.countm_empty_def [simp] Multiset.delm_empty_def [simp] count_empty [simp]
    1.97 -
    1.98 -end