src/HOLCF/IOA/NTP/Multiset.ML
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12218 6597093b77e7
child 17244 0b2ff9541727
permissions -rw-r--r--
Merged in license change from Isabelle2004
mueller@3073
     1
(*  Title:      HOL/IOA/NTP/Multiset.ML
mueller@3073
     2
    ID:         $Id$
mueller@3073
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3073
     4
mueller@3073
     5
Axiomatic multisets.
mueller@3073
     6
Should be done as a subtype and moved to a global place.
mueller@3073
     7
*)
mueller@3073
     8
wenzelm@5068
     9
Goalw [Multiset.count_def, Multiset.countm_empty_def]
mueller@3073
    10
   "count {|} x = 0";
mueller@3073
    11
 by (rtac refl 1);
mueller@3073
    12
qed "count_empty";
mueller@3073
    13
wenzelm@5068
    14
Goal 
mueller@3073
    15
     "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
wenzelm@4098
    16
  by (asm_simp_tac (simpset() addsimps 
nipkow@4833
    17
                    [Multiset.count_def,Multiset.countm_nonempty_def]) 1);
mueller@3073
    18
qed "count_addm_simp";
mueller@3073
    19
wenzelm@5068
    20
Goal "count M y <= count (addm M x) y";
nipkow@4833
    21
  by (simp_tac (simpset() addsimps [count_addm_simp]) 1);
mueller@3073
    22
qed "count_leq_addm";
mueller@3073
    23
wenzelm@5068
    24
Goalw [Multiset.count_def] 
wenzelm@4710
    25
     "count (delm M x) y = (if y=x then count M y - 1 else count M y)";
nipkow@4833
    26
by (res_inst_tac [("M","M")] Multiset.induction 1);
nipkow@4833
    27
by (asm_simp_tac (simpset() 
nipkow@4833
    28
             addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1);
nipkow@4833
    29
by (asm_full_simp_tac (simpset() 
mueller@3073
    30
                         addsimps [Multiset.delm_nonempty_def,
nipkow@4833
    31
                                   Multiset.countm_nonempty_def]) 1);
nipkow@4833
    32
by Safe_tac;
nipkow@4833
    33
by (Asm_full_simp_tac 1);
mueller@3073
    34
qed "count_delm_simp";
mueller@3073
    35
wenzelm@5068
    36
Goal "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
nipkow@4681
    37
by (res_inst_tac [("M","M")] Multiset.induction 1);
nipkow@4681
    38
 by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
nipkow@4681
    39
by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
wenzelm@5132
    40
by Auto_tac;
mueller@3073
    41
qed "countm_props";
mueller@3073
    42
wenzelm@5068
    43
Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
mueller@3073
    44
  by (res_inst_tac [("M","M")] Multiset.induction 1);
wenzelm@4098
    45
  by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
mueller@3073
    46
                                   Multiset.countm_empty_def]) 1);
wenzelm@4098
    47
  by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
nipkow@4833
    48
                                      Multiset.delm_nonempty_def]) 1);
mueller@3073
    49
qed "countm_spurious_delm";
mueller@3073
    50
mueller@3073
    51
wenzelm@5068
    52
Goal "!!P. P(x) ==> 0<count M x --> 0<countm M P";
mueller@3073
    53
  by (res_inst_tac [("M","M")] Multiset.induction 1);
wenzelm@4098
    54
  by (simp_tac (simpset() addsimps 
mueller@3073
    55
                          [Multiset.delm_empty_def,Multiset.count_def,
mueller@3073
    56
                           Multiset.countm_empty_def]) 1);
wenzelm@4098
    57
  by (asm_simp_tac (simpset() addsimps 
mueller@3073
    58
                       [Multiset.count_def,Multiset.delm_nonempty_def,
nipkow@4833
    59
                        Multiset.countm_nonempty_def]) 1);
nipkow@4681
    60
qed_spec_mp "pos_count_imp_pos_countm";
mueller@3073
    61
wenzelm@5068
    62
Goal
wenzelm@4710
    63
   "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1";
mueller@3073
    64
  by (res_inst_tac [("M","M")] Multiset.induction 1);
wenzelm@4098
    65
  by (simp_tac (simpset() addsimps 
mueller@3073
    66
                          [Multiset.delm_empty_def,
mueller@3073
    67
                           Multiset.countm_empty_def]) 1);
wenzelm@4098
    68
  by (asm_simp_tac (simpset() addsimps 
mueller@3073
    69
                      [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
nipkow@4833
    70
                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
mueller@3073
    71
qed "countm_done_delm";
mueller@3073
    72
mueller@3073
    73
mueller@3073
    74
Addsimps [count_addm_simp, count_delm_simp,
mueller@3073
    75
          Multiset.countm_empty_def, Multiset.delm_empty_def,
mueller@3073
    76
          count_empty];