src/HOLCF/IOA/NTP/Multiset.ML
author wenzelm
Mon, 03 Nov 1997 14:06:27 +0100
changeset 4098 71e05eb27fb6
parent 3073 88366253a09a
child 4377 2cba48b0f1c4
permissions -rw-r--r--
isatool fixclasimp;
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    10
goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
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
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    15
goal Multiset.thy 
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 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    18
                    [Multiset.count_def,Multiset.countm_nonempty_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    19
                    setloop (split_tac [expand_if])) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    20
qed "count_addm_simp";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    21
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    22
goal Multiset.thy "count M y <= count (addm M x) y";
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    23
  by (simp_tac (simpset() addsimps [count_addm_simp]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    24
                         setloop (split_tac [expand_if])) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    25
qed "count_leq_addm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    26
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    27
goalw Multiset.thy [Multiset.count_def] 
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    28
     "count (delm M x) y = (if y=x then pred(count M y) else count M y)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    29
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    30
  by (asm_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_empty_def,Multiset.countm_empty_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    32
                   setloop (split_tac [expand_if])) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    33
  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
    34
                         addsimps [Multiset.delm_nonempty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    35
                                   Multiset.countm_nonempty_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    36
                         setloop (split_tac [expand_if])) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    37
  by (safe_tac (claset()));
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    38
  by (Asm_full_simp_tac 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    39
qed "count_delm_simp";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    40
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    41
goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    42
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    43
  by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    44
  by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    45
  by (etac (less_eq_add_cong RS mp RS mp) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    46
  by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    47
                                  setloop (split_tac [expand_if])) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    48
qed "countm_props";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    49
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    50
goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    51
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    52
  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
    53
                                   Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    54
  by (asm_simp_tac (simpset() addsimps[Multiset.countm_nonempty_def,
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    55
                                      Multiset.delm_nonempty_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    56
                             setloop (split_tac [expand_if])) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    57
qed "countm_spurious_delm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    58
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    59
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    60
goal Multiset.thy "!!P. P(x) ==> 0<count M x --> 0<countm M P";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    61
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    62
  by (simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    63
                          [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
    64
                           Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    65
  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
    66
                       [Multiset.count_def,Multiset.delm_nonempty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    67
                        Multiset.countm_nonempty_def]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    68
                    setloop (split_tac [expand_if])) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    69
val pos_count_imp_pos_countm = store_thm("pos_count_imp_pos_countm", standard(result() RS mp));
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    70
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    71
goal Multiset.thy
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    72
   "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    73
  by (res_inst_tac [("M","M")] Multiset.induction 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    74
  by (simp_tac (simpset() addsimps 
3073
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    75
                          [Multiset.delm_empty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    76
                           Multiset.countm_empty_def]) 1);
4098
71e05eb27fb6 isatool fixclasimp;
wenzelm
parents: 3073
diff changeset
    77
  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
    78
                      [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    79
                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm,
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    80
                       suc_pred_id]
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    81
                    setloop (split_tac [expand_if])) 1);
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    82
qed "countm_done_delm";
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    83
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    84
88366253a09a Old NTP files now running under the IOA meta theory based on HOLCF;
mueller
parents:
diff changeset
    85
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
    86
          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
    87
          count_empty];