neuper@37906: (* theory collecting all knowledge for Root
neuper@37906:    created by: 
neuper@37906:          date: 
neuper@37906:    changed by: rlang
neuper@37906:    last change by: rlang
neuper@37906:              date: 02.10.21
neuper@37906: *)
neuper@37906: 
neuper@37947: (* use_thy_only"Knowledge/Root";
neuper@37906:    remove_thy"Root";
neuper@37947:    use_thy"Knowledge/Isac";
neuper@37906: *)
neuper@37906: Root = Simplify + 
neuper@37906: 
neuper@37906: (*-------------------- consts------------------------------------------------*)
neuper@37906: consts
neuper@37906: 
neuper@37906:   sqrt             :: "real => real"         (*"(sqrt _ )" [80] 80*)
neuper@37906:   nroot            :: "[real, real] => real"
neuper@37906: 
neuper@37906: (*----------------------scripts-----------------------*)
neuper@37906: 
neuper@37906: (*-------------------- rules------------------------------------------------*)
neuper@37906: rules (*.not contained in Isabelle2002,
neuper@37906:          stated as axioms, TODO: prove as theorems;
neuper@37906:          theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
neuper@37906: 
neuper@37906:   root_plus_minus       "0 <= b ==> \
neuper@37906: 			\(a^^^2 = b) = ((a = sqrt b) | (a = (-1)*sqrt b))"
neuper@37906:   root_false		"b < 0 ==> (a^^^2 = b) = False"
neuper@37906: 
neuper@37906:  (* for expand_rootbinom *)
neuper@37906:   real_pp_binom_times        "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
neuper@37906:   real_pm_binom_times        "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
neuper@37906:   real_mp_binom_times        "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
neuper@37906:   real_mm_binom_times        "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
neuper@37906:   real_plus_binom_pow3       "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
neuper@37906:   real_minus_binom_pow3      "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
neuper@37906:   realpow_mul                "(a*b)^^^n = a^^^n * b^^^n"
neuper@37906: 
neuper@37906:   real_diff_minus            "a - b = a + (-1) * b"
neuper@37906:   real_plus_binom_times      "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
neuper@37906:   real_minus_binom_times     "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
neuper@37906:   real_plus_binom_pow2       "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
neuper@37906:   real_minus_binom_pow2      "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
neuper@37906:   real_plus_minus_binom1     "(a + b)*(a - b) = a^^^2 - b^^^2"
neuper@37906:   real_plus_minus_binom2     "(a - b)*(a + b) = a^^^2 - b^^^2"
neuper@37906: 
neuper@37906:   real_root_positive     "0 <= a ==> (x ^^^ 2 = a) = (x = sqrt a)"
neuper@37906:   real_root_negative     "a <  0 ==> (x ^^^ 2 = a) = False"
neuper@37906: 
neuper@37906:       
neuper@37906: end