wneuper@59430
|
1 |
(* Knowledge for tests, specifically simplified or bound to a fixed state
|
wneuper@59430
|
2 |
for the purpose of simplifying tests.
|
neuper@37954
|
3 |
Author: Walther Neuper 2003
|
neuper@37954
|
4 |
(c) due to copyright terms
|
wneuper@59432
|
5 |
|
wneuper@59432
|
6 |
Notes on cleanup:
|
wneuper@59432
|
7 |
(0) revert import Test -- DiophantEq, this raises issues related to (1..4)
|
wneuper@59432
|
8 |
(1) transfer methods to respective theories, if only test, then hierarchy at ["...", "Test"]:
|
wneuper@59432
|
9 |
differentiate, root equatioh, polynomial equation, diophantine equation
|
wneuper@59432
|
10 |
(2) transfer problems accordingly
|
wneuper@59432
|
11 |
(3) rearrange rls according to (1..2)
|
wneuper@59432
|
12 |
(4) rearrange axiomatizations according to (3)
|
neuper@37954
|
13 |
*)
|
neuper@37906
|
14 |
|
wneuper@59424
|
15 |
theory Test imports Base_Tools Poly Rational Root Diff begin
|
neuper@37906
|
16 |
|
wneuper@59551
|
17 |
section \<open>consts for problems\<close>
|
wneuper@59430
|
18 |
consts
|
neuper@42008
|
19 |
"is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
|
neuper@42008
|
20 |
"contains'_root" :: "'a => bool" ("contains'_root _" 10)
|
neuper@42008
|
21 |
|
neuper@42008
|
22 |
"precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
|
neuper@42008
|
23 |
"precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
|
neuper@42008
|
24 |
"precond'_submet" :: "'a => bool" ("precond'_submet _" 10)
|
neuper@42008
|
25 |
"precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
|
neuper@37906
|
26 |
|
neuper@37906
|
27 |
|
wneuper@59472
|
28 |
section \<open>functions\<close>
|
wneuper@59472
|
29 |
ML \<open>
|
wneuper@59430
|
30 |
fun bin_o (Const (op_, (Type ("fun", [Type (s2, []), Type ("fun", [Type (s4, _),Type (s5, _)])]))))
|
wneuper@59430
|
31 |
= if s2 = s4 andalso s4 = s5 then [op_] else []
|
wneuper@59430
|
32 |
| bin_o _ = [];
|
neuper@37906
|
33 |
|
wneuper@59430
|
34 |
fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)
|
wneuper@59430
|
35 |
| bin_op t = bin_o t;
|
wneuper@59430
|
36 |
fun is_bin_op t = (bin_op t <> []);
|
neuper@37906
|
37 |
|
wneuper@59430
|
38 |
fun bin_op_arg1 ((Const (_,
|
wneuper@59430
|
39 |
(Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) $ arg1 $ _) = arg1
|
walther@59868
|
40 |
| bin_op_arg1 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);
|
wneuper@59430
|
41 |
fun bin_op_arg2 ((Const (_,
|
wneuper@59430
|
42 |
(Type ("fun", [Type (_, []),Type ("fun", [Type _, Type _])]))))$ _ $ arg2) = arg2
|
walther@59868
|
43 |
| bin_op_arg2 t = raise ERROR ("bin_op_arg1: t = " ^ UnparseC.term t);
|
neuper@37906
|
44 |
|
wneuper@59430
|
45 |
exception NO_EQUATION_TERM;
|
wneuper@59430
|
46 |
fun is_equation ((Const ("HOL.eq",
|
wneuper@59430
|
47 |
(Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ _ $ _) = true
|
wneuper@59430
|
48 |
| is_equation _ = false;
|
wneuper@59430
|
49 |
fun equ_lhs ((Const ("HOL.eq",
|
wneuper@59430
|
50 |
(Type ("fun", [Type (_, []), Type ("fun", [Type (_, []),Type ("bool",[])])])))) $ l $ _) = l
|
wneuper@59430
|
51 |
| equ_lhs _ = raise NO_EQUATION_TERM;
|
wneuper@59430
|
52 |
fun equ_rhs ((Const ("HOL.eq", (Type ("fun",
|
wneuper@59430
|
53 |
[Type (_, []), Type ("fun", [Type (_, []), Type ("bool",[])])])))) $ _ $ r) = r
|
wneuper@59430
|
54 |
| equ_rhs _ = raise NO_EQUATION_TERM;
|
neuper@37906
|
55 |
|
wneuper@59430
|
56 |
fun atom (Const (_, Type (_,[]))) = true
|
wneuper@59430
|
57 |
| atom (Free (_, Type (_,[]))) = true
|
wneuper@59430
|
58 |
| atom (Var (_, Type (_,[]))) = true
|
wneuper@59430
|
59 |
| atom((Const ("Bin.integ_of_bin",_)) $ _) = true
|
wneuper@59430
|
60 |
| atom _ = false;
|
wneuper@59430
|
61 |
|
wneuper@59430
|
62 |
fun varids (Const (s, Type (_,[]))) = [strip_thy s]
|
wneuper@59430
|
63 |
| varids (Free (s, Type (_,[]))) = if TermC.is_num' s then [] else [strip_thy s]
|
wneuper@59430
|
64 |
| varids (Var((s, _),Type (_,[]))) = [strip_thy s]
|
wneuper@59430
|
65 |
(*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
|
wneuper@59430
|
66 |
| varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
|
wneuper@59430
|
67 |
| varids (Abs (a, _, t)) = union op = [a] (varids t)
|
wneuper@59430
|
68 |
| varids (t1 $ t2) = union op = (varids t1) (varids t2)
|
wneuper@59430
|
69 |
| varids _ = [];
|
wneuper@59430
|
70 |
|
wneuper@59430
|
71 |
fun bin_ops_only ((Const op_) $ t1 $ t2) =
|
wneuper@59430
|
72 |
if is_bin_op (Const op_) then bin_ops_only t1 andalso bin_ops_only t2 else false
|
wneuper@59430
|
73 |
| bin_ops_only t = if atom t then true else bin_ops_only t;
|
wneuper@59430
|
74 |
|
wneuper@59430
|
75 |
fun polynomial opl t _(* bdVar TODO *) =
|
wneuper@59430
|
76 |
subset op = (bin_op t, opl) andalso (bin_ops_only t);
|
wneuper@59430
|
77 |
|
wneuper@59430
|
78 |
fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)
|
wneuper@59430
|
79 |
andalso polynomial opl (equ_lhs t) bdVar
|
wneuper@59430
|
80 |
andalso polynomial opl (equ_rhs t) bdVar
|
wneuper@59430
|
81 |
andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
|
wneuper@59430
|
82 |
subset op = (varids bdVar, varids (equ_lhs t)));
|
wneuper@59430
|
83 |
|
wneuper@59430
|
84 |
fun max (a,b) = if a < b then b else a;
|
wneuper@59430
|
85 |
|
wneuper@59430
|
86 |
fun degree addl mul bdVar t =
|
wneuper@59430
|
87 |
let
|
wneuper@59430
|
88 |
fun deg _ _ v (Const (s, Type (_, []))) = if v=strip_thy s then 1 else 0
|
wneuper@59430
|
89 |
| deg _ _ v (Free (s, Type (_, []))) = if v=strip_thy s then 1 else 0
|
wneuper@59430
|
90 |
| deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy s then 1 else 0
|
wneuper@59430
|
91 |
(*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
|
wneuper@59430
|
92 |
| deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0
|
wneuper@59430
|
93 |
| deg addl mul v (h $ t1 $ t2) =
|
wneuper@59430
|
94 |
if subset op = (bin_op h, addl)
|
wneuper@59430
|
95 |
then max (deg addl mul v t1 , deg addl mul v t2)
|
wneuper@59430
|
96 |
else (*mul!*)(deg addl mul v t1) + (deg addl mul v t2)
|
walther@59868
|
97 |
| deg _ _ _ t = raise ERROR ("deg: t = " ^ UnparseC.term t)
|
wneuper@59430
|
98 |
in
|
wneuper@59430
|
99 |
if polynomial (addl @ [mul]) t bdVar
|
wneuper@59430
|
100 |
then SOME (deg addl mul (id_of bdVar) t)
|
wneuper@59430
|
101 |
else (NONE:int option)
|
wneuper@59430
|
102 |
end;
|
wneuper@59430
|
103 |
fun degree_ addl mul bdVar t = (* do not export *)
|
wneuper@59430
|
104 |
let
|
wneuper@59430
|
105 |
fun opt (SOME i)= i
|
wneuper@59430
|
106 |
| opt NONE = 0
|
wneuper@59430
|
107 |
in opt (degree addl mul bdVar t) end;
|
wneuper@59430
|
108 |
|
wneuper@59430
|
109 |
fun linear addl mul t bdVar = (degree_ addl mul bdVar t) < 2;
|
wneuper@59430
|
110 |
|
wneuper@59430
|
111 |
fun linear_equ addl mul bdVar t =
|
wneuper@59430
|
112 |
if is_equation t
|
wneuper@59430
|
113 |
then
|
wneuper@59430
|
114 |
let
|
wneuper@59430
|
115 |
val degl = degree_ addl mul bdVar (equ_lhs t);
|
wneuper@59430
|
116 |
val degr = degree_ addl mul bdVar (equ_rhs t)
|
wneuper@59430
|
117 |
in if (degl>0 orelse degr>0)andalso max(degl,degr) < 2 then true else false end
|
wneuper@59430
|
118 |
else false;
|
wneuper@59430
|
119 |
(* strip_thy op_ before *)
|
wneuper@59430
|
120 |
fun is_div_op (dv, (Const (op_,
|
wneuper@59430
|
121 |
(Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) ) = (dv = strip_thy op_)
|
wneuper@59430
|
122 |
| is_div_op _ = false;
|
wneuper@59430
|
123 |
|
wneuper@59430
|
124 |
fun is_denom bdVar div_op t =
|
wneuper@59430
|
125 |
let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
|
wneuper@59430
|
126 |
| is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
|
wneuper@59430
|
127 |
| is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
|
wneuper@59430
|
128 |
| is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
|
wneuper@59430
|
129 |
| is bool[v]dv (h$n$d) =
|
wneuper@59430
|
130 |
if is_div_op(dv,h)
|
wneuper@59430
|
131 |
then (is false[v]dv n)orelse(is true[v]dv d)
|
wneuper@59430
|
132 |
else (is bool [v]dv n)orelse(is bool[v]dv d)
|
wneuper@59430
|
133 |
in is false (varids bdVar) (strip_thy div_op) t end;
|
wneuper@59430
|
134 |
|
wneuper@59430
|
135 |
|
wneuper@59430
|
136 |
fun rational t div_op bdVar =
|
wneuper@59430
|
137 |
is_denom bdVar div_op t andalso bin_ops_only t;
|
wneuper@59430
|
138 |
|
wneuper@59472
|
139 |
\<close>
|
wneuper@59430
|
140 |
|
wneuper@59472
|
141 |
section \<open>axiomatizations\<close>
|
neuper@52148
|
142 |
axiomatization where (*TODO: prove as theorems*)
|
neuper@37906
|
143 |
|
neuper@52148
|
144 |
radd_mult_distrib2: "(k::real) * (m + n) = k * m + k * n" and
|
neuper@52148
|
145 |
rdistr_right_assoc: "(k::real) + l * n + m * n = k + (l + m) * n" and
|
neuper@52148
|
146 |
rdistr_right_assoc_p: "l * n + (m * n + (k::real)) = (l + m) * n + k" and
|
neuper@52148
|
147 |
rdistr_div_right: "((k::real) + l) / n = k / n + l / n" and
|
neuper@37983
|
148 |
rcollect_right:
|
neuper@52148
|
149 |
"[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n" and
|
neuper@37983
|
150 |
rcollect_one_left:
|
neuper@52148
|
151 |
"m is_const ==> (n::real) + m * n = (1 + m) * n" and
|
neuper@37983
|
152 |
rcollect_one_left_assoc:
|
neuper@52148
|
153 |
"m is_const ==> (k::real) + n + m * n = k + (1 + m) * n" and
|
neuper@37983
|
154 |
rcollect_one_left_assoc_p:
|
neuper@52148
|
155 |
"m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k" and
|
neuper@37906
|
156 |
|
neuper@52148
|
157 |
rtwo_of_the_same: "a + a = 2 * a" and
|
neuper@52148
|
158 |
rtwo_of_the_same_assoc: "(x + a) + a = x + 2 * a" and
|
neuper@52148
|
159 |
rtwo_of_the_same_assoc_p:"a + (a + x) = 2 * a + x" and
|
neuper@37906
|
160 |
|
neuper@52148
|
161 |
rcancel_den: "not(a=0) ==> a * (b / a) = b" and
|
neuper@52148
|
162 |
rcancel_const: "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x" and
|
neuper@52148
|
163 |
rshift_nominator: "(a::real) * b / c = a / c * b" and
|
neuper@37906
|
164 |
|
walther@60242
|
165 |
exp_pow: "(a \<up> b) \<up> c = a \<up> (b * c)" and
|
walther@60242
|
166 |
rsqare: "(a::real) * a = a \<up> 2" and
|
walther@60242
|
167 |
power_1: "(a::real) \<up> 1 = a" and
|
walther@60242
|
168 |
rbinom_power_2: "((a::real) + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and
|
neuper@37906
|
169 |
|
neuper@52148
|
170 |
rmult_1: "1 * k = (k::real)" and
|
neuper@52148
|
171 |
rmult_1_right: "k * 1 = (k::real)" and
|
neuper@52148
|
172 |
rmult_0: "0 * k = (0::real)" and
|
neuper@52148
|
173 |
rmult_0_right: "k * 0 = (0::real)" and
|
neuper@52148
|
174 |
radd_0: "0 + k = (k::real)" and
|
neuper@52148
|
175 |
radd_0_right: "k + 0 = (k::real)" and
|
neuper@37906
|
176 |
|
neuper@37983
|
177 |
radd_real_const_eq:
|
neuper@52148
|
178 |
"[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)" and
|
neuper@37983
|
179 |
radd_real_const:
|
neuper@37906
|
180 |
"[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"
|
neuper@52148
|
181 |
and
|
neuper@37906
|
182 |
(*for AC-operators*)
|
neuper@52148
|
183 |
radd_commute: "(m::real) + (n::real) = n + m" and
|
neuper@52148
|
184 |
radd_left_commute: "(x::real) + (y + z) = y + (x + z)" and
|
neuper@52148
|
185 |
radd_assoc: "(m::real) + n + k = m + (n + k)" and
|
neuper@52148
|
186 |
rmult_commute: "(m::real) * n = n * m" and
|
neuper@52148
|
187 |
rmult_left_commute: "(x::real) * (y * z) = y * (x * z)" and
|
neuper@52148
|
188 |
rmult_assoc: "(m::real) * n * k = m * (n * k)" and
|
neuper@37906
|
189 |
|
neuper@37906
|
190 |
(*for equations: 'bdv' is a meta-constant*)
|
neuper@52148
|
191 |
risolate_bdv_add: "((k::real) + bdv = m) = (bdv = m + (-1)*k)" and
|
neuper@52148
|
192 |
risolate_bdv_mult_add: "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)" and
|
neuper@52148
|
193 |
risolate_bdv_mult: "((n::real) * bdv = m) = (bdv = m / n)" and
|
neuper@37906
|
194 |
|
neuper@37983
|
195 |
rnorm_equation_add:
|
neuper@52148
|
196 |
"~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)" and
|
neuper@37906
|
197 |
|
neuper@37906
|
198 |
(*17.9.02 aus SqRoot.thy------------------------------vvv---*)
|
walther@60262
|
199 |
root_ge0: "0 <= a ==> 0 <= sqrt a = True" and
|
neuper@37906
|
200 |
(*should be dropped with better simplification in eval_rls ...*)
|
neuper@37983
|
201 |
root_add_ge0:
|
neuper@52148
|
202 |
"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True" and
|
neuper@37983
|
203 |
root_ge0_1:
|
neuper@52148
|
204 |
"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True" and
|
neuper@37983
|
205 |
root_ge0_2:
|
neuper@52148
|
206 |
"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True" and
|
neuper@37906
|
207 |
|
neuper@37906
|
208 |
|
walther@60242
|
209 |
rroot_square_inv: "(sqrt a) \<up> 2 = a" and
|
neuper@52148
|
210 |
rroot_times_root: "sqrt a * sqrt b = sqrt(a*b)" and
|
neuper@52148
|
211 |
rroot_times_root_assoc: "(a * sqrt b) * sqrt c = a * sqrt(b*c)" and
|
neuper@52148
|
212 |
rroot_times_root_assoc_p: "sqrt b * (sqrt c * a)= sqrt(b*c) * a" and
|
neuper@37906
|
213 |
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
(*for root-equations*)
|
neuper@37983
|
216 |
square_equation_left:
|
walther@60242
|
217 |
"[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b \<up> 2)))" and
|
neuper@37983
|
218 |
square_equation_right:
|
walther@60242
|
219 |
"[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a \<up> 2)=b))" and
|
neuper@37906
|
220 |
(*causes frequently non-termination:*)
|
neuper@37983
|
221 |
square_equation:
|
walther@60242
|
222 |
"[| 0 <= a; 0 <= b |] ==> ((a=b)=((a \<up> 2)=b \<up> 2))" and
|
neuper@37906
|
223 |
|
neuper@52148
|
224 |
risolate_root_add: "(a+ sqrt c = d) = ( sqrt c = d + (-1)*a)" and
|
neuper@52148
|
225 |
risolate_root_mult: "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)" and
|
neuper@52148
|
226 |
risolate_root_div: "(a * sqrt c = d) = ( sqrt c = d / a)" and
|
neuper@37906
|
227 |
|
neuper@37906
|
228 |
(*for polynomial equations of degree 2; linear case in RatArith*)
|
walther@60242
|
229 |
mult_square: "(a*bdv \<up> 2 = b) = (bdv \<up> 2 = b / a)" and
|
walther@60242
|
230 |
constant_square: "(a + bdv \<up> 2 = b) = (bdv \<up> 2 = b + -1*a)" and
|
walther@60242
|
231 |
constant_mult_square: "(a + b*bdv \<up> 2 = c) = (b*bdv \<up> 2 = c + -1*a)" and
|
neuper@37906
|
232 |
|
neuper@37983
|
233 |
square_equality:
|
walther@60242
|
234 |
"0 <= a ==> (x \<up> 2 = a) = ((x=sqrt a) | (x=-1*sqrt a))" and
|
neuper@37983
|
235 |
square_equality_0:
|
walther@60242
|
236 |
"(x \<up> 2 = 0) = (x = 0)" and
|
neuper@37906
|
237 |
|
neuper@37906
|
238 |
(*isolate root on the LEFT hand side of the equation
|
neuper@37906
|
239 |
otherwise shuffling from left to right would not terminate*)
|
neuper@37906
|
240 |
|
neuper@37983
|
241 |
rroot_to_lhs:
|
neuper@52148
|
242 |
"is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
|
neuper@37983
|
243 |
rroot_to_lhs_mult:
|
neuper@52148
|
244 |
"is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
|
neuper@37983
|
245 |
rroot_to_lhs_add_mult:
|
neuper@37906
|
246 |
"is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
|
walther@60242
|
247 |
(*17.9.02 aus SqRoot.thy------------------------------ \<up> ---*)
|
neuper@37906
|
248 |
|
wneuper@59472
|
249 |
section \<open>eval functions\<close>
|
wneuper@59472
|
250 |
ML \<open>
|
neuper@37972
|
251 |
val thy = @{theory};
|
neuper@37972
|
252 |
|
neuper@37954
|
253 |
(** evaluation of numerals and predicates **)
|
neuper@37954
|
254 |
|
neuper@37954
|
255 |
(*does a term contain a root ?*)
|
neuper@37954
|
256 |
fun eval_contains_root (thmid:string) _
|
neuper@37954
|
257 |
(t as (Const("Test.contains'_root",t0) $ arg)) thy =
|
neuper@38053
|
258 |
if member op = (ids_of arg) "sqrt"
|
walther@59870
|
259 |
then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
|
wneuper@59390
|
260 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
walther@59870
|
261 |
else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
|
wneuper@59390
|
262 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
neuper@38053
|
263 |
| eval_contains_root _ _ _ _ = NONE;
|
neuper@42008
|
264 |
|
neuper@42008
|
265 |
(*dummy precondition for root-met of x+1=2*)
|
neuper@42008
|
266 |
fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
|
walther@59870
|
267 |
SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
|
wneuper@59390
|
268 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
neuper@52070
|
269 |
| eval_precond_rootmet _ _ _ _ = NONE;
|
neuper@42008
|
270 |
|
neuper@42008
|
271 |
(*dummy precondition for root-pbl of x+1=2*)
|
neuper@42008
|
272 |
fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
|
walther@59870
|
273 |
SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
|
wneuper@59390
|
274 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
s1210629013@52159
|
275 |
| eval_precond_rootpbl _ _ _ _ = NONE;
|
wneuper@59472
|
276 |
\<close>
|
wneuper@59472
|
277 |
setup \<open>KEStore_Elems.add_calcs
|
wneuper@59403
|
278 |
[("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
|
s1210629013@52145
|
279 |
("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
|
s1210629013@52145
|
280 |
("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
|
wneuper@59430
|
281 |
eval_precond_rootpbl"#Test.precond_rootpbl_"))]
|
wneuper@59472
|
282 |
\<close>
|
wneuper@59472
|
283 |
ML \<open>
|
wneuper@59430
|
284 |
(*8.4.03 aus Poly.ML--------------------------------vvv---
|
wneuper@59430
|
285 |
make_polynomial ---> make_poly
|
wneuper@59430
|
286 |
^-- for user ^-- for systest _ONLY_*)
|
wneuper@59430
|
287 |
|
wneuper@59430
|
288 |
local (*. for make_polytest .*)
|
wneuper@59430
|
289 |
|
wneuper@59430
|
290 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
wneuper@59430
|
291 |
|
wneuper@59430
|
292 |
fun pr_ord EQUAL = "EQUAL"
|
wneuper@59430
|
293 |
| pr_ord LESS = "LESS"
|
wneuper@59430
|
294 |
| pr_ord GREATER = "GREATER";
|
wneuper@59430
|
295 |
|
wneuper@59430
|
296 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
wneuper@59430
|
297 |
(case a of
|
walther@59603
|
298 |
"Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
|
wneuper@59430
|
299 |
| _ => (((a, 0), T), 0))
|
wneuper@59430
|
300 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
|
wneuper@59430
|
301 |
| dest_hd' (Var v) = (v, 2)
|
wneuper@59430
|
302 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
wneuper@59430
|
303 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
|
wneuper@59430
|
304 |
(* RL *)
|
wneuper@59430
|
305 |
fun get_order_pow (t $ (Free(order,_))) =
|
walther@59875
|
306 |
(case TermC.int_opt_of_string order of
|
wneuper@59430
|
307 |
SOME d => d
|
wneuper@59430
|
308 |
| NONE => 0)
|
wneuper@59430
|
309 |
| get_order_pow _ = 0;
|
wneuper@59430
|
310 |
|
wneuper@59430
|
311 |
fun size_of_term' (Const(str,_) $ t) =
|
walther@59603
|
312 |
if "Prog_Expr.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
|
wneuper@59430
|
313 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
wneuper@59430
|
314 |
| size_of_term' (f$t) = size_of_term' f + size_of_term' t
|
wneuper@59430
|
315 |
| size_of_term' _ = 1;
|
wneuper@59430
|
316 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
wneuper@59430
|
317 |
(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
|
wneuper@59430
|
318 |
| ord => ord)
|
wneuper@59430
|
319 |
| term_ord' pr thy (t, u) =
|
wneuper@59430
|
320 |
(if pr then
|
wneuper@59430
|
321 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
walther@59868
|
322 |
val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
|
walther@59868
|
323 |
commas(map UnparseC.term ts) ^ "]\"")
|
walther@59868
|
324 |
val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
|
walther@59868
|
325 |
commas(map UnparseC.term us) ^"]\"")
|
wneuper@59430
|
326 |
val _ = tracing ("size_of_term(t,u)= (" ^
|
wneuper@59430
|
327 |
string_of_int (size_of_term' t) ^ ", " ^
|
wneuper@59430
|
328 |
string_of_int (size_of_term' u) ^ ")")
|
wneuper@59430
|
329 |
val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g))
|
wneuper@59430
|
330 |
val _ = tracing ("terms_ord(ts,us) = " ^
|
wneuper@59430
|
331 |
(pr_ord o terms_ord str false) (ts,us));
|
wneuper@59430
|
332 |
val _ = tracing "-------"
|
wneuper@59430
|
333 |
in () end
|
wneuper@59430
|
334 |
else ();
|
wneuper@59430
|
335 |
case int_ord (size_of_term' t, size_of_term' u) of
|
wneuper@59430
|
336 |
EQUAL =>
|
wneuper@59430
|
337 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
wneuper@59430
|
338 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
wneuper@59430
|
339 |
| ord => ord)
|
wneuper@59430
|
340 |
end
|
wneuper@59430
|
341 |
| ord => ord)
|
wneuper@59430
|
342 |
and hd_ord (f, g) = (* ~ term.ML *)
|
wneuper@59430
|
343 |
prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
|
wneuper@59430
|
344 |
and terms_ord str pr (ts, us) =
|
walther@59881
|
345 |
list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
|
wneuper@59430
|
346 |
in
|
wneuper@59430
|
347 |
|
walther@59910
|
348 |
fun ord_make_polytest (pr:bool) thy (_: subst) tu =
|
wneuper@59430
|
349 |
(term_ord' pr thy(***) tu = LESS );
|
wneuper@59430
|
350 |
|
wneuper@59430
|
351 |
end;(*local*)
|
wneuper@59472
|
352 |
\<close>
|
wneuper@59430
|
353 |
|
wneuper@59472
|
354 |
section \<open>term order\<close>
|
wneuper@59472
|
355 |
ML \<open>
|
walther@59910
|
356 |
fun term_order (_: subst) tu = (term_ordI [] tu = LESS);
|
wneuper@59472
|
357 |
\<close>
|
s1210629013@52145
|
358 |
|
wneuper@59472
|
359 |
section \<open>rulesets\<close>
|
wneuper@59472
|
360 |
ML \<open>
|
neuper@37954
|
361 |
val testerls =
|
walther@59851
|
362 |
Rule_Def.Repeat {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
|
walther@59852
|
363 |
erls = Rule_Set.empty, srls = Rule_Set.Empty,
|
neuper@42451
|
364 |
calc = [], errpatts = [],
|
walther@59871
|
365 |
rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),
|
walther@59871
|
366 |
Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),
|
walther@59871
|
367 |
Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
|
walther@59871
|
368 |
Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
|
walther@59871
|
369 |
Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
|
walther@59871
|
370 |
Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
|
walther@59871
|
371 |
Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
|
walther@59871
|
372 |
Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
|
walther@59871
|
373 |
Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),
|
walther@59871
|
374 |
Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
|
walther@59871
|
375 |
Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
|
neuper@37954
|
376 |
|
walther@59878
|
377 |
Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
|
walther@59878
|
378 |
Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
|
neuper@37954
|
379 |
|
walther@59878
|
380 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
walther@59878
|
381 |
Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
|
walther@59878
|
382 |
Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_"),
|
neuper@37954
|
383 |
|
walther@59878
|
384 |
Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
|
walther@59878
|
385 |
Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
|
neuper@37954
|
386 |
|
walther@59878
|
387 |
Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")],
|
walther@59878
|
388 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
389 |
};
|
wneuper@59472
|
390 |
\<close>
|
wneuper@59472
|
391 |
ML \<open>
|
neuper@37954
|
392 |
(*.for evaluation of conditions in rewrite rules.*)
|
neuper@37954
|
393 |
(*FIXXXXXXME 10.8.02: handle like _simplify*)
|
neuper@37954
|
394 |
val tval_rls =
|
walther@59851
|
395 |
Rule_Def.Repeat{id = "tval_rls", preconds = [],
|
wneuper@59397
|
396 |
rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
|
walther@59852
|
397 |
erls=testerls,srls = Rule_Set.empty,
|
neuper@42451
|
398 |
calc=[], errpatts = [],
|
walther@59871
|
399 |
rules = [Rule.Thm ("refl",ThmC.numerals_to_Free @{thm refl}),
|
walther@59871
|
400 |
Rule.Thm ("order_refl",ThmC.numerals_to_Free @{thm order_refl}),
|
walther@59871
|
401 |
Rule.Thm ("radd_left_cancel_le",ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
|
walther@59871
|
402 |
Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
|
walther@59871
|
403 |
Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
|
walther@59871
|
404 |
Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
|
walther@59871
|
405 |
Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
|
walther@59871
|
406 |
Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
|
walther@59871
|
407 |
Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false}),
|
walther@59871
|
408 |
Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
|
walther@59871
|
409 |
Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
|
neuper@37954
|
410 |
|
walther@59871
|
411 |
Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
|
neuper@37954
|
412 |
|
walther@59871
|
413 |
Rule.Thm ("root_ge0",ThmC.numerals_to_Free @{thm root_ge0}),
|
walther@59871
|
414 |
Rule.Thm ("root_add_ge0",ThmC.numerals_to_Free @{thm root_add_ge0}),
|
walther@59871
|
415 |
Rule.Thm ("root_ge0_1",ThmC.numerals_to_Free @{thm root_ge0_1}),
|
walther@59871
|
416 |
Rule.Thm ("root_ge0_2",ThmC.numerals_to_Free @{thm root_ge0_2}),
|
neuper@37954
|
417 |
|
walther@59878
|
418 |
Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
|
walther@59878
|
419 |
Rule.Eval ("Test.contains'_root", eval_contains_root "#eval_contains_root"),
|
walther@59878
|
420 |
Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
|
walther@59878
|
421 |
Rule.Eval ("Test.contains'_root",
|
neuper@37954
|
422 |
eval_contains_root"#contains_root_"),
|
neuper@37954
|
423 |
|
walther@59878
|
424 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
walther@59878
|
425 |
Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
|
walther@59878
|
426 |
Rule.Eval ("NthRoot.sqrt", eval_sqrt "#sqrt_"),
|
walther@59878
|
427 |
Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
|
neuper@37954
|
428 |
|
walther@59878
|
429 |
Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
|
walther@59878
|
430 |
Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
|
neuper@37954
|
431 |
|
walther@59878
|
432 |
Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")],
|
walther@59878
|
433 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
434 |
};
|
wneuper@59472
|
435 |
\<close>
|
wneuper@59472
|
436 |
setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close>
|
neuper@52155
|
437 |
|
wneuper@59472
|
438 |
ML \<open>
|
neuper@37954
|
439 |
(*make () dissappear*)
|
neuper@37954
|
440 |
val rearrange_assoc =
|
walther@59851
|
441 |
Rule_Def.Repeat{id = "rearrange_assoc", preconds = [],
|
walther@59857
|
442 |
rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
|
walther@59852
|
443 |
erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
|
neuper@37954
|
444 |
rules =
|
walther@59877
|
445 |
[Rule.Thm ("sym_add.assoc",ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
|
walther@59871
|
446 |
Rule.Thm ("sym_rmult_assoc",ThmC.numerals_to_Free (@{thm rmult_assoc} RS @{thm sym}))],
|
walther@59878
|
447 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
448 |
};
|
neuper@37954
|
449 |
|
neuper@37954
|
450 |
val ac_plus_times =
|
walther@59851
|
451 |
Rule_Def.Repeat{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),
|
walther@59852
|
452 |
erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
|
neuper@37954
|
453 |
rules =
|
walther@59871
|
454 |
[Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
|
walther@59871
|
455 |
Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
|
walther@59877
|
456 |
Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
|
walther@59871
|
457 |
Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
|
walther@59871
|
458 |
Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
|
walther@59871
|
459 |
Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc})],
|
walther@59878
|
460 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
461 |
};
|
neuper@37954
|
462 |
|
walther@59871
|
463 |
(*todo: replace by Rewrite("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add)*)
|
neuper@37954
|
464 |
val norm_equation =
|
walther@59857
|
465 |
Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
|
walther@59852
|
466 |
erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
|
walther@59871
|
467 |
rules = [Rule.Thm ("rnorm_equation_add",ThmC.numerals_to_Free @{thm rnorm_equation_add})
|
neuper@37954
|
468 |
],
|
walther@59878
|
469 |
scr = Rule.Empty_Prog
|
wneuper@59406
|
470 |
};
|
wneuper@59472
|
471 |
\<close>
|
wneuper@59472
|
472 |
ML \<open>
|
neuper@37954
|
473 |
(* expects * distributed over + *)
|
neuper@37954
|
474 |
val Test_simplify =
|
walther@59851
|
475 |
Rule_Def.Repeat{id = "Test_simplify", preconds = [],
|
wneuper@59397
|
476 |
rew_ord = ("sqrt_right",sqrt_right false @{theory "Pure"}),
|
walther@59852
|
477 |
erls = tval_rls, srls = Rule_Set.empty,
|
s1210629013@55444
|
478 |
calc=[(*since 040209 filled by prep_rls'*)], errpatts = [],
|
neuper@37954
|
479 |
rules = [
|
walther@59871
|
480 |
Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
|
walther@59871
|
481 |
Rule.Thm ("radd_mult_distrib2",ThmC.numerals_to_Free @{thm radd_mult_distrib2}),
|
walther@59871
|
482 |
Rule.Thm ("rdistr_right_assoc",ThmC.numerals_to_Free @{thm rdistr_right_assoc}),
|
walther@59871
|
483 |
Rule.Thm ("rdistr_right_assoc_p",ThmC.numerals_to_Free @{thm rdistr_right_assoc_p}),
|
walther@59871
|
484 |
Rule.Thm ("rdistr_div_right",ThmC.numerals_to_Free @{thm rdistr_div_right}),
|
walther@59871
|
485 |
Rule.Thm ("rbinom_power_2",ThmC.numerals_to_Free @{thm rbinom_power_2}),
|
neuper@37954
|
486 |
|
walther@59871
|
487 |
Rule.Thm ("radd_commute",ThmC.numerals_to_Free @{thm radd_commute}),
|
walther@59871
|
488 |
Rule.Thm ("radd_left_commute",ThmC.numerals_to_Free @{thm radd_left_commute}),
|
walther@59877
|
489 |
Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
|
walther@59871
|
490 |
Rule.Thm ("rmult_commute",ThmC.numerals_to_Free @{thm rmult_commute}),
|
walther@59871
|
491 |
Rule.Thm ("rmult_left_commute",ThmC.numerals_to_Free @{thm rmult_left_commute}),
|
walther@59871
|
492 |
Rule.Thm ("rmult_assoc",ThmC.numerals_to_Free @{thm rmult_assoc}),
|
neuper@37954
|
493 |
|
walther@59871
|
494 |
Rule.Thm ("radd_real_const_eq",ThmC.numerals_to_Free @{thm radd_real_const_eq}),
|
walther@59871
|
495 |
Rule.Thm ("radd_real_const",ThmC.numerals_to_Free @{thm radd_real_const}),
|
neuper@37954
|
496 |
(* these 2 rules are invers to distr_div_right wrt. termination.
|
neuper@37954
|
497 |
thus they MUST be done IMMEDIATELY before calc *)
|
walther@59878
|
498 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
walther@59878
|
499 |
Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
|
walther@59878
|
500 |
Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
|
walther@59878
|
501 |
Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
|
neuper@37954
|
502 |
|
walther@59871
|
503 |
Rule.Thm ("rcollect_right",ThmC.numerals_to_Free @{thm rcollect_right}),
|
walther@59871
|
504 |
Rule.Thm ("rcollect_one_left",ThmC.numerals_to_Free @{thm rcollect_one_left}),
|
walther@59871
|
505 |
Rule.Thm ("rcollect_one_left_assoc",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc}),
|
walther@59871
|
506 |
Rule.Thm ("rcollect_one_left_assoc_p",ThmC.numerals_to_Free @{thm rcollect_one_left_assoc_p}),
|
neuper@37954
|
507 |
|
walther@59871
|
508 |
Rule.Thm ("rshift_nominator",ThmC.numerals_to_Free @{thm rshift_nominator}),
|
walther@59871
|
509 |
Rule.Thm ("rcancel_den",ThmC.numerals_to_Free @{thm rcancel_den}),
|
walther@59871
|
510 |
Rule.Thm ("rroot_square_inv",ThmC.numerals_to_Free @{thm rroot_square_inv}),
|
walther@59871
|
511 |
Rule.Thm ("rroot_times_root",ThmC.numerals_to_Free @{thm rroot_times_root}),
|
walther@59871
|
512 |
Rule.Thm ("rroot_times_root_assoc_p",ThmC.numerals_to_Free @{thm rroot_times_root_assoc_p}),
|
walther@59871
|
513 |
Rule.Thm ("rsqare",ThmC.numerals_to_Free @{thm rsqare}),
|
walther@59871
|
514 |
Rule.Thm ("power_1",ThmC.numerals_to_Free @{thm power_1}),
|
walther@59871
|
515 |
Rule.Thm ("rtwo_of_the_same",ThmC.numerals_to_Free @{thm rtwo_of_the_same}),
|
walther@59871
|
516 |
Rule.Thm ("rtwo_of_the_same_assoc_p",ThmC.numerals_to_Free @{thm rtwo_of_the_same_assoc_p}),
|
neuper@37954
|
517 |
|
walther@59871
|
518 |
Rule.Thm ("rmult_1",ThmC.numerals_to_Free @{thm rmult_1}),
|
walther@59871
|
519 |
Rule.Thm ("rmult_1_right",ThmC.numerals_to_Free @{thm rmult_1_right}),
|
walther@59871
|
520 |
Rule.Thm ("rmult_0",ThmC.numerals_to_Free @{thm rmult_0}),
|
walther@59871
|
521 |
Rule.Thm ("rmult_0_right",ThmC.numerals_to_Free @{thm rmult_0_right}),
|
walther@59871
|
522 |
Rule.Thm ("radd_0",ThmC.numerals_to_Free @{thm radd_0}),
|
walther@59871
|
523 |
Rule.Thm ("radd_0_right",ThmC.numerals_to_Free @{thm radd_0_right})
|
neuper@37954
|
524 |
],
|
walther@59878
|
525 |
scr = Rule.Empty_Prog
|
s1210629013@55444
|
526 |
(*since 040209 filled by prep_rls': STest_simplify*)
|
wneuper@59406
|
527 |
};
|
wneuper@59472
|
528 |
\<close>
|
wneuper@59472
|
529 |
ML \<open>
|
neuper@37954
|
530 |
(*isolate the root in a root-equation*)
|
neuper@37954
|
531 |
val isolate_root =
|
walther@59857
|
532 |
Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
|
walther@59852
|
533 |
erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
|
walther@59871
|
534 |
rules = [Rule.Thm ("rroot_to_lhs",ThmC.numerals_to_Free @{thm rroot_to_lhs}),
|
walther@59871
|
535 |
Rule.Thm ("rroot_to_lhs_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_mult}),
|
walther@59871
|
536 |
Rule.Thm ("rroot_to_lhs_add_mult",ThmC.numerals_to_Free @{thm rroot_to_lhs_add_mult}),
|
walther@59871
|
537 |
Rule.Thm ("risolate_root_add",ThmC.numerals_to_Free @{thm risolate_root_add}),
|
walther@59871
|
538 |
Rule.Thm ("risolate_root_mult",ThmC.numerals_to_Free @{thm risolate_root_mult}),
|
walther@59871
|
539 |
Rule.Thm ("risolate_root_div",ThmC.numerals_to_Free @{thm risolate_root_div}) ],
|
wneuper@59416
|
540 |
scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy))
|
neuper@37954
|
541 |
"empty_script")
|
wneuper@59406
|
542 |
};
|
neuper@37954
|
543 |
|
neuper@37954
|
544 |
(*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
|
neuper@37954
|
545 |
val isolate_bdv =
|
walther@59857
|
546 |
Rule_Def.Repeat{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
|
walther@59852
|
547 |
erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
|
neuper@37954
|
548 |
rules =
|
walther@59871
|
549 |
[Rule.Thm ("risolate_bdv_add",ThmC.numerals_to_Free @{thm risolate_bdv_add}),
|
walther@59871
|
550 |
Rule.Thm ("risolate_bdv_mult_add",ThmC.numerals_to_Free @{thm risolate_bdv_mult_add}),
|
walther@59871
|
551 |
Rule.Thm ("risolate_bdv_mult",ThmC.numerals_to_Free @{thm risolate_bdv_mult}),
|
walther@59871
|
552 |
Rule.Thm ("mult_square",ThmC.numerals_to_Free @{thm mult_square}),
|
walther@59871
|
553 |
Rule.Thm ("constant_square",ThmC.numerals_to_Free @{thm constant_square}),
|
walther@59871
|
554 |
Rule.Thm ("constant_mult_square",ThmC.numerals_to_Free @{thm constant_mult_square})
|
neuper@37954
|
555 |
],
|
wneuper@59416
|
556 |
scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy))
|
neuper@37954
|
557 |
"empty_script")
|
wneuper@59406
|
558 |
};
|
wneuper@59472
|
559 |
\<close>
|
walther@59618
|
560 |
ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory};\<close>
|
wneuper@59472
|
561 |
setup \<open>KEStore_Elems.add_rlss
|
s1210629013@55444
|
562 |
[("Test_simplify", (Context.theory_name @{theory}, prep_rls' Test_simplify)),
|
s1210629013@55444
|
563 |
("tval_rls", (Context.theory_name @{theory}, prep_rls' tval_rls)),
|
s1210629013@55444
|
564 |
("isolate_root", (Context.theory_name @{theory}, prep_rls' isolate_root)),
|
s1210629013@55444
|
565 |
("isolate_bdv", (Context.theory_name @{theory}, prep_rls' isolate_bdv)),
|
s1210629013@55444
|
566 |
("matches", (Context.theory_name @{theory}, prep_rls'
|
walther@59878
|
567 |
(Rule_Set.append_rules "matches" testerls [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_")])))]
|
wneuper@59472
|
568 |
\<close>
|
neuper@37954
|
569 |
|
wneuper@59472
|
570 |
subsection \<open>problems\<close>
|
neuper@37954
|
571 |
(** problem types **)
|
wneuper@59472
|
572 |
setup \<open>KEStore_Elems.add_pbts
|
walther@59973
|
573 |
[(Problem.prep_input thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
|
walther@59973
|
574 |
(Problem.prep_input thy "pbl_test_equ" [] Problem.id_empty
|
walther@59997
|
575 |
(["equation", "test"],
|
walther@59997
|
576 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
s1210629013@55339
|
577 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
s1210629013@55339
|
578 |
("#Find" ,["solutions v_v'i'"])],
|
s1210629013@55339
|
579 |
assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
|
walther@59973
|
580 |
(Problem.prep_input thy "pbl_test_uni" [] Problem.id_empty
|
walther@59997
|
581 |
(["univariate", "equation", "test"],
|
walther@59997
|
582 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
s1210629013@55339
|
583 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
s1210629013@55339
|
584 |
("#Find" ,["solutions v_v'i'"])],
|
s1210629013@55339
|
585 |
assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
|
walther@59973
|
586 |
(Problem.prep_input thy "pbl_test_uni_lin" [] Problem.id_empty
|
walther@59997
|
587 |
(["LINEAR", "univariate", "equation", "test"],
|
walther@59997
|
588 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
s1210629013@55339
|
589 |
("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
|
s1210629013@55339
|
590 |
"(matches (?a+v_v = 0) e_e) | (matches (?a+?b*v_v = 0) e_e) "]),
|
s1210629013@55339
|
591 |
("#Find" ,["solutions v_v'i'"])],
|
s1210629013@55339
|
592 |
assoc_rls' @{theory} "matches",
|
walther@59997
|
593 |
SOME "solve (e_e::bool, v_v)", [["Test", "solve_linear"]]))]
|
wneuper@59472
|
594 |
\<close>
|
wneuper@59472
|
595 |
ML \<open>
|
walther@59857
|
596 |
Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
|
neuper@37954
|
597 |
[("termlessI", termlessI),
|
neuper@37954
|
598 |
("ord_make_polytest", ord_make_polytest false thy)
|
neuper@37954
|
599 |
]);
|
neuper@37954
|
600 |
|
neuper@37954
|
601 |
val make_polytest =
|
walther@59851
|
602 |
Rule_Def.Repeat{id = "make_polytest", preconds = []:term list,
|
neuper@52105
|
603 |
rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
|
walther@59851
|
604 |
erls = testerls, srls = Rule_Set.Empty,
|
walther@59603
|
605 |
calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
|
walther@59603
|
606 |
("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
|
walther@59603
|
607 |
("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
|
neuper@42451
|
608 |
], errpatts = [],
|
walther@59871
|
609 |
rules = [Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
|
neuper@37954
|
610 |
(*"a - b = a + (-1) * b"*)
|
walther@59871
|
611 |
Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
|
neuper@37954
|
612 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
walther@59871
|
613 |
Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
|
neuper@37954
|
614 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
walther@59871
|
615 |
Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
|
neuper@37954
|
616 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
walther@59871
|
617 |
Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
|
neuper@37954
|
618 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
walther@59871
|
619 |
Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
|
neuper@37954
|
620 |
(*"1 * z = z"*)
|
walther@59871
|
621 |
Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
|
neuper@37954
|
622 |
(*"0 * z = 0"*)
|
walther@59871
|
623 |
Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
|
neuper@37954
|
624 |
(*"0 + z = z"*)
|
neuper@37954
|
625 |
|
neuper@37954
|
626 |
(*AC-rewriting*)
|
walther@59877
|
627 |
Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
|
neuper@37954
|
628 |
(* z * w = w * z *)
|
walther@59871
|
629 |
Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
|
neuper@37954
|
630 |
(*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
|
walther@59877
|
631 |
Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
|
neuper@37954
|
632 |
(*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
|
walther@59877
|
633 |
Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
|
neuper@37954
|
634 |
(*z + w = w + z*)
|
walther@59877
|
635 |
Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
|
neuper@37954
|
636 |
(*x + (y + z) = y + (x + z)*)
|
walther@59877
|
637 |
Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
|
neuper@37954
|
638 |
(*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
|
neuper@37954
|
639 |
|
wneuper@59416
|
640 |
Rule.Thm ("sym_realpow_twoI",
|
walther@59871
|
641 |
ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
|
walther@60242
|
642 |
(*"r1 * r1 = r1 \<up> 2"*)
|
walther@59871
|
643 |
Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
|
walther@60242
|
644 |
(*"r * r \<up> n = r \<up> (n + 1)"*)
|
wneuper@59416
|
645 |
Rule.Thm ("sym_real_mult_2",
|
walther@59871
|
646 |
ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37954
|
647 |
(*"z1 + z1 = 2 * z1"*)
|
walther@59871
|
648 |
Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
|
neuper@37954
|
649 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37954
|
650 |
|
walther@59871
|
651 |
Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
|
neuper@37954
|
652 |
(*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
|
walther@59871
|
653 |
Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
|
neuper@37954
|
654 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37954
|
655 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
walther@59871
|
656 |
Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
|
neuper@37954
|
657 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
walther@59871
|
658 |
Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
|
neuper@37954
|
659 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37954
|
660 |
|
walther@59878
|
661 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
walther@59878
|
662 |
Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
|
walther@59878
|
663 |
Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
|
neuper@37954
|
664 |
],
|
walther@59878
|
665 |
scr = Rule.Empty_Prog(*Rule.Prog ((Thm.term_of o the o (parse thy))
|
neuper@37954
|
666 |
scr_make_polytest)*)
|
wneuper@59406
|
667 |
};
|
neuper@37954
|
668 |
|
neuper@37954
|
669 |
val expand_binomtest =
|
walther@59851
|
670 |
Rule_Def.Repeat{id = "expand_binomtest", preconds = [],
|
neuper@37954
|
671 |
rew_ord = ("termlessI",termlessI),
|
walther@59851
|
672 |
erls = testerls, srls = Rule_Set.Empty,
|
walther@59603
|
673 |
calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
|
walther@59603
|
674 |
("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
|
walther@59603
|
675 |
("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
|
neuper@42451
|
676 |
], errpatts = [],
|
neuper@38001
|
677 |
rules =
|
walther@59871
|
678 |
[Rule.Thm ("real_plus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
|
walther@60242
|
679 |
(*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
|
walther@59871
|
680 |
Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
|
neuper@37954
|
681 |
(*"(a + b)*(a + b) = ...*)
|
walther@59871
|
682 |
Rule.Thm ("real_minus_binom_pow2" ,ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
|
walther@60242
|
683 |
(*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
|
walther@59871
|
684 |
Rule.Thm ("real_minus_binom_times",ThmC.numerals_to_Free @{thm real_minus_binom_times}),
|
neuper@38001
|
685 |
(*"(a - b)*(a - b) = ...*)
|
walther@59871
|
686 |
Rule.Thm ("real_plus_minus_binom1",ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
|
walther@60242
|
687 |
(*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
|
walther@59871
|
688 |
Rule.Thm ("real_plus_minus_binom2",ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
|
walther@60242
|
689 |
(*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
|
neuper@38001
|
690 |
(*RL 020915*)
|
walther@59871
|
691 |
Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
|
neuper@38001
|
692 |
(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
walther@59871
|
693 |
Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
|
neuper@38001
|
694 |
(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
walther@59871
|
695 |
Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
|
neuper@38001
|
696 |
(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
|
walther@59871
|
697 |
Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
|
neuper@38001
|
698 |
(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
|
walther@59871
|
699 |
Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
|
walther@60242
|
700 |
(*(a*b) \<up> n = a \<up> n * b \<up> n*)
|
walther@59871
|
701 |
Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
|
walther@60242
|
702 |
(* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
|
walther@59871
|
703 |
Rule.Thm ("real_minus_binom_pow3",ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
|
walther@60242
|
704 |
(* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
|
neuper@37954
|
705 |
|
neuper@37954
|
706 |
|
walther@59871
|
707 |
(* Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
|
neuper@38001
|
708 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
walther@59871
|
709 |
Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
|
neuper@38001
|
710 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
walther@59871
|
711 |
Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
|
neuper@38001
|
712 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
walther@59871
|
713 |
Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
|
neuper@38001
|
714 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@38001
|
715 |
*)
|
neuper@38001
|
716 |
|
walther@59871
|
717 |
Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
|
neuper@38001
|
718 |
(*"1 * z = z"*)
|
walther@59871
|
719 |
Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
|
neuper@38001
|
720 |
(*"0 * z = 0"*)
|
walther@59871
|
721 |
Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
|
neuper@38001
|
722 |
(*"0 + z = z"*)
|
neuper@37954
|
723 |
|
walther@59878
|
724 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
walther@59878
|
725 |
Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
|
walther@59878
|
726 |
Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
|
neuper@38001
|
727 |
(*
|
walther@59877
|
728 |
Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
|
neuper@38001
|
729 |
(*AC-rewriting*)
|
walther@59871
|
730 |
Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
|
walther@59877
|
731 |
Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
|
walther@59877
|
732 |
Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
|
walther@59877
|
733 |
Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
|
walther@59877
|
734 |
Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
|
neuper@38001
|
735 |
*)
|
neuper@38001
|
736 |
|
wneuper@59416
|
737 |
Rule.Thm ("sym_realpow_twoI",
|
walther@59871
|
738 |
ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
|
walther@60242
|
739 |
(*"r1 * r1 = r1 \<up> 2"*)
|
walther@59871
|
740 |
Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
|
walther@60242
|
741 |
(*"r * r \<up> n = r \<up> (n + 1)"*)
|
wneuper@59416
|
742 |
(*Rule.Thm ("sym_real_mult_2",
|
walther@59871
|
743 |
ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
|
neuper@38001
|
744 |
(*"z1 + z1 = 2 * z1"*)*)
|
walther@59871
|
745 |
Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
|
neuper@38001
|
746 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37954
|
747 |
|
walther@59871
|
748 |
Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
|
neuper@38001
|
749 |
(*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
|
walther@59871
|
750 |
Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
|
neuper@38001
|
751 |
(*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
|
walther@59871
|
752 |
Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
|
neuper@38001
|
753 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
walther@59871
|
754 |
Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
|
neuper@38001
|
755 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37954
|
756 |
|
walther@59878
|
757 |
Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
|
walther@59878
|
758 |
Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
|
walther@59878
|
759 |
Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
|
neuper@38001
|
760 |
],
|
walther@59878
|
761 |
scr = Rule.Empty_Prog
|
wneuper@59585
|
762 |
(*Program ((Thm.term_of o the o (parse thy)) scr_expand_binomtest)*)
|
wneuper@59406
|
763 |
};
|
wneuper@59472
|
764 |
\<close>
|
wneuper@59472
|
765 |
setup \<open>KEStore_Elems.add_rlss
|
s1210629013@55444
|
766 |
[("make_polytest", (Context.theory_name @{theory}, prep_rls' make_polytest)),
|
wneuper@59472
|
767 |
("expand_binomtest", (Context.theory_name @{theory}, prep_rls' expand_binomtest))]\<close>
|
wneuper@59472
|
768 |
setup \<open>KEStore_Elems.add_rlss
|
wneuper@59430
|
769 |
[("norm_equation", (Context.theory_name @{theory}, prep_rls' norm_equation)),
|
wneuper@59430
|
770 |
("ac_plus_times", (Context.theory_name @{theory}, prep_rls' ac_plus_times)),
|
wneuper@59472
|
771 |
("rearrange_assoc", (Context.theory_name @{theory}, prep_rls' rearrange_assoc))]\<close>
|
wneuper@59430
|
772 |
|
wneuper@59472
|
773 |
section \<open>problems\<close>
|
wneuper@59472
|
774 |
setup \<open>KEStore_Elems.add_pbts
|
walther@59973
|
775 |
[(Problem.prep_input thy "pbl_test_uni_plain2" [] Problem.id_empty
|
walther@59997
|
776 |
(["plain_square", "univariate", "equation", "test"],
|
walther@59997
|
777 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
walther@60242
|
778 |
("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
|
walther@60242
|
779 |
"(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^
|
walther@60242
|
780 |
"(matches (?a + v_v \<up> 2 = 0) e_e) |" ^
|
walther@60242
|
781 |
"(matches ( v_v \<up> 2 = 0) e_e)"]),
|
wneuper@59430
|
782 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59430
|
783 |
assoc_rls' @{theory} "matches",
|
walther@59997
|
784 |
SOME "solve (e_e::bool, v_v)", [["Test", "solve_plain_square"]])),
|
walther@59973
|
785 |
(Problem.prep_input thy "pbl_test_uni_poly" [] Problem.id_empty
|
walther@59997
|
786 |
(["polynomial", "univariate", "equation", "test"],
|
walther@60242
|
787 |
[("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
|
wneuper@59430
|
788 |
("#Where" ,["HOL.False"]),
|
wneuper@59430
|
789 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59852
|
790 |
Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
|
walther@59973
|
791 |
(Problem.prep_input thy "pbl_test_uni_poly_deg2" [] Problem.id_empty
|
walther@59997
|
792 |
(["degree_two", "polynomial", "univariate", "equation", "test"],
|
walther@60242
|
793 |
[("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
|
wneuper@59430
|
794 |
("#Find" ,["solutions v_v'i'"])],
|
walther@60242
|
795 |
Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
|
walther@59973
|
796 |
(Problem.prep_input thy "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
|
walther@59997
|
797 |
(["pq_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
|
walther@60242
|
798 |
[("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
|
wneuper@59430
|
799 |
("#Find" ,["solutions v_v'i'"])],
|
walther@60242
|
800 |
Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
|
walther@59973
|
801 |
(Problem.prep_input thy "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
|
walther@59997
|
802 |
(["abc_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
|
walther@60242
|
803 |
[("#Given" ,["equality (a_a * x \<up> 2 + b_b * x + c_c = 0)", "solveFor v_v"]),
|
wneuper@59430
|
804 |
("#Find" ,["solutions v_v'i'"])],
|
walther@60242
|
805 |
Rule_Set.empty, SOME "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)", [])),
|
walther@59973
|
806 |
(Problem.prep_input thy "pbl_test_uni_root" [] Problem.id_empty
|
walther@59997
|
807 |
(["squareroot", "univariate", "equation", "test"],
|
walther@59997
|
808 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
809 |
("#Where" ,["precond_rootpbl v_v"]),
|
wneuper@59430
|
810 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59878
|
811 |
Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains'_root",
|
wneuper@59430
|
812 |
eval_contains_root "#contains_root_")],
|
walther@59997
|
813 |
SOME "solve (e_e::bool, v_v)", [["Test", "square_equation"]])),
|
walther@59973
|
814 |
(Problem.prep_input thy "pbl_test_uni_norm" [] Problem.id_empty
|
walther@59997
|
815 |
(["normalise", "univariate", "equation", "test"],
|
walther@59997
|
816 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
817 |
("#Where" ,[]),
|
wneuper@59430
|
818 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59997
|
819 |
Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test", "norm_univar_equation"]])),
|
walther@59973
|
820 |
(Problem.prep_input thy "pbl_test_uni_roottest" [] Problem.id_empty
|
walther@59997
|
821 |
(["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
822 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
823 |
("#Where" ,["precond_rootpbl v_v"]),
|
wneuper@59430
|
824 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59852
|
825 |
Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
|
walther@59973
|
826 |
(Problem.prep_input thy "pbl_test_intsimp" [] Problem.id_empty
|
walther@59997
|
827 |
(["inttype", "test"],
|
wneuper@59430
|
828 |
[("#Given" ,["intTestGiven t_t"]),
|
wneuper@59430
|
829 |
("#Where" ,[]),
|
wneuper@59430
|
830 |
("#Find" ,["intTestFind s_s"])],
|
walther@59997
|
831 |
Rule_Set.empty, NONE, [["Test", "intsimp"]]))]\<close>
|
wneuper@59430
|
832 |
|
wneuper@59472
|
833 |
section \<open>methods\<close>
|
wneuper@59472
|
834 |
subsection \<open>differentiate\<close>
|
wneuper@59472
|
835 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
836 |
[MethodC.prep_input @{theory "Diff"} "met_test" [] MethodC.id_empty
|
wneuper@59430
|
837 |
(["Test"], [],
|
walther@59852
|
838 |
{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
|
walther@59852
|
839 |
crls=Atools_erls, errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
|
wneuper@59473
|
840 |
\<close>
|
wneuper@59545
|
841 |
|
wneuper@59504
|
842 |
partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
wneuper@59504
|
843 |
where
|
walther@59635
|
844 |
"solve_linear e_e v_v = (
|
walther@59635
|
845 |
let e_e =
|
walther@59635
|
846 |
Repeat (
|
walther@59637
|
847 |
(Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #>
|
walther@59635
|
848 |
(Rewrite_Set ''Test_simplify'')) e_e
|
walther@59635
|
849 |
in
|
walther@59635
|
850 |
[e_e])"
|
wneuper@59473
|
851 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
852 |
[MethodC.prep_input thy "met_test_solvelin" [] MethodC.id_empty
|
walther@59997
|
853 |
(["Test", "solve_linear"],
|
walther@59997
|
854 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
855 |
("#Where" ,["matches (?a = ?b) e_e"]),
|
wneuper@59430
|
856 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59852
|
857 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
|
wneuper@59430
|
858 |
prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
|
wneuper@59430
|
859 |
nrls = Test_simplify},
|
wneuper@59551
|
860 |
@{thm solve_linear.simps})]
|
wneuper@59472
|
861 |
\<close>
|
wneuper@59472
|
862 |
subsection \<open>root equation\<close>
|
wneuper@59545
|
863 |
|
wneuper@59504
|
864 |
partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
wneuper@59504
|
865 |
where
|
walther@59635
|
866 |
"solve_root_equ e_e v_v = (
|
walther@59635
|
867 |
let
|
walther@59635
|
868 |
e_e = (
|
walther@59635
|
869 |
(While (contains_root e_e) Do (
|
walther@59637
|
870 |
(Rewrite ''square_equation_left'' ) #>
|
walther@59637
|
871 |
(Try (Rewrite_Set ''Test_simplify'' )) #>
|
walther@59637
|
872 |
(Try (Rewrite_Set ''rearrange_assoc'' )) #>
|
walther@59637
|
873 |
(Try (Rewrite_Set ''isolate_root'' )) #>
|
walther@59637
|
874 |
(Try (Rewrite_Set ''Test_simplify'' )))) #>
|
walther@59637
|
875 |
(Try (Rewrite_Set ''norm_equation'' )) #>
|
walther@59637
|
876 |
(Try (Rewrite_Set ''Test_simplify'' )) #>
|
walther@59637
|
877 |
(Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #>
|
walther@59635
|
878 |
(Try (Rewrite_Set ''Test_simplify'' ))
|
walther@59635
|
879 |
) e_e
|
walther@59635
|
880 |
in
|
walther@59635
|
881 |
[e_e])"
|
wneuper@59472
|
882 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
883 |
[MethodC.prep_input thy "met_test_sqrt" [] MethodC.id_empty
|
wneuper@59430
|
884 |
(*root-equation, version for tests before 8.01.01*)
|
walther@59997
|
885 |
(["Test", "sqrt-equ-test"],
|
walther@59997
|
886 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
887 |
("#Where" ,["contains_root (e_e::bool)"]),
|
wneuper@59430
|
888 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59430
|
889 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
walther@59852
|
890 |
srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
|
walther@59878
|
891 |
[Rule.Eval ("Test.contains'_root", eval_contains_root "")],
|
walther@59852
|
892 |
prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
|
walther@59878
|
893 |
[Rule.Eval ("Test.contains'_root", eval_contains_root "")],
|
walther@59852
|
894 |
calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
|
walther@59997
|
895 |
asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
|
wneuper@59551
|
896 |
@{thm solve_root_equ.simps})]
|
wneuper@59472
|
897 |
\<close>
|
wneuper@59477
|
898 |
|
walther@59635
|
899 |
partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
walther@59635
|
900 |
where
|
walther@59635
|
901 |
"minisubpbl e_e v_v = (
|
walther@59635
|
902 |
let
|
walther@59635
|
903 |
e_e = (
|
walther@59637
|
904 |
(Try (Rewrite_Set ''norm_equation'' )) #>
|
walther@59635
|
905 |
(Try (Rewrite_Set ''Test_simplify'' ))) e_e;
|
walther@59635
|
906 |
L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
|
walther@59635
|
907 |
[''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
|
walther@59635
|
908 |
in
|
walther@59635
|
909 |
Check_elementwise L_L {(v_v::real). Assumptions})"
|
wneuper@59472
|
910 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
911 |
[MethodC.prep_input thy "met_test_squ_sub" [] MethodC.id_empty
|
wneuper@59430
|
912 |
(*tests subproblem fixed linear*)
|
walther@59997
|
913 |
(["Test", "squ-equ-test-subpbl1"],
|
walther@59997
|
914 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
915 |
("#Where" ,["precond_rootmet v_v"]),
|
wneuper@59430
|
916 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59852
|
917 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
|
walther@59852
|
918 |
prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
|
walther@59878
|
919 |
[Rule.Eval ("Test.precond'_rootmet", eval_precond_rootmet "")],
|
wneuper@59430
|
920 |
calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
|
wneuper@59551
|
921 |
@{thm minisubpbl.simps})]
|
wneuper@59472
|
922 |
\<close>
|
wneuper@59545
|
923 |
|
wneuper@59504
|
924 |
partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
walther@59635
|
925 |
where
|
walther@59635
|
926 |
"solve_root_equ2 e_e v_v = (
|
walther@59635
|
927 |
let
|
walther@59635
|
928 |
e_e = (
|
walther@59635
|
929 |
(While (contains_root e_e) Do (
|
walther@59637
|
930 |
(Rewrite ''square_equation_left'' ) #>
|
walther@59637
|
931 |
(Try (Rewrite_Set ''Test_simplify'' )) #>
|
walther@59637
|
932 |
(Try (Rewrite_Set ''rearrange_assoc'' )) #>
|
walther@59637
|
933 |
(Try (Rewrite_Set ''isolate_root'' )) #>
|
walther@59637
|
934 |
(Try (Rewrite_Set ''Test_simplify'' )))) #>
|
walther@59637
|
935 |
(Try (Rewrite_Set ''norm_equation'' )) #>
|
walther@59635
|
936 |
(Try (Rewrite_Set ''Test_simplify'' ))
|
walther@59635
|
937 |
) e_e;
|
walther@59635
|
938 |
L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
|
wneuper@59504
|
939 |
[''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
|
walther@59635
|
940 |
in
|
walther@59635
|
941 |
Check_elementwise L_L {(v_v::real). Assumptions}) "
|
wneuper@59472
|
942 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
943 |
[MethodC.prep_input thy "met_test_eq1" [] MethodC.id_empty
|
wneuper@59430
|
944 |
(*root-equation1:*)
|
walther@59997
|
945 |
(["Test", "square_equation1"],
|
walther@59997
|
946 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
947 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59430
|
948 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
walther@59852
|
949 |
srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
|
walther@59878
|
950 |
[Rule.Eval ("Test.contains'_root", eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
|
walther@59997
|
951 |
errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),
|
walther@59997
|
952 |
("square_equation_right", "")]*)},
|
wneuper@59551
|
953 |
@{thm solve_root_equ2.simps})]
|
wneuper@59472
|
954 |
\<close>
|
wneuper@59545
|
955 |
|
wneuper@59504
|
956 |
partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
wneuper@59504
|
957 |
where
|
walther@59635
|
958 |
"solve_root_equ3 e_e v_v = (
|
walther@59635
|
959 |
let
|
walther@59635
|
960 |
e_e = (
|
walther@59635
|
961 |
(While (contains_root e_e) Do ((
|
walther@59635
|
962 |
(Rewrite ''square_equation_left'' ) Or
|
walther@59637
|
963 |
(Rewrite ''square_equation_right'' )) #>
|
walther@59637
|
964 |
(Try (Rewrite_Set ''Test_simplify'' )) #>
|
walther@59637
|
965 |
(Try (Rewrite_Set ''rearrange_assoc'' )) #>
|
walther@59637
|
966 |
(Try (Rewrite_Set ''isolate_root'' )) #>
|
walther@59637
|
967 |
(Try (Rewrite_Set ''Test_simplify'' )))) #>
|
walther@59637
|
968 |
(Try (Rewrite_Set ''norm_equation'' )) #>
|
walther@59635
|
969 |
(Try (Rewrite_Set ''Test_simplify'' ))
|
walther@59635
|
970 |
) e_e;
|
walther@59635
|
971 |
L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
|
walther@59635
|
972 |
[''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
|
walther@59635
|
973 |
in
|
walther@59635
|
974 |
Check_elementwise L_L {(v_v::real). Assumptions})"
|
wneuper@59472
|
975 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
976 |
[MethodC.prep_input thy "met_test_squ2" [] MethodC.id_empty
|
wneuper@59430
|
977 |
(*root-equation2*)
|
walther@59997
|
978 |
(["Test", "square_equation2"],
|
walther@59997
|
979 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
980 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59430
|
981 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
walther@59852
|
982 |
srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
|
walther@59878
|
983 |
[Rule.Eval ("Test.contains'_root", eval_contains_root"")],
|
walther@59852
|
984 |
prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
|
walther@59997
|
985 |
asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
|
wneuper@59551
|
986 |
@{thm solve_root_equ3.simps})]
|
wneuper@59472
|
987 |
\<close>
|
wneuper@59545
|
988 |
|
wneuper@59504
|
989 |
partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
wneuper@59504
|
990 |
where
|
walther@59635
|
991 |
"solve_root_equ4 e_e v_v = (
|
walther@59635
|
992 |
let
|
walther@59635
|
993 |
e_e = (
|
walther@59635
|
994 |
(While (contains_root e_e) Do ((
|
walther@59635
|
995 |
(Rewrite ''square_equation_left'' ) Or
|
walther@59637
|
996 |
(Rewrite ''square_equation_right'' )) #>
|
walther@59637
|
997 |
(Try (Rewrite_Set ''Test_simplify'' )) #>
|
walther@59637
|
998 |
(Try (Rewrite_Set ''rearrange_assoc'' )) #>
|
walther@59637
|
999 |
(Try (Rewrite_Set ''isolate_root'' )) #>
|
walther@59637
|
1000 |
(Try (Rewrite_Set ''Test_simplify'' )))) #>
|
walther@59637
|
1001 |
(Try (Rewrite_Set ''norm_equation'' )) #>
|
walther@59635
|
1002 |
(Try (Rewrite_Set ''Test_simplify'' ))
|
walther@59635
|
1003 |
) e_e;
|
walther@59635
|
1004 |
L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
|
walther@59635
|
1005 |
[''no_met'']) [BOOL e_e, REAL v_v]
|
walther@59635
|
1006 |
in
|
walther@59635
|
1007 |
Check_elementwise L_L {(v_v::real). Assumptions})"
|
wneuper@59472
|
1008 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
1009 |
[MethodC.prep_input thy "met_test_squeq" [] MethodC.id_empty
|
wneuper@59430
|
1010 |
(*root-equation*)
|
walther@59997
|
1011 |
(["Test", "square_equation"],
|
walther@59997
|
1012 |
[("#Given" ,["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
1013 |
("#Find" ,["solutions v_v'i'"])],
|
wneuper@59430
|
1014 |
{rew_ord'="e_rew_ord",rls'=tval_rls,
|
walther@59852
|
1015 |
srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
|
walther@59878
|
1016 |
[Rule.Eval ("Test.contains'_root", eval_contains_root"")],
|
walther@59852
|
1017 |
prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
|
walther@59997
|
1018 |
asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
|
wneuper@59551
|
1019 |
@{thm solve_root_equ4.simps})]
|
wneuper@59472
|
1020 |
\<close>
|
wneuper@59545
|
1021 |
|
wneuper@59504
|
1022 |
partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
wneuper@59504
|
1023 |
where
|
walther@59635
|
1024 |
"solve_plain_square e_e v_v = (
|
walther@59635
|
1025 |
let
|
walther@59635
|
1026 |
e_e = (
|
walther@59637
|
1027 |
(Try (Rewrite_Set ''isolate_bdv'' )) #>
|
walther@59637
|
1028 |
(Try (Rewrite_Set ''Test_simplify'' )) #>
|
walther@59635
|
1029 |
((Rewrite ''square_equality_0'' ) Or
|
walther@59637
|
1030 |
(Rewrite ''square_equality'' )) #>
|
walther@59635
|
1031 |
(Try (Rewrite_Set ''tval_rls'' ))) e_e
|
walther@59635
|
1032 |
in
|
walther@59635
|
1033 |
Or_to_List e_e)"
|
wneuper@59472
|
1034 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
1035 |
[MethodC.prep_input thy "met_test_eq_plain" [] MethodC.id_empty
|
wneuper@59430
|
1036 |
(*solve_plain_square*)
|
walther@59997
|
1037 |
(["Test", "solve_plain_square"],
|
walther@59997
|
1038 |
[("#Given",["equality e_e", "solveFor v_v"]),
|
walther@60242
|
1039 |
("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
|
walther@60242
|
1040 |
"(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^
|
walther@60242
|
1041 |
"(matches (?a + v_v \<up> 2 = 0) e_e) |" ^
|
walther@60242
|
1042 |
"(matches ( v_v \<up> 2 = 0) e_e)"]),
|
wneuper@59430
|
1043 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59852
|
1044 |
{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
|
walther@59852
|
1045 |
prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
|
wneuper@59430
|
1046 |
asm_rls=[],asm_thm=[]*)},
|
wneuper@59551
|
1047 |
@{thm solve_plain_square.simps})]
|
wneuper@59472
|
1048 |
\<close>
|
wneuper@59472
|
1049 |
subsection \<open>polynomial equation\<close>
|
wneuper@59545
|
1050 |
|
wneuper@59504
|
1051 |
partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
|
wneuper@59504
|
1052 |
where
|
walther@59635
|
1053 |
"norm_univariate_equ e_e v_v = (
|
walther@59635
|
1054 |
let
|
walther@59635
|
1055 |
e_e = (
|
walther@59637
|
1056 |
(Try (Rewrite ''rnorm_equation_add'' )) #>
|
walther@59635
|
1057 |
(Try (Rewrite_Set ''Test_simplify'' )) ) e_e
|
walther@59635
|
1058 |
in
|
walther@59635
|
1059 |
SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
|
wneuper@59504
|
1060 |
[''no_met'']) [BOOL e_e, REAL v_v])"
|
wneuper@59472
|
1061 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
1062 |
[MethodC.prep_input thy "met_test_norm_univ" [] MethodC.id_empty
|
walther@59997
|
1063 |
(["Test", "norm_univar_equation"],
|
walther@59997
|
1064 |
[("#Given",["equality e_e", "solveFor v_v"]),
|
wneuper@59430
|
1065 |
("#Where" ,[]),
|
wneuper@59430
|
1066 |
("#Find" ,["solutions v_v'i'"])],
|
walther@59852
|
1067 |
{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
|
walther@59852
|
1068 |
errpats = [], nrls = Rule_Set.empty},
|
wneuper@59551
|
1069 |
@{thm norm_univariate_equ.simps})]
|
wneuper@59472
|
1070 |
\<close>
|
wneuper@59472
|
1071 |
subsection \<open>diophantine equation\<close>
|
wneuper@59545
|
1072 |
|
wneuper@59504
|
1073 |
partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
|
wneuper@59504
|
1074 |
where
|
walther@59635
|
1075 |
"test_simplify t_t = (
|
walther@59635
|
1076 |
Repeat (
|
walther@59637
|
1077 |
(Try (Calculate ''PLUS'')) #>
|
walther@59635
|
1078 |
(Try (Calculate ''TIMES''))) t_t)"
|
wneuper@59472
|
1079 |
setup \<open>KEStore_Elems.add_mets
|
walther@60154
|
1080 |
[MethodC.prep_input thy "met_test_intsimp" [] MethodC.id_empty
|
walther@59997
|
1081 |
(["Test", "intsimp"],
|
wneuper@59430
|
1082 |
[("#Given" ,["intTestGiven t_t"]),
|
wneuper@59430
|
1083 |
("#Where" ,[]),
|
wneuper@59430
|
1084 |
("#Find" ,["intTestFind s_s"])],
|
walther@59852
|
1085 |
{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
|
wneuper@59430
|
1086 |
crls = tval_rls, errpats = [], nrls = Test_simplify},
|
wneuper@59551
|
1087 |
@{thm test_simplify.simps})]
|
wneuper@59472
|
1088 |
\<close>
|
wneuper@59430
|
1089 |
|
neuper@37906
|
1090 |
end
|