author paulson Wed, 25 Jul 2018 00:25:05 +0200 changeset 68684 9a42b84f8838 parent 68683 d69127c6e80f child 68685 4b367da119ed
de-applying
 src/HOL/Algebra/AbelCoset.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Complete_Lattice.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/Divisibility.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Algebra/AbelCoset.thy	Sun Jul 22 21:04:49 2018 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Wed Jul 25 00:25:05 2018 +0200
@@ -269,17 +269,15 @@
by (rule a_comm_group)
by (rule a_subgroup)
-
-  show "abelian_subgroup H G"
-    apply unfold_locales
-  proof (simp add: r_coset_def l_coset_def, clarsimp)
-    fix x
-    assume xcarr: "x \<in> carrier G"
-    from a_subgroup have Hcarr: "H \<subseteq> carrier G"
-      unfolding subgroup_def by simp
-    from xcarr Hcarr show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
+  have "(\<Union>xa\<in>H. {xa \<oplus> x}) = (\<Union>xa\<in>H. {x \<oplus> xa})" if "x \<in> carrier G" for x
+  proof -
+    have "H \<subseteq> carrier G"
+      using a_subgroup that unfolding subgroup_def by simp
+    with that show "(\<Union>h\<in>H. {h \<oplus>\<^bsub>G\<^esub> x}) = (\<Union>h\<in>H. {x \<oplus>\<^bsub>G\<^esub> h})"
using m_comm [simplified] by fastforce
qed
+  then show "abelian_subgroup H G"
+    by unfold_locales (auto simp: r_coset_def l_coset_def)
qed

lemma abelian_subgroupI3:
@@ -304,14 +302,6 @@
by (rule normal.inv_op_closed2 [OF a_normal,
folded a_inv_def, simplified monoid_record_simps])

