diff -r 8cba439d0454 -r 68883c046963 src/Tools/isac/Knowledge/EqSystem.thy --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Apr 21 12:26:08 2020 +0200 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Apr 21 15:42:50 2020 +0200 @@ -406,18 +406,18 @@ (** problems **) setup \KEStore_Elems.add_pbts - [(Specify.prep_pbt thy "pbl_equsys" [] Celem.e_pblID + [(Specify.prep_pbt thy "pbl_equsys" [] Spec.e_pblID (["system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"](*''' is copy-named*))], Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), - (Specify.prep_pbt thy "pbl_equsys_lin" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin" [] Spec.e_pblID (["LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), (*TODO.WN050929 check linearity*) ("#Find" ,["solution ss'''"])], Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])), - (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_2x2" [] Spec.e_pblID (["2x2", "LINEAR", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) [("#Given" ,["equalities e_s", "solveForVars v_s"]), @@ -429,7 +429,7 @@ Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")], SOME "solveSystem e_s v_s", [])), - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Spec.e_pblID (["triangular", "2x2", "LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where", @@ -437,14 +437,14 @@ " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]), ("#Find" ,["solution ss'''"])], prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])), - (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_2x2_norm" [] Spec.e_pblID (["normalise", "2x2", "LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"])], Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [["EqSystem","normalise","2x2"]])), - (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_3x3" [] Spec.e_pblID (["3x3", "LINEAR", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) [("#Given" ,["equalities e_s", "solveForVars v_s"]), @@ -456,7 +456,7 @@ Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")], SOME "solveSystem e_s v_s", [])), - (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Spec.e_pblID (["4x4", "LINEAR", "system"], (*~~~~~~~~~~~~~~~~~~~~~~~~~*) [("#Given" ,["equalities e_s", "solveForVars v_s"]), @@ -468,7 +468,7 @@ Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"), Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")], SOME "solveSystem e_s v_s", [])), - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Spec.e_pblID (["triangular", "4x4", "LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" , (*accepts missing variables up to diagional form*) @@ -481,7 +481,7 @@ [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","4x4"]])), - (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.e_pblID + (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Spec.e_pblID (["normalise", "4x4", "LINEAR", "system"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), (*LENGTH is checked 1 level above*) @@ -510,12 +510,12 @@ (**methods**) setup \KEStore_Elems.add_mets - [Specify.prep_met thy "met_eqsys" [] Celem.e_metID + [Specify.prep_met thy "met_eqsys" [] Spec.e_metID (["EqSystem"], [], {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}, @{thm refl}), - Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID + Specify.prep_met thy "met_eqsys_topdown" [] Spec.e_metID (["EqSystem","top_down_substitution"], [], {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}, @@ -542,7 +542,7 @@ in Try (Rewrite_Set ''order_system'' ) e__s) " setup \KEStore_Elems.add_mets - [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID + [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Spec.e_metID (["EqSystem", "top_down_substitution", "2x2"], [("#Given", ["equalities e_s", "solveForVars v_s"]), ("#Where", @@ -558,7 +558,7 @@ @{thm solve_system.simps})] \ setup \KEStore_Elems.add_mets - [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID + [Specify.prep_met thy "met_eqsys_norm" [] Spec.e_metID (["EqSystem", "normalise"], [], {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}, @@ -580,7 +580,7 @@ SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met'']) [BOOL_LIST e__s, REAL_LIST v_s])" setup \KEStore_Elems.add_mets - [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID + [Specify.prep_met thy "met_eqsys_norm_2x2" [] Spec.e_metID (["EqSystem","normalise","2x2"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"])], @@ -612,7 +612,7 @@ SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met'']) [BOOL_LIST e__s, REAL_LIST v_s])" setup \KEStore_Elems.add_mets - [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID + [Specify.prep_met thy "met_eqsys_norm_4x4" [] Spec.e_metID (["EqSystem","normalise","4x4"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Find" ,["solution ss'''"])], @@ -644,7 +644,7 @@ in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])" setup \KEStore_Elems.add_mets - [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID + [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Spec.e_metID (["EqSystem","top_down_substitution","4x4"], [("#Given" ,["equalities e_s", "solveForVars v_s"]), ("#Where" , (*accepts missing variables up to diagonal form*)