author ballarin Wed, 15 Oct 2008 15:44:15 +0200 changeset 28599 12d914277b8d parent 28598 cb5f98e2e187 child 28600 54352ed7114f
Removed 'includes'.
```--- a/src/HOL/Algebra/Divisibility.thy	Wed Oct 15 00:18:43 2008 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Oct 15 15:44:15 2008 +0200
@@ -39,16 +39,21 @@
locale comm_monoid_cancel = monoid_cancel + comm_monoid

lemma comm_monoid_cancelI:
-  includes comm_monoid
+  fixes G (structure)
+  assumes "comm_monoid G"
assumes cancel:
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
shows "comm_monoid_cancel G"
-apply unfold_locales
- apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
-  apply (iprover intro: cancel)
-apply (iprover intro: cancel)
-done
+proof -
+  interpret comm_monoid [G] by fact
+  show "comm_monoid_cancel G"
+    apply unfold_locales
+    apply (subgoal_tac "a \<otimes> c = b \<otimes> c")
+    apply (iprover intro: cancel)
+    apply (iprover intro: cancel)
+    done
+qed

lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
"comm_monoid_cancel G"
@@ -1321,7 +1326,7 @@
subsubsection {* Factorization in irreducible elements *}

lemma wfactorsI:
-  includes (struct G)
+  fixes G (structure)
assumes "\<forall>f\<in>set fs. irreducible G f"
and "foldr (op \<otimes>) fs \<one> \<sim> a"
shows "wfactors G fs a"
@@ -1330,7 +1335,7 @@
by simp

lemma wfactorsE:
-  includes (struct G)
+  fixes G (structure)
assumes wf: "wfactors G fs a"
and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> \<sim> a\<rbrakk> \<Longrightarrow> P"
shows "P"
@@ -1339,7 +1344,7 @@
by (fast dest: e)

lemma (in monoid) factorsI:
-  includes (struct G)
+  fixes G (structure)
assumes "\<forall>f\<in>set fs. irreducible G f"
and "foldr (op \<otimes>) fs \<one> = a"
shows "factors G fs a"
@@ -1348,7 +1353,7 @@
by simp

lemma factorsE:
-  includes (struct G)
+  fixes G (structure)
assumes f: "factors G fs a"
and e: "\<lbrakk>\<forall>f\<in>set fs. irreducible G f; foldr (op \<otimes>) fs \<one> = a\<rbrakk> \<Longrightarrow> P"
shows "P"```