Some more proofs.
authornipkow
Wed Oct 28 13:25:09 1998 +0100 (1998-10-28)
changeset 5772d52d61a66c32
parent 5771 7c2c8cf20221
child 5773 af3eb75b11e5
Some more proofs.
src/HOL/Induct/Multiset.ML
     1.1 --- a/src/HOL/Induct/Multiset.ML	Wed Oct 28 11:25:38 1998 +0100
     1.2 +++ b/src/HOL/Induct/Multiset.ML	Wed Oct 28 13:25:09 1998 +0100
     1.3 @@ -120,6 +120,12 @@
     1.4  qed "count_union";
     1.5  Addsimps [count_union];
     1.6  
     1.7 +Goalw [count_def,diff_def]
     1.8 + "count (M-N) a = count M a - count N a";
     1.9 +by(Simp_tac 1);
    1.10 +qed "count_diff";
    1.11 +Addsimps [count_diff];
    1.12 +
    1.13  (* set_of *)
    1.14  
    1.15  Goalw [set_of_def] "set_of {#} = {}";
    1.16 @@ -159,6 +165,10 @@
    1.17  
    1.18  (* equalities *)
    1.19  
    1.20 +Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
    1.21 +by(Simp_tac 1);
    1.22 +qed "multiset_eq_conv_count_eq";
    1.23 +
    1.24  Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
    1.25  by(Simp_tac 1);
    1.26  qed "single_not_empty";
    1.27 @@ -432,15 +442,48 @@
    1.28  by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
    1.29  qed "wf_mult";
    1.30  
    1.31 -Goalw [mult_def,set_of_def]
    1.32 - "(M,N) : mult r = (? I J K. N = I+J & M = I+K & \
    1.33 -\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
    1.34 -br iffI 1;
    1.35 +(** Equivalence of mult with the usual (closure-free) def **)
    1.36 +
    1.37 +(* Badly needed: a linear arithmetic tactic for multisets *)
    1.38 +
    1.39 +Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})";
    1.40 +by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
    1.41 +qed "diff_union_single_conv";
    1.42  
    1.43 -be trancl_induct 1;
    1.44 -by(asm_full_simp_tac (simpset() addsimps [mult1_def]) 1);
    1.45 -
    1.46 +(* One direction *)
    1.47 +Goalw [mult_def,mult1_def,set_of_def]
    1.48 + "trans r ==> \
    1.49 +\ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
    1.50 +\                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
    1.51 +be converse_trancl_induct 1;
    1.52 + by(Clarify_tac 1);
    1.53 + by(res_inst_tac [("x","M0")] exI 1);
    1.54 + by(Simp_tac 1);
    1.55  by(Clarify_tac 1);
    1.56 -by(res_inst_tac [("x","M0")] exI 1);
    1.57 +by(case_tac "elem K a" 1);
    1.58 + by(res_inst_tac [("x","I")] exI 1);
    1.59 + by(Simp_tac 1);
    1.60 + by(res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
    1.61 + by(asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
    1.62 + by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
    1.63 + by(asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
    1.64 + by(full_simp_tac (simpset() addsimps [trans_def]) 1);
    1.65 + by(Blast_tac 1);
    1.66 +by(subgoal_tac "elem I a" 1);
    1.67 + by(res_inst_tac [("x","I-{#a#}")] exI 1);
    1.68 + by(res_inst_tac [("x","J+{#a#}")] exI 1);
    1.69 + by(res_inst_tac [("x","K + Ka")] exI 1);
    1.70 + br conjI 1;
    1.71 +  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
    1.72 +                             addsplits [nat_diff_split]) 1);
    1.73 + br conjI 1;
    1.74 +  by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
    1.75 +  by(Asm_full_simp_tac 1);
    1.76 +  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
    1.77 +                             addsplits [nat_diff_split]) 1);
    1.78 + by(full_simp_tac (simpset() addsimps [trans_def]) 1);
    1.79 + by(Blast_tac 1);
    1.80 +by(subgoal_tac "elem (M0 +{#a#}) a" 1);
    1.81 + by(Asm_full_simp_tac 1);
    1.82  by(Simp_tac 1);
    1.83 -
    1.84 +qed "mult_implies_one_step";