1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 15:53:18 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 16:56:22 2010 +0200
1.3 @@ -40,81 +40,81 @@
1.4 axioms
1.5
1.6 (* normalize *)
1.7 - makex1_x "a^^^1 = a"
1.8 - real_assoc_1 "a+(b+c) = a+b+c"
1.9 - real_assoc_2 "a*(b*c) = a*b*c"
1.10 + makex1_x: "a^^^1 = a"
1.11 + real_assoc_1: "a+(b+c) = a+b+c"
1.12 + real_assoc_2: "a*(b*c) = a*b*c"
1.13
1.14 (* simplification of root*)
1.15 - sqrt_square_1 "[|0 <= a|] ==> (sqrt a)^^^2 = a"
1.16 - sqrt_square_2 "sqrt (a ^^^ 2) = a"
1.17 - sqrt_times_root_1 "sqrt a * sqrt b = sqrt(a*b)"
1.18 - sqrt_times_root_2 "a * sqrt b * sqrt c = a * sqrt(b*c)"
1.19 + sqrt_square_1: "[|0 <= a|] ==> (sqrt a)^^^2 = a"
1.20 + sqrt_square_2: "sqrt (a ^^^ 2) = a"
1.21 + sqrt_times_root_1: "sqrt a * sqrt b = sqrt(a*b)"
1.22 + sqrt_times_root_2: "a * sqrt b * sqrt c = a * sqrt(b*c)"
1.23
1.24 (* isolate one root on the LEFT or RIGHT hand side of the equation *)
1.25 - sqrt_isolate_l_add1 "[|bdv occurs_in c|] ==>
1.26 + sqrt_isolate_l_add1: "[|bdv occurs_in c|] ==>
1.27 (a + b*sqrt(c) = d) = (b * sqrt(c) = d+ (-1) * a)"
1.28 - sqrt_isolate_l_add2 "[|bdv occurs_in c|] ==>
1.29 + sqrt_isolate_l_add2: "[|bdv occurs_in c|] ==>
1.30 (a + sqrt(c) = d) = ((sqrt(c) = d+ (-1) * a))"
1.31 - sqrt_isolate_l_add3 "[|bdv occurs_in c|] ==>
1.32 + sqrt_isolate_l_add3: "[|bdv occurs_in c|] ==>
1.33 (a + b*(e/sqrt(c)) = d) = (b * (e/sqrt(c)) = d + (-1) * a)"
1.34 - sqrt_isolate_l_add4 "[|bdv occurs_in c|] ==>
1.35 + sqrt_isolate_l_add4: "[|bdv occurs_in c|] ==>
1.36 (a + b/(f*sqrt(c)) = d) = (b / (f*sqrt(c)) = d + (-1) * a)"
1.37 - sqrt_isolate_l_add5 "[|bdv occurs_in c|] ==>
1.38 + sqrt_isolate_l_add5: "[|bdv occurs_in c|] ==>
1.39 (a + b*(e/(f*sqrt(c))) = d) = (b * (e/(f*sqrt(c))) = d+ (-1) * a)"
1.40 - sqrt_isolate_l_add6 "[|bdv occurs_in c|] ==>
1.41 + sqrt_isolate_l_add6: "[|bdv occurs_in c|] ==>
1.42 (a + b/sqrt(c) = d) = (b / sqrt(c) = d+ (-1) * a)"
1.43 - sqrt_isolate_r_add1 "[|bdv occurs_in f|] ==>
1.44 + sqrt_isolate_r_add1: "[|bdv occurs_in f|] ==>
1.45 (a = d + e*sqrt(f)) = (a + (-1) * d = e*sqrt(f))"
1.46 - sqrt_isolate_r_add2 "[|bdv occurs_in f|] ==>
1.47 + sqrt_isolate_r_add2: "[|bdv occurs_in f|] ==>
1.48 (a = d + sqrt(f)) = (a + (-1) * d = sqrt(f))"
1.49 (* small hack: thm 3,5,6 are not needed if rootnormalize is well done*)
1.50 - sqrt_isolate_r_add3 "[|bdv occurs_in f|] ==>
1.51 + sqrt_isolate_r_add3: "[|bdv occurs_in f|] ==>
1.52 (a = d + e*(g/sqrt(f))) = (a + (-1) * d = e*(g/sqrt(f)))"
1.53 - sqrt_isolate_r_add4 "[|bdv occurs_in f|] ==>
1.54 + sqrt_isolate_r_add4: "[|bdv occurs_in f|] ==>
1.55 (a = d + g/sqrt(f)) = (a + (-1) * d = g/sqrt(f))"
1.56 - sqrt_isolate_r_add5 "[|bdv occurs_in f|] ==>
1.57 + sqrt_isolate_r_add5: "[|bdv occurs_in f|] ==>
1.58 (a = d + e*(g/(h*sqrt(f)))) = (a + (-1) * d = e*(g/(h*sqrt(f))))"
1.59 - sqrt_isolate_r_add6 "[|bdv occurs_in f|] ==>
1.60 + sqrt_isolate_r_add6: "[|bdv occurs_in f|] ==>
1.61 (a = d + g/(h*sqrt(f))) = (a + (-1) * d = g/(h*sqrt(f)))"
1.62
1.63 (* eliminate isolates sqrt *)
1.64 - sqrt_square_equation_both_1 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.65 + sqrt_square_equation_both_1: "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.66 ( (sqrt a + sqrt b = sqrt c + sqrt d) =
1.67 (a+2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.68 - sqrt_square_equation_both_2 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.69 + sqrt_square_equation_both_2: "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.70 ( (sqrt a - sqrt b = sqrt c + sqrt d) =
1.71 (a - 2*sqrt(a)*sqrt(b)+b = c+2*sqrt(c)*sqrt(d)+d))"
1.72 - sqrt_square_equation_both_3 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.73 + sqrt_square_equation_both_3: "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.74 ( (sqrt a + sqrt b = sqrt c - sqrt d) =
1.75 (a + 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.76 - sqrt_square_equation_both_4 "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.77 + sqrt_square_equation_both_4: "[|bdv occurs_in b; bdv occurs_in d|] ==>
1.78 ( (sqrt a - sqrt b = sqrt c - sqrt d) =
1.79 (a - 2*sqrt(a)*sqrt(b)+b = c - 2*sqrt(c)*sqrt(d)+d))"
1.80 - sqrt_square_equation_left_1 "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
1.81 + sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
1.82 ( (sqrt (a) = b) = (a = (b^^^2)))"
1.83 - sqrt_square_equation_left_2 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
1.84 + sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
1.85 ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))"
1.86 - sqrt_square_equation_left_3 "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
1.87 + sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==>
1.88 ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)"
1.89 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
1.90 - sqrt_square_equation_left_4 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
1.91 + sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
1.92 ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))"
1.93 - sqrt_square_equation_left_5 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
1.94 + sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==>
1.95 ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)"
1.96 - sqrt_square_equation_left_6 "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
1.97 + sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==>
1.98 ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))"
1.99 - sqrt_square_equation_right_1 "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
1.100 + sqrt_square_equation_right_1: "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==>
1.101 ( (a = sqrt (b)) = (a^^^2 = b))"
1.102 - sqrt_square_equation_right_2 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
1.103 + sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
1.104 ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))"
1.105 - sqrt_square_equation_right_3 "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
1.106 + sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==>
1.107 ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))"
1.108 (* small hack: thm 4-6 are not needed if rootnormalize is well done*)
1.109 - sqrt_square_equation_right_4 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
1.110 + sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
1.111 ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))"
1.112 - sqrt_square_equation_right_5 "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
1.113 + sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==>
1.114 ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))"
1.115 - sqrt_square_equation_right_6 "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
1.116 + sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==>
1.117 ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
1.118
1.119 ML {*