neuper@37906: (*. (c) by Richard Lang, 2003 .*) neuper@37906: (* theory collecting all knowledge for LinearEquations neuper@37906: created by: rlang neuper@37906: date: 02.10 neuper@37906: changed by: rlang neuper@37906: last change by: rlang neuper@37906: date: 02.10.20 neuper@37906: *) neuper@37906: neuper@37950: theory LinEq imports Poly Equation begin neuper@37906: neuper@37906: consts neuper@37906: Solve'_lineq'_equation neuper@37950: :: "[bool,real, neuper@37950: bool list] => bool list" neuper@37950: ("((Script Solve'_lineq'_equation (_ _ =))// neuper@37950: (_))" 9) neuper@37906: neuper@37950: axioms neuper@37906: (*-- normalize --*) neuper@37906: (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*) neuper@37982: all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" neuper@37982: makex1_x: "a^^^1 = a" neuper@37982: real_assoc_1: "a+(b+c) = a+b+c" neuper@37982: real_assoc_2: "a*(b*c) = a*b*c" neuper@37906: neuper@37906: (*-- solve --*) neuper@37982: lin_isolate_add1: "(a + b*bdv = 0) = (b*bdv = (-1)*a)" neuper@37982: lin_isolate_add2: "(a + bdv = 0) = ( bdv = (-1)*a)" neuper@37982: lin_isolate_div: "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)" neuper@37950: neuper@37950: ML {* neuper@37972: val thy = @{theory}; neuper@37972: neuper@37950: val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*) neuper@37950: append_rls "LinEq_prls" e_rls neuper@37950: [Calc ("op =",eval_equal "#equal_"), neuper@37950: Calc ("Tools.matches",eval_matches ""), neuper@37950: Calc ("Tools.lhs" ,eval_lhs ""), neuper@37950: Calc ("Tools.rhs" ,eval_rhs ""), neuper@37950: Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), neuper@37950: Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), neuper@37950: Calc ("Atools.occurs'_in",eval_occurs_in ""), neuper@37950: Calc ("Atools.ident",eval_ident "#ident_"), neuper@37969: Thm ("not_true",num_str @{thm not_true}), neuper@37969: Thm ("not_false",num_str @{thm not_false}), neuper@37969: Thm ("and_true",num_str @{thm and_true}), neuper@37969: Thm ("and_false",num_str @{thm and_false}), neuper@37969: Thm ("or_true",num_str @{thm or_true}), neuper@37969: Thm ("or_false",num_str @{thm or_false}) neuper@37950: ]; neuper@37950: (* ----- erls ----- *) neuper@37950: val LinEq_crls = neuper@37950: append_rls "LinEq_crls" poly_crls neuper@37969: [Thm ("real_assoc_1",num_str @{thm real_assoc_1}) neuper@37950: (* neuper@37950: Don't use neuper@37981: Calc ("HOL.divide", eval_cancel "#divide_e"), neuper@37950: Calc ("Atools.pow" ,eval_binop "#power_"), neuper@37950: *) neuper@37950: ]; neuper@37950: neuper@37950: (* ----- crls ----- *) neuper@37950: val LinEq_erls = neuper@37950: append_rls "LinEq_erls" Poly_erls neuper@37969: [Thm ("real_assoc_1",num_str @{thm real_assoc_1}) neuper@37950: (* neuper@37950: Don't use neuper@37981: Calc ("HOL.divide", eval_cancel "#divide_e"), neuper@37950: Calc ("Atools.pow" ,eval_binop "#power_"), neuper@37950: *) neuper@37950: ]; neuper@37950: neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("LinEq_erls",LinEq_erls)(*FIXXXME:del with rls.rls'*) neuper@37950: ]); neuper@37950: neuper@37950: val LinPoly_simplify = prep_rls( neuper@37950: Rls {id = "LinPoly_simplify", preconds = [], neuper@37950: rew_ord = ("termlessI",termlessI), neuper@37950: erls = LinEq_erls, neuper@37950: srls = Erls, neuper@37950: calc = [], neuper@37950: (*asm_thm = [],*) neuper@37950: rules = [ neuper@37969: Thm ("real_assoc_1",num_str @{thm real_assoc_1}), neuper@37950: Calc ("op +",eval_binop "#add_"), neuper@37950: Calc ("op -",eval_binop "#sub_"), neuper@37950: Calc ("op *",eval_binop "#mult_"), neuper@37950: (* Dont use neuper@37981: Calc ("HOL.divide", eval_cancel "#divide_e"), neuper@37982: Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), neuper@37950: *) neuper@37950: Calc ("Atools.pow" ,eval_binop "#power_") neuper@37950: ], neuper@37982: scr = EmptyScr}:rls); neuper@37982: neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("LinPoly_simplify",LinPoly_simplify)]); neuper@37950: neuper@37950: (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) neuper@37950: val LinEq_simplify = prep_rls( neuper@37950: Rls {id = "LinEq_simplify", preconds = [], neuper@37950: rew_ord = ("e_rew_ord",e_rew_ord), neuper@37950: erls = LinEq_erls, neuper@37950: srls = Erls, neuper@37950: calc = [], neuper@37950: (*asm_thm = [("lin_isolate_div","")],*) neuper@37950: rules = [ neuper@37969: Thm("lin_isolate_add1",num_str @{thm lin_isolate_add1}), neuper@37950: (* a+bx=0 -> bx=-a *) neuper@37969: Thm("lin_isolate_add2",num_str @{thm lin_isolate_add2}), neuper@37950: (* a+ x=0 -> x=-a *) neuper@37969: Thm("lin_isolate_div",num_str @{thm lin_isolate_div}) neuper@37950: (* bx=c -> x=c/b *) neuper@37950: ], neuper@37982: scr = EmptyScr}:rls); neuper@37967: ruleset' := overwritelthy @{theory} (!ruleset', neuper@37950: [("LinEq_simplify",LinEq_simplify)]); neuper@37950: neuper@37950: (*----------------------------- problem types --------------------------------*) neuper@37950: (* neuper@37950: show_ptyps(); neuper@37950: (get_pbt ["linear","univariate","equation"]); neuper@37950: *) neuper@37982: neuper@37950: (* ---------linear----------- *) neuper@37950: store_pbt neuper@37972: (prep_pbt thy "pbl_equ_univ_lin" [] e_pblID neuper@37950: (["linear","univariate","equation"], neuper@37981: [("#Given" ,["equality e_e","solveFor v_v"]), neuper@37950: ("#Where" ,["False", (*WN0509 just detected: this pbl can never be used?!?*) neuper@37981: "Not( (lhs e_e) is_polyrat_in v_v)", neuper@37981: "Not( (rhs e_e) is_polyrat_in v_v)", neuper@37981: "((lhs e_e) has_degree_in v_v)=1", neuper@37981: "((rhs e_e) has_degree_in v_v)=1"]), neuper@38010: ("#Find" ,["solutions v'i'"]) neuper@37950: ], neuper@37981: LinEq_prls, SOME "solve (e_e::bool, v_v)", neuper@37950: [["LinEq","solve_lineq_equation"]])); neuper@37950: neuper@37950: (*-------------- methods------------------------------------------------------*) neuper@37950: store_met neuper@37972: (prep_met thy "met_eqlin" [] e_metID neuper@37950: (["LinEq"], neuper@37950: [], neuper@37950: {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, neuper@37950: crls=LinEq_crls, nrls=norm_Poly neuper@37950: (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); neuper@37950: neuper@37950: (* ansprechen mit ["LinEq","solve_univar_equation"] *) neuper@37950: store_met neuper@37972: (prep_met thy "met_eq_lin" [] e_metID neuper@37950: (["LinEq","solve_lineq_equation"], neuper@37982: [("#Given", ["equality e_e", "solveFor v_v"]), neuper@37982: ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", neuper@37982: "((lhs e_e) has_degree_in v_v) = 1"]), neuper@38010: ("#Find", ["solutions v'i'"]) neuper@37950: ], neuper@37982: {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls, neuper@37982: calc=[], crls=LinEq_crls, nrls=norm_Poly}, neuper@37982: "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^ neuper@37982: "(let e_e =((Try (Rewrite all_left False)) @@ " ^ neuper@37982: " (Try (Repeat (Rewrite makex1_x False))) @@ " ^ neuper@37982: " (Try (Rewrite_Set expand_binoms False)) @@ " ^ neuper@37982: " (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)] " ^ neuper@37982: " make_ratpoly_in False))) @@ " ^ neuper@37982: " (Try (Repeat (Rewrite_Set LinPoly_simplify False))))e_e;" ^ neuper@37982: " e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)] " ^ neuper@37982: " LinEq_simplify True)) @@ " ^ neuper@37981: " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^ neuper@37981: " in ((Or_to_List e_e)::bool list))" neuper@37950: )); neuper@37950: get_met ["LinEq","solve_lineq_equation"]; neuper@37982: neuper@37950: *} neuper@37950: neuper@37906: end neuper@37906: