|
neuper@37906
|
1 |
(* tests on systems of equations over the reals
|
|
neuper@37906
|
2 |
author: Walther Neuper 050905
|
|
neuper@37906
|
3 |
(c) due to copyright terms
|
|
neuper@37906
|
4 |
|
|
neuper@37906
|
5 |
use"../smltest/IsacKnowledge/system.sml";
|
|
neuper@37906
|
6 |
*)
|
|
neuper@37906
|
7 |
val thy = EqSystem.thy;
|
|
neuper@37906
|
8 |
|
|
neuper@37906
|
9 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
10 |
"table of contents -----------------------------------------------";
|
|
neuper@37906
|
11 |
"-----------------------------------------------------------------";
|
|
wneuper@59370
|
12 |
"----------- normalise system ------------------------------------";
|
|
neuper@37906
|
13 |
"----------- me --------------------------------------------------";
|
|
neuper@37906
|
14 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
15 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
16 |
"-----------------------------------------------------------------";
|
|
neuper@37906
|
17 |
|
|
neuper@37906
|
18 |
|
|
wneuper@59370
|
19 |
"----------- normalise system ------------------------------------";
|
|
wneuper@59370
|
20 |
"----------- normalise system ------------------------------------";
|
|
wneuper@59370
|
21 |
"----------- normalise system ------------------------------------";
|
|
Walther@60565
|
22 |
val t = TermC.parse_test @{context} "[0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\
|
|
walther@60329
|
23 |
\ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]";
|
|
neuper@37926
|
24 |
val SOME (t,_) = rewrite_set_ thy false norm_Poly t;
|
|
walther@59868
|
25 |
if UnparseC.term t =
|
|
walther@60329
|
26 |
"[0 = - 1 * q_0 * (0 / 2) + c_2, 0 = L * c + - 1 * q_0 * (L \<up> 2 / 2) + c_2]"
|
|
neuper@38031
|
27 |
then () else error "system.sml, diff.behav. in norm_Poly";
|
|
neuper@37906
|
28 |
|
|
Walther@60565
|
29 |
val t = TermC.parse_test @{context} "[0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\
|
|
walther@60329
|
30 |
\ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]";
|
|
neuper@37926
|
31 |
val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
|
|
walther@59868
|
32 |
if UnparseC.term t =
|
|
walther@60329
|
33 |
"[0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
|
|
neuper@38031
|
34 |
then () else error "system.sml, diff.behav. in norm_Rational";
|
|
neuper@37906
|
35 |
|
|
neuper@37906
|
36 |
|
|
Walther@60565
|
37 |
val t = TermC.parse_test @{context} "nth_ 1 [0 = c*0 + - 1*q_0*(0 \<up> 2 / 2) + c_2,\
|
|
walther@60329
|
38 |
\ 0 = c*L + - 1*q_0*(L \<up> 2 / 2) + c_2]";
|
|
walther@59801
|
39 |
val SOME (t,_) = rewrite_set_ thy false prog_expr t;
|
|
walther@60329
|
40 |
if UnparseC.term t = "0 = c * 0 + - 1 * q_0 * (0 \<up> 2 / 2) + c_2"
|
|
walther@59801
|
41 |
then () else error "system.sml, prog_expr";
|
|
neuper@37906
|
42 |
|
|
neuper@37906
|
43 |
|
|
neuper@37906
|
44 |
"----------- me --------------------------------------------------";
|
|
neuper@37906
|
45 |
"----------- me --------------------------------------------------";
|
|
neuper@37906
|
46 |
"----------- me --------------------------------------------------";
|
|
walther@60329
|
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]",
|
|
neuper@37906
|
48 |
"solveForVars [c, c_2]", "solution ss___"];
|
|
neuper@37906
|
49 |
val (dI',pI',mI') =
|
|
walther@59997
|
50 |
("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
|
|
walther@59997
|
51 |
["EqSystem", "normalise", "2x2"]);
|
|
neuper@37906
|
52 |
val p = e_pos'; val c = [];
|
|
neuper@37906
|
53 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
54 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
55 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
56 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
57 |
case nxt of (_, Specify_Theory "Biegelinie") => ()
|
|
walther@60329
|
58 |
| _ => error "system.sml diff.behav.in me -- 1";
|
|
neuper@37906
|
59 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
60 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
61 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@59367
|
62 |
case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
|
|
walther@60329
|
63 |
| _ => error "system.sml diff.behav.in me -- 2";
|
|
neuper@37906
|
64 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
65 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
66 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
67 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
68 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
69 |
|
|
neuper@37991
|
70 |
case nxt of (_, Subproblem ("Biegelinie", ["triangular", "2x2",
|
|
neuper@55276
|
71 |
"LINEAR", "system"])) => ()
|
|
neuper@38031
|
72 |
| _ => error "system.sml diff.behav.in me --3";
|
|
neuper@37906
|
73 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
|
neuper@37906
|
74 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
75 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
76 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37991
|
77 |
case nxt of (_, Specify_Theory "Biegelinie") => ()
|
|
walther@60329
|
78 |
| _ => error "system.sml diff.behav.in me -- 1";
|
|
neuper@37906
|
79 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
80 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
81 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
wneuper@59367
|
82 |
case nxt of (_, Apply_Method ["EqSystem", "normalise", "2x2"]) => ()
|
|
walther@60329
|
83 |
| _ => error "system.sml diff.behav.in me -- 2";
|
|
neuper@37906
|
84 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
85 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
86 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
87 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
88 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
|
|
neuper@37906
|
89 |
|
|
neuper@37906
|
90 |
|
|
neuper@37906
|
91 |
(*---
|
|
walther@60329
|
92 |
WN060421 stopped as soon as exp_IsacCore_Equ_Sys_Lin_No- 1.xml worked ...
|
|
neuper@37906
|
93 |
|
|
neuper@37906
|
94 |
if f2str f = "" then ()
|
|
neuper@38031
|
95 |
else error "system.sml diff.behav.in me --99";
|
|
neuper@37906
|
96 |
case nxt of ("End_Proof'", End_Proof') => ()
|
|
neuper@38031
|
97 |
| _ => error "system.sml diff.behav.in me --99";
|
|
neuper@37906
|
98 |
|
|
wneuper@59111
|
99 |
default_print_depth 11;nxt;default_print_depth 3;
|
|
neuper@37906
|
100 |
---*)
|
|
neuper@37906
|
101 |
(*
|
|
neuper@37906
|
102 |
use"../smltest/IsacKnowledge/system.sml";
|
|
neuper@37906
|
103 |
*)
|