# HG changeset patch
# User paulson
# Date 1529535681 -3600
# Node ID b6e48841d0a5cb75a48896b33cdb4a92fea9de33
# Parent  1b8457cc4de8afec5fc2c209e0c9fb9c16864859# Parent  346bdafaf5fad9e9c1df5b35aadbbbf7fa9d19cd
merged

diff -r 1b8457cc4de8 -r b6e48841d0a5 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Jun 20 22:41:52 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Thu Jun 21 00:01:21 2018 +0100
@@ -1429,15 +1429,13 @@
     and ascarr: "set fa \<subseteq> carrier G"
     and bscarr: "set fb \<subseteq> carrier G"
   shows "factors G (fa @ fb) (a \<otimes> b)"
-  using assms
-  unfolding factors_def
-  apply safe
-   apply force
-  apply hypsubst_thin
-  apply (induct fa)
-   apply simp
-  apply (simp add: m_assoc)
-  done
+proof -
+  have "foldr (\<otimes>) (fa @ fb) \<one> = foldr (\<otimes>) fa \<one> \<otimes> foldr (\<otimes>) fb \<one>" if "set fa \<subseteq> carrier G" 
+    "Ball (set fa) (irreducible G)"
+    using that bscarr by (induct fa) (simp_all add: m_assoc)
+  then show ?thesis
+    using assms unfolding factors_def by force
+qed
 
 lemma (in comm_monoid_cancel) wfactors_mult [intro]:
   assumes asf: "wfactors G as a" and bsf:"wfactors G bs b"
@@ -1555,16 +1553,10 @@
 text \<open>Helper lemmas\<close>
 
 lemma (in monoid) assocs_repr_independence:
-  assumes "y \<in> assocs G x"
-    and "x \<in> carrier G"
+  assumes "y \<in> assocs G x" "x \<in> carrier G"
   shows "assocs G x = assocs G y"
   using assms
-  apply safe
-   apply (elim closure_ofE2, intro closure_ofI2[of _ _ y])
-     apply (clarsimp, iprover intro: associated_trans associated_sym, simp+)
-  apply (elim closure_ofE2, intro closure_ofI2[of _ _ x])
-    apply (clarsimp, iprover intro: associated_trans, simp+)
-  done
+  by (simp add: eq_closure_of_def elem_def) (use associated_sym associated_trans in \<open>blast+\<close>)
 
 lemma (in monoid) assocs_self:
   assumes "x \<in> carrier G"
@@ -1572,14 +1564,12 @@
   using assms by (fastforce intro: closure_ofI2)
 
 lemma (in monoid) assocs_repr_independenceD:
-  assumes repr: "assocs G x = assocs G y"
-    and ycarr: "y \<in> carrier G"
+  assumes repr: "assocs G x = assocs G y" and ycarr: "y \<in> carrier G"
   shows "y \<in> assocs G x"
   unfolding repr using ycarr by (intro assocs_self)
 
 lemma (in comm_monoid) assocs_assoc:
-  assumes "a \<in> assocs G b"
-    and "b \<in> carrier G"
+  assumes "a \<in> assocs G b" "b \<in> carrier G"
   shows "a \<sim> b"
   using assms by (elim closure_ofE2) simp
 
@@ -1594,30 +1584,23 @@
   using perm_map[OF prm] unfolding mset_eq_perm fmset_def by blast
 
 lemma (in comm_monoid_cancel) eqc_listassoc_cong:
-  assumes "as [\<sim>] bs"
-    and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
+  assumes "as [\<sim>] bs" and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
   shows "map (assocs G) as = map (assocs G) bs"
   using assms
-  apply (induct as arbitrary: bs, simp)
-  apply (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1, safe)
-   apply (clarsimp elim!: closure_ofE2) defer 1
-   apply (clarsimp elim!: closure_ofE2) defer 1
-proof -
-  fix a x z
-  assume carr[simp]: "a \<in> carrier G"  "x \<in> carrier G"  "z \<in> carrier G"
-  assume "x \<sim> a"
-  also assume "a \<sim> z"
-  finally have "x \<sim> z" by simp
-  with carr show "x \<in> assocs G z"
-    by (intro closure_ofI2) simp_all
+proof (induction as arbitrary: bs)
+  case Nil
+  then show ?case by simp
 next
