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