25 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true |
25 1/(sqrt(x+3)*(x+4)) -> false; 1/(sqrt(x)+2) -> true |
26 if false then (term)^2 contains no (sq)root *) |
26 if false then (term)^2 contains no (sq)root *) |
27 fun is_rootRatAddTerm_in t v = |
27 fun is_rootRatAddTerm_in t v = |
28 let |
28 let |
29 fun coeff_in c v = member op = (vars c) v; |
29 fun coeff_in c v = member op = (vars c) v; |
30 fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse |
30 fun rootadd (t as (Const ("op +",_) $ t2 $ t3)) v = |
31 (is_rootTerm_in t3 v) |
31 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v) |
32 | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = (is_rootTerm_in t2 v) orelse |
32 | rootadd (t as (Const ("op -",_) $ t2 $ t3)) v = |
33 (is_rootTerm_in t3 v) |
33 (is_rootTerm_in t2 v) orelse (is_rootTerm_in t3 v) |
34 | rootadd _ _ = false; |
34 | rootadd _ _ = false; |
35 fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:") |
35 fun findrootrat (_ $ _ $ _ $ _) v = raise error("is_rootRatAddTerm_in:") |
36 (* at the moment there is no term like this, but ....*) |
36 (* at the moment there is no term like this, but ....*) |
37 | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = |
37 | findrootrat (t as (Const ("HOL.divide",_) $ _ $ t3)) v = |
38 if (is_rootTerm_in t3 v) then rootadd t3 v else false |
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) |
39 | findrootrat (_ $ t1 $ t2) v = |
|
40 (findrootrat t1 v) orelse (findrootrat t2 v) |
40 | findrootrat (_ $ t1) v = (findrootrat t1 v) |
41 | findrootrat (_ $ t1) v = (findrootrat t1 v) |
41 | findrootrat _ _ = false; |
42 | findrootrat _ _ = false; |
42 in |
43 in |
43 findrootrat t v |
44 findrootrat t v |
44 end; |
45 end; |
45 |
46 |
46 fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ = |
47 fun eval_is_rootRatAddTerm_in _ _ |
|
48 (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ = |
47 if is_rootRatAddTerm_in t v then |
49 if is_rootRatAddTerm_in t v then |
48 SOME ((term2str p) ^ " = True", |
50 SOME ((term2str p) ^ " = True", |
49 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
51 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
50 else SOME ((term2str p) ^ " = True", |
52 else SOME ((term2str p) ^ " = True", |
51 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
53 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
57 [Calc ("Atools.ident",eval_ident "#ident_"), |
59 [Calc ("Atools.ident",eval_ident "#ident_"), |
58 Calc ("Tools.matches",eval_matches ""), |
60 Calc ("Tools.matches",eval_matches ""), |
59 Calc ("Tools.lhs" ,eval_lhs ""), |
61 Calc ("Tools.lhs" ,eval_lhs ""), |
60 Calc ("Tools.rhs" ,eval_rhs ""), |
62 Calc ("Tools.rhs" ,eval_rhs ""), |
61 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), |
63 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""), |
62 Calc ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""), |
64 Calc ("RootRatEq.is'_rootRatAddTerm'_in", |
|
65 eval_is_rootRatAddTerm_in ""), |
63 Calc ("op =",eval_equal "#equal_"), |
66 Calc ("op =",eval_equal "#equal_"), |
64 Thm ("not_true",num_str not_true), |
67 Thm ("not_true",num_str not_true), |
65 Thm ("not_false",num_str not_false), |
68 Thm ("not_false",num_str not_false), |
66 Thm ("and_true",num_str and_true), |
69 Thm ("and_true",num_str and_true), |
67 Thm ("and_false",num_str and_false), |
70 Thm ("and_false",num_str and_false), |
68 Thm ("or_true",num_str or_true), |
71 Thm ("or_true",num_str or_true), |
69 Thm ("or_false",num_str or_false) |
72 Thm ("or_false",num_str or_false) |
70 ]; |
73 ]; |
71 |
|
72 |
74 |
73 val RooRatEq_erls = |
75 val RooRatEq_erls = |
74 merge_rls "RooRatEq_erls" rootrat_erls |
76 merge_rls "RooRatEq_erls" rootrat_erls |
75 (merge_rls "" RootEq_erls |
77 (merge_rls "" RootEq_erls |
76 (merge_rls "" rateq_erls |
78 (merge_rls "" rateq_erls |
83 (merge_rls "" rateq_erls |
85 (merge_rls "" rateq_erls |
84 (append_rls "" e_rls |
86 (append_rls "" e_rls |
85 []))); |
87 []))); |
86 |
88 |
87 ruleset' := overwritelthy thy (!ruleset', |
89 ruleset' := overwritelthy thy (!ruleset', |
88 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*) |
90 [("RooRatEq_erls",RooRatEq_erls) (*FIXXXME:del with rls.rls'*)]); |
89 ]); |
|
90 |
91 |
91 (* Solves a rootrat Equation *) |
92 (* Solves a rootrat Equation *) |
92 val rootrat_solve = prep_rls( |
93 val rootrat_solve = prep_rls( |
93 Rls {id = "rootrat_solve", preconds = [], |
94 Rls {id = "rootrat_solve", preconds = [], |
94 rew_ord = ("termlessI",termlessI), |
95 rew_ord = ("termlessI",termlessI), |
95 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
96 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*) |
96 rules = [ Thm("rootrat_equation_left_1",num_str rootrat_equation_left_1), |
97 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 (* [|c is_rootTerm_in bdv|] ==> |
98 Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2), |
99 ( (a + b/c = d) = ( b = (d - a) * c )) *) |
|
100 Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2), |
99 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) |
101 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *) |
100 Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1), |
102 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 )) *) |
103 (* [|f is_rootTerm_in bdv|] ==> |
102 Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2) |
104 ( (a = d + e/f) = ( (a - d) * f = e )) *) |
103 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e )) *) |
105 Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2) |
|
106 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*) |
104 ], |
107 ], |
105 scr = Script ((term_of o the o (parse thy)) "empty_script") |
108 scr = Script ((term_of o the o (parse thy)) "empty_script") |
106 }:rls); |
109 }:rls); |
107 ruleset' := overwritelthy thy (!ruleset', |
110 ruleset' := overwritelthy thy (!ruleset', |
108 [("rootrat_solve",rootrat_solve) |
111 [("rootrat_solve",rootrat_solve) |
115 *) |
118 *) |
116 store_pbt |
119 store_pbt |
117 (prep_pbt RootRatEq.thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
120 (prep_pbt RootRatEq.thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
118 (["rat","sq","root","univariate","equation"], |
121 (["rat","sq","root","univariate","equation"], |
119 [("#Given" ,["equality e_","solveFor v_"]), |
122 [("#Given" ,["equality e_","solveFor v_"]), |
120 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| \ |
123 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) )| " ^ |
121 \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]), |
124 "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]), |
122 ("#Find" ,["solutions v_i_"]) |
125 ("#Find" ,["solutions v_i_"]) |
123 ], |
126 ], |
124 RootRatEq_prls, SOME "solve (e_::bool, v_)", |
127 RootRatEq_prls, SOME "solve (e_::bool, v_)", |
125 [["RootRatEq","elim_rootrat_equation"]])); |
128 [["RootRatEq","elim_rootrat_equation"]])); |
126 |
129 |
128 store_met |
131 store_met |
129 (prep_met LinEq.thy "met_rootrateq" [] e_metID |
132 (prep_met LinEq.thy "met_rootrateq" [] e_metID |
130 (["RootRatEq"], |
133 (["RootRatEq"], |
131 [], |
134 [], |
132 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
135 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
133 crls=Atools_erls, nrls=norm_Rational(*, |
136 crls=Atools_erls, nrls=norm_Rational}, "empty_script")); |
134 asm_rls=[],asm_thm=[]*)}, "empty_script")); |
|
135 (*-- left 20.10.02 --*) |
137 (*-- left 20.10.02 --*) |
136 store_met |
138 store_met |
137 (prep_met RootRatEq.thy "met_rootrateq_elim" [] e_metID |
139 (prep_met RootRatEq.thy "met_rootrateq_elim" [] e_metID |
138 (["RootRatEq","elim_rootrat_equation"], |
140 (["RootRatEq","elim_rootrat_equation"], |
139 [("#Given" ,["equality e_","solveFor v_"]), |
141 [("#Given" ,["equality e_","solveFor v_"]), |
140 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | \ |
142 ("#Where" ,["( (lhs e_) is_rootRatAddTerm_in (v_::real) ) | " ^ |
141 \( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]), |
143 "( (rhs e_) is_rootRatAddTerm_in (v_::real) )"]), |
142 ("#Find" ,["solutions v_i_"]) |
144 ("#Find" ,["solutions v_i_"]) |
143 ], |
145 ], |
144 {rew_ord'="termlessI", |
146 {rew_ord'="termlessI", |
145 rls'=RooRatEq_erls, |
147 rls'=RooRatEq_erls, |
146 srls=e_rls, |
148 srls=e_rls, |
147 prls=RootRatEq_prls, |
149 prls=RootRatEq_prls, |
148 calc=[], |
150 calc=[], |
149 crls=RootRatEq_crls, nrls=norm_Rational(*, |
151 crls=RootRatEq_crls, nrls=norm_Rational(*, |
150 asm_rls=[], |
152 asm_rls=[], |
151 asm_thm=[]*)}, |
153 asm_thm=[]*)}, |
152 "Script Elim_rootrat_equation (e_::bool) (v_::real) = \ |
154 "Script Elim_rootrat_equation (e_::bool) (v_::real) = " ^ |
153 \(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@ \ |
155 "(let e_ = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^ |
154 \ (Try (Rewrite_Set rooteq_simplify False)) @@ \ |
156 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
155 \ (Try (Rewrite_Set make_rooteq False)) @@ \ |
157 " (Try (Rewrite_Set make_rooteq False)) @@ " ^ |
156 \ (Try (Rewrite_Set rooteq_simplify False)) @@ \ |
158 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^ |
157 \ (Try (Rewrite_Set_Inst [(bdv,v_)] \ |
159 " (Try (Rewrite_Set_Inst [(bdv,v_)] " ^ |
158 \ rootrat_solve False))) e_ \ |
160 " rootrat_solve False))) e_ " ^ |
159 \ in (SubProblem (RootEq_,[univariate,equation], \ |
161 " in (SubProblem (RootEq_,[univariate,equation], " ^ |
160 \ [no_met]) [bool_ e_, real_ v_]))" |
162 " [no_met]) [bool_ e_, real_ v_]))" |
161 )); |
163 )); |
162 calclist':= overwritel (!calclist', |
164 calclist':= overwritel (!calclist', |
163 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", |
165 [("is_rootRatAddTerm_in", ("RootRatEq.is_rootRatAddTerm_in", |
164 eval_is_rootRatAddTerm_in"")) |
166 eval_is_rootRatAddTerm_in"")) |
165 ]);(*("", ("", "")),*) |
167 ]); |
166 "******* RootRatEq.ML end *******"; |
|