1 (*. (c) by Richard Lang, 2003 .*) |
|
2 (* collecting all knowledge for LinearEquations |
|
3 created by: rlang |
|
4 date: 02.10 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.11.04 |
|
8 *) |
|
9 |
|
10 (* remove_thy"LinEq"; |
|
11 use_thy"IsacKnowledge/Isac"; |
|
12 |
|
13 use_thy"IsacKnowledge/LinEq"; |
|
14 |
|
15 use"ROOT.ML"; |
|
16 cd"knowledge"; |
|
17 *) |
|
18 |
|
19 "******* LinEq.ML begin *******"; |
|
20 |
|
21 (*-------------------- theory -------------------------------------------------*) |
|
22 theory' := overwritel (!theory', [("LinEq.thy",LinEq.thy)]); |
|
23 |
|
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) |
|
41 ]; |
|
42 (* ----- erls ----- *) |
|
43 val LinEq_crls = |
|
44 append_rls "LinEq_crls" poly_crls |
|
45 [Thm ("real_assoc_1",num_str real_assoc_1) |
|
46 (* |
|
47 Don't use |
|
48 Calc ("HOL.divide", eval_cancel "#divide_"), |
|
49 Calc ("Atools.pow" ,eval_binop "#power_"), |
|
50 *) |
|
51 ]; |
|
52 |
|
53 (* ----- crls ----- *) |
|
54 val LinEq_erls = |
|
55 append_rls "LinEq_erls" Poly_erls |
|
56 [Thm ("real_assoc_1",num_str real_assoc_1) |
|
57 (* |
|
58 Don't use |
|
59 Calc ("HOL.divide", eval_cancel "#divide_"), |
|
60 Calc ("Atools.pow" ,eval_binop "#power_"), |
|
61 *) |
|
62 ]; |
|
63 |
|
64 ruleset' := overwritelthy thy (!ruleset', |
|
65 [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*) |
|
66 ]); |
|
67 |
|
68 val LinPoly_simplify = prep_rls( |
|
69 Rls {id = "LinPoly_simplify", preconds = [], |
|
70 rew_ord = ("termlessI",termlessI), |
|
71 erls = LinEq_erls, |
|
72 srls = Erls, |
|
73 calc = [], |
|
74 (*asm_thm = [],*) |
|
75 rules = [ |
|
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_"), |
|
80 (* Dont use |
|
81 Calc ("HOL.divide", eval_cancel "#divide_"), |
|
82 Calc ("Root.sqrt",eval_sqrt "#sqrt_"), |
|
83 *) |
|
84 Calc ("Atools.pow" ,eval_binop "#power_") |
|
85 ], |
|
86 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
87 }:rls); |
|
88 ruleset' := overwritelthy thy (!ruleset', |
|
89 [("LinPoly_simplify",LinPoly_simplify)]); |
|
90 |
|
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), |
|
95 erls = LinEq_erls, |
|
96 srls = Erls, |
|
97 calc = [], |
|
98 (*asm_thm = [("lin_isolate_div","")],*) |
|
99 rules = [ |
|
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), |
|
103 (* a+ x=0 -> x=-a *) |
|
104 Thm("lin_isolate_div",num_str lin_isolate_div) |
|
105 (* bx=c -> x=c/b *) |
|
106 ], |
|
107 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
108 }:rls); |
|
109 ruleset' := overwritelthy thy (!ruleset', |
|
110 [("LinEq_simplify",LinEq_simplify)]); |
|
111 |
|
112 (*----------------------------- problem types --------------------------------*) |
|
113 (* |
|
114 show_ptyps(); |
|
115 (get_pbt ["linear","univariate","equation"]); |
|
116 *) |
|
117 (* ---------linear----------- *) |
|
118 store_pbt |
|
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_"]) |
|
128 ], |
|
129 LinEq_prls, SOME "solve (e_::bool, v_)", |
|
130 [["LinEq","solve_lineq_equation"]])); |
|
131 |
|
132 (*-------------- methods-------------------------------------------------------*) |
|
133 store_met |
|
134 (prep_met LinEq.thy "met_eqlin" [] e_metID |
|
135 (["LinEq"], |
|
136 [], |
|
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")); |
|
140 |
|
141 (* ansprechen mit ["LinEq","solve_univar_equation"] *) |
|
142 store_met |
|
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_"]) |
|
149 ], |
|
150 {rew_ord'="termlessI", |
|
151 rls'=LinEq_erls, |
|
152 srls=e_rls, |
|
153 prls=LinEq_prls, |
|
154 calc=[], |
|
155 crls=LinEq_crls, nrls=norm_Poly(*, |
|
156 asm_rls=[], |
|
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))" |
|
169 )); |
|
170 "******* LinEq.ML end *******"; |
|
171 get_met ["LinEq","solve_lineq_equation"]; |
|