1 (*. (c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for LinearEquations
11 use_thy"Knowledge/Isac";
13 use_thy"Knowledge/LinEq";
19 "******* LinEq.ML begin *******";
21 (*-------------------- theory -------------------------------------------------*)
22 theory' := overwritel (!theory', [("LinEq.thy",LinEq.thy)]);
24 (*-------------- rules -------------------------------------------------------*)
25 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
26 append_rls "LinEq_prls" e_rls
27 [Calc ("op =",eval_equal "#equal_"),
28 Calc ("Tools.matches",eval_matches ""),
29 Calc ("Tools.lhs" ,eval_lhs ""),
30 Calc ("Tools.rhs" ,eval_rhs ""),
31 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
32 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
33 Calc ("Atools.occurs'_in",eval_occurs_in ""),
34 Calc ("Atools.ident",eval_ident "#ident_"),
35 Thm ("not_true",num_str not_true),
36 Thm ("not_false",num_str not_false),
37 Thm ("and_true",num_str and_true),
38 Thm ("and_false",num_str and_false),
39 Thm ("or_true",num_str or_true),
40 Thm ("or_false",num_str or_false)
42 (* ----- erls ----- *)
44 append_rls "LinEq_crls" poly_crls
45 [Thm ("real_assoc_1",num_str real_assoc_1)
48 Calc ("HOL.divide", eval_cancel "#divide_"),
49 Calc ("Atools.pow" ,eval_binop "#power_"),
53 (* ----- crls ----- *)
55 append_rls "LinEq_erls" Poly_erls
56 [Thm ("real_assoc_1",num_str real_assoc_1)
59 Calc ("HOL.divide", eval_cancel "#divide_"),
60 Calc ("Atools.pow" ,eval_binop "#power_"),
64 ruleset' := overwritelthy thy (!ruleset',
65 [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
68 val LinPoly_simplify = prep_rls(
69 Rls {id = "LinPoly_simplify", preconds = [],
70 rew_ord = ("termlessI",termlessI),
76 Thm ("real_assoc_1",num_str real_assoc_1),
77 Calc ("op +",eval_binop "#add_"),
78 Calc ("op -",eval_binop "#sub_"),
79 Calc ("op *",eval_binop "#mult_"),
81 Calc ("HOL.divide", eval_cancel "#divide_"),
82 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
84 Calc ("Atools.pow" ,eval_binop "#power_")
86 scr = Script ((term_of o the o (parse thy)) "empty_script")
88 ruleset' := overwritelthy thy (!ruleset',
89 [("LinPoly_simplify",LinPoly_simplify)]);
91 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
92 val LinEq_simplify = prep_rls(
93 Rls {id = "LinEq_simplify", preconds = [],
94 rew_ord = ("e_rew_ord",e_rew_ord),
98 (*asm_thm = [("lin_isolate_div","")],*)
100 Thm("lin_isolate_add1",num_str lin_isolate_add1),
101 (* a+bx=0 -> bx=-a *)
102 Thm("lin_isolate_add2",num_str lin_isolate_add2),
104 Thm("lin_isolate_div",num_str lin_isolate_div)
107 scr = Script ((term_of o the o (parse thy)) "empty_script")
109 ruleset' := overwritelthy thy (!ruleset',
110 [("LinEq_simplify",LinEq_simplify)]);
112 (*----------------------------- problem types --------------------------------*)
115 (get_pbt ["linear","univariate","equation"]);
117 (* ---------linear----------- *)
119 (prep_pbt LinEq.thy "pbl_equ_univ_lin" [] e_pblID
120 (["linear","univariate","equation"],
121 [("#Given" ,["equality e_","solveFor v_"]),
122 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
123 "Not( (lhs e_) is_polyrat_in v_)",
124 "Not( (rhs e_) is_polyrat_in v_)",
125 "((lhs e_) has_degree_in v_)=1",
126 "((rhs e_) has_degree_in v_)=1"]),
127 ("#Find" ,["solutions v_i_"])
129 LinEq_prls, SOME "solve (e_::bool, v_)",
130 [["LinEq","solve_lineq_equation"]]));
132 (*-------------- methods-------------------------------------------------------*)
134 (prep_met LinEq.thy "met_eqlin" [] e_metID
137 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
138 crls=LinEq_crls, nrls=norm_Poly
139 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
141 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
143 (prep_met LinEq.thy "met_eq_lin" [] e_metID
144 (["LinEq","solve_lineq_equation"],
145 [("#Given" ,["equality e_","solveFor v_"]),
146 ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
147 "( (lhs e_) has_degree_in v_)=1"]),
148 ("#Find" ,["solutions v_i_"])
150 {rew_ord'="termlessI",
155 crls=LinEq_crls, nrls=norm_Poly(*,
157 asm_thm=[("lin_isolate_div","")]*)},
158 "Script Solve_lineq_equation (e_::bool) (v_::real) = \
159 \(let e_ =((Try (Rewrite all_left False)) @@ \
160 \ (Try (Repeat (Rewrite makex1_x False))) @@ \
161 \ (Try (Rewrite_Set expand_binoms False)) @@ \
162 \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \
163 \ make_ratpoly_in False))) @@ \
164 \ (Try (Repeat (Rewrite_Set LinPoly_simplify False)))) e_;\
165 \ e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
166 \ LinEq_simplify True)) @@ \
167 \ (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_ \
168 \ in ((Or_to_List e_)::bool list))"
170 "******* LinEq.ML end *******";
171 get_met ["LinEq","solve_lineq_equation"];