66 SOME ((term2str p) ^ " = True", |
66 SOME ((term2str p) ^ " = True", |
67 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
67 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
68 else SOME ((term2str p) ^ " = True", |
68 else SOME ((term2str p) ^ " = True", |
69 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
69 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
70 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); |
70 | eval_is_rootRatAddTerm_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); |
71 |
71 *} |
|
72 ML {* |
72 (*-------------------------rulse-------------------------*) |
73 (*-------------------------rulse-------------------------*) |
73 val RootRatEq_prls = |
74 val RootRatEq_prls = |
74 append_rls "RootRatEq_prls" e_rls |
75 append_rls "RootRatEq_prls" e_rls |
75 [Calc ("Atools.ident",eval_ident "#ident_"), |
76 [Calc ("Atools.ident",eval_ident "#ident_"), |
76 Calc ("Tools.matches",eval_matches ""), |
77 Calc ("Tools.matches",eval_matches ""), |
103 []))); |
104 []))); |
104 |
105 |
105 ruleset' := overwritelthy @{theory} (!ruleset', |
106 ruleset' := overwritelthy @{theory} (!ruleset', |
106 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]); |
107 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]); |
107 |
108 |
|
109 *} |
|
110 ML {* |
108 (* Solves a rootrat Equation *) |
111 (* Solves a rootrat Equation *) |
109 val rootrat_solve = prep_rls( |
112 val rootrat_solve = prep_rls( |
110 Rls {id = "rootrat_solve", preconds = [], |
113 Rls {id = "rootrat_solve", preconds = [], |
111 rew_ord = ("termlessI",termlessI), |
114 rew_ord = ("termlessI",termlessI), |
112 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
115 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
113 rules = [Thm("rootrat_equation_left_1", num_str @{thm }rootrat_equation_left_1), |
116 rules = |
|
117 [Thm("rootrat_equation_left_1", num_str @{thm rootrat_equation_left_1}), |
114 (* [|c is_rootTerm_in bdv|] ==> |
118 (* [|c is_rootTerm_in bdv|] ==> |
115 ( (a + b/c = d) = ( b = (d - a) * c )) *) |
119 ( (a + b/c = d) = ( b = (d - a) * c )) *) |
116 Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}), |
120 Thm("rootrat_equation_left_2",num_str @{thm rootrat_equation_left_2}), |
117 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) |
121 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) |
118 Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}), |
122 Thm("rootrat_equation_right_1",num_str @{thm rootrat_equation_right_1}), |
119 (* [|f is_rootTerm_in bdv|] ==> |
123 (* [|f is_rootTerm_in bdv|] ==> |
120 ( (a = d + e/f) = ( (a - d) * f = e )) *) |
124 ( (a = d + e/f) = ( (a - d) * f = e )) *) |
121 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2}) |
125 Thm("rootrat_equation_right_2",num_str @{thm rootrat_equation_right_2}) |
122 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*) |
126 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*) |
123 ], |
127 ], scr = Script ((term_of o the o (parse thy)) "empty_script")}:rls); |
124 scr = Script ((term_of o the o (parse thy)) "empty_script") |
128 |
125 }:rls); |
|
126 ruleset' := overwritelthy @{theory} (!ruleset', |
129 ruleset' := overwritelthy @{theory} (!ruleset', |
127 [("rootrat_solve",rootrat_solve) |
130 [("rootrat_solve",rootrat_solve) |
128 ]); |
131 ]); |
|
132 *} |
|
133 ML {* |
129 |
134 |
130 (*-----------------------probleme------------------------*) |
135 (*-----------------------probleme------------------------*) |
131 (* |
136 (* |
132 (get_pbt ["rat","root'","univariate","equation"]); |
137 (get_pbt ["rat","root'","univariate","equation"]); |
133 show_ptyps(); |
138 show_ptyps(); |
141 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
146 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
142 ("#Find" ,["solutions v_i"]) |
147 ("#Find" ,["solutions v_i"]) |
143 ], |
148 ], |
144 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
149 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
145 [["RootRatEq","elim_rootrat_equation"]])); |
150 [["RootRatEq","elim_rootrat_equation"]])); |
146 |
151 *} |
|
152 ML {* |
147 (*-------------------------Methode-----------------------*) |
153 (*-------------------------Methode-----------------------*) |
148 store_met |
154 store_met |
149 (prep_met (theory "LinEq") "met_rootrateq" [] e_metID |
155 (prep_met (theory "LinEq") "met_rootrateq" [] e_metID |
150 (["RootRatEq"], |
156 (["RootRatEq"], |
151 [], |
157 [], |
171 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^ |
177 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^ |
172 "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^ |
178 "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^ |
173 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
179 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
174 " (Try (Rewrite_Set make_rooteq False)) @@ " ^ |
180 " (Try (Rewrite_Set make_rooteq False)) @@ " ^ |
175 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
181 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
176 " (Try (Rewrite_Set_Inst [(bdv,v_)] " ^ |
182 " (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^ |
177 " rootrat_solve False))) e_e " ^ |
183 " rootrat_solve False))) e_e " ^ |
178 " in (SubProblem (RootEq',[univariate,equation], " ^ |
184 " in (SubProblem (RootEq',[univariate,equation], " ^ |
179 " [no_met]) [BOOL e_e, REAL v_]))" |
185 " [no_met]) [BOOL e_e, REAL v_v]))" |
180 )); |
186 )); |
181 calclist':= overwritel (!calclist', |
187 calclist':= overwritel (!calclist', |
182 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", |
188 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", |
183 eval_is_rootRatAddTerm_in"")) |
189 eval_is_rootRatAddTerm_in"")) |
184 ]); |
190 ]); |