src/HOL/Algebra/Divisibility.thy

 (*
   Title:     Divisibility in monoids and rings
-  Id:        $Id$
   Author:    Clemens Ballarin, started 18 July 2008
 
 Based on work by Stephan Hohe.
 *)
 

 
 lemma (in monoid_cancel) is_monoid_cancel:
   "monoid_cancel G"
   ..
 
-interpretation group \<subseteq> monoid_cancel
+sublocale group \<subseteq> monoid_cancel
   proof qed simp+
 
 
 locale comm_monoid_cancel = monoid_cancel + comm_monoid
 

   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"
 proof -
-  interpret comm_monoid [G] by fact
+  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 (simp add: m_comm)

 
 lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
   "comm_monoid_cancel G"
   by intro_locales
 
-interpretation comm_group \<subseteq> comm_monoid_cancel
+sublocale comm_group \<subseteq> comm_monoid_cancel
   ..
 
 
 subsection {* Products of Units in Monoids *}
 

     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "properfactor G x' y"
 using pf
 unfolding properfactor_lless
 proof -
-  interpret weak_partial_order ["division_rel G"] ..
+  interpret weak_partial_order "division_rel G" ..
   from x'x
        have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
   also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
   finally
        show "x' \<sqsubset>\<^bsub>division_rel G\<^esub> y" by (simp add: carr)

     and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   shows "properfactor G x y'"
 using pf
 unfolding properfactor_lless
 proof -
-  interpret weak_partial_order ["division_rel G"] ..
+  interpret weak_partial_order "division_rel G" ..
   assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
   also from yy'
        have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
   finally
        show "x \<sqsubset>\<^bsub>division_rel G\<^esub> y'" by (simp add: carr)

 subsubsection {* Gcd condition *}
 
 lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
   shows "weak_lower_semilattice (division_rel G)"
 proof -
-  interpret weak_partial_order ["division_rel G"] ..
+  interpret weak_partial_order "division_rel G" ..
   show ?thesis
   apply (unfold_locales, simp_all)
   proof -
     fix x y
     assume carr: "x \<in> carrier G"  "y \<in> carrier G"

     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"
   shows "a' gcdof b c"
 proof -
   note carr = a'carr carr'
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  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 add: a'a)
       apply (simp add: carr)

 
 lemma (in gcd_condition_monoid) gcd_closed [simp]:
   assumes carr: "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
+  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
 qed
 
 lemma (in gcd_condition_monoid) gcd_isgcd:
   assumes carr: "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
+  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+)

 
 lemma (in gcd_condition_monoid) gcd_exists:
   assumes carr: "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
+  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
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_l:
   assumes carr: "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
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_left[simplified], fact+)
   done
 qed
 
 lemma (in gcd_condition_monoid) gcd_divides_r:
   assumes carr: "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
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet[OF carr])
     apply (rule meet_right[simplified], fact+)
   done
 qed

 lemma (in gcd_condition_monoid) gcd_divides:
   assumes sub: "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 -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: somegcd_meet L)
     apply (rule meet_le[simplified], fact+)
   done
 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"
   shows "somegcd G x y \<sim> somegcd G x' y"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  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
 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'"
   shows "somegcd G x y \<sim> somegcd G x y'"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  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
 qed

 
 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"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (simp add: SomeGcd_def)
     apply (rule finite_inf_closed[simplified], fact+)
   done
 qed
 
 lemma (in gcd_condition_monoid) gcd_assoc:
   assumes carr: "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
+  interpret weak_lower_semilattice "division_rel G" by simp
   show ?thesis
     apply (subst (2 3) somegcd_meet, (simp add: carr)+)
     apply (simp add: somegcd_meet carr)
     apply (rule weak_meet_assoc[simplified], fact+)
   done

     with pnunit
         show "False" ..
   qed
 qed
 
-interpretation gcd_condition_monoid \<subseteq> primeness_condition_monoid
+sublocale gcd_condition_monoid \<subseteq> primeness_condition_monoid
   by (rule primeness_condition)
 
 
 subsubsection {* Divisor chain condition *}
 

   qed
 
   with fca fcb show ?thesis by simp
 qed
 
-interpretation factorial_monoid \<subseteq> divisor_chain_condition_monoid
+sublocale factorial_monoid \<subseteq> divisor_chain_condition_monoid
 apply unfold_locales
 apply (rule wfUNIVI)
 apply (rule measure_induct[of "factorcount G"])
 apply simp (* slow *) (*
   [1]Applying congruence rule:

     apply (rule r2)
     apply (rule properfactor_fcount, simp+)
   done
 qed
 
-interpretation factorial_monoid \<subseteq> primeness_condition_monoid
+sublocale factorial_monoid \<subseteq> primeness_condition_monoid
   proof qed (rule irreducible_is_prime)
 
 
 lemma (in factorial_monoid) primeness_condition:
   shows "primeness_condition_monoid G"

 
 lemma (in factorial_monoid) gcd_condition [simp]:
   shows "gcd_condition_monoid G"
   proof qed (rule gcdof_exists)
 
-interpretation factorial_monoid \<subseteq> gcd_condition_monoid
+sublocale factorial_monoid \<subseteq> gcd_condition_monoid
   proof qed (rule gcdof_exists)
 
 lemma (in factorial_monoid) division_weak_lattice [simp]:
   shows "weak_lattice (division_rel G)"
 proof -
-  interpret weak_lower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice "division_rel G" by simp
 
   show "weak_lattice (division_rel G)"
   apply (unfold_locales, simp_all)
   proof -
     fix x y

          factorial_monoid G"
 apply rule
 proof clarify
   assume dcc: "divisor_chain_condition_monoid G"
      and pc: "primeness_condition_monoid G"
-  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
-  interpret primeness_condition_monoid ["G"] by (rule pc)
+  interpret divisor_chain_condition_monoid "G" by (rule dcc)
+  interpret primeness_condition_monoid "G" by (rule pc)
 
   show "factorial_monoid G"
       by (fast intro: factorial_monoidI wfactors_exist wfactors_unique)
 next
   assume fm: "factorial_monoid G"
-  interpret factorial_monoid ["G"] by (rule fm)
+  interpret factorial_monoid "G" by (rule fm)
   show "divisor_chain_condition_monoid G \<and> primeness_condition_monoid G"
       by rule unfold_locales
 qed
 
 theorem factorial_condition_two: (* Jacobson theorem 2.22 *)
   shows "(divisor_chain_condition_monoid G \<and> gcd_condition_monoid G) = factorial_monoid G"
 apply rule
 proof clarify
     assume dcc: "divisor_chain_condition_monoid G"
      and gc: "gcd_condition_monoid G"
-  interpret divisor_chain_condition_monoid ["G"] by (rule dcc)
-  interpret gcd_condition_monoid ["G"] by (rule gc)
+  interpret divisor_chain_condition_monoid "G" by (rule dcc)
+  interpret gcd_condition_monoid "G" by (rule gc)
   show "factorial_monoid G"
       by (simp add: factorial_condition_one[symmetric], rule, unfold_locales)
 next
   assume fm: "factorial_monoid G"
-  interpret factorial_monoid ["G"] by (rule fm)
+  interpret factorial_monoid "G" by (rule fm)
   show "divisor_chain_condition_monoid G \<and> gcd_condition_monoid G"
       by rule unfold_locales
 qed
 
 end