1 (* collecting all knowledge for Root and Rational Equations
7 (c) by Richard Lang, 2003
10 theory RootRatEq imports RootEq RatEq RootRat begin
14 is'_rootRatAddTerm'_in :: "[real, real] => bool"
15 ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
17 (*---------scripts--------------------------*)
18 Elim'_rootrat'_equation
20 bool list] => bool list"
21 ("((Script Elim'_rootrat'_equation (_ _ =))//
23 (*-------------------- rules------------------------------------------------*)
26 (* eliminate ratRootTerm *)
27 rootrat_equation_left_1
28 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))"
29 rootrat_equation_left_2
30 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))"
31 rootrat_equation_right_2
32 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))"
33 rootrat_equation_right_1
34 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
39 (*-------------------------functions---------------------*)
40 (* true if denominator contains (sq)root in + or - term
41 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
42 if false then (term)^2 contains no (sq)root *)
43 fun is_rootRatAddTerm_in t v =
45 fun coeff_in c v = member op = (vars c) v;
46 fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v =
47 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
48 | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v =
49 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
50 | rootadd _ _ = false;
51 fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:")
52 (* at the moment there is no term like this, but ....*)
53 | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v =
54 if (is_rootTerm_in t3 v) then rootadd t3 v else false
55 | findrootrat (_ $ t1 $ t2) v =
56 (findrootrat t1 v) orelse (findrootrat t2 v)
57 | findrootrat (_ $ t1) v = (findrootrat t1 v)
58 | findrootrat _ _ = false;
63 fun eval_is_rootRatAddTerm_in _ _
64 (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ =
65 if is_rootRatAddTerm_in t v then
66 SOME ((term2str p) ^ " = True",
67 Trueprop $ (mk_equality (p, HOLogic.true_const)))
68 else SOME ((term2str p) ^ " = True",
69 Trueprop $ (mk_equality (p, HOLogic.false_const)))
70 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE);
72 (*-------------------------rulse-------------------------*)
74 append_rls "RootRatEq_prls" e_rls
75 [Calc ("Atools.ident",eval_ident "#ident_"),
76 Calc ("Tools.matches",eval_matches ""),
77 Calc ("Tools.lhs" ,eval_lhs ""),
78 Calc ("Tools.rhs" ,eval_rhs ""),
79 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
80 Calc ("RootRatEq.is'_rootRatAddTerm'_in",
81 eval_is_rootRatAddTerm_in ""),
82 Calc ("op =",eval_equal "#equal_"),
83 Thm ("not_true",num_str @{thm not_true}),
84 Thm ("not_false",num_str @{thm not_false}),
85 Thm ("and_true",num_str @{thm and_true}),
86 Thm ("and_false",num_str @{thm and_false}),
87 Thm ("or_true",num_str @{thm or_true}),
88 Thm ("or_false",num_str @{thm or_false})
92 merge_rls "RooRatEq_erls" rootrat_erls
93 (merge_rls "" RootEq_erls
94 (merge_rls "" rateq_erls
99 merge_rls "RootRatEq_crls" rootrat_erls
100 (merge_rls "" RootEq_erls
101 (merge_rls "" rateq_erls
105 ruleset' := overwritelthy @{theory} (!ruleset',
106 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]);
108 (* Solves a rootrat Equation *)
109 val rootrat_solve = prep_rls(
110 Rls {id = "rootrat_solve", preconds = [],
111 rew_ord = ("termlessI",termlessI),
112 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
113 rules = [Thm("rootrat_equation_left_1", num_str @{thm }rootrat_equation_left_1),
114 (* [|c is_rootTerm_in bdv|] ==>
115 ( (a + b/c = d) = ( b = (d - a) * c )) *)
116 Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
117 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
118 Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
119 (* [|f is_rootTerm_in bdv|] ==>
120 ( (a = d + e/f) = ( (a - d) * f = e )) *)
121 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
122 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
124 scr = Script ((term_of o the o (parse thy)) "empty_script")
126 ruleset' := overwritelthy @{theory} (!ruleset',
127 [("rootrat_solve",rootrat_solve)
130 (*-----------------------probleme------------------------*)
132 (get_pbt ["rat","root","univariate","equation"]);
137 (prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
138 (["rat","sq","root","univariate","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_"])
144 RootRatEq_prls, SOME "solve (e_::bool, v_)",
145 [["RootRatEq","elim_rootrat_equation"]]));
147 (*-------------------------Methode-----------------------*)
149 (prep_met (theory "LinEq") "met_rootrateq" [] e_metID
152 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
153 crls=Atools_erls, nrls=norm_Rational}, "empty_script"));
154 (*-- left 20.10.02 --*)
156 (prep_met thy "met_rootrateq_elim" [] e_metID
157 (["RootRatEq","elim_rootrat_equation"],
158 [("#Given" ,["equality e_","solveFor v_"]),
159 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | " ^
160 "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]),
161 ("#Find" ,["solutions v_i_"])
163 {rew_ord'="termlessI",
168 crls=RootRatEq_crls, nrls=norm_Rational(*,
171 "Script Elim_rootrat_equation (e_::bool) (v_::real) = " ^
172 "(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
173 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
174 " (Try (Rewrite_Set make_rooteq False)) @@ " ^
175 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
176 " (Try (Rewrite_Set_Inst [(bdv,v_)] " ^
177 " rootrat_solve False))) e_ " ^
178 " in (SubProblem (RootEq_,[univariate,equation], " ^
179 " [no_met]) [bool_ e_, real_ v_]))"
181 calclist':= overwritel (!calclist',
182 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",
183 eval_is_rootRatAddTerm_in""))