17 |
17 |
18 |
18 |
19 "----------- normalise system ------------------------------------"; |
19 "----------- normalise system ------------------------------------"; |
20 "----------- normalise system ------------------------------------"; |
20 "----------- normalise system ------------------------------------"; |
21 "----------- normalise system ------------------------------------"; |
21 "----------- normalise system ------------------------------------"; |
22 val t = TermC.str2term "[0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\ |
22 val t = TermC.parse_test @{context} "[0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\ |
23 \ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]"; |
23 \ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]"; |
24 val SOME (t,_) = rewrite_set_ thy false norm_Poly t; |
24 val SOME (t,_) = rewrite_set_ thy false norm_Poly t; |
25 if UnparseC.term t = |
25 if UnparseC.term t = |
26 "[0 = - 1 * q_0 * (0 / 2) + c_2, 0 = L * c + - 1 * q_0 * (L \<up> 2 / 2) + c_2]" |
26 "[0 = - 1 * q_0 * (0 / 2) + c_2, 0 = L * c + - 1 * q_0 * (L \<up> 2 / 2) + c_2]" |
27 then () else error "system.sml, diff.behav. in norm_Poly"; |
27 then () else error "system.sml, diff.behav. in norm_Poly"; |
28 |
28 |
29 val t = TermC.str2term "[0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\ |
29 val t = TermC.parse_test @{context} "[0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\ |
30 \ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]"; |
30 \ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]"; |
31 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
31 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
32 if UnparseC.term t = |
32 if UnparseC.term t = |
33 "[0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" |
33 "[0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]" |
34 then () else error "system.sml, diff.behav. in norm_Rational"; |
34 then () else error "system.sml, diff.behav. in norm_Rational"; |
35 |
35 |
36 |
36 |
37 val t = TermC.str2term "nth_ 1 [0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\ |
37 val t = TermC.parse_test @{context} "nth_ 1 [0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\ |
38 \ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]"; |
38 \ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]"; |
39 val SOME (t,_) = rewrite_set_ thy false prog_expr t; |
39 val SOME (t,_) = rewrite_set_ thy false prog_expr t; |
40 if UnparseC.term t = "0 = c * 0 + - 1 * q_0 * (0 \<up> 2 / 2) + c_2" |
40 if UnparseC.term t = "0 = c * 0 + - 1 * q_0 * (0 \<up> 2 / 2) + c_2" |
41 then () else error "system.sml, prog_expr"; |
41 then () else error "system.sml, prog_expr"; |
42 |
42 |