1 (* collecting all knowledge for Root and Rational Equations
7 (c) by Richard Lang, 2003
10 theory RootRatEq imports LinEq RootEq RatEq RootRat begin
12 text {* univariate equations over rational terms containing real square roots:
13 In 2003 this type has been developed as part of ISAC's equation solver
14 by Richard Lang in 2003.
15 The migration Isabelle2002 --> 2011 dropped this type of equation, see RootEq.thy.
20 is'_rootRatAddTerm'_in :: "[real, real] => bool"
21 ("_ is'_rootRatAddTerm'_in _") (*RL DA*)
23 (*---------scripts--------------------------*)
24 Elim'_rootrat'_equation
26 bool list] => bool list"
27 ("((Script Elim'_rootrat'_equation (_ _ =))//
29 (*-------------------- rules------------------------------------------------*)
32 (* eliminate ratRootTerm *)
33 rootrat_equation_left_1:
34 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" and
35 rootrat_equation_left_2:
36 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" and
37 rootrat_equation_right_2:
38 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" and
39 rootrat_equation_right_1:
40 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
45 (*-------------------------functions---------------------*)
46 (* true if denominator contains (sq)root in + or - term
47 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
48 if false then (term)^2 contains no (sq)root *)
49 fun is_rootRatAddTerm_in t v =
51 fun coeff_in c v = member op = (vars c) v;
52 fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v =
53 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
54 | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v =
55 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
56 | rootadd _ _ = false;
57 fun findrootrat (_ $ _ $ _ $ _) v = error("is_rootRatAddTerm_in:")
58 (* at the moment there is no term like this, but ....*)
59 | findrootrat (t as (Const ("Fields.inverse_class.divide",_) $ _ $ t3)) v =
60 if (is_rootTerm_in t3 v) then rootadd t3 v else false
61 | findrootrat (_ $ t1 $ t2) v =
62 (findrootrat t1 v) orelse (findrootrat t2 v)
63 | findrootrat (_ $ t1) v = (findrootrat t1 v)
64 | findrootrat _ _ = false;
69 fun eval_is_rootRatAddTerm_in _ _
70 (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ =
71 if is_rootRatAddTerm_in t v then
72 SOME ((term2str p) ^ " = True",
73 Trueprop $ (mk_equality (p, @{term True})))
74 else SOME ((term2str p) ^ " = True",
75 Trueprop $ (mk_equality (p, @{term False})))
76 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
79 (*-------------------------rulse-------------------------*)
81 append_rls "RootRatEq_prls" e_rls
82 [Calc ("Atools.ident",eval_ident "#ident_"),
83 Calc ("Tools.matches",eval_matches ""),
84 Calc ("Tools.lhs" ,eval_lhs ""),
85 Calc ("Tools.rhs" ,eval_rhs ""),
86 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
87 Calc ("RootRatEq.is'_rootRatAddTerm'_in",
88 eval_is_rootRatAddTerm_in ""),
89 Calc ("HOL.eq",eval_equal "#equal_"),
90 Thm ("not_true",num_str @{thm not_true}),
91 Thm ("not_false",num_str @{thm not_false}),
92 Thm ("and_true",num_str @{thm and_true}),
93 Thm ("and_false",num_str @{thm and_false}),
94 Thm ("or_true",num_str @{thm or_true}),
95 Thm ("or_false",num_str @{thm or_false})
99 merge_rls "RooRatEq_erls" rootrat_erls
100 (merge_rls "" RootEq_erls
101 (merge_rls "" rateq_erls
106 merge_rls "RootRatEq_crls" rootrat_erls
107 (merge_rls "" RootEq_erls
108 (merge_rls "" rateq_erls
112 setup {* KEStore_Elems.add_rlss
113 [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))] *}
115 (* Solves a rootrat Equation *)
116 val rootrat_solve = prep_rls'(
117 Rls {id = "rootrat_solve", preconds = [],
118 rew_ord = ("termlessI",termlessI),
119 erls = e_rls, srls = Erls, calc = [], errpatts = [],
121 [Thm("rootrat_equation_left_1", num_str @{thm rootrat_equation_left_1}),
122 (* [|c is_rootTerm_in bdv|] ==>
123 ( (a + b/c = d) = ( b = (d - a) * c )) *)
124 Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}),
125 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
126 Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}),
127 (* [|f is_rootTerm_in bdv|] ==>
128 ( (a = d + e/f) = ( (a - d) * f = e )) *)
129 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2})
130 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
131 ], scr = Prog ((Thm.term_of o the o (parse thy)) "empty_script")}:rls);
133 setup {* KEStore_Elems.add_rlss
134 [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))] *}
136 (*-----------------------probleme------------------------*)
138 (get_pbt ["rat","root'","univariate","equation"]);
142 setup {* KEStore_Elems.add_pbts
143 [(Specify.prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID
144 (["rat","sq","root'","univariate","equation"],
145 [("#Given" ,["equality e_e","solveFor v_v"]),
146 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
147 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
148 ("#Find" ,["solutions v_v'i'"])],
149 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]]))] *}
151 (*-------------------------Methode-----------------------*)
152 setup {* KEStore_Elems.add_mets
153 [Specify.prep_met @{theory LinEq} "met_rootrateq" [] e_metID
155 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
156 crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script"),
157 (*-- left 20.10.02 --*)
158 Specify.prep_met thy "met_rootrateq_elim" [] e_metID
159 (["RootRatEq","elim_rootrat_equation"],
160 [("#Given" ,["equality e_e","solveFor v_v"]),
161 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
162 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
163 ("#Find" ,["solutions v_v'i'"])],
164 {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=e_rls, prls=RootRatEq_prls, calc=[],
165 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
166 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
167 "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
168 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
169 " (Try (Rewrite_Set make_rooteq False)) @@ " ^
170 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
171 " (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^
172 " rootrat_solve False))) e_e " ^
173 " in (SubProblem (RootEq',[univariate,equation], " ^
174 " [no_met]) [BOOL e_e, REAL v_v]))")]
177 setup {* KEStore_Elems.add_calcs
178 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))] *}