--- 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