22 |
22 |
23 axioms |
23 axioms |
24 (* FIXME also in Poly.thy def. --> FIXED*) |
24 (* FIXME also in Poly.thy def. --> FIXED*) |
25 (*real_diff_minus |
25 (*real_diff_minus |
26 "a - b = a + (-1) * b"*) |
26 "a - b = a + (-1) * b"*) |
27 real_rat_mult_1 |
27 real_rat_mult_1: "a*(b/c) = (a*b)/c" |
28 "a*(b/c) = (a*b)/c" |
28 real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" |
29 real_rat_mult_2 |
29 real_rat_mult_3: "(a/b)*c = (a*c)/b" |
30 "(a/b)*(c/d) = (a*c)/(b*d)" |
30 real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" |
31 real_rat_mult_3 |
31 |
32 "(a/b)*c = (a*c)/b" |
32 rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" |
33 real_rat_pow |
33 rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==> |
34 "(a/b)^^^2 = a^^^2/b^^^2" |
34 ((a/b) / (c/d) = (a*d) / (b*c))" |
35 |
35 rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" |
36 rat_double_rat_1 |
|
37 "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" |
|
38 rat_double_rat_2 |
|
39 "[|Not(b=0);Not(c=0); Not(d=0)|] ==> ((a/b) / (c/d) = (a*d) / (b*c))" |
|
40 rat_double_rat_3 |
|
41 "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" |
|
42 |
36 |
43 (* equation to same denominator *) |
37 (* equation to same denominator *) |
44 rat_mult_denominator_both |
38 rat_mult_denominator_both: |
45 "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" |
39 "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" |
46 rat_mult_denominator_left |
40 rat_mult_denominator_left: |
47 "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" |
41 "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" |
48 rat_mult_denominator_right |
42 rat_mult_denominator_right: |
49 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)" |
43 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)" |
50 |
44 |
51 ML {* |
45 ML {* |
52 val thy = @{theory}; |
46 val thy = @{theory}; |
53 |
47 |