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