1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 21 12:32:54 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Nov 28 11:46:00 2018 +0100
1.3 @@ -516,7 +516,7 @@
1.4
1.5 (**methods**)
1.6 setup \<open>KEStore_Elems.add_mets
1.7 - [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
1.8 + [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
1.9 (["EqSystem"], [],
1.10 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.11 errpats = [], nrls = Rule.Erls},
1.12 @@ -525,8 +525,10 @@
1.13 (["EqSystem","top_down_substitution"], [],
1.14 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.15 errpats = [], nrls = Rule.Erls},
1.16 - "empty_script"),
1.17 - Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
1.18 + "empty_script")]
1.19 +\<close>
1.20 +setup \<open>KEStore_Elems.add_mets
1.21 + [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
1.22 (["EqSystem", "top_down_substitution", "2x2"],
1.23 [("#Given", ["equalities e_s", "solveForVars v_s"]),
1.24 ("#Where",
1.25 @@ -571,13 +573,17 @@
1.26 " isolate_bdvs False)) @@ " ^
1.27 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
1.28 " simplify_System False))) e__s)"
1.29 - ---------------------------------------------------------------------------*)),
1.30 - Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
1.31 + ---------------------------------------------------------------------------*))]
1.32 +\<close>
1.33 +setup \<open>KEStore_Elems.add_mets
1.34 + [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
1.35 (["EqSystem", "normalise"], [],
1.36 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
1.37 errpats = [], nrls = Rule.Erls},
1.38 - "empty_script"),
1.39 - Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
1.40 + "empty_script")]
1.41 +\<close>
1.42 +setup \<open>KEStore_Elems.add_mets
1.43 + [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
1.44 (["EqSystem","normalise","2x2"],
1.45 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.46 ("#Find" ,["solution ss'''"])],
1.47 @@ -597,8 +603,10 @@
1.48 " simplify_System_parenthesized False)) @@ " ^
1.49 " (Try (Rewrite_Set order_system False))) e_s " ^
1.50 " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
1.51 - " [BOOL_LIST e__s, REAL_LIST v_s]))"),
1.52 - Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
1.53 + " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.54 +\<close>
1.55 +setup \<open>KEStore_Elems.add_mets
1.56 + [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
1.57 (["EqSystem","normalise","4x4"],
1.58 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.59 ("#Find" ,["solution ss'''"])],
1.60 @@ -624,8 +632,10 @@
1.61 " simplify_System_parenthesized False)) @@ " ^
1.62 " (Try (Rewrite_Set order_system False))) e_s " ^
1.63 " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
1.64 - " [BOOL_LIST e__s, REAL_LIST v_s]))"),
1.65 - Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
1.66 + " [BOOL_LIST e__s, REAL_LIST v_s]))")]
1.67 +\<close>
1.68 +setup \<open>KEStore_Elems.add_mets
1.69 + [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
1.70 (["EqSystem","top_down_substitution","4x4"],
1.71 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
1.72 ("#Where" , (*accepts missing variables up to diagonal form*)