# 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 \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
+by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
+
 lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> 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 \<leftarrow> xs. y = x]"
   by (induct xs) auto
 
+lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (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 \<or> x \<in> 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 \<longrightarrow>
+	(\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> 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 \<noteq> y \<Longrightarrow> 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: "\<lbrakk> multiset_of ys = multiset_of xs; sorted ys\<rbrakk> \<Longrightarrow> sort xs = ys"
+proof (induct xs arbitrary: ys)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs)
+  hence "x \<in> 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 \<le># A + B"
   unfolding mset_le_def by auto
 
+lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
+by (simp add: mset_le_def)
+
+lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> 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 \<le># A"
+  shows "A - B + C = A + C - B"
+proof -
+ from mset_le_exists_conv [of "B" "A"] assms have "\<exists>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) \<le># multiset_of xs"
 apply (induct xs)
  apply auto
@@ -953,6 +1044,38 @@
  apply auto
 done
 
+lemma multiset_of_update: "i < length ls \<Longrightarrow> 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: "\<lbrakk> i < length ls; j < length ls \<rbrakk> \<Longrightarrow> 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 \<le>#" "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: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
+by (cases xs) auto
+
+lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
+by (induct xs, auto simp add: sorted_Cons)
+
+lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
+by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
+
+lemma sorted_remdups[simp]:
+  "sorted l \<Longrightarrow> 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: "\<forall>n \<in> N. k \<le> (n::nat)"
+  shows "inj_on (\<lambda>n. n - k) N"
+proof (rule inj_onI)
+  fix x y
+  assume a: "x \<in> N" "y \<in> 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\<le>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 *}