14 where "0\<^sub>N \<equiv> (0, 0)" |
14 where "0\<^sub>N \<equiv> (0, 0)" |
15 |
15 |
16 abbreviation Numi_syn :: "int \<Rightarrow> Num" ("'((_)')\<^sub>N") |
16 abbreviation Numi_syn :: "int \<Rightarrow> Num" ("'((_)')\<^sub>N") |
17 where "(i)\<^sub>N \<equiv> (i, 1)" |
17 where "(i)\<^sub>N \<equiv> (i, 1)" |
18 |
18 |
19 definition isnormNum :: "Num \<Rightarrow> bool" where |
19 definition isnormNum :: "Num \<Rightarrow> bool" |
20 "isnormNum = (\<lambda>(a,b). (if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1))" |
20 where "isnormNum = (\<lambda>(a, b). if a = 0 then b = 0 else b > 0 \<and> gcd a b = 1)" |
21 |
21 |
22 definition normNum :: "Num \<Rightarrow> Num" where |
22 definition normNum :: "Num \<Rightarrow> Num" |
|
23 where |
23 "normNum = (\<lambda>(a,b). |
24 "normNum = (\<lambda>(a,b). |
24 (if a=0 \<or> b = 0 then (0,0) else |
25 (if a = 0 \<or> b = 0 then (0, 0) |
|
26 else |
25 (let g = gcd a b |
27 (let g = gcd a b |
26 in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))" |
28 in if b > 0 then (a div g, b div g) else (- (a div g), - (b div g)))))" |
27 |
29 |
28 declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger] |
30 declare gcd_dvd1_int[presburger] gcd_dvd2_int[presburger] |
29 |
31 |
30 lemma normNum_isnormNum [simp]: "isnormNum (normNum x)" |
32 lemma normNum_isnormNum [simp]: "isnormNum (normNum x)" |
31 proof - |
33 proof - |
32 obtain a b where x: "x = (a, b)" by (cases x) |
34 obtain a b where x: "x = (a, b)" by (cases x) |
33 { assume "a=0 \<or> b = 0" hence ?thesis by (simp add: x normNum_def isnormNum_def) } |
35 consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0" by blast |
34 moreover |
36 then show ?thesis |
35 { assume anz: "a \<noteq> 0" and bnz: "b \<noteq> 0" |
37 proof cases |
|
38 case 1 |
|
39 then show ?thesis |
|
40 by (simp add: x normNum_def isnormNum_def) |
|
41 next |
|
42 case 2 |
36 let ?g = "gcd a b" |
43 let ?g = "gcd a b" |
37 let ?a' = "a div ?g" |
44 let ?a' = "a div ?g" |
38 let ?b' = "b div ?g" |
45 let ?b' = "b div ?g" |
39 let ?g' = "gcd ?a' ?b'" |
46 let ?g' = "gcd ?a' ?b'" |
40 from anz bnz have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b] |
47 from 2 have "?g \<noteq> 0" by simp with gcd_ge_0_int[of a b] |
41 have gpos: "?g > 0" by arith |
48 have gpos: "?g > 0" by arith |
42 have gdvd: "?g dvd a" "?g dvd b" by arith+ |
49 have gdvd: "?g dvd a" "?g dvd b" by arith+ |
43 from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] anz bnz |
50 from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] 2 |
44 have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+ |
51 have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+ |
45 from anz bnz have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith |
52 from 2 have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith |
46 from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" . |
53 from div_gcd_coprime_int[OF stupid] have gp1: "?g' = 1" . |
47 from bnz have "b < 0 \<or> b > 0" by arith |
54 from 2 consider "b < 0" | "b > 0" by arith |
48 moreover |
55 then show ?thesis |
49 { assume b: "b > 0" |
56 proof cases |
50 from b have "?b' \<ge> 0" |
57 case 1 |
|
58 have False if b': "?b' \<ge> 0" |
|
59 proof - |
|
60 from gpos have th: "?g \<ge> 0" by arith |
|
61 from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)] |
|
62 show ?thesis using 1 by arith |
|
63 qed |
|
64 then have b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) |
|
65 from \<open>a \<noteq> 0\<close> nz' 1 b' gp1 show ?thesis |
|
66 by (simp add: x isnormNum_def normNum_def Let_def split_def) |
|
67 next |
|
68 case 2 |
|
69 then have "?b' \<ge> 0" |
51 by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos]) |
70 by (presburger add: pos_imp_zdiv_nonneg_iff[OF gpos]) |
52 with nz' have b': "?b' > 0" by arith |
71 with nz' have b': "?b' > 0" by arith |
53 from b b' anz bnz nz' gp1 have ?thesis |
72 from 2 b' \<open>a \<noteq> 0\<close> nz' gp1 show ?thesis |
54 by (simp add: x isnormNum_def normNum_def Let_def split_def) } |
73 by (simp add: x isnormNum_def normNum_def Let_def split_def) |
55 moreover { |
74 qed |
56 assume b: "b < 0" |
75 qed |
57 { assume b': "?b' \<ge> 0" |
|
58 from gpos have th: "?g \<ge> 0" by arith |
|
59 from mult_nonneg_nonneg[OF th b'] dvd_mult_div_cancel[OF gdvd(2)] |
|
60 have False using b by arith } |
|
61 hence b': "?b' < 0" by (presburger add: linorder_not_le[symmetric]) |
|
62 from anz bnz nz' b b' gp1 have ?thesis |
|
63 by (simp add: x isnormNum_def normNum_def Let_def split_def) } |
|
64 ultimately have ?thesis by blast |
|
65 } |
|
66 ultimately show ?thesis by blast |
|
67 qed |
76 qed |
68 |
77 |
69 text \<open>Arithmetic over Num\<close> |
78 text \<open>Arithmetic over Num\<close> |
70 |
79 |
71 definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60) where |
80 definition Nadd :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "+\<^sub>N" 60) |
72 "Nadd = (\<lambda>(a,b) (a',b'). if a = 0 \<or> b = 0 then normNum(a',b') |
81 where |
73 else if a'=0 \<or> b' = 0 then normNum(a,b) |
82 "Nadd = (\<lambda>(a, b) (a', b'). |
74 else normNum(a*b' + b*a', b*b'))" |
83 if a = 0 \<or> b = 0 then normNum (a', b') |
75 |
84 else if a' = 0 \<or> b' = 0 then normNum (a, b) |
76 definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60) where |
85 else normNum (a * b' + b * a', b * b'))" |
77 "Nmul = (\<lambda>(a,b) (a',b'). let g = gcd (a*a') (b*b') |
86 |
78 in (a*a' div g, b*b' div g))" |
87 definition Nmul :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "*\<^sub>N" 60) |
|
88 where |
|
89 "Nmul = (\<lambda>(a, b) (a', b'). |
|
90 let g = gcd (a * a') (b * b') |
|
91 in (a * a' div g, b * b' div g))" |
79 |
92 |
80 definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N") |
93 definition Nneg :: "Num \<Rightarrow> Num" ("~\<^sub>N") |
81 where "Nneg \<equiv> (\<lambda>(a,b). (-a,b))" |
94 where "Nneg = (\<lambda>(a, b). (- a, b))" |
82 |
95 |
83 definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60) |
96 definition Nsub :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "-\<^sub>N" 60) |
84 where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)" |
97 where "Nsub = (\<lambda>a b. a +\<^sub>N ~\<^sub>N b)" |
85 |
98 |
86 definition Ninv :: "Num \<Rightarrow> Num" |
99 definition Ninv :: "Num \<Rightarrow> Num" |
87 where "Ninv = (\<lambda>(a,b). if a < 0 then (-b, \<bar>a\<bar>) else (b,a))" |
100 where "Ninv = (\<lambda>(a, b). if a < 0 then (- b, \<bar>a\<bar>) else (b, a))" |
88 |
101 |
89 definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60) |
102 definition Ndiv :: "Num \<Rightarrow> Num \<Rightarrow> Num" (infixl "\<div>\<^sub>N" 60) |
90 where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)" |
103 where "Ndiv = (\<lambda>a b. a *\<^sub>N Ninv b)" |
91 |
104 |
92 lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)" |
105 lemma Nneg_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (~\<^sub>N x)" |
93 by (simp add: isnormNum_def Nneg_def split_def) |
106 by (simp add: isnormNum_def Nneg_def split_def) |
94 |
107 |
95 lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)" |
108 lemma Nadd_normN[simp]: "isnormNum (x +\<^sub>N y)" |
96 by (simp add: Nadd_def split_def) |
109 by (simp add: Nadd_def split_def) |
97 |
110 |
98 lemma Nsub_normN[simp]: "\<lbrakk> isnormNum y\<rbrakk> \<Longrightarrow> isnormNum (x -\<^sub>N y)" |
111 lemma Nsub_normN[simp]: "isnormNum y \<Longrightarrow> isnormNum (x -\<^sub>N y)" |
99 by (simp add: Nsub_def split_def) |
112 by (simp add: Nsub_def split_def) |
100 |
113 |
101 lemma Nmul_normN[simp]: |
114 lemma Nmul_normN[simp]: |
102 assumes xn: "isnormNum x" and yn: "isnormNum y" |
115 assumes xn: "isnormNum x" |
|
116 and yn: "isnormNum y" |
103 shows "isnormNum (x *\<^sub>N y)" |
117 shows "isnormNum (x *\<^sub>N y)" |
104 proof - |
118 proof - |
105 obtain a b where x: "x = (a, b)" by (cases x) |
119 obtain a b where x: "x = (a, b)" by (cases x) |
106 obtain a' b' where y: "y = (a', b')" by (cases y) |
120 obtain a' b' where y: "y = (a', b')" by (cases y) |
107 { assume "a = 0" |
121 consider "a = 0" | "a' = 0" | "a \<noteq> 0" "a' \<noteq> 0" by blast |
108 hence ?thesis using xn x y |
122 then show ?thesis |
109 by (simp add: isnormNum_def Let_def Nmul_def split_def) } |
123 proof cases |
110 moreover |
124 case 1 |
111 { assume "a' = 0" |
125 then show ?thesis |
112 hence ?thesis using yn x y |
126 using xn x y by (simp add: isnormNum_def Let_def Nmul_def split_def) |
113 by (simp add: isnormNum_def Let_def Nmul_def split_def) } |
127 next |
114 moreover |
128 case 2 |
115 { assume a: "a \<noteq>0" and a': "a'\<noteq>0" |
129 then show ?thesis |
116 hence bp: "b > 0" "b' > 0" using xn yn x y by (simp_all add: isnormNum_def) |
130 using yn x y by (simp add: isnormNum_def Let_def Nmul_def split_def) |
|
131 next |
|
132 case 3 |
|
133 then have bp: "b > 0" "b' > 0" |
|
134 using xn yn x y by (simp_all add: isnormNum_def) |
117 from bp have "x *\<^sub>N y = normNum (a * a', b * b')" |
135 from bp have "x *\<^sub>N y = normNum (a * a', b * b')" |
118 using x y a a' bp by (simp add: Nmul_def Let_def split_def normNum_def) |
136 using x y 3 bp by (simp add: Nmul_def Let_def split_def normNum_def) |
119 hence ?thesis by simp } |
137 then show ?thesis by simp |
120 ultimately show ?thesis by blast |
138 qed |
121 qed |
139 qed |
122 |
140 |
123 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)" |
141 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)" |
124 by (simp add: Ninv_def isnormNum_def split_def) |
142 apply (simp add: Ninv_def isnormNum_def split_def) |
125 (cases "fst x = 0", auto simp add: gcd_commute_int) |
143 apply (cases "fst x = 0") |
126 |
144 apply (auto simp add: gcd_commute_int) |
127 lemma isnormNum_int[simp]: |
145 done |
128 "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N" |
146 |
|
147 lemma isnormNum_int[simp]: "isnormNum 0\<^sub>N" "isnormNum ((1::int)\<^sub>N)" "i \<noteq> 0 \<Longrightarrow> isnormNum (i)\<^sub>N" |
129 by (simp_all add: isnormNum_def) |
148 by (simp_all add: isnormNum_def) |
130 |
149 |
131 |
150 |
132 text \<open>Relations over Num\<close> |
151 text \<open>Relations over Num\<close> |
133 |
152 |
134 definition Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N") |
153 definition Nlt0:: "Num \<Rightarrow> bool" ("0>\<^sub>N") |
135 where "Nlt0 = (\<lambda>(a,b). a < 0)" |
154 where "Nlt0 = (\<lambda>(a, b). a < 0)" |
136 |
155 |
137 definition Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N") |
156 definition Nle0:: "Num \<Rightarrow> bool" ("0\<ge>\<^sub>N") |
138 where "Nle0 = (\<lambda>(a,b). a \<le> 0)" |
157 where "Nle0 = (\<lambda>(a, b). a \<le> 0)" |
139 |
158 |
140 definition Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N") |
159 definition Ngt0:: "Num \<Rightarrow> bool" ("0<\<^sub>N") |
141 where "Ngt0 = (\<lambda>(a,b). a > 0)" |
160 where "Ngt0 = (\<lambda>(a, b). a > 0)" |
142 |
161 |
143 definition Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N") |
162 definition Nge0:: "Num \<Rightarrow> bool" ("0\<le>\<^sub>N") |
144 where "Nge0 = (\<lambda>(a,b). a \<ge> 0)" |
163 where "Nge0 = (\<lambda>(a, b). a \<ge> 0)" |
145 |
164 |
146 definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55) |
165 definition Nlt :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "<\<^sub>N" 55) |
147 where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))" |
166 where "Nlt = (\<lambda>a b. 0>\<^sub>N (a -\<^sub>N b))" |
148 |
167 |
149 definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55) |
168 definition Nle :: "Num \<Rightarrow> Num \<Rightarrow> bool" (infix "\<le>\<^sub>N" 55) |
150 where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))" |
169 where "Nle = (\<lambda>a b. 0\<ge>\<^sub>N (a -\<^sub>N b))" |
151 |
170 |
152 definition "INum = (\<lambda>(a,b). of_int a / of_int b)" |
171 definition "INum = (\<lambda>(a, b). of_int a / of_int b)" |
153 |
172 |
154 lemma INum_int [simp]: "INum (i)\<^sub>N = ((of_int i) ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" |
173 lemma INum_int [simp]: "INum (i)\<^sub>N = (of_int i ::'a::field)" "INum 0\<^sub>N = (0::'a::field)" |
155 by (simp_all add: INum_def) |
174 by (simp_all add: INum_def) |
156 |
175 |
157 lemma isnormNum_unique[simp]: |
176 lemma isnormNum_unique[simp]: |
158 assumes na: "isnormNum x" and nb: "isnormNum y" |
177 assumes na: "isnormNum x" |
159 shows "((INum x ::'a::{field_char_0, field}) = INum y) = (x = y)" (is "?lhs = ?rhs") |
178 and nb: "isnormNum y" |
|
179 shows "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> x = y" |
|
180 (is "?lhs = ?rhs") |
160 proof |
181 proof |
161 obtain a b where x: "x = (a, b)" by (cases x) |
182 obtain a b where x: "x = (a, b)" by (cases x) |
162 obtain a' b' where y: "y = (a', b')" by (cases y) |
183 obtain a' b' where y: "y = (a', b')" by (cases y) |
163 assume H: ?lhs |
184 consider "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" | "a \<noteq> 0" "b \<noteq> 0" "a' \<noteq> 0" "b' \<noteq> 0" |
164 { assume "a = 0 \<or> b = 0 \<or> a' = 0 \<or> b' = 0" |
185 by blast |
165 hence ?rhs using na nb H |
186 then show ?rhs if H: ?lhs |
166 by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) } |
187 proof cases |
167 moreover |
188 case 1 |
168 { assume az: "a \<noteq> 0" and bz: "b \<noteq> 0" and a'z: "a'\<noteq>0" and b'z: "b'\<noteq>0" |
189 then show ?thesis |
169 from az bz a'z b'z na nb have pos: "b > 0" "b' > 0" by (simp_all add: x y isnormNum_def) |
190 using na nb H by (simp add: x y INum_def split_def isnormNum_def split: split_if_asm) |
170 from H bz b'z have eq: "a * b' = a'*b" |
191 next |
|
192 case 2 |
|
193 with na nb have pos: "b > 0" "b' > 0" |
|
194 by (simp_all add: x y isnormNum_def) |
|
195 from H \<open>b \<noteq> 0\<close> \<open>b' \<noteq> 0\<close> have eq: "a * b' = a'*b" |
171 by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult) |
196 by (simp add: x y INum_def eq_divide_eq divide_eq_eq of_int_mult[symmetric] del: of_int_mult) |
172 from az a'z na nb have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1" |
197 from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb |
|
198 have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1" |
173 by (simp_all add: x y isnormNum_def add: gcd_commute_int) |
199 by (simp_all add: x y isnormNum_def add: gcd_commute_int) |
174 from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'" |
200 from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'" |
175 apply - |
201 apply - |
176 apply algebra |
202 apply algebra |
177 apply algebra |
203 apply algebra |
180 done |
206 done |
181 from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)] |
207 from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)] |
182 coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]] |
208 coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]] |
183 have eq1: "b = b'" using pos by arith |
209 have eq1: "b = b'" using pos by arith |
184 with eq have "a = a'" using pos by simp |
210 with eq have "a = a'" using pos by simp |
185 with eq1 have ?rhs by (simp add: x y) } |
211 with eq1 show ?thesis by (simp add: x y) |
186 ultimately show ?rhs by blast |
212 qed |
187 next |
213 show ?lhs if ?rhs |
188 assume ?rhs thus ?lhs by simp |
214 using that by simp |
189 qed |
215 qed |
190 |
216 |
191 |
217 lemma isnormNum0[simp]: "isnormNum x \<Longrightarrow> INum x = (0::'a::{field_char_0,field}) \<longleftrightarrow> x = 0\<^sub>N" |
192 lemma isnormNum0[simp]: |
|
193 "isnormNum x \<Longrightarrow> (INum x = (0::'a::{field_char_0, field})) = (x = 0\<^sub>N)" |
|
194 unfolding INum_int(2)[symmetric] |
218 unfolding INum_int(2)[symmetric] |
195 by (rule isnormNum_unique) simp_all |
219 by (rule isnormNum_unique) simp_all |
196 |
220 |
197 lemma of_int_div_aux: "d ~= 0 ==> ((of_int x)::'a::field_char_0) / (of_int d) = |
221 lemma of_int_div_aux: |
198 of_int (x div d) + (of_int (x mod d)) / ((of_int d)::'a)" |
222 assumes "d \<noteq> 0" |
199 proof - |
223 shows "(of_int x ::'a::field_char_0) / of_int d = |
200 assume "d ~= 0" |
224 of_int (x div d) + (of_int (x mod d)) / of_int d" |
201 let ?t = "of_int (x div d) * ((of_int d)::'a) + of_int(x mod d)" |
225 proof - |
|
226 let ?t = "of_int (x div d) * (of_int d ::'a) + of_int (x mod d)" |
202 let ?f = "\<lambda>x. x / of_int d" |
227 let ?f = "\<lambda>x. x / of_int d" |
203 have "x = (x div d) * d + x mod d" |
228 have "x = (x div d) * d + x mod d" |
204 by auto |
229 by auto |
205 then have eq: "of_int x = ?t" |
230 then have eq: "of_int x = ?t" |
206 by (simp only: of_int_mult[symmetric] of_int_add [symmetric]) |
231 by (simp only: of_int_mult[symmetric] of_int_add [symmetric]) |
207 then have "of_int x / of_int d = ?t / of_int d" |
232 then have "of_int x / of_int d = ?t / of_int d" |
208 using cong[OF refl[of ?f] eq] by simp |
233 using cong[OF refl[of ?f] eq] by simp |
209 then show ?thesis by (simp add: add_divide_distrib algebra_simps \<open>d ~= 0\<close>) |
234 then show ?thesis |
210 qed |
235 by (simp add: add_divide_distrib algebra_simps \<open>d \<noteq> 0\<close>) |
211 |
236 qed |
212 lemma of_int_div: "(d::int) ~= 0 ==> d dvd n ==> |
237 |
213 (of_int(n div d)::'a::field_char_0) = of_int n / of_int d" |
238 lemma of_int_div: |
214 using of_int_div_aux [of d n, where ?'a = 'a] by simp |
239 fixes d :: int |
215 |
240 assumes "d \<noteq> 0" "d dvd n" |
216 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0, field})" |
241 shows "(of_int (n div d) ::'a::field_char_0) = of_int n / of_int d" |
217 proof - |
242 using assms of_int_div_aux [of d n, where ?'a = 'a] by simp |
218 obtain a b where x: "x = (a, b)" by (cases x) |
243 |
219 { assume "a = 0 \<or> b = 0" |
244 lemma normNum[simp]: "INum (normNum x) = (INum x :: 'a::{field_char_0,field})" |
220 hence ?thesis by (simp add: x INum_def normNum_def split_def Let_def) } |
245 proof - |
221 moreover |
246 obtain a b where x: "x = (a, b)" by (cases x) |
222 { assume a: "a \<noteq> 0" and b: "b \<noteq> 0" |
247 consider "a = 0 \<or> b = 0" | "a \<noteq> 0" "b \<noteq> 0" by blast |
|
248 then show ?thesis |
|
249 proof cases |
|
250 case 1 |
|
251 then show ?thesis |
|
252 by (simp add: x INum_def normNum_def split_def Let_def) |
|
253 next |
|
254 case 2 |
223 let ?g = "gcd a b" |
255 let ?g = "gcd a b" |
224 from a b have g: "?g \<noteq> 0"by simp |
256 from 2 have g: "?g \<noteq> 0"by simp |
225 from of_int_div[OF g, where ?'a = 'a] |
257 from of_int_div[OF g, where ?'a = 'a] show ?thesis |
226 have ?thesis by (auto simp add: x INum_def normNum_def split_def Let_def) } |
258 by (auto simp add: x INum_def normNum_def split_def Let_def) |
227 ultimately show ?thesis by blast |
259 qed |
228 qed |
260 qed |
229 |
261 |
230 lemma INum_normNum_iff: |
262 lemma INum_normNum_iff: "(INum x ::'a::{field_char_0,field}) = INum y \<longleftrightarrow> normNum x = normNum y" |
231 "(INum x ::'a::{field_char_0, field}) = INum y \<longleftrightarrow> normNum x = normNum y" |
263 (is "?lhs \<longleftrightarrow> _") |
232 (is "?lhs = ?rhs") |
|
233 proof - |
264 proof - |
234 have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)" |
265 have "normNum x = normNum y \<longleftrightarrow> (INum (normNum x) :: 'a) = INum (normNum y)" |
235 by (simp del: normNum) |
266 by (simp del: normNum) |
236 also have "\<dots> = ?lhs" by simp |
267 also have "\<dots> = ?lhs" by simp |
237 finally show ?thesis by simp |
268 finally show ?thesis by simp |
238 qed |
269 qed |
239 |
270 |
240 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0, field})" |
271 lemma Nadd[simp]: "INum (x +\<^sub>N y) = INum x + (INum y :: 'a :: {field_char_0,field})" |
241 proof - |
272 proof - |
242 let ?z = "0:: 'a" |
273 let ?z = "0::'a" |
243 obtain a b where x: "x = (a, b)" by (cases x) |
274 obtain a b where x: "x = (a, b)" by (cases x) |
244 obtain a' b' where y: "y = (a', b')" by (cases y) |
275 obtain a' b' where y: "y = (a', b')" by (cases y) |
245 { assume "a=0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" |
276 consider "a = 0 \<or> a'= 0 \<or> b =0 \<or> b' = 0" | "a \<noteq> 0" "a'\<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0" |
246 hence ?thesis |
277 by blast |
247 apply (cases "a=0", simp_all add: x y Nadd_def) |
278 then show ?thesis |
248 apply (cases "b= 0", simp_all add: INum_def) |
279 proof cases |
249 apply (cases "a'= 0", simp_all) |
280 case 1 |
250 apply (cases "b'= 0", simp_all) |
281 then show ?thesis |
251 done } |
282 apply (cases "a = 0") |
252 moreover |
283 apply (simp_all add: x y Nadd_def) |
253 { assume aa': "a \<noteq> 0" "a'\<noteq> 0" and bb': "b \<noteq> 0" "b' \<noteq> 0" |
284 apply (cases "b = 0") |
254 { assume z: "a * b' + b * a' = 0" |
285 apply (simp_all add: INum_def) |
255 hence "of_int (a*b' + b*a') / (of_int b* of_int b') = ?z" by simp |
286 apply (cases "a'= 0") |
256 hence "of_int b' * of_int a / (of_int b * of_int b') + |
287 apply simp_all |
|
288 apply (cases "b'= 0") |
|
289 apply simp_all |
|
290 done |
|
291 next |
|
292 case 2 |
|
293 show ?thesis |
|
294 proof (cases "a * b' + b * a' = 0") |
|
295 case True |
|
296 then have "of_int (a * b' + b * a') / (of_int b * of_int b') = ?z" |
|
297 by simp |
|
298 then have "of_int b' * of_int a / (of_int b * of_int b') + |
257 of_int b * of_int a' / (of_int b * of_int b') = ?z" |
299 of_int b * of_int a' / (of_int b * of_int b') = ?z" |
258 by (simp add:add_divide_distrib) |
300 by (simp add: add_divide_distrib) |
259 hence th: "of_int a / of_int b + of_int a' / of_int b' = ?z" using bb' aa' |
301 then have th: "of_int a / of_int b + of_int a' / of_int b' = ?z" |
260 by simp |
302 using 2 by simp |
261 from z aa' bb' have ?thesis |
303 from True 2 show ?thesis |
262 by (simp add: x y th Nadd_def normNum_def INum_def split_def) } |
304 by (simp add: x y th Nadd_def normNum_def INum_def split_def) |
263 moreover { |
305 next |
264 assume z: "a * b' + b * a' \<noteq> 0" |
306 case False |
265 let ?g = "gcd (a * b' + b * a') (b * b')" |
307 let ?g = "gcd (a * b' + b * a') (b * b')" |
266 have gz: "?g \<noteq> 0" using z by simp |
308 have gz: "?g \<noteq> 0" |
267 have ?thesis using aa' bb' z gz |
309 using False by simp |
268 of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * b' + b * a'" "b * b'"]] |
310 show ?thesis |
269 of_int_div [where ?'a = 'a, OF gz gcd_dvd2 [of "a * b' + b * a'" "b * b'"]] |
311 using 2 False gz |
|
312 of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * b' + b * a'" "b * b'"]] |
|
313 of_int_div [where ?'a = 'a, OF gz gcd_dvd2 [of "a * b' + b * a'" "b * b'"]] |
270 by (simp add: x y Nadd_def INum_def normNum_def Let_def) (simp add: field_simps) |
314 by (simp add: x y Nadd_def INum_def normNum_def Let_def) (simp add: field_simps) |
271 } |
315 qed |
272 ultimately have ?thesis using aa' bb' |
316 qed |
273 by (simp add: x y Nadd_def INum_def normNum_def Let_def) } |
317 qed |
274 ultimately show ?thesis by blast |
318 |
275 qed |
319 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a::{field_char_0,field})" |
276 |
|
277 lemma Nmul[simp]: "INum (x *\<^sub>N y) = INum x * (INum y:: 'a :: {field_char_0, field})" |
|
278 proof - |
320 proof - |
279 let ?z = "0::'a" |
321 let ?z = "0::'a" |
280 obtain a b where x: "x = (a, b)" by (cases x) |
322 obtain a b where x: "x = (a, b)" by (cases x) |
281 obtain a' b' where y: "y = (a', b')" by (cases y) |
323 obtain a' b' where y: "y = (a', b')" by (cases y) |
282 { assume "a=0 \<or> a'= 0 \<or> b = 0 \<or> b' = 0" |
324 consider "a = 0 \<or> a' = 0 \<or> b = 0 \<or> b' = 0" | "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0" |
283 hence ?thesis |
325 by blast |
284 apply (cases "a=0", simp_all add: x y Nmul_def INum_def Let_def) |
326 then show ?thesis |
285 apply (cases "b=0", simp_all) |
327 proof cases |
286 apply (cases "a'=0", simp_all) |
328 case 1 |
287 done } |
329 then show ?thesis |
288 moreover |
330 apply (cases "a = 0") |
289 { assume z: "a \<noteq> 0" "a' \<noteq> 0" "b \<noteq> 0" "b' \<noteq> 0" |
331 apply (simp_all add: x y Nmul_def INum_def Let_def) |
290 let ?g="gcd (a*a') (b*b')" |
332 apply (cases "b = 0") |
291 have gz: "?g \<noteq> 0" using z by simp |
333 apply simp_all |
292 from z of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * a'" "b * b'"]] |
334 apply (cases "a' = 0") |
|
335 apply simp_all |
|
336 done |
|
337 next |
|
338 case 2 |
|
339 let ?g = "gcd (a * a') (b * b')" |
|
340 have gz: "?g \<noteq> 0" |
|
341 using 2 by simp |
|
342 from 2 of_int_div [where ?'a = 'a, OF gz gcd_dvd1 [of "a * a'" "b * b'"]] |
293 of_int_div [where ?'a = 'a , OF gz gcd_dvd2 [of "a * a'" "b * b'"]] |
343 of_int_div [where ?'a = 'a , OF gz gcd_dvd2 [of "a * a'" "b * b'"]] |
294 have ?thesis by (simp add: Nmul_def x y Let_def INum_def) } |
344 show ?thesis |
295 ultimately show ?thesis by blast |
345 by (simp add: Nmul_def x y Let_def INum_def) |
296 qed |
346 qed |
297 |
347 qed |
298 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a:: field)" |
348 |
|
349 lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a::field)" |
299 by (simp add: Nneg_def split_def INum_def) |
350 by (simp add: Nneg_def split_def INum_def) |
300 |
351 |
301 lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0, field})" |
352 lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0,field})" |
302 by (simp add: Nsub_def split_def) |
353 by (simp add: Nsub_def split_def) |
303 |
354 |
304 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)" |
355 lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)" |
305 by (simp add: Ninv_def INum_def split_def) |
356 by (simp add: Ninv_def INum_def split_def) |
306 |
357 |
307 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0, field})" |
358 lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0,field})" |
308 by (simp add: Ndiv_def) |
359 by (simp add: Ndiv_def) |
309 |
360 |
310 lemma Nlt0_iff[simp]: |
361 lemma Nlt0_iff[simp]: |
311 assumes nx: "isnormNum x" |
362 assumes nx: "isnormNum x" |
312 shows "((INum x :: 'a :: {field_char_0, linordered_field})< 0) = 0>\<^sub>N x" |
363 shows "((INum x :: 'a::{field_char_0,linordered_field})< 0) = 0>\<^sub>N x" |
313 proof - |
364 proof - |
314 obtain a b where x: "x = (a, b)" by (cases x) |
365 obtain a b where x: "x = (a, b)" by (cases x) |
315 { assume "a = 0" hence ?thesis by (simp add: x Nlt0_def INum_def) } |
366 show ?thesis |
316 moreover |
367 proof (cases "a = 0") |
317 { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" |
368 case True |
|
369 then show ?thesis |
|
370 by (simp add: x Nlt0_def INum_def) |
|
371 next |
|
372 case False |
|
373 then have b: "(of_int b::'a) > 0" |
318 using nx by (simp add: x isnormNum_def) |
374 using nx by (simp add: x isnormNum_def) |
319 from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"] |
375 from pos_divide_less_eq[OF b, where b="of_int a" and a="0::'a"] |
320 have ?thesis by (simp add: x Nlt0_def INum_def) } |
376 show ?thesis |
321 ultimately show ?thesis by blast |
377 by (simp add: x Nlt0_def INum_def) |
|
378 qed |
322 qed |
379 qed |
323 |
380 |
324 lemma Nle0_iff[simp]: |
381 lemma Nle0_iff[simp]: |
325 assumes nx: "isnormNum x" |
382 assumes nx: "isnormNum x" |
326 shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x" |
383 shows "((INum x :: 'a::{field_char_0,linordered_field}) \<le> 0) = 0\<ge>\<^sub>N x" |
327 proof - |
384 proof - |
328 obtain a b where x: "x = (a, b)" by (cases x) |
385 obtain a b where x: "x = (a, b)" by (cases x) |
329 { assume "a = 0" hence ?thesis by (simp add: x Nle0_def INum_def) } |
386 show ?thesis |
330 moreover |
387 proof (cases "a = 0") |
331 { assume a: "a \<noteq> 0" hence b: "(of_int b :: 'a) > 0" |
388 case True |
|
389 then show ?thesis |
|
390 by (simp add: x Nle0_def INum_def) |
|
391 next |
|
392 case False |
|
393 then have b: "(of_int b :: 'a) > 0" |
332 using nx by (simp add: x isnormNum_def) |
394 using nx by (simp add: x isnormNum_def) |
333 from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"] |
395 from pos_divide_le_eq[OF b, where b="of_int a" and a="0::'a"] |
334 have ?thesis by (simp add: x Nle0_def INum_def) } |
396 show ?thesis |
335 ultimately show ?thesis by blast |
397 by (simp add: x Nle0_def INum_def) |
|
398 qed |
336 qed |
399 qed |
337 |
400 |
338 lemma Ngt0_iff[simp]: |
401 lemma Ngt0_iff[simp]: |
339 assumes nx: "isnormNum x" |
402 assumes nx: "isnormNum x" |
340 shows "((INum x :: 'a :: {field_char_0, linordered_field})> 0) = 0<\<^sub>N x" |
403 shows "((INum x :: 'a::{field_char_0,linordered_field})> 0) = 0<\<^sub>N x" |
341 proof - |
404 proof - |
342 obtain a b where x: "x = (a, b)" by (cases x) |
405 obtain a b where x: "x = (a, b)" by (cases x) |
343 { assume "a = 0" hence ?thesis by (simp add: x Ngt0_def INum_def) } |
406 show ?thesis |
344 moreover |
407 proof (cases "a = 0") |
345 { assume a: "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx |
408 case True |
346 by (simp add: x isnormNum_def) |
409 then show ?thesis |
|
410 by (simp add: x Ngt0_def INum_def) |
|
411 next |
|
412 case False |
|
413 then have b: "(of_int b::'a) > 0" |
|
414 using nx by (simp add: x isnormNum_def) |
347 from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"] |
415 from pos_less_divide_eq[OF b, where b="of_int a" and a="0::'a"] |
348 have ?thesis by (simp add: x Ngt0_def INum_def) } |
416 show ?thesis |
349 ultimately show ?thesis by blast |
417 by (simp add: x Ngt0_def INum_def) |
|
418 qed |
350 qed |
419 qed |
351 |
420 |
352 lemma Nge0_iff[simp]: |
421 lemma Nge0_iff[simp]: |
353 assumes nx: "isnormNum x" |
422 assumes nx: "isnormNum x" |
354 shows "((INum x :: 'a :: {field_char_0, linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x" |
423 shows "((INum x :: 'a::{field_char_0,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x" |
355 proof - |
424 proof - |
356 obtain a b where x: "x = (a, b)" by (cases x) |
425 obtain a b where x: "x = (a, b)" by (cases x) |
357 { assume "a = 0" hence ?thesis by (simp add: x Nge0_def INum_def) } |
426 show ?thesis |
358 moreover |
427 proof (cases "a = 0") |
359 { assume "a \<noteq> 0" hence b: "(of_int b::'a) > 0" using nx |
428 case True |
360 by (simp add: x isnormNum_def) |
429 then show ?thesis |
|
430 by (simp add: x Nge0_def INum_def) |
|
431 next |
|
432 case False |
|
433 then have b: "(of_int b::'a) > 0" |
|
434 using nx by (simp add: x isnormNum_def) |
361 from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"] |
435 from pos_le_divide_eq[OF b, where b="of_int a" and a="0::'a"] |
362 have ?thesis by (simp add: x Nge0_def INum_def) } |
436 show ?thesis |
363 ultimately show ?thesis by blast |
437 by (simp add: x Nge0_def INum_def) |
|
438 qed |
364 qed |
439 qed |
365 |
440 |
366 lemma Nlt_iff[simp]: |
441 lemma Nlt_iff[simp]: |
367 assumes nx: "isnormNum x" and ny: "isnormNum y" |
442 assumes nx: "isnormNum x" |
368 shows "((INum x :: 'a :: {field_char_0, linordered_field}) < INum y) = (x <\<^sub>N y)" |
443 and ny: "isnormNum y" |
|
444 shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) = (x <\<^sub>N y)" |
369 proof - |
445 proof - |
370 let ?z = "0::'a" |
446 let ?z = "0::'a" |
371 have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" |
447 have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)" |
372 using nx ny by simp |
448 using nx ny by simp |
373 also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" |
449 also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))" |
374 using Nlt0_iff[OF Nsub_normN[OF ny]] by simp |
450 using Nlt0_iff[OF Nsub_normN[OF ny]] by simp |
375 finally show ?thesis by (simp add: Nlt_def) |
451 finally show ?thesis |
|
452 by (simp add: Nlt_def) |
376 qed |
453 qed |
377 |
454 |
378 lemma Nle_iff[simp]: |
455 lemma Nle_iff[simp]: |
379 assumes nx: "isnormNum x" and ny: "isnormNum y" |
456 assumes nx: "isnormNum x" |
380 shows "((INum x :: 'a :: {field_char_0, linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)" |
457 and ny: "isnormNum y" |
|
458 shows "((INum x :: 'a::{field_char_0,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)" |
381 proof - |
459 proof - |
382 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" |
460 have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))" |
383 using nx ny by simp |
461 using nx ny by simp |
384 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" |
462 also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))" |
385 using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
463 using Nle0_iff[OF Nsub_normN[OF ny]] by simp |
386 finally show ?thesis by (simp add: Nle_def) |
464 finally show ?thesis |
|
465 by (simp add: Nle_def) |
387 qed |
466 qed |
388 |
467 |
389 lemma Nadd_commute: |
468 lemma Nadd_commute: |
390 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
469 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
391 shows "x +\<^sub>N y = y +\<^sub>N x" |
470 shows "x +\<^sub>N y = y +\<^sub>N x" |
392 proof - |
471 proof - |
393 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" by simp_all |
472 have n: "isnormNum (x +\<^sub>N y)" "isnormNum (y +\<^sub>N x)" |
394 have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" by simp |
473 by simp_all |
395 with isnormNum_unique[OF n] show ?thesis by simp |
474 have "(INum (x +\<^sub>N y)::'a) = INum (y +\<^sub>N x)" |
|
475 by simp |
|
476 with isnormNum_unique[OF n] show ?thesis |
|
477 by simp |
396 qed |
478 qed |
397 |
479 |
398 lemma [simp]: |
480 lemma [simp]: |
399 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
481 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
400 shows "(0, b) +\<^sub>N y = normNum y" |
482 shows "(0, b) +\<^sub>N y = normNum y" |
401 and "(a, 0) +\<^sub>N y = normNum y" |
483 and "(a, 0) +\<^sub>N y = normNum y" |
402 and "x +\<^sub>N (0, b) = normNum x" |
484 and "x +\<^sub>N (0, b) = normNum x" |
403 and "x +\<^sub>N (a, 0) = normNum x" |
485 and "x +\<^sub>N (a, 0) = normNum x" |
404 apply (simp add: Nadd_def split_def) |
486 apply (simp add: Nadd_def split_def) |
405 apply (simp add: Nadd_def split_def) |
487 apply (simp add: Nadd_def split_def) |
406 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
488 apply (subst Nadd_commute) |
407 apply (subst Nadd_commute, simp add: Nadd_def split_def) |
489 apply (simp add: Nadd_def split_def) |
|
490 apply (subst Nadd_commute) |
|
491 apply (simp add: Nadd_def split_def) |
408 done |
492 done |
409 |
493 |
410 lemma normNum_nilpotent_aux[simp]: |
494 lemma normNum_nilpotent_aux[simp]: |
411 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
495 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
412 assumes nx: "isnormNum x" |
496 assumes nx: "isnormNum x" |
413 shows "normNum x = x" |
497 shows "normNum x = x" |
414 proof - |
498 proof - |
415 let ?a = "normNum x" |
499 let ?a = "normNum x" |
416 have n: "isnormNum ?a" by simp |
500 have n: "isnormNum ?a" by simp |
417 have th: "INum ?a = (INum x ::'a)" by simp |
501 have th: "INum ?a = (INum x ::'a)" by simp |
418 with isnormNum_unique[OF n nx] show ?thesis by simp |
502 with isnormNum_unique[OF n nx] show ?thesis by simp |
419 qed |
503 qed |
420 |
504 |
421 lemma normNum_nilpotent[simp]: |
505 lemma normNum_nilpotent[simp]: |
422 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
506 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
423 shows "normNum (normNum x) = normNum x" |
507 shows "normNum (normNum x) = normNum x" |
424 by simp |
508 by simp |
425 |
509 |
426 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
510 lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N" |
427 by (simp_all add: normNum_def) |
511 by (simp_all add: normNum_def) |
428 |
512 |
429 lemma normNum_Nadd: |
513 lemma normNum_Nadd: |
430 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
514 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
431 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" by simp |
515 shows "normNum (x +\<^sub>N y) = x +\<^sub>N y" |
|
516 by simp |
432 |
517 |
433 lemma Nadd_normNum1[simp]: |
518 lemma Nadd_normNum1[simp]: |
434 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
519 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
435 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
520 shows "normNum x +\<^sub>N y = x +\<^sub>N y" |
436 proof - |
521 proof - |
437 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
522 have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all |
438 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
523 have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp |
439 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
524 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
440 finally show ?thesis using isnormNum_unique[OF n] by simp |
525 finally show ?thesis using isnormNum_unique[OF n] by simp |
441 qed |
526 qed |
442 |
527 |
443 lemma Nadd_normNum2[simp]: |
528 lemma Nadd_normNum2[simp]: |
444 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
529 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
445 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
530 shows "x +\<^sub>N normNum y = x +\<^sub>N y" |
446 proof - |
531 proof - |
447 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
532 have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all |
448 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
533 have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp |
449 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
534 also have "\<dots> = INum (x +\<^sub>N y)" by simp |
450 finally show ?thesis using isnormNum_unique[OF n] by simp |
535 finally show ?thesis using isnormNum_unique[OF n] by simp |
451 qed |
536 qed |
452 |
537 |
453 lemma Nadd_assoc: |
538 lemma Nadd_assoc: |
454 assumes "SORT_CONSTRAINT('a::{field_char_0, field})" |
539 assumes "SORT_CONSTRAINT('a::{field_char_0,field})" |
455 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
540 shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)" |
456 proof - |
541 proof - |
457 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
542 have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all |
458 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
543 have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp |
459 with isnormNum_unique[OF n] show ?thesis by simp |
544 with isnormNum_unique[OF n] show ?thesis by simp |