Test_Isac works again, perfectly ..
# the same tests works as in 8df4b6196660 (the *child* of "Test_Isac works...")
# ..EXCEPT those marked with "exception Div raised"
# for general state of tests see Test_Isac section {* history of tests *}.
1 (*.(c) by Richard Lang, 2003 .*)
2 (* theory collecting all knowledge for RationalEquations
10 theory RatEq imports Rational begin
12 text {* univariate equations over multivariate rational terms:
13 In 2003 this type has been integrated into ISAC's equation solver
14 by Richard Lang; the root for the solver is Equation.thy.
15 The migration Isabelle2002 --> 2011 found that application of theorems like
16 rat_mult_denominator_right: "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
17 in rule-sets does not transfer "d ~= 0" to the assumptions; see
18 test --- repair NO asms from rls RatEq_eliminate ---.
19 Thus the migration dropped update of Check_elementwise, which would require
20 these assumptions; see
21 test --- pbl: rational, univariate, equation ---, --- x / (x ^ 2 - 6 * x + 9) - 1 /...
26 is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
28 (*----------------------scripts-----------------------*)
31 bool list] => bool list"
32 ("((Script Solve'_rat'_equation (_ _ =))//
35 axioms(*axiomatization where*)
36 (* FIXME also in Poly.thy def. --> FIXED*)
38 "a - b = a + (-1) * b"*)
39 real_rat_mult_1: "a*(b/c) = (a*b)/c" (*and*)
40 real_rat_mult_2: "(a/b)*(c/d) = (a*c)/(b*d)" (*and*)
41 real_rat_mult_3: "(a/b)*c = (a*c)/b" (*and*)
42 real_rat_pow: "(a/b)^^^2 = a^^^2/b^^^2" (*and*)
44 rat_double_rat_1: "[|Not(c=0); Not(d=0)|] ==> (a / (c/d) = (a*d) / c)" (*and*)
45 rat_double_rat_2: "[|Not(b=0);Not(c=0); Not(d=0)|] ==>
46 ((a/b) / (c/d) = (a*d) / (b*c))" (*and*)
47 rat_double_rat_3: "[|Not(b=0);Not(c=0)|] ==> ((a/b) / c = a / (b*c))" (*and*)
49 (* equation to same denominator *)
50 rat_mult_denominator_both:
51 "[|Not(b=0); Not(d=0)|] ==> ((a::real) / b = c / d) = (a*d = c*b)" (*and*)
52 rat_mult_denominator_left:
53 "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" (*and*)
54 rat_mult_denominator_right:
55 "[|Not(b=0)|] ==> ((a::real) / b = c) = (a = c*b)"
60 (*-------------------------functions-----------------------*)
61 (* is_rateqation_in becomes true, if a bdv is in the denominator of a fraction*)
62 fun is_rateqation_in t v =
64 fun coeff_in c v = member op = (vars c) v;
65 fun finddivide (_ $ _ $ _ $ _) v = error("is_rateqation_in:")
66 (* at the moment there is no term like this, but ....*)
67 | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v = coeff_in b v
68 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v)
69 orelse (finddivide t2 v)
70 | finddivide (_ $ t1) v = (finddivide t1 v)
71 | finddivide _ _ = false;
76 fun eval_is_ratequation_in _ _
77 (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
78 if is_rateqation_in t v then
79 SOME ((term2str p) ^ " = True",
80 Trueprop $ (mk_equality (p, @{term True})))
81 else SOME ((term2str p) ^ " = True",
82 Trueprop $ (mk_equality (p, @{term False})))
83 | eval_is_ratequation_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
85 (*-------------------------rulse-----------------------*)
86 val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
87 append_rls "RatEq_prls" e_rls
88 [Calc ("Atools.ident",eval_ident "#ident_"),
89 Calc ("Tools.matches",eval_matches ""),
90 Calc ("Tools.lhs" ,eval_lhs ""),
91 Calc ("Tools.rhs" ,eval_rhs ""),
92 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
93 Calc ("HOL.eq",eval_equal "#equal_"),
94 Thm ("not_true",num_str @{thm not_true}),
95 Thm ("not_false",num_str @{thm not_false}),
96 Thm ("and_true",num_str @{thm and_true}),
97 Thm ("and_false",num_str @{thm and_false}),
98 Thm ("or_true",num_str @{thm or_true}),
99 Thm ("or_false",num_str @{thm or_false})
103 (*rls = merge_rls erls Poly_erls *)
105 remove_rls "rateq_erls" (*WN: ein Hack*)
106 (merge_rls "is_ratequation_in" calculate_Rational
107 (append_rls "is_ratequation_in"
109 [(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
110 Calc ("RatEq.is'_ratequation'_in",
111 eval_is_ratequation_in "")
114 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)
115 Thm ("or_commute",num_str @{thm or_commute}) (*WN: ein Hack*)
117 ruleset' := overwritelthy @{theory} (!ruleset',
118 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
123 remove_rls "RatEq_crls" (*WN: ein Hack*)
124 (merge_rls "is_ratequation_in" calculate_Rational
125 (append_rls "is_ratequation_in"
127 [(*Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),*)
128 Calc ("RatEq.is'_ratequation'_in",
129 eval_is_ratequation_in "")
131 [Thm ("and_commute",num_str @{thm and_commute}), (*WN: ein Hack*)
132 Thm ("or_commute",num_str @{thm or_commute}) (*WN: ein Hack*)
135 val RatEq_eliminate = prep_rls(
136 Rls {id = "RatEq_eliminate", preconds = [],
137 rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls,
138 calc = [], errpatts = [],
140 Thm("rat_mult_denominator_both",num_str @{thm rat_mult_denominator_both}),
141 (* a/b=c/d -> ad=cb *)
142 Thm("rat_mult_denominator_left",num_str @{thm rat_mult_denominator_left}),
144 Thm("rat_mult_denominator_right",num_str @{thm rat_mult_denominator_right})
147 scr = Prog ((term_of o the o (parse thy)) "empty_script")
149 ruleset' := overwritelthy @{theory} (!ruleset',
150 [("RatEq_eliminate",RatEq_eliminate)
153 val RatEq_simplify = prep_rls(
154 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
155 erls = rateq_erls, srls = Erls, calc = [], errpatts = [],
157 Thm("real_rat_mult_1",num_str @{thm real_rat_mult_1}),
158 (*a*(b/c) = (a*b)/c*)
159 Thm("real_rat_mult_2",num_str @{thm real_rat_mult_2}),
160 (*(a/b)*(c/d) = (a*c)/(b*d)*)
161 Thm("real_rat_mult_3",num_str @{thm real_rat_mult_3}),
162 (* (a/b)*c = (a*c)/b*)
163 Thm("real_rat_pow",num_str @{thm real_rat_pow}),
164 (*(a/b)^^^2 = a^^^2/b^^^2*)
165 Thm("real_diff_minus",num_str @{thm real_diff_minus}),
166 (* a - b = a + (-1) * b *)
167 Thm("rat_double_rat_1",num_str @{thm rat_double_rat_1}),
168 (* (a / (c/d) = (a*d) / c) *)
169 Thm("rat_double_rat_2",num_str @{thm rat_double_rat_2}),
170 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
171 Thm("rat_double_rat_3",num_str @{thm rat_double_rat_3})
172 (* ((a/b) / c = a / (b*c) ) *)
174 scr = Prog ((term_of o the o (parse thy)) "empty_script")
176 ruleset' := overwritelthy @{theory} (!ruleset',
177 [("RatEq_simplify",RatEq_simplify)
180 (*-------------------------Problem-----------------------*)
182 (get_pbt ["rational","univariate","equation"]);
186 (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID
187 (["rational","univariate","equation"],
188 [("#Given" ,["equality e_e","solveFor v_v"]),
189 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
190 ("#Find" ,["solutions v_v'i'"])
193 RatEq_prls, SOME "solve (e_e::bool, v_v)",
194 [["RatEq","solve_rat_equation"]]));
198 (*-------------------------methods-----------------------*)
200 (prep_met thy "met_rateq" [] e_metID
203 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
204 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));
209 (prep_met thy "met_rat_eq" [] e_metID
210 (["RatEq", "solve_rat_equation"],
211 [("#Given" ,["equality e_e","solveFor v_v"]),
212 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
213 ("#Find" ,["solutions v_v'i'"])
215 {rew_ord'="termlessI",
220 crls=RatEq_crls, errpats = [], nrls = norm_Rational},
221 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
222 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^
223 " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^
224 " (Repeat(Try (Rewrite_Set add_fractions_p False))) @@ " ^
225 " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^
226 " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
227 " [BOOL e_e, REAL v_v]) " ^
228 " in Check_elementwise L_L {(v_v::real). Assumptions})"
233 calclist':= overwritel (!calclist',
234 [("is_ratequation_in", ("RatEq.is_ratequation_in",
235 eval_is_ratequation_in ""))