46 ==> (a + b = c) = (b = -1*a + c)" and |
46 ==> (a + b = c) = (b = -1*a + c)" and |
47 separate_bdvs_mult: |
47 separate_bdvs_mult: |
48 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] |
48 "[| [] from [bdv_1,bdv_2,bdv_3,bdv_4] occur_exactly_in a; Not (a=!=0) |] |
49 ==>(a * b = c) = (b = c / a)" |
49 ==>(a * b = c) = (b = c / a)" |
50 axiomatization where (*..if replaced by "and" we get an error in |
50 axiomatization where (*..if replaced by "and" we get an error in |
51 --- rewrite in [EqSystem,normalize,2x2] --- step "--- 3---";*) |
51 --- rewrite in [EqSystem,normalise,2x2] --- step "--- 3---";*) |
52 order_system_NxN: "[a,b] = [b,a]" |
52 order_system_NxN: "[a,b] = [b,a]" |
53 (*requires rew_ord for termination, eg. ord_simplify_Integral; |
53 (*requires rew_ord for termination, eg. ord_simplify_Integral; |
54 works for lists of any length, interestingly !?!*) |
54 works for lists of any length, interestingly !?!*) |
55 |
55 |
56 ML {* |
56 ML {* |
496 SOME "solveSystem e_s v_s", |
496 SOME "solveSystem e_s v_s", |
497 [["EqSystem","normalise","4x4"]]))] *} |
497 [["EqSystem","normalise","4x4"]]))] *} |
498 |
498 |
499 ML {* |
499 ML {* |
500 (*this is for NTH only*) |
500 (*this is for NTH only*) |
501 val srls = Rls {id="srls_normalize_4x4", |
501 val srls = Rls {id="srls_normalise_4x4", |
502 preconds = [], |
502 preconds = [], |
503 rew_ord = ("termlessI",termlessI), |
503 rew_ord = ("termlessI",termlessI), |
504 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
504 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls |
505 [(*for asm in NTH_CONS ...*) |
505 [(*for asm in NTH_CONS ...*) |
506 Calc ("Orderings.ord_class.less",eval_equ "#less_"), |
506 Calc ("Orderings.ord_class.less",eval_equ "#less_"), |
580 Specify.prep_met thy "met_eqsys_norm_2x2" [] e_metID |
580 Specify.prep_met thy "met_eqsys_norm_2x2" [] e_metID |
581 (["EqSystem","normalise","2x2"], |
581 (["EqSystem","normalise","2x2"], |
582 [("#Given" ,["equalities e_s", "solveForVars v_s"]), |
582 [("#Given" ,["equalities e_s", "solveForVars v_s"]), |
583 ("#Find" ,["solution ss'''"])], |
583 ("#Find" ,["solution ss'''"])], |
584 {rew_ord'="tless_true", rls' = Erls, calc = [], |
584 {rew_ord'="tless_true", rls' = Erls, calc = [], |
585 srls = append_rls "srls_normalize_2x2" e_rls |
585 srls = append_rls "srls_normalise_2x2" e_rls |
586 [Thm ("hd_thm",num_str @{thm hd_thm}), |
586 [Thm ("hd_thm",num_str @{thm hd_thm}), |
587 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
587 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
588 Thm ("tl_Nil",num_str @{thm tl_Nil})], |
588 Thm ("tl_Nil",num_str @{thm tl_Nil})], |
589 prls = Erls, crls = Erls, errpats = [], nrls = Erls}, |
589 prls = Erls, crls = Erls, errpats = [], nrls = Erls}, |
590 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
590 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
601 Specify.prep_met thy "met_eqsys_norm_4x4" [] e_metID |
601 Specify.prep_met thy "met_eqsys_norm_4x4" [] e_metID |
602 (["EqSystem","normalise","4x4"], |
602 (["EqSystem","normalise","4x4"], |
603 [("#Given" ,["equalities e_s", "solveForVars v_s"]), |
603 [("#Given" ,["equalities e_s", "solveForVars v_s"]), |
604 ("#Find" ,["solution ss'''"])], |
604 ("#Find" ,["solution ss'''"])], |
605 {rew_ord'="tless_true", rls' = Erls, calc = [], |
605 {rew_ord'="tless_true", rls' = Erls, calc = [], |
606 srls = append_rls "srls_normalize_4x4" srls |
606 srls = append_rls "srls_normalise_4x4" srls |
607 [Thm ("hd_thm",num_str @{thm hd_thm}), |
607 [Thm ("hd_thm",num_str @{thm hd_thm}), |
608 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
608 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
609 Thm ("tl_Nil",num_str @{thm tl_Nil})], |
609 Thm ("tl_Nil",num_str @{thm tl_Nil})], |
610 prls = Erls, crls = Erls, errpats = [], nrls = Erls}, |
610 prls = Erls, crls = Erls, errpats = [], nrls = Erls}, |
611 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
611 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |