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

author | haftmann |

Mon, 22 Feb 2010 09:15:10 +0100 | |

changeset 35272 | c283ae736bea |

parent 35271 | 586d800321f5 |

child 35273 | 51692ec1b220 |

switched notations for pointwise and multiset order

src/HOL/Algebra/Divisibility.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Library/Permutation.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Algebra/Divisibility.thy Mon Feb 22 09:15:10 2010 +0100 +++ b/src/HOL/Algebra/Divisibility.thy Mon Feb 22 09:15:10 2010 +0100 @@ -2250,7 +2250,7 @@ assumes ab: "a divides b" and afs: "wfactors G as a" and bfs: "wfactors G bs b" and carr: "a \<in> carrier G" "b \<in> carrier G" "set as \<subseteq> carrier G" "set bs \<subseteq> carrier G" - shows "fmset G as \<le># fmset G bs" + shows "fmset G as \<le> fmset G bs" using ab proof (elim dividesE) fix c @@ -2270,7 +2270,7 @@ qed lemma (in comm_monoid_cancel) fmsubset_divides: - assumes msubset: "fmset G as \<le># fmset G bs" + assumes msubset: "fmset G as \<le> fmset G bs" and afs: "wfactors G as a" and bfs: "wfactors G bs b" and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G" @@ -2323,7 +2323,7 @@ assumes "wfactors G as a" and "wfactors G bs b" and "a \<in> carrier G" and "b \<in> carrier G" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" - shows "a divides b = (fmset G as \<le># fmset G bs)" + shows "a divides b = (fmset G as \<le> fmset G bs)" using assms by (blast intro: divides_fmsubset fmsubset_divides) @@ -2331,7 +2331,7 @@ text {* Proper factors on multisets *} lemma (in factorial_monoid) fmset_properfactor: - assumes asubb: "fmset G as \<le># fmset G bs" + assumes asubb: "fmset G as \<le> fmset G bs" and anb: "fmset G as \<noteq> fmset G bs" and "wfactors G as a" and "wfactors G bs b" and "a \<in> carrier G" and "b \<in> carrier G" @@ -2341,10 +2341,10 @@ apply (rule fmsubset_divides[of as bs], fact+) proof assume "b divides a" - hence "fmset G bs \<le># fmset G as" + hence "fmset G bs \<le> fmset G as" by (rule divides_fmsubset) fact+ with asubb - have "fmset G as = fmset G bs" by (simp add: mset_le_antisym) + have "fmset G as = fmset G bs" by (rule order_antisym) with anb show "False" .. qed @@ -2354,7 +2354,7 @@ and "wfactors G as a" and "wfactors G bs b" and "a \<in> carrier G" and "b \<in> carrier G" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G" - shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs" + shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs" using pf apply (elim properfactorE) apply rule @@ -2738,12 +2738,12 @@ have "c gcdof a b" proof (simp add: isgcd_def, safe) from csmset - have "fmset G cs \<le># fmset G as" + have "fmset G cs \<le> fmset G as" by (simp add: multiset_inter_def mset_le_def) thus "c divides a" by (rule fmsubset_divides) fact+ next from csmset - have "fmset G cs \<le># fmset G bs" + have "fmset G cs \<le> fmset G bs" by (simp add: multiset_inter_def mset_le_def, force) thus "c divides b" by (rule fmsubset_divides) fact+ next @@ -2756,13 +2756,13 @@ by auto assume "y divides a" - hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+ + hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+ assume "y divides b" - hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+ + hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+ from ya yb csmset - have "fmset G ys \<le># fmset G cs" by (simp add: mset_le_def multiset_inter_count) + have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count) thus "y divides c" by (rule fmsubset_divides) fact+ qed @@ -2837,10 +2837,10 @@ have "c lcmof a b" proof (simp add: islcm_def, safe) - from csmset have "fmset G as \<le># fmset G cs" by (simp add: mset_le_def, force) + from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force) thus "a divides c" by (rule fmsubset_divides) fact+ next - from csmset have "fmset G bs \<le># fmset G cs" by (simp add: mset_le_def) + from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def) thus "b divides c" by (rule fmsubset_divides) fact+ next fix y @@ -2852,13 +2852,13 @@ by auto assume "a divides y" - hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+ + hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+ assume "b divides y" - hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+ + hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+ from ya yb csmset - have "fmset G cs \<le># fmset G ys" + have "fmset G cs \<le> fmset G ys" apply (simp add: mset_le_def, clarify) apply (case_tac "count (fmset G as) a < count (fmset G bs) a") apply simp

--- a/src/HOL/Library/Permutation.thy Mon Feb 22 09:15:10 2010 +0100 +++ b/src/HOL/Library/Permutation.thy Mon Feb 22 09:15:10 2010 +0100 @@ -154,7 +154,7 @@ done lemma multiset_of_le_perm_append: - "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)" + "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)" apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv) apply (insert surj_multiset_of, drule surjD) apply (blast intro: sym)+