removed some finiteness conditions from bag_of/sublist theorems
authorpaulson
Thu Jun 22 11:37:13 2000 +0200 (2000-06-22)
changeset 910767202a50ee6d
parent 9106 0fe9200f64bd
child 9108 9fff97d29837
removed some finiteness conditions from bag_of/sublist theorems
src/HOL/UNITY/AllocBase.ML
     1.1 --- a/src/HOL/UNITY/AllocBase.ML	Thu Jun 22 11:36:08 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.ML	Thu Jun 22 11:37:13 2000 +0200
     1.3 @@ -95,30 +95,46 @@
     1.4  by (rtac union_upper1 1); 
     1.5  qed "mono_bag_of";
     1.6  
     1.7 -Goal "finite A ==> \
     1.8 -\     setsum (%i. if i < Suc(length zs) then {#(zs @ [z]) ! i#} else {#}) A = \
     1.9 -\       setsum (%i. if i < length zs then {#zs ! i#} else {#}) A + \
    1.10 -\       (if length zs : A then {#z#} else {#})";
    1.11 -by (etac finite_induct 1);
    1.12 -by (Simp_tac 1);
    1.13 -by (asm_simp_tac (simpset() addsimps (nth_append :: thms "plus_ac0")) 1);
    1.14 -by (subgoal_tac "x < Suc (length zs) & ~ x < length zs --> length zs = x" 1);
    1.15 -by Auto_tac;
    1.16 +(** setsum **)
    1.17 +
    1.18 +Addcongs [setsum_cong];
    1.19 +
    1.20 +Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
    1.21 +\     setsum (%i. {#f i#}) (A Int lessThan k)";
    1.22 +by (rtac setsum_cong 1);
    1.23 +by Auto_tac;  
    1.24  qed "bag_of_sublist_lemma";
    1.25  
    1.26 -Goal "finite A \
    1.27 -\     ==> bag_of (sublist l A) = \
    1.28 -\         setsum (%i. if i < length l then {# nth l i #} else {#}) A";
    1.29 +Goal "bag_of (sublist l A) = \
    1.30 +\     setsum (%i. {# l!i #}) (A Int lessThan (length l))";
    1.31  by (res_inst_tac [("xs","l")] rev_induct 1);
    1.32  by (Simp_tac 1);
    1.33 -by (stac (symmetric Zero_def) 1);
    1.34 -by (rtac (setsum_0 RS sym) 1);
    1.35 -by (asm_simp_tac (simpset() addsimps [sublist_append, 
    1.36 -				      bag_of_sublist_lemma]) 1);
    1.37 +by (asm_simp_tac
    1.38 +    (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc, 
    1.39 +                    nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
    1.40  qed "bag_of_sublist";
    1.41  
    1.42 -Goal "[| finite A; finite B |] \
    1.43 -\     ==> bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
    1.44 -\         bag_of (sublist l A) + bag_of (sublist l B)";
    1.45 -by (asm_simp_tac (simpset() addsimps [bag_of_sublist, setsum_Un_Int]) 1);
    1.46 +
    1.47 +Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
    1.48 +\     bag_of (sublist l A) + bag_of (sublist l B)";
    1.49 +by (subgoal_tac "A Int B Int {..length l(} = \
    1.50 +\                (A Int {..length l(}) Int (B Int {..length l(})" 1);
    1.51 +by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2, 
    1.52 +                                      setsum_Un_Int]) 1);
    1.53 +by (Blast_tac 1);
    1.54  qed "bag_of_sublist_Un_Int";
    1.55 +
    1.56 +Goal "A Int B = {} \
    1.57 +\     ==> bag_of (sublist l (A Un B)) = \
    1.58 +\         bag_of (sublist l A) + bag_of (sublist l B)"; 
    1.59 +by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
    1.60 +qed "bag_of_sublist_Un_disjoint";
    1.61 +
    1.62 +Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
    1.63 +\     ==> bag_of (sublist l (UNION I A)) =  \
    1.64 +\         setsum (%i. bag_of (sublist l (A i))) I";  
    1.65 +by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
    1.66 +			    addsimps [bag_of_sublist]) 1);
    1.67 +by (stac setsum_UN_disjoint 1);
    1.68 +by Auto_tac;  
    1.69 +qed_spec_mp "bag_of_sublist_UN_disjoint";