src/HOL/Induct/Multiset.ML
author paulson
Fri Dec 11 10:41:53 1998 +0100 (1998-12-11)
changeset 6024 cb87f103d114
parent 5983 79e301a6a51b
child 6162 484adda70b65
permissions -rw-r--r--
new Close_locale synatx
nipkow@5628
     1
(*  Title:      HOL/Induct/Multiset.ML
nipkow@5628
     2
    ID:         $Id$
nipkow@5628
     3
    Author:     Tobias Nipkow
nipkow@5628
     4
    Copyright   1998 TUM
nipkow@5628
     5
*)
nipkow@5628
     6
nipkow@5628
     7
Addsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
nipkow@5628
     8
nipkow@5628
     9
(** Preservation of representing set `multiset' **)
nipkow@5628
    10
nipkow@5628
    11
Goalw [multiset_def] "(%a. 0) : multiset";
nipkow@5628
    12
by(Simp_tac 1);
nipkow@5628
    13
qed "const0_in_multiset";
nipkow@5628
    14
Addsimps [const0_in_multiset];
nipkow@5628
    15
nipkow@5628
    16
Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
nipkow@5628
    17
by(Simp_tac 1);
nipkow@5628
    18
qed "only1_in_multiset";
nipkow@5628
    19
Addsimps [only1_in_multiset];
nipkow@5628
    20
nipkow@5628
    21
Goalw [multiset_def]
nipkow@5628
    22
 "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
nipkow@5628
    23
by(Asm_full_simp_tac 1);
nipkow@5628
    24
bd finite_UnI 1;
nipkow@5628
    25
ba 1;
nipkow@5628
    26
by(asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
nipkow@5628
    27
qed "union_preserves_multiset";
nipkow@5628
    28
Addsimps [union_preserves_multiset];
nipkow@5628
    29
nipkow@5628
    30
Goalw [multiset_def]
nipkow@5628
    31
 "[| M : multiset |] ==> (%a. M a - N a) : multiset";
nipkow@5628
    32
by(Asm_full_simp_tac 1);
nipkow@5628
    33
be (rotate_prems 1 finite_subset) 1;
nipkow@5628
    34
by(Auto_tac);
nipkow@5628
    35
qed "diff_preserves_multiset";
nipkow@5628
    36
Addsimps [diff_preserves_multiset];
nipkow@5628
    37
nipkow@5628
    38
(** Injectivity of Rep_multiset **)
nipkow@5628
    39
nipkow@5628
    40
Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
nipkow@5628
    41
br iffI 1;
nipkow@5628
    42
 by(Asm_simp_tac 1);
nipkow@5628
    43
by(dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
nipkow@5628
    44
by(Asm_full_simp_tac 1);
nipkow@5628
    45
qed "multiset_eq_conv_Rep_eq";
nipkow@5628
    46
Addsimps [multiset_eq_conv_Rep_eq];
nipkow@5628
    47
Addsimps [expand_fun_eq];
nipkow@5628
    48
(*
nipkow@5628
    49
Goal
nipkow@5628
    50
 "[| f : multiset; g : multiset |] ==> \
nipkow@5628
    51
\ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
nipkow@5628
    52
br iffI 1;
nipkow@5628
    53
 by(dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
nipkow@5628
    54
 by(Asm_full_simp_tac 1);
nipkow@5628
    55
by(subgoal_tac "f = g" 1);
nipkow@5628
    56
 by(Asm_simp_tac 1);
nipkow@5628
    57
br ext 1;
nipkow@5628
    58
by(Blast_tac 1);
nipkow@5628
    59
qed "Abs_multiset_eq";
nipkow@5628
    60
Addsimps [Abs_multiset_eq];
nipkow@5628
    61
*)
nipkow@5628
    62
nipkow@5628
    63
(** Equations **)
nipkow@5628
    64
nipkow@5628
    65
(* union *)
nipkow@5628
    66
nipkow@5628
    67
Goalw [union_def,empty_def]
nipkow@5628
    68
 "M + {#} = M & {#} + M = M";
nipkow@5628
    69
by(Simp_tac 1);
nipkow@5628
    70
qed "union_empty";
nipkow@5628
    71
Addsimps [union_empty];
nipkow@5628
    72
nipkow@5628
    73
Goalw [union_def]
nipkow@5628
    74
 "(M::'a multiset) + N = N + M";
nipkow@5628
    75
by(simp_tac (simpset() addsimps add_ac) 1);
nipkow@5628
    76
qed "union_comm";
nipkow@5628
    77
nipkow@5628
    78
Goalw [union_def]
nipkow@5628
    79
 "((M::'a multiset)+N)+K = M+(N+K)";
nipkow@5628
    80
by(simp_tac (simpset() addsimps add_ac) 1);
nipkow@5628
    81
qed "union_assoc";
nipkow@5628
    82
nipkow@5628
    83
qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
nipkow@5628
    84
 (fn _ => [rtac (union_comm RS trans) 1, rtac (union_assoc RS trans) 1,
nipkow@5628
    85
           rtac (union_comm RS arg_cong) 1]);
nipkow@5628
    86
nipkow@5628
    87
val union_ac = [union_assoc, union_comm, union_lcomm];
nipkow@5628
    88
nipkow@5628
    89
(* diff *)
nipkow@5628
    90
nipkow@5628
    91
Goalw [empty_def,diff_def]
nipkow@5628
    92
 "M-{#} = M & {#}-M = {#}";
nipkow@5628
    93
by(Simp_tac 1);
nipkow@5628
    94
qed "diff_empty";
nipkow@5628
    95
Addsimps [diff_empty];
nipkow@5628
    96
nipkow@5628
    97
Goalw [union_def,diff_def]
nipkow@5628
    98
 "M+{#a#}-{#a#} = M";
nipkow@5628
    99
by(Simp_tac 1);
nipkow@5628
   100
qed "diff_union_inverse2";
nipkow@5628
   101
Addsimps [diff_union_inverse2];
nipkow@5628
   102
nipkow@5628
   103
(* count *)
nipkow@5628
   104
nipkow@5628
   105
Goalw [count_def,empty_def]
nipkow@5628
   106
 "count {#} a = 0";
nipkow@5628
   107
by(Simp_tac 1);
nipkow@5628
   108
qed "count_empty";
nipkow@5628
   109
Addsimps [count_empty];
nipkow@5628
   110
nipkow@5628
   111
Goalw [count_def,single_def]
nipkow@5628
   112
 "count {#b#} a = (if b=a then 1 else 0)";
nipkow@5628
   113
by(Simp_tac 1);
nipkow@5628
   114
qed "count_single";
nipkow@5628
   115
Addsimps [count_single];
nipkow@5628
   116
nipkow@5628
   117
Goalw [count_def,union_def]
nipkow@5628
   118
 "count (M+N) a = count M a + count N a";
nipkow@5628
   119
by(Simp_tac 1);
nipkow@5628
   120
qed "count_union";
nipkow@5628
   121
Addsimps [count_union];
nipkow@5628
   122
nipkow@5772
   123
Goalw [count_def,diff_def]
nipkow@5772
   124
 "count (M-N) a = count M a - count N a";
nipkow@5772
   125
by(Simp_tac 1);
nipkow@5772
   126
qed "count_diff";
nipkow@5772
   127
Addsimps [count_diff];
nipkow@5772
   128
nipkow@5628
   129
(* set_of *)
nipkow@5628
   130
nipkow@5628
   131
Goalw [set_of_def] "set_of {#} = {}";
nipkow@5628
   132
by(Simp_tac 1);
nipkow@5628
   133
qed "set_of_empty";
nipkow@5628
   134
Addsimps [set_of_empty];
nipkow@5628
   135
nipkow@5628
   136
Goalw [set_of_def]
nipkow@5628
   137
 "set_of {#b#} = {b}";
nipkow@5628
   138
by(Simp_tac 1);
nipkow@5628
   139
qed "set_of_single";
nipkow@5628
   140
Addsimps [set_of_single];
nipkow@5628
   141
nipkow@5628
   142
Goalw [set_of_def]
nipkow@5628
   143
 "set_of(M+N) = set_of M Un set_of N";
nipkow@5628
   144
by(Auto_tac);
nipkow@5628
   145
qed "set_of_union";
nipkow@5628
   146
Addsimps [set_of_union];
nipkow@5628
   147
nipkow@5628
   148
(* size *)
nipkow@5628
   149
nipkow@5628
   150
Goalw [size_def] "size {#} = 0";
nipkow@5628
   151
by(Simp_tac 1);
nipkow@5628
   152
qed "size_empty";
nipkow@5628
   153
Addsimps [size_empty];
nipkow@5628
   154
nipkow@5628
   155
Goalw [size_def]
nipkow@5628
   156
 "size {#b#} = 1";
nipkow@5628
   157
by(Simp_tac 1);
nipkow@5628
   158
qed "size_single";
nipkow@5628
   159
Addsimps [size_single];
nipkow@5628
   160
nipkow@5628
   161
(* Some other day...
nipkow@5628
   162
Goalw [size_def]
nipkow@5628
   163
 "size (M+N::'a multiset) = size M + size N";
nipkow@5628
   164
*)
nipkow@5628
   165
nipkow@5628
   166
(* equalities *)
nipkow@5628
   167
nipkow@5772
   168
Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
nipkow@5772
   169
by(Simp_tac 1);
nipkow@5772
   170
qed "multiset_eq_conv_count_eq";
nipkow@5772
   171
nipkow@5628
   172
Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
nipkow@5628
   173
by(Simp_tac 1);
nipkow@5628
   174
qed "single_not_empty";
nipkow@5628
   175
Addsimps [single_not_empty];
nipkow@5628
   176
nipkow@5628
   177
Goalw [single_def] "({#a#}={#b#}) = (a=b)";
nipkow@5628
   178
by(Auto_tac);
nipkow@5628
   179
qed "single_eq_single";
nipkow@5628
   180
Addsimps [single_eq_single];
nipkow@5628
   181
nipkow@5628
   182
Goalw [union_def,empty_def]
nipkow@5628
   183
 "(M+N = {#}) = (M = {#} & N = {#})";
nipkow@5628
   184
by(Simp_tac 1);
nipkow@5628
   185
by(Blast_tac 1);
nipkow@5628
   186
qed "union_eq_empty";
nipkow@5628
   187
AddIffs [union_eq_empty];
nipkow@5628
   188
nipkow@5628
   189
Goalw [union_def,empty_def]
nipkow@5628
   190
 "({#} = M+N) = (M = {#} & N = {#})";
nipkow@5628
   191
by(Simp_tac 1);
nipkow@5628
   192
by(Blast_tac 1);
nipkow@5628
   193
qed "empty_eq_union";
nipkow@5628
   194
AddIffs [empty_eq_union];
nipkow@5628
   195
nipkow@5628
   196
Goalw [union_def]
nipkow@5628
   197
 "(M+K = N+K) = (M=(N::'a multiset))";
nipkow@5628
   198
by(Simp_tac 1);
nipkow@5628
   199
qed "union_right_cancel";
nipkow@5628
   200
Addsimps [union_right_cancel];
nipkow@5628
   201
nipkow@5628
   202
Goalw [union_def]
nipkow@5628
   203
 "(K+M = K+N) = (M=(N::'a multiset))";
nipkow@5628
   204
by(Simp_tac 1);
nipkow@5628
   205
qed "union_left_cancel";
nipkow@5628
   206
Addsimps [union_left_cancel];
nipkow@5628
   207
nipkow@5628
   208
Goalw [empty_def,single_def,union_def]
nipkow@5628
   209
 "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
nipkow@5628
   210
by(simp_tac (simpset() addsimps [add_is_1]) 1);
nipkow@5628
   211
by(Blast_tac 1);
nipkow@5628
   212
qed "union_is_single";
nipkow@5628
   213
nipkow@5628
   214
Goalw [empty_def,single_def,union_def]
nipkow@5628
   215
 "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
nipkow@5628
   216
by(simp_tac (simpset() addsimps [one_is_add]) 1);
nipkow@5628
   217
by(blast_tac (claset() addDs [sym]) 1);
nipkow@5628
   218
qed "single_is_union";
nipkow@5628
   219
nipkow@5628
   220
Goalw [single_def,union_def,diff_def]
nipkow@5628
   221
 "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
nipkow@5628
   222
by(Simp_tac 1);
nipkow@5628
   223
br conjI 1;
nipkow@5628
   224
 by(Force_tac 1);
nipkow@5628
   225
by(Clarify_tac 1);
nipkow@5628
   226
br conjI 1;
nipkow@5628
   227
 by(Blast_tac 1);
nipkow@5628
   228
by(Clarify_tac 1);
nipkow@5628
   229
br iffI 1;
nipkow@5628
   230
 br conjI 1;
nipkow@5628
   231
 by(Clarify_tac 1);
nipkow@5628
   232
  br conjI 1;
nipkow@5628
   233
   by(asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
nipkow@5628
   234
(* PROOF FAILED:
nipkow@5628
   235
by(Blast_tac 1);
nipkow@5628
   236
*)
nipkow@5628
   237
  by(Fast_tac 1);
nipkow@5628
   238
 by(Asm_simp_tac 1);
nipkow@5628
   239
by(Force_tac 1);
nipkow@5628
   240
qed "add_eq_conv_diff";
nipkow@5628
   241
nipkow@5628
   242
(* FIXME
nipkow@5628
   243
val prems = Goal
nipkow@5628
   244
 "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
nipkow@5628
   245
by(res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
nipkow@5628
   246
     measure_induct 1);
nipkow@5628
   247
by(Clarify_tac 1);
nipkow@5628
   248
brs prems 1;
nipkow@5628
   249
 ba 1;
nipkow@5628
   250
by(Clarify_tac 1);
nipkow@5628
   251
by(subgoal_tac "finite G" 1);
nipkow@5628
   252
 by(fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
nipkow@5628
   253
be allE 1;
nipkow@5628
   254
be impE 1;
nipkow@5628
   255
 by(Blast_tac 2);
nipkow@5628
   256
by(asm_simp_tac (simpset() addsimps [psubset_card]) 1);
nipkow@5628
   257
val lemma = result();
nipkow@5628
   258
nipkow@5628
   259
val prems = Goal
nipkow@5628
   260
 "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
nipkow@5628
   261
br (lemma RS mp) 1;
nipkow@5628
   262
by (REPEAT(ares_tac prems 1));
nipkow@5628
   263
qed "finite_psubset_induct";
nipkow@5628
   264
nipkow@5628
   265
Better: use wf_finite_psubset in WF_Rel
nipkow@5628
   266
*)
nipkow@5628
   267
nipkow@5628
   268
(** Towards the induction rule **)
nipkow@5628
   269
nipkow@5628
   270
Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
nipkow@5628
   271
be finite_induct 1;
nipkow@5628
   272
by(Auto_tac);
nipkow@5628
   273
qed "setsum_0";
nipkow@5628
   274
Addsimps [setsum_0];
nipkow@5628
   275
nipkow@5628
   276
Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
nipkow@5628
   277
be finite_induct 1;
nipkow@5628
   278
by(Auto_tac);
nipkow@5628
   279
val lemma = result();
nipkow@5628
   280
nipkow@5628
   281
Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
nipkow@5628
   282
bd lemma 1;
nipkow@5628
   283
by(Fast_tac 1);
nipkow@5628
   284
qed "setsum_SucD";
nipkow@5628
   285
nipkow@5628
   286
Goal "[| finite F; 0 < f a |] ==> \
nipkow@5628
   287
\     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
nipkow@5628
   288
be finite_induct 1;
nipkow@5628
   289
by(Auto_tac);
nipkow@5628
   290
 by(asm_simp_tac (simpset() addsimps add_ac) 1);
nipkow@5628
   291
by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
nipkow@5628
   292
by(Auto_tac);
nipkow@5628
   293
qed "setsum_decr";
nipkow@5628
   294
nipkow@5628
   295
val prems = Goalw [multiset_def]
nipkow@5628
   296
 "[| P(%a.0); \
nipkow@5628
   297
\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
nipkow@5628
   298
\  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
nipkow@5628
   299
by(induct_tac "n" 1);
nipkow@5628
   300
 by(Asm_simp_tac 1);
nipkow@5628
   301
 by(Clarify_tac 1);
nipkow@5628
   302
 by(subgoal_tac "f = (%a.0)" 1);
nipkow@5628
   303
  by(Asm_simp_tac 1);
nipkow@5628
   304
  brs prems 1;
nipkow@5628
   305
 br ext 1;
nipkow@5628
   306
 by(Force_tac 1);
nipkow@5628
   307
by(Clarify_tac 1);
nipkow@5628
   308
by(forward_tac [setsum_SucD] 1);
nipkow@5628
   309
 ba 1;
nipkow@5628
   310
by(Clarify_tac 1);
nipkow@5628
   311
by(rename_tac "a" 1);
nipkow@5628
   312
by(subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
nipkow@5628
   313
 be (rotate_prems 1 finite_subset) 2;
nipkow@5628
   314
 by(Simp_tac 2);
nipkow@5628
   315
 by(Blast_tac 2);
nipkow@5628
   316
by(subgoal_tac
nipkow@5628
   317
   "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
nipkow@5628
   318
 br ext 2;
nipkow@5628
   319
 by(Asm_simp_tac 2);
nipkow@5628
   320
by(EVERY1[etac ssubst, resolve_tac prems]);
nipkow@5628
   321
 by(Blast_tac 1);
nipkow@5628
   322
by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
nipkow@5628
   323
 by(Blast_tac 1);
nipkow@5628
   324
by(asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
nipkow@5628
   325
by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
nipkow@5628
   326
 by(Blast_tac 2);
nipkow@5628
   327
by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
nipkow@5628
   328
 by(Blast_tac 2);
nipkow@5628
   329
by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
nipkow@5983
   330
                           addcongs [conj_cong]) 1);
nipkow@5628
   331
val lemma = result();
nipkow@5628
   332
nipkow@5628
   333
val major::prems = Goal
nipkow@5628
   334
 "[| f : multiset; \
nipkow@5628
   335
\    P(%a.0); \
nipkow@5628
   336
\    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
nipkow@5628
   337
by(rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
nipkow@5628
   338
by(REPEAT(ares_tac (refl::prems) 1));
nipkow@5628
   339
qed "Rep_multiset_induct";
nipkow@5628
   340
nipkow@5628
   341
val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
nipkow@5628
   342
 "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
nipkow@5628
   343
by (rtac (Rep_multiset_inverse RS subst) 1);
nipkow@5628
   344
by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
nipkow@5628
   345
 by(rtac prem1 1);
nipkow@5628
   346
by(Clarify_tac 1);
nipkow@5628
   347
by(subgoal_tac
nipkow@5628
   348
    "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
nipkow@5628
   349
 by(Simp_tac 2);
nipkow@5628
   350
be ssubst 1;
nipkow@5628
   351
by(etac (Abs_multiset_inverse RS subst) 1);
nipkow@5628
   352
by(etac(simplify (simpset()) prem2)1);
nipkow@5628
   353
qed "multiset_induct";
nipkow@5628
   354
nipkow@5628
   355
Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
nipkow@5628
   356
Delsimps [Abs_multiset_inverse,Rep_multiset_inverse,Rep_multiset];
nipkow@5628
   357
nipkow@5628
   358
Goal
nipkow@5628
   359
 "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
nipkow@5628
   360
by(simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
nipkow@5628
   361
by(Auto_tac);
nipkow@5628
   362
qed "add_eq_conv_ex";
nipkow@5628
   363
nipkow@5628
   364
(** order **)
nipkow@5628
   365
nipkow@5628
   366
Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
nipkow@5628
   367
by(Simp_tac 1);
nipkow@5628
   368
qed "not_less_empty";
nipkow@5628
   369
AddIffs [not_less_empty];
nipkow@5628
   370
nipkow@5628
   371
Goalw [mult1_def]
nipkow@5628
   372
 "(N,M0 + {#a#}) : mult1(r) = \
nipkow@5628
   373
\ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
nipkow@5628
   374
\  (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
nipkow@5628
   375
br iffI 1;
nipkow@5628
   376
 by(asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
nipkow@5628
   377
 by(Clarify_tac 1);
nipkow@5628
   378
 be disjE 1;
nipkow@5628
   379
  by(Blast_tac 1);
nipkow@5628
   380
 by(Clarify_tac 1);
nipkow@5628
   381
 by(res_inst_tac [("x","Ka+K")] exI 1);
nipkow@5628
   382
 by(simp_tac (simpset() addsimps union_ac) 1);
nipkow@5628
   383
 by(Blast_tac 1);
nipkow@5628
   384
be disjE 1;
nipkow@5628
   385
 by(Clarify_tac 1);
nipkow@5628
   386
 by(res_inst_tac [("x","aa")] exI 1);
nipkow@5628
   387
 by(res_inst_tac [("x","M0+{#a#}")] exI 1);
nipkow@5628
   388
 by(res_inst_tac [("x","K")] exI 1);
nipkow@5628
   389
 by(simp_tac (simpset() addsimps union_ac) 1);
nipkow@5628
   390
by(Blast_tac 1);
nipkow@5628
   391
qed "less_add_conv";
nipkow@5628
   392
nipkow@5628
   393
Open_locale "MSOrd";
nipkow@5628
   394
nipkow@5628
   395
val W_def = thm "W_def";
nipkow@5628
   396
nipkow@5628
   397
Goalw [W_def]
nipkow@5628
   398
 "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
nipkow@5628
   399
\    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
nipkow@5628
   400
\ ==> M0+{#a#} : W";
nipkow@5628
   401
br accI 1;
nipkow@5628
   402
by(rename_tac "N" 1);
nipkow@5628
   403
by(full_simp_tac (simpset() addsimps [less_add_conv]) 1);
nipkow@5628
   404
be disjE 1;
nipkow@5628
   405
 by(Blast_tac 1);
nipkow@5628
   406
by(Clarify_tac 1);
nipkow@5628
   407
by(rotate_tac ~1 1);
nipkow@5628
   408
be rev_mp 1;
nipkow@5628
   409
by(res_inst_tac [("M","K")] multiset_induct 1);
nipkow@5628
   410
 by(Asm_simp_tac 1);
nipkow@5628
   411
by(simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
nipkow@5628
   412
by(Blast_tac 1);
nipkow@5628
   413
qed "lemma1";
nipkow@5628
   414
nipkow@5628
   415
Goalw [W_def]
nipkow@5628
   416
 "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
nipkow@5628
   417
be acc_induct 1;
nipkow@5628
   418
by(blast_tac (claset() addIs [export lemma1]) 1);
nipkow@5628
   419
qed "lemma2";
nipkow@5628
   420
nipkow@5628
   421
Goalw [W_def]
nipkow@5628
   422
 "wf(r) ==> !M:W. M+{#a#} : W";
nipkow@5628
   423
by(eres_inst_tac [("a","a")] wf_induct 1);
nipkow@5628
   424
by(blast_tac (claset() addIs [export lemma2]) 1);
nipkow@5628
   425
qed "lemma3";
nipkow@5628
   426
nipkow@5628
   427
Goalw [W_def] "wf(r) ==> M : W";
nipkow@5628
   428
by(res_inst_tac [("M","M")] multiset_induct 1);
nipkow@5628
   429
 br accI 1;
nipkow@5628
   430
 by(Asm_full_simp_tac 1);
nipkow@5628
   431
by(blast_tac (claset() addDs [export lemma3]) 1);
nipkow@5628
   432
qed "all_accessible";
nipkow@5628
   433
paulson@6024
   434
Close_locale "MSOrd";
nipkow@5628
   435
nipkow@5628
   436
Goal "wf(r) ==> wf(mult1 r)";
nipkow@5628
   437
by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
nipkow@5628
   438
qed "wf_mult1";
nipkow@5628
   439
nipkow@5628
   440
Goalw [mult_def] "wf(r) ==> wf(mult r)";
nipkow@5628
   441
by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
nipkow@5628
   442
qed "wf_mult";
nipkow@5628
   443
nipkow@5772
   444
(** Equivalence of mult with the usual (closure-free) def **)
nipkow@5772
   445
nipkow@5772
   446
(* Badly needed: a linear arithmetic tactic for multisets *)
nipkow@5772
   447
nipkow@5772
   448
Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})";
nipkow@5772
   449
by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
nipkow@5772
   450
qed "diff_union_single_conv";
nipkow@5628
   451
nipkow@5772
   452
(* One direction *)
nipkow@5772
   453
Goalw [mult_def,mult1_def,set_of_def]
nipkow@5772
   454
 "trans r ==> \
nipkow@5772
   455
\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
nipkow@5772
   456
\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
nipkow@5772
   457
be converse_trancl_induct 1;
nipkow@5772
   458
 by(Clarify_tac 1);
nipkow@5772
   459
 by(res_inst_tac [("x","M0")] exI 1);
nipkow@5772
   460
 by(Simp_tac 1);
nipkow@5628
   461
by(Clarify_tac 1);
nipkow@5772
   462
by(case_tac "elem K a" 1);
nipkow@5772
   463
 by(res_inst_tac [("x","I")] exI 1);
nipkow@5772
   464
 by(Simp_tac 1);
nipkow@5772
   465
 by(res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
nipkow@5772
   466
 by(asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
nipkow@5772
   467
 by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
nipkow@5772
   468
 by(asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
nipkow@5772
   469
 by(full_simp_tac (simpset() addsimps [trans_def]) 1);
nipkow@5772
   470
 by(Blast_tac 1);
nipkow@5772
   471
by(subgoal_tac "elem I a" 1);
nipkow@5772
   472
 by(res_inst_tac [("x","I-{#a#}")] exI 1);
nipkow@5772
   473
 by(res_inst_tac [("x","J+{#a#}")] exI 1);
nipkow@5772
   474
 by(res_inst_tac [("x","K + Ka")] exI 1);
nipkow@5772
   475
 br conjI 1;
nipkow@5772
   476
  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
nipkow@5772
   477
                             addsplits [nat_diff_split]) 1);
nipkow@5772
   478
 br conjI 1;
nipkow@5772
   479
  by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
nipkow@5772
   480
  by(Asm_full_simp_tac 1);
nipkow@5772
   481
  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
nipkow@5772
   482
                             addsplits [nat_diff_split]) 1);
nipkow@5772
   483
 by(full_simp_tac (simpset() addsimps [trans_def]) 1);
nipkow@5772
   484
 by(Blast_tac 1);
nipkow@5772
   485
by(subgoal_tac "elem (M0 +{#a#}) a" 1);
nipkow@5772
   486
 by(Asm_full_simp_tac 1);
nipkow@5628
   487
by(Simp_tac 1);
nipkow@5772
   488
qed "mult_implies_one_step";