diff -r d1b52fcd4023 -r 229e5c9cf78b src/Tools/isac/Knowledge/LinEq.thy --- a/src/Tools/isac/Knowledge/LinEq.thy Sun Mar 25 13:59:57 2018 +0200 +++ b/src/Tools/isac/Knowledge/LinEq.thy Mon Mar 26 07:28:39 2018 +0200 @@ -32,41 +32,41 @@ val thy = @{theory}; val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*) - Celem.append_rls "LinEq_prls" Celem.e_rls - [Celem.Calc ("HOL.eq",eval_equal "#equal_"), - Celem.Calc ("Tools.matches",eval_matches ""), - Celem.Calc ("Tools.lhs" ,eval_lhs ""), - Celem.Calc ("Tools.rhs" ,eval_rhs ""), - Celem.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), - Celem.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), - Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""), - Celem.Calc ("Atools.ident",eval_ident "#ident_"), - Celem.Thm ("not_true",TermC.num_str @{thm not_true}), - Celem.Thm ("not_false",TermC.num_str @{thm not_false}), - Celem.Thm ("and_true",TermC.num_str @{thm and_true}), - Celem.Thm ("and_false",TermC.num_str @{thm and_false}), - Celem.Thm ("or_true",TermC.num_str @{thm or_true}), - Celem.Thm ("or_false",TermC.num_str @{thm or_false}) + Rule.append_rls "LinEq_prls" Rule.e_rls + [Rule.Calc ("HOL.eq",eval_equal "#equal_"), + Rule.Calc ("Tools.matches",eval_matches ""), + Rule.Calc ("Tools.lhs" ,eval_lhs ""), + Rule.Calc ("Tools.rhs" ,eval_rhs ""), + Rule.Calc ("Poly.has'_degree'_in",eval_has_degree_in ""), + Rule.Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""), + Rule.Calc ("Atools.occurs'_in",eval_occurs_in ""), + Rule.Calc ("Atools.ident",eval_ident "#ident_"), + Rule.Thm ("not_true",TermC.num_str @{thm not_true}), + Rule.Thm ("not_false",TermC.num_str @{thm not_false}), + Rule.Thm ("and_true",TermC.num_str @{thm and_true}), + Rule.Thm ("and_false",TermC.num_str @{thm and_false}), + Rule.Thm ("or_true",TermC.num_str @{thm or_true}), + Rule.Thm ("or_false",TermC.num_str @{thm or_false}) ]; (* ----- erls ----- *) val LinEq_crls = - Celem.append_rls "LinEq_crls" poly_crls - [Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) + Rule.append_rls "LinEq_crls" poly_crls + [Rule.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) (* Don't use - Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), - Celem.Calc ("Atools.pow" ,eval_binop "#power_"), + Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), + Rule.Calc ("Atools.pow" ,eval_binop "#power_"), *) ]; (* ----- crls ----- *) val LinEq_erls = - Celem.append_rls "LinEq_erls" Poly_erls - [Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) + Rule.append_rls "LinEq_erls" Poly_erls + [Rule.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}) (* Don't use - Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), - Celem.Calc ("Atools.pow" ,eval_binop "#power_"), + Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), + Rule.Calc ("Atools.pow" ,eval_binop "#power_"), *) ]; *} @@ -75,23 +75,23 @@ ML {* val LinPoly_simplify = prep_rls'( - Celem.Rls {id = "LinPoly_simplify", preconds = [], + Rule.Rls {id = "LinPoly_simplify", preconds = [], rew_ord = ("termlessI",termlessI), erls = LinEq_erls, - srls = Celem.Erls, + srls = Rule.Erls, calc = [], errpatts = [], rules = [ - Celem.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}), - Celem.Calc ("Groups.plus_class.plus",eval_binop "#add_"), - Celem.Calc ("Groups.minus_class.minus",eval_binop "#sub_"), - Celem.Calc ("Groups.times_class.times",eval_binop "#mult_"), + Rule.Thm ("real_assoc_1",TermC.num_str @{thm real_assoc_1}), + Rule.Calc ("Groups.plus_class.plus",eval_binop "#add_"), + Rule.Calc ("Groups.minus_class.minus",eval_binop "#sub_"), + Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"), (* Dont use - Celem.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), - Celem.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), + Rule.Calc ("Rings.divide_class.divide", eval_cancel "#divide_e"), + Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"), *) - Celem.Calc ("Atools.pow" ,eval_binop "#power_") + Rule.Calc ("Atools.pow" ,eval_binop "#power_") ], - scr = Celem.EmptyScr}); + scr = Rule.EmptyScr}); *} setup {* KEStore_Elems.add_rlss [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *} @@ -99,20 +99,20 @@ (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*) val LinEq_simplify = prep_rls'( -Celem.Rls {id = "LinEq_simplify", preconds = [], - rew_ord = ("e_rew_ord", Celem.e_rew_ord), +Rule.Rls {id = "LinEq_simplify", preconds = [], + rew_ord = ("e_rew_ord", Rule.e_rew_ord), erls = LinEq_erls, - srls = Celem.Erls, + srls = Rule.Erls, calc = [], errpatts = [], rules = [ - Celem.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), + Rule.Thm("lin_isolate_add1",TermC.num_str @{thm lin_isolate_add1}), (* a+bx=0 -> bx=-a *) - Celem.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), + Rule.Thm("lin_isolate_add2",TermC.num_str @{thm lin_isolate_add2}), (* a+ x=0 -> x=-a *) - Celem.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div}) + Rule.Thm("lin_isolate_div",TermC.num_str @{thm lin_isolate_div}) (* bx=c -> x=c/b *) ], - scr = Celem.EmptyScr}); + scr = Rule.EmptyScr}); *} setup {* KEStore_Elems.add_rlss [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *} @@ -135,7 +135,7 @@ setup {* KEStore_Elems.add_mets [Specify.prep_met thy "met_eqlin" [] Celem.e_metID (["LinEq"], [], - {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Celem.e_rls, prls = Celem.e_rls, + {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = LinEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"), (* ansprechen mit ["LinEq","solve_univar_equation"] *) @@ -144,7 +144,7 @@ [("#Given", ["equality e_e", "solveFor v_v"]), ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]), ("#Find", ["solutions v_v'i'"])], - {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Celem.e_rls, prls = LinEq_prls, calc = [], + {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [], crls = LinEq_crls, errpats = [], nrls = norm_Poly}, "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^ "(let e_e =((Try (Rewrite all_left False)) @@ " ^