1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Jul 28 11:43:27 2022 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Sat Jul 30 16:47:45 2022 +0200
1.3 @@ -52,57 +52,56 @@
1.4 "----------- tests on predicates in problems ---------------------";
1.5 val thy = @{theory};
1.6 val ctxt = Proof_Context.init_global thy;
1.7 -Rewrite.trace_on:=false; (*true false*)
1.8
1.9 val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)";
1.10 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.11 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t1;
1.12 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then ()
1.13 else error "polyeq.sml: diff.behav. in lhs";
1.14
1.15 val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x";
1.16 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2;
1.17 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t2;
1.18 if (UnparseC.term t) = "True" then ()
1.19 else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.20
1.21 val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x";
1.22 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0;
1.23 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t0;
1.24 if (UnparseC.term t) = "False" then ()
1.25 else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.26
1.27 val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x";
1.28 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.29 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;
1.30 if (UnparseC.term t) = "True" then ()
1.31 else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.32
1.33 val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x";
1.34 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.35 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4;
1.36 if (UnparseC.term t) = "True" then ()
1.37 else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.38
1.39 val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
1.40 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
1.41 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t6;
1.42 if (UnparseC.term t) = "True" then ()
1.43 else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.44
1.45 val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.46 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.47 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;
1.48 if (UnparseC.term t) = "True" then ()
1.49 else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.50
1.51 val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2";
1.52 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3;
1.53 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3;
1.54 if (UnparseC.term t) = "False" then ()
1.55 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.56
1.57 val t4 = TermC.parseNEW' ctxt
1.58 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1";
1.59 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4;
1.60 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4;
1.61 if (UnparseC.term t) = "False" then ()
1.62 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.63
1.64 val t5 = TermC.parseNEW' ctxt
1.65 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
1.66 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5;
1.67 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t5;
1.68 if (UnparseC.term t) = "True" then ()
1.69 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.70
1.71 @@ -375,29 +374,29 @@
1.72 val x = TermC.parseNEW' ctxt "x ::real";
1.73 val a = TermC.parseNEW' ctxt "a ::real";
1.74 val b = TermC.parseNEW' ctxt "b ::real";
1.75 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
1.76 +val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,a)] make_polynomial_in x2;
1.77 if UnparseC.term t' = "b + x + a" then ()
1.78 else error "termorder.sml diff.behav ord_make_polynomial_in #11";
1.79
1.80 -val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
1.81 +val NONE = rewrite_set_inst_ ctxt false [(bdv,b)] make_polynomial_in x2;
1.82
1.83 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
1.84 +val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in x2;
1.85 if UnparseC.term t' = "a + b + x" then ()
1.86 else error "termorder.sml diff.behav ord_make_polynomial_in #13";
1.87
1.88 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
1.89 val ppp = TermC.parseNEW' ctxt ppp';
1.90 -val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
1.91 +val SOME (t', _) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in ppp;
1.92 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
1.93 else error "termorder.sml diff.behav ord_make_polynomial_in #15";
1.94
1.95 val ttt' = "(3*x + 5)/18 ::real";
1.96 val ttt = TermC.parseNEW' ctxt ttt';
1.97 -val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
1.98 +val SOME (uuu,_) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in ttt;
1.99 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.100 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
1.101
1.102 -val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
1.103 +val SOME (uuu,_) = rewrite_set_ ctxt false make_polynomial ttt;
1.104 if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
1.105 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
1.106
1.107 @@ -1014,42 +1013,42 @@
1.108 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)";
1.109
1.110 val rls = complete_square;
1.111 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
1.112 +val SOME (t,asm) = rewrite_set_inst_ ctxt true inst rls t;
1.113 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2"
1.114 then () else error "rls complete_square CHANGED";
1.115
1.116 val thm = @{thm square_explicit1};
1.117 -val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t;
1.118 +val SOME (t,asm) = rewrite_ ctxt dummy_ord Rule_Set.Empty true thm t;
1.119 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8"
1.120 then () else error "thm square_explicit1 CHANGED";
1.121
1.122 val thm = @{thm root_plus_minus};
1.123 -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
1.124 +val SOME (t,asm) = rewrite_ ctxt dummy_ord PolyEq_erls true thm t;
1.125 if UnparseC.term t =
1.126 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
1.127 then () else error "thm root_plus_minus CHANGED";
1.128
1.129 (*the thm bdv_explicit2* here required to be constrained to ::real*)
1.130 val thm = @{thm bdv_explicit2};
1.131 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.132 +val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
1.133 if UnparseC.term t =
1.134 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)"
1.135 then () else error "thm bdv_explicit2 CHANGED";
1.136
1.137 val thm = @{thm bdv_explicit3};
1.138 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.139 +val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
1.140 if UnparseC.term t =
1.141 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
1.142 then () else error "thm bdv_explicit3 CHANGED";
1.143
1.144 val thm = @{thm bdv_explicit2};
1.145 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t;
1.146 +val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t;
1.147 if UnparseC.term t =
1.148 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))"
1.149 then () else error "thm bdv_explicit2 CHANGED";
1.150
1.151 val rls = calculate_RootRat;
1.152 -val SOME (t,asm) = rewrite_set_ thy true rls t;
1.153 +val SOME (t,asm) = rewrite_set_ ctxt true rls t;
1.154 if UnparseC.term t =
1.155 "- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - - 8) \<or>\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - - 8))"
1.156 (*"- 1 * x = - 1 + sqrt (2 \<up> 2 / 2 \<up> 2 - -8) |\nx = - 1 * - 1 + - 1 * (- 1 * sqrt (2 \<up> 2 / 2 \<up> 2 - -8))"..isabisac15*)
1.157 @@ -1062,7 +1061,7 @@
1.158 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------";
1.159 "---- test the erls ----";
1.160 val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \<up> 2 - 1";
1.161 - val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
1.162 + val SOME (t,_) = rewrite_set_ ctxt false PolyEq_erls t1;
1.163 val t' = UnparseC.term t;
1.164 (*if t'= \<^const_name>\<open>True\<close> then ()
1.165 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)