1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.ML Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,171 @@
1.4 +(*. (c) by Richard Lang, 2003 .*)
1.5 +(* collecting all knowledge for LinearEquations
1.6 + created by: rlang
1.7 + date: 02.10
1.8 + changed by: rlang
1.9 + last change by: rlang
1.10 + date: 02.11.04
1.11 +*)
1.12 +
1.13 +(* remove_thy"LinEq";
1.14 + use_thy"Knowledge/Isac";
1.15 +
1.16 + use_thy"Knowledge/LinEq";
1.17 +
1.18 + use"ROOT.ML";
1.19 + cd"knowledge";
1.20 +*)
1.21 +
1.22 +"******* LinEq.ML begin *******";
1.23 +
1.24 +(*-------------------- theory -------------------------------------------------*)
1.25 +theory' := overwritel (!theory', [("LinEq.thy",LinEq.thy)]);
1.26 +
1.27 +(*-------------- rules -------------------------------------------------------*)
1.28 +val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
1.29 + append_rls "LinEq_prls" e_rls
1.30 + [Calc ("op =",eval_equal "#equal_"),
1.31 + Calc ("Tools.matches",eval_matches ""),
1.32 + Calc ("Tools.lhs" ,eval_lhs ""),
1.33 + Calc ("Tools.rhs" ,eval_rhs ""),
1.34 + Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
1.35 + Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
1.36 + Calc ("Atools.occurs'_in",eval_occurs_in ""),
1.37 + Calc ("Atools.ident",eval_ident "#ident_"),
1.38 + Thm ("not_true",num_str not_true),
1.39 + Thm ("not_false",num_str not_false),
1.40 + Thm ("and_true",num_str and_true),
1.41 + Thm ("and_false",num_str and_false),
1.42 + Thm ("or_true",num_str or_true),
1.43 + Thm ("or_false",num_str or_false)
1.44 + ];
1.45 +(* ----- erls ----- *)
1.46 +val LinEq_crls =
1.47 + append_rls "LinEq_crls" poly_crls
1.48 + [Thm ("real_assoc_1",num_str real_assoc_1)
1.49 + (*
1.50 + Don't use
1.51 + Calc ("HOL.divide", eval_cancel "#divide_"),
1.52 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.53 + *)
1.54 + ];
1.55 +
1.56 +(* ----- crls ----- *)
1.57 +val LinEq_erls =
1.58 + append_rls "LinEq_erls" Poly_erls
1.59 + [Thm ("real_assoc_1",num_str real_assoc_1)
1.60 + (*
1.61 + Don't use
1.62 + Calc ("HOL.divide", eval_cancel "#divide_"),
1.63 + Calc ("Atools.pow" ,eval_binop "#power_"),
1.64 + *)
1.65 + ];
1.66 +
1.67 +ruleset' := overwritelthy thy (!ruleset',
1.68 + [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*)
1.69 + ]);
1.70 +
1.71 +val LinPoly_simplify = prep_rls(
1.72 + Rls {id = "LinPoly_simplify", preconds = [],
1.73 + rew_ord = ("termlessI",termlessI),
1.74 + erls = LinEq_erls,
1.75 + srls = Erls,
1.76 + calc = [],
1.77 + (*asm_thm = [],*)
1.78 + rules = [
1.79 + Thm ("real_assoc_1",num_str real_assoc_1),
1.80 + Calc ("op +",eval_binop "#add_"),
1.81 + Calc ("op -",eval_binop "#sub_"),
1.82 + Calc ("op *",eval_binop "#mult_"),
1.83 + (* Dont use
1.84 + Calc ("HOL.divide", eval_cancel "#divide_"),
1.85 + Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
1.86 + *)
1.87 + Calc ("Atools.pow" ,eval_binop "#power_")
1.88 + ],
1.89 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.90 + }:rls);
1.91 +ruleset' := overwritelthy thy (!ruleset',
1.92 + [("LinPoly_simplify",LinPoly_simplify)]);
1.93 +
1.94 +(*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
1.95 +val LinEq_simplify = prep_rls(
1.96 +Rls {id = "LinEq_simplify", preconds = [],
1.97 + rew_ord = ("e_rew_ord",e_rew_ord),
1.98 + erls = LinEq_erls,
1.99 + srls = Erls,
1.100 + calc = [],
1.101 + (*asm_thm = [("lin_isolate_div","")],*)
1.102 + rules = [
1.103 + Thm("lin_isolate_add1",num_str lin_isolate_add1),
1.104 + (* a+bx=0 -> bx=-a *)
1.105 + Thm("lin_isolate_add2",num_str lin_isolate_add2),
1.106 + (* a+ x=0 -> x=-a *)
1.107 + Thm("lin_isolate_div",num_str lin_isolate_div)
1.108 + (* bx=c -> x=c/b *)
1.109 + ],
1.110 + scr = Script ((term_of o the o (parse thy)) "empty_script")
1.111 + }:rls);
1.112 +ruleset' := overwritelthy thy (!ruleset',
1.113 + [("LinEq_simplify",LinEq_simplify)]);
1.114 +
1.115 +(*----------------------------- problem types --------------------------------*)
1.116 +(*
1.117 +show_ptyps();
1.118 +(get_pbt ["linear","univariate","equation"]);
1.119 +*)
1.120 +(* ---------linear----------- *)
1.121 +store_pbt
1.122 + (prep_pbt LinEq.thy "pbl_equ_univ_lin" [] e_pblID
1.123 + (["linear","univariate","equation"],
1.124 + [("#Given" ,["equality e_","solveFor v_"]),
1.125 + ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*)
1.126 + "Not( (lhs e_) is_polyrat_in v_)",
1.127 + "Not( (rhs e_) is_polyrat_in v_)",
1.128 + "((lhs e_) has_degree_in v_)=1",
1.129 + "((rhs e_) has_degree_in v_)=1"]),
1.130 + ("#Find" ,["solutions v_i_"])
1.131 + ],
1.132 + LinEq_prls, SOME "solve (e_::bool, v_)",
1.133 + [["LinEq","solve_lineq_equation"]]));
1.134 +
1.135 +(*-------------- methods-------------------------------------------------------*)
1.136 +store_met
1.137 + (prep_met LinEq.thy "met_eqlin" [] e_metID
1.138 + (["LinEq"],
1.139 + [],
1.140 + {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.141 + crls=LinEq_crls, nrls=norm_Poly
1.142 + (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
1.143 +
1.144 +(* ansprechen mit ["LinEq","solve_univar_equation"] *)
1.145 +store_met
1.146 +(prep_met LinEq.thy "met_eq_lin" [] e_metID
1.147 + (["LinEq","solve_lineq_equation"],
1.148 + [("#Given" ,["equality e_","solveFor v_"]),
1.149 + ("#Where" ,["Not( (lhs e_) is_polyrat_in v_)",
1.150 + "( (lhs e_) has_degree_in v_)=1"]),
1.151 + ("#Find" ,["solutions v_i_"])
1.152 + ],
1.153 + {rew_ord'="termlessI",
1.154 + rls'=LinEq_erls,
1.155 + srls=e_rls,
1.156 + prls=LinEq_prls,
1.157 + calc=[],
1.158 + crls=LinEq_crls, nrls=norm_Poly(*,
1.159 + asm_rls=[],
1.160 + asm_thm=[("lin_isolate_div","")]*)},
1.161 + "Script Solve_lineq_equation (e_::bool) (v_::real) = \
1.162 + \(let e_ =((Try (Rewrite all_left False)) @@ \
1.163 + \ (Try (Repeat (Rewrite makex1_x False))) @@ \
1.164 + \ (Try (Rewrite_Set expand_binoms False)) @@ \
1.165 + \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \
1.166 + \ make_ratpoly_in False))) @@ \
1.167 + \ (Try (Repeat (Rewrite_Set LinPoly_simplify False)))) e_;\
1.168 + \ e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
1.169 + \ LinEq_simplify True)) @@ \
1.170 + \ (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_ \
1.171 + \ in ((Or_to_List e_)::bool list))"
1.172 + ));
1.173 +"******* LinEq.ML end *******";
1.174 +get_met ["LinEq","solve_lineq_equation"];