walther@60278
|
1 |
(* testexamples for Poly, polynomials
|
neuper@37906
|
2 |
author: Matthias Goldgruber 2003
|
neuper@37906
|
3 |
(c) due to copyright terms
|
neuper@37906
|
4 |
|
neuper@42395
|
5 |
LEGEND:
|
neuper@42395
|
6 |
WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
|
neuper@42395
|
7 |
examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
|
neuper@38022
|
8 |
*)
|
neuper@42395
|
9 |
|
walther@60318
|
10 |
"-----------------------------------------------------------------------------------------------";
|
walther@60318
|
11 |
"-----------------------------------------------------------------------------------------------";
|
walther@60318
|
12 |
"table of contents -----------------------------------------------------------------------------";
|
walther@60318
|
13 |
"-----------------------------------------------------------------------------------------------";
|
walther@60318
|
14 |
"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
|
walther@60318
|
15 |
"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
|
walther@60318
|
16 |
"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
|
walther@60318
|
17 |
"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
|
walther@60318
|
18 |
"-------- investigate (new 2002) uniary minus --------------------------------------------------";
|
walther@60318
|
19 |
"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
|
walther@60318
|
20 |
"-------- examples from textbook Schalk I ------------------------------------------------------";
|
walther@60318
|
21 |
"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
|
walther@60318
|
22 |
"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
|
walther@60318
|
23 |
"-------- check pbl 'polynomial simplification' -----------------------------------------------";
|
walther@60318
|
24 |
"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
|
walther@60318
|
25 |
"-------- interSteps for Schalk 299a -----------------------------------------------------------";
|
walther@60318
|
26 |
"-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
|
walther@60318
|
27 |
"-------- ord_make_polynomial ------------------------------------------------------------------";
|
walther@60318
|
28 |
"-----------------------------------------------------------------------------------------------";
|
walther@60318
|
29 |
"-----------------------------------------------------------------------------------------------";
|
walther@60318
|
30 |
"-----------------------------------------------------------------------------------------------";
|
neuper@37906
|
31 |
|
neuper@37906
|
32 |
|
walther@60318
|
33 |
"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
|
walther@60318
|
34 |
"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
|
walther@60318
|
35 |
"-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
|
walther@60318
|
36 |
(* indentation indicates call hierarchy:
|
walther@60318
|
37 |
"~~~~~ fun is_addUnordered
|
walther@60318
|
38 |
"~~~~~~~ fun is_polyexp
|
walther@60318
|
39 |
"~~~~~~~ fun sort_monoms
|
walther@60318
|
40 |
"~~~~~~~~~ fun sort_monList
|
walther@60318
|
41 |
"~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order
|
walther@60318
|
42 |
"~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order
|
walther@60318
|
43 |
"~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order
|
walther@60318
|
44 |
"~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order
|
walther@60318
|
45 |
"~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv
|
walther@60318
|
46 |
"~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv
|
walther@60318
|
47 |
"~~~~~~~~~~~~~~~ fun monom_degree : term list -> int
|
walther@60318
|
48 |
"~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order
|
walther@60318
|
49 |
"~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option
|
walther@60318
|
50 |
"~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string
|
walther@60318
|
51 |
"~~~~~ fun is_multUnordered
|
walther@60318
|
52 |
"~~~~~~~ fun sort_variables
|
walther@60318
|
53 |
"~~~~~~~~~ fun sort_varList
|
walther@60318
|
54 |
"~~~~~~~~~~~ fun var_ord
|
walther@60318
|
55 |
"~~~~~~~~~~~~~ fun get_basStr used twice --^^
|
walther@60318
|
56 |
"~~~~~~~~~~~~~ fun get_potStr used twice --^^
|
wneuper@59529
|
57 |
|
walther@60318
|
58 |
fun int_ord (i1, i2) =
|
walther@60318
|
59 |
(@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
|
walther@60318
|
60 |
Int.compare (i1, i2)
|
walther@60318
|
61 |
);
|
walther@60318
|
62 |
fun var_ord (a, b) =
|
walther@60318
|
63 |
(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
|
walther@60318
|
64 |
sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
|
walther@60318
|
65 |
prod_ord string_ord string_ord
|
walther@60318
|
66 |
((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
|
walther@60318
|
67 |
);
|
walther@60318
|
68 |
fun var_ord_revPow (a, b: term) =
|
walther@60318
|
69 |
(@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
|
walther@60318
|
70 |
sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
|
walther@60318
|
71 |
prod_ord string_ord string_ord_rev
|
walther@60318
|
72 |
((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
|
walther@60318
|
73 |
);
|
walther@60318
|
74 |
fun sort_varList ts =
|
walther@60318
|
75 |
(@{print} {a = "sort_varList", args = UnparseC.terms ts};
|
walther@60318
|
76 |
sort var_ord ts
|
walther@60318
|
77 |
);
|
walther@60318
|
78 |
fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
|
walther@60318
|
79 |
| dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
|
walther@60318
|
80 |
| dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
|
walther@60318
|
81 |
| dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
|
walther@60318
|
82 |
(@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",
|
walther@60318
|
83 |
is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
|
walther@60318
|
84 |
case (cond x, cond y) of
|
walther@60318
|
85 |
(false, false) =>
|
walther@60318
|
86 |
(case elem_ord (x, y) of
|
walther@60318
|
87 |
EQUAL => dict_cond_ord elem_ord cond (xs, ys)
|
walther@60318
|
88 |
| ord => ord)
|
walther@60318
|
89 |
| (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
|
walther@60318
|
90 |
| (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
|
walther@60318
|
91 |
| (true, true) => dict_cond_ord elem_ord cond (xs, ys)
|
walther@60318
|
92 |
);
|
walther@60318
|
93 |
fun compare_koeff_ord (xs, ys) =
|
walther@60318
|
94 |
(@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",
|
walther@60318
|
95 |
sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};
|
walther@60318
|
96 |
string_ord
|
walther@60318
|
97 |
((koeff2ordStr o get_koeff_of_mon) xs,
|
walther@60318
|
98 |
(koeff2ordStr o get_koeff_of_mon) ys)
|
walther@60318
|
99 |
);
|
walther@60318
|
100 |
fun var_ord (a,b: term) =
|
walther@60318
|
101 |
(@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
|
walther@60318
|
102 |
sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
|
walther@60318
|
103 |
prod_ord string_ord string_ord
|
walther@60318
|
104 |
((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
|
walther@60318
|
105 |
);
|
walther@60318
|
106 |
*)
|
walther@60318
|
107 |
|
walther@60318
|
108 |
|
walther@60318
|
109 |
"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
|
walther@60318
|
110 |
"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
|
walther@60318
|
111 |
"-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
|
walther@60318
|
112 |
(* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.
|
walther@60318
|
113 |
|
walther@60318
|
114 |
sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
|
walther@60318
|
115 |
@{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
|
walther@60318
|
116 |
val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
|
walther@60318
|
117 |
val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
|
walther@60318
|
118 |
|
Walther@60521
|
119 |
val SOME (t', []) = rewrite_ @{context} tless_true Rule_Set.empty true thm_isac t_isac;
|
walther@60329
|
120 |
if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("- 1", _)*))
|
walther@60318
|
121 |
else error "thm - ?z = - 1 * ?z loops with new numerals";
|
walther@60318
|
122 |
|
walther@60318
|
123 |
|
walther@60318
|
124 |
"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
|
walther@60318
|
125 |
"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
|
walther@60318
|
126 |
"-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
|
Walther@60521
|
127 |
val thy = Proof_Context.init_global @{theory Partial_Fractions}
|
Walther@60521
|
128 |
val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
|
walther@60336
|
129 |
val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
|
wneuper@59522
|
130 |
|
Walther@60521
|
131 |
val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
|
walther@60336
|
132 |
val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
|
wneuper@59522
|
133 |
|
walther@60318
|
134 |
"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
|
walther@60318
|
135 |
"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
|
walther@60318
|
136 |
"-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
|
Walther@60521
|
137 |
val t = TermC.parseNEW' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
|
wneuper@59522
|
138 |
val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
|
walther@60317
|
139 |
if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
|
walther@60317
|
140 |
andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
|
wneuper@59522
|
141 |
then () else error "eval_is_expanded_in x ..changed";
|
wneuper@59522
|
142 |
|
Walther@60521
|
143 |
val thy = Proof_Context.init_global @{theory Partial_Fractions}
|
Walther@60521
|
144 |
val t = TermC.parseNEW' thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
|
wneuper@59522
|
145 |
val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
|
walther@60317
|
146 |
if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
|
walther@60317
|
147 |
andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
|
wneuper@59522
|
148 |
then () else error "eval_is_expanded_in AA ..changed";
|
wneuper@59522
|
149 |
|
wneuper@59522
|
150 |
|
Walther@60521
|
151 |
val t = TermC.parseNEW' thy "(8 + 2*x + x \<up> 2) is_poly_in x";
|
wneuper@59522
|
152 |
val SOME (id, t') = eval_is_poly_in 0 0 t 0;
|
walther@60242
|
153 |
if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
|
walther@60242
|
154 |
andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
|
wneuper@59522
|
155 |
then () else error "is_poly_in x ..changed";
|
wneuper@59522
|
156 |
|
Walther@60521
|
157 |
val t = TermC.parseNEW' thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
|
wneuper@59522
|
158 |
val SOME (id, t') = eval_is_poly_in 0 0 t 0;
|
walther@60242
|
159 |
if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
|
walther@60242
|
160 |
andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
|
wneuper@59522
|
161 |
then () else error "is_poly_in AA ..changed";
|
wneuper@59522
|
162 |
|
wneuper@59522
|
163 |
|
Walther@60521
|
164 |
val thy = Proof_Context.init_global @{theory Partial_Fractions}
|
Walther@60521
|
165 |
val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
|
wenzelm@60309
|
166 |
val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
|
wneuper@59522
|
167 |
|
Walther@60521
|
168 |
val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
|
wenzelm@60309
|
169 |
val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
|
wneuper@59522
|
170 |
|
walther@60318
|
171 |
"-------- investigate (new 2002) uniary minus --------------------------------------------------";
|
walther@60318
|
172 |
"-------- investigate (new 2002) uniary minus --------------------------------------------------";
|
walther@60318
|
173 |
"-------- investigate (new 2002) uniary minus --------------------------------------------------";
|
wenzelm@60203
|
174 |
val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
|
walther@60230
|
175 |
TermC.atomty t;
|
wneuper@59117
|
176 |
(*
|
wneuper@59117
|
177 |
*** Const (HOL.Trueprop, bool => prop)
|
wneuper@59117
|
178 |
*** . Const (HOL.eq, real => real => bool)
|
wneuper@59117
|
179 |
*** . . Const (Groups.minus_class.minus, real => real => real)
|
wneuper@59117
|
180 |
*** . . . Const (Groups.zero_class.zero, real)
|
neuper@37906
|
181 |
*** . . . Var ((x, 0), real)
|
wneuper@59117
|
182 |
*** . . Const (Groups.uminus_class.uminus, real => real)
|
wneuper@59117
|
183 |
*** . . . Var ((x, 0), real)
|
wneuper@59117
|
184 |
*)
|
neuper@42395
|
185 |
case t of
|
wenzelm@60309
|
186 |
Const (\<^const_name>\<open>Trueprop\<close>, _) $
|
wenzelm@60309
|
187 |
(Const (\<^const_name>\<open>HOL.eq\<close>, _) $
|
wenzelm@60309
|
188 |
(Const (\<^const_name>\<open>minus\<close>, _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _) $
|
wneuper@59117
|
189 |
Var (("x", 0), _)) $
|
wenzelm@60309
|
190 |
(Const (\<^const_name>\<open>uminus\<close>, _) $ Var (("x", 0), _))) => ()
|
neuper@42395
|
191 |
| _ => error "internal representation of \"0 - ?x = - ?x\" changed";
|
neuper@37906
|
192 |
|
walther@60318
|
193 |
|
Walther@60521
|
194 |
val t = TermC.parseNEW' thy "- 1";
|
walther@60230
|
195 |
TermC.atomty t;
|
wneuper@59117
|
196 |
(*
|
wneuper@59117
|
197 |
***
|
walther@60329
|
198 |
*** Free (- 1, real)
|
wneuper@59117
|
199 |
***
|
wneuper@59117
|
200 |
*)
|
neuper@42395
|
201 |
case t of
|
walther@60336
|
202 |
Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
|
neuper@42395
|
203 |
| _ => error "internal representation of \"- 1\" changed";
|
neuper@37906
|
204 |
|
neuper@42395
|
205 |
"======= these external values all have the same internal representation";
|
neuper@42395
|
206 |
(* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
|
neuper@42395
|
207 |
(*----------------------------------- vvvvv -------------------------------------------*)
|
Walther@60521
|
208 |
val t = TermC.parseNEW' thy "-x";
|
walther@60230
|
209 |
TermC.atomty t;
|
neuper@37906
|
210 |
(**** -------------
|
neuper@37906
|
211 |
*** Free ( -x, real)*)
|
neuper@42395
|
212 |
case t of
|
wenzelm@60309
|
213 |
Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
|
neuper@42395
|
214 |
| _ => error "internal representation of \"-x\" changed";
|
neuper@42395
|
215 |
(*----------------------------------- vvvvv -------------------------------------------*)
|
Walther@60521
|
216 |
val t = TermC.parseNEW' thy "- x";
|
walther@60230
|
217 |
TermC.atomty t;
|
neuper@37906
|
218 |
(**** -------------
|
neuper@37906
|
219 |
*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
|
neuper@42395
|
220 |
case t of
|
wenzelm@60309
|
221 |
Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
|
neuper@42395
|
222 |
| _ => error "internal representation of \"- x\" changed";
|
neuper@42395
|
223 |
(*----------------------------------- vvvvvv ------------------------------------------*)
|
Walther@60521
|
224 |
val t = TermC.parseNEW' thy "-(x)";
|
walther@60230
|
225 |
TermC.atomty t;
|
neuper@37906
|
226 |
(**** -------------
|
neuper@37906
|
227 |
*** Free ( -x, real)*)
|
neuper@42395
|
228 |
case t of
|
wenzelm@60309
|
229 |
Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
|
neuper@42395
|
230 |
| _ => error "internal representation of \"-(x)\" changed";
|
neuper@37906
|
231 |
|
walther@60318
|
232 |
|
walther@60318
|
233 |
"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
|
walther@60318
|
234 |
"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
|
walther@60318
|
235 |
"-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
|
walther@60318
|
236 |
(* indentation partially indicates call hierarchy:
|
walther@60318
|
237 |
"~~~~~ fun is_addUnordered
|
walther@60318
|
238 |
"~~~~~~~ fun is_polyexp
|
walther@60318
|
239 |
"~~~~~~~ fun sort_monoms
|
walther@60318
|
240 |
"~~~~~~~~~ fun sort_monList
|
walther@60318
|
241 |
"~~~~~~~~~~~ fun koeff_degree_ord
|
walther@60318
|
242 |
"~~~~~~~~~~~~~ fun degree_ord
|
walther@60318
|
243 |
"~~~~~~~~~~~~~~~ fun dict_cond_ord
|
walther@60318
|
244 |
"~~~~~~~~~~~~~~~~~ fun var_ord_revPow
|
walther@60318
|
245 |
"~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
|
walther@60318
|
246 |
"~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
|
walther@60318
|
247 |
"~~~~~~~~~~~~~~~ fun monom_degree
|
walther@60318
|
248 |
"~~~~~~~~~~~~~ fun compare_koeff_ord
|
walther@60318
|
249 |
"~~~~~~~~~~~~~~~ fun get_koeff_of_mon
|
walther@60318
|
250 |
"~~~~~~~~~~~~~~~~~ fun koeff2ordStr
|
walther@60318
|
251 |
"~~~~~ fun is_multUnordered
|
walther@60318
|
252 |
"~~~~~~~ fun sort_variables
|
walther@60318
|
253 |
"~~~~~~~~~ fun sort_varList
|
walther@60318
|
254 |
"~~~~~~~~~~~ fun var_ord
|
walther@60318
|
255 |
"~~~~~~~~~~~~~ fun get_basStr used twice --^^
|
walther@60318
|
256 |
"~~~~~~~~~~~~~ fun get_potStr used twice --^^
|
walther@60318
|
257 |
*)
|
Walther@60565
|
258 |
val t = TermC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
|
walther@60318
|
259 |
|
Walther@60521
|
260 |
eval_is_addUnordered "xxx" "yyy" t @{context};
|
walther@60318
|
261 |
"~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
|
walther@60336
|
262 |
(t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =
|
Walther@60521
|
263 |
("xxx", "yyy", t, @{context});
|
walther@60318
|
264 |
|
walther@60318
|
265 |
(*if*) is_addUnordered arg;
|
walther@60318
|
266 |
"~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
|
walther@60318
|
267 |
((is_polyexp t) andalso not (t = sort_monoms t));
|
walther@60318
|
268 |
|
walther@60318
|
269 |
(t = sort_monoms t);
|
walther@60318
|
270 |
"~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
|
walther@60318
|
271 |
val ll = map monom2list (poly2list t);
|
walther@60318
|
272 |
val lls =
|
walther@60318
|
273 |
|
walther@60318
|
274 |
sort_monList ll;
|
walther@60318
|
275 |
"~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
|
walther@60318
|
276 |
val xxx =
|
walther@60318
|
277 |
|
walther@60318
|
278 |
sort koeff_degree_ord ll(*return value*);
|
walther@60318
|
279 |
"~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
|
walther@60318
|
280 |
koeff_degree_ord: term list * term list -> order;
|
walther@60318
|
281 |
(*we check all elements at once..*)
|
walther@60318
|
282 |
val eee1 = ll |> nth 1;
|
walther@60318
|
283 |
val eee2 = ll |> nth 2;
|
walther@60318
|
284 |
val eee3 = ll |> nth 3;
|
walther@60318
|
285 |
val eee3 = ll |> nth 3;
|
walther@60318
|
286 |
val eee4 = ll |> nth 4;
|
walther@60318
|
287 |
|
walther@60318
|
288 |
if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";
|
walther@60318
|
289 |
if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";
|
walther@60318
|
290 |
if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";
|
walther@60318
|
291 |
if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";
|
walther@60318
|
292 |
|
walther@60318
|
293 |
if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
|
walther@60318
|
294 |
if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
|
walther@60318
|
295 |
if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
|
walther@60318
|
296 |
if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
|
walther@60318
|
297 |
|
walther@60318
|
298 |
if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
|
walther@60318
|
299 |
if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
|
walther@60318
|
300 |
if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
|
walther@60318
|
301 |
if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
|
walther@60318
|
302 |
|
walther@60318
|
303 |
if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
|
walther@60318
|
304 |
if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
|
walther@60318
|
305 |
if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
|
walther@60318
|
306 |
if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
|
walther@60318
|
307 |
|
walther@60318
|
308 |
if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
|
walther@60318
|
309 |
if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
|
walther@60318
|
310 |
if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
|
walther@60318
|
311 |
if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
|
walther@60318
|
312 |
|
walther@60318
|
313 |
"~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
|
walther@60318
|
314 |
degree_ord: term list * term list -> order;
|
walther@60318
|
315 |
|
walther@60318
|
316 |
if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
|
walther@60318
|
317 |
if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
|
walther@60318
|
318 |
if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
|
walther@60318
|
319 |
if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
|
walther@60318
|
320 |
|
walther@60318
|
321 |
if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
|
walther@60318
|
322 |
if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
|
walther@60318
|
323 |
if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
|
walther@60318
|
324 |
if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
|
walther@60318
|
325 |
|
walther@60318
|
326 |
if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
|
walther@60318
|
327 |
if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
|
walther@60318
|
328 |
if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
|
walther@60318
|
329 |
if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
|
walther@60318
|
330 |
|
walther@60318
|
331 |
if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
|
walther@60318
|
332 |
if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
|
walther@60318
|
333 |
if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
|
walther@60318
|
334 |
if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
|
walther@60318
|
335 |
|
walther@60318
|
336 |
"~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
|
walther@60318
|
337 |
dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
|
walther@60318
|
338 |
dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
|
walther@60318
|
339 |
dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
|
walther@60318
|
340 |
val xxx = dict_cond_ord var_ord_revPow is_nums;
|
walther@60318
|
341 |
(* output from:
|
walther@60318
|
342 |
fun var_ord_revPow (a,b: term) =
|
walther@60318
|
343 |
(@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};
|
walther@60318
|
344 |
@ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
|
walther@60318
|
345 |
prod_ord string_ord string_ord_rev
|
walther@60318
|
346 |
((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
|
walther@60318
|
347 |
*)
|
walther@60318
|
348 |
if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
|
walther@60318
|
349 |
if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
|
walther@60318
|
350 |
if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
|
walther@60318
|
351 |
if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
|
walther@60318
|
352 |
(*-------------------------------------------------------------------------------------*)
|
walther@60318
|
353 |
if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
|
walther@60318
|
354 |
if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
|
walther@60318
|
355 |
if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
|
walther@60318
|
356 |
if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
|
walther@60318
|
357 |
(*-------------------------------------------------------------------------------------*)
|
walther@60318
|
358 |
if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
|
walther@60318
|
359 |
if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
|
walther@60318
|
360 |
if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
|
walther@60318
|
361 |
if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
|
walther@60318
|
362 |
(*-------------------------------------------------------------------------------------*)
|
walther@60318
|
363 |
if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
|
walther@60318
|
364 |
if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
|
walther@60318
|
365 |
if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
|
walther@60318
|
366 |
if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
|
walther@60318
|
367 |
(*-------------------------------------------------------------------------------------*)
|
walther@60318
|
368 |
|
walther@60318
|
369 |
"~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
|
walther@60318
|
370 |
(* we check all at once//*)
|
walther@60318
|
371 |
if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
|
walther@60318
|
372 |
if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
|
walther@60318
|
373 |
if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
|
walther@60318
|
374 |
if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
|
walther@60318
|
375 |
|
walther@60318
|
376 |
"~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
|
walther@60318
|
377 |
compare_koeff_ord: term list * term list -> order;
|
walther@60318
|
378 |
(* we check all at once//*)
|
walther@60318
|
379 |
if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
|
walther@60318
|
380 |
if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
|
walther@60318
|
381 |
if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
|
walther@60318
|
382 |
if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
|
walther@60318
|
383 |
|
walther@60318
|
384 |
if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
|
walther@60318
|
385 |
if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
|
walther@60318
|
386 |
if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
|
walther@60318
|
387 |
if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
|
walther@60318
|
388 |
|
walther@60318
|
389 |
if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
|
walther@60318
|
390 |
if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
|
walther@60318
|
391 |
if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
|
walther@60318
|
392 |
if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
|
walther@60318
|
393 |
|
walther@60318
|
394 |
if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
|
walther@60318
|
395 |
if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
|
walther@60318
|
396 |
if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
|
walther@60318
|
397 |
if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
|
walther@60318
|
398 |
|
walther@60318
|
399 |
"~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
|
walther@60318
|
400 |
get_koeff_of_mon: term list -> term option;
|
walther@60318
|
401 |
|
walther@60318
|
402 |
val SOME xxx1 = get_koeff_of_mon eee1;
|
walther@60318
|
403 |
val SOME xxx2 = get_koeff_of_mon eee2;
|
walther@60318
|
404 |
val SOME xxx3 = get_koeff_of_mon eee3;
|
walther@60318
|
405 |
val NONE = get_koeff_of_mon eee4;
|
walther@60318
|
406 |
|
walther@60318
|
407 |
if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
|
walther@60318
|
408 |
if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
|
walther@60318
|
409 |
if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
|
walther@60318
|
410 |
|
walther@60318
|
411 |
"~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
|
walther@60318
|
412 |
koeff2ordStr: term option -> string;
|
walther@60318
|
413 |
if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
|
walther@60318
|
414 |
if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
|
walther@60318
|
415 |
if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
|
walther@60318
|
416 |
if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
|
walther@60318
|
417 |
|
walther@60318
|
418 |
|
walther@60318
|
419 |
"-------- examples from textbook Schalk I ------------------------------------------------------";
|
walther@60318
|
420 |
"-------- examples from textbook Schalk I ------------------------------------------------------";
|
walther@60318
|
421 |
"-------- examples from textbook Schalk I ------------------------------------------------------";
|
neuper@38036
|
422 |
"-----SPB Schalk I p.63 No.267b ---";
|
Walther@60565
|
423 |
val t = TermC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
|
walther@60318
|
424 |
val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60318
|
425 |
if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
|
neuper@42395
|
426 |
then () else error "poly.sml: diff.behav. in make_polynomial 1";
|
neuper@37906
|
427 |
|
neuper@38036
|
428 |
"-----SPB Schalk I p.63 No.275b ---";
|
Walther@60565
|
429 |
val t = TermC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
|
neuper@42395
|
430 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@60318
|
431 |
if UnparseC.term t =
|
walther@60318
|
432 |
"3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4"
|
neuper@42395
|
433 |
then () else error "poly.sml: diff.behav. in make_polynomial 2";
|
neuper@37906
|
434 |
|
neuper@38036
|
435 |
"-----SPB Schalk I p.63 No.279b ---";
|
Walther@60565
|
436 |
val t = TermC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";
|
neuper@42395
|
437 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@60318
|
438 |
if UnparseC.term t =
|
walther@60318
|
439 |
("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
|
walther@60318
|
440 |
"- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
|
walther@60318
|
441 |
"- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
|
walther@60318
|
442 |
" * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
|
neuper@42395
|
443 |
then () else error "poly.sml: diff.behav. in make_polynomial 3";
|
walther@60318
|
444 |
(*associate poly*)
|
neuper@37906
|
445 |
|
neuper@38036
|
446 |
"-----SPB Schalk I p.63 No.291 ---";
|
Walther@60565
|
447 |
val t = TermC.parse_test @{context} "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";
|
neuper@42395
|
448 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@60318
|
449 |
if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
|
neuper@42395
|
450 |
then () else error "poly.sml: diff.behav. in make_polynomial 4";
|
neuper@37906
|
451 |
|
neuper@38036
|
452 |
"-----SPB Schalk I p.64 No.295c ---";
|
Walther@60565
|
453 |
val t = TermC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
|
neuper@42395
|
454 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@60318
|
455 |
if UnparseC.term t =
|
walther@60318
|
456 |
"169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18"
|
neuper@42395
|
457 |
then ()else error "poly.sml: diff.behav. in make_polynomial 5";
|
neuper@37906
|
458 |
|
neuper@38036
|
459 |
"-----SPB Schalk I p.64 No.299a ---";
|
Walther@60565
|
460 |
val t = TermC.parse_test @{context} "(x - y)*(x + y)";
|
neuper@42395
|
461 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@60318
|
462 |
if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
|
neuper@42395
|
463 |
then () else error "poly.sml: diff.behav. in make_polynomial 6";
|
neuper@37906
|
464 |
|
neuper@38036
|
465 |
"-----SPB Schalk I p.64 No.300c ---";
|
Walther@60565
|
466 |
val t = TermC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
|
neuper@42395
|
467 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@60318
|
468 |
if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
|
neuper@42395
|
469 |
then () else error "poly.sml: diff.behav. in make_polynomial 7";
|
neuper@37906
|
470 |
|
neuper@38036
|
471 |
"-----SPB Schalk I p.64 No.302 ---";
|
Walther@60565
|
472 |
val t = TermC.parse_test @{context}
|
walther@60242
|
473 |
"(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
|
neuper@42395
|
474 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
|
walther@59868
|
475 |
if UnparseC.term t = "0"
|
neuper@42395
|
476 |
then () else error "poly.sml: diff.behav. in make_polynomial 8";
|
neuper@42395
|
477 |
(* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
|
neuper@37906
|
478 |
|
neuper@38036
|
479 |
"-----SPB Schalk I p.64 No.306a ---";
|
Walther@60565
|
480 |
val t = TermC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
|
walther@59868
|
481 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60318
|
482 |
if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
|
walther@60329
|
483 |
else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 = - 2 * x \<up> 4";
|
neuper@37906
|
484 |
|
neuper@37906
|
485 |
(*WN071729 when reducing "rls reduce_012_" for Schaerding,
|
neuper@37906
|
486 |
the above resulted in the term below ... but reduces from then correctly*)
|
Walther@60565
|
487 |
val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
|
walther@59868
|
488 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60318
|
489 |
if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
|
neuper@42395
|
490 |
then () else error "poly.sml: diff.behav. in make_polynomial 9b";
|
neuper@37906
|
491 |
|
neuper@38036
|
492 |
"-----SPB Schalk I p.64 No.296a ---";
|
Walther@60565
|
493 |
val t = TermC.parse_test @{context} "(x - a) \<up> 3";
|
walther@59868
|
494 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60318
|
495 |
|
Walther@60565
|
496 |
val NONE = eval_is_even "aaa" "bbb" (TermC.parse_test @{context} "3::real") "ccc";
|
walther@60318
|
497 |
|
walther@60318
|
498 |
if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
|
neuper@38031
|
499 |
then () else error "poly.sml: diff.behav. in make_polynomial 10";
|
neuper@37906
|
500 |
|
neuper@38036
|
501 |
"-----SPB Schalk I p.64 No.296c ---";
|
Walther@60565
|
502 |
val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
|
walther@59868
|
503 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60318
|
504 |
if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
|
neuper@38031
|
505 |
then () else error "poly.sml: diff.behav. in make_polynomial 11";
|
neuper@37906
|
506 |
|
neuper@38036
|
507 |
"-----SPB Schalk I p.62 No.242c ---";
|
Walther@60565
|
508 |
val t = TermC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
|
walther@59868
|
509 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60318
|
510 |
if UnparseC.term t = "1"
|
neuper@42395
|
511 |
then () else error "poly.sml: diff.behav. in make_polynomial 12";
|
neuper@37906
|
512 |
|
neuper@38036
|
513 |
"-----SPB Schalk I p.60 No.209a ---";
|
Walther@60565
|
514 |
val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
|
walther@59868
|
515 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60242
|
516 |
if UnparseC.term t = "a \<up> 7"
|
neuper@42395
|
517 |
then () else error "poly.sml: diff.behav. in make_polynomial 13";
|
neuper@37906
|
518 |
|
neuper@38036
|
519 |
"-----SPB Schalk I p.60 No.209d ---";
|
Walther@60565
|
520 |
val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
|
walther@59868
|
521 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60242
|
522 |
if UnparseC.term t = "d \<up> 3"
|
neuper@42395
|
523 |
then () else error "poly.sml: diff.behav. in make_polynomial 14";
|
neuper@37906
|
524 |
|
walther@60318
|
525 |
"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
|
walther@60318
|
526 |
"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
|
walther@60318
|
527 |
"-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
|
neuper@38036
|
528 |
"-----Schalk I p.64 No.303 ---";
|
Walther@60565
|
529 |
val t = TermC.parse_test @{context} "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
|
walther@60318
|
530 |
(*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
|
walther@60318
|
531 |
val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60242
|
532 |
if UnparseC.term t = "1280 * b \<up> 4"
|
neuper@42395
|
533 |
then () else error "poly.sml: diff.behav. in make_polynomial 14b";
|
neuper@37906
|
534 |
(* Richtig - aber Binomische Formel wurde nicht verwendet! *)
|
walther@60318
|
535 |
(*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
|
neuper@37906
|
536 |
|
walther@60318
|
537 |
"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
|
walther@60318
|
538 |
"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
|
walther@60318
|
539 |
"-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
|
neuper@38036
|
540 |
"-----SPO ---";
|
Walther@60565
|
541 |
val t = TermC.parse_test @{context} "a + a + a";
|
walther@59868
|
542 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@59868
|
543 |
if UnparseC.term t = "3 * a" then ()
|
neuper@38031
|
544 |
else error "poly.sml: diff.behav. in make_polynomial 16";
|
neuper@38036
|
545 |
"-----SPO ---";
|
Walther@60565
|
546 |
val t = TermC.parse_test @{context} "a + b + b + b";
|
walther@59868
|
547 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@59868
|
548 |
if UnparseC.term t = "a + 3 * b" then ()
|
neuper@38031
|
549 |
else error "poly.sml: diff.behav. in make_polynomial 17";
|
neuper@38036
|
550 |
"-----SPO ---";
|
Walther@60565
|
551 |
val t = TermC.parse_test @{context} "b * a * a";
|
walther@59868
|
552 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60242
|
553 |
if UnparseC.term t = "a \<up> 2 * b" then ()
|
neuper@38031
|
554 |
else error "poly.sml: diff.behav. in make_polynomial 21";
|
neuper@38036
|
555 |
"-----SPO ---";
|
Walther@60565
|
556 |
val t = TermC.parse_test @{context} "(a \<up> 2) \<up> 3";
|
walther@59868
|
557 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60242
|
558 |
if UnparseC.term t = "a \<up> 6" then ()
|
neuper@38031
|
559 |
else error "poly.sml: diff.behav. in make_polynomial 22";
|
neuper@38036
|
560 |
"-----SPO ---";
|
Walther@60565
|
561 |
val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
|
walther@59868
|
562 |
val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
|
walther@60242
|
563 |
if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
|
neuper@38031
|
564 |
else error "poly.sml: diff.behav. in make_polynomial 23";
|
neuper@38036
|
565 |
"-----SPO ---";
|
Walther@60565
|
566 |
val t = TermC.parse_test @{context} "a * b * b \<up> (- 1) + a";
|
Walther@60521
|
567 |
val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
|
walther@60318
|
568 |
if UnparseC.term t = "2 * a" then ()
|
neuper@38031
|
569 |
else error "poly.sml: diff.behav. in make_polynomial 25";
|
neuper@38036
|
570 |
"-----SPO ---";
|
Walther@60565
|
571 |
val t = TermC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
|
Walther@60521
|
572 |
val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
|
walther@60318
|
573 |
if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
|
neuper@38031
|
574 |
then () else error "poly.sml: diff.behav. in make_polynomial 26";
|
neuper@37906
|
575 |
|
neuper@42395
|
576 |
(*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
|
neuper@38036
|
577 |
"-----SPO ---";
|
Walther@60565
|
578 |
val t = TermC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
|
Walther@60521
|
579 |
val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
|
walther@60242
|
580 |
if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
|
neuper@42395
|
581 |
then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
|
neuper@42395
|
582 |
|
Walther@60565
|
583 |
val t = TermC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
|
Walther@60521
|
584 |
val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
|
walther@60242
|
585 |
if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
|
neuper@42395
|
586 |
then () else error "poly.sml: diff.behav. in make_polynomial 28";
|
neuper@37906
|
587 |
|
walther@60318
|
588 |
"-------- check pbl 'polynomial simplification' -----------------------------------------------";
|
walther@60318
|
589 |
"-------- check pbl 'polynomial simplification' -----------------------------------------------";
|
walther@60318
|
590 |
"-------- check pbl 'polynomial simplification' -----------------------------------------------";
|
walther@60242
|
591 |
val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
|
neuper@38036
|
592 |
"-----0 ---";
|
Walther@60556
|
593 |
case Refine.refine_PIDE @{context} fmz ["polynomial", "simplification"] of
|
walther@59984
|
594 |
[M_Match.Matches (["polynomial", "simplification"], _)] => ()
|
walther@59968
|
595 |
| _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
|
neuper@37906
|
596 |
(*...if there is an error, then ...*)
|
neuper@37906
|
597 |
|
walther@60329
|
598 |
"----- 1 ---";
|
wneuper@59348
|
599 |
(*default_print_depth 7;*)
|
Walther@60559
|
600 |
val pbt = Problem.from_store @{context} ["polynomial", "simplification"];
|
wneuper@59348
|
601 |
(*default_print_depth 3;*)
|
neuper@37906
|
602 |
(*if there is ...
|
walther@59984
|
603 |
> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
|
walther@59901
|
604 |
... then Rewrite.trace_on:*)
|
walther@60242
|
605 |
|
walther@60329
|
606 |
"----- 2 ---";
|
walther@59984
|
607 |
M_Match.match_pbl fmz pbt;
|
neuper@37906
|
608 |
(*... if there is no rewrite, then there is something wrong with prls*)
|
neuper@52101
|
609 |
|
neuper@38036
|
610 |
"-----3 ---";
|
wneuper@59348
|
611 |
(*default_print_depth 7;*)
|
Walther@60559
|
612 |
val prls = (#prls o Problem.from_store @{context}) ["polynomial", "simplification"];
|
wneuper@59348
|
613 |
(*default_print_depth 3;*)
|
Walther@60565
|
614 |
val t = TermC.parse_test @{context} "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
|
neuper@37926
|
615 |
val SOME (t',_) = rewrite_set_ thy false prls t;
|
neuper@48760
|
616 |
if t' = @{term True} then ()
|
neuper@38031
|
617 |
else error "poly.sml: diff.behav. in check pbl 'polynomial..";
|
walther@60329
|
618 |
(*... if this works, but -- 1-- does still NOT work, check types:*)
|
neuper@37906
|
619 |
|
neuper@38036
|
620 |
"-----4 ---";
|
neuper@42395
|
621 |
(*show_types:=true;*)
|
neuper@37906
|
622 |
(*
|
walther@59984
|
623 |
> val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
|
neuper@37906
|
624 |
val wh = [False "(t_::real => real) (is_polyexp::real)"]
|
walther@60242
|
625 |
...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
|
walther@59984
|
626 |
val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
|
neuper@42395
|
627 |
(*show_types:=false;*)
|
neuper@37906
|
628 |
|
walther@59787
|
629 |
|
walther@60318
|
630 |
"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
|
walther@60318
|
631 |
"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
|
walther@60318
|
632 |
"-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
|
walther@60242
|
633 |
val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
|
neuper@37906
|
634 |
val (dI',pI',mI') =
|
walther@59997
|
635 |
("Poly",["polynomial", "simplification"],
|
walther@59997
|
636 |
["simplification", "for_polynomials"]);
|
neuper@37906
|
637 |
val p = e_pos'; val c = [];
|
neuper@37906
|
638 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
|
walther@60242
|
639 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)
|
walther@59787
|
640 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
|
walther@59787
|
641 |
|
walther@59997
|
642 |
(*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
|
walther@60242
|
643 |
(*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"
|
walther@59943
|
644 |
(*+*)then () else error "No.267b: I_Model.T CHANGED";
|
walther@59997
|
645 |
( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
|
walther@59787
|
646 |
|
walther@59787
|
647 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
|
walther@59787
|
648 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
|
walther@59787
|
649 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
|
walther@59787
|
650 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
|
walther@59787
|
651 |
(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
|
walther@59787
|
652 |
|
walther@60242
|
653 |
(*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
|
walther@59787
|
654 |
(*+*)then () else error "";
|
walther@59787
|
655 |
|
walther@59787
|
656 |
(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
|
walther@59787
|
657 |
|
walther@60318
|
658 |
(*+*)if f2str f = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
|
walther@60329
|
659 |
(*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b - 1";
|
walther@59787
|
660 |
|
walther@59790
|
661 |
(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
|
walther@59787
|
662 |
|
walther@59787
|
663 |
|
neuper@37906
|
664 |
|
walther@60318
|
665 |
"-------- interSteps for Schalk 299a -----------------------------------------------------------";
|
walther@60318
|
666 |
"-------- interSteps for Schalk 299a -----------------------------------------------------------";
|
walther@60318
|
667 |
"-------- interSteps for Schalk 299a -----------------------------------------------------------";
|
Walther@60549
|
668 |
States.reset ();
|
neuper@37906
|
669 |
CalcTree
|
neuper@42395
|
670 |
[(["Term ((x - y)*(x + (y::real)))", "normalform N"],
|
walther@59997
|
671 |
("Poly",["polynomial", "simplification"],
|
walther@59997
|
672 |
["simplification", "for_polynomials"]))];
|
neuper@37906
|
673 |
Iterator 1;
|
neuper@37906
|
674 |
moveActiveRoot 1;
|
wneuper@59248
|
675 |
autoCalculate 1 CompleteCalc;
|
Walther@60549
|
676 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
neuper@37906
|
677 |
|
walther@59833
|
678 |
interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
|
Walther@60549
|
679 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
neuper@37906
|
680 |
if existpt' ([1,1], Frm) pt then ()
|
neuper@38031
|
681 |
else error "poly.sml: interSteps doesnt work again 1";
|
neuper@37906
|
682 |
|
walther@59833
|
683 |
interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
|
Walther@60549
|
684 |
val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
|
neuper@42395
|
685 |
(*============ inhibit exn WN120316 ==============================================
|
neuper@37906
|
686 |
if existpt' ([1,1,1], Frm) pt then ()
|
neuper@38031
|
687 |
else error "poly.sml: interSteps doesnt work again 2";
|
neuper@42395
|
688 |
============ inhibit exn WN120316 ==============================================*)
|
neuper@37906
|
689 |
|
walther@60318
|
690 |
"-------- ord_make_polynomial ------------------------------------------------------------------";
|
walther@60318
|
691 |
"-------- ord_make_polynomial ------------------------------------------------------------------";
|
walther@60318
|
692 |
"-------- ord_make_polynomial ------------------------------------------------------------------";
|
Walther@60565
|
693 |
val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
|
Walther@60565
|
694 |
val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
|
neuper@37906
|
695 |
|
Walther@60521
|
696 |
if ord_make_polynomial true @{theory} [] (t1, t2) then ()
|
neuper@38031
|
697 |
else error "poly.sml: diff.behav. in ord_make_polynomial";
|
walther@60318
|
698 |
(*SO: WHY IS THERE NO REWRITING ...*)
|
neuper@37906
|
699 |
|
Walther@60565
|
700 |
val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)";
|
Walther@60521
|
701 |
(*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;
|
walther@60325
|
702 |
(*
|
walther@60325
|
703 |
WHY IS THERE NO REWRITING ?!?
|
walther@60325
|
704 |
most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
|
walther@60325
|
705 |
while order_add_mult uses isac's rewriter -- and this is used rarely!
|
walther@60318
|
706 |
*)
|
neuper@37906
|
707 |
|