1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue May 19 12:33:35 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed May 20 12:52:09 2020 +0200
1.3 @@ -85,7 +85,7 @@
1.4 ML \<open>
1.5 (** rewrite order 'ord_simplify_System' **)
1.6
1.7 -(* order wrt. several linear (i.e. without exponents) variables "c","c_2",..
1.8 +(* order wrt. several linear (i.e. without exponents) variables "c", "c_2",..
1.9 which leaves the monomials containing c, c_2,... at the end of an Integral
1.10 and puts the c, c_2,... rightmost within a monomial.
1.11
1.12 @@ -436,14 +436,14 @@
1.13 ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
1.14 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
1.15 ("#Find" ,["solution ss'''"])],
1.16 - prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])),
1.17 + prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem", "top_down_substitution", "2x2"]])),
1.18 (Problem.prep_input thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
1.19 (["normalise", "2x2", "LINEAR", "system"],
1.20 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.21 ("#Find" ,["solution ss'''"])],
1.22 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.23 SOME "solveSystem e_s v_s",
1.24 - [["EqSystem","normalise","2x2"]])),
1.25 + [["EqSystem", "normalise", "2x2"]])),
1.26 (Problem.prep_input thy "pbl_equsys_lin_3x3" [] Problem.id_empty
1.27 (["3x3", "LINEAR", "system"],
1.28 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.29 @@ -480,7 +480,7 @@
1.30 Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
1.31 [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.32 SOME "solveSystem e_s v_s",
1.33 - [["EqSystem","top_down_substitution","4x4"]])),
1.34 + [["EqSystem", "top_down_substitution", "4x4"]])),
1.35 (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
1.36 (["normalise", "4x4", "LINEAR", "system"],
1.37 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.38 @@ -488,7 +488,7 @@
1.39 ("#Find" ,["solution ss'''"])],
1.40 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
1.41 SOME "solveSystem e_s v_s",
1.42 - [["EqSystem","normalise","4x4"]]))]\<close>
1.43 + [["EqSystem", "normalise", "4x4"]]))]\<close>
1.44
1.45 ML \<open>
1.46 (*this is for NTH only*)
1.47 @@ -516,7 +516,7 @@
1.48 errpats = [], nrls = Rule_Set.Empty},
1.49 @{thm refl}),
1.50 Method.prep_input thy "met_eqsys_topdown" [] Method.id_empty
1.51 - (["EqSystem","top_down_substitution"], [],
1.52 + (["EqSystem", "top_down_substitution"], [],
1.53 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
1.54 errpats = [], nrls = Rule_Set.Empty},
1.55 @{thm refl})]
1.56 @@ -581,7 +581,7 @@
1.57 [BOOL_LIST e__s, REAL_LIST v_s])"
1.58 setup \<open>KEStore_Elems.add_mets
1.59 [Method.prep_input thy "met_eqsys_norm_2x2" [] Method.id_empty
1.60 - (["EqSystem","normalise","2x2"],
1.61 + (["EqSystem", "normalise", "2x2"],
1.62 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.63 ("#Find" ,["solution ss'''"])],
1.64 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.65 @@ -613,7 +613,7 @@
1.66 [BOOL_LIST e__s, REAL_LIST v_s])"
1.67 setup \<open>KEStore_Elems.add_mets
1.68 [Method.prep_input thy "met_eqsys_norm_4x4" [] Method.id_empty
1.69 - (["EqSystem","normalise","4x4"],
1.70 + (["EqSystem", "normalise", "4x4"],
1.71 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.72 ("#Find" ,["solution ss'''"])],
1.73 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
1.74 @@ -622,7 +622,7 @@
1.75 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
1.76 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})],
1.77 prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
1.78 - (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.79 + (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
1.80 @{thm solve_system3.simps})]
1.81 \<close>
1.82
1.83 @@ -645,7 +645,7 @@
1.84 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
1.85 setup \<open>KEStore_Elems.add_mets
1.86 [Method.prep_input thy "met_eqsys_topdown_4x4" [] Method.id_empty
1.87 - (["EqSystem","top_down_substitution","4x4"],
1.88 + (["EqSystem", "top_down_substitution", "4x4"],
1.89 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.90 ("#Where" , (*accepts missing variables up to diagonal form*)
1.91 ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",