1 (* tests on systems of equations over the reals
2 author: Walther Neuper 050905
3 (c) due to copyright terms
5 use"../smltest/IsacKnowledge/system.sml";
7 val thy = EqSystem.thy;
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "----------- normalise system ------------------------------------";
13 "----------- me --------------------------------------------------";
14 "-----------------------------------------------------------------";
15 "-----------------------------------------------------------------";
16 "-----------------------------------------------------------------";
19 "----------- normalise system ------------------------------------";
20 "----------- normalise system ------------------------------------";
21 "----------- normalise system ------------------------------------";
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]";
24 val SOME (t,_) = rewrite_set_ thy false norm_Poly t;
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";
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]";
31 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
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";
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]";
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"
41 then () else error "system.sml, prog_expr";
44 "----------- me --------------------------------------------------";
45 "----------- me --------------------------------------------------";
46 "----------- me --------------------------------------------------";
47 val fmz = ["equalities [0 = c_2 + c * 0 + - 1 * q_0 / 2 * 0 \<up> 2, 0 = c_2 + c * L + - 1 * q_0 / 2 * L \<up> 2]",
48 "solveForVars [c, c_2]", "solution ss___"];
50 ("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
51 ["EqSystem", "normalise", "2x2"]);
52 val p = e_pos'; val c = [];
53 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
54 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
56 val (p,_,f,nxt,_,pt) = me nxt p c pt;
57 case nxt of (_, Specify_Theory "Biegelinie") => ()
58 | _ => error "system.sml diff.behav.in me -- 1";
59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
62 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
63 | _ => error "system.sml diff.behav.in me -- 2";
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
66 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
67 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
70 case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2",
71 "LINEAR", "system"])) => ()
72 | _ => error "system.sml diff.behav.in me --3";
73 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
74 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
75 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 val (p,_,f,nxt,_,pt) = me nxt p c pt;
77 case nxt of (_, Specify_Theory "Biegelinie") => ()
78 | _ => error "system.sml diff.behav.in me -- 1";
79 val (p,_,f,nxt,_,pt) = me nxt p c pt;
80 val (p,_,f,nxt,_,pt) = me nxt p c pt;
81 val (p,_,f,nxt,_,pt) = me nxt p c pt;
82 case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
83 | _ => error "system.sml diff.behav.in me -- 2";
84 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
85 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
86 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
87 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
88 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
92 WN060421 stopped as soon as exp_IsacCore_Equ_Sys_Lin_No- 1.xml worked ...
94 if f2str f = "" then ()
95 else error "system.sml diff.behav.in me --99";
96 case nxt of ("End_Proof'", End_Proof') => ()
97 | _ => error "system.sml diff.behav.in me --99";
99 default_print_depth 11;nxt;default_print_depth 3;
102 use"../smltest/IsacKnowledge/system.sml";