\<^sub>N" 60) -where - "Ndiv \ \a b. a *\<^sub>N Ninv b" +definition Ndiv :: "Num \ Num \ Num" (infixl "\

\<^sub>N" 60) + where "Ndiv = (\a b. a *\<^sub>N Ninv b)" lemma Nneg_normN[simp]: "isnormNum x \ isnormNum (~\<^sub>N x)" - by(simp add: isnormNum_def Nneg_def split_def) + by (simp add: isnormNum_def Nneg_def split_def) + lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)" by (simp add: Nadd_def split_def) + lemma Nsub_normN[simp]: "\ isnormNum y\ \ isnormNum (x -\<^sub>N y)" by (simp add: Nsub_def split_def) -lemma Nmul_normN[simp]: assumes xn:"isnormNum x" and yn: "isnormNum y" + +lemma Nmul_normN[simp]: + assumes xn: "isnormNum x" and yn: "isnormNum y" shows "isnormNum (x *\<^sub>N y)" -proof- - have "\a b. x = (a,b)" and "\ a' b'. y = (a',b')" by auto - then obtain a b a' b' where ab: "x = (a,b)" and ab': "y = (a',b')" by blast - {assume "a = 0" - hence ?thesis using xn ab ab' - by (simp add: isnormNum_def Let_def Nmul_def split_def)} +proof - + obtain a b where x: "x = (a, b)" by (cases x) + obtain a' b' where y: "y = (a', b')" by (cases y) + { assume "a = 0" + hence ?thesis using xn x y + by (simp add: isnormNum_def Let_def Nmul_def split_def) } moreover - {assume "a' = 0" - hence ?thesis using yn ab ab' - by (simp add: isnormNum_def Let_def Nmul_def split_def)} + { assume "a' = 0" + hence ?thesis using yn x y + by (simp add: isnormNum_def Let_def Nmul_def split_def) } moreover - {assume a: "a \0" and a': "a'\0" - hence bp: "b > 0" "b' > 0" using xn yn ab ab' by (simp_all add: isnormNum_def) - from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a*a', b*b')" - using ab ab' a a' bp by (simp add: Nmul_def Let_def split_def normNum_def) - hence ?thesis by simp} + { assume a: "a \0" and a': "a'\0" + hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def) + from mult_pos_pos[OF bp] have "x *\<^sub>N y = normNum (a * a', b * b')" + using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def) + hence ?thesis by simp } ultimately show ?thesis by blast qed @@ -139,89 +124,77 @@ by (simp add: Ninv_def isnormNum_def split_def) (cases "fst x = 0", auto simp add: gcd_commute_int) -lemma isnormNum_int[simp]: +lemma isnormNum_int[simp]: "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \ 0 \ isnormNum (i\<^sub>N)" by (simp_all add: isnormNum_def) text {* Relations over Num *} -definition - Nlt0:: "Num \ bool" ("0>\<^sub>N") -where - "Nlt0 = (\(a,b). a < 0)" +definition Nlt0:: "Num \ bool" ("0>\<^sub>N") + where "Nlt0 = (\(a,b). a < 0)" -definition - Nle0:: "Num \ bool" ("0\\<^sub>N") -where - "Nle0 = (\(a,b). a \ 0)" +definition Nle0:: "Num \ bool" ("0\\<^sub>N") + where "Nle0 = (\(a,b). a \ 0)" -definition - Ngt0:: "Num \ bool" ("0<\<^sub>N") -where - "Ngt0 = (\(a,b). a > 0)" +definition Ngt0:: "Num \ bool" ("0<\<^sub>N") + where "Ngt0 = (\(a,b). a > 0)" -definition - Nge0:: "Num \ bool" ("0\\<^sub>N") -where - "Nge0 = (\(a,b). a \ 0)" +definition Nge0:: "Num \ bool" ("0\\<^sub>N") + where "Nge0 = (\(a,b). a \ 0)" -definition - Nlt :: "Num \ Num \ bool" (infix "<\<^sub>N" 55) -where - "Nlt = (\a b. 0>\<^sub>N (a -\<^sub>N b))" +definition Nlt :: "Num \ Num \ bool" (infix "<\<^sub>N" 55) + where "Nlt = (\a b. 0>\<^sub>N (a -\<^sub>N b))" -definition - Nle :: "Num \ Num \ bool" (infix "\\<^sub>N" 55) -where - "Nle = (\a b. 0\\<^sub>N (a -\<^sub>N b))" +definition Nle :: "Num \ Num \ bool" (infix "\\<^sub>N" 55) + where "Nle = (\a b. 0\\<^sub>N (a -\<^sub>N b))" -definition - "INum = (\(a,b). of_int a / of_int b)" +definition "INum = (\(a,b). of_int a / of_int b)" lemma INum_int [simp]: "INum (i\<^sub>N) = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" by (simp_all add: INum_def) -lemma isnormNum_unique[simp]: - assumes na: "isnormNum x" and nb: "isnormNum y" +lemma isnormNum_unique[simp]: + assumes na: "isnormNum x" and nb: "isnormNum y" shows "((INum x ::'a::{field_char_0, field_inverse_zero}) = INum y) = (x = y)" (is "?lhs = ?rhs") proof - have "\ a b a' b'. x = (a,b) \ y = (a',b')" by auto - then obtain a b a' b' where xy[simp]: "x = (a,b)" "y=(a',b')" by blast - assume H: ?lhs - {assume "a = 0 \ b = 0 \ a' = 0 \ b' = 0" + obtain a b where x: "x = (a, b)" by (cases x) + obtain a' b' where y: "y = (a', b')" by (cases y) + assume H: ?lhs + { assume "a = 0 \ b = 0 \ a' = 0 \ b' = 0" hence ?rhs using na nb H - by (simp add: INum_def split_def isnormNum_def split: split_if_asm)} + by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) } moreover { assume az: "a \ 0" and bz: "b \ 0" and a'z: "a'\0" and b'z: "b'\0" - from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: isnormNum_def) - from H bz b'z have eq:"a * b' = a'*b" - by (simp add: INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult) - from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1" - by (simp_all add: isnormNum_def add: gcd_commute_int) - from eq have raw_dvd: "a dvd a'*b" "b dvd b'*a" "a' dvd a*b'" "b' dvd b*a'" - apply - + from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: x y isnormNum_def) + from H bz b'z have eq: "a * b' = a'*b" + by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult) + from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1" + by (simp_all add: x y isnormNum_def add: gcd_commute_int) + from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'" + apply - apply algebra apply algebra apply simp apply algebra done from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)] - coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]] + coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]] have eq1: "b = b'" using pos by arith with eq have "a = a'" using pos by simp - with eq1 have ?rhs by simp} + with eq1 have ?rhs by (simp add: x y) } ultimately show ?rhs by blast next assume ?rhs thus ?lhs by simp qed -lemma isnormNum0[simp]: "isnormNum x \ (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)" +lemma isnormNum0[simp]: + "isnormNum x \ (INum x = (0::'a::{field_char_0, field_inverse_zero})) = (x = 0\<^sub>N)" unfolding INum_int(2)[symmetric] - by (rule isnormNum_unique, simp_all) + by (rule isnormNum_unique) simp_all -lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = +lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)" proof - assume "d ~= 0" @@ -231,7 +204,7 @@ by auto then have eq: "of_int x = ?t" by (simp only: of_int_mult[symmetric] of_int_add [symmetric]) - then have "of_int x / of_int d = ?t / of_int d" + then have "of_int x / of_int d = ?t / of_int d" using cong[OF refl[of ?f] eq] by simp then show ?thesis by (simp add: add_divide_distrib algebra_simps `d ~= 0`) qed @@ -241,25 +214,26 @@ apply (frule of_int_div_aux [of d n, where ?'a = 'a]) apply simp apply (simp add: dvd_eq_mod_eq_0) -done + done lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field_inverse_zero})" -proof- - have "\ a b. x = (a,b)" by auto - then obtain a b where x[simp]: "x = (a,b)" by blast - {assume "a=0 \ b = 0" hence ?thesis - by (simp add: INum_def normNum_def split_def Let_def)} - moreover - {assume a: "a\0" and b: "b\0" +proof - + obtain a b where x: "x = (a, b)" by (cases x) + { assume "a = 0 \ b = 0" + hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) } + moreover + { assume a: "a \ 0" and b: "b \ 0" let ?g = "gcd a b" from a b have g: "?g \ 0"by simp from of_int_div[OF g, where ?'a = 'a] - have ?thesis by (auto simp add: INum_def normNum_def split_def Let_def)} + have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) } ultimately show ?thesis by blast qed -lemma INum_normNum_iff: "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \ normNum x = normNum y" (is "?lhs = ?rhs") +lemma INum_normNum_iff: + "(INum x ::'a::{field_char_0, field_inverse_zero}) = INum y \ normNum x = normNum y" + (is "?lhs = ?rhs") proof - have "normNum x = normNum y \ (INum (normNum x) :: 'a) = INum (normNum y)" by (simp del: normNum) @@ -268,139 +242,157 @@ qed lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field_inverse_zero})" -proof- -let ?z = "0:: 'a" - have " \ a b. x = (a,b)" " \ a' b'. y = (a',b')" by auto - then obtain a b a' b' where x[simp]: "x = (a,b)" - and y[simp]: "y = (a',b')" by blast - {assume "a=0 \ a'= 0 \ b =0 \ b' = 0" hence ?thesis - apply (cases "a=0",simp_all add: Nadd_def) - apply (cases "b= 0",simp_all add: INum_def) - apply (cases "a'= 0",simp_all) - apply (cases "b'= 0",simp_all) +proof - + let ?z = "0:: 'a" + obtain a b where x: "x = (a, b)" by (cases x) + obtain a' b' where y: "y = (a', b')" by (cases y) + { assume "a=0 \ a'= 0 \ b =0 \ b' = 0" + hence ?thesis + apply (cases "a=0", simp_all add: x y Nadd_def) + apply (cases "b= 0", simp_all add: INum_def) + apply (cases "a'= 0", simp_all) + apply (cases "b'= 0", simp_all) done } - moreover - {assume aa':"a \ 0" "a'\ 0" and bb': "b \ 0" "b' \ 0" - {assume z: "a * b' + b * a' = 0" + moreover + { assume aa': "a \ 0" "a'\ 0" and bb': "b \ 0" "b' \ 0" + { assume z: "a * b' + b * a' = 0" hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp - hence "of_int b' * of_int a / (of_int b * of_int b') + of_int b * of_int a' / (of_int b * of_int b') = ?z" by (simp add:add_divide_distrib) - hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' by simp - from z aa' bb' have ?thesis - by (simp add: th Nadd_def normNum_def INum_def split_def)} - moreover {assume z: "a * b' + b * a' \ 0" + hence "of_int b' * of_int a / (of_int b * of_int b') + + of_int b * of_int a' / (of_int b * of_int b') = ?z" + by (simp add:add_divide_distrib) + hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' + by simp + from z aa' bb' have ?thesis + by (simp add: x y th Nadd_def normNum_def INum_def split_def) } + moreover { + assume z: "a * b' + b * a' \ 0" let ?g = "gcd (a * b' + b * a') (b*b')" have gz: "?g \ 0" using z by simp have ?thesis using aa' bb' z gz - of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]] of_int_div[where ?'a = 'a, - OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]] - by (simp add: Nadd_def INum_def normNum_def Let_def add_divide_distrib)} - ultimately have ?thesis using aa' bb' - by (simp add: Nadd_def INum_def normNum_def Let_def) } + of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a * b' + b * a'" and y="b*b'"]] + of_int_div[where ?'a = 'a, OF gz gcd_dvd2_int[where x="a * b' + b * a'" and y="b*b'"]] + by (simp add: x y Nadd_def INum_def normNum_def Let_def add_divide_distrib) } + ultimately have ?thesis using aa' bb' + by (simp add: x y Nadd_def INum_def normNum_def Let_def) } ultimately show ?thesis by blast qed -lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero}) " -proof- +lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field_inverse_zero})" +proof - let ?z = "0::'a" - have " \ a b. x = (a,b)" " \ a' b'. y = (a',b')" by auto - then obtain a b a' b' where x: "x = (a,b)" and y: "y = (a',b')" by blast - {assume "a=0 \ a'= 0 \ b = 0 \ b' = 0" hence ?thesis - apply (cases "a=0",simp_all add: x y Nmul_def INum_def Let_def) - apply (cases "b=0",simp_all) - apply (cases "a'=0",simp_all) + obtain a b where x: "x = (a, b)" by (cases x) + obtain a' b' where y: "y = (a', b')" by (cases y) + { assume "a=0 \ a'= 0 \ b = 0 \ b' = 0" + hence ?thesis + apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def) + apply (cases "b=0", simp_all) + apply (cases "a'=0", simp_all) done } moreover - {assume z: "a \ 0" "a' \ 0" "b \ 0" "b' \ 0" + { assume z: "a \ 0" "a' \ 0" "b \ 0" "b' \ 0" let ?g="gcd (a*a') (b*b')" have gz: "?g \ 0" using z by simp - from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]] - of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]] - have ?thesis by (simp add: Nmul_def x y Let_def INum_def)} + from z of_int_div[where ?'a = 'a, OF gz gcd_dvd1_int[where x="a*a'" and y="b*b'"]] + of_int_div[where ?'a = 'a , OF gz gcd_dvd2_int[where x="a*a'" and y="b*b'"]] + have ?thesis by (simp add: Nmul_def x y Let_def INum_def) } ultimately show ?thesis by blast qed lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" by (simp add: Nneg_def split_def INum_def) -lemma Nsub[simp]: shows "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})" -by (simp add: Nsub_def split_def) +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field_inverse_zero})" + by (simp add: Nsub_def split_def) lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field_inverse_zero) / (INum x)" by (simp add: Ninv_def INum_def split_def) -lemma Ndiv[simp]: "INum (x \

\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" by (simp add: Ndiv_def) +lemma Ndiv[simp]: "INum (x \

\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field_inverse_zero})" + by (simp add: Ndiv_def) -lemma Nlt0_iff[simp]: assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x " -proof- - have " \ a b. x = (a,b)" by simp - then obtain a b where x[simp]:"x = (a,b)" by blast - {assume "a = 0" hence ?thesis by (simp add: Nlt0_def INum_def) } +lemma Nlt0_iff[simp]: + assumes nx: "isnormNum x" + shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})< 0) = 0>\<^sub>N x" +proof - + obtain a b where x: "x = (a, b)" by (cases x) + { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) } moreover - {assume a: "a\0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def) + { assume a: "a \ 0" hence b: "(of_int b::'a) > 0" + using nx by (simp add: x isnormNum_def) from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"] - have ?thesis by (simp add: Nlt0_def INum_def)} + have ?thesis by (simp add: x Nlt0_def INum_def) } ultimately show ?thesis by blast qed -lemma Nle0_iff[simp]:assumes nx: "isnormNum x" +lemma Nle0_iff[simp]: + assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \ 0) = 0\\<^sub>N x" -proof- - have " \ a b. x = (a,b)" by simp - then obtain a b where x[simp]:"x = (a,b)" by blast - {assume "a = 0" hence ?thesis by (simp add: Nle0_def INum_def) } +proof - + obtain a b where x: "x = (a, b)" by (cases x) + { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) } moreover - {assume a: "a\0" hence b: "(of_int b :: 'a) > 0" using nx by (simp add: isnormNum_def) + { assume a: "a \ 0" hence b: "(of_int b :: 'a) > 0" + using nx by (simp add: x isnormNum_def) from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"] - have ?thesis by (simp add: Nle0_def INum_def)} + have ?thesis by (simp add: x Nle0_def INum_def) } ultimately show ?thesis by blast qed -lemma Ngt0_iff[simp]:assumes nx: "isnormNum x" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x" -proof- - have " \ a b. x = (a,b)" by simp - then obtain a b where x[simp]:"x = (a,b)" by blast - {assume "a = 0" hence ?thesis by (simp add: Ngt0_def INum_def) } +lemma Ngt0_iff[simp]: + assumes nx: "isnormNum x" + shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})> 0) = 0<\<^sub>N x" +proof - + obtain a b where x: "x = (a, b)" by (cases x) + { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) } moreover - {assume a: "a\0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def) + { assume a: "a \ 0" hence b: "(of_int b::'a) > 0" using nx + by (simp add: x isnormNum_def) from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"] - have ?thesis by (simp add: Ngt0_def INum_def)} - ultimately show ?thesis by blast -qed -lemma Nge0_iff[simp]:assumes nx: "isnormNum x" - shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \ 0) = 0\\<^sub>N x" -proof- - have " \ a b. x = (a,b)" by simp - then obtain a b where x[simp]:"x = (a,b)" by blast - {assume "a = 0" hence ?thesis by (simp add: Nge0_def INum_def) } - moreover - {assume a: "a\0" hence b: "(of_int b::'a) > 0" using nx by (simp add: isnormNum_def) - from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"] - have ?thesis by (simp add: Nge0_def INum_def)} + have ?thesis by (simp add: x Ngt0_def INum_def) } ultimately show ?thesis by blast qed -lemma Nlt_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" +lemma Nge0_iff[simp]: + assumes nx: "isnormNum x" + shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) \ 0) = 0\\<^sub>N x" +proof - + obtain a b where x: "x = (a, b)" by (cases x) + { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) } + moreover + { assume "a \ 0" hence b: "(of_int b::'a) > 0" using nx + by (simp add: x isnormNum_def) + from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"] + have ?thesis by (simp add: x Nge0_def INum_def) } + ultimately show ?thesis by blast +qed + +lemma Nlt_iff[simp]: + assumes nx: "isnormNum x" and ny: "isnormNum y" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero}) < INum y) = (x <\<^sub>N y)" -proof- +proof - let ?z = "0::'a" - have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" using nx ny by simp - also have "\ = (0>\<^sub>N (x -\<^sub>N y))" using Nlt0_iff[OF Nsub_normN[OF ny]] by simp + have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" + using nx ny by simp + also have "\ = (0>\<^sub>N (x -\<^sub>N y))" + using Nlt0_iff[OF Nsub_normN[OF ny]] by simp finally show ?thesis by (simp add: Nlt_def) qed -lemma Nle_iff[simp]: assumes nx: "isnormNum x" and ny: "isnormNum y" +lemma Nle_iff[simp]: + assumes nx: "isnormNum x" and ny: "isnormNum y" shows "((INum x :: 'a :: {field_char_0, linordered_field_inverse_zero})\ INum y) = (x \\<^sub>N y)" -proof- - have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" using nx ny by simp - also have "\ = (0\\<^sub>N (x -\<^sub>N y))" using Nle0_iff[OF Nsub_normN[OF ny]] by simp +proof - + have "((INum x ::'a) \ INum y) = (INum (x -\<^sub>N y) \ (0::'a))" + using nx ny by simp + also have "\ = (0\\<^sub>N (x -\<^sub>N y))" + using Nle0_iff[OF Nsub_normN[OF ny]] by simp finally show ?thesis by (simp add: Nle_def) qed lemma Nadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "x +\<^sub>N y = y +\<^sub>N x" -proof- +proof - have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp with isnormNum_unique[OF n] show ?thesis by simp @@ -409,7 +401,7 @@ lemma [simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "(0, b) +\<^sub>N y = normNum y" - and "(a, 0) +\<^sub>N y = normNum y" + and "(a, 0) +\<^sub>N y = normNum y" and "x +\<^sub>N (0, b) = normNum x" and "x +\<^sub>N (a, 0) = normNum x" apply (simp add: Nadd_def split_def) @@ -420,14 +412,13 @@ lemma normNum_nilpotent_aux[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - assumes nx: "isnormNum x" + assumes nx: "isnormNum x" shows "normNum x = x" -proof- +proof - let ?a = "normNum x" have n: "isnormNum ?a" by simp - have th:"INum ?a = (INum x ::'a)" by simp - with isnormNum_unique[OF n nx] - show ?thesis by simp + have th: "INum ?a = (INum x ::'a)" by simp + with isnormNum_unique[OF n nx] show ?thesis by simp qed lemma normNum_nilpotent[simp]: @@ -445,7 +436,7 @@ lemma Nadd_normNum1[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "normNum x +\<^sub>N y = x +\<^sub>N y" -proof- +proof - have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp also have "\ = INum (x +\<^sub>N y)" by simp @@ -455,7 +446,7 @@ lemma Nadd_normNum2[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "x +\<^sub>N normNum y = x +\<^sub>N y" -proof- +proof - have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp also have "\ = INum (x +\<^sub>N y)" by simp @@ -465,7 +456,7 @@ lemma Nadd_assoc: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" -proof- +proof - have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp with isnormNum_unique[OF n] show ?thesis by simp @@ -476,10 +467,10 @@ lemma Nmul_assoc: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - assumes nx: "isnormNum x" and ny:"isnormNum y" and nz:"isnormNum z" + assumes nx: "isnormNum x" and ny: "isnormNum y" and nz: "isnormNum z" shows "x *\<^sub>N y *\<^sub>N z = x *\<^sub>N (y *\<^sub>N z)" -proof- - from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" +proof - + from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))" by simp_all have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp with isnormNum_unique[OF n] show ?thesis by simp @@ -487,14 +478,15 @@ lemma Nsub0: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - assumes x: "isnormNum x" and y:"isnormNum y" shows "(x -\<^sub>N y = 0\<^sub>N) = (x = y)" -proof- - { fix h :: 'a - from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] - have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp - also have "\ = (INum x = (INum y :: 'a))" by simp - also have "\ = (x = y)" using x y by simp - finally show ?thesis . } + assumes x: "isnormNum x" and y: "isnormNum y" + shows "x -\<^sub>N y = 0\<^sub>N \ x = y" +proof - + fix h :: 'a + from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"] + have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp + also have "\ = (INum x = (INum y :: 'a))" by simp + also have "\ = (x = y)" using x y by simp + finally show ?thesis . qed lemma Nmul0[simp]: "c *\<^sub>N 0\<^sub>N = 0\<^sub>N" " 0\<^sub>N *\<^sub>N c = 0\<^sub>N" @@ -502,24 +494,26 @@ lemma Nmul_eq0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" - assumes nx:"isnormNum x" and ny: "isnormNum y" - shows "(x*\<^sub>N y = 0\<^sub>N) = (x = 0\<^sub>N \ y = 0\<^sub>N)" -proof- - { fix h :: 'a - have " \ a b a' b'. x = (a,b) \ y= (a',b')" by auto - then obtain a b a' b' where xy[simp]: "x = (a,b)" "y = (a',b')" by blast - have n0: "isnormNum 0\<^sub>N" by simp - show ?thesis using nx ny - apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric] Nmul[where ?'a = 'a]) - by (simp add: INum_def split_def isnormNum_def split: split_if_asm) - } + assumes nx: "isnormNum x" and ny: "isnormNum y" + shows "x*\<^sub>N y = 0\<^sub>N \ x = 0\<^sub>N \ y = 0\<^sub>N" +proof - + fix h :: 'a + obtain a b where x: "x = (a, b)" by (cases x) + obtain a' b' where y: "y = (a', b')" by (cases y) + have n0: "isnormNum 0\<^sub>N" by simp + show ?thesis using nx ny + apply (simp only: isnormNum_unique[where ?'a = 'a, OF Nmul_normN[OF nx ny] n0, symmetric] + Nmul[where ?'a = 'a]) + apply (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) + done qed + lemma Nneg_Nneg[simp]: "~\<^sub>N (~\<^sub>N c) = c" by (simp add: Nneg_def split_def) -lemma Nmul1[simp]: - "isnormNum c \ 1\<^sub>N *\<^sub>N c = c" - "isnormNum c \ c *\<^sub>N (1\<^sub>N) = c" +lemma Nmul1[simp]: + "isnormNum c \ 1\<^sub>N *\<^sub>N c = c" + "isnormNum c \ c *\<^sub>N (1\<^sub>N) = c" apply (simp_all add: Nmul_def Let_def split_def isnormNum_def) apply (cases "fst c = 0", simp_all, cases c, simp_all)+ done