src/HOL/IOA/NTP/Multiset.ML
author paulson
Mon, 07 Oct 1996 10:28:44 +0200
changeset 2056 93c093620c28
parent 1894 c2c8279d40f0
permissions -rw-r--r--
Removed commands made redundant by new one-point rules
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/IOA/NTP/Multiset.ML
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     2
    ID:         $Id$
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow & Konrad Slind
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     4
    Copyright   1994  TU Muenchen
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     5
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     6
Axiomatic multisets.
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     7
Should be done as a subtype and moved to a global place.
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     8
*)
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
     9
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    10
goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    11
   "count {|} x = 0";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    12
 by (rtac refl 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    13
qed "count_empty";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    14
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    15
goal Multiset.thy 
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    16
     "count (addm M x) y = (if y=x then Suc(count M y) else count M y)";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    17
  by (asm_simp_tac (!simpset addsimps 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    18
                    [Multiset.count_def,Multiset.countm_nonempty_def]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    19
                    setloop (split_tac [expand_if])) 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    20
qed "count_addm_simp";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    21
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    22
goal Multiset.thy "count M y <= count (addm M x) y";
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    23
  by (simp_tac (!simpset addsimps [count_addm_simp]
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    24
                         setloop (split_tac [expand_if])) 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    25
qed "count_leq_addm";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    26
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    27
goalw Multiset.thy [Multiset.count_def] 
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    28
     "count (delm M x) y = (if y=x then pred(count M y) else count M y)";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    29
  by (res_inst_tac [("M","M")] Multiset.induction 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    30
  by (asm_simp_tac (!simpset 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    31
                   addsimps [Multiset.delm_empty_def,Multiset.countm_empty_def]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    32
                   setloop (split_tac [expand_if])) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    33
  by (asm_full_simp_tac (!simpset 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    34
                         addsimps [Multiset.delm_nonempty_def,
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    35
                                   Multiset.countm_nonempty_def]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    36
                         setloop (split_tac [expand_if])) 1);
1894
c2c8279d40f0 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    37
  by (safe_tac (!claset));
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    38
  by (Asm_full_simp_tac 1);
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    39
qed "count_delm_simp";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    40
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    41
goal Multiset.thy "!!M. (!x. P(x) --> Q(x)) ==> (countm M P <= countm M Q)";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    42
  by (res_inst_tac [("M","M")] Multiset.induction 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    43
  by (simp_tac (!simpset addsimps [Multiset.countm_empty_def]) 1);
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    44
  by (simp_tac (!simpset addsimps[Multiset.countm_nonempty_def]) 1);
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    45
  by (etac (less_eq_add_cong RS mp RS mp) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    46
  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    47
                                  setloop (split_tac [expand_if])) 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    48
qed "countm_props";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    49
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    50
goal Multiset.thy "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    51
  by (res_inst_tac [("M","M")] Multiset.induction 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    52
  by (simp_tac (!simpset addsimps [Multiset.delm_empty_def,
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    53
                                   Multiset.countm_empty_def]) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    54
  by (asm_simp_tac (!simpset addsimps[Multiset.countm_nonempty_def,
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    55
                                      Multiset.delm_nonempty_def]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    56
                             setloop (split_tac [expand_if])) 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    57
qed "countm_spurious_delm";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    58
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    59
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    60
goal Multiset.thy "!!P. P(x) ==> 0<count M x --> 0<countm M P";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    61
  by (res_inst_tac [("M","M")] Multiset.induction 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    62
  by (simp_tac (!simpset addsimps 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    63
                          [Multiset.delm_empty_def,Multiset.count_def,
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    64
                           Multiset.countm_empty_def]) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    65
  by (asm_simp_tac (!simpset addsimps 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    66
                       [Multiset.count_def,Multiset.delm_nonempty_def,
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    67
                        Multiset.countm_nonempty_def]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    68
                    setloop (split_tac [expand_if])) 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    69
val pos_count_imp_pos_countm = store_thm("pos_count_imp_pos_countm", standard(result() RS mp));
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    70
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    71
goal Multiset.thy
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    72
   "!!P. P(x) ==> 0<count M x --> countm (delm M x) P = pred (countm M P)";
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    73
  by (res_inst_tac [("M","M")] Multiset.induction 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    74
  by (simp_tac (!simpset addsimps 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    75
                          [Multiset.delm_empty_def,
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    76
                           Multiset.countm_empty_def]) 1);
1266
3ae9fe3c0f68 added local simpsets
clasohm
parents: 1051
diff changeset
    77
  by (asm_simp_tac (!simpset addsimps 
1051
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    78
                      [eq_sym_conv,count_addm_simp,Multiset.delm_nonempty_def,
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    79
                       Multiset.countm_nonempty_def,pos_count_imp_pos_countm,
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    80
                       suc_pred_id]
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    81
                    setloop (split_tac [expand_if])) 1);
4fcd0638e61d Directory example is now called NTP
nipkow
parents:
diff changeset
    82
qed "countm_done_delm";
1328
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    83
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    84
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    85
Addsimps [count_addm_simp, count_delm_simp,
9a449a91425d *** empty log message ***
mueller
parents: 1266
diff changeset
    86
          Multiset.countm_empty_def, Multiset.delm_empty_def,
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1328
diff changeset
    87
          count_empty];