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@60347
|
6 |
"-----------------------------------------------------------------";
|
walther@60347
|
7 |
"table of contents -----------------------------------------------";
|
walther@60347
|
8 |
"-----------------------------------------------------------------";
|
walther@60347
|
9 |
"----------- occur_exactly_in ------------------------------------";
|
walther@60347
|
10 |
"----------- problems --------------------------------------------";
|
walther@60347
|
11 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
12 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
walther@60347
|
13 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
14 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
walther@60347
|
15 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
16 |
"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
|
walther@60347
|
17 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
18 |
"----------- refine [2x2,linear,system] search error--------------";
|
Walther@60556
|
19 |
(*^^^--- eqsystem-1.sml #####################################################################*)
|
Walther@60556
|
20 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
Walther@60556
|
21 |
(*^^^--- eqsystem-1a.sml #####################################################################
|
Walther@60556
|
22 |
vvv--- eqsystem-2.sml #####################################################################*)
|
walther@60347
|
23 |
"----------- me [linear,system] ..normalise..top_down_sub..-------";
|
walther@60347
|
24 |
"----------- all systems from Biegelinie -------------------------";
|
walther@60347
|
25 |
"----------- 4x4 systems from Biegelinie -------------------------";
|
walther@60347
|
26 |
"-----------------------------------------------------------------";
|
walther@60347
|
27 |
"-----------------------------------------------------------------";
|
walther@60347
|
28 |
"-----------------------------------------------------------------";
|
walther@60347
|
29 |
|
walther@60347
|
30 |
val thy = @{theory "EqSystem"};
|
walther@60347
|
31 |
val ctxt = Proof_Context.init_global thy;
|
walther@60347
|
32 |
|
walther@60347
|
33 |
"----------- occur_exactly_in ------------------------------------";
|
walther@60347
|
34 |
"----------- occur_exactly_in ------------------------------------";
|
walther@60347
|
35 |
"----------- occur_exactly_in ------------------------------------";
|
Walther@60565
|
36 |
val all = [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"];
|
Walther@60565
|
37 |
val t = TermC.parse_test @{context}"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
|
walther@60347
|
38 |
|
Walther@60565
|
39 |
if occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2"] all t
|
walther@60347
|
40 |
then () else error "eqsystem.sml occur_exactly_in 1";
|
walther@60347
|
41 |
|
Walther@60565
|
42 |
if not (occur_exactly_in [TermC.parse_test @{context}"c", TermC.parse_test @{context}"c_2", TermC.parse_test @{context}"c_3"] all t)
|
walther@60347
|
43 |
then () else error "eqsystem.sml occur_exactly_in 2";
|
walther@60347
|
44 |
|
Walther@60565
|
45 |
if not (occur_exactly_in [TermC.parse_test @{context}"c_2"] all t)
|
walther@60347
|
46 |
then () else error "eqsystem.sml occur_exactly_in 3";
|
walther@60347
|
47 |
|
Walther@60565
|
48 |
val t = TermC.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
|
49 |
eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
50 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
51 |
if str = "[c, c_2] from [c, c_2,\n" ^
|
walther@60347
|
52 |
" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
|
walther@60347
|
53 |
then () else error "eval_occur_exactly_in [c, c_2]";
|
walther@60347
|
54 |
|
Walther@60565
|
55 |
val t = TermC.parse_test @{context} ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
|
walther@60347
|
56 |
"- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
|
walther@60347
|
57 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
58 |
if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
|
walther@60347
|
59 |
" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
|
walther@60347
|
60 |
then () else error "eval_occur_exactly_in [c, c_2, c_3]";
|
walther@60347
|
61 |
|
Walther@60565
|
62 |
val t = TermC.parse_test @{context}"[c_2] from [c,c_2,c_3] occur_exactly_in \
|
walther@60347
|
63 |
\- 1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
|
walther@60347
|
64 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
65 |
if str = "[c_2] from [c, c_2,\n" ^
|
walther@60347
|
66 |
" c_3] occur_exactly_in - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
|
walther@60347
|
67 |
then () else error "eval_occur_exactly_in [c, c_2, c_3]";
|
walther@60347
|
68 |
|
Walther@60565
|
69 |
val t = TermC.parse_test @{context}"[] from [c,c_2,c_3] occur_exactly_in 0";
|
walther@60347
|
70 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
71 |
if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
|
walther@60347
|
72 |
else error "eval_occur_exactly_in [c, c_2, c_3]";
|
walther@60347
|
73 |
|
walther@60347
|
74 |
val t =
|
Walther@60565
|
75 |
TermC.parse_test @{context}
|
walther@60347
|
76 |
"[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) /2";
|
walther@60347
|
77 |
val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
|
walther@60347
|
78 |
if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
|
walther@60347
|
79 |
\- 1 * (q_0 * L \<up> 2) / 2 = True" then ()
|
walther@60347
|
80 |
else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
|
walther@60347
|
81 |
|
walther@60347
|
82 |
"----------- problems --------------------------------------------";
|
walther@60347
|
83 |
"----------- problems --------------------------------------------";
|
walther@60347
|
84 |
"----------- problems --------------------------------------------";
|
Walther@60565
|
85 |
val t = TermC.parse_test @{context} "Length [x+y=1,y=2] = 2";
|
walther@60347
|
86 |
TermC.atomty t;
|
walther@60347
|
87 |
val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
|
walther@60347
|
88 |
[(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
|
walther@60347
|
89 |
(Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
|
Walther@60516
|
90 |
Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
|
walther@60347
|
91 |
Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
|
walther@60347
|
92 |
];
|
Walther@60500
|
93 |
val SOME (t',_) = rewrite_set_ ctxt false testrls t;
|
walther@60347
|
94 |
if UnparseC.term t' = "True" then ()
|
walther@60347
|
95 |
else error "eqsystem.sml: length_ [x+y=1,y=2] = 2";
|
walther@60347
|
96 |
|
Walther@60424
|
97 |
val SOME t = TermC.parseNEW ctxt "solution LL";
|
Walther@60424
|
98 |
TermC.atomty t;
|
Walther@60424
|
99 |
val SOME t = TermC.parseNEW ctxt "solution LL";
|
Walther@60424
|
100 |
TermC.atomty t;
|
walther@60347
|
101 |
|
Walther@60565
|
102 |
val t = TermC.parse_test @{context}
|
walther@60347
|
103 |
"(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))";
|
walther@60347
|
104 |
TermC.atomty t;
|
Walther@60565
|
105 |
val t = TermC.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
|
106 |
"(NTH 1 [c_4 = 1, 2 = 2, 3 = 3, 4 = 4])");
|
walther@60347
|
107 |
(*----- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----\\
|
walther@60347
|
108 |
assume flawed test setup hidden by "handle _ => ..."
|
walther@60347
|
109 |
ERROR rewrite__set_ called with 'Erls' for '1 < 1'
|
walther@60347
|
110 |
val SOME (t,_) =
|
Walther@60500
|
111 |
rewrite_set_ ctxt true
|
walther@60347
|
112 |
(Rule_Set.append_rules "prls_" Rule_Set.empty
|
walther@60347
|
113 |
[Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
|
walther@60347
|
114 |
Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
|
walther@60347
|
115 |
Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
|
walther@60347
|
116 |
Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
|
walther@60347
|
117 |
Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
|
walther@60347
|
118 |
]) t;
|
walther@60347
|
119 |
if t = @{term True} then ()
|
walther@60347
|
120 |
else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
|
walther@60347
|
121 |
broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite ---//*)
|
walther@60347
|
122 |
|
walther@60347
|
123 |
|
walther@60347
|
124 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
125 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
126 |
"----------- rewrite-order ord_simplify_System -------------------";
|
walther@60347
|
127 |
"M_b x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";
|
walther@60347
|
128 |
"--- add.commute ---"; (* ... add.commute cf. b42e334c97ee *)
|
Walther@60565
|
129 |
if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
|
Walther@60565
|
130 |
TermC.parse_test @{context}"c * x") then ()
|
walther@60347
|
131 |
else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c * x) not#1";
|
walther@60347
|
132 |
|
Walther@60565
|
133 |
if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2)",
|
Walther@60565
|
134 |
TermC.parse_test @{context}"c_2") then ()
|
walther@60347
|
135 |
else error "integrate.sml, (- 1 * q_0 * (x \<up> 2 / 2)) < (c_2) not#2";
|
walther@60347
|
136 |
|
Walther@60565
|
137 |
if ord_simplify_System false thy [] (TermC.parse_test @{context}"c * x",
|
Walther@60565
|
138 |
TermC.parse_test @{context}"c_2") then ()
|
walther@60347
|
139 |
else error "integrate.sml, (c * x) < (c_2) not#3";
|
walther@60347
|
140 |
|
walther@60347
|
141 |
"--- mult.commute ---";
|
Walther@60565
|
142 |
if ord_simplify_System false thy [] (TermC.parse_test @{context}"x * c",
|
Walther@60565
|
143 |
TermC.parse_test @{context}"c * x") then ()
|
walther@60347
|
144 |
else error "integrate.sml, (x * c) < (c * x) not#4";
|
walther@60347
|
145 |
|
Walther@60565
|
146 |
if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
|
Walther@60565
|
147 |
TermC.parse_test @{context}"- 1 * q_0 * c * (x \<up> 2 / 2)")
|
walther@60347
|
148 |
then () else error "integrate.sml, (. * .) < (. * .) not#5";
|
walther@60347
|
149 |
|
Walther@60565
|
150 |
if ord_simplify_System false thy [] (TermC.parse_test @{context}"- 1 * q_0 * (x \<up> 2 / 2) * c",
|
Walther@60565
|
151 |
TermC.parse_test @{context}"c * - 1 * q_0 * (x \<up> 2 / 2)")
|
walther@60347
|
152 |
then () else error "integrate.sml, (. * .) < (. * .) not#6";
|
walther@60347
|
153 |
|
walther@60347
|
154 |
|
walther@60347
|
155 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
walther@60347
|
156 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
walther@60347
|
157 |
"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
|
Walther@60565
|
158 |
val t = TermC.parse_test @{context}"[0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2,\
|
walther@60347
|
159 |
\0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2]";
|
Walther@60565
|
160 |
val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
|
Walther@60565
|
161 |
(TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
|
Walther@60556
|
162 |
val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
walther@60347
|
163 |
if UnparseC.term t = "[0 = - 1 * q_0 * L \<up> 2 / 2 + (L * c + c_2), 0 = c_2]"
|
walther@60347
|
164 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1";
|
walther@60347
|
165 |
|
Walther@60500
|
166 |
val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
|
walther@60347
|
167 |
if UnparseC.term t = "[L * c + c_2 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2), c_2 = 0]"
|
walther@60347
|
168 |
then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs";
|
walther@60347
|
169 |
|
Walther@60556
|
170 |
val SOME (t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
|
walther@60347
|
171 |
if UnparseC.term t = "[L * c + c_2 = q_0 * L \<up> 2 / 2, c_2 = 0]"
|
walther@60347
|
172 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.2";
|
walther@60347
|
173 |
|
walther@60347
|
174 |
"--- 3--- see EqSystem.thy (*..if replaced by 'and' ...*)";
|
Walther@60500
|
175 |
val SOME (t,_) = rewrite_set_ ctxt true order_system t;
|
walther@60347
|
176 |
if UnparseC.term t = "[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"
|
walther@60347
|
177 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.3";
|
walther@60347
|
178 |
|
walther@60347
|
179 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
180 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
181 |
"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
|
walther@60347
|
182 |
val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
|
Walther@60500
|
183 |
val ctxt = Proof_Context.init_global thy;
|
walther@60347
|
184 |
val t =
|
Walther@60565
|
185 |
TermC.parse_test @{context}"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 \<up> 3 + \
|
walther@60347
|
186 |
\ - 1 * q_0 / 24 * 0 \<up> 4),\
|
walther@60347
|
187 |
\ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L \<up> 3 + \
|
walther@60347
|
188 |
\ - 1 * q_0 / 24 * L \<up> 4)]";
|
Walther@60500
|
189 |
val SOME (t, _) = rewrite_set_ ctxt true norm_Rational t;
|
walther@60347
|
190 |
if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
191 |
"[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
|
walther@60347
|
192 |
"[0 = c_2, 0 = (24 * c_2 + 24 * L * c + L \<up> 4 * q_0) / 24]"
|
walther@60347
|
193 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
|
walther@60347
|
194 |
|
Walther@60500
|
195 |
val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
walther@60347
|
196 |
if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
197 |
"[c_2 = 0, 0 = q_0 * L \<up> 4 / (24 * EI) + (L * c + c_2)]"*)
|
walther@60347
|
198 |
"[0 = c_2, 0 = q_0 * L \<up> 4 / 24 + (L * c + c_2)]"
|
walther@60347
|
199 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
|
walther@60347
|
200 |
|
Walther@60500
|
201 |
val SOME (t,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
|
walther@60347
|
202 |
if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
203 |
"[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / (24 * EI))]"*)
|
walther@60347
|
204 |
"[c_2 = 0, L * c + c_2 = 0 + - 1 * (q_0 * L \<up> 4 / 24)]"
|
walther@60347
|
205 |
then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
|
walther@60347
|
206 |
|
Walther@60500
|
207 |
val SOME(t,_)= rewrite_set_inst_ ctxt true bdvs simplify_System t;
|
walther@60347
|
208 |
if UnparseC.term t = (*BEFORE "eliminate ThmC.numerals_to_Free"..
|
walther@60347
|
209 |
"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / (24 * EI)]"*)
|
walther@60347
|
210 |
"[c_2 = 0, L * c + c_2 = - 1 * q_0 * L \<up> 4 / 24]"
|
walther@60347
|
211 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
|
walther@60347
|
212 |
|
Walther@60500
|
213 |
val xxx = rewrite_set_ ctxt true order_system t;
|
walther@60347
|
214 |
if is_none xxx
|
walther@60347
|
215 |
then () else error "eqsystem.sml rewrite in 2x2 simplify_System.3b";
|
walther@60347
|
216 |
|
walther@60347
|
217 |
|
walther@60347
|
218 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
walther@60347
|
219 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
walther@60347
|
220 |
"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
|
Walther@60565
|
221 |
val e1__ = TermC.parse_test @{context} "c_2 = 77";
|
Walther@60565
|
222 |
val e2__ = TermC.parse_test @{context} "L * c + c_2 = q_0 * L \<up> 2 / 2";
|
Walther@60565
|
223 |
val bdvs = [(TermC.parse_test @{context}"bdv_1",TermC.parse_test @{context}"c"),
|
Walther@60565
|
224 |
(TermC.parse_test @{context}"bdv_2",TermC.parse_test @{context}"c_2")];
|
Walther@60509
|
225 |
val SOME (e2__,_) = rewrite_terms_ ctxt Rewrite_Ord.function_empty Rule_Set.Empty [e1__] e2__;
|
walther@60347
|
226 |
if UnparseC.term e2__ = "L * c + 77 = q_0 * L \<up> 2 / 2" then ()
|
walther@60347
|
227 |
else error "eqsystem.sml top_down_substitution,2x2] subst";
|
walther@60347
|
228 |
|
walther@60347
|
229 |
val SOME (e2__,_) =
|
Walther@60500
|
230 |
rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized e2__;
|
walther@60347
|
231 |
if UnparseC.term e2__ = "77 + L * c = q_0 * L \<up> 2 / 2" then ()
|
walther@60347
|
232 |
else error "eqsystem.sml top_down_substitution,2x2] simpl_par";
|
walther@60347
|
233 |
|
Walther@60500
|
234 |
val SOME (e2__,_) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs e2__;
|
walther@60347
|
235 |
if UnparseC.term e2__ = "c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L" then ()
|
walther@60347
|
236 |
else error "eqsystem.sml top_down_substitution,2x2] isolate";
|
walther@60347
|
237 |
|
Walther@60565
|
238 |
val t = TermC.parse_test @{context} "[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]";
|
Walther@60500
|
239 |
val SOME (t,_) = rewrite_set_ ctxt true order_system t;
|
walther@60347
|
240 |
if UnparseC.term t = "[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]" then ()
|
walther@60347
|
241 |
else error "eqsystem.sml top_down_substitution,2x2] order_system";
|
walther@60347
|
242 |
|
walther@60347
|
243 |
if not (ord_simplify_System
|
walther@60347
|
244 |
false thy []
|
Walther@60565
|
245 |
(TermC.parse_test @{context}"[c_2 = 77, c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L]",
|
Walther@60565
|
246 |
TermC.parse_test @{context}"[c = (q_0 * L \<up> 2 / 2 + - 1 * 77) / L, c_2 = 77]"))
|
walther@60347
|
247 |
then () else error "eqsystem.sml, order_result rew_ord";
|
walther@60347
|
248 |
|
walther@60347
|
249 |
|
walther@60347
|
250 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
251 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
252 |
"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
|
walther@60347
|
253 |
(*STOPPED.WN06?: revise rewrite in [EqSystem,normalise,4x4] from before 0609*)
|
Walther@60565
|
254 |
val t = TermC.parse_test @{context} (
|
walther@60347
|
255 |
"[(0::real) = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c_3 + c_4, " ^
|
walther@60347
|
256 |
"(0::real) = - 1 * q_0 * L \<up> 2 / 2 + L * c_3 + c_4, " ^
|
walther@60347
|
257 |
"c + c_2 + c_3 + c_4 = 0, " ^
|
walther@60347
|
258 |
"c_2 + c_3 + c_4 = 0]");
|
Walther@60565
|
259 |
val bdvs = [(TermC.parse_test @{context}"bdv_1::real",TermC.parse_test @{context}"c::real"),
|
Walther@60565
|
260 |
(TermC.parse_test @{context}"bdv_2::real",TermC.parse_test @{context}"c_2::real"),
|
Walther@60565
|
261 |
(TermC.parse_test @{context}"bdv_3::real",TermC.parse_test @{context}"c_3::real"),
|
Walther@60565
|
262 |
(TermC.parse_test @{context}"bdv_4::real",TermC.parse_test @{context}"c_4::real")];
|
walther@60347
|
263 |
val SOME (t, _) =
|
Walther@60500
|
264 |
rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
walther@60347
|
265 |
if UnparseC.term 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
|
266 |
then () else error "eqsystem.sml rewrite in 4x4 simplify_System_paren";
|
walther@60347
|
267 |
|
Walther@60500
|
268 |
val SOME (t, _) = rewrite_set_inst_ ctxt true bdvs isolate_bdvs t;
|
walther@60347
|
269 |
if UnparseC.term t = "[c_4 = 0, \
|
walther@60347
|
270 |
\L * c_3 + c_4 = 0 + - 1 * (- 1 * q_0 * L \<up> 2 / 2),\n \
|
walther@60347
|
271 |
\c + (c_2 + (c_3 + c_4)) = 0, c_2 + (c_3 + c_4) = 0]"
|
walther@60347
|
272 |
then () else error "eqsystem.sml rewrite in 4x4 isolate_bdvs";
|
walther@60347
|
273 |
|
Walther@60500
|
274 |
val SOME(t, _)= rewrite_set_inst_ ctxt true bdvs simplify_System_parenthesized t;
|
walther@60347
|
275 |
if UnparseC.term t = "[c_4 = 0,\
|
walther@60347
|
276 |
\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
|
walther@60347
|
277 |
\ c + (c_2 + (c_3 + c_4)) = 0,\n\
|
walther@60347
|
278 |
\ c_2 + (c_3 + c_4) = 0]"
|
walther@60347
|
279 |
then () else error "eqsystem.sml rewrite in 4x4 simplify_System_p..2";
|
walther@60347
|
280 |
|
Walther@60500
|
281 |
val SOME (t, _) = rewrite_set_ ctxt true order_system t;
|
walther@60347
|
282 |
if UnparseC.term t = "[c_4 = 0,\
|
walther@60347
|
283 |
\ L * c_3 + c_4 = q_0 * L \<up> 2 / 2,\
|
walther@60347
|
284 |
\ c_2 + (c_3 + c_4) = 0,\n\
|
walther@60347
|
285 |
\ c + (c_2 + (c_3 + c_4)) = 0]"
|
walther@60347
|
286 |
then () else error "eqsystem.sml rewrite in 4x4 order_system";
|
walther@60347
|
287 |
|
walther@60347
|
288 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
289 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
290 |
"----------- refine [linear,system]-------------------------------";
|
walther@60347
|
291 |
val fmz =
|
walther@60347
|
292 |
["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2," ^
|
walther@60347
|
293 |
"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]",
|
walther@60347
|
294 |
"solveForVars [c, c_2]", "solution LL"];
|
walther@60347
|
295 |
|
Walther@60556
|
296 |
(*WN120313 in "solution L" above "Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]" caused an error...*)
|
Walther@60556
|
297 |
"~~~~~ fun Refine.refine , args:"; val ((fmz: Formalise.model), (pblID:Problem.id)) = (fmz, ["LINEAR", "system"]);
|
Walther@60556
|
298 |
"~~~~~ fun refin' , args:"; val ((pblRD: Problem.id_reverse), fmz, pbls, ((Store.Node (pI, [py], [])): Problem.T Store.node)) =
|
walther@60347
|
299 |
((rev o tl) pblID, fmz, [(*match list*)],
|
Walther@60559
|
300 |
((Store.Node ("LINEAR", [Problem.from_store ctxt ["LINEAR", "system"]], [])): Problem.T Store.node));
|
walther@60347
|
301 |
val {thy, ppc, where_, prls, ...} = py ;
|
Walther@60469
|
302 |
"~~~~~ fun O_Model.init, args:"; val (thy, fmz, pbt) = (thy, fmz, ppc);
|
walther@60347
|
303 |
val ctxt = Proof_Context.init_global thy;
|
walther@60347
|
304 |
"~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
|
walther@60347
|
305 |
fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
|
walther@60347
|
306 |
(_, _::_) => (Free (v,T)::get_vars vs)
|
walther@60347
|
307 |
| (_, [] ) => get_vars vs) (*filter out nums as long as
|
walther@60347
|
308 |
we have Free ("123",_)*)
|
walther@60347
|
309 |
| get_vars [] = [];
|
walther@60347
|
310 |
t = "equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,"^
|
walther@60347
|
311 |
"0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + (c_2::real)]";
|
walther@60347
|
312 |
val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
|
walther@60347
|
313 |
val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
|
walther@60347
|
314 |
val ctxt = Variable.declare_constraints (nth 2 ts) ctxt;
|
walther@60347
|
315 |
val ctxt = Variable.declare_constraints (nth 3 ts) ctxt;
|
walther@60347
|
316 |
val ctxt = Variable.declare_constraints (nth 4 ts) ctxt;
|
walther@60347
|
317 |
val t = nth 2 fmz; t = "solveForVars [c, c_2]";
|
walther@60347
|
318 |
val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
|
walther@60347
|
319 |
val ctxt = Variable.declare_constraints (nth 1 ts) ctxt;
|
walther@60347
|
320 |
val t = nth 3 fmz; t = "solution LL";
|
walther@60347
|
321 |
(*(Syntax.read_term ctxt t);
|
walther@60347
|
322 |
Type unification failed: Clash of types "real" and "_ list"
|
walther@60347
|
323 |
Type error in application: incompatible operand type
|
walther@60347
|
324 |
|
walther@60347
|
325 |
Operator: solution :: bool list \<Rightarrow> toreall
|
walther@60347
|
326 |
Operand: L :: real ========== L was already present in equalities ========== *)
|
walther@60347
|
327 |
|
walther@60347
|
328 |
"===== case 1 =====";
|
Walther@60556
|
329 |
val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
|
walther@60347
|
330 |
case matches of
|
Walther@60556
|
331 |
[M_Match.Matches (["LINEAR", "system"], _), (*Matches*)
|
Walther@60556
|
332 |
M_Match.Matches (["2x2", "LINEAR", "system"], _), (*NoMatch ! GOON !*)
|
Walther@60556
|
333 |
M_Match.NoMatch (["triangular", "2x2", "LINEAR", "system"], _), (**)
|
Walther@60556
|
334 |
M_Match.Matches (["normalise", "2x2", "LINEAR", "system"], (**)
|
Walther@60556
|
335 |
{Find = [Correct "solution LL"], With = [], (**)
|
Walther@60556
|
336 |
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
|
337 |
Correct "solveForVars [c, c_2]"],
|
Walther@60556
|
338 |
Where = [],
|
Walther@60556
|
339 |
Relate = []})] => ()
|
walther@60347
|
340 |
| _ => error "eqsystem.sml Refine.refine ['normalise','2x2'...]";
|
walther@60347
|
341 |
|
walther@60347
|
342 |
"===== case 2 =====";
|
walther@60347
|
343 |
val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
344 |
"solveForVars [c, c_2]", "solution LL"];
|
Walther@60556
|
345 |
val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"];
|
walther@60347
|
346 |
case matches of [_,_,
|
walther@60347
|
347 |
M_Match.Matches
|
walther@60347
|
348 |
(["triangular", "2x2", "LINEAR", "system"],
|
walther@60347
|
349 |
{Find = [Correct "solution LL"],
|
walther@60347
|
350 |
With = [],
|
walther@60347
|
351 |
Given =
|
walther@60347
|
352 |
[Correct "equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
353 |
Correct "solveForVars [c, c_2]"],
|
walther@60347
|
354 |
Where = [Correct
|
walther@60347
|
355 |
"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
|
356 |
Correct
|
walther@60347
|
357 |
"[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
|
358 |
Relate = []})] => ()
|
walther@60347
|
359 |
| _ => error "eqsystem.sml Refine.refine ['triangular','2x2'...]";
|
walther@60347
|
360 |
|
walther@60347
|
361 |
(*WN051014-----------------------------------------------------------------------------------\\
|
Walther@60556
|
362 |
the above 'val matches = Refine.refine_PIDE @{context} fmz ["LINEAR", "system"]'
|
walther@60347
|
363 |
didn't work anymore; we investigated in these steps:*)
|
walther@60347
|
364 |
val fmz = ["equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]",
|
walther@60347
|
365 |
"solveForVars [c, c_2]", "solution LL"];
|
Walther@60556
|
366 |
val matches = Refine.refine_PIDE @{context} fmz ["triangular", "2x2", "LINEAR", "system"];
|
walther@60347
|
367 |
(*... resulted in
|
walther@60347
|
368 |
False "[c, c_2] from_ [c, c_2] occur_exactly_in nth_ 2\n
|
walther@60347
|
369 |
[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]"]*)
|
Walther@60565
|
370 |
val t = TermC.parse_test @{context} ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
|
walther@60347
|
371 |
"[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]");
|
Walther@60500
|
372 |
|
Walther@60500
|
373 |
val SOME (t', _) = rewrite_set_ ctxt false prls_triangular t;
|
walther@60347
|
374 |
(*found:...
|
walther@60347
|
375 |
## try thm: NTH_CONS
|
walther@60347
|
376 |
### eval asms: 1 < 2 + - 1
|
walther@60347
|
377 |
==> nth_ (2 + - 1) [L * c + c_2 = q_0 * L \<up> 2 / 2] =
|
walther@60347
|
378 |
nth_ (2 + - 1 + - 1) []
|
walther@60347
|
379 |
#### rls: erls_prls_triangular on: 1 < 2 + - 1
|
walther@60347
|
380 |
##### try calc: op <'
|
walther@60347
|
381 |
### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
|
walther@60347
|
382 |
|
Walther@60516
|
383 |
... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
|
walther@60347
|
384 |
(*--------------------------------------------------------------------------------------------//*)
|
walther@60347
|
385 |
|
walther@60347
|
386 |
|
walther@60347
|
387 |
"===== case 3: relaxed preconditions for triangular system =====";
|
walther@60347
|
388 |
val fmz = ["equalities [L * q_0 = c, \
|
walther@60347
|
389 |
\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
|
walther@60347
|
390 |
\ 0 = c_4, \
|
walther@60347
|
391 |
\ 0 = c_3]",
|
walther@60347
|
392 |
"solveForVars [c, c_2, c_3, c_4]", "solution LL"];
|
walther@60347
|
393 |
(*============ inhibit exn WN120314 TODO: investigate type error (same) in these 2 cases:
|
walther@60347
|
394 |
probably exn thrown by fun declare_constraints
|
walther@60347
|
395 |
/-------------------------------------------------------\
|
walther@60347
|
396 |
Type unification failed
|
walther@60347
|
397 |
Type error in application: incompatible operand type
|
walther@60347
|
398 |
|
walther@60347
|
399 |
Operator: op # c_3 :: 'a list \<Rightarrow> 'a list
|
walther@60347
|
400 |
Operand: [c_4] :: 'b list
|
walther@60347
|
401 |
\-------------------------------------------------------/
|
walther@60347
|
402 |
val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
|
walther@60347
|
403 |
case TermC.matches of
|
walther@60347
|
404 |
[M_Match.Matches (["LINEAR", "system"], _),
|
walther@60347
|
405 |
M_Match.NoMatch (["2x2", "LINEAR", "system"], _),
|
walther@60347
|
406 |
M_Match.NoMatch (["3x3", "LINEAR", "system"], _),
|
walther@60347
|
407 |
M_Match.Matches (["4x4", "LINEAR", "system"], _),
|
walther@60347
|
408 |
M_Match.NoMatch (["triangular", "4x4", "LINEAR", "system"], _),
|
walther@60347
|
409 |
M_Match.Matches (["normalise", "4x4", "LINEAR", "system"], _)] => ()
|
walther@60347
|
410 |
| _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
|
walther@60347
|
411 |
(*WN060914 does NOT match, because 3rd and 4th equ are not ordered*)
|
walther@60347
|
412 |
|
walther@60347
|
413 |
"===== case 4 =====";
|
walther@60347
|
414 |
val fmz = ["equalities [L * q_0 = c, \
|
walther@60347
|
415 |
\ 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2,\
|
walther@60347
|
416 |
\ 0 = c_3, \
|
walther@60347
|
417 |
\ 0 = c_4]",
|
walther@60347
|
418 |
"solveForVars [c, c_2, c_3, c_4]", "solution LL"];
|
walther@60347
|
419 |
val TermC.matches = Refine.refine fmz ["triangular", "4x4", "LINEAR", "system"];
|
walther@60347
|
420 |
case TermC.matches of
|
walther@60347
|
421 |
[M_Match.Matches (["triangular", "4x4", "LINEAR", "system"], _)] => ()
|
walther@60347
|
422 |
| _ => error "eqsystem.sml: Refine.refine relaxed triangular sys M_Match.NoMatch";
|
walther@60347
|
423 |
val TermC.matches = Refine.refine fmz ["LINEAR", "system"];
|
walther@60347
|
424 |
============ inhibit exn WN120314 ==============================================*)
|
walther@60347
|
425 |
|
walther@60347
|
426 |
"----------- Refine.refine [2x2,linear,system] search error--------------";
|
walther@60347
|
427 |
"----------- Refine.refine [2x2,linear,system] search error--------------";
|
walther@60347
|
428 |
"----------- Refine.refine [2x2,linear,system] search error--------------";
|
walther@60347
|
429 |
(*didn't go into ["2x2", "LINEAR", "system"];
|
walther@60347
|
430 |
we investigated in these steps:*)
|
walther@60347
|
431 |
val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
|
walther@60347
|
432 |
\0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
|
walther@60347
|
433 |
"solveForVars [c, c_2]", "solution LL"];
|
Walther@60556
|
434 |
val matches = Refine.refine_PIDE @{context} fmz ["2x2", "LINEAR", "system"];
|
walther@60347
|
435 |
(*default_print_depth 11;*) TermC.matches; (*default_print_depth 3;*)
|
walther@60347
|
436 |
(*brought: 'False "length_ es_ = 2"'*)
|
walther@60347
|
437 |
|
walther@60347
|
438 |
(*-----fun refin' (pblRD:Problem.id_reverse) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
|
walther@60347
|
439 |
(* val ((pblRD:Problem.id_reverse), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
|
walther@60347
|
440 |
(rev ["LINEAR", "system"], fmz, [(*match list*)],
|
walther@60347
|
441 |
((Store.Node ("2x2",[Problem.from_store ["2x2", "LINEAR", "system"]],[])):pbt Store.store));
|
walther@60347
|
442 |
*)
|
walther@60347
|
443 |
> show_types:=true; UnparseC.term (hd where_); show_types:=false;
|
walther@60347
|
444 |
val it = "length_ (es_::real list) = (2::real)" : string
|
walther@60347
|
445 |
|
walther@60347
|
446 |
=========================================================================\
|
walther@60347
|
447 |
-------fun Problem.prep_input
|
walther@60347
|
448 |
(* val (thy, (pblID, dsc_dats: (string * (string list)) list,
|
walther@60347
|
449 |
ev:rls, ca: string option, metIDs:metID list)) =
|
walther@60347
|
450 |
(EqSystem.thy, (["system"],
|
walther@60347
|
451 |
[("#Given" ,["equalities es_", "solveForVars v_s"]),
|
walther@60347
|
452 |
("#Find" ,["solution ss___"](*___ is copy-named*))
|
walther@60347
|
453 |
],
|
walther@60347
|
454 |
Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
|
walther@60347
|
455 |
SOME "solveSystem es_ v_s",
|
walther@60347
|
456 |
[]));
|
walther@60347
|
457 |
*)
|
walther@60347
|
458 |
> val [("#Given", [equalities_es_, "solveForVars v_s"])] = gi;
|
walther@60347
|
459 |
val equalities_es_ = "equalities es_" : string
|
walther@60347
|
460 |
> val (dd, ii) = (split_did o Thm.term_of o the o (TermC.parse thy)) equalities_es_;
|
walther@60347
|
461 |
> show_types:=true; UnparseC.term ii; show_types:=false;
|
walther@60347
|
462 |
val it = "es_::bool list" : string
|
walther@60347
|
463 |
~~~~~~~~~~~~~~~ \<up> \<up> \<up> OK~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
walther@60347
|
464 |
|
walther@60347
|
465 |
> val {where_,...} = Problem.from_store ["2x2", "LINEAR", "system"];
|
walther@60347
|
466 |
> show_types:=true; UnparseC.term (hd where_); show_types:=false;
|
walther@60347
|
467 |
|
walther@60347
|
468 |
=========================================================================/
|
walther@60347
|
469 |
|
walther@60347
|
470 |
-----fun refin' ff:
|
walther@60360
|
471 |
> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
|
walther@60347
|
472 |
[
|
walther@60347
|
473 |
(1 ,[1] ,true ,#Given ,Cor equalities
|
walther@60347
|
474 |
[0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
|
walther@60347
|
475 |
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
|
476 |
0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]])),
|
walther@60347
|
477 |
(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
|
walther@60347
|
478 |
(3 ,[1] ,true ,#Find ,Cor solution L ,(ss___, [L]))]
|
walther@60347
|
479 |
|
walther@60347
|
480 |
> (writeln o pres2str) pre';
|
walther@60347
|
481 |
[
|
walther@60347
|
482 |
(false, length_ es_ = 2),
|
walther@60347
|
483 |
(true, length_ [c, c_2] = 2)]
|
walther@60347
|
484 |
|
walther@60347
|
485 |
----- fun match_oris':
|
walther@60360
|
486 |
> (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) itms;
|
walther@60347
|
487 |
> (writeln o pres2str) pre';
|
walther@60347
|
488 |
..as in refin'
|
walther@60347
|
489 |
|
walther@60347
|
490 |
----- fun check in Pre_Conds.
|
walther@60347
|
491 |
> (writeln o env2str) env;
|
walther@60347
|
492 |
["
|
walther@60347
|
493 |
(es_, [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,
|
walther@60347
|
494 |
0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2])", "
|
walther@60347
|
495 |
(v_s, [c, c_2])", "
|
walther@60347
|
496 |
(ss___, L)"]
|
walther@60347
|
497 |
|
walther@60347
|
498 |
> val es_ = (fst o hd) env;
|
walther@60347
|
499 |
val es_ = Free ("es_", "bool List.list") : Term.term
|
walther@60347
|
500 |
|
walther@60347
|
501 |
> val pre1 = hd pres;
|
walther@60347
|
502 |
TermC.atomty pre1;
|
walther@60347
|
503 |
***
|
walther@60347
|
504 |
*** Const (op =, [real, real] => bool)
|
walther@60347
|
505 |
*** . Const (ListG.length_, real list => real)
|
walther@60347
|
506 |
*** . . Free (es_, real list)
|
walther@60347
|
507 |
~~~~~~~~~~~~~~~~~~~ \<up> \<up> \<up> should be bool list~~~~~~~~~~~~~~~~~~~
|
walther@60347
|
508 |
*** . Free (2, real)
|
walther@60347
|
509 |
***
|
walther@60347
|
510 |
|
walther@60347
|
511 |
THE REASON WAS A non-type-constrained variable IN #WHERE OF PROBLEM
|
walther@60347
|
512 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
walther@60347
|
513 |
*)
|
walther@60347
|
514 |
|
Walther@60556
|
515 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
Walther@60556
|
516 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
Walther@60556
|
517 |
"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
|
walther@60347
|
518 |
val fmz = ["equalities [0 = - 1 * q_0 * 0 \<up> 2 / 2 + 0 * c + c_2,\
|
walther@60347
|
519 |
\0 = - 1 * q_0 * L \<up> 2 / 2 + L * c + c_2]",
|
walther@60347
|
520 |
"solveForVars [c, c_2]", "solution LL"];
|
walther@60347
|
521 |
val (dI',pI',mI') =
|
walther@60347
|
522 |
("Biegelinie",["normalise", "2x2", "LINEAR", "system"],
|
walther@60347
|
523 |
["EqSystem", "normalise", "2x2"]);
|
walther@60347
|
524 |
val p = e_pos'; val c = [];
|
walther@60347
|
525 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60347
|
526 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
527 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
528 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
529 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
530 |
case nxt of Specify_Method ["EqSystem", "normalise", "2x2"] => ()
|
walther@60347
|
531 |
| _ => error "eqsystem.sml [EqSystem,normalise,2x2] specify";
|
walther@60347
|
532 |
|
walther@60347
|
533 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
534 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
535 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f(*["(bdv_1, c)", "(bdv_2, hd (tl [c, c_2] ... corrected srls; ran only AFTER use"RCODE-root.sml", store_met was NOT SUFFICIENT*);
|
walther@60347
|
536 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
537 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
538 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
539 |
case nxt of
|
walther@60347
|
540 |
(Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
|
walther@60347
|
541 |
| _ => error "eqsystem.sml me [EqSystem,normalise,2x2] SubProblem";
|
walther@60347
|
542 |
|
walther@60347
|
543 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
544 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
545 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
546 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
547 |
case nxt of
|
walther@60347
|
548 |
(Specify_Method ["EqSystem", "top_down_substitution", "2x2"]) => ()
|
walther@60347
|
549 |
| _ => error "eqsystem.sml me [EqSys...2x2] top_down_substitution";
|
walther@60347
|
550 |
|
walther@60347
|
551 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@60347
|
552 |
val PblObj {probl,...} = get_obj I pt [5];
|
walther@60360
|
553 |
(writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl;
|
walther@60347
|
554 |
(*[
|
walther@60347
|
555 |
(1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])),
|
walther@60347
|
556 |
(2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
|
walther@60347
|
557 |
(3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))]
|
walther@60347
|
558 |
*)
|
walther@60347
|
559 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
560 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
561 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
562 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
563 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
564 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
565 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
566 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
567 |
case nxt of
|
walther@60347
|
568 |
(Check_Postcond ["triangular", "2x2", "LINEAR", "system"]) => ()
|
walther@60347
|
569 |
| _ => error "eqsystem.sml me Subpbl .[EqSys...2x2] finished";
|
walther@60347
|
570 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
571 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
walther@60347
|
572 |
if f2str f = "[c = L * q_0 / 2, c_2 = 0]" then ()
|
walther@60347
|
573 |
else error "eqsystem.sml me [EqSys...2x2] finished f2str f";
|
walther@60347
|
574 |
case nxt of
|
walther@60347
|
575 |
(End_Proof') => ()
|
walther@60347
|
576 |
| _ => error "eqsystem.sml me [EqSys...2x2] finished End_Proof'";
|