50 "----------- tests on predicates in problems ---------------------"; |
50 "----------- tests on predicates in problems ---------------------"; |
51 "----------- tests on predicates in problems ---------------------"; |
51 "----------- tests on predicates in problems ---------------------"; |
52 "----------- tests on predicates in problems ---------------------"; |
52 "----------- tests on predicates in problems ---------------------"; |
53 val thy = @{theory}; |
53 val thy = @{theory}; |
54 val ctxt = Proof_Context.init_global thy; |
54 val ctxt = Proof_Context.init_global thy; |
55 Rewrite.trace_on:=false; (*true false*) |
|
56 |
55 |
57 val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)"; |
56 val t1 = TermC.parseNEW' ctxt "lhs (-8 - 2*x + x \<up> 2 = 0)"; |
58 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1; |
57 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t1; |
59 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then () |
58 if ((UnparseC.term t) = "- 8 - 2 * x + x \<up> 2") then () |
60 else error "polyeq.sml: diff.behav. in lhs"; |
59 else error "polyeq.sml: diff.behav. in lhs"; |
61 |
60 |
62 val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x"; |
61 val t2 = TermC.parseNEW' ctxt "(-8 - 2*x + x \<up> 2) is_expanded_in x"; |
63 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t2; |
62 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t2; |
64 if (UnparseC.term t) = "True" then () |
63 if (UnparseC.term t) = "True" then () |
65 else error "polyeq.sml: diff.behav. 1 in is_expended_in"; |
64 else error "polyeq.sml: diff.behav. 1 in is_expended_in"; |
66 |
65 |
67 val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x"; |
66 val t0 = TermC.parseNEW' ctxt "(sqrt(x)) is_poly_in x"; |
68 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t0; |
67 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t0; |
69 if (UnparseC.term t) = "False" then () |
68 if (UnparseC.term t) = "False" then () |
70 else error "polyeq.sml: diff.behav. 2 in is_poly_in"; |
69 else error "polyeq.sml: diff.behav. 2 in is_poly_in"; |
71 |
70 |
72 val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x"; |
71 val t3 = TermC.parseNEW' ctxt "(-8 + (- 1)*2*x + x \<up> 2) is_poly_in x"; |
73 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; |
72 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3; |
74 if (UnparseC.term t) = "True" then () |
73 if (UnparseC.term t) = "True" then () |
75 else error "polyeq.sml: diff.behav. 3 in is_poly_in"; |
74 else error "polyeq.sml: diff.behav. 3 in is_poly_in"; |
76 |
75 |
77 val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x"; |
76 val t4 = TermC.parseNEW' ctxt "(lhs (-8 + (- 1)*2*x + x \<up> 2 = 0)) is_expanded_in x"; |
78 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; |
77 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4; |
79 if (UnparseC.term t) = "True" then () |
78 if (UnparseC.term t) = "True" then () |
80 else error "polyeq.sml: diff.behav. 4 in is_expended_in"; |
79 else error "polyeq.sml: diff.behav. 4 in is_expended_in"; |
81 |
80 |
82 val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x"; |
81 val t6 = TermC.parseNEW' ctxt "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x"; |
83 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6; |
82 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t6; |
84 if (UnparseC.term t) = "True" then () |
83 if (UnparseC.term t) = "True" then () |
85 else error "polyeq.sml: diff.behav. 5 in is_expended_in"; |
84 else error "polyeq.sml: diff.behav. 5 in is_expended_in"; |
86 |
85 |
87 val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2"; |
86 val t3 = TermC.parseNEW' ctxt"((-8 - 2*x + x \<up> 2) has_degree_in x) = 2"; |
88 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; |
87 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3; |
89 if (UnparseC.term t) = "True" then () |
88 if (UnparseC.term t) = "True" then () |
90 else error "polyeq.sml: diff.behav. in has_degree_in_in"; |
89 else error "polyeq.sml: diff.behav. in has_degree_in_in"; |
91 |
90 |
92 val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2"; |
91 val t3 = TermC.parseNEW' ctxt "((sqrt(x)) has_degree_in x) = 2"; |
93 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t3; |
92 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t3; |
94 if (UnparseC.term t) = "False" then () |
93 if (UnparseC.term t) = "False" then () |
95 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; |
94 else error "polyeq.sml: diff.behav. 6 in has_degree_in_in"; |
96 |
95 |
97 val t4 = TermC.parseNEW' ctxt |
96 val t4 = TermC.parseNEW' ctxt |
98 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1"; |
97 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 1"; |
99 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t4; |
98 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t4; |
100 if (UnparseC.term t) = "False" then () |
99 if (UnparseC.term t) = "False" then () |
101 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; |
100 else error "polyeq.sml: diff.behav. 7 in has_degree_in_in"; |
102 |
101 |
103 val t5 = TermC.parseNEW' ctxt |
102 val t5 = TermC.parseNEW' ctxt |
104 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2"; |
103 "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2"; |
105 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t5; |
104 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_prls t5; |
106 if (UnparseC.term t) = "True" then () |
105 if (UnparseC.term t) = "True" then () |
107 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; |
106 else error "polyeq.sml: diff.behav. 8 in has_degree_in_in"; |
108 |
107 |
109 "----------- test matching problems --------------------------0---"; |
108 "----------- test matching problems --------------------------0---"; |
110 "----------- test matching problems --------------------------0---"; |
109 "----------- test matching problems --------------------------0---"; |
373 kannst Du die 'gr"osste' Variable frei w"ahlen: *) |
372 kannst Du die 'gr"osste' Variable frei w"ahlen: *) |
374 val bdv= TermC.parseNEW' ctxt "bdv ::real"; |
373 val bdv= TermC.parseNEW' ctxt "bdv ::real"; |
375 val x = TermC.parseNEW' ctxt "x ::real"; |
374 val x = TermC.parseNEW' ctxt "x ::real"; |
376 val a = TermC.parseNEW' ctxt "a ::real"; |
375 val a = TermC.parseNEW' ctxt "a ::real"; |
377 val b = TermC.parseNEW' ctxt "b ::real"; |
376 val b = TermC.parseNEW' ctxt "b ::real"; |
378 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2; |
377 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,a)] make_polynomial_in x2; |
379 if UnparseC.term t' = "b + x + a" then () |
378 if UnparseC.term t' = "b + x + a" then () |
380 else error "termorder.sml diff.behav ord_make_polynomial_in #11"; |
379 else error "termorder.sml diff.behav ord_make_polynomial_in #11"; |
381 |
380 |
382 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2; |
381 val NONE = rewrite_set_inst_ ctxt false [(bdv,b)] make_polynomial_in x2; |
383 |
382 |
384 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2; |
383 val SOME (t',_) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in x2; |
385 if UnparseC.term t' = "a + b + x" then () |
384 if UnparseC.term t' = "a + b + x" then () |
386 else error "termorder.sml diff.behav ord_make_polynomial_in #13"; |
385 else error "termorder.sml diff.behav ord_make_polynomial_in #13"; |
387 |
386 |
388 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2"; |
387 val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2"; |
389 val ppp = TermC.parseNEW' ctxt ppp'; |
388 val ppp = TermC.parseNEW' ctxt ppp'; |
390 val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp; |
389 val SOME (t', _) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in ppp; |
391 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then () |
390 if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then () |
392 else error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
391 else error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
393 |
392 |
394 val ttt' = "(3*x + 5)/18 ::real"; |
393 val ttt' = "(3*x + 5)/18 ::real"; |
395 val ttt = TermC.parseNEW' ctxt ttt'; |
394 val ttt = TermC.parseNEW' ctxt ttt'; |
396 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; |
395 val SOME (uuu,_) = rewrite_set_inst_ ctxt false [(bdv,x)] make_polynomial_in ttt; |
397 if UnparseC.term uuu = "(5 + 3 * x) / 18" then () |
396 if UnparseC.term uuu = "(5 + 3 * x) / 18" then () |
398 else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; |
397 else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; |
399 |
398 |
400 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt; |
399 val SOME (uuu,_) = rewrite_set_ ctxt false make_polynomial ttt; |
401 if UnparseC.term uuu = "(5 + 3 * x) / 18" then () |
400 if UnparseC.term uuu = "(5 + 3 * x) / 18" then () |
402 else error "termorder.sml diff.behav ord_make_polynomial_in #16b"; |
401 else error "termorder.sml diff.behav ord_make_polynomial_in #16b"; |
403 |
402 |
404 "----------- lin.eq degree_0 -------------------------------------"; |
403 "----------- lin.eq degree_0 -------------------------------------"; |
405 "----------- lin.eq degree_0 -------------------------------------"; |
404 "----------- lin.eq degree_0 -------------------------------------"; |
1012 val ctxt = Proof_Context.init_global thy; |
1011 val ctxt = Proof_Context.init_global thy; |
1013 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")]; |
1012 val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")]; |
1014 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)"; |
1013 val t = (the o (parseNEW ctxt)) "-8 - 2*x + x \<up> 2 = (0::real)"; |
1015 |
1014 |
1016 val rls = complete_square; |
1015 val rls = complete_square; |
1017 val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t; |
1016 val SOME (t,asm) = rewrite_set_inst_ ctxt true inst rls t; |
1018 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2" |
1017 if UnparseC.term t = "- 8 + (2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2" |
1019 then () else error "rls complete_square CHANGED"; |
1018 then () else error "rls complete_square CHANGED"; |
1020 |
1019 |
1021 val thm = @{thm square_explicit1}; |
1020 val thm = @{thm square_explicit1}; |
1022 val SOME (t,asm) = rewrite_ thy dummy_ord Rule_Set.Empty true thm t; |
1021 val SOME (t,asm) = rewrite_ ctxt dummy_ord Rule_Set.Empty true thm t; |
1023 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8" |
1022 if UnparseC.term t = "(2 / 2 - x) \<up> 2 = (2 / 2) \<up> 2 - - 8" |
1024 then () else error "thm square_explicit1 CHANGED"; |
1023 then () else error "thm square_explicit1 CHANGED"; |
1025 |
1024 |
1026 val thm = @{thm root_plus_minus}; |
1025 val thm = @{thm root_plus_minus}; |
1027 val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t; |
1026 val SOME (t,asm) = rewrite_ ctxt dummy_ord PolyEq_erls true thm t; |
1028 if UnparseC.term t = |
1027 if UnparseC.term t = |
1029 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1028 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n2 / 2 - x = - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1030 then () else error "thm root_plus_minus CHANGED"; |
1029 then () else error "thm root_plus_minus CHANGED"; |
1031 |
1030 |
1032 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
1031 (*the thm bdv_explicit2* here required to be constrained to ::real*) |
1033 val thm = @{thm bdv_explicit2}; |
1032 val thm = @{thm bdv_explicit2}; |
1034 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
1033 val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t; |
1035 if UnparseC.term t = |
1034 if UnparseC.term t = |
1036 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1035 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\n- 1 * x = - (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8)" |
1037 then () else error "thm bdv_explicit2 CHANGED"; |
1036 then () else error "thm bdv_explicit2 CHANGED"; |
1038 |
1037 |
1039 val thm = @{thm bdv_explicit3}; |
1038 val thm = @{thm bdv_explicit3}; |
1040 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
1039 val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t; |
1041 if UnparseC.term t = |
1040 if UnparseC.term t = |
1042 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1041 "2 / 2 - x = sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1043 then () else error "thm bdv_explicit3 CHANGED"; |
1042 then () else error "thm bdv_explicit3 CHANGED"; |
1044 |
1043 |
1045 val thm = @{thm bdv_explicit2}; |
1044 val thm = @{thm bdv_explicit2}; |
1046 val SOME (t,asm) = rewrite_inst_ thy dummy_ord Rule_Set.Empty true inst thm t; |
1045 val SOME (t,asm) = rewrite_inst_ ctxt dummy_ord Rule_Set.Empty true inst thm t; |
1047 if UnparseC.term t = |
1046 if UnparseC.term t = |
1048 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1047 "- 1 * x = - (2 / 2) + sqrt ((2 / 2) \<up> 2 - - 8) \<or>\nx = - 1 * (- (2 / 2) + - 1 * sqrt ((2 / 2) \<up> 2 - - 8))" |
1049 then () else error "thm bdv_explicit2 CHANGED"; |
1048 then () else error "thm bdv_explicit2 CHANGED"; |
1050 |
1049 |
1051 val rls = calculate_RootRat; |
1050 val rls = calculate_RootRat; |
1052 val SOME (t,asm) = rewrite_set_ thy true rls t; |
1051 val SOME (t,asm) = rewrite_set_ ctxt true rls t; |
1053 if UnparseC.term t = |
1052 if UnparseC.term t = |
1054 "- 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))" |
1053 "- 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))" |
1055 (*"- 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*) |
1054 (*"- 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*) |
1056 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; |
1055 then () else error "(-8 - 2*x + x \<up> 2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT"; |
1057 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) |
1056 (*SHOULD BE: UnparseC.term = "x = - 2 | x = 4;*) |
1060 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
1059 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
1061 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
1060 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
1062 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
1061 "-------------------- (3 - 10*x + 3*x \<up> 2 = 0), ----------------------"; |
1063 "---- test the erls ----"; |
1062 "---- test the erls ----"; |
1064 val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \<up> 2 - 1"; |
1063 val t1 = TermC.parseNEW' ctxt "0 <= (10/3/2) \<up> 2 - 1"; |
1065 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1; |
1064 val SOME (t,_) = rewrite_set_ ctxt false PolyEq_erls t1; |
1066 val t' = UnparseC.term t; |
1065 val t' = UnparseC.term t; |
1067 (*if t'= \<^const_name>\<open>True\<close> then () |
1066 (*if t'= \<^const_name>\<open>True\<close> then () |
1068 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) |
1067 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*) |
1069 (* *) |
1068 (* *) |
1070 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)", |
1069 val fmz = ["equality (3 - 10*x + 3*x \<up> 2 = 0)", |