330 qed |
330 qed |
331 thus ?thesis by (unfold Fract_def rat_of_def) |
331 thus ?thesis by (unfold Fract_def rat_of_def) |
332 qed |
332 qed |
333 |
333 |
334 theorem rat_function: |
334 theorem rat_function: |
335 "(!!q r. f q r == g (fraction_of q) (fraction_of r)) ==> |
335 assumes "!!q r. f q r == g (fraction_of q) (fraction_of r)" |
336 (!!a b a' b' c d c' d'. |
336 and "!!a b a' b' c d c' d'. |
337 \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==> |
337 \<lfloor>fract a b\<rfloor> = \<lfloor>fract a' b'\<rfloor> ==> \<lfloor>fract c d\<rfloor> = \<lfloor>fract c' d'\<rfloor> ==> |
338 b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==> |
338 b \<noteq> 0 ==> b' \<noteq> 0 ==> d \<noteq> 0 ==> d' \<noteq> 0 ==> |
339 g (fract a b) (fract c d) = g (fract a' b') (fract c' d')) ==> |
339 g (fract a b) (fract c d) = g (fract a' b') (fract c' d')" |
340 f (Fract a b) (Fract c d) = g (fract a b) (fract c d)" |
340 shows "f (Fract a b) (Fract c d) = g (fract a b) (fract c d)" |
341 proof - |
341 using prems and TrueI by (rule rat_cond_function) |
342 case rule_context from this TrueI |
|
343 show ?thesis by (rule rat_cond_function) |
|
344 qed |
|
345 |
342 |
346 |
343 |
347 subsubsection {* Standard operations on rational numbers *} |
344 subsubsection {* Standard operations on rational numbers *} |
348 |
345 |
349 instance rat :: "{zero, one, plus, minus, times, inverse, ord}" .. |
346 instance rat :: "{zero, one, plus, minus, times, inverse, ord}" .. |