neuper@37906
|
1 |
(* collecting all knowledge for Root and Rational Equations
|
neuper@37906
|
2 |
created by: rlang
|
neuper@37906
|
3 |
date: 02.10
|
neuper@37906
|
4 |
changed by: rlang
|
neuper@37906
|
5 |
last change by: rlang
|
neuper@37906
|
6 |
date: 02.11.04
|
neuper@37954
|
7 |
(c) by Richard Lang, 2003
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37954
|
10 |
theory RootRatEq imports RootEq RatEq RootRat begin
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
consts
|
neuper@37906
|
13 |
|
neuper@37954
|
14 |
is'_rootRatAddTerm'_in :: "[real, real] => bool"
|
neuper@37954
|
15 |
("_ is'_rootRatAddTerm'_in _") (*RL DA*)
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
(*---------scripts--------------------------*)
|
neuper@37906
|
18 |
Elim'_rootrat'_equation
|
neuper@37954
|
19 |
:: "[bool,real,
|
neuper@37954
|
20 |
bool list] => bool list"
|
neuper@37954
|
21 |
("((Script Elim'_rootrat'_equation (_ _ =))//
|
neuper@37954
|
22 |
(_))" 9)
|
neuper@37906
|
23 |
(*-------------------- rules------------------------------------------------*)
|
neuper@37906
|
24 |
|
neuper@37954
|
25 |
axioms
|
neuper@37906
|
26 |
(* eliminate ratRootTerm *)
|
neuper@37983
|
27 |
rootrat_equation_left_1:
|
neuper@37906
|
28 |
"[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
|
neuper@37983
|
29 |
rootrat_equation_left_2:
|
neuper@37906
|
30 |
"[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
|
neuper@37983
|
31 |
rootrat_equation_right_2:
|
neuper@37906
|
32 |
"[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
|
neuper@37983
|
33 |
rootrat_equation_right_1:
|
neuper@37906
|
34 |
"[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
|
neuper@37906
|
35 |
|
neuper@37954
|
36 |
ML {*
|
neuper@37972
|
37 |
val thy = @{theory};
|
neuper@37972
|
38 |
|
neuper@37954
|
39 |
(*-------------------------functions---------------------*)
|
neuper@37954
|
40 |
(* true if denominator contains (sq)root in + or - term
|
neuper@37954
|
41 |
1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
|
neuper@37954
|
42 |
if false then (term)^2 contains no (sq)root *)
|
neuper@37954
|
43 |
fun is_rootRatAddTerm_in t v =
|
neuper@37954
|
44 |
let
|
neuper@37954
|
45 |
fun coeff_in c v = member op = (vars c) v;
|
neuper@37954
|
46 |
fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v =
|
neuper@37954
|
47 |
(is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
|
neuper@37954
|
48 |
| rootadd (t as (Const ("op -",_) $ t2 $ t3)) v =
|
neuper@37954
|
49 |
(is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
|
neuper@37954
|
50 |
| rootadd _ _ = false;
|
neuper@37954
|
51 |
fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
|
neuper@37954
|
52 |
(* at the moment there is no term like this, but ....*)
|
neuper@37954
|
53 |
| findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v =
|
neuper@37954
|
54 |
if (is_rootTerm_in t3 v) then rootadd t3 v else false
|
neuper@37954
|
55 |
| findrootrat (_ $ t1 $ t2) v =
|
neuper@37954
|
56 |
(findrootrat t1 v) orelse (findrootrat t2 v)
|
neuper@37954
|
57 |
| findrootrat (_ $ t1) v = (findrootrat t1 v)
|
neuper@37954
|
58 |
| findrootrat _ _ = false;
|
neuper@37954
|
59 |
in
|
neuper@37954
|
60 |
findrootrat t v
|
neuper@37954
|
61 |
end;
|
neuper@37906
|
62 |
|
neuper@37954
|
63 |
fun eval_is_rootRatAddTerm_in _ _
|
neuper@37954
|
64 |
(p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ =
|
neuper@37954
|
65 |
if is_rootRatAddTerm_in t v then
|
neuper@37954
|
66 |
SOME ((term2str p) ^ " = True",
|
neuper@37954
|
67 |
Trueprop $ (mk_equality (p, HOLogic.true_const)))
|
neuper@37954
|
68 |
else SOME ((term2str p) ^ " = True",
|
neuper@37954
|
69 |
Trueprop $ (mk_equality (p, HOLogic.false_const)))
|
neuper@37954
|
70 |
| eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
|
neuper@37989
|
71 |
*}
|
neuper@37989
|
72 |
ML {*
|
neuper@37954
|
73 |
(*-------------------------rulse-------------------------*)
|
neuper@37954
|
74 |
val RootRatEq_prls =
|
neuper@37954
|
75 |
append_rls "RootRatEq_prls" e_rls
|
neuper@37954
|
76 |
[Calc ("Atools.ident",eval_ident "#ident_"),
|
neuper@37954
|
77 |
Calc ("Tools.matches",eval_matches ""),
|
neuper@37954
|
78 |
Calc ("Tools.lhs" ,eval_lhs ""),
|
neuper@37954
|
79 |
Calc ("Tools.rhs" ,eval_rhs ""),
|
neuper@37954
|
80 |
Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
|
neuper@37954
|
81 |
Calc ("RootRatEq.is'_rootRatAddTerm'_in",
|
neuper@37954
|
82 |
eval_is_rootRatAddTerm_in ""),
|
neuper@37954
|
83 |
Calc ("op =",eval_equal "#equal_"),
|
neuper@37969
|
84 |
Thm ("not_true",num_str @{thm not_true}),
|
neuper@37969
|
85 |
Thm ("not_false",num_str @{thm not_false}),
|
neuper@37969
|
86 |
Thm ("and_true",num_str @{thm and_true}),
|
neuper@37969
|
87 |
Thm ("and_false",num_str @{thm and_false}),
|
neuper@37969
|
88 |
Thm ("or_true",num_str @{thm or_true}),
|
neuper@37969
|
89 |
Thm ("or_false",num_str @{thm or_false})
|
neuper@37954
|
90 |
];
|
neuper@37954
|
91 |
|
neuper@37954
|
92 |
val RooRatEq_erls =
|
neuper@37954
|
93 |
merge_rls "RooRatEq_erls" rootrat_erls
|
neuper@37954
|
94 |
(merge_rls "" RootEq_erls
|
neuper@37954
|
95 |
(merge_rls "" rateq_erls
|
neuper@37954
|
96 |
(append_rls "" e_rls
|
neuper@37954
|
97 |
[])));
|
neuper@37954
|
98 |
|
neuper@37954
|
99 |
val RootRatEq_crls =
|
neuper@37954
|
100 |
merge_rls "RootRatEq_crls" rootrat_erls
|
neuper@37954
|
101 |
(merge_rls "" RootEq_erls
|
neuper@37954
|
102 |
(merge_rls "" rateq_erls
|
neuper@37954
|
103 |
(append_rls "" e_rls
|
neuper@37954
|
104 |
[])));
|
neuper@37954
|
105 |
|
neuper@37967
|
106 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
107 |
[("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
|
neuper@37954
|
108 |
|
neuper@37989
|
109 |
*}
|
neuper@37989
|
110 |
ML {*
|
neuper@37954
|
111 |
(* Solves a rootrat Equation *)
|
neuper@37954
|
112 |
val rootrat_solve = prep_rls(
|
neuper@37954
|
113 |
Rls {id = "rootrat_solve", preconds = [],
|
neuper@37954
|
114 |
rew_ord = ("termlessI",termlessI),
|
neuper@37954
|
115 |
erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
|
neuper@37989
|
116 |
rules =
|
neuper@37989
|
117 |
[Thm("rootrat_equation_left_1", num_str @{thm rootrat_equation_left_1}),
|
neuper@37954
|
118 |
(* [|c is_rootTerm_in bdv|] ==>
|
neuper@37954
|
119 |
( (a + b/c = d) = ( b = (d - a) * c )) *)
|
neuper@37989
|
120 |
Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
|
neuper@37954
|
121 |
(* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
|
neuper@37989
|
122 |
Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
|
neuper@37954
|
123 |
(* [|f is_rootTerm_in bdv|] ==>
|
neuper@37954
|
124 |
( (a = d + e/f) = ( (a - d) * f = e )) *)
|
neuper@37989
|
125 |
Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
|
neuper@37954
|
126 |
(* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
|
neuper@37989
|
127 |
], scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls);
|
neuper@37989
|
128 |
|
neuper@37967
|
129 |
ruleset' := overwritelthy @{theory} (!ruleset',
|
neuper@37954
|
130 |
[("rootrat_solve",rootrat_solve)
|
neuper@37954
|
131 |
]);
|
neuper@37989
|
132 |
*}
|
neuper@37989
|
133 |
ML {*
|
neuper@37954
|
134 |
|
neuper@37954
|
135 |
(*-----------------------probleme------------------------*)
|
neuper@37954
|
136 |
(*
|
neuper@37986
|
137 |
(get_pbt ["rat","root'","univariate","equation"]);
|
neuper@37954
|
138 |
show_ptyps();
|
neuper@37954
|
139 |
*)
|
neuper@37972
|
140 |
|
neuper@37954
|
141 |
store_pbt
|
neuper@37972
|
142 |
(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
|
neuper@37986
|
143 |
(["rat","sq","root'","univariate","equation"],
|
neuper@37981
|
144 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37982
|
145 |
("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
|
neuper@37982
|
146 |
"( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
|
neuper@38009
|
147 |
("#Find" ,["solutions v_i'''"])
|
neuper@37954
|
148 |
],
|
neuper@37981
|
149 |
RootRatEq_prls, SOME "solve (e_e::bool, v_v)",
|
neuper@37954
|
150 |
[["RootRatEq","elim_rootrat_equation"]]));
|
neuper@37989
|
151 |
*}
|
neuper@37989
|
152 |
ML {*
|
neuper@37954
|
153 |
(*-------------------------Methode-----------------------*)
|
neuper@37954
|
154 |
store_met
|
neuper@37954
|
155 |
(prep_met (theory "LinEq") "met_rootrateq" [] e_metID
|
neuper@37954
|
156 |
(["RootRatEq"],
|
neuper@37954
|
157 |
[],
|
neuper@37954
|
158 |
{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
|
neuper@37954
|
159 |
crls=Atools_erls, nrls=norm_Rational}, "empty_script"));
|
neuper@37954
|
160 |
(*-- left 20.10.02 --*)
|
neuper@37954
|
161 |
store_met
|
neuper@37972
|
162 |
(prep_met thy "met_rootrateq_elim" [] e_metID
|
neuper@37954
|
163 |
(["RootRatEq","elim_rootrat_equation"],
|
neuper@37981
|
164 |
[("#Given" ,["equality e_e","solveFor v_v"]),
|
neuper@37982
|
165 |
("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
|
neuper@37982
|
166 |
"( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
|
neuper@38009
|
167 |
("#Find" ,["solutions v_i'''"])
|
neuper@37954
|
168 |
],
|
neuper@37954
|
169 |
{rew_ord'="termlessI",
|
neuper@37954
|
170 |
rls'=RooRatEq_erls,
|
neuper@37954
|
171 |
srls=e_rls,
|
neuper@37954
|
172 |
prls=RootRatEq_prls,
|
neuper@37954
|
173 |
calc=[],
|
neuper@37954
|
174 |
crls=RootRatEq_crls, nrls=norm_Rational(*,
|
neuper@37954
|
175 |
asm_rls=[],
|
neuper@37954
|
176 |
asm_thm=[]*)},
|
neuper@37982
|
177 |
"Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
|
neuper@37981
|
178 |
"(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
|
neuper@37954
|
179 |
" (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
|
neuper@37954
|
180 |
" (Try (Rewrite_Set make_rooteq False)) @@ " ^
|
neuper@37954
|
181 |
" (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
|
neuper@37989
|
182 |
" (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^
|
neuper@37981
|
183 |
" rootrat_solve False))) e_e " ^
|
neuper@37987
|
184 |
" in (SubProblem (RootEq',[univariate,equation], " ^
|
neuper@37989
|
185 |
" [no_met]) [BOOL e_e, REAL v_v]))"
|
neuper@37954
|
186 |
));
|
neuper@37954
|
187 |
calclist':= overwritel (!calclist',
|
neuper@37954
|
188 |
[("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",
|
neuper@37954
|
189 |
eval_is_rootRatAddTerm_in""))
|
neuper@37954
|
190 |
]);
|
neuper@37954
|
191 |
*}
|
neuper@37906
|
192 |
|
neuper@37906
|
193 |
end
|