simplified construction of fold combinator on multisets;
authorhaftmann
Thu Oct 11 11:56:42 2012 +0200 (2012-10-11)
changeset 498220cfc1651be25
parent 49814 0aaed83532e1
child 49823 1c146fa7701e
simplified construction of fold combinator on multisets;
more coherent name for fold combinator on multisets
NEWS
src/HOL/Library/Multiset.thy
     1.1 --- a/NEWS	Thu Oct 11 00:13:21 2012 +0200
     1.2 +++ b/NEWS	Thu Oct 11 11:56:42 2012 +0200
     1.3 @@ -62,6 +62,16 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory "Library/Multiset":
     1.8 +
     1.9 +  - Renamed constants
    1.10 +      fold_mset ~> Multiset.fold  -- for coherence with other fold combinators
    1.11 +
    1.12 +  - Renamed facts
    1.13 +      fold_mset_commute ~> fold_mset_comm  -- for coherence with fold_comm
    1.14 +
    1.15 +INCOMPATIBILITY.
    1.16 +
    1.17  * Theorem UN_o generalized to SUP_comp.  INCOMPATIBILITY.
    1.18  
    1.19  * Class "comm_monoid_diff" formalises properties of bounded
     2.1 --- a/src/HOL/Library/Multiset.thy	Thu Oct 11 00:13:21 2012 +0200
     2.2 +++ b/src/HOL/Library/Multiset.thy	Thu Oct 11 11:56:42 2012 +0200
     2.3 @@ -657,146 +657,82 @@
     2.4  
     2.5  subsection {* The fold combinator *}
     2.6  
     2.7 -text {*
     2.8 -  The intended behaviour is
     2.9 -  @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"}
    2.10 -  if @{text f} is associative-commutative. 
    2.11 -*}
    2.12 -
    2.13 -text {*
    2.14 -  The graph of @{text "fold_mset"}, @{text "z"}: the start element,
    2.15 -  @{text "f"}: folding function, @{text "A"}: the multiset, @{text
    2.16 -  "y"}: the result.
    2.17 -*}
    2.18 -inductive 
    2.19 -  fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool" 
    2.20 -  for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
    2.21 -  and z :: 'b
    2.22 +definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b"
    2.23  where
    2.24 -  emptyI [intro]:  "fold_msetG f z {#} z"
    2.25 -| insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)"
    2.26 +  "fold f s M = Finite_Set.fold (\<lambda>x. f x ^^ count M x) s (set_of M)"
    2.27  
    2.28 -inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x"
    2.29 -inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" 
    2.30 -
    2.31 -definition
    2.32 -  fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where
    2.33 -  "fold_mset f z A = (THE x. fold_msetG f z A x)"
    2.34 -
    2.35 -lemma Diff1_fold_msetG:
    2.36 -  "fold_msetG f z (A - {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)"
    2.37 -apply (frule_tac x = x in fold_msetG.insertI)
    2.38 -apply auto
    2.39 -done
    2.40 -
    2.41 -lemma fold_msetG_nonempty: "\<exists>x. fold_msetG f z A x"
    2.42 -apply (induct A)
    2.43 - apply blast
    2.44 -apply clarsimp
    2.45 -apply (drule_tac x = x in fold_msetG.insertI)
    2.46 -apply auto
    2.47 -done
    2.48 -
    2.49 -lemma fold_mset_empty[simp]: "fold_mset f z {#} = z"
    2.50 -unfolding fold_mset_def by blast
    2.51 +lemma fold_mset_empty [simp]:
    2.52 +  "fold f s {#} = s"
    2.53 +  by (simp add: fold_def)
    2.54  
    2.55  context comp_fun_commute
    2.56  begin
    2.57  
    2.58 -lemma fold_msetG_insertE_aux:
    2.59 -  "fold_msetG f z A y \<Longrightarrow> a \<in># A \<Longrightarrow> \<exists>y'. y = f a y' \<and> fold_msetG f z (A - {#a#}) y'"
    2.60 -proof (induct set: fold_msetG)
    2.61 -  case (insertI A y x) show ?case
    2.62 -  proof (cases "x = a")
    2.63 -    assume "x = a" with insertI show ?case by auto
    2.64 +lemma fold_mset_insert:
    2.65 +  "fold f s (M + {#x#}) = f x (fold f s M)"
    2.66 +proof -
    2.67 +  interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
    2.68 +    by (fact comp_fun_commute_funpow)
    2.69 +  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
    2.70 +    by (fact comp_fun_commute_funpow)
    2.71 +  show ?thesis
    2.72 +  proof (cases "x \<in> set_of M")
    2.73 +    case False
    2.74 +    then have *: "count (M + {#x#}) x = 1" by simp
    2.75 +    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_of M) =
    2.76 +      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_of M)"
    2.77 +      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
    2.78 +    with False * show ?thesis
    2.79 +      by (simp add: fold_def del: count_union)
    2.80    next
    2.81 -    assume "x \<noteq> a"
    2.82 -    then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'"
    2.83 -      using insertI by auto
    2.84 -    have "f x y = f a (f x y')"
    2.85 -      unfolding y by (rule fun_left_comm)
    2.86 -    moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')"
    2.87 -      using y' and `x \<noteq> a`
    2.88 -      by (simp add: diff_union_swap [symmetric] fold_msetG.insertI)
    2.89 -    ultimately show ?case by fast
    2.90 +    case True
    2.91 +    def N \<equiv> "set_of M - {x}"
    2.92 +    from N_def True have *: "set_of M = insert x N" "x \<notin> N" "finite N" by auto
    2.93 +    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
    2.94 +      Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
    2.95 +      by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
    2.96 +    with * show ?thesis by (simp add: fold_def del: count_union) simp
    2.97    qed
    2.98 -qed simp
    2.99 -
   2.100 -lemma fold_msetG_insertE:
   2.101 -  assumes "fold_msetG f z (A + {#x#}) v"
   2.102 -  obtains y where "v = f x y" and "fold_msetG f z A y"
   2.103 -using assms by (auto dest: fold_msetG_insertE_aux [where a=x])
   2.104 -
   2.105 -lemma fold_msetG_determ:
   2.106 -  "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x"
   2.107 -proof (induct arbitrary: y set: fold_msetG)
   2.108 -  case (insertI A y x v)
   2.109 -  from `fold_msetG f z (A + {#x#}) v`
   2.110 -  obtain y' where "v = f x y'" and "fold_msetG f z A y'"
   2.111 -    by (rule fold_msetG_insertE)
   2.112 -  from `fold_msetG f z A y'` have "y' = y" by (rule insertI)
   2.113 -  with `v = f x y'` show "v = f x y" by simp
   2.114 -qed fast
   2.115 -
   2.116 -lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y"
   2.117 -unfolding fold_mset_def by (blast intro: fold_msetG_determ)
   2.118 -
   2.119 -lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)"
   2.120 -proof -
   2.121 -  from fold_msetG_nonempty fold_msetG_determ
   2.122 -  have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I)
   2.123 -  then show ?thesis unfolding fold_mset_def by (rule theI')
   2.124  qed
   2.125  
   2.126 -lemma fold_mset_insert:
   2.127 -  "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)"
   2.128 -by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset)
   2.129 +corollary fold_mset_single [simp]:
   2.130 +  "fold f s {#x#} = f x s"
   2.131 +proof -
   2.132 +  have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
   2.133 +  then show ?thesis by simp
   2.134 +qed
   2.135  
   2.136 -lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A"
   2.137 -by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])
   2.138 -
   2.139 -lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z"
   2.140 -using fold_mset_insert [of z "{#}"] by simp
   2.141 +lemma fold_mset_fun_comm:
   2.142 +  "f x (fold f s M) = fold f (f x s) M"
   2.143 +  by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
   2.144  
   2.145  lemma fold_mset_union [simp]:
   2.146 -  "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B"
   2.147 -proof (induct A)
   2.148 +  "fold f s (M + N) = fold f (fold f s M) N"
   2.149 +proof (induct M)
   2.150    case empty then show ?case by simp
   2.151  next
   2.152 -  case (add A x)
   2.153 -  have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac)
   2.154 -  then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" 
   2.155 -    by (simp add: fold_mset_insert)
   2.156 -  also have "\<dots> = fold_mset f (fold_mset f z (A + {#x#})) B"
   2.157 -    by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert)
   2.158 -  finally show ?case .
   2.159 +  case (add M x)
   2.160 +  have "M + {#x#} + N = (M + N) + {#x#}"
   2.161 +    by (simp add: add_ac)
   2.162 +  with add show ?case by (simp add: fold_mset_insert fold_mset_fun_comm)
   2.163  qed
   2.164  
   2.165  lemma fold_mset_fusion:
   2.166    assumes "comp_fun_commute g"
   2.167 -  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
   2.168 +  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold g w A) = fold f (h w) A" (is "PROP ?P")
   2.169  proof -
   2.170    interpret comp_fun_commute g by (fact assms)
   2.171    show "PROP ?P" by (induct A) auto
   2.172  qed
   2.173  
   2.174 -lemma fold_mset_rec:
   2.175 -  assumes "a \<in># A" 
   2.176 -  shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))"
   2.177 -proof -
   2.178 -  from assms obtain A' where "A = A' + {#a#}"
   2.179 -    by (blast dest: multi_member_split)
   2.180 -  then show ?thesis by simp
   2.181 -qed
   2.182 -
   2.183  end
   2.184  
   2.185  text {*
   2.186    A note on code generation: When defining some function containing a
   2.187 -  subterm @{term"fold_mset F"}, code generation is not automatic. When
   2.188 +  subterm @{term "fold F"}, code generation is not automatic. When
   2.189    interpreting locale @{text left_commutative} with @{text F}, the
   2.190 -  would be code thms for @{const fold_mset} become thms like
   2.191 -  @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but
   2.192 +  would be code thms for @{const fold} become thms like
   2.193 +  @{term "fold F z {#} = z"} where @{text F} is not a pattern but
   2.194    contains defined symbols, i.e.\ is not a code thm. Hence a separate
   2.195    constant with its own code thms needs to be introduced for @{text
   2.196    F}. See the image operator below.
   2.197 @@ -806,7 +742,7 @@
   2.198  subsection {* Image *}
   2.199  
   2.200  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   2.201 -  "image_mset f = fold_mset (op + o single o f) {#}"
   2.202 +  "image_mset f = fold (plus o single o f) {#}"
   2.203  
   2.204  interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
   2.205  proof qed (simp add: add_ac fun_eq_iff)
   2.206 @@ -989,7 +925,7 @@
   2.207  lemma fold_multiset_equiv:
   2.208    assumes f: "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set xs \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
   2.209      and equiv: "multiset_of xs = multiset_of ys"
   2.210 -  shows "fold f xs = fold f ys"
   2.211 +  shows "List.fold f xs = List.fold f ys"
   2.212  using f equiv [symmetric]
   2.213  proof (induct xs arbitrary: ys)
   2.214    case Nil then show ?case by simp
   2.215 @@ -999,8 +935,8 @@
   2.216    have "\<And>x y. x \<in> set ys \<Longrightarrow> y \<in> set ys \<Longrightarrow> f x \<circ> f y = f y \<circ> f x" 
   2.217      by (rule Cons.prems(1)) (simp_all add: *)
   2.218    moreover from * have "x \<in> set ys" by simp
   2.219 -  ultimately have "fold f ys = fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   2.220 -  moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   2.221 +  ultimately have "List.fold f ys = List.fold f (remove1 x ys) \<circ> f x" by (fact fold_remove1_split)
   2.222 +  moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps)
   2.223    ultimately show ?case by simp
   2.224  qed
   2.225  
   2.226 @@ -1915,5 +1851,7 @@
   2.227      multiset_postproc
   2.228  *}
   2.229  
   2.230 +hide_const (open) fold
   2.231 +
   2.232  end
   2.233