# HG changeset patch # User nipkow # Date 1251480949 -7200 # Node ID 620a5d8cfa78dfe1b516f0156ec9fb58dcda21de # Parent 66f1a0dfe7d904e21bcf6bbcb3be8b675bfbb9cc tuned proofs diff -r 66f1a0dfe7d9 -r 620a5d8cfa78 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Aug 28 19:15:59 2009 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Aug 28 19:35:49 2009 +0200 @@ -331,7 +331,7 @@ lemma multiset_inter_count: "count (A #\ B) x = min (count A x) (count B x)" -by (simp add: multiset_inter_def min_def) +by (simp add: multiset_inter_def) lemma multiset_inter_commute: "A #\ B = B #\ A" by (simp add: multiset_eq_conv_count_eq multiset_inter_count @@ -353,7 +353,7 @@ by (simp add: multiset_eq_conv_count_eq multiset_inter_count) lemma multiset_union_diff_commute: "B #\ C = {#} \ A + B - C = A - C + B" -apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def +apply (simp add: multiset_eq_conv_count_eq multiset_inter_count split: split_if_asm) apply clarsimp apply (erule_tac x = a in allE) diff -r 66f1a0dfe7d9 -r 620a5d8cfa78 src/HOL/Library/Word.thy --- a/src/HOL/Library/Word.thy Fri Aug 28 19:15:59 2009 +0200 +++ b/src/HOL/Library/Word.thy Fri Aug 28 19:35:49 2009 +0200 @@ -1519,9 +1519,7 @@ proof - have "((2::int) ^ (length w1 - 1)) + (2 ^ (length w2 - 1)) \ 2 ^ (max (length w1) (length w2) - 1) + 2 ^ (max (length w1) (length w2) - 1)" - apply (cases "length w1 \ length w2") - apply (auto simp add: max_def) - done + by (auto simp:max_def) also have "... = 2 ^ max (length w1) (length w2)" proof - from lw @@ -2173,16 +2171,16 @@ apply (subst bv_sliceI [where ?j = i and ?i = j and ?w = w and ?w1.0 = "w1 @ w2" and ?w2.0 = w3 and ?w3.0 = "w4 @ w5"]) apply simp_all apply (rule w_def) - apply (simp add: w_defs min_def) - apply (simp add: w_defs min_def) + apply (simp add: w_defs) + apply (simp add: w_defs) apply (subst bv_sliceI [where ?j = k and ?i = l and ?w = w and ?w1.0 = w1 and ?w2.0 = "w2 @ w3 @ w4" and ?w3.0 = w5]) apply simp_all apply (rule w_def) - apply (simp add: w_defs min_def) - apply (simp add: w_defs min_def) + apply (simp add: w_defs) + apply (simp add: w_defs) apply (subst bv_sliceI [where ?j = "i-k" and ?i = "j-k" and ?w = "w2 @ w3 @ w4" and ?w1.0 = w2 and ?w2.0 = w3 and ?w3.0 = w4]) apply simp_all - apply (simp_all add: w_defs min_def) + apply (simp_all add: w_defs) done qed