1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/Root.thy Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,53 @@
1.4 +(* theory collecting all knowledge for Root
1.5 + created by:
1.6 + date:
1.7 + changed by: rlang
1.8 + last change by: rlang
1.9 + date: 02.10.21
1.10 +*)
1.11 +
1.12 +(* use_thy_only"Knowledge/Root";
1.13 + remove_thy"Root";
1.14 + use_thy"Knowledge/Isac";
1.15 +*)
1.16 +Root = Simplify +
1.17 +
1.18 +(*-------------------- consts------------------------------------------------*)
1.19 +consts
1.20 +
1.21 + sqrt :: "real => real" (*"(sqrt _ )" [80] 80*)
1.22 + nroot :: "[real, real] => real"
1.23 +
1.24 +(*----------------------scripts-----------------------*)
1.25 +
1.26 +(*-------------------- rules------------------------------------------------*)
1.27 +rules (*.not contained in Isabelle2002,
1.28 + stated as axioms, TODO: prove as theorems;
1.29 + theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
1.30 +
1.31 + root_plus_minus "0 <= b ==> \
1.32 + \(a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))"
1.33 + root_false "b < 0 ==> (a^^^2 = b) = False"
1.34 +
1.35 + (* for expand_rootbinom *)
1.36 + real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
1.37 + real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
1.38 + real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
1.39 + real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
1.40 + real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
1.41 + real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
1.42 + realpow_mul "(a*b)^^^n = a^^^n * b^^^n"
1.43 +
1.44 + real_diff_minus "a - b = a + (-1) * b"
1.45 + real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
1.46 + real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
1.47 + real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
1.48 + real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
1.49 + real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
1.50 + real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
1.51 +
1.52 + real_root_positive "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)"
1.53 + real_root_negative "a < 0 ==> (x ^^^ 2 = a) = False"
1.54 +
1.55 +
1.56 +end