1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -28,13 +28,13 @@
     1.4  subsection \<open>theorems not yet adopted from Isabelle\<close>
     1.5  axiomatization where
     1.6  (* normalise *)
     1.7 -  makex1_x:            "a^^^1  = a"   and
     1.8 +  makex1_x:            "a \<up> 1  = a"   and
     1.9    real_assoc_1:        "a+(b+c) = a+b+c" and
    1.10    real_assoc_2:        "a*(b*c) = a*b*c" and
    1.11  
    1.12    (* simplification of root*)
    1.13 -  sqrt_square_1:       "[|0 <= a|] ==>  (sqrt a)^^^2 = a" and
    1.14 -  sqrt_square_2:       "sqrt (a ^^^ 2) = a" and
    1.15 +  sqrt_square_1:       "[|0 <= a|] ==>  (sqrt a) \<up> 2 = a" and
    1.16 +  sqrt_square_2:       "sqrt (a  \<up>  2) = a" and
    1.17    sqrt_times_root_1:   "sqrt a * sqrt b = sqrt(a*b)" and
    1.18    sqrt_times_root_2:   "a * sqrt b * sqrt c = a * sqrt(b*c)" and
    1.19  
    1.20 @@ -79,31 +79,31 @@
    1.21     ( (sqrt a - sqrt b           = sqrt c - sqrt d) = 
    1.22       (a - 2*sqrt(a)*sqrt(b)+b  = c - 2*sqrt(c)*sqrt(d)+d))" and
    1.23    sqrt_square_equation_left_1: "[|bdv occurs_in a; 0 <= a; 0 <= b|] ==>
    1.24 -   ( (sqrt (a) = b) = (a = (b^^^2)))" and
    1.25 +   ( (sqrt (a) = b) = (a = (b \<up> 2)))" and
    1.26    sqrt_square_equation_left_2: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> 
    1.27 -   ( (c*sqrt(a) = b) = (c^^^2*a = b^^^2))" and
    1.28 +   ( (c*sqrt(a) = b) = (c \<up> 2*a = b \<up> 2))" and
    1.29    sqrt_square_equation_left_3: "[|bdv occurs_in a; 0 <= a; 0 <= b*c|] ==> 
    1.30 -   ( c/sqrt(a) = b) = (c^^^2 / a = b^^^2)" and
    1.31 +   ( c/sqrt(a) = b) = (c \<up> 2 / a = b \<up> 2)" and
    1.32    (* small hack: thm 4-6 are not needed if rootnormalise is well done*)
    1.33    sqrt_square_equation_left_4: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> 
    1.34 -   ( (c*(d/sqrt (a)) = b) = (c^^^2*(d^^^2/a) = b^^^2))" and
    1.35 +   ( (c*(d/sqrt (a)) = b) = (c \<up> 2*(d \<up> 2/a) = b \<up> 2))" and
    1.36    sqrt_square_equation_left_5: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d|] ==> 
    1.37 -   ( c/(d*sqrt(a)) = b) = (c^^^2 / (d^^^2*a) = b^^^2)" and
    1.38 +   ( c/(d*sqrt(a)) = b) = (c \<up> 2 / (d \<up> 2*a) = b \<up> 2)" and
    1.39    sqrt_square_equation_left_6: "[|bdv occurs_in a; 0 <= a; 0 <= b*c*d*e|] ==> 
    1.40 -   ( (c*(d/(e*sqrt (a))) = b) = (c^^^2*(d^^^2/(e^^^2*a)) = b^^^2))" and
    1.41 +   ( (c*(d/(e*sqrt (a))) = b) = (c \<up> 2*(d \<up> 2/(e \<up> 2*a)) = b \<up> 2))" and
    1.42    sqrt_square_equation_right_1:  "[|bdv occurs_in b; 0 <= a; 0 <= b|] ==> 
    1.43 -   ( (a = sqrt (b)) = (a^^^2 = b))" and
    1.44 +   ( (a = sqrt (b)) = (a \<up> 2 = b))" and
    1.45    sqrt_square_equation_right_2: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> 
    1.46 -   ( (a = c*sqrt (b)) = ((a^^^2) = c^^^2*b))" and
    1.47 +   ( (a = c*sqrt (b)) = ((a \<up> 2) = c \<up> 2*b))" and
    1.48    sqrt_square_equation_right_3: "[|bdv occurs_in b; 0 <= a*c; 0 <= b|] ==> 
    1.49 -   ( (a = c/sqrt (b)) = (a^^^2 = c^^^2/b))" and
    1.50 +   ( (a = c/sqrt (b)) = (a \<up> 2 = c \<up> 2/b))" and
    1.51   (* small hack: thm 4-6 are not needed if rootnormalise is well done*)
    1.52    sqrt_square_equation_right_4: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> 
    1.53 -   ( (a = c*(d/sqrt (b))) = ((a^^^2) = c^^^2*(d^^^2/b)))" and
    1.54 +   ( (a = c*(d/sqrt (b))) = ((a \<up> 2) = c \<up> 2*(d \<up> 2/b)))" and
    1.55    sqrt_square_equation_right_5: "[|bdv occurs_in b; 0 <= a*c*d; 0 <= b|] ==> 
    1.56 -   ( (a = c/(d*sqrt (b))) = (a^^^2 = c^^^2/(d^^^2*b)))" and
    1.57 +   ( (a = c/(d*sqrt (b))) = (a \<up> 2 = c \<up> 2/(d \<up> 2*b)))" and
    1.58    sqrt_square_equation_right_6: "[|bdv occurs_in b; 0 <= a*c*d*e; 0 <= b|] ==> 
    1.59 -   ( (a = c*(d/(e*sqrt (b)))) = ((a^^^2) = c^^^2*(d^^^2/(e^^^2*b))))"
    1.60 +   ( (a = c*(d/(e*sqrt (b)))) = ((a \<up> 2) = c \<up> 2*(d \<up> 2/(e \<up> 2*b))))"
    1.61  
    1.62  subsection \<open>predicates\<close>
    1.63  ML \<open>