summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Tue, 29 May 2012 11:13:00 +0200 | |

changeset 48010 | 0da831254551 |

parent 48009 | 9b9150033b5a |

child 48011 | 391439b10100 |

shortened more multiset proofs

--- a/src/HOL/Library/Multiset.thy Tue May 29 10:30:47 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Tue May 29 11:13:00 2012 +0200 @@ -1542,87 +1542,54 @@ context comp_fun_commute begin +lemma fold_msetG_insertE_aux: + "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'" +proof (induct set: fold_msetG) + case (insertI A y x) show ?case + proof (cases "x = a") + assume "x = a" with insertI show ?case by auto + next + assume "x \<noteq> a" + then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'" + using insertI by auto + have "f x y = f a (f x y')" + unfolding y by (rule fun_left_comm) + moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')" + using y' and `x \<noteq> a` + by (simp add: diff_union_swap [symmetric] fold_msetG.insertI) + ultimately show ?case by fast + qed +qed simp + +lemma fold_msetG_insertE: + assumes "fold_msetG f z (A + {#x#}) v" + obtains y where "v = f x y" and "fold_msetG f z A y" +using assms by (auto dest: fold_msetG_insertE_aux [where a=x]) + lemma fold_msetG_determ: "fold_msetG f z A x \<Longrightarrow> fold_msetG f z A y \<Longrightarrow> y = x" -proof (induct arbitrary: x y z rule: full_multiset_induct) - case (less M x\<^isub>1 x\<^isub>2 Z) - have IH: "\<forall>A. A < M \<longrightarrow> - (\<forall>x x' x''. fold_msetG f x'' A x \<longrightarrow> fold_msetG f x'' A x' - \<longrightarrow> x' = x)" by fact - have Mfoldx\<^isub>1: "fold_msetG f Z M x\<^isub>1" and Mfoldx\<^isub>2: "fold_msetG f Z M x\<^isub>2" by fact+ - show ?case - proof (rule fold_msetG.cases [OF Mfoldx\<^isub>1]) - assume "M = {#}" and "x\<^isub>1 = Z" - then show ?case using Mfoldx\<^isub>2 by auto - next - fix B b u - assume "M = B + {#b#}" and "x\<^isub>1 = f b u" and Bu: "fold_msetG f Z B u" - then have MBb: "M = B + {#b#}" and x\<^isub>1: "x\<^isub>1 = f b u" by auto - show ?case - proof (rule fold_msetG.cases [OF Mfoldx\<^isub>2]) - assume "M = {#}" "x\<^isub>2 = Z" - then show ?case using Mfoldx\<^isub>1 by auto - next - fix C c v - assume "M = C + {#c#}" and "x\<^isub>2 = f c v" and Cv: "fold_msetG f Z C v" - then have MCc: "M = C + {#c#}" and x\<^isub>2: "x\<^isub>2 = f c v" by auto - then have CsubM: "C < M" by simp - from MBb have BsubM: "B < M" by simp - show ?case - proof cases - assume *: "b = c" - then have "B = C" using MBb MCc by auto - with * show ?thesis using Bu Cv x\<^isub>1 x\<^isub>2 CsubM IH by auto - next - assume diff: "b \<noteq> c" - let ?D = "B - {#c#}" - have cinB: "c \<in># B" and binC: "b \<in># C" using MBb MCc diff - by (auto intro: insert_noteq_member dest: sym) - have "B - {#c#} < B" using cinB by (rule mset_less_diff_self) - then have DsubM: "?D < M" using BsubM by (blast intro: order_less_trans) - from MBb MCc have "B + {#b#} = C + {#c#}" by blast - then have [simp]: "B + {#b#} - {#c#} = C" - using MBb MCc binC cinB by auto - have B: "B = ?D + {#c#}" and C: "C = ?D + {#b#}" - using MBb MCc diff binC cinB - by (auto simp: multiset_add_sub_el_shuffle) - then obtain d where Dfoldd: "fold_msetG f Z ?D d" - using fold_msetG_nonempty by iprover - then have "fold_msetG f Z B (f c d)" using cinB - by (rule Diff1_fold_msetG) - then have "f c d = u" using IH BsubM Bu by blast - moreover - have "fold_msetG f Z C (f b d)" using binC cinB diff Dfoldd - by (auto simp: multiset_add_sub_el_shuffle - dest: fold_msetG.insertI [where x=b]) - then have "f b d = v" using IH CsubM Cv by blast - ultimately show ?thesis using x\<^isub>1 x\<^isub>2 - by (auto simp: fun_left_comm) - qed - qed - qed -qed - -lemma fold_mset_insert_aux: - "(fold_msetG f z (A + {#x#}) v) = - (\<exists>y. fold_msetG f z A y \<and> v = f x y)" -apply (rule iffI) - prefer 2 - apply blast -apply (rule_tac A1=A and f1=f in fold_msetG_nonempty [THEN exE]) -apply (blast intro: fold_msetG_determ) -done +proof (induct arbitrary: y set: fold_msetG) + case (insertI A y x v) + from `fold_msetG f z (A + {#x#}) v` + obtain y' where "v = f x y'" and "fold_msetG f z A y'" + by (rule fold_msetG_insertE) + from `fold_msetG f z A y'` have "y' = y" by (rule insertI) + with `v = f x y'` show "v = f x y" by simp +qed fast lemma fold_mset_equality: "fold_msetG f z A y \<Longrightarrow> fold_mset f z A = y" unfolding fold_mset_def by (blast intro: fold_msetG_determ) +lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)" +proof - + from fold_msetG_nonempty fold_msetG_determ + have "\<exists>!x. fold_msetG f z A x" by (rule ex_ex1I) + then show ?thesis unfolding fold_mset_def by (rule theI') +qed + lemma fold_mset_insert: "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)" -apply (simp add: fold_mset_def fold_mset_insert_aux) -apply (rule the_equality) - apply (auto cong add: conj_cong - simp add: fold_mset_def [symmetric] fold_mset_equality fold_msetG_nonempty) -done +by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset) lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A" by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x])