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]