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 \<open>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 (_ _ =))// (_))" 9)
28 (*-------------------- rules------------------------------------------------*)
31 (* eliminate ratRootTerm *)
32 rootrat_equation_left_1:
33 "[|c is_rootTerm_in bdv|] ==> ( (a + b/c = d) = ( b = (d - a) * c ))" and
34 rootrat_equation_left_2:
35 "[|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c ))" and
36 rootrat_equation_right_2:
37 "[|f is_rootTerm_in bdv|] ==> ( (a = d + e/f) = ( (a - d) * f = e ))" and
38 rootrat_equation_right_1:
39 "[|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))"
44 (*-------------------------functions---------------------*)
45 (* true if denominator contains (sq)root in + or - term
46 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true
47 if false then (term)^2 contains no (sq)root *)
48 fun is_rootRatAddTerm_in t v =
50 fun coeff_in c v = member op = (TermC.vars c) v;
51 fun rootadd (t as (Const ("Groups.plus_class.plus",_) $ t2 $ t3)) v =
52 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
53 | rootadd (t as (Const ("Groups.minus_class.minus",_) $ t2 $ t3)) v =
54 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v)
55 | rootadd _ _ = false;
56 fun findrootrat (_ $ _ $ _ $ _) v = error("is_rootRatAddTerm_in:")
57 (* at the moment there is no term like this, but ....*)
58 | findrootrat (t as (Const ("Rings.divide_class.divide",_) $ _ $ t3)) v =
59 if (is_rootTerm_in t3 v) then rootadd t3 v else false
60 | findrootrat (_ $ t1 $ t2) v =
61 (findrootrat t1 v) orelse (findrootrat t2 v)
62 | findrootrat (_ $ t1) v = (findrootrat t1 v)
63 | findrootrat _ _ = false;
68 fun eval_is_rootRatAddTerm_in _ _
69 (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ =
70 if is_rootRatAddTerm_in t v then
71 SOME ((Rule.term2str p) ^ " = True",
72 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
73 else SOME ((Rule.term2str p) ^ " = True",
74 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
75 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
78 (*-------------------------rulse-------------------------*)
80 Rule.append_rls "RootRatEq_prls" Rule.e_rls
81 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
82 Rule.Calc ("Tools.matches", Tools.eval_matches ""),
83 Rule.Calc ("Tools.lhs" , Tools.eval_lhs ""),
84 Rule.Calc ("Tools.rhs" , Tools.eval_rhs ""),
85 Rule.Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
86 Rule.Calc ("RootRatEq.is'_rootRatAddTerm'_in",
87 eval_is_rootRatAddTerm_in ""),
88 Rule.Calc ("HOL.eq",eval_equal "#equal_"),
89 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
90 Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
91 Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
92 Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
93 Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
94 Rule.Thm ("or_false",TermC.num_str @{thm or_false})
98 Rule.merge_rls "RooRatEq_erls" rootrat_erls
99 (Rule.merge_rls "" RootEq_erls
100 (Rule.merge_rls "" rateq_erls
101 (Rule.append_rls "" Rule.e_rls
105 Rule.merge_rls "RootRatEq_crls" rootrat_erls
106 (Rule.merge_rls "" RootEq_erls
107 (Rule.merge_rls "" rateq_erls
108 (Rule.append_rls "" Rule.e_rls
111 setup \<open>KEStore_Elems.add_rlss
112 [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls))]\<close>
114 (* Solves a rootrat Equation *)
115 val rootrat_solve = prep_rls'(
116 Rule.Rls {id = "rootrat_solve", preconds = [],
117 rew_ord = ("termlessI",termlessI),
118 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
120 [Rule.Thm("rootrat_equation_left_1", TermC.num_str @{thm rootrat_equation_left_1}),
121 (* [|c is_rootTerm_in bdv|] ==>
122 ( (a + b/c = d) = ( b = (d - a) * c )) *)
123 Rule.Thm("rootrat_equation_left_2",TermC.num_str @{thm rootrat_equation_left_2}),
124 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
125 Rule.Thm("rootrat_equation_right_1",TermC.num_str @{thm rootrat_equation_right_1}),
126 (* [|f is_rootTerm_in bdv|] ==>
127 ( (a = d + e/f) = ( (a - d) * f = e )) *)
128 Rule.Thm("rootrat_equation_right_2",TermC.num_str @{thm rootrat_equation_right_2})
129 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
130 ], scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
132 setup \<open>KEStore_Elems.add_rlss
133 [("rootrat_solve", (Context.theory_name @{theory}, rootrat_solve))]\<close>
135 (*-----------------------probleme------------------------*)
137 (get_pbt ["rat","rootX","univariate","equation"]);
141 setup \<open>KEStore_Elems.add_pbts
142 [(Specify.prep_pbt thy "pbl_equ_univ_root_sq_rat" [] Celem.e_pblID
143 (["rat","sq","rootX","univariate","equation"],
144 [("#Given" ,["equality e_e","solveFor v_v"]),
145 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
146 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
147 ("#Find" ,["solutions v_v'i'"])],
148 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq","elim_rootrat_equation"]]))]\<close>
150 (*-------------------------Methode-----------------------*)
151 setup \<open>KEStore_Elems.add_mets
152 [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Celem.e_metID
154 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
155 crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script")]
157 (*-- left 20.10.02 --*)
158 setup \<open>KEStore_Elems.add_mets
159 [Specify.prep_met thy "met_rootrateq_elim" [] Celem.e_metID
160 (["RootRatEq","elim_rootrat_equation"],
161 [("#Given" ,["equality e_e","solveFor v_v"]),
162 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
163 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
164 ("#Find" ,["solutions v_v'i'"])],
165 {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule.e_rls, prls=RootRatEq_prls, calc=[],
166 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
167 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
168 "(let e_e = ((Try (Rewrite_Set ''expand_rootbinoms'' False)) @@ " ^
169 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
170 " (Try (Rewrite_Set ''make_rooteq'' False)) @@ " ^
171 " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
172 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] " ^
173 " ''rootrat_solve'' False))) e_e " ^
174 " in (SubProblem (''RootEq'',[''univariate'',''equation''], " ^
175 " [no_met]) [BOOL e_e, REAL v_v]))")]
178 setup \<open>KEStore_Elems.add_calcs
179 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in""))]\<close>