src/HOL/UNITY/Comp/AllocBase.thy
changeset 15074 277b3a4da341
parent 15045 d59f7e2e18d3
child 16417 9bc16273c2d4
equal deleted inserted replaced
15073:279c2daaf517 15074:277b3a4da341
    69 (** setsum **)
    69 (** setsum **)
    70 
    70 
    71 declare setsum_cong [cong]
    71 declare setsum_cong [cong]
    72 
    72 
    73 lemma bag_of_sublist_lemma:
    73 lemma bag_of_sublist_lemma:
    74      "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
    74      "(\<Sum>i\<in> A Int lessThan k. {#if i<k then f i else g i#}) =  
    75       (\<Sum>i: A Int lessThan k. {#f i#})"
    75       (\<Sum>i\<in> A Int lessThan k. {#f i#})"
    76 by (rule setsum_cong, auto)
    76 by (rule setsum_cong, auto)
    77 
    77 
    78 lemma bag_of_sublist:
    78 lemma bag_of_sublist:
    79      "bag_of (sublist l A) =  
    79      "bag_of (sublist l A) =  
    80       (\<Sum>i: A Int lessThan (length l). {# l!i #})"
    80       (\<Sum>i\<in> A Int lessThan (length l). {# l!i #})"
    81 apply (rule_tac xs = l in rev_induct, simp)
    81 apply (rule_tac xs = l in rev_induct, simp)
    82 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    82 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    83                  bag_of_sublist_lemma add_ac)
    83                  bag_of_sublist_lemma add_ac)
    84 done
    84 done
    85 
    85 
    99 by (simp add: bag_of_sublist_Un_Int [symmetric])
    99 by (simp add: bag_of_sublist_Un_Int [symmetric])
   100 
   100 
   101 lemma bag_of_sublist_UN_disjoint [rule_format]:
   101 lemma bag_of_sublist_UN_disjoint [rule_format]:
   102      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
   102      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
   103       ==> bag_of (sublist l (UNION I A)) =   
   103       ==> bag_of (sublist l (UNION I A)) =   
   104           (\<Sum>i:I. bag_of (sublist l (A i)))"
   104           (\<Sum>i\<in>I. bag_of (sublist l (A i)))"
   105 apply (simp del: UN_simps 
   105 apply (simp del: UN_simps 
   106             add: UN_simps [symmetric] add: bag_of_sublist)
   106             add: UN_simps [symmetric] add: bag_of_sublist)
   107 apply (subst setsum_UN_disjoint, auto)
   107 apply (subst setsum_UN_disjoint, auto)
   108 done
   108 done
   109 
   109