author paulson Thu Jun 22 11:37:13 2000 +0200 (2000-06-22) changeset 9107 67202a50ee6d parent 9106 0fe9200f64bd child 9108 9fff97d29837
removed some finiteness conditions from bag_of/sublist theorems
```     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.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])