1.1 --- a/src/Tools/isac/IsacKnowledge/Root.thy	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,53 +0,0 @@
     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"IsacKnowledge/Root";
    1.13 -   remove_thy"Root";
    1.14 -   use_thy"IsacKnowledge/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