diff -r d82a32869f27 -r f3cac3053e7b src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Apr 01 19:20:05 2020 +0200 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sat Apr 04 12:11:32 2020 +0200 @@ -170,10 +170,10 @@ (*.adapted from 'order_add_mult_in' by just replacing the rew_ord.*) val order_add_mult_System = - Rule.Rls{id = "order_add_mult_System", preconds = [], + Rule_Set.Rls{id = "order_add_mult_System", preconds = [], rew_ord = ("ord_simplify_System", ord_simplify_System false @{theory "Integrate"}), - erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [], + erls = Rule_Set.e_rls,srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}), (* z * w = w * z *) Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}), @@ -194,9 +194,9 @@ #1 using 'ord_simplify_System' in 'order_add_mult_System' #2 NOT using common_nominator_p .*) val norm_System_noadd_fractions = - Rule.Rls {id = "norm_System_noadd_fractions", preconds = [], + Rule_Set.Rls {id = "norm_System_noadd_fractions", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), - erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [(*sequence given by operator precedence*) Rule.Rls_ discard_minus, Rule.Rls_ powers, @@ -215,9 +215,9 @@ (*.adapted from 'norm_Rational' by *1* using 'ord_simplify_System' in 'order_add_mult_System'.*) val norm_System = - Rule.Rls {id = "norm_System", preconds = [], + Rule_Set.Rls {id = "norm_System", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), - erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = norm_rat_erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [(*sequence given by operator precedence*) Rule.Rls_ discard_minus, Rule.Rls_ powers, @@ -243,9 +243,9 @@ *3* discard_parentheses only for (.*(.*.)) analoguous to simplify_Integral .*) val simplify_System_parenthesized = - Rule.Seq {id = "simplify_System_parenthesized", preconds = []:term list, + Rule_Set.Seq {id = "simplify_System_parenthesized", preconds = []:term list, rew_ord = ("dummy_ord", Rule.dummy_ord), - erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("distrib_right",TermC.num_str @{thm distrib_right}), (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*) Rule.Thm ("add_divide_distrib",TermC.num_str @{thm add_divide_distrib}), @@ -268,9 +268,9 @@ *1* ord_simplify_System instead of termlessI .*) (*TODO.WN051031 ^^^^^^^^^^ should be in EACH rls contained *) val simplify_System = - Rule.Seq {id = "simplify_System", preconds = []:term list, + Rule_Set.Seq {id = "simplify_System", preconds = []:term list, rew_ord = ("dummy_ord", Rule.dummy_ord), - erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = Atools_erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Rls_ norm_Rational, Rule.Rls_ (*order_add_mult_in*) norm_System (**1**), Rule.Rls_ discard_parentheses, @@ -281,21 +281,21 @@ scr = Rule.EmptyScr}; (* val simplify_System = - Rule.append_rls "simplify_System" simplify_System_parenthesized + Rule_Set.append_rls "simplify_System" simplify_System_parenthesized [Rule.Thm ("sym_add_assoc", TermC.num_str (@{thm add.assoc} RS @{thm sym}))]; *) \ ML \ val isolate_bdvs = - Rule.Rls {id="isolate_bdvs", preconds = [], + Rule_Set.Rls {id="isolate_bdvs", preconds = [], rew_ord = ("e_rew_ord", Rule.e_rew_ord), - erls = Rule.append_rls "erls_isolate_bdvs" Rule.e_rls + erls = Rule_Set.append_rls "erls_isolate_bdvs" Rule_Set.e_rls [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_")) ], - srls = Rule.Erls, calc = [], errpatts = [], + srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}), Rule.Thm ("separate_bdvs_add", TermC.num_str @{thm separate_bdvs_add}), @@ -304,10 +304,10 @@ \ ML \ val isolate_bdvs_4x4 = - Rule.Rls {id="isolate_bdvs_4x4", preconds = [], + Rule_Set.Rls {id="isolate_bdvs_4x4", preconds = [], rew_ord = ("e_rew_ord", Rule.e_rew_ord), - erls = Rule.append_rls - "erls_isolate_bdvs_4x4" Rule.e_rls + erls = Rule_Set.append_rls + "erls_isolate_bdvs_4x4" Rule_Set.e_rls [Rule.Num_Calc ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_"), Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"), @@ -315,7 +315,7 @@ Rule.Thm ("not_true",TermC.num_str @{thm not_true}), Rule.Thm ("not_false",TermC.num_str @{thm not_false}) ], - srls = Rule.Erls, calc = [], errpatts = [], + srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("commute_0_equality", TermC.num_str @{thm commute_0_equality}), Rule.Thm ("separate_bdvs0", TermC.num_str @{thm separate_bdvs0}), Rule.Thm ("separate_bdvs_add1", TermC.num_str @{thm separate_bdvs_add1}), @@ -329,20 +329,20 @@ (*.order the equations in a system such, that a triangular system (if any) appears as [..c_4 = .., ..., ..., ..c_1 + ..c_2 + ..c_3 ..c_4 = ..].*) val order_system = - Rule.Rls {id="order_system", preconds = [], + Rule_Set.Rls {id="order_system", preconds = [], rew_ord = ("ord_simplify_System", ord_simplify_System false thy), - erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("order_system_NxN", TermC.num_str @{thm order_system_NxN}) ], scr = Rule.EmptyScr}; val prls_triangular = - Rule.Rls {id="prls_triangular", preconds = [], + Rule_Set.Rls {id="prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rule.e_rew_ord), - erls = Rule.Rls {id="erls_prls_triangular", preconds = [], + erls = Rule_Set.Rls {id="erls_prls_triangular", preconds = [], rew_ord = ("e_rew_ord", Rule.e_rew_ord), - erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [(*for precond NTH_CONS ...*) Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_") @@ -350,7 +350,7 @@ '+' into precondition !*) ], scr = Rule.EmptyScr}, - srls = Rule.Erls, calc = [], errpatts = [], + srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), @@ -367,11 +367,11 @@ (*WN060914 quickly created for 4x4; more similarity to prls_triangular desirable*) val prls_triangular4 = - Rule.Rls {id="prls_triangular4", preconds = [], + Rule_Set.Rls {id="prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rule.e_rew_ord), - erls = Rule.Rls {id="erls_prls_triangular4", preconds = [], + erls = Rule_Set.Rls {id="erls_prls_triangular4", preconds = [], rew_ord = ("e_rew_ord", Rule.e_rew_ord), - erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [], + erls = Rule_Set.Erls, srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [(*for precond NTH_CONS ...*) Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_") @@ -379,7 +379,7 @@ '+' into precondition !*) ], scr = Rule.EmptyScr}, - srls = Rule.Erls, calc = [], errpatts = [], + srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}), @@ -410,20 +410,20 @@ (["system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"](*''' is copy-named*))], - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID (["LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), (*TODO.WN050929 check linearity*) ("#Find" ,["solution ss'''"])], - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID (["2x2", "LINEAR", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" ,["LENGTH (e_s:: bool list) = 2", "LENGTH v_s = 2"]), ("#Find" ,["solution ss'''"])], - Rule.append_rls "prls_2x2_linear_system" Rule.e_rls + Rule_Set.append_rls "prls_2x2_linear_system" Rule_Set.e_rls [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), @@ -441,7 +441,7 @@ (["normalise", "2x2", "LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"])], - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [["EqSystem","normalise","2x2"]])), (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID @@ -450,7 +450,7 @@ [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" ,["LENGTH (e_s:: bool list) = 3", "LENGTH v_s = 3"]), ("#Find" ,["solution ss'''"])], - Rule.append_rls "prls_3x3_linear_system" Rule.e_rls + Rule_Set.append_rls "prls_3x3_linear_system" Rule_Set.e_rls [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), @@ -462,7 +462,7 @@ [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" ,["LENGTH (e_s:: bool list) = 4", "LENGTH v_s = 4"]), ("#Find" ,["solution ss'''"])], - Rule.append_rls "prls_4x4_linear_system" Rule.e_rls + Rule_Set.append_rls "prls_4x4_linear_system" Rule_Set.e_rls [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}), Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}), Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"), @@ -477,7 +477,7 @@ "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))", "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]), ("#Find" ,["solution ss'''"])], - Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular + Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","4x4"]])), @@ -486,22 +486,22 @@ [("#Given" ,["equalities e_s", "solveForVars v_s"]), (*LENGTH is checked 1 level above*) ("#Find" ,["solution ss'''"])], - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], + Rule_Set.append_rls "e_rls" Rule_Set.e_rls [(*for preds in where_*)], SOME "solveSystem e_s v_s", [["EqSystem","normalise","4x4"]]))]\ ML \ (*this is for NTH only*) -val srls = Rule.Rls {id="srls_normalise_4x4", +val srls = Rule_Set.Rls {id="srls_normalise_4x4", preconds = [], rew_ord = ("termlessI",termlessI), - erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls + erls = Rule_Set.append_rls "erls_in_srls_IntegrierenUnd.." Rule_Set.e_rls [(*for asm in NTH_CONS ...*) Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"), (*2nd NTH_CONS pushes n+-1 into asms*) Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_") ], - srls = Rule.Erls, calc = [], errpatts = [], + srls = Rule_Set.Erls, calc = [], errpatts = [], rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}), Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})], @@ -512,13 +512,13 @@ setup \KEStore_Elems.add_mets [Specify.prep_met thy "met_eqsys" [] Celem.e_metID (["EqSystem"], [], - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, - errpats = [], nrls = Rule.Erls}, + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls, + errpats = [], nrls = Rule_Set.Erls}, @{thm refl}), Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID (["EqSystem","top_down_substitution"], [], - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, - errpats = [], nrls = Rule.Erls}, + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls, + errpats = [], nrls = Rule_Set.Erls}, @{thm refl})] \ @@ -549,19 +549,19 @@ ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))", " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]), ("#Find" ,["solution ss'''"])], - {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [], - srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [], + srls = Rule_Set.append_rls "srls_top_down_2x2" Rule_Set.e_rls [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], - prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, + prls = prls_triangular, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls}, @{thm solve_system.simps})] \ setup \KEStore_Elems.add_mets [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID (["EqSystem", "normalise"], [], - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, - errpats = [], nrls = Rule.Erls}, + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], srls = Rule_Set.Erls, prls = Rule_Set.Erls, crls = Rule_Set.Erls, + errpats = [], nrls = Rule_Set.Erls}, @{thm refl})] \ @@ -584,12 +584,12 @@ (["EqSystem","normalise","2x2"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"])], - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], - srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], + srls = Rule_Set.append_rls "srls_normalise_2x2" Rule_Set.e_rls [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], - prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, + prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls}, @{thm solve_system2.simps})] \ @@ -616,12 +616,12 @@ (["EqSystem","normalise","4x4"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"])], - {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], - srls = Rule.append_rls "srls_normalise_4x4" srls + {rew_ord'="tless_true", rls' = Rule_Set.Erls, calc = [], + srls = Rule_Set.append_rls "srls_normalise_4x4" srls [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], - prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, + prls = Rule_Set.Erls, crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls}, (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*) @{thm solve_system3.simps})] \ @@ -653,11 +653,11 @@ "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))", "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]), ("#Find", ["solution ss'''"])], - {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [], - srls = Rule.append_rls "srls_top_down_4x4" srls [], - prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular + {rew_ord'="ord_simplify_System", rls' = Rule_Set.Erls, calc = [], + srls = Rule_Set.append_rls "srls_top_down_4x4" srls [], + prls = Rule_Set.append_rls "prls_tri_4x4_lin_sys" prls_triangular [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], - crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, + crls = Rule_Set.Erls, errpats = [], nrls = Rule_Set.Erls}, (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*) @{thm solve_system4.simps})] \