-  fix a x z
-  assume carr[simp]: "a \<in> carrier G"  "x \<in> carrier G"  "z \<in> carrier G"
-  assume "x \<sim> z"
-  also assume [symmetric]: "a \<sim> z"
-  finally have "x \<sim> a" by simp
-  with carr show "x \<in> assocs G a"
-    by (intro closure_ofI2) simp_all
+  case (Cons a as)
+  then show ?case
+  proof (clarsimp simp add: Cons_eq_map_conv list_all2_Cons1)
+    fix z zs 
+    assume zzs: "a \<in> carrier G" "set as \<subseteq> carrier G" "bs = z # zs" "a \<sim> z"
+      "as [\<sim>] zs" "z \<in> carrier G" "set zs \<subseteq> carrier G"
+    then show "assocs G a = assocs G z"
+      apply (simp add: eq_closure_of_def elem_def)
+      using \<open>a \<in> carrier G\<close> \<open>z \<in> carrier G\<close> \<open>a \<sim> z\<close> associated_sym associated_trans by blast+
+  qed
 qed
 
 lemma (in comm_monoid_cancel) fmset_listassoc_cong:
@@ -1636,7 +1619,6 @@
   assume prm: "as <~~> as'"
   from prm ascarr have as'carr: "set as' \<subseteq> carrier G"
     by (rule perm_closed)
-
   from prm have "fmset G as = fmset G as'"
     by (rule fmset_perm_cong)
   also assume "as' [\<sim>] bs"
@@ -1645,99 +1627,31 @@
   finally show "fmset G as = fmset G bs" .
 qed
 
