Added useful general lemmas from the work with the HeapMonad
authorbulwahn
Tue Feb 26 11:18:43 2008 +0100 (2008-02-26)
changeset 26143314c0bcb7df7
parent 26142 3d5df9a56537
child 26144 98d23fc02585
Added useful general lemmas from the work with the HeapMonad
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Feb 26 07:59:59 2008 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Feb 26 11:18:43 2008 +0100
     1.3 @@ -162,6 +162,9 @@
     1.4  lemma diff_union_inverse2 [simp]: "M + {#a#} - {#a#} = M"
     1.5  by (simp add: union_def diff_def in_multiset)
     1.6  
     1.7 +lemma diff_cancel: "A - A = {#}"
     1.8 +by (simp add: diff_def Mempty_def)
     1.9 +
    1.10  
    1.11  subsubsection {* Count of elements *}
    1.12  
    1.13 @@ -359,6 +362,9 @@
    1.14    multiset_inter_assoc
    1.15    multiset_inter_left_commute
    1.16  
    1.17 +lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
    1.18 +by (simp add: multiset_eq_conv_count_eq multiset_inter_count)
    1.19 +
    1.20  lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B - C = A - C + B"
    1.21    apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def
    1.22      split: split_if_asm)
    1.23 @@ -896,6 +902,64 @@
    1.24      "count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]"
    1.25    by (induct xs) auto
    1.26  
    1.27 +lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls"
    1.28 +by (induct ls arbitrary: i, simp, case_tac i, auto)
    1.29 +
    1.30 +lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs - {#a#}"
    1.31 +by (induct xs, auto simp add: multiset_eq_conv_count_eq)
    1.32 +
    1.33 +lemma multiset_of_eq_length:
    1.34 +  assumes "multiset_of xs = multiset_of ys"
    1.35 +  shows "List.length xs = List.length ys"
    1.36 +  using assms
    1.37 +proof (induct arbitrary: ys rule: length_induct)
    1.38 +  case (1 xs ys)
    1.39 +  show ?case
    1.40 +  proof (cases xs)
    1.41 +    case Nil with 1(2) show ?thesis by simp
    1.42 +  next
    1.43 +    case (Cons x xs')
    1.44 +    note xCons = Cons
    1.45 +    show ?thesis
    1.46 +    proof (cases ys)
    1.47 +      case Nil
    1.48 +      with 1(2) Cons show ?thesis by simp
    1.49 +    next
    1.50 +      case (Cons y ys')
    1.51 +      have x_in_ys: "x = y \<or> x \<in> set ys'"
    1.52 +      proof (cases "x = y")
    1.53 +	case True thus ?thesis ..
    1.54 +      next
    1.55 +	case False
    1.56 +	from 1(2)[symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp
    1.57 +	with False show ?thesis by (simp add: mem_set_multiset_eq)
    1.58 +      qed
    1.59 +      from 1(1) have IH: "List.length xs' < List.length xs \<longrightarrow>
    1.60 +	(\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> List.length xs' = List.length x)" by blast
    1.61 +      from 1(2) x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))"
    1.62 +	apply -
    1.63 +	apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff)
    1.64 +	apply fastsimp
    1.65 +	done
    1.66 +      with IH xCons have IH': "List.length xs' = List.length (remove1 x (y#ys'))" by fastsimp
    1.67 +      from x_in_ys have "x \<noteq> y \<Longrightarrow> List.length ys' > 0" by auto
    1.68 +      with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1)
    1.69 +    qed
    1.70 +  qed
    1.71 +qed
    1.72 +
    1.73 +text {* This lemma shows which properties suffice to show that
    1.74 +  a function f with f xs = ys behaves like sort. *}
    1.75 +lemma properties_for_sort: "\<lbrakk> multiset_of ys = multiset_of xs; sorted ys\<rbrakk> \<Longrightarrow> sort xs = ys"
    1.76 +proof (induct xs arbitrary: ys)
    1.77 +  case Nil thus ?case by simp
    1.78 +next
    1.79 +  case (Cons x xs)
    1.80 +  hence "x \<in> set ys" by (auto simp add:  mem_set_multiset_eq intro!: ccontr)
    1.81 +  with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case
    1.82 +    by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1)
    1.83 +qed
    1.84 +
    1.85  
    1.86  subsection {* Pointwise ordering induced by count *}
    1.87  
    1.88 @@ -946,6 +1010,33 @@
    1.89  lemma mset_le_add_right[simp]: "B \<le># A + B"
    1.90    unfolding mset_le_def by auto
    1.91  
    1.92 +lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B"
    1.93 +by (simp add: mset_le_def)
    1.94 +
    1.95 +lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
    1.96 +by (simp add: multiset_eq_conv_count_eq mset_le_def)
    1.97 +
    1.98 +lemma mset_le_multiset_union_diff_commute:
    1.99 +  assumes "B \<le># A"
   1.100 +  shows "A - B + C = A + C - B"
   1.101 +proof -
   1.102 + from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
   1.103 + from this obtain D where "A = B + D" ..
   1.104 + thus ?thesis
   1.105 +   apply -
   1.106 +   apply simp
   1.107 +   apply (subst union_commute)
   1.108 +   apply (subst multiset_diff_union_assoc)
   1.109 +   apply simp
   1.110 +   apply (simp add: diff_cancel)
   1.111 +   apply (subst union_assoc)
   1.112 +   apply (subst union_commute[of "B" _])
   1.113 +   apply (subst multiset_diff_union_assoc)
   1.114 +   apply simp
   1.115 +   apply (simp add: diff_cancel)
   1.116 +   done
   1.117 +qed
   1.118 +
   1.119  lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
   1.120  apply (induct xs)
   1.121   apply auto
   1.122 @@ -953,6 +1044,38 @@
   1.123   apply auto
   1.124  done
   1.125  
   1.126 +lemma multiset_of_update: "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
   1.127 +proof (induct ls arbitrary: i)
   1.128 +  case Nil thus ?case by simp
   1.129 +next
   1.130 +  case (Cons x xs)
   1.131 +  show ?case
   1.132 +    proof (cases i)
   1.133 +      case 0 thus ?thesis by simp
   1.134 +    next
   1.135 +      case (Suc i')
   1.136 +      with Cons show ?thesis
   1.137 +	apply -
   1.138 +	apply simp
   1.139 +	apply (subst union_assoc)
   1.140 +	apply (subst union_commute[where M="{#v#}" and N="{#x#}"])
   1.141 +	apply (subst union_assoc[symmetric])
   1.142 +	apply simp
   1.143 +	apply (rule mset_le_multiset_union_diff_commute)
   1.144 +	apply (simp add: mset_le_single nth_mem_multiset_of)
   1.145 +	done
   1.146 +  qed
   1.147 +qed
   1.148 +
   1.149 +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"
   1.150 +apply (case_tac "i=j")
   1.151 +apply simp
   1.152 +apply (simp add: multiset_of_update)
   1.153 +apply (subst elem_imp_eq_diff_union[symmetric])
   1.154 +apply (simp add: nth_mem_multiset_of)
   1.155 +apply simp
   1.156 +done
   1.157 +
   1.158  interpretation mset_order:
   1.159    order ["op \<le>#" "op <#"]
   1.160    by (auto intro: order.intro mset_le_refl mset_le_antisym
     2.1 --- a/src/HOL/List.thy	Tue Feb 26 07:59:59 2008 +0100
     2.2 +++ b/src/HOL/List.thy	Tue Feb 26 11:18:43 2008 +0100
     2.3 @@ -2655,6 +2655,19 @@
     2.4  theorem sorted_sort[simp]: "sorted (sort xs)"
     2.5  by (induct xs) (auto simp:sorted_insort)
     2.6  
     2.7 +lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
     2.8 +by (cases xs) auto
     2.9 +
    2.10 +lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
    2.11 +by (induct xs, auto simp add: sorted_Cons)
    2.12 +
    2.13 +lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
    2.14 +by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
    2.15 +
    2.16 +lemma sorted_remdups[simp]:
    2.17 +  "sorted l \<Longrightarrow> sorted (remdups l)"
    2.18 +by (induct l) (auto simp: sorted_Cons)
    2.19 +
    2.20  lemma sorted_distinct_set_unique:
    2.21  assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
    2.22  shows "xs = ys"
     3.1 --- a/src/HOL/Nat.thy	Tue Feb 26 07:59:59 2008 +0100
     3.2 +++ b/src/HOL/Nat.thy	Tue Feb 26 11:18:43 2008 +0100
     3.3 @@ -1260,6 +1260,19 @@
     3.4  lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
     3.5  by (simp split add: nat_diff_split)
     3.6  
     3.7 +lemma min_diff: "min (m - (i::nat)) (n - i) = min m n - i"
     3.8 +unfolding min_def by auto
     3.9 +
    3.10 +lemma inj_on_diff_nat: 
    3.11 +  assumes k_le_n: "\<forall>n \<in> N. k \<le> (n::nat)"
    3.12 +  shows "inj_on (\<lambda>n. n - k) N"
    3.13 +proof (rule inj_onI)
    3.14 +  fix x y
    3.15 +  assume a: "x \<in> N" "y \<in> N" "x - k = y - k"
    3.16 +  with k_le_n have "x - k + k = y - k + k" by auto
    3.17 +  with a k_le_n show "x = y" by auto
    3.18 +qed
    3.19 +
    3.20  text{*Rewriting to pull differences out*}
    3.21  
    3.22  lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
     4.1 --- a/src/HOL/Product_Type.thy	Tue Feb 26 07:59:59 2008 +0100
     4.2 +++ b/src/HOL/Product_Type.thy	Tue Feb 26 11:18:43 2008 +0100
     4.3 @@ -821,6 +821,10 @@
     4.4    "prod_case = split"
     4.5    by (auto simp add: expand_fun_eq)
     4.6  
     4.7 +lemma prod_case_beta:
     4.8 +  "prod_case f p = f (fst p) (snd p)"
     4.9 +  unfolding prod_case_split split_beta ..
    4.10 +
    4.11  
    4.12  subsection {* Further cases/induct rules for tuples *}
    4.13