1.1 --- a/src/Tools/isac/IsacKnowledge/RootEq.thy Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,142 +0,0 @@
1.4 -(*.(c) by Richard Lang, 2003 .*)
1.5 -(* collecting all knowledge for Root Equations
1.6 - created by: rlang
1.7 - date: 02.08
1.8 - changed by: rlang
1.9 - last change by: rlang
1.10 - date: 02.11.14
1.11 -*)
1.12 -(* use"../knowledge/RootEq.ML";
1.13 - use"knowledge/RootEq.ML";
1.14 - use"RootEq.ML";
1.15 -
1.16 - remove_thy"RootEq";
1.17 - use_thy"Isac";
1.18 -
1.19 - use"ROOT.ML";
1.20 - cd"knowledge";
1.21 - *)
1.22 -
1.23 -RootEq = Root +
1.24 -
1.25 -(*-------------------- consts------------------------------------------------*)
1.26 -consts
1.27 - (*-------------------------root-----------------------*)
1.28 - is'_rootTerm'_in :: [real, real] => bool ("_ is'_rootTerm'_in _")
1.29 - is'_sqrtTerm'_in :: [real, real] => bool ("_ is'_sqrtTerm'_in _")
1.30 - is'_normSqrtTerm'_in :: [real, real] => bool ("_ is'_normSqrtTerm'_in _")
1.31 - (*----------------------scripts-----------------------*)
1.32 - Norm'_sq'_root'_equation
1.33 - :: "[bool,real, \
1.34 - \ bool list] => bool list"
1.35 - ("((Script Norm'_sq'_root'_equation (_ _ =))// \
1.36 - \ (_))" 9)
1.37 - Solve'_sq'_root'_equation
1.38 - :: "[bool,real, \
1.39 - \ bool list] => bool list"
1.40 - ("((Script Solve'_sq'_root'_equation (_ _ =))// \
1.41 - \ (_))" 9)
1.42 - Solve'_left'_sq'_root'_equation
1.43 - :: "[bool,real, \
1.44 - \ bool list] => bool list"
1.45 - ("((Script Solve'_left'_sq'_root'_equation (_ _ =))// \
1.46 - \ (_))" 9)
1.47 - Solve'_right'_sq'_root'_equation
1.48 - :: "[bool,real, \
1.49 - \ bool list] => bool list"
1.50 - ("((Script Solve'_right'_sq'_root'_equation (_ _ =))// \
1.51 - \ (_))" 9)
1.52 -
1.53 -(*-------------------- rules------------------------------------------------*)
1.54 -rules
1.55 -
1.56 -(* normalize *)
1.57 - makex1_x
1.58 - "a^^^1 = a"
1.59 - real_assoc_1
1.60 - "a+(b+c) = a+b+c"
1.61 - real_assoc_2
1.62 - "a*(b*c) = a*b*c"
1.63 -
1.64 - (* simplification of root*)
1.65 - sqrt_square_1
1.66 - "[|0 <= a|] ==> (sqrt a)^^^2 = a"
1.67 - sqrt_square_2
1.68 - "sqrt (a ^^^ 2) = a"
1.69 - sqrt_times_root_1
1.70 - "sqrt a * sqrt b = sqrt(a*b)"
1.71 - sqrt_times_root_2
1.72 - "a * sqrt b * sqrt c = a * sqrt(b*c)"
1.73 -
1.74 - (* isolate one root on the LEFT or RIGHT hand side of the equation *)
1.75 - sqrt_isolate_l_add1
1.76 - "[|bdv occurs_in c|] ==> (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
1.77 - sqrt_isolate_l_add2
1.78 - "[|bdv occurs_in c|] ==>(a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
1.79 - sqrt_isolate_l_add3
1.80 - "[|bdv occurs_in c|] ==> (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d+ (-1) * a)"
1.81 - sqrt_isolate_l_add4
1.82 - "[|bdv occurs_in c|] ==>(a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d+ (-1) * a)"
1.83 - sqrt_isolate_l_add5
1.84 - "[|bdv occurs_in c|] ==> (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
1.85 - sqrt_isolate_l_add6
1.86 - "[|bdv occurs_in c|] ==>(a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
1.87 - sqrt_isolate_r_add1
1.88 - "[|bdv occurs_in f|] ==>(a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
1.89 - sqrt_isolate_r_add2
1.90 - "[|bdv occurs_in f|] ==>(a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
1.91 - (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
1.92 - sqrt_isolate_r_add3
1.93 - "[|bdv occurs_in f|] ==>(a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
1.94 - sqrt_isolate_r_add4
1.95 - "[|bdv occurs_in f|] ==>(a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
1.96 - sqrt_isolate_r_add5
1.97 - "[|bdv occurs_in f|] ==>(a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
1.98 - sqrt_isolate_r_add6
1.99 - "[|bdv occurs_in f|] ==>(a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
1.100 -
1.101 - (* eliminate isolates sqrt *)
1.102 - sqrt_square_equation_both_1
1.103 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.104 - ( (sqrt a + sqrt b = sqrt c + sqrt d) =
1.105 - (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.106 - sqrt_square_equation_both_2
1.107 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.108 - ( (sqrt a - sqrt b = sqrt c + sqrt d) =
1.109 - (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.110 - sqrt_square_equation_both_3
1.111 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.112 - ( (sqrt a + sqrt b = sqrt c - sqrt d) =
1.113 - (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.114 - sqrt_square_equation_both_4
1.115 - "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.116 - ( (sqrt a - sqrt b = sqrt c - sqrt d) =
1.117 - (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.118 - sqrt_square_equation_left_1
1.119 - "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==> ( (sqrt (a) = b) = (a = (b^^^2)))"
1.120 - sqrt_square_equation_left_2
1.121 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
1.122 - sqrt_square_equation_left_3
1.123 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
1.124 - (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
1.125 - sqrt_square_equation_left_4
1.126 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
1.127 - sqrt_square_equation_left_5
1.128 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
1.129 - sqrt_square_equation_left_6
1.130 - "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
1.131 - sqrt_square_equation_right_1
1.132 - "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> ( (a = sqrt (b)) = (a^^^2 = b))"
1.133 - sqrt_square_equation_right_2
1.134 - "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
1.135 - sqrt_square_equation_right_3
1.136 - "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
1.137 - (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
1.138 - sqrt_square_equation_right_4
1.139 - "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
1.140 - sqrt_square_equation_right_5
1.141 - "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
1.142 - sqrt_square_equation_right_6
1.143 - "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
1.144 -
1.145 -end