-lemma (in monoid_cancel) fmset_ee__hlp_induct:
-  assumes prm: "cas <~~> cbs"
-    and cdef: "cas = map (assocs G) as"  "cbs = map (assocs G) bs"
-  shows "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and>
-    cbs = map (assocs G) bs) \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
-  apply (rule perm.induct[of cas cbs], rule prm)
-     apply safe
-     apply (simp_all del: mset_map)
-    apply (simp add: map_eq_Cons_conv)
-    apply blast
-   apply force
-proof -
-  fix ys as bs
-  assume p1: "map (assocs G) as <~~> ys"
-    and r1[rule_format]:
-      "\<forall>asa bs. map (assocs G) as = map (assocs G) asa \<and> ys = map (assocs G) bs
-        \<longrightarrow> (\<exists>as'. asa <~~> as' \<and> map (assocs G) as' = map (assocs G) bs)"
-    and p2: "ys <~~> map (assocs G) bs"
-    and r2[rule_format]: "\<forall>as bsa. ys = map (assocs G) as \<and> map (assocs G) bs = map (assocs G) bsa
-      \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bsa)"
-    and p3: "map (assocs G) as <~~> map (assocs G) bs"
-
-  from p1 have "mset (map (assocs G) as) = mset ys"
-    by (simp add: mset_eq_perm del: mset_map)
-  then have setys: "set (map (assocs G) as) = set ys"
-    by (rule mset_eq_setD)
-
-  have "set (map (assocs G) as) = {assocs G x | x. x \<in> set as}" by auto
-  with setys have "set ys \<subseteq> { assocs G x | x. x \<in> set as}" by simp
-  then have "\<exists>yy. ys = map (assocs G) yy"
-  proof (induct ys)
-    case Nil
-    then show ?case by simp
-  next
-    case Cons
-    then show ?case
-    proof clarsimp
-      fix yy x
-      show "\<exists>yya. assocs G x # map (assocs G) yy = map (assocs G) yya"
-        by (rule exI[of _ "x#yy"]) simp
-    qed
-  qed
-  then obtain yy where ys: "ys = map (assocs G) yy" ..
-
-  from p1 ys have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) yy"
-    by (intro r1) simp
-  then obtain as' where asas': "as <~~> as'" and as'yy: "map (assocs G) as' = map (assocs G) yy"
-    by auto
-
-  from p2 ys have "\<exists>as'. yy <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
-    by (intro r2) simp
-  then obtain as'' where yyas'': "yy <~~> as''" and as''bs: "map (assocs G) as'' = map (assocs G) bs"
-    by auto
-
-  from perm_map_switch [OF as'yy yyas'']
-  obtain cs where as'cs: "as' <~~> cs" and csas'': "map (assocs G) cs = map (assocs G) as''"
-    by blast
-
-  from asas' and as'cs have ascs: "as <~~> cs"
-    by fast
-  from csas'' and as''bs have "map (assocs G) cs = map (assocs G) bs"
-    by simp
-  with ascs show "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
-    by fast
-qed
+lemma (in monoid_cancel) fmset_ee_aux:
+  assumes "cas <~~> cbs" "cas = map (assocs G) as" "cbs = map (assocs G) bs"
+  shows "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs"
+  using assms
+proof (induction cas cbs arbitrary: as bs rule: perm.induct)
+  case (Cons xs ys z)
+  then show ?case
+    by (clarsimp simp add: map_eq_Cons_conv) blast
+next
+  case (trans xs ys zs)
+  then show ?case
+    by (smt ex_map_conv perm.trans perm_setP)
+qed auto
 
 lemma (in comm_monoid_cancel) fmset_ee:
   assumes mset: "fmset G as = fmset G bs"
     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
   shows "essentially_equal G as bs"
 proof -
-  from mset have mpp: "map (assocs G) as <~~> map (assocs G) bs"
+  from mset have "map (assocs G) as <~~> map (assocs G) bs"
     by (simp add: fmset_def mset_eq_perm del: mset_map)
-
-  define cas where "cas = map (assocs G) as"
-  define cbs where "cbs = map (assocs G) bs"
-
-  from cas_def cbs_def mpp have [rule_format]:
-    "\<forall>as bs. (cas <~~> cbs \<and> cas = map (assocs G) as \<and> cbs = map (assocs G) bs)
-      \<longrightarrow> (\<exists>as'. as <~~> as' \<and> map (assocs G) as' = cbs)"
-    by (intro fmset_ee__hlp_induct, simp+)
-  with mpp cas_def cbs_def have "\<exists>as'. as <~~> as' \<and> map (assocs G) as' = map (assocs G) bs"
-    by simp
-
   then obtain as' where tp: "as <~~> as'" and tm: "map (assocs G) as' = map (assocs G) bs"
-    by auto
-  from tm have lene: "length as' = length bs"
-    by (rule map_eq_imp_length_eq)
-  from tp have "set as = set as'"
-    by (simp add: mset_eq_perm mset_eq_setD)
+    using fmset_ee_aux by blast
   with ascarr have as'carr: "set as' \<subseteq> carrier G"
-    by simp
-
+    using perm_closed by blast
   from tm as'carr[THEN subsetD] bscarr[THEN subsetD] have "as' [\<sim>] bs"
     by (induct as' arbitrary: bs) (simp, fastforce dest: assocs_eqD[THEN associated_sym])
   with tp show "essentially_equal G as bs"
@@ -1958,13 +1872,9 @@
     and "set bs \<subseteq> carrier G"
   shows "fmset G as \<subseteq># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
   using pf
-  apply (elim properfactorE)
-  apply rule
-   apply (intro divides_fmsubset, assumption)
-        apply (rule assms)+
-  using assms(2,3,4,6,7) divides_as_fmsubset
-  apply auto
-  done
+  apply safe
+   apply (meson assms divides_as_fmsubset monoid.properfactor_divides monoid_axioms)
+  by (meson assms associated_def comm_monoid_cancel.ee_wfactorsD comm_monoid_cancel.fmset_ee factorial_monoid_axioms factorial_monoid_def properfactorE)
 
 subsection \<open>Irreducible Elements are Prime\<close>
 
@@ -2377,11 +2287,7 @@
       by (rule divides_fmsubset) fact+
 
     from ya yb csmset have "fmset G cs \<subseteq># fmset G ys"
-      apply (simp add: subseteq_mset_def, clarify)
-      apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
-       apply simp
-      apply simp
-      done
+      using subset_eq_diff_conv subset_mset.le_diff_conv2 by fastforce
     then show "c divides y"
       by (rule fmsubset_divides) fact+
   qed
@@ -2399,8 +2305,7 @@
 proof -
   interpret weak_partial_order "division_rel G" ..
   show ?thesis
-    apply (unfold_locales, simp_all)
-  proof -
+  proof (unfold_locales, simp_all)
     fix x y
     assume carr: "x \<in> carrier G"  "y \<in> carrier G"
     from gcdof_exists [OF this] obtain z where zcarr: "z \<in> carrier G" and isgcd: "z gcdof x y"
@@ -2420,11 +2325,10 @@
 proof -
   note carr = a'carr carr'
   interpret weak_lower_semilattice "division_rel G" by simp
-  have "a' \<in> carrier G \<and> a' gcdof b c"
-    apply (simp add: gcdof_greatestLower carr')
-    apply (subst greatest_Lower_cong_l[of _ a])
-        apply (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
-    done
+  have "is_glb (division_rel G) a' {b, c}"
+    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
+  then have "a' \<in> carrier G \<and> a' gcdof b c"
+    by (simp add: gcdof_greatestLower carr')
   then show ?thesis ..
 qed
 
@@ -2446,10 +2350,7 @@
   interpret weak_lower_semilattice "division_rel G"
     by simp
   from carr have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
-    apply (subst gcdof_greatestLower, simp, simp)
-    apply (simp add: somegcd_meet[OF carr] meet_def)
-    apply (rule inf_of_two_greatest[simplified], assumption+)
-    done
+    by (simp add: gcdof_greatestLower inf_of_two_greatest meet_def somegcd_meet)
   then show "(somegcd G a b) gcdof a b"
     by simp
 qed
@@ -2541,21 +2442,23 @@
 
 lemma (in gcd_condition_monoid) gcdI:
   assumes dvd: "a divides b"  "a divides c"
-    and others: "\<forall>y\<in>carrier G. y divides b \<and> y divides c \<longrightarrow> y divides a"
+    and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"
     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G" and ccarr: "c \<in> carrier G"
   shows "a \<sim> somegcd G b c"
-  apply (simp add: somegcd_def)
-  apply (rule someI2_ex)
-   apply (rule exI[of _ a], simp add: isgcd_def)
-   apply (simp add: assms)
-  apply (simp add: isgcd_def assms, clarify)
-  apply (insert assms, blast intro: associatedI)
-  done
+proof -
+  have "\<exists>a. a \<in> carrier G \<and> a gcdof b c"
+    by (simp add: bcarr ccarr gcdof_exists)
+  moreover have "\<And>x. x \<in> carrier G \<and> x gcdof b c \<Longrightarrow> a \<sim> x"
+    by (simp add: acarr associated_def dvd isgcd_def others)
+  ultimately show ?thesis
+    unfolding somegcd_def by (blast intro: someI2_ex)
+qed
 
 lemma (in gcd_condition_monoid) gcdI2:
   assumes "a gcdof b c" and "a \<in> carrier G" and "b \<in> carrier G" and "c \<in> carrier G"
   shows "a \<sim> somegcd G b c"
-  using assms unfolding isgcd_def by (blast intro: gcdI)
+  using assms unfolding isgcd_def
+  by (simp add: gcdI)
 
 lemma (in gcd_condition_monoid) SomeGcd_ex:
   assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
@@ -3193,10 +3096,7 @@
     with nbdvda show False by simp
   qed
   with cfs have "length cs > 0"
-    apply -
-    apply (rule ccontr, simp)
-    apply (metis Units_one_closed ccarr cscarr l_one one_closed properfactorI3 properfactor_fmset unit_wfactors)
-    done
+    by (metis Units_one_closed assoc_unit_r ccarr foldr.simps(1) id_apply length_greater_0_conv wfactors_def)
   with fca fcb show ?thesis
     by simp
 qed