30 |
30 |
31 ML {* |
31 ML {* |
32 val thy = @{theory}; |
32 val thy = @{theory}; |
33 |
33 |
34 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*) |
34 val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*) |
35 append_rls "LinEq_prls" e_rls |
35 Celem.append_rls "LinEq_prls" Celem.e_rls |
36 [Calc ("HOL.eq",eval_equal "#equal_"), |
36 [Celem.Calc ("HOL.eq",eval_equal "#equal_"), |
37 Calc ("Tools.matches",eval_matches ""), |
37 Celem.Calc ("Tools.matches",eval_matches ""), |
38 Calc ("Tools.lhs" ,eval_lhs ""), |
38 Celem.Calc ("Tools.lhs" ,eval_lhs ""), |
39 Calc ("Tools.rhs" ,eval_rhs ""), |
39 Celem.Calc ("Tools.rhs" ,eval_rhs ""), |
40 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), |
40 Celem.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), |
41 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), |
41 Celem.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), |
42 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
42 Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""), |
43 Calc ("Atools.ident",eval_ident "#ident_"), |
43 Celem.Calc ("Atools.ident",eval_ident "#ident_"), |
44 Thm ("not_true",TermC.num_str @{thm not_true}), |
44 Celem.Thm ("not_true",TermC.num_str @{thm not_true}), |
45 Thm ("not_false",TermC.num_str @{thm not_false}), |
45 Celem.Thm ("not_false",TermC.num_str @{thm not_false}), |
46 Thm ("and_true",TermC.num_str @{thm and_true}), |
46 Celem.Thm ("and_true",TermC.num_str @{thm and_true}), |
47 Thm ("and_false",TermC.num_str @{thm and_false}), |
47 Celem.Thm ("and_false",TermC.num_str @{thm and_false}), |
48 Thm ("or_true",TermC.num_str @{thm or_true}), |
48 Celem.Thm ("or_true",TermC.num_str @{thm or_true}), |
49 Thm ("or_false",TermC.num_str @{thm or_false}) |
49 Celem.Thm ("or_false",TermC.num_str @{thm or_false}) |
50 ]; |
50 ]; |
51 (* ----- erls ----- *) |
51 (* ----- erls ----- *) |
52 val LinEq_crls = |
52 val LinEq_crls = |
53 append_rls "LinEq_crls" poly_crls |
53 Celem.append_rls "LinEq_crls" poly_crls |
54 [Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) |
54 [Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) |
55 (* |
55 (* |
56 Don't use |
56 Don't use |
57 Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), |
57 Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), |
58 Calc ("Atools.pow" ,eval_binop "#power_"), |
58 Celem.Calc ("Atools.pow" ,eval_binop "#power_"), |
59 *) |
59 *) |
60 ]; |
60 ]; |
61 |
61 |
62 (* ----- crls ----- *) |
62 (* ----- crls ----- *) |
63 val LinEq_erls = |
63 val LinEq_erls = |
64 append_rls "LinEq_erls" Poly_erls |
64 Celem.append_rls "LinEq_erls" Poly_erls |
65 [Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) |
65 [Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) |
66 (* |
66 (* |
67 Don't use |
67 Don't use |
68 Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), |
68 Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), |
69 Calc ("Atools.pow" ,eval_binop "#power_"), |
69 Celem.Calc ("Atools.pow" ,eval_binop "#power_"), |
70 *) |
70 *) |
71 ]; |
71 ]; |
72 *} |
72 *} |
73 setup {* KEStore_Elems.add_rlss |
73 setup {* KEStore_Elems.add_rlss |
74 [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *} |
74 [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *} |
75 ML {* |
75 ML {* |
76 |
76 |
77 val LinPoly_simplify = prep_rls'( |
77 val LinPoly_simplify = prep_rls'( |
78 Rls {id = "LinPoly_simplify", preconds = [], |
78 Celem.Rls {id = "LinPoly_simplify", preconds = [], |
79 rew_ord = ("termlessI",termlessI), |
79 rew_ord = ("termlessI",termlessI), |
80 erls = LinEq_erls, |
80 erls = LinEq_erls, |
81 srls = Erls, |
81 srls = Celem.Erls, |
82 calc = [], errpatts = [], |
82 calc = [], errpatts = [], |
83 rules = [ |
83 rules = [ |
84 Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}), |
84 Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}), |
85 Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
85 Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"), |
86 Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
86 Celem.Calc ("Groups.minus_class.minus",eval_binop "#sub_"), |
87 Calc ("Groups.times_class.times",eval_binop "#mult_"), |
87 Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"), |
88 (* Dont use |
88 (* Dont use |
89 Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), |
89 Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), |
90 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
90 Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), |
91 *) |
91 *) |
92 Calc ("Atools.pow" ,eval_binop "#power_") |
92 Celem.Calc ("Atools.pow" ,eval_binop "#power_") |
93 ], |
93 ], |
94 scr = EmptyScr}:rls); |
94 scr = Celem.EmptyScr}); |
95 *} |
95 *} |
96 setup {* KEStore_Elems.add_rlss |
96 setup {* KEStore_Elems.add_rlss |
97 [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *} |
97 [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *} |
98 ML {* |
98 ML {* |
99 |
99 |
100 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) |
100 (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) |
101 val LinEq_simplify = prep_rls'( |
101 val LinEq_simplify = prep_rls'( |
102 Rls {id = "LinEq_simplify", preconds = [], |
102 Celem.Rls {id = "LinEq_simplify", preconds = [], |
103 rew_ord = ("e_rew_ord",e_rew_ord), |
103 rew_ord = ("xxxe_rew_ordxxx", Celem.e_rew_ord), |
104 erls = LinEq_erls, |
104 erls = LinEq_erls, |
105 srls = Erls, |
105 srls = Celem.Erls, |
106 calc = [], errpatts = [], |
106 calc = [], errpatts = [], |
107 rules = [ |
107 rules = [ |
108 Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), |
108 Celem.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), |
109 (* a+bx=0 -> bx=-a *) |
109 (* a+bx=0 -> bx=-a *) |
110 Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), |
110 Celem.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), |
111 (* a+ x=0 -> x=-a *) |
111 (* a+ x=0 -> x=-a *) |
112 Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div}) |
112 Celem.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div}) |
113 (* bx=c -> x=c/b *) |
113 (* bx=c -> x=c/b *) |
114 ], |
114 ], |
115 scr = EmptyScr}:rls); |
115 scr = Celem.EmptyScr}); |
116 *} |
116 *} |
117 setup {* KEStore_Elems.add_rlss |
117 setup {* KEStore_Elems.add_rlss |
118 [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *} |
118 [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *} |
119 |
119 |
120 (*----------------------------- problem types --------------------------------*) |
120 (*----------------------------- problem types --------------------------------*) |
121 (* ---------linear----------- *) |
121 (* ---------linear----------- *) |
122 setup {* KEStore_Elems.add_pbts |
122 setup {* KEStore_Elems.add_pbts |
123 [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] e_pblID |
123 [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Celem.e_pblID |
124 (["LINEAR", "univariate", "equation"], |
124 (["LINEAR", "univariate", "equation"], |
125 [("#Given" ,["equality e_e", "solveFor v_v"]), |
125 [("#Given" ,["equality e_e", "solveFor v_v"]), |
126 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*) |
126 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*) |
127 "Not( (lhs e_e) is_polyrat_in v_v)", |
127 "Not( (lhs e_e) is_polyrat_in v_v)", |
128 "Not( (rhs e_e) is_polyrat_in v_v)", |
128 "Not( (rhs e_e) is_polyrat_in v_v)", |
131 ("#Find" ,["solutions v_v'i'"])], |
131 ("#Find" ,["solutions v_v'i'"])], |
132 LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *} |
132 LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *} |
133 |
133 |
134 (*-------------- methods------------------------------------------------------*) |
134 (*-------------- methods------------------------------------------------------*) |
135 setup {* KEStore_Elems.add_mets |
135 setup {* KEStore_Elems.add_mets |
136 [Specify.prep_met thy "met_eqlin" [] e_metID |
136 [Specify.prep_met thy "met_eqlin" [] Celem.e_metID |
137 (["LinEq"], [], |
137 (["LinEq"], [], |
138 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = e_rls, prls = e_rls, |
138 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Celem.e_rls, prls = Celem.e_rls, |
139 crls = LinEq_crls, errpats = [], nrls = norm_Poly}, |
139 crls = LinEq_crls, errpats = [], nrls = norm_Poly}, |
140 "empty_script"), |
140 "empty_script"), |
141 (* ansprechen mit ["LinEq","solve_univar_equation"] *) |
141 (* ansprechen mit ["LinEq","solve_univar_equation"] *) |
142 Specify.prep_met thy "met_eq_lin" [] e_metID |
142 Specify.prep_met thy "met_eq_lin" [] Celem.e_metID |
143 (["LinEq","solve_lineq_equation"], |
143 (["LinEq","solve_lineq_equation"], |
144 [("#Given", ["equality e_e", "solveFor v_v"]), |
144 [("#Given", ["equality e_e", "solveFor v_v"]), |
145 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), |
145 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), |
146 ("#Find", ["solutions v_v'i'"])], |
146 ("#Find", ["solutions v_v'i'"])], |
147 {rew_ord' = "termlessI", rls' = LinEq_erls, srls = e_rls, prls = LinEq_prls, calc = [], |
147 {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Celem.e_rls, prls = LinEq_prls, calc = [], |
148 crls = LinEq_crls, errpats = [], nrls = norm_Poly}, |
148 crls = LinEq_crls, errpats = [], nrls = norm_Poly}, |
149 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^ |
149 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^ |
150 "(let e_e =((Try (Rewrite all_left False)) @@ " ^ |
150 "(let e_e =((Try (Rewrite all_left False)) @@ " ^ |
151 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^ |
151 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^ |
152 " (Try (Rewrite_Set expand_binoms False)) @@ " ^ |
152 " (Try (Rewrite_Set expand_binoms False)) @@ " ^ |