more code lemmas by Rene Thiemann
authornipkow
Mon Mar 03 16:44:46 2014 +0100 (2014-03-03)
changeset 5588725bd4745ee38
parent 55886 b11b358fec57
child 55888 cac1add157e8
more code lemmas by Rene Thiemann
src/HOL/Library/DAList_Multiset.thy
     1.1 --- a/src/HOL/Library/DAList_Multiset.thy	Mon Mar 03 15:14:00 2014 +0100
     1.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Mon Mar 03 16:44:46 2014 +0100
     1.3 @@ -231,12 +231,17 @@
     1.4  lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1"
     1.5  by (metis equal_multiset_def eq_iff)
     1.6  
     1.7 -lemma mset_less_eq_Bag [code]:
     1.8 +text{* By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
     1.9 +With equality implemented by @{text"\<le>"}, this leads to three calls of  @{text"\<le>"}.
    1.10 +Here is a more efficient version: *}
    1.11 +lemma mset_less[code]: "xs < (ys :: 'a multiset) \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
    1.12 +by (rule less_le_not_le)
    1.13 +
    1.14 +lemma mset_less_eq_Bag0:
    1.15    "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
    1.16      (is "?lhs \<longleftrightarrow> ?rhs")
    1.17  proof
    1.18 -  assume ?lhs then show ?rhs
    1.19 -    by (auto simp add: mset_le_def)
    1.20 +  assume ?lhs thus ?rhs by (auto simp add: mset_le_def)
    1.21  next
    1.22    assume ?rhs
    1.23    show ?lhs
    1.24 @@ -244,15 +249,177 @@
    1.25      fix x
    1.26      from `?rhs` have "count_of (DAList.impl_of xs) x \<le> count A x"
    1.27        by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
    1.28 -    then show "count (Bag xs) x \<le> count A x"
    1.29 -      by (simp add: mset_le_def)
    1.30 +    thus "count (Bag xs) x \<le> count A x" by (simp add: mset_le_def)
    1.31    qed
    1.32  qed
    1.33  
    1.34 +lemma mset_less_eq_Bag [code]:
    1.35 +  "Bag xs \<le> (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
    1.36 +proof -
    1.37 +  {
    1.38 +    fix x n
    1.39 +    assume "(x,n) \<in> set (DAList.impl_of xs)"
    1.40 +    hence "count_of (DAList.impl_of xs) x = n" 
    1.41 +    proof (transfer)
    1.42 +      fix x n and xs :: "('a \<times> nat) list"
    1.43 +      show "(distinct \<circ> map fst) xs \<Longrightarrow> (x, n) \<in> set xs \<Longrightarrow> count_of xs x = n"
    1.44 +      proof (induct xs) 
    1.45 +        case (Cons ym ys)        
    1.46 +        obtain y m where ym: "ym = (y,m)" by force
    1.47 +        note Cons = Cons[unfolded ym]
    1.48 +        show ?case
    1.49 +        proof (cases "x = y")
    1.50 +          case False
    1.51 +          with Cons show ?thesis unfolding ym by auto
    1.52 +        next
    1.53 +          case True
    1.54 +          with Cons(2-3) have "m = n" by force
    1.55 +          with True show ?thesis unfolding ym by auto
    1.56 +        qed
    1.57 +      qed auto
    1.58 +    qed
    1.59 +  }
    1.60 +  thus ?thesis unfolding mset_less_eq_Bag0 by auto
    1.61 +qed
    1.62 +
    1.63  declare multiset_inter_def [code]
    1.64  declare sup_multiset_def [code]
    1.65  declare multiset_of.simps [code]
    1.66  
    1.67 +
    1.68 +fun fold_impl :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a \<times> nat)list \<Rightarrow> 'b" where
    1.69 +  "fold_impl fn e ((a,n) # ms) = (fold_impl fn ((fn a n) e) ms)"
    1.70 +| "fold_impl fn e [] = e"
    1.71 +
    1.72 +definition fold :: "('a \<Rightarrow> nat \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> ('a, nat)alist \<Rightarrow> 'b" where
    1.73 +"fold f e al = fold_impl f e (DAList.impl_of al)"
    1.74 +
    1.75 +hide_const (open) fold
    1.76 +
    1.77 +context comp_fun_commute
    1.78 +begin
    1.79 +
    1.80 +lemma DAList_Multiset_fold: assumes fn: "\<And> a n x. fn a n x = (f a ^^ n) x"
    1.81 +  shows "Multiset.fold f e (Bag al) = DAList_Multiset.fold fn e al"
    1.82 +unfolding DAList_Multiset.fold_def
    1.83 +proof (induct al)
    1.84 +  fix ys
    1.85 +  let ?inv = "{xs :: ('a \<times> nat)list. (distinct \<circ> map fst) xs}"
    1.86 +  note cs[simp del] = count_simps
    1.87 +  have count[simp]: "\<And> x. count (Abs_multiset (count_of x)) = count_of x"
    1.88 +    by (rule Abs_multiset_inverse[OF count_of_multiset])
    1.89 +  assume ys: "ys \<in> ?inv"
    1.90 +  thus "Multiset.fold f e (Bag (Alist ys)) = fold_impl fn e (DAList.impl_of (Alist ys))"
    1.91 +    unfolding Bag_def unfolding Alist_inverse[OF ys]
    1.92 +  proof (induct ys arbitrary: e rule: list.induct)
    1.93 +    case Nil
    1.94 +    show ?case
    1.95 +      by (rule trans[OF arg_cong[of _ "{#}" "Multiset.fold f e", OF multiset_eqI]])
    1.96 +         (auto, simp add: cs)
    1.97 +  next
    1.98 +    case (Cons pair ys e)
    1.99 +    obtain a n where pair: "pair = (a,n)" by force
   1.100 +    from fn[of a n] have [simp]: "fn a n = (f a ^^ n)" by auto
   1.101 +    have inv: "ys \<in> ?inv" using Cons(2) by auto
   1.102 +    note IH = Cons(1)[OF inv]
   1.103 +    def Ys \<equiv> "Abs_multiset (count_of ys)"
   1.104 +    have id: "Abs_multiset (count_of ((a, n) # ys)) = ((op + {# a #}) ^^ n) Ys"
   1.105 +      unfolding Ys_def
   1.106 +    proof (rule multiset_eqI, unfold count)
   1.107 +      fix c      
   1.108 +      show "count_of ((a, n) # ys) c = count ((op + {#a#} ^^ n) (Abs_multiset (count_of ys))) c" (is "?l = ?r")
   1.109 +      proof (cases "c = a")
   1.110 +        case False thus ?thesis unfolding cs by (induct n) auto
   1.111 +      next
   1.112 +        case True
   1.113 +        hence "?l = n" by (simp add: cs)
   1.114 +        also have "n = ?r" unfolding True
   1.115 +        proof (induct n)
   1.116 +          case 0
   1.117 +          from Cons(2)[unfolded pair] have "a \<notin> fst ` set ys" by auto
   1.118 +          thus ?case by (induct ys) (simp, auto simp: cs)
   1.119 +        qed auto
   1.120 +        finally show ?thesis .
   1.121 +      qed
   1.122 +    qed
   1.123 +    show ?case unfolding pair    
   1.124 +      by (simp add: IH[symmetric], unfold id Ys_def[symmetric],
   1.125 +      induct n, auto simp: fold_mset_fun_left_comm[symmetric])
   1.126 +  qed
   1.127 +qed
   1.128 +
   1.129 +end 
   1.130 +
   1.131 +lift_definition single_alist_entry :: "'a \<Rightarrow> 'b \<Rightarrow> ('a,'b)alist" is "\<lambda> a b. [(a,b)]" by auto
   1.132 +
   1.133 +lemma image_mset_Bag[code]:
   1.134 +  "image_mset f (Bag ms) =
   1.135 +   DAList_Multiset.fold (\<lambda> a n m. Bag (single_alist_entry (f a) n) + m) {#} ms"
   1.136 +unfolding image_mset_def 
   1.137 +proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
   1.138 +  fix a n m
   1.139 +  show "Bag (single_alist_entry (f a) n) + m = ((op + \<circ> single \<circ> f) a ^^ n) m" (is "?l = ?r")
   1.140 +  proof (rule multiset_eqI)
   1.141 +    fix x
   1.142 +    have "count ?r x = (if x = f a then n + count m x else count m x)"
   1.143 +      by (induct n, auto)
   1.144 +    also have "\<dots> = count ?l x" by (simp add: single_alist_entry.rep_eq)
   1.145 +    finally show "count ?l x = count ?r x" ..
   1.146 +  qed
   1.147 +qed
   1.148 +
   1.149 +hide_const single_alist_entry
   1.150 +
   1.151 +(* we cannot use (\<lambda> a n. op + (a * n)) for folding, since * is not defined
   1.152 +   in comm_monoid_add *)
   1.153 +lemma msetsum_Bag[code]:
   1.154 +  "msetsum (Bag ms) = DAList_Multiset.fold (\<lambda> a n. ((op + a) ^^ n)) 0 ms"
   1.155 +unfolding msetsum.eq_fold
   1.156 +by (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, auto simp: ac_simps)
   1.157 +
   1.158 +(* we cannot use (\<lambda> a n. op * (a ^ n)) for folding, since ^ is not defined
   1.159 +   in comm_monoid_mult *)
   1.160 +lemma msetprod_Bag[code]:
   1.161 +  "msetprod (Bag ms) = DAList_Multiset.fold (\<lambda> a n. ((op * a) ^^ n)) 1 ms"
   1.162 +unfolding msetprod.eq_fold
   1.163 +by (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, auto simp: ac_simps)
   1.164 +
   1.165 +lemma mcard_fold: "mcard A = Multiset.fold (\<lambda> _. Suc) 0 A" (is "_ = Multiset.fold ?f _ _")
   1.166 +proof -
   1.167 +  interpret comp_fun_commute ?f by (default, auto)
   1.168 +  show ?thesis by (induct A) auto
   1.169 +qed
   1.170 +
   1.171 +lemma mcard_Bag[code]:
   1.172 +  "mcard (Bag ms) = DAList_Multiset.fold (\<lambda> a n. op + n) 0 ms"
   1.173 +unfolding mcard_fold
   1.174 +proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, simp)
   1.175 +  fix a n x
   1.176 +  show "n + x = (Suc ^^ n) x" by (induct n) auto
   1.177 +qed
   1.178 +
   1.179 +
   1.180 +lemma set_of_fold: "set_of A = Multiset.fold insert {} A" (is "_ = Multiset.fold ?f _ _")
   1.181 +proof -
   1.182 +  interpret comp_fun_commute ?f by (default, auto)
   1.183 +  show ?thesis by (induct A, auto)
   1.184 +qed
   1.185 +
   1.186 +lemma set_of_Bag[code]:
   1.187 +  "set_of (Bag ms) = DAList_Multiset.fold (\<lambda> a n. (if n = 0 then (\<lambda> m. m) else insert a)) {} ms"
   1.188 +unfolding set_of_fold
   1.189 +proof (rule comp_fun_commute.DAList_Multiset_fold, unfold_locales, (auto simp: ac_simps)[1])
   1.190 +  fix a n x
   1.191 +  show "(if n = 0 then \<lambda>m. m else insert a) x = (insert a ^^ n) x" (is "?l n = ?r n")
   1.192 +  proof (cases n)
   1.193 +    case (Suc m)
   1.194 +    hence "?l n = insert a x" by simp
   1.195 +    moreover have "?r n = insert a x" unfolding Suc by (induct m) auto
   1.196 +    ultimately show ?thesis by auto
   1.197 +  qed auto
   1.198 +qed
   1.199 +
   1.200 +
   1.201  instantiation multiset :: (exhaustive) exhaustive
   1.202  begin
   1.203