1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/sml/IsacKnowledge/Root.thy	Thu Apr 17 18:01:03 2003 +0200
     1.3 @@ -0,0 +1,49 @@
     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 +(* 
    1.13 +   remove_thy"Root";
    1.14 +   use_thy"Isac";
    1.15 +*)
    1.16 +Root = Atools + 
    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 = -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 +end