walther@60347
|
1 |
(* Title: Knowledge/eqsystem-1.sml
|
walther@60347
|
2 |
author: Walther Neuper 050826,
|
walther@60347
|
3 |
(c) due to copyright terms
|
walther@60347
|
4 |
*)
|
walther@60347
|
5 |
|
Walther@60567
|
6 |
"-----------------------------------------------------------------------------------------------";
|
Walther@60567
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
Walther@60567
|
8 |
"-----------------------------------------------------------------------------------------------";
|
Walther@60567
|
9 |
"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
|
Walther@60567
|
10 |
"----------- problems -----------------------------------------------------------equsystem-1.sml";
|
Walther@60567
|
11 |
"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
|
Walther@60567
|
12 |
"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
|
Walther@60567
|
13 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
|
Walther@60567
|
14 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
|
Walther@60567
|
15 |
"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
|
Walther@60567
|
16 |
"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
|
Walther@60567
|
17 |
"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
|
Walther@60567
|
18 |
"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
|
Walther@60567
|
19 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
|
Walther@60567
|
20 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
|
Walther@60567
|
21 |
"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
|
Walther@60567
|
22 |
"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
|
Walther@60567
|
23 |
"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
|
Walther@60567
|
24 |
"-----------------------------------------------------------------------------------------------";
|
Walther@60567
|
25 |
"-----------------------------------------------------------------------------------------------";
|
Walther@60567
|
26 |
"-----------------------------------------------------------------------------------------------";
|
walther@60347
|
27 |
|
walther@60347
|
28 |
val thy = @{theory "EqSystem"};
|
walther@60347
|
29 |
val ctxt = Proof_Context.init_global thy;
|
walther@60347
|
30 |
|
walther@60347
|
31 |
"----------- occur_exactly_in ------------------------------------";
|
walther@60347
|
32 |
"----------- occur_exactly_in ------------------------------------";
|
walther@60347
|
33 |
"----------- occur_exactly_in ------------------------------------";
|
Walther@60660
|
34 |
val all = [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"];
|
Walther@60660
|
35 |
val t = ParseC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
|
walther@60347
|
36 |
|
Walther@60660
|
37 |
if occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2"] all t
|
walther@60347
|
38 |
then () else error "eqsystem.sml occur_exactly_in 1";
|
walther@60347
|
39 |
|
Walther@60660
|
40 |
if not (occur_exactly_in [ParseC.parse_test @{context}"c", ParseC.parse_test @{context}"c_2", ParseC.parse_test @{context}"c_3"] all t)
|
walther@60347
|
41 |
then () else error "eqsystem.sml occur_exactly_in 2";
|
walther@60347
|
42 |
|
Walther@60660
|
43 |
if not (occur_exactly_in [ParseC.parse_test @{context}"c_2"] all t)
|
walther@60347
|
44 |
then () else error "eqsystem.sml occur_exactly_in 3";
|
walther@60347
|
45 |
|
Walther@60660
|
46 |
val t = ParseC.parse_test @{context}"[c,c_2] from [c,c_2,c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
|
walther@60347
|
47 |
eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
48 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
49 |
if str = "[c, c_2] from [c, c_2,\n" ^
|
walther@60347
|
50 |
" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
|
walther@60347
|
51 |
then () else error "eval_occur_exactly_in [c, c_2]";
|
walther@60347
|
52 |
|
Walther@60660
|
53 |
val t = ParseC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
|
walther@60347
|
54 |
"- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
|
walther@60347
|
55 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
56 |
if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
|
walther@60347
|
57 |
" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
|
walther@60347
|
58 |
then () else error "eval_occur_exactly_in [c, c_2, c_3]";
|
walther@60347
|
59 |
|
Walther@60660
|
60 |
val t = ParseC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
|
walther@60347
|
61 |
\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
|
walther@60347
|
62 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
63 |
if str = "[c_2] from [c, c_2,\n" ^
|
walther@60347
|
64 |
" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
|
walther@60347
|
65 |
then () else error "eval_occur_exactly_in [c, c_2, c_3]";
|
walther@60347
|
66 |
|
Walther@60660
|
67 |
val t = ParseC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
|
walther@60347
|
68 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
69 |
if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
|
walther@60347
|
70 |
else error "eval_occur_exactly_in [c, c_2, c_3]";
|
walther@60347
|
71 |
|
walther@60347
|
72 |
val t =
|
Walther@60660
|
73 |
ParseC.parse_test @{context}
|
walther@60347
|
74 |
"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
|
walther@60347
|
75 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
76 |
if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
|
walther@60347
|
77 |
\- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
|
walther@60347
|
78 |
else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
|
walther@60347
|
79 |
|
walther@60347
|
80 |
"----------- problems --------------------------------------------";
|
walther@60347
|
81 |
"----------- problems --------------------------------------------";
|
walther@60347
|
82 |
"----------- problems --------------------------------------------";
|
Walther@60660
|
83 |
val t = ParseC.parse_test @{context} "Length [x+y=1,y=2] = 2";
|
Walther@60650
|
84 |
TermC.atom_trace_detail @{context} t;
|
walther@60347
|
85 |
val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
|
walther@60347
|
86 |
[(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
|
walther@60347
|
87 |
(Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
|
Walther@60516
|
88 |
Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
|
walther@60347
|
89 |
Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
|
walther@60347
|
90 |
];
|
Walther@60500
|
91 |
val SOME (t',_) = rewrite_set_ ctxt false testrls t;
|
Walther@60675
|
92 |
if UnparseC.term @{context} t' = "True" then ()
|
walther@60347
|
93 |
else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
|
walther@60347
|
94 |
|
Walther@60663
|
95 |
val SOME t = ParseC.term_opt ctxt "solution LL";
|
Walther@60650
|
96 |
TermC.atom_trace_detail @{context} t;
|
Walther@60663
|
97 |
val SOME t = ParseC.term_opt ctxt "solution LL";
|
Walther@60650
|
98 |
TermC.atom_trace_detail @{context} t;
|
walther@60347
|
99 |
|
Walther@60660
|
100 |
val t = ParseC.parse_test @{context}
|
walther@60347
|
101 |
"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
|
Walther@60650
|
102 |
TermC.atom_trace_detail @{context} t;
|
Walther@60660
|
103 |
val t = ParseC.parse_test @{context} ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^
|
walther@60347
|
104 |
"(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
|
walther@60347
|
105 |
(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
|
walther@60347
|
106 |
assume flawed test setup hidden by "handle _ => ..."
|
walther@60347
|
107 |
ERROR rewrite__set_ called with 'Erls' for '1 < 1'
|
walther@60347
|
108 |
val SOME (t,_) =
|
Walther@60500
|
109 |
rewrite_set_ ctxt true
|
walther@60347
|
110 |
(Rule_Set.append_rules "prls_" Rule_Set.empty
|
walther@60347
|
111 |
[Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
|
walther@60347
|
112 |
Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
|
walther@60347
|
113 |
Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
|
walther@60347
|
114 |
Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
|
walther@60347
|
115 |
Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
|
walther@60347
|
116 |
]) t;
|
walther@60347
|
117 |
if t = @{term True} then ()
|
walther@60347
|
118 |
else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
|
walther@60347
|
119 |
broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
|
walther@60347
|
120 |
|
walther@60347
|
121 |
|
walther@60347
|
122 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
123 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
124 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
125 |
"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
|
walther@60347
|
126 |
"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
|
Walther@60660
|
127 |
if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
|
Walther@60660
|
128 |
ParseC.parse_test @{context}"c * x") then ()
|
walther@60347
|
129 |
else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
|
walther@60347
|
130 |
|
Walther@60660
|
131 |
if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
|
Walther@60660
|
132 |
ParseC.parse_test @{context}"c_2") then ()
|
walther@60347
|
133 |
else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
|
walther@60347
|
134 |
|
Walther@60660
|
135 |
if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"c * x",
|
Walther@60660
|
136 |
ParseC.parse_test @{context}"c_2") then ()
|
walther@60347
|
137 |
else error "integrate.sml, (c * x) < (c_2) not#3";
|
walther@60347
|
138 |
|
walther@60347
|
139 |
"--- mult.commute ---";
|
Walther@60660
|
140 |
if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"x * c",
|
Walther@60660
|
141 |
ParseC.parse_test @{context}"c * x") then ()
|
walther@60347
|
142 |
else error "integrate.sml, (x * c) < (c * x) not#4";
|
walther@60347
|
143 |
|
Walther@60660
|
144 |
if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
|
Walther@60660
|
145 |
ParseC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")
|
walther@60347
|
146 |
then () else error "integrate.sml, (. * .) < (. * .) not#5";
|
walther@60347
|
147 |
|
Walther@60660
|
148 |
if ord_simplify_System false ctxt [] (ParseC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
|
Walther@60660
|
149 |
ParseC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")
|
walther@60347
|
150 |
then () else error "integrate.sml, (. * .) < (. * .) not#6";
|
walther@60347
|
151 |
|
walther@60347
|
152 |
|
walther@60347
|
153 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
walther@60347
|
154 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
walther@60347
|
155 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
Walther@60660
|
156 |
val t = ParseC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
|
walther@60347
|
157 |
\0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
|
Walther@60660
|
158 |
val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
|
Walther@60660
|
159 |
(ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];
|
Walther@60556
|
160 |
val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
Walther@60675
|
161 |
if UnparseC.term @{context} t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
|
walther@60347
|
162 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
|
walther@60347
|
163 |
|
Walther@60500
|
164 |
val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
|
Walther@60675
|
165 |
if UnparseC.term @{context} t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
|
walther@60347
|
166 |
then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
|
walther@60347
|
167 |
|
Walther@60556
|
168 |
val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
|
Walther@60675
|
169 |
if UnparseC.term @{context} t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
|
walther@60347
|
170 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
|
walther@60347
|
171 |
|
walther@60347
|
172 |
"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
|
Walther@60500
|
173 |
val SOME (t,_) = rewrite_set_ ctxt true order_system t;
|
Walther@60675
|
174 |
if UnparseC.term @{context} t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
|
walther@60347
|
175 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
|
walther@60347
|
176 |
|
Walther@60567
|
177 |
|
walther@60347
|
178 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
179 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
180 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
181 |
val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
|
Walther@60500
|
182 |
val ctxt = Proof_Context.init_global thy;
|
walther@60347
|
183 |
val t =
|
Walther@60660
|
184 |
ParseC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
|
walther@60347
|
185 |
\ - 1 * q_0 / 24 * 0 \<up> 4),\
|
walther@60347
|
186 |
\ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
|
walther@60347
|
187 |
\ - 1 * q_0 / 24 * L \<up> 4)]";
|
Walther@60500
|
188 |
val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
|
Walther@60675
|
189 |
if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
190 |
"[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
|
walther@60347
|
191 |
"[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
|
walther@60347
|
192 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
|
walther@60347
|
193 |
|
Walther@60500
|
194 |
val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
Walther@60675
|
195 |
if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
196 |
"[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
|
walther@60347
|
197 |
"[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
|
walther@60347
|
198 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
|
walther@60347
|
199 |
|
Walther@60500
|
200 |
val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
|
Walther@60675
|
201 |
if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
202 |
"[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
|
walther@60347
|
203 |
"[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
|
walther@60347
|
204 |
then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
|
walther@60347
|
205 |
|
Walther@60500
|
206 |
val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
|
Walther@60675
|
207 |
if UnparseC.term @{context} t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
208 |
"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
|
walther@60347
|
209 |
"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
|
walther@60347
|
210 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
|
walther@60347
|
211 |
|
Walther@60500
|
212 |
val xxx = rewrite_set_ ctxt true order_system t;
|
walther@60347
|
213 |
if is_none xxx
|
walther@60347
|
214 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
|
walther@60347
|
215 |
|
walther@60347
|
216 |
|
walther@60347
|
217 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
walther@60347
|
218 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
walther@60347
|
219 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
Walther@60660
|
220 |
val e1__ = ParseC.parse_test @{context} "c_2 = 77";
|
Walther@60660
|
221 |
val e2__ = ParseC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
|
Walther@60660
|
222 |
val bdvs = [(ParseC.parse_test @{context}"bdv_1",ParseC.parse_test @{context}"c"),
|
Walther@60660
|
223 |
(ParseC.parse_test @{context}"bdv_2",ParseC.parse_test @{context}"c_2")];
|
Walther@60509
|
224 |
val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
|
Walther@60675
|
225 |
if UnparseC.term @{context} e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
|
walther@60347
|
226 |
else error "eqsystem.sml top_down_substitution,2x2] subst";
|
walther@60347
|
227 |
|
walther@60347
|
228 |
val SOME (e2__,_) =
|
Walther@60500
|
229 |
rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
|
Walther@60675
|
230 |
if UnparseC.term @{context} e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
|
walther@60347
|
231 |
else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
|
walther@60347
|
232 |
|
Walther@60500
|
233 |
val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
|
Walther@60675
|
234 |
if UnparseC.term @{context} e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
|
walther@60347
|
235 |
else error "eqsystem.sml top_down_substitution,2x2] isolate";
|
walther@60347
|
236 |
|
Walther@60660
|
237 |
val t = ParseC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
|
Walther@60500
|
238 |
val SOME (t,_) = rewrite_set_ ctxt true order_system t;
|
Walther@60675
|
239 |
if UnparseC.term @{context} t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
|
walther@60347
|
240 |
else error "eqsystem.sml top_down_substitution,2x2] order_system";
|
walther@60347
|
241 |
|
walther@60347
|
242 |
if not (ord_simplify_System
|
Walther@60594
|
243 |
false ctxt []
|
Walther@60660
|
244 |
(ParseC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
|
Walther@60660
|
245 |
ParseC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
|
walther@60347
|
246 |
then () else error "eqsystem.sml, order_result rew_ord";
|
walther@60347
|
247 |
|
walther@60347
|
248 |
|
walther@60347
|
249 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
250 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
251 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
252 |
(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
|
Walther@60660
|
253 |
val t = ParseC.parse_test @{context} (
|
walther@60347
|
254 |
"[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
|
walther@60347
|
255 |
"(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
|
walther@60347
|
256 |
"c + c_2 + c_3 + c_4 = 0, " ^
|
walther@60347
|
257 |
"c_2 + c_3 + c_4 = 0]");
|
Walther@60660
|
258 |
val bdvs = [(ParseC.parse_test @{context}"bdv_1::real",ParseC.parse_test @{context}"c::real"),
|
Walther@60660
|
259 |
(ParseC.parse_test @{context}"bdv_2::real",ParseC.parse_test @{context}"c_2::real"),
|
Walther@60660
|
260 |
(ParseC.parse_test @{context}"bdv_3::real",ParseC.parse_test @{context}"c_3::real"),
|
Walther@60660
|
261 |
(ParseC.parse_test @{context}"bdv_4::real",ParseC.parse_test @{context}"c_4::real")];
|
walther@60347
|
262 |
val SOME (t, _) =
|
Walther@60500
|
263 |
rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
Walther@60675
|
264 |
if UnparseC.term @{context} t = "[0 = c_4, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c_3 + c_4),\n c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
|
walther@60347
|
265 |
then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
|
walther@60347
|
266 |
|
Walther@60500
|
267 |
val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
|
Walther@60675
|
268 |
if UnparseC.term @{context} t = "[c_4 = 0, \
|
walther@60347
|
269 |
\L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
|
walther@60347
|
270 |
\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
|
walther@60347
|
271 |
then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
|
walther@60347
|
272 |
|
Walther@60500
|
273 |
val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
Walther@60675
|
274 |
if UnparseC.term @{context} t = "[c_4 = 0,\
|
walther@60347
|
275 |
\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
|
walther@60347
|
276 |
\ c + (c_2 + (c_3 + c_4)) = 0,\n\
|
walther@60347
|
277 |
\ c_2 + (c_3 + c_4) = 0]"
|
walther@60347
|
278 |
then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
|
walther@60347
|
279 |
|
Walther@60500
|
280 |
val SOME (t, _) = rewrite_set_ ctxt true order_system t;
|
Walther@60675
|
281 |
if UnparseC.term @{context} t = "[c_4 = 0,\
|
walther@60347
|
282 |
\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
|
walther@60347
|
283 |
\ c_2 + (c_3 + c_4) = 0,\n\
|
walther@60347
|
284 |
\ c + (c_2 + (c_3 + c_4)) = 0]"
|
walther@60347
|
285 |
then () else error "eqsystem.sml rewrite in 4x4 order_system";
|
walther@60347
|
286 |
|
Walther@60567
|
287 |
|
Walther@60567
|
288 |
|
walther@60347
|
289 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
290 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
291 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
292 |
val fmz =
|
walther@60347
|
293 |
["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
|
walther@60347
|
294 |
"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
|
walther@60347
|
295 |
"solveForVars [c, c_2]", "solution LL"];
|
walther@60347
|
296 |
|
Walther@60575
|
297 |
(*WN120313 in "solution L" above "Refine.xxxxx @{context} fmz ["LINEAR", "system"]" caused an error...*)
|
Walther@60556
|
298 |
"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
|
Walther@60556
|
299 |
"~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
|
walther@60347
|
300 |
((rev o tl) pblID, fmz, [(*match list*)],
|
Walther@60559
|
301 |
((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
|
Walther@60586
|
302 |
val {thy, model, where_, where_rls, ...} = py ;
|
Walther@60586
|
303 |
"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, model);
|
Walther@60656
|
304 |
val (ts, ctxt) = ContextC.init_while_parsing fmz thy;
|
walther@60347
|
305 |
"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
|
walther@60347
|
306 |
fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
|
walther@60347
|
307 |
(_, _::_) => (Free (v,T)::get_vars vs)
|
walther@60347
|
308 |
| (_, [] ) => get_vars vs) (*filter out nums as long as
|
walther@60347
|
309 |
we have Free ("123",_)*)
|
walther@60347
|
310 |
| get_vars [] = [];
|
walther@60347
|
311 |
t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
|
walther@60347
|
312 |
"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
|
walther@60347
|
313 |
val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
|
walther@60347
|
314 |
val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
|
walther@60347
|
315 |
val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
|
walther@60347
|
316 |
val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
|
walther@60347
|
317 |
val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
|
walther@60347
|
318 |
val t = nth 2 fmz; t = "solveForVars [c, c_2]";
|
walther@60347
|
319 |
val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
|
walther@60347
|
320 |
val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
|
walther@60347
|
321 |
val t = nth 3 fmz; t = "solution LL";
|
walther@60347
|
322 |
(*(Syntax.read_term ctxt t);
|
walther@60347
|
323 |
Type unification failed: Clash of types "real" and "_ list"
|
walther@60347
|
324 |
Type error in application: incompatible operand type
|
walther@60347
|
325 |
|
walther@60347
|
326 |
Operator: solution :: bool list \<Rightarrow> toreall
|
walther@60347
|
327 |
Operand: L :: real ========== L was already present in equalities ========== *)
|
walther@60347
|
328 |
|
walther@60347
|
329 |
"===== case 1 =====";
|
Walther@60575
|
330 |
val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"];
|
walther@60347
|
331 |
case matches of
|
Walther@60556
|
332 |
[M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
|
Walther@60705
|
333 |
M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch !--> continue search !*)
|
Walther@60556
|
334 |
M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
|
Walther@60556
|
335 |
M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
|
Walther@60556
|
336 |
{Find = [Correct "solution LL"], With = [], (**)
|
Walther@60556
|
337 |
Given = [Correct "equalities\n [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\n 0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
|
Walther@60556
|
338 |
Correct "solveForVars [c, c_2]"],
|
Walther@60556
|
339 |
Where = [],
|
Walther@60556
|
340 |
Relate = []})] => ()
|
walther@60347
|
341 |
| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
|
walther@60347
|
342 |
|
walther@60347
|
343 |
"===== case 2 =====";
|
walther@60347
|
344 |
val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
345 |
"solveForVars [c, c_2]", "solution LL"];
|
Walther@60575
|
346 |
val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"];
|
walther@60347
|
347 |
case matches of [_,_,
|
walther@60347
|
348 |
M_Match.Matches
|
walther@60347
|
349 |
(["triangular", "2x2", "LINEAR", "system"],
|
walther@60347
|
350 |
{Find = [Correct "solution LL"],
|
walther@60347
|
351 |
With = [],
|
walther@60347
|
352 |
Given =
|
walther@60347
|
353 |
[Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
354 |
Correct "solveForVars [c, c_2]"],
|
walther@60347
|
355 |
Where = [Correct
|
walther@60347
|
356 |
"tl [c, c_2] from [c, c_2] occur_exactly_in NTH 1\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
357 |
Correct
|
walther@60347
|
358 |
"[c, c_2] from [c, c_2] occur_exactly_in NTH 2\n [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"],
|
walther@60347
|
359 |
Relate = []})] => ()
|
walther@60347
|
360 |
| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
|
walther@60347
|
361 |
|
walther@60347
|
362 |
(*WN051014-----------------------------------------------------------------------------------\\
|
Walther@60575
|
363 |
the above 'val matches = Refine.xxxxx @{context} fmz ["LINEAR", "system"]'
|
walther@60347
|
364 |
didn't work anymore; we investigated in these steps:*)
|
walther@60347
|
365 |
val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
366 |
"solveForVars [c, c_2]", "solution LL"];
|
Walther@60575
|
367 |
val matches = Refine.xxxxx @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
|
walther@60347
|
368 |
(*... resulted in
|
walther@60347
|
369 |
False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
|
walther@60347
|
370 |
[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
|
Walther@60660
|
371 |
val t = ParseC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
|
walther@60347
|
372 |
"[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
|
Walther@60500
|
373 |
|
Walther@60500
|
374 |
val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
|
walther@60347
|
375 |
(*found:...
|
walther@60347
|
376 |
## try thm: NTH_CONS
|
walther@60347
|
377 |
### eval asms: 1 < 2 + - 1
|
walther@60347
|
378 |
==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
|
walther@60347
|
379 |
nth_ (2 + - 1 + - 1) []
|
walther@60347
|
380 |
#### rls: erls_prls_triangular on: 1 < 2 + - 1
|
walther@60347
|
381 |
##### try calc: op <'
|
walther@60347
|
382 |
### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
|
walther@60347
|
383 |
|
Walther@60516
|
384 |
... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
|
walther@60347
|
385 |
(*--------------------------------------------------------------------------------------------//*)
|
walther@60347
|
386 |
|
walther@60347
|
387 |
|
walther@60347
|
388 |
"===== case 3: relaxed preconditions for triangular system =====";
|
walther@60347
|
389 |
val fmz = ["equalities [L * q_0 = c, \
|
walther@60347
|
390 |
\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
|
walther@60347
|
391 |
\ 0 = c_4, \
|
walther@60347
|
392 |
\ 0 = c_3]",
|
walther@60347
|
393 |
"solveForVars [c, c_2, c_3, c_4]", "solution LL"];
|
walther@60347
|
394 |
(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
|
walther@60347
|
395 |
probably exn thrown by fun declare_constraints
|
walther@60347
|
396 |
/-------------------------------------------------------\
|
walther@60347
|
397 |
Type unification failed
|
walther@60347
|
398 |
Type error in application: incompatible operand type
|
walther@60347
|
399 |
|
walther@60347
|
400 |
Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
|
walther@60347
|
401 |
Operand: [c_4] :: 'b list
|
walther@60347
|
402 |
\-------------------------------------------------------/
|
walther@60347
|
403 |
val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
|
walther@60347
|
404 |
case TermC.matches of
|
walther@60347
|
405 |
[M_Match.Matches (["LINEAR", "system"], _),
|
walther@60347
|
406 |
M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
|
walther@60347
|
407 |
M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
|
walther@60347
|
408 |
M_Match.Matches (["4x4", "LINEAR", "system"], _),
|
walther@60347
|
409 |
M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
|
walther@60347
|
410 |
M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
|
walther@60347
|
411 |
| _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
|
walther@60347
|
412 |
(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
|
walther@60347
|
413 |
|
walther@60347
|
414 |
"===== case 4 =====";
|
walther@60347
|
415 |
val fmz = ["equalities [L * q_0 = c, \
|
walther@60347
|
416 |
\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
|
walther@60347
|
417 |
\ 0 = c_3, \
|
walther@60347
|
418 |
\ 0 = c_4]",
|
walther@60347
|
419 |
"solveForVars [c, c_2, c_3, c_4]", "solution LL"];
|
walther@60347
|
420 |
val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
|
walther@60347
|
421 |
case TermC.matches of
|
walther@60347
|
422 |
[M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
|
walther@60347
|
423 |
| _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
|
walther@60347
|
424 |
val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
|
walther@60347
|
425 |
============ inhibit exn WN120314 ==============================================*)
|
walther@60347
|
426 |
|
Walther@60567
|
427 |
|
Walther@60567
|
428 |
|
walther@60347
|
429 |
"----------- Refine.refine [2x2,linear,system] search error--------------";
|
walther@60347
|
430 |
"----------- Refine.refine [2x2,linear,system] search error--------------";
|
walther@60347
|
431 |
"----------- Refine.refine [2x2,linear,system] search error--------------";
|
walther@60347
|
432 |
(*didn't go into ["2x2", "LINEAR", "system"];
|
walther@60347
|
433 |
we investigated in these steps:*)
|
walther@60347
|
434 |
val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
|
walther@60347
|
435 |
\0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
|
walther@60347
|
436 |
"solveForVars [c, c_2]", "solution LL"];
|
Walther@60575
|
437 |
val matches = Refine.xxxxx @{context} fmz ["2x2", "LINEAR", "system"];
|
walther@60347
|
438 |
(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
|
walther@60347
|
439 |
(*brought: 'False "length_ es_ = 2"'*)
|
walther@60347
|
440 |
|
walther@60347
|
441 |
(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
|
walther@60347
|
442 |
(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
|
walther@60347
|
443 |
(rev ["LINEAR", "system"], fmz, [(*match list*)],
|
walther@60347
|
444 |
((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
|
walther@60347
|
445 |
*)
|
Walther@60675
|
446 |
> show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;
|
walther@60347
|
447 |
val it = "length_ (es_::real list) = (2::real)" : string
|
walther@60347
|
448 |
|
walther@60347
|
449 |
=========================================================================\
|
walther@60347
|
450 |
-------fun Problem.prep_input
|
walther@60347
|
451 |
(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
|
walther@60347
|
452 |
ev:rls, ca: string option, metIDs:metID list)) =
|
walther@60347
|
453 |
(EqSystem.thy, (["system"],
|
walther@60347
|
454 |
[("#Given" ,["equalities es_", "solveForVars v_s"]),
|
walther@60347
|
455 |
("#Find" ,["solution ss___"](*___ is copy-named*))
|
walther@60347
|
456 |
],
|
walther@60347
|
457 |
Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
|
walther@60347
|
458 |
SOME "solveSystem es_ v_s",
|
walther@60347
|
459 |
[]));
|
walther@60347
|
460 |
*)
|
walther@60347
|
461 |
> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
|
walther@60347
|
462 |
val equalities_es_ = "equalities es_" : string
|
Walther@60583
|
463 |
> val (dd, ii) = ((Model_Pattern.split_descriptor ctxt) o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
|
Walther@60675
|
464 |
> show_types:=true; UnparseC.term @{context} ii; show_types:=false;
|
walther@60347
|
465 |
val it = "es_::bool list" : string
|
walther@60347
|
466 |
~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
walther@60347
|
467 |
|
walther@60347
|
468 |
> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
|
Walther@60675
|
469 |
> show_types:=true; UnparseC.term @{context} (hd where_); show_types:=false;
|
walther@60347
|
470 |
|
walther@60347
|
471 |
=========================================================================/
|
walther@60347
|
472 |
|
walther@60347
|
473 |
-----fun refin' ff:
|
walther@60360
|
474 |
> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
|
walther@60347
|
475 |
[
|
walther@60347
|
476 |
(1 ,[1] ,true ,#Given ,Cor equalities
|
walther@60347
|
477 |
[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
|
walther@60347
|
478 |
0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2] ,(es_, [[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
|
walther@60347
|
479 |
0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
|
walther@60347
|
480 |
(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
|
walther@60347
|
481 |
(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
|
walther@60347
|
482 |
|
walther@60347
|
483 |
> (writeln o pres2str) pre';
|
walther@60347
|
484 |
[
|
walther@60347
|
485 |
(false, length_ es_ = 2),
|
walther@60347
|
486 |
(true, length_ [c, c_2] = 2)]
|
walther@60347
|
487 |
|
walther@60347
|
488 |
----- fun match_oris':
|
walther@60360
|
489 |
> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
|
walther@60347
|
490 |
> (writeln o pres2str) pre';
|
walther@60347
|
491 |
..as in refin'
|
walther@60347
|
492 |
|
walther@60347
|
493 |
----- fun check in Pre_Conds.
|
walther@60347
|
494 |
> (writeln o env2str) env;
|
walther@60347
|
495 |
["
|
walther@60347
|
496 |
(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
|
walther@60347
|
497 |
0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
|
walther@60347
|
498 |
(v_s, [c, c_2])", "
|
walther@60347
|
499 |
(ss___, L)"]
|
walther@60347
|
500 |
|
walther@60347
|
501 |
> val es_ = (fst o hd) env;
|
walther@60347
|
502 |
val es_ = Free ("es_", "bool List.list") : Term.term
|
walther@60347
|
503 |
|
walther@60347
|
504 |
> val pre1 = hd pres;
|
Walther@60650
|
505 |
TermC.atom_trace_detail @{context} pre1;
|
walther@60347
|
506 |
***
|
walther@60347
|
507 |
*** Const (op =, [real, real] => bool)
|
walther@60347
|
508 |
*** . Const (ListG.length_, real list => real)
|
walther@60347
|
509 |
*** . . Free (es_, real list)
|
walther@60347
|
510 |
~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
|
walther@60347
|
511 |
*** . Free (2, real)
|
walther@60347
|
512 |
***
|
walther@60347
|
513 |
|
walther@60347
|
514 |
THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
|
walther@60347
|
515 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
walther@60347
|
516 |
*)
|
walther@60347
|
517 |
|
Walther@60567
|
518 |
|
Walther@60556
|
519 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
Walther@60556
|
520 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
Walther@60556
|
521 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
Walther@60706
|
522 |
(*this test fails, see TODO WN230404*)
|
Walther@60567
|
523 |
val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
|
Walther@60567
|
524 |
"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
|
walther@60347
|
525 |
"solveForVars [c, c_2]", "solution LL"];
|
walther@60347
|
526 |
val (dI',pI',mI') =
|
walther@60347
|
527 |
("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
|
walther@60347
|
528 |
["EqSystem", "normalise", "2x2"]);
|
walther@60347
|
529 |
val p = e_pos'; val c = [];
|
Walther@60571
|
530 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
|
walther@60347
|
531 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
532 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
533 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
534 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
535 |
case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
|
walther@60347
|
536 |
| _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
|
walther@60347
|
537 |
|
walther@60347
|
538 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
539 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
Walther@60567
|
540 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
541 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
542 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
543 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
544 |
case nxt of
|
walther@60347
|
545 |
(Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
|
walther@60347
|
546 |
| _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
|
walther@60347
|
547 |
|
Walther@60706
|
548 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
Walther@60706
|
549 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]" = nxt;
|
Walther@60706
|
550 |
|
Walther@60706
|
551 |
(*ERROR WN230404: mk_env not reasonable for "Cor_TEST equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(e_s, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])"*)
|
Walther@60706
|
552 |
(** )val return_Add_Given_equ
|
Walther@60706
|
553 |
= me nxt p c pt;( **)
|
Walther@60706
|
554 |
(*//------------------ step into Add_Given_equ ---------------------------------------------\\*);
|
Walther@60706
|
555 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
|
Walther@60706
|
556 |
val ctxt = Ctree.get_ctxt pt p
|
Walther@60706
|
557 |
val ("ok", (_, _, (pt, p))) =
|
Walther@60706
|
558 |
(*case*) Step.by_tactic tac (pt, p) (*of*);
|
Walther@60706
|
559 |
|
Walther@60706
|
560 |
(** ) (*case*)
|
Walther@60706
|
561 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);( **)
|
Walther@60706
|
562 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
|
Walther@60706
|
563 |
(p, ((pt, Pos.e_pos'), []));
|
Walther@60706
|
564 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60706
|
565 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60706
|
566 |
val _ =
|
Walther@60706
|
567 |
(*case*) tacis (*of*);
|
Walther@60706
|
568 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60706
|
569 |
|
Walther@60706
|
570 |
(** ) switch_specify_solve p_ (pt, ip);( **)
|
Walther@60706
|
571 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60706
|
572 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60706
|
573 |
|
Walther@60706
|
574 |
(** ) specify_do_next (pt, input_pos);( **)
|
Walther@60706
|
575 |
"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
Walther@60706
|
576 |
|
Walther@60706
|
577 |
(** )val (_, (p_', tac)) =
|
Walther@60706
|
578 |
Specify.find_next_step ptp;( **)
|
Walther@60706
|
579 |
"~~~~~ fun find_next_step , args:"; val (ptp as (pt, (p, p_))) = (ptp);
|
Walther@60706
|
580 |
|
Walther@60706
|
581 |
(** )val (_, (p_', tac)) =
|
Walther@60706
|
582 |
Specify.find_next_step ptp;( **);
|
Walther@60706
|
583 |
"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
|
Walther@60706
|
584 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
Walther@60706
|
585 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60706
|
586 |
val ctxt = Ctree.get_ctxt pt pos;
|
Walther@60706
|
587 |
(*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
|
Walther@60706
|
588 |
(*if*) p_ = Pos.Pbl (*then*);
|
Walther@60706
|
589 |
|
Walther@60706
|
590 |
(** )Specify.for_problem ctxt oris (o_refs, refs) (pbl, met); ( **)
|
Walther@60706
|
591 |
"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
|
Walther@60706
|
592 |
(ctxt, oris, (o_refs, refs), (pbl, met));
|
Walther@60706
|
593 |
val cpI = if pI = Problem.id_empty then pI' else pI;
|
Walther@60706
|
594 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60706
|
595 |
val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
|
Walther@60706
|
596 |
val {model = mpc, ...} = MethodC.from_store ctxt cmI
|
Walther@60706
|
597 |
|
Walther@60706
|
598 |
(** )val (preok, _) =
|
Walther@60706
|
599 |
Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); ( **);
|
Walther@60706
|
600 |
"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
|
Walther@60706
|
601 |
(ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
|
Walther@60706
|
602 |
|
Walther@60706
|
603 |
(** )val (env_subst, env_eval) =
|
Walther@60706
|
604 |
sep_variants_envs_OLD model_patt i_model ( **)
|
Walther@60706
|
605 |
"~~~~~ fun sep_variants_envs_OLD , args:"; val (model_patt, i_model) = (model_patt, i_model);
|
Walther@60706
|
606 |
val equal_descr_pairs =
|
Walther@60706
|
607 |
map (get_equal_descr i_model) model_patt
|
Walther@60706
|
608 |
|> flat
|
Walther@60706
|
609 |
val all_variants =
|
Walther@60706
|
610 |
map (fn (_, (_, variants, _, _, _)) => variants) equal_descr_pairs
|
Walther@60706
|
611 |
|> flat
|
Walther@60706
|
612 |
|> distinct op =
|
Walther@60706
|
613 |
val variants_separated = map (filter_variants equal_descr_pairs) all_variants
|
Walther@60706
|
614 |
val restricted_to_given = map (filter (fn ((m_field, (_, _)), (_, _, _, _, (_, _))) =>
|
Walther@60706
|
615 |
m_field = "#Given")) variants_separated;
|
Walther@60706
|
616 |
|
Walther@60706
|
617 |
(** )val envs_subst = map
|
Walther@60706
|
618 |
mk_env_subst restricted_to_given ( **)
|
Walther@60706
|
619 |
"~~~~~ fun mk_env_subst , args:"; val (equal_descr_pairs) = (nth 1 (nth 1 restricted_to_given));
|
Walther@60706
|
620 |
|
Walther@60706
|
621 |
val xxx =
|
Walther@60706
|
622 |
(*+*)(fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
|
Walther@60706
|
623 |
=> (mk_env feedb) |> map fst (*dummy rhs dropped*)|> map (pair id))
|
Walther@60706
|
624 |
: Model_Pattern.single * I_Model.single_TEST -> Pre_Conds.env_subst;
|
Walther@60706
|
625 |
(*+*)equal_descr_pairs: Model_Pattern.single * I_Model.single_TEST;
|
Walther@60706
|
626 |
|
Walther@60706
|
627 |
(** ) xxx equal_descr_pairs ( **)
|
Walther@60706
|
628 |
"~~~~~ fun xxx , args:"; val (((_, (_, id)), (_, _, _, _, (feedb, _)))) = (equal_descr_pairs);
|
Walther@60706
|
629 |
(*ERROR WN230404 (see TODO.md:
|
Walther@60706
|
630 |
mk_env not reasonable for "Cor_TEST equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(e_s, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])" (**)
|
Walther@60706
|
631 |
(mk_env feedb) *)
|
Walther@60706
|
632 |
|
Walther@60706
|
633 |
(*+*)feedb: Model_Def.i_model_feedback_TEST;
|
Walther@60706
|
634 |
(*+*)(*----^^^^^^^^^^^^^^^^^^*)
|
Walther@60706
|
635 |
(*+*) I_Model.Cor_TEST: (descriptor * term list) * (term * term list) -> feedback_TEST;
|
Walther@60706
|
636 |
(*+*)Model_Def.Cor_TEST: (descriptor * term list) * (term * term list) -> Model_Def.i_model_feedback_TEST;
|
Walther@60706
|
637 |
(*\\------------------ step into Add_Given_equ ---------------------------------------------//*)
|
Walther@60706
|
638 |
|
Walther@60706
|
639 |
|
Walther@60706
|
640 |
(*-------------------- step Add_Given_equ failed, thus the following is outcommended ---------* )
|
Walther@60706
|
641 |
val (p,_,f,nxt,_,pt) = return_Add_Given_equ; (**)val Add_Given "solveForVars [c]" = nxt;(**)
|
Walther@60706
|
642 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "solveForVars [c_2]" = nxt;
|
Walther@60706
|
643 |
|
walther@60347
|
644 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
645 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
646 |
case nxt of
|
walther@60347
|
647 |
(Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
|
walther@60347
|
648 |
| _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
|
walther@60347
|
649 |
|
walther@60347
|
650 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
651 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
652 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
653 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
654 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
655 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
656 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
657 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
658 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
659 |
case nxt of
|
walther@60347
|
660 |
(Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
|
walther@60347
|
661 |
| _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
|
walther@60347
|
662 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
663 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
Walther@60567
|
664 |
(* final test ... ----------------------------------------------------------------------------*)
|
walther@60347
|
665 |
if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
|
walther@60347
|
666 |
else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
|
Walther@60567
|
667 |
|
walther@60347
|
668 |
case nxt of
|
walther@60347
|
669 |
(End_Proof') => ()
|
walther@60347
|
670 |
| _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
|
Walther@60567
|
671 |
|
Walther@60567
|
672 |
Test_Tool.show_pt pt (*[
|
Walther@60567
|
673 |
(([], Frm), solveSystem
|
Walther@60567
|
674 |
[[0 = - 1 * q_0 * 0 \<up> 2 div 2 + 0 * c + c_2],
|
Walther@60567
|
675 |
[0 = - 1 * q_0 * L \<up> 2 div 2 + L * c + c_2]]
|
Walther@60567
|
676 |
[[c], [c_2]]),
|
Walther@60567
|
677 |
(([1], Frm), [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
|
Walther@60567
|
678 |
0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]),
|
Walther@60567
|
679 |
(([1], Res), [0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]),
|
Walther@60567
|
680 |
(([2], Res), [0 = c_2, 0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2)]),
|
Walther@60567
|
681 |
(([3], Res), [c_2 = 0, L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2)]),
|
Walther@60567
|
682 |
(([4], Res), [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]),
|
Walther@60567
|
683 |
(([5], Pbl), solveSystem [L * c + c_2 = q_0 * L \<up> 2 / 2] [c_2]),
|
Walther@60567
|
684 |
(([5, 1], Frm), L * c + c_2 = q_0 * L \<up> 2 / 2),
|
Walther@60567
|
685 |
(([5, 1], Res), L * c + 0 = q_0 * L \<up> 2 / 2),
|
Walther@60567
|
686 |
(([5, 2], Res), L * c = q_0 * L \<up> 2 / 2),
|
Walther@60567
|
687 |
(([5, 3], Res), c = q_0 * L \<up> 2 / 2 / L),
|
Walther@60567
|
688 |
(([5, 4], Res), c = L * q_0 / 2),
|
Walther@60567
|
689 |
(([5, 5], Frm), [c_2 = 0, c = L * q_0 / 2]),
|
Walther@60567
|
690 |
(([5, 5], Res), [c = L * q_0 / 2, c_2 = 0]),
|
Walther@60567
|
691 |
(([5], Res), [c = L * q_0 / 2, c_2 = 0]),
|
Walther@60567
|
692 |
(([], Res), [c = L * q_0 / 2, c_2 = 0])]
|
Walther@60567
|
693 |
*)
|
Walther@60706
|
694 |
( *-------------------- step Add_Given_equ failed, thus the above is outcommended -----------//*)
|