diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy Sun Nov 26 13:19:52 2017 +0100
+++ b/src/HOL/Algebra/Ring.thy Sun Nov 26 21:08:32 2017 +0100
@@ -238,9 +238,9 @@
locale cring = ring + comm_monoid R
locale "domain" = cring +
- assumes one_not_zero [simp]: "\ ~= \"
+ assumes one_not_zero [simp]: "\ \ \"
and integral: "[| a \ b = \; a \ carrier R; b \ carrier R |] ==>
- a = \ | b = \"
+ a = \ \ b = \"
locale field = "domain" +
assumes field_Units: "Units R = carrier R - {\}"
@@ -427,7 +427,7 @@
a_lcomm m_lcomm r_distr l_null r_null l_minus r_minus
lemma (in semiring) nat_pow_zero:
- "(n::nat) ~= 0 ==> \ (^) n = \"
+ "(n::nat) \ 0 \ \ (^) n = \"
by (induct n) simp_all
context semiring begin
@@ -469,7 +469,7 @@
fixes R (structure) and S (structure)
assumes "ring R" "cring S"
assumes RS: "a \ carrier R" "b \ carrier R" "c \ carrier S" "d \ carrier S"
- shows "a \ \ (a \ \ b) = b & c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c"
+ shows "a \ \ (a \ \ b) = b \ c \\<^bsub>S\<^esub> d = d \\<^bsub>S\<^esub> c"
proof -
interpret ring R by fact
interpret cring S by fact
@@ -513,27 +513,27 @@
context "domain" begin
lemma zero_not_one [simp]:
- "\ ~= \"
+ "\ \ \"
by (rule not_sym) simp
lemma integral_iff: (* not by default a simp rule! *)
- "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ | b = \)"
+ "[| a \ carrier R; b \ carrier R |] ==> (a \ b = \) = (a = \ \ b = \)"
proof
assume "a \ carrier R" "b \ carrier R" "a \ b = \"
- then show "a = \ | b = \" by (simp add: integral)
+ then show "a = \ \ b = \" by (simp add: integral)
next
- assume "a \ carrier R" "b \ carrier R" "a = \ | b = \"
+ assume "a \ carrier R" "b \ carrier R" "a = \ \ b = \"
then show "a \ b = \" by auto
qed
lemma m_lcancel:
- assumes prem: "a ~= \"
+ assumes prem: "a \ \"
and R: "a \ carrier R" "b \ carrier R" "c \ carrier R"
shows "(a \ b = a \ c) = (b = c)"
proof
assume eq: "a \ b = a \ c"
with R have "a \ (b \ c) = \" by algebra
- with R have "a = \ | (b \ c) = \" by (simp add: integral_iff)
+ with R have "a = \ \ (b \ c) = \" by (simp add: integral_iff)
with prem and R have "b \ c = \" by auto
with R have "b = b \ (b \ c)" by algebra
also from R have "b \ (b \ c) = c" by algebra
@@ -543,7 +543,7 @@
qed
lemma m_rcancel:
- assumes prem: "a ~= \"
+ assumes prem: "a \ \"
and R: "a \ carrier R" "b \ carrier R" "c \ carrier R"
shows conc: "(b \ a = c \ a) = (b = c)"
proof -
@@ -609,9 +609,9 @@
definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
where "ring_hom R S =
- {h. h \ carrier R \ carrier S &
- (ALL x y. x \ carrier R & y \ carrier R -->
- h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y & h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y) &
+ {h. h \ carrier R \ carrier S \
+ (\x y. x \ carrier R \ y \ carrier R \
+ h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y \ h (x \\<^bsub>R\<^esub> y) = h x \\<^bsub>S\<^esub> h y) \
h \\<^bsub>R\<^esub> = \\<^bsub>S\<^esub>}"
lemma ring_hom_memI:
@@ -675,13 +675,13 @@
qed
lemma (in ring_hom_cring) hom_finsum [simp]:
- "f \ A \ carrier R ==>
- h (finsum R f A) = finsum S (h o f) A"
+ "f \ A \ carrier R \
+ h (finsum R f A) = finsum S (h \ f) A"
by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
lemma (in ring_hom_cring) hom_finprod:
- "f \ A \ carrier R ==>
- h (finprod R f A) = finprod S (h o f) A"
+ "f \ A \ carrier R \
+ h (finprod R f A) = finprod S (h \ f) A"
by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
declare ring_hom_cring.hom_finprod [simp]