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