1 (*.(c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for Root and Rational Equations
10 (* use"knowledge/RootRatEq.ML";
16 remove_thy"RootRatEq";
20 "******* RootRatEq.ML begin *******";
21 theory' := overwritel (!theory', [("RootRatEq.thy",RootRatEq.thy)]);
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 =
29 fun coeff_in c v = v mem (vars c);
30 fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse
32 | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse
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;
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);
54 (*-------------------------rulse-------------------------*)
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)
74 merge_rls "RooRatEq_erls" rootrat_erls
75 (merge_rls "" RootEq_erls
76 (merge_rls "" rateq_erls
81 merge_rls "RootRatEq_crls" rootrat_erls
82 (merge_rls "" RootEq_erls
83 (merge_rls "" rateq_erls
87 ruleset' := overwritelthy thy (!ruleset',
88 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)
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 )) *)
105 scr = Script ((term_of o the o (parse thy)) "empty_script")
107 ruleset' := overwritelthy thy (!ruleset',
108 [("rootrat_solve",rootrat_solve)
111 (*-----------------------probleme------------------------*)
113 (get_pbt ["rat","root","univariate","equation"]);
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_"])
124 RootRatEq_prls, SOME "solve (e_::bool, v_)",
125 [["RootRatEq","elim_rootrat_equation"]]));
127 (*-------------------------Methode-----------------------*)
129 (prep_met LinEq.thy "met_rootrateq" [] e_metID
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 --*)
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_"])
144 {rew_ord'="termlessI",
149 crls=RootRatEq_crls, nrls=norm_Rational(*,
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_]))"
162 calclist':= overwritel (!calclist',
163 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in",
164 eval_is_rootRatAddTerm_in""))
165 ]);(*("", ("", "")),*)
166 "******* RootRatEq.ML end *******";