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