--- a/src/HOL/UNITY/Comp/AllocBase.thy Tue Jul 15 15:20:54 2003 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed Jul 16 12:09:41 2003 +0200
@@ -71,14 +71,13 @@
declare setsum_cong [cong]
lemma bag_of_sublist_lemma:
- "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =
- (\<Sum>i: A Int lessThan k. {#f i#})"
-apply (rule setsum_cong, auto)
-done
+ "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =
+ (\\<Sum>i: A Int lessThan k. {#f i#})"
+by (rule setsum_cong, auto)
lemma bag_of_sublist:
"bag_of (sublist l A) =
- (\<Sum>i: A Int lessThan (length l). {# l!i #})"
+ (\\<Sum>i: A Int lessThan (length l). {# l!i #})"
apply (rule_tac xs = l in rev_induct, simp)
apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append
bag_of_sublist_lemma plus_ac0)
@@ -88,7 +87,8 @@
lemma bag_of_sublist_Un_Int:
"bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) =
bag_of (sublist l A) + bag_of (sublist l B)"
-apply (subgoal_tac "A Int B Int {..length l (} = (A Int {..length l (}) Int (B Int {..length l (}) ")
+apply (subgoal_tac "A Int B Int {..length l (} =
+ (A Int {..length l (}) Int (B Int {..length l (}) ")
apply (simp add: bag_of_sublist Int_Un_distrib2 setsum_Un_Int, blast)
done
@@ -96,13 +96,12 @@
"A Int B = {}
==> bag_of (sublist l (A Un B)) =
bag_of (sublist l A) + bag_of (sublist l B)"
-apply (simp add: bag_of_sublist_Un_Int [symmetric])
-done
+by (simp add: bag_of_sublist_Un_Int [symmetric])
lemma bag_of_sublist_UN_disjoint [rule_format]:
"[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]
==> bag_of (sublist l (UNION I A)) =
- (\<Sum>i:I. bag_of (sublist l (A i)))"
+ (\\<Sum>i:I. bag_of (sublist l (A i)))"
apply (simp del: UN_simps
add: UN_simps [symmetric] add: bag_of_sublist)
apply (subst setsum_UN_disjoint, auto)