src/HOL/Algebra/Divisibility.thy
 changeset 64587 8355a6e2df79 parent 63919 9aed2da07200 child 66453 cc19f7ca2ed6
```     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Sat Dec 17 15:22:00 2016 +0100
1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sat Dec 17 15:22:13 2016 +0100
1.3 @@ -1918,7 +1918,7 @@
1.4      and afs: "wfactors G as a"
1.5      and bfs: "wfactors G bs b"
1.6      and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
1.7 -  shows "fmset G as \<le># fmset G bs"
1.8 +  shows "fmset G as \<subseteq># fmset G bs"
1.9    using ab
1.10  proof (elim dividesE)
1.11    fix c
1.12 @@ -1935,7 +1935,7 @@
1.13  qed
1.14
1.15  lemma (in comm_monoid_cancel) fmsubset_divides:
1.16 -  assumes msubset: "fmset G as \<le># fmset G bs"
1.17 +  assumes msubset: "fmset G as \<subseteq># fmset G bs"
1.18      and afs: "wfactors G as a"
1.19      and bfs: "wfactors G bs b"
1.20      and acarr: "a \<in> carrier G"
1.21 @@ -1988,7 +1988,7 @@
1.22      and "b \<in> carrier G"
1.23      and "set as \<subseteq> carrier G"
1.24      and "set bs \<subseteq> carrier G"
1.25 -  shows "a divides b = (fmset G as \<le># fmset G bs)"
1.26 +  shows "a divides b = (fmset G as \<subseteq># fmset G bs)"
1.27    using assms
1.28    by (blast intro: divides_fmsubset fmsubset_divides)
1.29
1.30 @@ -1996,7 +1996,7 @@
1.31  text \<open>Proper factors on multisets\<close>
1.32
1.33  lemma (in factorial_monoid) fmset_properfactor:
1.34 -  assumes asubb: "fmset G as \<le># fmset G bs"
1.35 +  assumes asubb: "fmset G as \<subseteq># fmset G bs"
1.36      and anb: "fmset G as \<noteq> fmset G bs"
1.37      and "wfactors G as a"
1.38      and "wfactors G bs b"
1.39 @@ -2009,7 +2009,7 @@
1.40     apply (rule fmsubset_divides[of as bs], fact+)
1.41  proof
1.42    assume "b divides a"
1.43 -  then have "fmset G bs \<le># fmset G as"
1.44 +  then have "fmset G bs \<subseteq># fmset G as"
1.45      by (rule divides_fmsubset) fact+
1.46    with asubb have "fmset G as = fmset G bs"
1.47      by (rule subset_mset.antisym)
1.48 @@ -2024,7 +2024,7 @@
1.49      and "b \<in> carrier G"
1.50      and "set as \<subseteq> carrier G"
1.51      and "set bs \<subseteq> carrier G"
1.52 -  shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
1.53 +  shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
1.54    using pf
1.55    apply (elim properfactorE)
1.56    apply rule
1.57 @@ -2334,11 +2334,11 @@
1.58    have "c gcdof a b"
1.59    proof (simp add: isgcd_def, safe)
1.60      from csmset
1.61 -    have "fmset G cs \<le># fmset G as"
1.62 +    have "fmset G cs \<subseteq># fmset G as"
1.63        by (simp add: multiset_inter_def subset_mset_def)
1.64      then show "c divides a" by (rule fmsubset_divides) fact+
1.65    next
1.66 -    from csmset have "fmset G cs \<le># fmset G bs"
1.67 +    from csmset have "fmset G cs \<subseteq># fmset G bs"
1.68        by (simp add: multiset_inter_def subseteq_mset_def, force)
1.69      then show "c divides b"
1.70        by (rule fmsubset_divides) fact+
1.71 @@ -2350,14 +2350,14 @@
1.72        by blast
1.73
1.74      assume "y divides a"
1.75 -    then have ya: "fmset G ys \<le># fmset G as"
1.76 +    then have ya: "fmset G ys \<subseteq># fmset G as"
1.77        by (rule divides_fmsubset) fact+
1.78
1.79      assume "y divides b"
1.80 -    then have yb: "fmset G ys \<le># fmset G bs"
1.81 +    then have yb: "fmset G ys \<subseteq># fmset G bs"
1.82        by (rule divides_fmsubset) fact+
1.83
1.84 -    from ya yb csmset have "fmset G ys \<le># fmset G cs"
1.85 +    from ya yb csmset have "fmset G ys \<subseteq># fmset G cs"
1.86        by (simp add: subset_mset_def)
1.87      then show "y divides c"
1.88        by (rule fmsubset_divides) fact+
1.89 @@ -2420,12 +2420,12 @@
1.90
1.91    have "c lcmof a b"
1.92    proof (simp add: islcm_def, safe)
1.93 -    from csmset have "fmset G as \<le># fmset G cs"
1.94 +    from csmset have "fmset G as \<subseteq># fmset G cs"
1.95        by (simp add: subseteq_mset_def, force)
1.96      then show "a divides c"
1.97        by (rule fmsubset_divides) fact+
1.98    next
1.99 -    from csmset have "fmset G bs \<le># fmset G cs"
1.100 +    from csmset have "fmset G bs \<subseteq># fmset G cs"
1.101        by (simp add: subset_mset_def)
1.102      then show "b divides c"
1.103        by (rule fmsubset_divides) fact+
1.104 @@ -2437,14 +2437,14 @@
1.105        by blast
1.106
1.107      assume "a divides y"
1.108 -    then have ya: "fmset G as \<le># fmset G ys"
1.109 +    then have ya: "fmset G as \<subseteq># fmset G ys"
1.110        by (rule divides_fmsubset) fact+
1.111
1.112      assume "b divides y"
1.113 -    then have yb: "fmset G bs \<le># fmset G ys"
1.114 +    then have yb: "fmset G bs \<subseteq># fmset G ys"
1.115        by (rule divides_fmsubset) fact+
1.116
1.117 -    from ya yb csmset have "fmset G cs \<le># fmset G ys"
1.118 +    from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"
1.119        apply (simp add: subseteq_mset_def, clarify)
1.120        apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
1.121         apply simp
```