neuper@37906
|
1 |
(* WN.020812: theorems in the Reals,
|
neuper@37906
|
2 |
necessary for special rule sets, in addition to Isabelle2002.
|
neuper@37906
|
3 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@37906
|
4 |
!!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
|
neuper@37906
|
5 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@37906
|
6 |
xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
|
neuper@37906
|
7 |
changed by: Richard Lang 020912
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
(*
|
neuper@37906
|
11 |
use_thy"IsacKnowledge/Poly";
|
neuper@37906
|
12 |
use_thy"Poly";
|
neuper@37906
|
13 |
use_thy_only"IsacKnowledge/Poly";
|
neuper@37906
|
14 |
|
neuper@37906
|
15 |
remove_thy"Poly";
|
neuper@37906
|
16 |
use_thy"IsacKnowledge/Isac";
|
neuper@37906
|
17 |
|
neuper@37906
|
18 |
|
neuper@37906
|
19 |
use"ROOT.ML";
|
neuper@37906
|
20 |
cd"IsacKnowledge";
|
neuper@37906
|
21 |
*)
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
Poly = Simplify +
|
neuper@37906
|
24 |
|
neuper@37906
|
25 |
(*-------------------- consts-----------------------------------------------*)
|
neuper@37906
|
26 |
consts
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
|
neuper@37906
|
29 |
is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
|
neuper@37906
|
30 |
has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
|
neuper@37906
|
31 |
is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
|
neuper@37906
|
32 |
|
neuper@37906
|
33 |
is'_multUnordered :: "real => bool" ("_ is'_multUnordered")
|
neuper@37906
|
34 |
is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
|
neuper@37906
|
35 |
is'_polyexp :: "real => bool" ("_ is'_polyexp")
|
neuper@37906
|
36 |
|
neuper@37906
|
37 |
Expand'_binoms
|
neuper@37906
|
38 |
:: "['y, \
|
neuper@37906
|
39 |
\ 'y] => 'y"
|
neuper@37906
|
40 |
("((Script Expand'_binoms (_ =))// \
|
neuper@37906
|
41 |
\ (_))" 9)
|
neuper@37906
|
42 |
|
neuper@37906
|
43 |
(*-------------------- rules------------------------------------------------*)
|
neuper@37906
|
44 |
rules (*.not contained in Isabelle2002,
|
neuper@37906
|
45 |
stated as axioms, TODO: prove as theorems;
|
neuper@37906
|
46 |
theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
|
neuper@37906
|
47 |
|
neuper@37906
|
48 |
realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
|
neuper@37906
|
49 |
realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
|
neuper@37906
|
50 |
realpow_addI_assoc_l "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
|
neuper@37906
|
51 |
realpow_addI_assoc_r "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
|
neuper@37906
|
52 |
|
neuper@37906
|
53 |
realpow_oneI "r ^^^ 1 = r"
|
neuper@37906
|
54 |
realpow_zeroI "r ^^^ 0 = 1"
|
neuper@37906
|
55 |
realpow_eq_oneI "1 ^^^ n = 1"
|
neuper@37906
|
56 |
realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
|
neuper@37906
|
57 |
realpow_multI_poly "[| r is_polyexp; s is_polyexp |] ==> \
|
neuper@37906
|
58 |
\(r * s) ^^^ n = r ^^^ n * s ^^^ n"
|
neuper@37906
|
59 |
realpow_minus_oneI "-1 ^^^ (2 * n) = 1"
|
neuper@37906
|
60 |
|
neuper@37906
|
61 |
realpow_twoI "r ^^^ 2 = r * r"
|
neuper@37906
|
62 |
realpow_twoI_assoc_l "r * (r * s) = r ^^^ 2 * s"
|
neuper@37906
|
63 |
realpow_twoI_assoc_r "s * r * r = s * r ^^^ 2"
|
neuper@37906
|
64 |
realpow_two_atom "r is_atom ==> r * r = r ^^^ 2"
|
neuper@37906
|
65 |
realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)"
|
neuper@37906
|
66 |
realpow_plus_1_assoc_l "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
|
neuper@37906
|
67 |
realpow_plus_1_assoc_l2 "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
|
neuper@37906
|
68 |
realpow_plus_1_assoc_r "s * r * r ^^^ m = s * r ^^^ (1 + m)"
|
neuper@37906
|
69 |
realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
|
neuper@37906
|
70 |
realpow_def_atom "[| Not (r is_atom); 1 < n |] \
|
neuper@37906
|
71 |
\ ==> r ^^^ n = r * r ^^^ (n + -1)"
|
neuper@37906
|
72 |
realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
|
neuper@37906
|
73 |
|
neuper@37906
|
74 |
|
neuper@37906
|
75 |
realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n"
|
neuper@37906
|
76 |
realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
|
neuper@37906
|
77 |
|
neuper@37906
|
78 |
|
neuper@37906
|
79 |
(* RL 020914 *)
|
neuper@37906
|
80 |
real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
|
neuper@37906
|
81 |
real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
|
neuper@37906
|
82 |
real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
|
neuper@37906
|
83 |
real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
|
neuper@37906
|
84 |
real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
|
neuper@37906
|
85 |
real_plus_binom_pow3_poly "[| a is_polyexp; b is_polyexp |] ==> \
|
neuper@37906
|
86 |
\(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
|
neuper@37906
|
87 |
real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
|
neuper@37906
|
88 |
real_minus_binom_pow3_p "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 + -1*b^^^3"
|
neuper@37906
|
89 |
(* real_plus_binom_pow "[| n is_const; 3 < n |] ==> \
|
neuper@37906
|
90 |
\(a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
|
neuper@37906
|
91 |
real_plus_binom_pow4 "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)"
|
neuper@37906
|
92 |
real_plus_binom_pow4_poly "[| a is_polyexp; b is_polyexp |] ==> \
|
neuper@37906
|
93 |
\(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a + b)"
|
neuper@37906
|
94 |
real_plus_binom_pow5 "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
|
neuper@37906
|
95 |
|
neuper@37906
|
96 |
real_plus_binom_pow5_poly "[| a is_polyexp; b is_polyexp |] ==> \
|
neuper@37906
|
97 |
\(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
|
neuper@37906
|
98 |
|
neuper@37906
|
99 |
real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*)
|
neuper@37906
|
100 |
real_diff_minus "a - b = a + -1 * b"
|
neuper@37906
|
101 |
real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
|
neuper@37906
|
102 |
real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
|
neuper@37906
|
103 |
(*WN071229 changed for Schaerding -----vvv*)
|
neuper@37906
|
104 |
(*real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
|
neuper@37906
|
105 |
real_plus_binom_pow2 "(a + b)^^^2 = (a + b) * (a + b)"
|
neuper@37906
|
106 |
(*WN071229 changed for Schaerding -----^^^*)
|
neuper@37906
|
107 |
real_plus_binom_pow2_poly "[| a is_polyexp; b is_polyexp |] ==> \
|
neuper@37906
|
108 |
\(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
|
neuper@37906
|
109 |
real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
|
neuper@37906
|
110 |
real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
|
neuper@37906
|
111 |
real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
|
neuper@37906
|
112 |
real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
|
neuper@37906
|
113 |
real_plus_minus_binom1_p_p "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
|
neuper@37906
|
114 |
real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
|
neuper@37906
|
115 |
real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
|
neuper@37906
|
116 |
real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
|
neuper@37906
|
117 |
real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
|
neuper@37906
|
118 |
real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
|
neuper@37906
|
119 |
|
neuper@37906
|
120 |
real_num_collect "[| l is_const; m is_const |] ==> \
|
neuper@37906
|
121 |
\l * n + m * n = (l + m) * n"
|
neuper@37906
|
122 |
(* FIXME.MG.0401: replace 'real_num_collect_assoc'
|
neuper@37906
|
123 |
by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
|
neuper@37906
|
124 |
real_num_collect_assoc "[| l is_const; m is_const |] ==> \
|
neuper@37906
|
125 |
\l * n + (m * n + k) = (l + m) * n + k"
|
neuper@37906
|
126 |
real_num_collect_assoc_l "[| l is_const; m is_const |] ==> \
|
neuper@37906
|
127 |
\l * n + (m * n + k) = (l + m)
|
neuper@37906
|
128 |
* n + k"
|
neuper@37906
|
129 |
real_num_collect_assoc_r "[| l is_const; m is_const |] ==> \
|
neuper@37906
|
130 |
\(k + m * n) + l * n = k + (l + m) * n"
|
neuper@37906
|
131 |
real_one_collect "m is_const ==> n + m * n = (1 + m) * n"
|
neuper@37906
|
132 |
(* FIXME.MG.0401: replace 'real_one_collect_assoc'
|
neuper@37906
|
133 |
by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
|
neuper@37906
|
134 |
real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
|
neuper@37906
|
135 |
|
neuper@37906
|
136 |
real_one_collect_assoc_l "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
|
neuper@37906
|
137 |
real_one_collect_assoc_r "m is_const ==>(k + n) + m * n = k + (1 + m) * n"
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
(* FIXME.MG.0401: replace 'real_mult_2_assoc'
|
neuper@37906
|
140 |
by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
|
neuper@37906
|
141 |
real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k"
|
neuper@37906
|
142 |
real_mult_2_assoc_l "z1 + (z1 + k) = 2 * z1 + k"
|
neuper@37906
|
143 |
real_mult_2_assoc_r "(k + z1) + z1 = k + 2 * z1"
|
neuper@37906
|
144 |
|
neuper@37906
|
145 |
real_add_mult_distrib_poly "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
|
neuper@37906
|
146 |
real_add_mult_distrib2_poly "w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
|
neuper@37906
|
147 |
end
|