-text\<open>Alternative characterization of normal subgroups\<close>
-lemma (in abelian_group) a_normal_inv_iff:
-     "(N \<lhd> (add_monoid G)) =
-      (subgroup N (add_monoid G) & (\<forall>x \<in> carrier G. \<forall>h \<in> N. x \<oplus> h \<oplus> (\<ominus> x) \<in> N))"
-      (is "_ = ?rhs")
-by (rule group.normal_inv_iff [OF a_group,
-    folded a_inv_def, simplified monoid_record_simps])
-
lemma (in abelian_group) a_lcos_m_assoc:
"\<lbrakk> M \<subseteq> carrier G; g \<in> carrier G; h \<in> carrier G \<rbrakk> \<Longrightarrow> g <+ (h <+ M) = (g \<oplus> h) <+ M"
by (rule group.lcos_m_assoc [OF a_group,
@@ -322,13 +312,11 @@
by (rule group.lcos_mult_one [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])

-
lemma (in abelian_group) a_l_coset_subset_G:
"\<lbrakk> H \<subseteq> carrier G; x \<in> carrier G \<rbrakk> \<Longrightarrow> x <+ H \<subseteq> carrier G"
by (rule group.l_coset_subset_G [OF a_group,
folded a_l_coset_def, simplified monoid_record_simps])

-
lemma (in abelian_group) a_l_coset_swap:
"\<lbrakk>y \<in> x <+ H;  x \<in> carrier G;  subgroup H (add_monoid G)\<rbrakk> \<Longrightarrow> x \<in> y <+ H"
by (rule group.l_coset_swap [OF a_group,
@@ -498,15 +486,15 @@

text \<open>Since the Factorization is based on an \emph{abelian} subgroup, is results in
a commutative group\<close>
-theorem (in abelian_subgroup) a_factorgroup_is_comm_group:
-  "comm_group (G A_Mod H)"
-apply (intro comm_group.intro comm_monoid.intro) prefer 3
-  apply (rule a_factorgroup_is_group)
- apply (rule group.axioms[OF a_factorgroup_is_group])
-apply (rule comm_monoid_axioms.intro)
-apply (unfold A_FactGroup_def FactGroup_def RCOSETS_def, fold set_add_def a_r_coset_def, clarsimp)
-done
+theorem (in abelian_subgroup) a_factorgroup_is_comm_group: "comm_group (G A_Mod H)"
+proof -
+  have "Group.comm_monoid_axioms (G A_Mod H)"
+    apply (rule comm_monoid_axioms.intro)
+    apply (auto simp: A_FactGroup_def FactGroup_def RCOSETS_def a_normal add.m_comm normal.rcos_sum)
+    done
+  then show ?thesis
+    by (intro comm_group.intro comm_monoid.intro) (simp_all add: a_factorgroup_is_group group.is_monoid)
+qed

lemma add_A_FactGroup [simp]: "X \<otimes>\<^bsub>(G A_Mod H)\<^esub> X' = X <+>\<^bsub>G\<^esub> X'"
@@ -552,11 +540,8 @@
interpret G: abelian_group G by fact
interpret H: abelian_group H by fact
show ?thesis
-    apply (intro abelian_group_hom.intro abelian_group_hom_axioms.intro)
-      apply fact
-     apply fact
-    apply (rule a_group_hom)
-    done
+    by (intro abelian_group_hom.intro abelian_group_hom_axioms.intro
+        G.abelian_group_axioms H.abelian_group_axioms a_group_hom)
qed

lemma (in abelian_group_hom) is_abelian_group_hom:
@@ -576,8 +561,7 @@

lemma (in abelian_group_hom) zero_closed [simp]:
"h \<zero> \<in> carrier H"
-by (rule group_hom.one_closed[OF a_group_hom,
-    simplified ring_record_simps])
+  by simp

lemma (in abelian_group_hom) hom_zero [simp]:
"h \<zero> = \<zero>\<^bsub>H\<^esub>"
@@ -586,8 +570,7 @@

lemma (in abelian_group_hom) a_inv_closed [simp]:
"x \<in> carrier G ==> h (\<ominus>x) \<in> carrier H"
-by (rule group_hom.inv_closed[OF a_group_hom,
-    folded a_inv_def, simplified ring_record_simps])
+  by simp

lemma (in abelian_group_hom) hom_a_inv [simp]:
"x \<in> carrier G ==> h (\<ominus>x) = \<ominus>\<^bsub>H\<^esub> (h x)"
@@ -596,19 +579,15 @@

"additive_subgroup (a_kernel G H h) G"
-apply (rule group_hom.subgroup_kernel[OF a_group_hom,
-       folded a_kernel_def, simplified ring_record_simps])
-done

text\<open>The kernel of a homomorphism is an abelian subgroup\<close>
lemma (in abelian_group_hom) abelian_subgroup_a_kernel:
"abelian_subgroup (a_kernel G H h) G"
-apply (rule abelian_subgroupI)
-apply (rule group_hom.normal_kernel[OF a_group_hom,
-       folded a_kernel_def, simplified ring_record_simps])
-done
+  apply (rule abelian_subgroupI)
+  done

lemma (in abelian_group_hom) A_FactGroup_nonempty:
assumes X: "X \<in> carrier (G A_Mod a_kernel G H h)"
@@ -715,48 +694,34 @@
qed

lemma (in abelian_subgroup) a_repr_independence':
-  assumes y: "y \<in> H +> x"
-      and xcarr: "x \<in> carrier G"
+  assumes "y \<in> H +> x" "x \<in> carrier G"
shows "H +> x = H +> y"
-  apply (rule a_repr_independence)
-    apply (rule y)
-   apply (rule xcarr)
-  apply (rule a_subgroup)
-  done
+  using a_repr_independence a_subgroup assms by blast

lemma (in abelian_subgroup) a_repr_independenceD:
-  assumes ycarr: "y \<in> carrier G"
-      and repr:  "H +> x = H +> y"
+  assumes "y \<in> carrier G" "H +> x = H +> y"
shows "y \<in> H +> x"
-by (rule group.repr_independenceD [OF a_group a_subgroup,
-    folded a_r_coset_def, simplified monoid_record_simps]) (rule ycarr, rule repr)
+  by (simp add: a_rcos_self assms)

lemma (in abelian_subgroup) a_rcosets_carrier:
"X \<in> a_rcosets H \<Longrightarrow> X \<subseteq> carrier G"
-by (rule subgroup.rcosets_carrier [OF a_subgroup a_group,
-    folded A_RCOSETS_def, simplified monoid_record_simps])
+  using a_rcosets_part_G by auto

-  assumes Acarr: "A \<subseteq> carrier G"
-      and Bcarr: "B \<subseteq> carrier G"
+  assumes "A \<subseteq> carrier G" "B \<subseteq> carrier G"
shows "A <+> B \<subseteq> carrier G"
-by (rule monoid.set_mult_closed [OF a_monoid,
-    folded set_add_def, simplified monoid_record_simps]) (rule Acarr, rule Bcarr)

-      and subK: "additive_subgroup K G"
+    and subK: "additive_subgroup K G"
shows "additive_subgroup (H <+> K) G"
-apply (intro comm_group.mult_subgroups)
-  apply (rule a_comm_group)
-done

end
--- a/src/HOL/Algebra/Complete_Lattice.thy	Sun Jul 22 21:04:49 2018 +0200
+++ b/src/HOL/Algebra/Complete_Lattice.thy	Wed Jul 25 00:25:05 2018 +0200
@@ -680,22 +680,25 @@
next
case False
show ?thesis
-      proof (rule_tac x="\<Squnion>\<^bsub>L\<^esub> A" in exI, rule least_UpperI, simp_all)
+      proof (intro exI least_UpperI, simp_all)
show b:"\<And> x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
using a by (auto intro: L.sup_upper, meson L.at_least_at_most_closed L.sup_upper subset_trans)
show "\<And>y. y \<in> Upper (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> y"
using a L.at_least_at_most_closed by (rule_tac L.sup_least, auto intro: funcset_mem simp add: Upper_def)
-        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          by (auto)
-        from a show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          apply (rule_tac L.at_least_at_most_member)
-          apply (auto)
-          apply (meson L.at_least_at_most_closed L.sup_closed subset_trans)
-          apply (meson False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_closed b all_not_in_conv assms(2) contra_subsetD subset_trans)
-          apply (rule L.sup_least)
-          apply (auto simp add: assms)
-          using L.at_least_at_most_closed apply blast
-        done
+        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          by auto
+        show "\<Squnion>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+        proof (rule_tac L.at_least_at_most_member)
+          show 1: "\<Squnion>\<^bsub>L\<^esub>A \<in> carrier L"
+            by (meson L.at_least_at_most_closed L.sup_closed subset_trans *)
+          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Squnion>\<^bsub>L\<^esub>A"
+            by (meson "*" False L.at_least_at_most_closed L.at_least_at_most_lower L.le_trans L.sup_upper 1 all_not_in_conv assms(2) set_mp subset_trans)
+          show "\<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
+          proof (rule L.sup_least)
+            show "A \<subseteq> carrier L" "\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> b"
+              using * L.at_least_at_most_closed by blast+
+        qed
qed
qed
show "\<exists>s. is_glb (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) s A"
@@ -711,15 +714,17 @@
using a L.at_least_at_most_closed by (force intro!: L.inf_lower)
show "\<And>y. y \<in> Lower (L\<lparr>carrier := \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>\<rparr>) A \<Longrightarrow> y \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
using a L.at_least_at_most_closed by (rule_tac L.inf_greatest, auto intro: funcset_carrier' simp add: Lower_def)
-        from a show "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          by (auto)
-        from a show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
-          apply (rule_tac L.at_least_at_most_member)
-          apply (auto)
-          apply (meson L.at_least_at_most_closed L.inf_closed subset_trans)
-          apply (meson L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) set_rev_mp subset_trans)
-          apply (meson False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_closed L.le_trans b all_not_in_conv assms(3) contra_subsetD subset_trans)
-        done
+        from a show *: "A \<subseteq> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+          by auto
+        show "\<Sqinter>\<^bsub>L\<^esub>A \<in> \<lbrace>a..b\<rbrace>\<^bsub>L\<^esub>"
+        proof (rule_tac L.at_least_at_most_member)
+          show 1: "\<Sqinter>\<^bsub>L\<^esub>A \<in> carrier L"
+            by (meson "*" L.at_least_at_most_closed L.inf_closed subset_trans)
+          show "a \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
+            by (meson "*" L.at_least_at_most_closed L.at_least_at_most_lower L.inf_greatest assms(2) subsetD subset_trans)
+          show "\<Sqinter>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> b"
+            by (meson * 1 False L.at_least_at_most_closed L.at_least_at_most_upper L.inf_lower L.le_trans all_not_in_conv assms(3) set_mp subset_trans)
+        qed
qed
qed
qed
@@ -731,7 +736,7 @@
text \<open>The set of fixed points of a complete lattice is itself a complete lattice\<close>

theorem Knaster_Tarski:
-  assumes "weak_complete_lattice L" "f \<in> carrier L \<rightarrow> carrier L" "isotone L L f"
+  assumes "weak_complete_lattice L" and f: "f \<in> carrier L \<rightarrow> carrier L" and "isotone L L f"
shows "weak_complete_lattice (fpl L f)" (is "weak_complete_lattice ?L'")
proof -
interpret L: weak_complete_lattice L
@@ -805,15 +810,14 @@
show "is_lub ?L'' (LFP\<^bsub>?L'\<^esub> f) A"
proof (rule least_UpperI, simp_all)
fix x
-        assume "x \<in> Upper ?L'' A"
-        hence "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
-          apply (rule_tac L'.LFP_lowerbound)
-          apply (auto simp add: Upper_def)
-          apply (simp add: A AL L.at_least_at_most_member L.sup_least set_rev_mp)
-          apply (simp add: Pi_iff assms(2) fps_def, rule_tac L.weak_refl)
-          apply (auto)
-          apply (rule funcset_mem[of f "carrier L"], simp_all add: assms(2))
-        done
+        assume x: "x \<in> Upper ?L'' A"
+        have "LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>?L'\<^esub> x"
+        proof (rule L'.LFP_lowerbound, simp_all)
+          show "x \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
+            using x by (auto simp add: Upper_def A AL L.at_least_at_most_member L.sup_least set_rev_mp)
+          with x show "f x \<sqsubseteq>\<^bsub>L\<^esub> x"
+            by (simp add: Upper_def) (meson L.at_least_at_most_closed L.use_fps L.weak_refl subsetD f_top_chain imageI)
+        qed
thus " LFP\<^bsub>?L'\<^esub> f \<sqsubseteq>\<^bsub>L\<^esub> x"
by (simp)
next
@@ -838,17 +842,13 @@
have "LFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (LFP\<^bsub>?L'\<^esub> f)"
proof (rule "L'.LFP_weak_unfold", simp_all)
-            show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
-              apply (auto simp add: Pi_def at_least_at_most_def)
-              using assms(2) apply blast
-              apply (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
-              using assms(2) apply blast
-            done
-            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
-              apply (auto simp add: isotone_def)
-              using L'.weak_partial_order_axioms apply blast
-              apply (meson L.at_least_at_most_closed subsetCE)
-            done
+            have "\<And>x. \<lbrakk>x \<in> carrier L; \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> x\<rbrakk> \<Longrightarrow> \<Squnion>\<^bsub>L\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f x"
+              by (meson AL funcset_mem L.le_trans L.sup_closed assms(2) assms(3) pf_w use_iso2)
+            with f show "f \<in> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>"
+              by (auto simp add: Pi_def at_least_at_most_def)
+            show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<Squnion>\<^bsub>L\<^esub>A..\<top>\<^bsub>L\<^esub>\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
+              using L'.weak_partial_order_axioms assms(3)
+              by (auto simp add: isotone_def) (meson L.at_least_at_most_closed subsetCE)
qed
thus "f (LFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> LFP\<^bsub>?L'\<^esub> f"
by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)
@@ -889,7 +889,6 @@
thus ?thesis
by (meson AL L.inf_closed L.le_trans assms(3) b(1) b(2) fx use_iso2 w)
qed
-
show "\<bottom>\<^bsub>L\<^esub> \<sqsubseteq>\<^bsub>L\<^esub> f x"
qed
@@ -905,12 +904,16 @@
proof (rule greatest_LowerI, simp_all)
fix x
assume "x \<in> Lower ?L'' A"
-        hence "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
-          apply (rule_tac L'.GFP_upperbound)
-          apply (auto simp add: Lower_def)
-          apply (meson A AL L.at_least_at_most_member L.bottom_lower L.weak_complete_lattice_axioms fps_carrier subsetCE weak_complete_lattice.inf_greatest)
-          apply (simp add: funcset_carrier' L.sym assms(2) fps_def)
-        done
+        then have x: "\<forall>y. y \<in> A \<and> y \<in> fps L f \<longrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y" "x \<in> fps L f"
+          by (auto simp add: Lower_def)
+        have "x \<sqsubseteq>\<^bsub>?L'\<^esub> GFP\<^bsub>?L'\<^esub> f"
+          unfolding Lower_def
+        proof (rule_tac L'.GFP_upperbound; simp)
+          show "x \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>"
+            by (meson x A AL L.at_least_at_most_member L.bottom_lower L.inf_greatest contra_subsetD fps_carrier)
+          show "x \<sqsubseteq>\<^bsub>L\<^esub> f x"
+            using x by (simp add: funcset_carrier' L.sym assms(2) fps_def)
+        qed
thus "x \<sqsubseteq>\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
by (simp)
next
@@ -935,17 +938,14 @@
have "GFP\<^bsub>?L'\<^esub> f .=\<^bsub>?L'\<^esub> f (GFP\<^bsub>?L'\<^esub> f)"
proof (rule "L'.GFP_weak_unfold", simp_all)
-            show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
-              apply (auto simp add: Pi_def at_least_at_most_def)
-              using assms(2) apply blast
-              apply (simp add: funcset_carrier' assms(2))
-              apply (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
-            done
-            from assms(3) show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
-              apply (auto simp add: isotone_def)
-              using L'.weak_partial_order_axioms apply blast
-              using L.at_least_at_most_closed apply (blast intro: funcset_carrier')
-            done
+            have "\<And>x. \<lbrakk>x \<in> carrier L; x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A\<rbrakk> \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L\<^esub> \<Sqinter>\<^bsub>L\<^esub>A"
+              by (meson AL funcset_carrier L.inf_closed L.le_trans assms(2) assms(3) pf_w use_iso2)
+            with assms(2) show "f \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub> \<rightarrow> \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>"
+              by (auto simp add: Pi_def at_least_at_most_def)
+            have "\<And>x y. \<lbrakk>x \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>; y \<in> \<lbrace>\<bottom>\<^bsub>L\<^esub>..\<Sqinter>\<^bsub>L\<^esub>A\<rbrace>\<^bsub>L\<^esub>; x \<sqsubseteq>\<^bsub>L\<^esub> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq>\<^bsub>L\<^esub> f y"
+              by (meson L.at_least_at_most_closed subsetD use_iso1  assms(3))
+            with L'.weak_partial_order_axioms show "Mono\<^bsub>L\<lparr>carrier := \<lbrace>\<bottom>\<^bsub>L\<^esub>..?w\<rbrace>\<^bsub>L\<^esub>\<rparr>\<^esub> f"
+              by (auto simp add: isotone_def)
qed
thus "f (GFP\<^bsub>?L'\<^esub> f) .=\<^bsub>L\<^esub> GFP\<^bsub>?L'\<^esub> f"
by (simp add: L.equivalence_axioms funcset_carrier' c assms(2) equivalence.sym)
@@ -1117,17 +1117,16 @@
qed
show "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>L\<^esub>A)"
proof -
+      have *: "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<in> carrier L"
+        using FA infA by blast
have "\<And>x. x \<in> A \<Longrightarrow> \<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>fpl L f\<^esub> x"
by (rule L'.inf_lower, simp_all add: assms)
hence "\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> (\<Sqinter>\<^bsub>L\<^esub>A)"
-        apply (rule_tac L.inf_greatest, simp_all add: A)
-        using FA infA apply blast
-        done
+        by (rule_tac L.inf_greatest, simp_all add: A *)
hence 1:"f(\<Sqinter>\<^bsub>fpl L f\<^esub>A) \<sqsubseteq>\<^bsub>L\<^esub> f(\<Sqinter>\<^bsub>L\<^esub>A)"
by (metis (no_types, lifting) A FA L.inf_closed assms(2) infA subsetCE use_iso1)
have 2:"\<Sqinter>\<^bsub>fpl L f\<^esub>A \<sqsubseteq>\<^bsub>L\<^esub> f (\<Sqinter>\<^bsub>fpl L f\<^esub>A)"
by (metis (no_types, lifting) FA L.sym L.use_fps L.weak_complete_lattice_axioms PiE assms(4) infA subsetCE weak_complete_lattice_def weak_partial_order.weak_refl)
-
show ?thesis
using FA fA infA by (auto intro!: L.le_trans[OF 2 1] ic fc, metis FA PiE assms(4) subsetCE)
qed
@@ -1189,21 +1188,11 @@
lemma sup_pres_is_join_pres:
assumes "weak_sup_pres X Y f"
shows "join_pres X Y f"
-  using assms
-  apply (simp add: join_pres_def weak_sup_pres_def, safe)
-  apply (rename_tac x y)
-  apply (drule_tac x="{x, y}" in spec)
-  apply (auto simp add: join_def)
-done
+  using assms by (auto simp: join_pres_def weak_sup_pres_def join_def)

lemma inf_pres_is_meet_pres:
assumes "weak_inf_pres X Y f"
shows "meet_pres X Y f"
-  using assms
-  apply (simp add: meet_pres_def weak_inf_pres_def, safe)
-  apply (rename_tac x y)
-  apply (drule_tac x="{x, y}" in spec)
-  apply (auto simp add: meet_def)
-done
+  using assms by (auto simp: meet_pres_def weak_inf_pres_def meet_def)

end
--- a/src/HOL/Algebra/Divisibility.thy	Sun Jul 22 21:04:49 2018 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jul 25 00:25:05 2018 +0200
@@ -547,22 +547,14 @@
using pf by (elim properfactorE)

lemma (in monoid) properfactor_trans1 [trans]:
-  assumes dvds: "a divides b"  "properfactor G b c"
-    and carr: "a \<in> carrier G"  "c \<in> carrier G"
+  assumes "a divides b"  "properfactor G b c" "a \<in> carrier G"  "c \<in> carrier G"
shows "properfactor G a c"
-  using dvds carr
-  apply (elim properfactorE, intro properfactorI)
-   apply (iprover intro: divides_trans)+
-  done
+  by (meson divides_trans properfactorE properfactorI assms)

lemma (in monoid) properfactor_trans2 [trans]:
-  assumes dvds: "properfactor G a b"  "b divides c"
-    and carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "properfactor G a b"  "b divides c" "a \<in> carrier G"  "b \<in> carrier G"
shows "properfactor G a c"
-  using dvds carr
-  apply (elim properfactorE, intro properfactorI)
-   apply (iprover intro: divides_trans)+
-  done
+  by (meson divides_trans properfactorE properfactorI assms)

lemma properfactor_lless:
fixes G (structure)
@@ -660,23 +652,20 @@
using assms by (fast elim: irreducibleE)

lemma (in monoid_cancel) irreducible_cong [trans]:
-  assumes irred: "irreducible G a"
-    and aa': "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
+  assumes "irreducible G a" "a \<sim> a'" "a \<in> carrier G"  "a' \<in> carrier G"
shows "irreducible G a'"
-  using assms
-  apply (auto simp: irreducible_def assoc_unit_l)
-  apply (metis aa' associated_sym properfactor_cong_r)
-  done
+proof -
+  have "a' divides a"
+    by (meson \<open>a \<sim> a'\<close> associated_def)
+  then show ?thesis
+    by (metis (no_types) assms assoc_unit_l irreducibleE irreducibleI monoid.properfactor_trans2 monoid_axioms)
+qed

lemma (in monoid) irreducible_prod_rI:
-  assumes airr: "irreducible G a"
-    and bunit: "b \<in> Units G"
-    and carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "irreducible G a" "b \<in> Units G" "a \<in> carrier G"  "b \<in> carrier G"
shows "irreducible G (a \<otimes> b)"
-  using airr carr bunit
-  apply (elim irreducibleE, intro irreducibleI)
-  using prod_unit_r apply blast
-  using associatedI2' properfactor_cong_r by auto
+  using assms
+  by (metis (no_types, lifting) associatedI2' irreducible_def monoid.m_closed monoid_axioms prod_unit_r properfactor_cong_r)

lemma (in comm_monoid) irreducible_prod_lI:
assumes birr: "irreducible G b"
@@ -764,9 +753,7 @@
and pp': "p \<sim> p'" "p \<in> carrier G"  "p' \<in> carrier G"
shows "prime G p'"
using assms
-  apply (auto simp: prime_def assoc_unit_l)
-  apply (metis pp' associated_sym divides_cong_l)
-  done
+  by (auto simp: prime_def assoc_unit_l) (metis pp' associated_sym divides_cong_l)

(*by Paulo Emílio de Vilhena*)
lemma (in comm_monoid_cancel) prime_irreducible:
@@ -849,9 +836,7 @@
and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
shows "\<forall>a\<in>set bs. irreducible G a"
using assms
-  apply (clarsimp simp add: list_all2_conv_all_nth set_conv_nth)
-  apply (blast intro: irreducible_cong)
-  done
+  by (fastforce simp add: list_all2_conv_all_nth set_conv_nth intro: irreducible_cong)

text \<open>Permutations\<close>
@@ -1001,15 +986,7 @@
then have f: "f \<in> carrier G"
by blast
show ?case
-  proof (cases "f = a")
-    case True
-    then show ?thesis
-      using Cons.prems by auto
-  next
-    case False
-    with Cons show ?thesis
-      by clarsimp (metis f divides_prod_l multlist_closed)
-  qed
+    using Cons.IH Cons.prems(1) Cons.prems(2) divides_prod_l f by auto
qed auto

lemma (in comm_monoid_cancel) multlist_listassoc_cong:
@@ -1051,9 +1028,7 @@
and "set fs \<subseteq> carrier G" and "set fs' \<subseteq> carrier G"
shows "foldr (\<otimes>) fs \<one> \<sim> foldr (\<otimes>) fs' \<one>"
using assms
-  apply (elim essentially_equalE)
-  apply (simp add: multlist_perm_cong multlist_listassoc_cong perm_closed)
-  done
+  by (metis essentially_equal_def multlist_listassoc_cong multlist_perm_cong perm_closed)

subsubsection \<open>Factorization in irreducible elements\<close>
@@ -1120,9 +1095,6 @@
and carr[simp]: "set fs \<subseteq> carrier G"
shows "fs = []"
proof (cases fs)
-  case Nil
-  then show ?thesis .
-next
case fs: (Cons f fs')
from carr have fcarr[simp]: "f \<in> carrier G" and carr'[simp]: "set fs' \<subseteq> carrier G"
@@ -1874,6 +1846,18 @@
qed

lemma (in factorial_monoid) properfactor_fmset:
+  assumes "properfactor G a b"
+    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 \<subseteq># fmset G bs"
+  using assms
+  by (meson divides_as_fmsubset properfactor_divides)
+
+lemma (in factorial_monoid) properfactor_fmset_ne:
assumes pf: "properfactor G a b"
and "wfactors G as a"
and "wfactors G bs b"
@@ -1881,11 +1865,8 @@
and "b \<in> carrier G"
and "set as \<subseteq> carrier G"
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 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)
+  shows "fmset G as \<noteq> fmset G bs"
+  using properfactorE [OF pf] assms divides_as_fmsubset by force

subsection \<open>Irreducible Elements are Prime\<close>

@@ -2246,75 +2227,70 @@
qed

lemma (in gcd_condition_monoid) gcdof_cong_l:
-  assumes a'a: "a' \<sim> a"
-    and agcd: "a gcdof b c"
-    and a'carr: "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  assumes "a' \<sim> a" "a gcdof b c" "a' \<in> carrier G" and carr': "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
shows "a' gcdof b c"
proof -
-  note carr = a'carr carr'
interpret weak_lower_semilattice "division_rel G" by simp
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)
+    by (subst greatest_Lower_cong_l[of _ a]) (simp_all add: assms gcdof_greatestLower[symmetric])
then have "a' \<in> carrier G \<and> a' gcdof b c"
then show ?thesis ..
qed

lemma (in gcd_condition_monoid) gcd_closed [simp]:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G" "b \<in> carrier G"
shows "somegcd G a b \<in> carrier G"
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
-    apply (simp add: somegcd_meet[OF carr])
-    apply (rule meet_closed[simplified], fact+)
-    done
+  using  assms meet_closed by (simp add: somegcd_meet)
qed

lemma (in gcd_condition_monoid) gcd_isgcd:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"
shows "(somegcd G a b) gcdof a b"
proof -
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"
+  from assms have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
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

lemma (in gcd_condition_monoid) gcd_exists:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"
shows "\<exists>x\<in>carrier G. x = somegcd G a b"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
-    by (metis carr(1) carr(2) gcd_closed)
+    by (metis assms gcd_closed)
qed

lemma (in gcd_condition_monoid) gcd_divides_l:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G" "b \<in> carrier G"
shows "(somegcd G a b) divides a"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
-    by (metis carr(1) carr(2) gcd_isgcd isgcd_def)
+    by (metis assms gcd_isgcd isgcd_def)
qed

lemma (in gcd_condition_monoid) gcd_divides_r:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"
shows "(somegcd G a b) divides b"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
-    by (metis carr gcd_isgcd isgcd_def)
+    by (metis assms gcd_isgcd isgcd_def)
qed

lemma (in gcd_condition_monoid) gcd_divides:
-  assumes sub: "z divides x"  "z divides y"
+  assumes "z divides x" "z divides y"
and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
shows "z divides (somegcd G x y)"
proof -
@@ -2325,49 +2301,25 @@
qed

lemma (in gcd_condition_monoid) gcd_cong_l:
-  assumes xx': "x \<sim> x'"
-    and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
+  assumes "x \<sim> x'" "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
shows "somegcd G x y \<sim> somegcd G x' y"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
-    apply (simp add: somegcd_meet carr)
-    apply (rule meet_cong_l[simplified], fact+)
-    done
+    using somegcd_meet assms
+    by (metis eq_object.select_convs(1) meet_cong_l partial_object.select_convs(1))
qed

lemma (in gcd_condition_monoid) gcd_cong_r:
-  assumes carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
-    and yy': "y \<sim> y'"
+  assumes "y \<sim> y'" "x \<in> carrier G"  "y \<in> carrier G" "y' \<in> carrier G"
shows "somegcd G x y \<sim> somegcd G x y'"
proof -
interpret weak_lower_semilattice "division_rel G" by simp
show ?thesis
-    apply (simp add: somegcd_meet carr)
-    apply (rule meet_cong_r[simplified], fact+)
-    done
+    by (meson associated_def assms gcd_closed gcd_divides gcd_divides_l gcd_divides_r monoid.divides_trans monoid_axioms)
qed

-(*
-lemma (in gcd_condition_monoid) asc_cong_gcd_l [intro]:
-  assumes carr: "b \<in> carrier G"
-  shows "asc_cong (\<lambda>a. somegcd G a b)"
-using carr
-unfolding CONG_def
-by clarsimp (blast intro: gcd_cong_l)
-
-lemma (in gcd_condition_monoid) asc_cong_gcd_r [intro]:
-  assumes carr: "a \<in> carrier G"
-  shows "asc_cong (\<lambda>b. somegcd G a b)"
-using carr
-unfolding CONG_def
-by clarsimp (blast intro: gcd_cong_r)
-
-lemmas (in gcd_condition_monoid) asc_cong_gcd_split [simp] =
-    assoc_split[OF _ asc_cong_gcd_l] assoc_split[OF _ asc_cong_gcd_r]
-*)
-
lemma (in gcd_condition_monoid) gcdI:
assumes dvd: "a divides b"  "a divides c"
and others: "\<And>y. \<lbrakk>y\<in>carrier G; y divides b; y divides c\<rbrakk> \<Longrightarrow> y divides a"
@@ -2390,25 +2342,23 @@

lemma (in gcd_condition_monoid) SomeGcd_ex:
assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
-  shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
+  shows "\<exists>x \<in> carrier G. x = SomeGcd G A"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
-    apply (rule finite_inf_closed[simplified], fact+)
-    done
+    using finite_inf_closed by (simp add: assms SomeGcd_def)
qed

lemma (in gcd_condition_monoid) gcd_assoc:
-  assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
+  assumes "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
proof -
interpret weak_lower_semilattice "division_rel G"
by simp
show ?thesis
unfolding associated_def
-    by (meson carr divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
+    by (meson assms divides_trans gcd_divides gcd_divides_l gcd_divides_r gcd_exists)
qed

lemma (in gcd_condition_monoid) gcd_mult:
@@ -2641,141 +2591,124 @@
using Cons.IH Cons.prems(1) by force
qed

-
-lemma (in primeness_condition_monoid) wfactors_unique__hlp_induct:
-  "\<forall>a as'. a \<in> carrier G \<and> set as \<subseteq> carrier G \<and> set as' \<subseteq> carrier G \<and>
-           wfactors G as a \<and> wfactors G as' a \<longrightarrow> essentially_equal G as as'"
-proof (induct as)
+proposition (in primeness_condition_monoid) wfactors_unique:
+  assumes "wfactors G as a"  "wfactors G as' a"
+    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
+  shows "essentially_equal G as as'"
+  using assms
+proof (induct as arbitrary: a as')
case Nil
-  show ?case
-    apply (clarsimp simp: wfactors_def)
-    by (metis Units_one_closed assoc_unit_r list_update_nonempty unit_wfactors_empty unitfactor_ee wfactorsI)
+  then have "a \<sim> \<one>"
+    by (meson Units_one_closed one_closed perm.Nil perm_wfactorsD unit_wfactors)
+  then have "as' = []"
+    using Nil.prems assoc_unit_l unit_wfactors_empty by blast
+  then show ?case
+    by auto
next
case (Cons ah as)
-  then show ?case
-  proof clarsimp
-    fix a as'
-    assume ih [rule_format]:
-      "\<forall>a as'. a \<in> carrier G \<and> set as' \<subseteq> carrier G \<and> wfactors G as a \<and>
-        wfactors G as' a \<longrightarrow> essentially_equal G as as'"
-      and acarr: "a \<in> carrier G" and ahcarr: "ah \<in> carrier G"
-      and ascarr: "set as \<subseteq> carrier G" and as'carr: "set as' \<subseteq> carrier G"
-      and afs: "wfactors G (ah # as) a"
-      and afs': "wfactors G as' a"
-    then have ahdvda: "ah divides a"
-      by (intro wfactors_dividesI[of "ah#as" "a"]) simp_all
+  then have ahdvda: "ah divides a"
+    using wfactors_dividesI by auto
then obtain a' where a'carr: "a' \<in> carrier G" and a: "a = ah \<otimes> a'"
by blast
+    have carr_ah: "ah \<in> carrier G" "set as \<subseteq> carrier G"
+      using Cons.prems by fastforce+
+    have "ah \<otimes> foldr (\<otimes>) as \<one> \<sim> a"
+      by (rule wfactorsE[OF \<open>wfactors G (ah # as) a\<close>]) auto
+    then have "foldr (\<otimes>) as \<one> \<sim> a'"
+      by (metis Cons.prems(4) a a'carr assoc_l_cancel insert_subset list.set(2) monoid.multlist_closed monoid_axioms)
+    then
have a'fs: "wfactors G as a'"
-      apply (rule wfactorsE[OF afs], rule wfactorsI, simp)
-      by (metis a a'carr ahcarr ascarr assoc_l_cancel factorsI factors_def factors_mult_single list.set_intros(1) list.set_intros(2) multlist_closed)
-    from afs have ahirr: "irreducible G ah"
-      by (elim wfactorsE) simp
-    with ascarr have ahprime: "prime G ah"
-      by (intro irreducible_prime ahcarr)
-
-    note carr [simp] = acarr ahcarr ascarr as'carr a'carr
-
+      by (meson Cons.prems(1) set_subset_Cons subset_iff wfactorsE wfactorsI)
+    then have ahirr: "irreducible G ah"
+      by (meson Cons.prems(1) list.set_intros(1) wfactorsE)
+    with Cons have ahprime: "prime G ah"
note ahdvda
-    also from afs' have "a divides (foldr (\<otimes>) as' \<one>)"
-      by (elim wfactorsE associatedE, simp)
+    also have "a divides (foldr (\<otimes>) as' \<one>)"
+      by (meson Cons.prems(2) associatedE wfactorsE)
finally have "ah divides (foldr (\<otimes>) as' \<one>)"
-      by simp
+      using Cons.prems(4) by auto
with ahprime have "\<exists>i<length as'. ah divides as'!i"
-      by (intro multlist_prime_pos) simp_all
+      by (intro multlist_prime_pos) (use Cons.prems in auto)
then obtain i where len: "i<length as'" and ahdvd: "ah divides as'!i"
by blast
-    from afs' carr have irrasi: "irreducible G (as'!i)"
-      by (fast intro: nth_mem[OF len] elim: wfactorsE)
-    from len carr have asicarr[simp]: "as'!i \<in> carrier G"
-      unfolding set_conv_nth by force
-    note carr = carr asicarr
-
-    from ahdvd obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
+    then obtain x where "x \<in> carrier G" and asi: "as'!i = ah \<otimes> x"
by blast
-    with carr irrasi[simplified asi] have asiah: "as'!i \<sim> ah"
-      by (metis ahprime associatedI2 irreducible_prodE primeE)
+    have irrasi: "irreducible G (as'!i)"
+      using nth_mem[OF len] wfactorsE
+      by (metis Cons.prems(2))
+    have asicarr[simp]: "as'!i \<in> carrier G"
+      using len \<open>set as' \<subseteq> carrier G\<close> nth_mem by blast
+    have asiah: "as'!i \<sim> ah"
+      by (metis \<open>ah \<in> carrier G\<close> \<open>x \<in> carrier G\<close> asi irrasi ahprime associatedI2 irreducible_prodE primeE)
note setparts = set_take_subset[of i as'] set_drop_subset[of "Suc i" as']
-    note partscarr [simp] = setparts[THEN subset_trans[OF _ as'carr]]
-    note carr = carr partscarr
-
have "\<exists>aa_1. aa_1 \<in> carrier G \<and> wfactors G (take i as') aa_1"
-      by (meson afs' in_set_takeD partscarr(1) wfactorsE wfactors_prod_exists)
-    then obtain aa_1 where aa1carr: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
+      using Cons
+      by (metis setparts(1) subset_trans in_set_takeD wfactorsE wfactors_prod_exists)
+    then obtain aa_1 where aa1carr [simp]: "aa_1 \<in> carrier G" and aa1fs: "wfactors G (take i as') aa_1"
by auto
-
-    have "\<exists>aa_2. aa_2 \<in> carrier G \<and> wfactors G (drop (Suc i) as') aa_2"
-      by (meson afs' in_set_dropD partscarr(2) wfactors_def wfactors_prod_exists)
-    then obtain aa_2 where aa2carr: "aa_2 \<in> carrier G"
+    obtain aa_2 where aa2carr [simp]: "aa_2 \<in> carrier G"
and aa2fs: "wfactors G (drop (Suc i) as') aa_2"
-      by auto
-
-    note carr = carr aa1carr[simp] aa2carr[simp]
-
-    from aa1fs aa2fs
-    have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
-      by (intro wfactors_mult, simp+)
-    then have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
-      using irrasi wfactors_mult_single by auto
-    from aa2carr carr aa1fs aa2fs have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
-      by (metis irrasi wfactors_mult_single)
-    with len carr aa1carr aa2carr aa1fs
+      by (metis Cons.prems(2) Cons.prems(5) subset_code(1) in_set_dropD wfactors_def wfactors_prod_exists)
+
+    have set_drop: "set (drop (Suc i) as') \<subseteq> carrier G"
+      using Cons.prems(5) setparts(2) by blast
+    moreover have set_take: "set (take i as') \<subseteq> carrier G"
+      using  Cons.prems(5) setparts by auto
+    moreover have v1: "wfactors G (take i as' @ drop (Suc i) as') (aa_1 \<otimes> aa_2)"
+      using aa1fs aa2fs \<open>set as' \<subseteq> carrier G\<close> by (force simp add: dest: in_set_takeD in_set_dropD)
+    ultimately have v1': "wfactors G (as'!i # take i as' @ drop (Suc i) as') (as'!i \<otimes> (aa_1 \<otimes> aa_2))"
+      using irrasi wfactors_mult_single
+        by (simp add: irrasi v1 wfactors_mult_single)
+    have "wfactors G (as'!i # drop (Suc i) as') (as'!i \<otimes> aa_2)"
+      by (simp add: aa2fs irrasi set_drop wfactors_mult_single)
+    with len  aa1carr aa2carr aa1fs
have v2: "wfactors G (take i as' @ as'!i # drop (Suc i) as') (aa_1 \<otimes> (as'!i \<otimes> aa_2))"
-      using wfactors_mult by auto
+      using wfactors_mult  by (simp add: set_take set_drop)
from len have as': "as' = (take i as' @ as'!i # drop (Suc i) as')"
-    with carr have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
-      by simp
-    with v2 afs' carr aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
-      by (metis as' ee_wfactorsD m_closed)
+    have eer: "essentially_equal G (take i as' @ as'!i # drop (Suc i) as') as'"
+      using Cons.prems(5) as' by auto
+    with v2 aa1carr aa2carr nth_mem[OF len] have "aa_1 \<otimes> (as'!i \<otimes> aa_2) \<sim> a"
+      using Cons.prems as' comm_monoid_cancel.ee_wfactorsD is_comm_monoid_cancel by fastforce
then have t1: "as'!i \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
by (metis aa1carr aa2carr asicarr m_lcomm)
-    from carr asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
-      by (metis associated_sym m_closed mult_cong_l)
+    from asiah have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> as'!i \<otimes> (aa_1 \<otimes> aa_2)"
+      by (simp add: \<open>ah \<in> carrier G\<close> associated_sym mult_cong_l)
also note t1
-    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a" by simp
-
-    with carr aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
-      by (simp add: a, fast intro: assoc_l_cancel[of ah _ a'])
-
+    finally have "ah \<otimes> (aa_1 \<otimes> aa_2) \<sim> a"
+      using Cons.prems(3) carr_ah aa1carr aa2carr by blast
+    with aa1carr aa2carr a'carr nth_mem[OF len] have a': "aa_1 \<otimes> aa_2 \<sim> a'"
+      using a assoc_l_cancel carr_ah(1) by blast
note v1
also note a'
finally have "wfactors G (take i as' @ drop (Suc i) as') a'"
-      by simp
-
-    from a'fs this carr have "essentially_equal G as (take i as' @ drop (Suc i) as')"
-      by (intro ih[of a']) simp
-    then have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
-      by (elim essentially_equalE) (fastforce intro: essentially_equalI)
-
-    from carr have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
+      by (simp add: a'carr set_drop set_take)
+    from a'fs this have "essentially_equal G as (take i as' @ drop (Suc i) as')"
+      using Cons.hyps a'carr carr_ah(2) set_drop set_take by auto
+    with carr_ah have ee1: "essentially_equal G (ah # as) (ah # take i as' @ drop (Suc i) as')"
+      by (auto simp: essentially_equal_def)
+    have ee2: "essentially_equal G (ah # take i as' @ drop (Suc i) as')
(as' ! i # take i as' @ drop (Suc i) as')"
proof (intro essentially_equalI)
show "ah # take i as' @ drop (Suc i) as' <~~> ah # take i as' @ drop (Suc i) as'"
by simp
next
show "ah # take i as' @ drop (Suc i) as' [\<sim>] as' ! i # take i as' @ drop (Suc i) as'"
+        by (simp add: asiah associated_sym set_drop set_take)
qed

note ee1
also note ee2
also have "essentially_equal G (as' ! i # take i as' @ drop (Suc i) as')
(take i as' @ as' ! i # drop (Suc i) as')"
-      by (metis as' as'carr listassoc_refl essentially_equalI perm_append_Cons)
+      by (metis Cons.prems(5) as' essentially_equalI listassoc_refl perm_append_Cons)
finally have "essentially_equal G (ah # as) (take i as' @ as' ! i # drop (Suc i) as')"
-      by simp
-    then show "essentially_equal G (ah # as) as'"
-      by (subst as')
-  qed
+      using Cons.prems(4) set_drop set_take by auto
+    then show ?case
+      using as' by auto
qed

-lemma (in primeness_condition_monoid) wfactors_unique:
-  assumes "wfactors G as a"  "wfactors G as' a"
-    and "a \<in> carrier G"  "set as \<subseteq> carrier G"  "set as' \<subseteq> carrier G"
-  shows "essentially_equal G as as'"
-  by (rule wfactors_unique__hlp_induct[rule_format, of a]) (simp add: assms)
-

subsubsection \<open>Application to factorial monoids\<close>

@@ -2841,7 +2774,6 @@
by blast

note [simp] = acarr bcarr ccarr ascarr cscarr
-
assume b: "b = a \<otimes> c"
from afs cfs have "wfactors G (as@cs) (a \<otimes> c)"
by (intro wfactors_mult) simp_all
@@ -2918,9 +2850,7 @@
apply unfold_locales
apply (rule wfUNIVI)
apply (rule measure_induct[of "factorcount G"])
-  apply simp
-  apply (metis properfactor_fcount)
-  done
+  using properfactor_fcount by auto

sublocale factorial_monoid \<subseteq> primeness_condition_monoid
by standard (rule irreducible_prime)