# HG changeset patch # User bulwahn # Date 1204021123 -3600 # Node ID 314c0bcb7df746d3ef4b5faf13d39cd0c5a8d690 # Parent 3d5df9a565372aa90f802ad86c747e36eea2ef6d Added useful general lemmas from the work with the HeapMonad diff -r 3d5df9a56537 -r 314c0bcb7df7 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Feb 26 07:59:59 2008 +0100 +++ b/src/HOL/Library/Multiset.thy Tue Feb 26 11:18:43 2008 +0100 @@ -162,6 +162,9 @@ lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M" by (simp add: union_def diff_def in_multiset) +lemma diff_cancel: "A - A = {#}" +by (simp add: diff_def Mempty_def) + subsubsection {* Count of elements *} @@ -359,6 +362,9 @@ multiset_inter_assoc multiset_inter_left_commute +lemma multiset_inter_single: "a \ b \ {#a#} #\ {#b#} = {#}" +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 split: split_if_asm) @@ -896,6 +902,64 @@ "count (multiset_of xs) x = length [y \ xs. y = x]" by (induct xs) auto +lemma nth_mem_multiset_of: "i < length ls \ (ls ! i) :# multiset_of ls" +by (induct ls arbitrary: i, simp, case_tac i, auto) + +lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}" +by (induct xs, auto simp add: multiset_eq_conv_count_eq) + +lemma multiset_of_eq_length: + assumes "multiset_of xs = multiset_of ys" + shows "List.length xs = List.length ys" + using assms +proof (induct arbitrary: ys rule: length_induct) + case (1 xs ys) + show ?case + proof (cases xs) + case Nil with 1(2) show ?thesis by simp + next + case (Cons x xs') + note xCons = Cons + show ?thesis + proof (cases ys) + case Nil + with 1(2) Cons show ?thesis by simp + next + case (Cons y ys') + have x_in_ys: "x = y \ x \ set ys'" + proof (cases "x = y") + case True thus ?thesis .. + next + case False + from 1(2)[symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp + with False show ?thesis by (simp add: mem_set_multiset_eq) + qed + from 1(1) have IH: "List.length xs' < List.length xs \ + (\x. multiset_of xs' = multiset_of x \ List.length xs' = List.length x)" by blast + from 1(2) x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))" + apply - + apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff) + apply fastsimp + done + with IH xCons have IH': "List.length xs' = List.length (remove1 x (y#ys'))" by fastsimp + from x_in_ys have "x \ y \ List.length ys' > 0" by auto + with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1) + qed + qed +qed + +text {* This lemma shows which properties suffice to show that + a function f with f xs = ys behaves like sort. *} +lemma properties_for_sort: "\ multiset_of ys = multiset_of xs; sorted ys\ \ sort xs = ys" +proof (induct xs arbitrary: ys) + case Nil thus ?case by simp +next + case (Cons x xs) + hence "x \ set ys" by (auto simp add: mem_set_multiset_eq intro!: ccontr) + with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case + by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1) +qed + subsection {* Pointwise ordering induced by count *} @@ -946,6 +1010,33 @@ lemma mset_le_add_right[simp]: "B \# A + B" unfolding mset_le_def by auto +lemma mset_le_single: "a :# B \ {#a#} \# B" +by (simp add: mset_le_def) + +lemma multiset_diff_union_assoc: "C \# B \ A + B - C = A + (B - C)" +by (simp add: multiset_eq_conv_count_eq mset_le_def) + +lemma mset_le_multiset_union_diff_commute: + assumes "B \# A" + shows "A - B + C = A + C - B" +proof - + from mset_le_exists_conv [of "B" "A"] assms have "\D. A = B + D" .. + from this obtain D where "A = B + D" .. + thus ?thesis + apply - + apply simp + apply (subst union_commute) + apply (subst multiset_diff_union_assoc) + apply simp + apply (simp add: diff_cancel) + apply (subst union_assoc) + apply (subst union_commute[of "B" _]) + apply (subst multiset_diff_union_assoc) + apply simp + apply (simp add: diff_cancel) + done +qed + lemma multiset_of_remdups_le: "multiset_of (remdups xs) \# multiset_of xs" apply (induct xs) apply auto @@ -953,6 +1044,38 @@ apply auto done +lemma multiset_of_update: "i < length ls \ multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}" +proof (induct ls arbitrary: i) + case Nil thus ?case by simp +next + case (Cons x xs) + show ?case + proof (cases i) + case 0 thus ?thesis by simp + next + case (Suc i') + with Cons show ?thesis + apply - + apply simp + apply (subst union_assoc) + apply (subst union_commute[where M="{#v#}" and N="{#x#}"]) + apply (subst union_assoc[symmetric]) + apply simp + apply (rule mset_le_multiset_union_diff_commute) + apply (simp add: mset_le_single nth_mem_multiset_of) + done + qed +qed + +lemma multiset_of_swap: "\ i < length ls; j < length ls \ \ multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls" +apply (case_tac "i=j") +apply simp +apply (simp add: multiset_of_update) +apply (subst elem_imp_eq_diff_union[symmetric]) +apply (simp add: nth_mem_multiset_of) +apply simp +done + interpretation mset_order: order ["op \#" "op <#"] by (auto intro: order.intro mset_le_refl mset_le_antisym diff -r 3d5df9a56537 -r 314c0bcb7df7 src/HOL/List.thy --- a/src/HOL/List.thy Tue Feb 26 07:59:59 2008 +0100 +++ b/src/HOL/List.thy Tue Feb 26 11:18:43 2008 +0100 @@ -2655,6 +2655,19 @@ theorem sorted_sort[simp]: "sorted (sort xs)" by (induct xs) (auto simp:sorted_insort) +lemma insort_is_Cons: "\x\set xs. a \ x \ insort a xs = a # xs" +by (cases xs) auto + +lemma sorted_remove1: "sorted xs \ sorted (remove1 a xs)" +by (induct xs, auto simp add: sorted_Cons) + +lemma insort_remove1: "\ a \ set xs; sorted xs \ \ insort a (remove1 a xs) = xs" +by (induct xs, auto simp add: sorted_Cons insort_is_Cons) + +lemma sorted_remdups[simp]: + "sorted l \ sorted (remdups l)" +by (induct l) (auto simp: sorted_Cons) + lemma sorted_distinct_set_unique: assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys" shows "xs = ys" diff -r 3d5df9a56537 -r 314c0bcb7df7 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Feb 26 07:59:59 2008 +0100 +++ b/src/HOL/Nat.thy Tue Feb 26 11:18:43 2008 +0100 @@ -1260,6 +1260,19 @@ lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n" by (simp split add: nat_diff_split) +lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i" +unfolding min_def by auto + +lemma inj_on_diff_nat: + assumes k_le_n: "\n \ N. k \ (n::nat)" + shows "inj_on (\n. n - k) N" +proof (rule inj_onI) + fix x y + assume a: "x \ N" "y \ N" "x - k = y - k" + with k_le_n have "x - k + k = y - k + k" by auto + with a k_le_n show "x = y" by auto +qed + text{*Rewriting to pull differences out*} lemma diff_diff_right [simp]: "k\j --> i - (j - k) = i + (k::nat) - j" diff -r 3d5df9a56537 -r 314c0bcb7df7 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Feb 26 07:59:59 2008 +0100 +++ b/src/HOL/Product_Type.thy Tue Feb 26 11:18:43 2008 +0100 @@ -821,6 +821,10 @@ "prod_case = split" by (auto simp add: expand_fun_eq) +lemma prod_case_beta: + "prod_case f p = f (fst p) (snd p)" + unfolding prod_case_split split_beta .. + subsection {* Further cases/induct rules for tuples *}