|
1 (* theory collecting all knowledge for Root |
|
2 created by: |
|
3 date: |
|
4 changed by: rlang |
|
5 last change by: rlang |
|
6 date: 02.10.21 |
|
7 *) |
|
8 |
|
9 (* use_thy_only"Knowledge/Root"; |
|
10 remove_thy"Root"; |
|
11 use_thy"Knowledge/Isac"; |
|
12 *) |
|
13 Root = Simplify + |
|
14 |
|
15 (*-------------------- consts------------------------------------------------*) |
|
16 consts |
|
17 |
|
18 sqrt :: "real => real" (*"(sqrt _ )" [80] 80*) |
|
19 nroot :: "[real, real] => real" |
|
20 |
|
21 (*----------------------scripts-----------------------*) |
|
22 |
|
23 (*-------------------- rules------------------------------------------------*) |
|
24 rules (*.not contained in Isabelle2002, |
|
25 stated as axioms, TODO: prove as theorems; |
|
26 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*) |
|
27 |
|
28 root_plus_minus "0 <= b ==> \ |
|
29 \(a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))" |
|
30 root_false "b < 0 ==> (a^^^2 = b) = False" |
|
31 |
|
32 (* for expand_rootbinom *) |
|
33 real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d" |
|
34 real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d" |
|
35 real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d" |
|
36 real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d" |
|
37 real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" |
|
38 real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" |
|
39 realpow_mul "(a*b)^^^n = a^^^n * b^^^n" |
|
40 |
|
41 real_diff_minus "a - b = a + (-1) * b" |
|
42 real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" |
|
43 real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" |
|
44 real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" |
|
45 real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" |
|
46 real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2" |
|
47 real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2" |
|
48 |
|
49 real_root_positive "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)" |
|
50 real_root_negative "a < 0 ==> (x ^^^ 2 = a) = False" |
|
51 |
|
52 |
|
53 end |