src/HOLCF/IOA/NTP/Multiset.ML
author nipkow
Sat, 08 Oct 2005 15:20:58 +0200
changeset 17790 aa6ec0efe4d3
parent 17244 0b2ff9541727
permissions -rw-r--r--
fix due to new neq_simproc
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     5
Axiomatic multisets.
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     6
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
     7
*)
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
     8
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
     9
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
    10
   "count {|} x = 0";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    11
 by (rtac refl 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    12
qed "count_empty";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    13
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    14
Goal 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    15
     "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
    16
  by (asm_simp_tac (simpset() addsimps 
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    17
                    [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
    18
qed "count_addm_simp";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    19
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    20
Goal "count M y <= count (addm M x) y";
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    21
  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
    22
qed "count_leq_addm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    23
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    24
Goalw [Multiset.count_def] 
4710
05e57f1879ee eliminated pred function;
wenzelm
parents: 4681
diff changeset
    25
     "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
    26
by (res_inst_tac [("M","M")] Multiset.induction 1);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    27
by (asm_simp_tac (simpset() 
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    28
             addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]) 1);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    29
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
    30
                         addsimps [Multiset.delm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    31
                                   Multiset.countm_nonempty_def]) 1);
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    32
by Safe_tac;
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    33
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
    34
qed "count_delm_simp";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    35
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    36
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
    37
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
    38
 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
    39
by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5068
diff changeset
    40
by Auto_tac;
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    41
qed "countm_props";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    42
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    43
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
    44
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    45
  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
    46
                                   Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    47
  by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    48
                                      Multiset.delm_nonempty_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    49
qed "countm_spurious_delm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    50
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    51
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    52
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
    53
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    54
  by (simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    55
                          [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
    56
                           Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    57
  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
    58
                       [Multiset.count_def,Multiset.delm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    59
                        Multiset.countm_nonempty_def]) 1);
4681
a331c1f5a23e expand_if is now by default part of the simpset.
nipkow
parents: 4423
diff changeset
    60
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
    61
5068
fb28eaa07e01 isatool fixgoal;
wenzelm
parents: 4833
diff changeset
    62
Goal
4710
05e57f1879ee eliminated pred function;
wenzelm
parents: 4681
diff changeset
    63
   "!!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
    64
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    65
  by (simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    66
                          [Multiset.delm_empty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    67
                           Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    68
  by (asm_simp_tac (simpset() addsimps 
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    69
                      [count_addm_simp,Multiset.delm_nonempty_def,
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4710
diff changeset
    70
                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
17790
aa6ec0efe4d3 fix due to new neq_simproc
nipkow
parents: 17244
diff changeset
    71
  by (Auto_tac);
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];