src/HOLCF/IOA/NTP/Multiset.ML
author wenzelm
Mon, 22 Jun 1998 17:13:09 +0200
changeset 5068 fb28eaa07e01
parent 4833 2e53109d4bc8
child 5132 24f992a25adc
permissions -rw-r--r--
isatool fixgoal;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Multiset.ML
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     2
    ID:         $Id$
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     5
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     6
Axiomatic multisets.
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     7
Should be done as a subtype and moved to a global place.
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     8
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     9
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    10
Goalw [Multiset.count_def, Multiset.countm_empty_def]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    11
   "count {|} x = 0";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    12
 by (rtac refl 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    13
qed "count_empty";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    14
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    15
Goal 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    16
     "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    17
  by (asm_simp_tac (simpset() addsimps 
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    18
                    [Multiset.count_def,Multiset.countm_nonempty_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    19
qed "count_addm_simp";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    20
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    21
Goal "count M y <= count (addm M x) y";
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    22
  by (simp_tac (simpset() addsimps [count_addm_simp]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    23
qed "count_leq_addm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    24
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    25
Goalw [Multiset.count_def] 
4710
05e57f1879ee eliminated pred function;
wenzelm
parents: 4681
diff changeset
    26
     "count (delm M x) y = (if y=x then count M y - 1 else count M y)";
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    27
by (res_inst_tac [("M","M")] Multiset.induction 1);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    28
by (asm_simp_tac (simpset() 
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    29
             addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    30
by (asm_full_simp_tac (simpset() 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    31
                         addsimps [Multiset.delm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    32
                                   Multiset.countm_nonempty_def]) 1);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    33
by Safe_tac;
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    34
by (Asm_full_simp_tac 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    35
qed "count_delm_simp";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    36
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    37
Goal "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    38
by (res_inst_tac [("M","M")] Multiset.induction 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    39
 by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    40
by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    41
auto();
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    42
qed "countm_props";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    43
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    44
Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    45
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    46
  by (simp_tac (simpset() addsimps [Multiset.delm_empty_def,
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    47
                                   Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    48
  by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    49
                                      Multiset.delm_nonempty_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    50
qed "countm_spurious_delm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    51
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    52
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    53
Goal "!!P. P(x) ==> 0<count M x --> 0<countm M P";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    54
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    55
  by (simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    56
                          [Multiset.delm_empty_def,Multiset.count_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    57
                           Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    58
  by (asm_simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    59
                       [Multiset.count_def,Multiset.delm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    60
                        Multiset.countm_nonempty_def]) 1);
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    61
qed_spec_mp "pos_count_imp_pos_countm";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    62
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    63
Goal
4710
05e57f1879ee eliminated pred function;
wenzelm
parents: 4681
diff changeset
    64
   "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = countm M P - 1";
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    65
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    66
  by (simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    67
                          [Multiset.delm_empty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    68
                           Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    69
  by (asm_simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    70
                      [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    71
                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    72
qed "countm_done_delm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    73
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    74
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    75
Addsimps [count_addm_simp, count_delm_simp,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    76
          Multiset.countm_empty_def, Multiset.delm_empty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    77
          count_empty];