src/HOL/Semiring_Normalization.thy

       hence "w = x" using kp by simp }
     ultimately have "w=x" by blast }
   then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto
 qed
 
+text {* semiring normalization proper *}
+
 setup Semiring_Normalizer.setup
 
-lemma (in comm_semiring_1) semiring_ops:
+context comm_semiring_1
+begin
+
+lemma semiring_ops:
   shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)"
     and "TERM 0" and "TERM 1" .
 
-lemma (in comm_semiring_1) semiring_rules:
+lemma semiring_rules:
   "(a * m) + (b * m) = (a + b) * m"
   "(a * m) + m = (a + 1) * m"
   "m + (a * m) = (a + 1) * m"
   "m + m = (1 + 1) * m"
   "0 + a = a"

   "x ^ (Suc q) = x * (x ^ q)"
   "x ^ (2*n) = (x ^ n) * (x ^ n)"
   "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"
   by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult)
 
-lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms =
+lemmas normalizing_comm_semiring_1_axioms =
   comm_semiring_1_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules]
 
-declaration (in comm_semiring_1)
+declaration
   {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *}
 
-lemma (in comm_ring_1) ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
-
-lemma (in comm_ring_1) ring_rules:
+end
+
+context comm_ring_1
+begin
+
+lemma ring_ops: shows "TERM (x- y)" and "TERM (- x)" .
+
+lemma ring_rules:
   "- x = (- 1) * x"
   "x - y = x + (- y)"
   by (simp_all add: diff_minus)
 
-lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms =
+lemmas normalizing_comm_ring_1_axioms =
   comm_ring_1_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules
     ring ops: ring_ops
     ring rules: ring_rules]
 
-declaration (in comm_ring_1)
+declaration
   {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *}
 
-lemma (in comm_semiring_1_cancel_norm) noteq_reduce:
+end
+
+context comm_semiring_1_cancel_norm
+begin
+
+lemma noteq_reduce:
   "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
 proof-
   have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp
   also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
     using add_mult_solve by blast
   finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)"
     by simp
 qed
 
-lemma (in comm_semiring_1_cancel_norm) add_scale_eq_noteq:
+lemma add_scale_eq_noteq:
   "\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)"
 proof(clarify)
   assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d"
     and eq: "b + (r * c) = b + (r * d)"
   have "(0 * d) + (r * c) = (0 * c) + (r * d)"
     using add_imp_eq eq mult_zero_left by simp
   thus "False" using add_mult_solve[of 0 d] nz cnd by simp
 qed
 
-lemma (in comm_semiring_1_cancel_norm) add_0_iff:
+lemma add_0_iff:
   "x = x + a \<longleftrightarrow> a = 0"
 proof-
   have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto
   thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute)
 qed
 
-declare (in comm_semiring_1_cancel_norm)
+declare
   normalizing_comm_semiring_1_axioms [normalizer del]
 
-lemmas (in comm_semiring_1_cancel_norm)
+lemmas
   normalizing_comm_semiring_1_cancel_norm_axioms =
   comm_semiring_1_cancel_norm_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules
     idom rules: noteq_reduce add_scale_eq_noteq]
 
-declaration (in comm_semiring_1_cancel_norm)
+declaration
   {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *}
 
-declare (in idom) normalizing_comm_ring_1_axioms [normalizer del]
-
-lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer
+end
+
+context idom
+begin
+
+declare normalizing_comm_ring_1_axioms [normalizer del]
+
+lemmas normalizing_idom_axioms = idom_axioms [normalizer
   semiring ops: semiring_ops
   semiring rules: semiring_rules
   ring ops: ring_ops
   ring rules: ring_rules
   idom rules: noteq_reduce add_scale_eq_noteq
   ideal rules: right_minus_eq add_0_iff]
 
-declaration (in idom)
+declaration
   {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *}
 
-lemma (in field) field_ops:
+end
+
+context field
+begin
+
+lemma field_ops:
   shows "TERM (x / y)" and "TERM (inverse x)" .
 
-lemmas (in field) field_rules = divide_inverse inverse_eq_divide
-
-lemmas (in field) normalizing_field_axioms =
+lemmas field_rules = divide_inverse inverse_eq_divide
+
+lemmas normalizing_field_axioms =
   field_axioms [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules
     ring ops: ring_ops
     ring rules: ring_rules
     field ops: field_ops
     field rules: field_rules
     idom rules: noteq_reduce add_scale_eq_noteq
     ideal rules: right_minus_eq add_0_iff]
 
-declaration (in field)
+declaration
   {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *}
+
+end
 
 hide_fact (open) normalizing_comm_semiring_1_axioms
   normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules
 
 hide_fact (open) normalizing_comm_ring_1_axioms
   normalizing_idom_axioms ring_ops ring_rules
 
-hide_fact (open)  normalizing_field_axioms field_ops field_rules
+hide_fact (open) normalizing_field_axioms field_ops field_rules
 
 hide_fact (open) add_scale_eq_noteq noteq_reduce
 
 end