(* theory collecting all knowledge for Root

    created by: 

          date: 

    changed by: rlang

    last change by: rlang

              date: 02.10.21

 *)

 (* use_thy_only"Knowledge/Root";

    remove_thy"Root";

    use_thy"Knowledge/Isac";

 *)

 Root = Simplify + 

 (*-------------------- consts------------------------------------------------*)

 consts

   sqrt             :: "real => real"         (*"(sqrt _ )" [80] 80*)

   nroot            :: "[real, real] => real"

 (*----------------------scripts-----------------------*)

 (*-------------------- rules------------------------------------------------*)

 rules (*.not contained in Isabelle2002,

          stated as axioms, TODO: prove as theorems;

          theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)

   root_plus_minus       "0 <= b ==> \

 			\(a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))"

   root_false		"b < 0 ==> (a^^^2 = b) = False"

  (* for expand_rootbinom *)

   real_pp_binom_times        "(a + b)*(c + d) = a*c + a*d + b*c + b*d"

   real_pm_binom_times        "(a + b)*(c - d) = a*c - a*d + b*c - b*d"

   real_mp_binom_times        "(a - b)*(c + d) = a*c + a*d - b*c - b*d"

   real_mm_binom_times        "(a - b)*(c - d) = a*c - a*d - b*c + b*d"

   real_plus_binom_pow3       "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"

   real_minus_binom_pow3      "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"

   realpow_mul                "(a*b)^^^n = a^^^n * b^^^n"

   real_diff_minus            "a - b = a + (-1) * b"

   real_plus_binom_times      "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"

   real_minus_binom_times     "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"

   real_plus_binom_pow2       "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"

   real_minus_binom_pow2      "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"

   real_plus_minus_binom1     "(a + b)*(a - b) = a^^^2 - b^^^2"

   real_plus_minus_binom2     "(a - b)*(a + b) = a^^^2 - b^^^2"

   real_root_positive     "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)"

   real_root_negative     "a <  0 ==> (x ^^^ 2 = a) = False"

 end