1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -27,7 +27,7 @@
1.4
1.5
1.6 (*
1.7 -> val t = (Thm.term_of o the o (TermC.parse thy)) "#2^^^#3";
1.8 +> val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";
1.9 > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
1.10 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
1.11 > Syntax.string_of_term (ThyC.to_ctxt thy) t';
1.12 @@ -41,30 +41,30 @@
1.13 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
1.14 val thm = ("square_equation_left", "");
1.15 val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
1.16 -(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)
1.17 +(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) \<up> 2"*)
1.18 val rls = ("Test_simplify");
1.19 val (ct,_) = the (rewrite_set thy' false rls ct);
1.20 -(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*)
1.21 +(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x \<up> 2 + -3 * x))"*)
1.22 val rls = ("rearrange_assoc");
1.23 val (ct,_) = the (rewrite_set thy' false rls ct);
1.24 -(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*)
1.25 +(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x \<up> 2 + -3 * x)"*)
1.26 val rls = ("isolate_root");
1.27 val (ct,_) = the (rewrite_set thy' false rls ct);
1.28 -(*"sqrt (x ^^^ 2 + -3 * x) =
1.29 +(*"sqrt (x \<up> 2 + -3 * x) =
1.30 (-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
1.31 val rls = ("Test_simplify");
1.32 val (ct,_) = the (rewrite_set thy' false rls ct);
1.33 -(*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)
1.34 +(*"sqrt (x \<up> 2 + -3 * x) = 6 + x"*)
1.35 val thm = ("square_equation_left", "");
1.36 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.37 val asm = asm union asm';
1.38 -(*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)
1.39 +(*"x \<up> 2 + -3 * x = (6 + x) \<up> 2"*)
1.40 val rls = ("Test_simplify");
1.41 val (ct,_) = the (rewrite_set thy' false rls ct);
1.42 -(*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*)
1.43 +(*"x \<up> 2 + -3 * x = 36 + (x \<up> 2 + 12 * x)"*)
1.44 val rls = ("norm_equation");
1.45 val (ct,_) = the (rewrite_set thy' false rls ct);
1.46 -(*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*)
1.47 +(*"x \<up> 2 + -3 * x + -1 * (36 + (x \<up> 2 + 12 * x)) = 0"*)
1.48 val rls = ("Test_simplify");
1.49 val (ct,_) = the (rewrite_set thy' false rls ct);
1.50 (*"-36 + -15 * x = 0"*)
1.51 @@ -81,7 +81,7 @@
1.52 > asm;
1.53 val it =
1.54 ["(+0) <= sqrt x + sqrt ((-3) + x) ", "(+0) <= 9 + 4 * x",
1.55 - "(+0) <= (-3) * x + x ^^^ 2", "(+0) <= 6 + x"] : TermC.as_string list
1.56 + "(+0) <= (-3) * x + x \<up> 2", "(+0) <= 6 + x"] : TermC.as_string list
1.57 *)
1.58
1.59
1.60 @@ -145,33 +145,33 @@
1.61 val rls = Test_simplify;
1.62 val (t,_) = the (rewrite_set_ thy false rls t);
1.63 (*
1.64 -sqrt (x ^^^ 2 + 5 * x) =
1.65 +sqrt (x \<up> 2 + 5 * x) =
1.66 (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
1.67 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.68 ### trying thm 'rdistr_div_right'
1.69 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.70 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.71 (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
1.72 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.73 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.74 (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
1.75 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.76 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.77 5 / (-1 * 2) + 2 * x / (-1 * 2) +
1.78 (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
1.79
1.80 ### trying thm 'radd_left_commute'
1.81 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.82 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.83 -1 * 9 / (-1 * 2) +
1.84 (5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
1.85 ### trying thm 'radd_assoc'
1.86 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.87 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.88 -1 * 9 / (-1 * 2) +
1.89 (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
1.90
1.91 ### trying thm 'radd_real_const_eq'
1.92 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.93 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.94 -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
1.95 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.96 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.97 -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
1.98 -### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
1.99 +### rewrites to: sqrt (x \<up> 2 + 5 * x) =
1.100 (-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
1.101 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.102
1.103 @@ -207,29 +207,29 @@
1.104 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
1.105 (*1*)val thm = ("square_equation_left", "");
1.106 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.107 -"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
1.108 +"9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2";
1.109 (*2*)val rls = "Test_simplify";
1.110 val (ct,_) = the (rewrite_set thy' false rls ct);
1.111 -"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";
1.112 +"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 2 + 5 * x))";
1.113 (*3*)val rls = "rearrange_assoc";
1.114 val (ct,_) = the (rewrite_set thy' false rls ct);
1.115 -"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";
1.116 +"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)";
1.117 (*4*)val rls = "isolate_root";
1.118 val (ct,_) = the (rewrite_set thy' false rls ct);
1.119 -"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
1.120 +"sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
1.121 (*5*)val rls = "Test_simplify";
1.122 val (ct,_) = the (rewrite_set thy' false rls ct);
1.123 -"sqrt (x ^^^ 2 + 5 * x) = 2 + x";
1.124 +"sqrt (x \<up> 2 + 5 * x) = 2 + x";
1.125 (*6*)val thm = ("square_equation_left", "");
1.126 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
1.127 val asm = asm union asm';
1.128 -"x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
1.129 +"x \<up> 2 + 5 * x = (2 + x) \<up> 2";
1.130 (*7*)val rls = "Test_simplify";
1.131 val (ct,_) = the (rewrite_set thy' false rls ct);
1.132 -"x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";
1.133 +"x \<up> 2 + 5 * x = 4 + (x \<up> 2 + 4 * x)";
1.134 (*8*)val rls = "norm_equation";
1.135 val (ct,_) = the (rewrite_set thy' false rls ct);
1.136 -"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";
1.137 +"x \<up> 2 + 5 * x + -1 * (4 + (x \<up> 2 + 4 * x)) = 0";
1.138 (*9*)val rls = "Test_simplify";
1.139 val (ct,_) = the (rewrite_set thy' false rls ct);
1.140 "-4 + x = 0";
1.141 @@ -362,14 +362,14 @@
1.142 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
1.143 1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
1.144 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
1.145 -1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2
1.146 -1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )
1.147 -1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2)
1.148 -1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
1.149 -1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x
1.150 -2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2
1.151 -3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?!
1.152 -4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)
1.153 +1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) \<up> 2
1.154 +1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x \<up> 2) )
1.155 +1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x \<up> 2)
1.156 +1.5. sqrt (5 * x + x \<up> 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
1.157 +1.6. sqrt (5 * x + x \<up> 2) = (+2) + x
1.158 +2. 5 * x + x \<up> 2 = ((+2) + x) \<up> 2
1.159 +3. 5 * x + x \<up> 2 = 4 + (4 * x + x \<up> 2) ###12.12.99: indent 2.1. !?!
1.160 +4. 5 * x + x \<up> 2 + (-1) * (4 + (4 * x + x \<up> 2)) = (+0)
1.161 5. (-4) + x = (+0)
1.162 6. x = (+0) + (-1) * (-4)
1.163 *)