1 (*. (c) by Richard Lang, 2003 .*)
2 (* theory collecting all knowledge for LinearEquations
10 theory LinEq imports Poly Equation begin
13 Solve'_lineq'_equation
15 bool list] => bool list"
16 ("((Script Solve'_lineq'_equation (_ _ =))//
21 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
22 all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"
24 real_assoc_1 "a+(b+c) = a+b+c"
25 real_assoc_2 "a*(b*c) = a*b*c"
28 lin_isolate_add1 "(a + b*bdv = 0) = (b*bdv = (-1)*a)"
29 lin_isolate_add2 "(a + bdv = 0) = ( bdv = (-1)*a)"
30 lin_isolate_div "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
33 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
34 append_rls "LinEq_prls" e_rls
35 [Calc ("op =",eval_equal "#equal_"),
36 Calc ("Tools.matches",eval_matches ""),
37 Calc ("Tools.lhs" ,eval_lhs ""),
38 Calc ("Tools.rhs" ,eval_rhs ""),
39 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
40 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
41 Calc ("Atools.occurs'_in",eval_occurs_in ""),
42 Calc ("Atools.ident",eval_ident "#ident_"),
43 Thm ("not_true",num_str not_true),
44 Thm ("not_false",num_str not_false),
45 Thm ("and_true",num_str and_true),
46 Thm ("and_false",num_str and_false),
47 Thm ("or_true",num_str or_true),
48 Thm ("or_false",num_str or_false)
50 (* ----- erls ----- *)
52 append_rls "LinEq_crls" poly_crls
53 [Thm ("real_assoc_1",num_str real_assoc_1)
56 Calc ("HOL.divide", eval_cancel "#divide_"),
57 Calc ("Atools.pow" ,eval_binop "#power_"),
61 (* ----- crls ----- *)
63 append_rls "LinEq_erls" Poly_erls
64 [Thm ("real_assoc_1",num_str real_assoc_1)
67 Calc ("HOL.divide", eval_cancel "#divide_"),
68 Calc ("Atools.pow" ,eval_binop "#power_"),
72 ruleset' := overwritelthy thy (!ruleset',
73 [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
76 val LinPoly_simplify = prep_rls(
77 Rls {id = "LinPoly_simplify", preconds = [],
78 rew_ord = ("termlessI",termlessI),
84 Thm ("real_assoc_1",num_str real_assoc_1),
85 Calc ("op +",eval_binop "#add_"),
86 Calc ("op -",eval_binop "#sub_"),
87 Calc ("op *",eval_binop "#mult_"),
89 Calc ("HOL.divide", eval_cancel "#divide_"),
90 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
92 Calc ("Atools.pow" ,eval_binop "#power_")
94 scr = Script ((term_of o the o (parse thy)) "empty_script")
96 ruleset' := overwritelthy thy (!ruleset',
97 [("LinPoly_simplify",LinPoly_simplify)]);
99 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
100 val LinEq_simplify = prep_rls(
101 Rls {id = "LinEq_simplify", preconds = [],
102 rew_ord = ("e_rew_ord",e_rew_ord),
106 (*asm_thm = [("lin_isolate_div","")],*)
108 Thm("lin_isolate_add1",num_str lin_isolate_add1),
109 (* a+bx=0 -> bx=-a *)
110 Thm("lin_isolate_add2",num_str lin_isolate_add2),
112 Thm("lin_isolate_div",num_str lin_isolate_div)
115 scr = Script ((term_of o the o (parse thy)) "empty_script")
117 ruleset' := overwritelthy thy (!ruleset',
118 [("LinEq_simplify",LinEq_simplify)]);
120 (*----------------------------- problem types --------------------------------*)
123 (get_pbt ["linear","univariate","equation"]);
125 (* ---------linear----------- *)
127 (prep_pbt LinEq.thy "pbl_equ_univ_lin" [] e_pblID
128 (["linear","univariate","equation"],
129 [("#Given" ,["equality e_","solveFor v_"]),
130 ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
131 "Not( (lhs e_) is_polyrat_in v_)",
132 "Not( (rhs e_) is_polyrat_in v_)",
133 "((lhs e_) has_degree_in v_)=1",
134 "((rhs e_) has_degree_in v_)=1"]),
135 ("#Find" ,["solutions v_i_"])
137 LinEq_prls, SOME "solve (e_::bool, v_)",
138 [["LinEq","solve_lineq_equation"]]));
140 (*-------------- methods------------------------------------------------------*)
142 (prep_met LinEq.thy "met_eqlin" [] e_metID
145 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
146 crls=LinEq_crls, nrls=norm_Poly
147 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
149 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
151 (prep_met LinEq.thy "met_eq_lin" [] e_metID
152 (["LinEq","solve_lineq_equation"],
153 [("#Given" ,["equality e_","solveFor v_"]),
154 ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
155 "( (lhs e_) has_degree_in v_)=1"]),
156 ("#Find" ,["solutions v_i_"])
158 {rew_ord'="termlessI",
163 crls=LinEq_crls, nrls=norm_Poly(*,
165 asm_thm=[("lin_isolate_div","")]*)},
166 "Script Solve_lineq_equation (e_::bool) (v_::real) = " ^
167 "(let e_ =((Try (Rewrite all_left False)) @@ " ^
168 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
169 " (Try (Rewrite_Set expand_binoms False)) @@ " ^
170 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] " ^
171 " make_ratpoly_in False))) @@ " ^
172 " (Try (Repeat (Rewrite_Set LinPoly_simplify False)))) e_;" ^
173 " e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
174 " LinEq_simplify True)) @@ " ^
175 " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_ " ^
176 " in ((Or_to_List e_)::bool list))"
178 "******* LinEq.ML end *******";
179 get_met ["LinEq","solve_lineq_equation"];