(* 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