Isar command 'method' as combination of KEStore_Elems.add_mets + MethodC.prep_import, without change of semantics;
1.1 --- a/src/Tools/isac/BaseDefinitions/references-def.sml Sat Jun 12 18:33:15 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/references-def.sml Tue Jun 15 22:24:20 2021 +0200
1.3 @@ -10,6 +10,8 @@
1.4 val id_to_string: id -> string
1.5 val empty_probl_id: id
1.6 val empty_meth_id: id
1.7 + val explode_id: string -> id
1.8 + val implode_id: id -> string
1.9
1.10 type T
1.11 val empty: T
1.12 @@ -28,6 +30,9 @@
1.13 val empty_probl_id = ["empty_probl_id"];
1.14 val empty_meth_id = ["empty_meth_id"];
1.15
1.16 +val explode_id = space_explode "/";
1.17 +val implode_id = space_implode "/";
1.18 +
1.19 type T = (* 3-dimensional universe of math knowledge: *)
1.20 ThyC.id * (* reference to a theory comprising definitions *)
1.21 id * (* will become Problem.id; a reference into a tree *)
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sat Jun 12 18:33:15 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Jun 15 22:24:20 2021 +0200
2.3 @@ -63,6 +63,7 @@
2.4 val mk_var_op_num: term -> string -> typ -> typ -> int -> term
2.5
2.6 val matches: theory -> term -> term -> bool
2.7 + val parse_strict: theory -> string -> term
2.8 val parse: theory -> string -> cterm option
2.9 val parseN: theory -> string -> cterm option
2.10 val parseNEW: Proof.context -> string -> term option
2.11 @@ -504,9 +505,11 @@
2.12 \<^try>\<open>
2.13 let val t = (*(typ_a2real o numbers_to_string)*) (Syntax.read_term_global thy str)
2.14 in Thm.global_cterm_of thy t end\<close>;
2.15 +
2.16 +fun parse_strict thy str = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str);
2.17 fun parse thy str = (* introduced 2010 *)
2.18 \<^try>\<open>
2.19 - let val t = (typ_a2real o numbers_to_string) (Syntax.read_term_global thy str)
2.20 + let val t = parse_strict thy str
2.21 in Thm.global_cterm_of thy t end\<close>;
2.22
2.23 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
3.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Sat Jun 12 18:33:15 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Tue Jun 15 22:24:20 2021 +0200
3.3 @@ -30,18 +30,13 @@
3.4 ("#Find", ["GesamtLaenge l_l"])],
3.5 Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
3.6
3.7 -setup \<open>KEStore_Elems.add_mets
3.8 - [MethodC.prep_input @{theory} "met_algein" [] MethodC.id_empty
3.9 - (["Berechnung"], [],
3.10 - {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
3.11 - errpats = [], nrls = Rule_Set.Empty},
3.12 - @{thm refl}),
3.13 - MethodC.prep_input @{theory} "met_algein_numsym" [] MethodC.id_empty
3.14 - (["Berechnung", "erstNumerisch"], [],
3.15 - {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
3.16 - errpats = [], nrls = Rule_Set.Empty},
3.17 - @{thm refl})]
3.18 -\<close>
3.19 +method met_algein : "Berechnung" =
3.20 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
3.21 + errpats = [], nrls = Rule_Set.Empty}\<close>
3.22 +
3.23 +method met_algein_numsym : "Berechnung/erstNumerisch" =
3.24 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
3.25 + errpats = [], nrls = Rule_Set.Empty}\<close>
3.26
3.27 partial_function (tailrec) symbolisch_rechnen :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
3.28 where
3.29 @@ -65,18 +60,16 @@
3.30 t_t = Repeat (Try (Rewrite_Set ''norm_Poly'')) t_t
3.31 in
3.32 Try (Rewrite_Set ''norm_Poly'') t_t)"
3.33 -setup \<open>KEStore_Elems.add_mets
3.34 - [MethodC.prep_input @{theory} "met_algein_numsym_1num" [] MethodC.id_empty
3.35 - (["Berechnung", "erstNumerisch"],
3.36 - [("#Given" ,["KantenLaenge k_k", "Querschnitt q__q", "KantenUnten u_u",
3.37 - "KantenSenkrecht s_s", "KantenOben o_o"]),
3.38 - ("#Find" ,["GesamtLaenge l_l"])],
3.39 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
3.40 - srls = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
3.41 - [\<^rule_eval>\<open>Prog_Expr.boollist2sum\<close> (Prog_Expr.eval_boollist2sum "")],
3.42 - prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},
3.43 - @{thm symbolisch_rechnen.simps})]
3.44 -\<close>
3.45 +
3.46 +method met_algein_numsym_1num : "Berechnung/erstNumerisch" =
3.47 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
3.48 + srls =
3.49 + Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
3.50 + [\<^rule_eval>\<open>Prog_Expr.boollist2sum\<close> (Prog_Expr.eval_boollist2sum "")],
3.51 + prls = Rule_Set.empty, crls =Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
3.52 + Program: symbolisch_rechnen.simps
3.53 + Given: "KantenLaenge k_k" "Querschnitt q__q" "KantenUnten u_u" "KantenSenkrecht s_s" "KantenOben o_o"
3.54 + Find: "GesamtLaenge l_l"
3.55
3.56 partial_function (tailrec) symbolisch_rechnen_2 :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
3.57 where
3.58 @@ -98,18 +91,18 @@
3.59 t_t = Substitute [k_k, q__q] t_t
3.60 in
3.61 (Try (Rewrite_Set ''norm_Poly'')) t_t)"
3.62 -setup \<open>KEStore_Elems.add_mets
3.63 - [MethodC.prep_input @{theory} "met_algein_symnum" [] MethodC.id_empty
3.64 - (["Berechnung", "erstSymbolisch"],
3.65 - [("#Given" ,["KantenLaenge k_k", "Querschnitt q__q", "KantenUnten u_u",
3.66 - "KantenSenkrecht s_s", "KantenOben o_o"]),
3.67 - ("#Find" ,["GesamtLaenge l_l"])],
3.68 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
3.69 - srls = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
3.70 - [\<^rule_eval>\<open>Prog_Expr.boollist2sum\<close> (Prog_Expr.eval_boollist2sum "")],
3.71 - prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},
3.72 - @{thm symbolisch_rechnen.simps})]
3.73 -\<close> ML \<open>
3.74 +
3.75 +method met_algein_symnum : "Berechnung/erstSymbolisch" =
3.76 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
3.77 + srls =
3.78 + Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty
3.79 + [\<^rule_eval>\<open>Prog_Expr.boollist2sum\<close> (Prog_Expr.eval_boollist2sum "")],
3.80 + prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational}\<close>
3.81 + Program: symbolisch_rechnen.simps
3.82 + Given: "KantenLaenge k_k" "Querschnitt q__q" "KantenUnten u_u" "KantenSenkrecht s_s" "KantenOben o_o"
3.83 + Find: "GesamtLaenge l_l"
3.84 +
3.85 +ML \<open>
3.86 \<close> ML \<open>
3.87 \<close>
3.88 end
4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Sat Jun 12 18:33:15 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Jun 15 22:24:20 2021 +0200
4.3 @@ -193,13 +193,9 @@
4.4
4.5 section \<open>Methods\<close>
4.6 (* setup parent directory *)
4.7 -setup \<open>KEStore_Elems.add_mets
4.8 - [MethodC.prep_input @{theory} "met_biege" [] MethodC.id_empty
4.9 - (["IntegrierenUndKonstanteBestimmen"], [],
4.10 - {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
4.11 - errpats = [], nrls = Rule_Set.Empty},
4.12 - @{thm refl})]
4.13 -\<close>
4.14 +method met_biege : "IntegrierenUndKonstanteBestimmen" =
4.15 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
4.16 + errpats = [], nrls = Rule_Set.Empty}\<close>
4.17
4.18 subsection \<open>Survey on Methods\<close>
4.19 text \<open>
4.20 @@ -249,51 +245,45 @@
4.21 B = Take (lastI funs);
4.22 B = ((Substitute cons) #> (Rewrite_Set_Inst [(''bdv'', fun_var)] ''make_ratpoly_in'')) B
4.23 in B)"
4.24 -setup \<open>KEStore_Elems.add_mets
4.25 - [MethodC.prep_input @{theory} "met_biege_2" [] MethodC.id_empty
4.26 - (["IntegrierenUndKonstanteBestimmen2"],
4.27 - [("#Given" ,["Traegerlaenge beam", "Streckenlast load",
4.28 - "FunktionsVariable fun_var", "GleichungsVariablen vs", "AbleitungBiegelinie id_der"]),
4.29 - (*("#Where",["0 < beam"]), ...wait for < and handling Arbfix*)
4.30 - ("#Find" ,["Biegelinie id_fun"]),
4.31 - ("#Relate",["Randbedingungen side_conds"])],
4.32 - {rew_ord'="tless_true",
4.33 - rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
4.34 - [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.35 - \<^rule_thm>\<open>not_true\<close>,
4.36 - \<^rule_thm>\<open>not_false\<close>],
4.37 - calc = [],
4.38 - srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
4.39 - [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
4.40 - \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.41 - \<^rule_thm>\<open>last_thmI\<close>,
4.42 - \<^rule_thm>\<open>if_True\<close>,
4.43 - \<^rule_thm>\<open>if_False\<close>],
4.44 - prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty},
4.45 - @{thm biegelinie.simps})]
4.46 -\<close>
4.47 -setup \<open>KEStore_Elems.add_mets
4.48 - [MethodC.prep_input @{theory} "met_biege_intconst_2" [] MethodC.id_empty
4.49 - (["IntegrierenUndKonstanteBestimmen", "2xIntegrieren"], [],
4.50 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.51 - errpats = [], nrls = Rule_Set.empty},
4.52 - @{thm refl}),
4.53 - MethodC.prep_input @{theory} "met_biege_intconst_4" [] MethodC.id_empty
4.54 - (["IntegrierenUndKonstanteBestimmen", "4x4System"], [],
4.55 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.56 - errpats = [], nrls = Rule_Set.empty},
4.57 - @{thm refl}),
4.58 - MethodC.prep_input @{theory} "met_biege_intconst_1" [] MethodC.id_empty
4.59 - (["IntegrierenUndKonstanteBestimmen", "1xIntegrieren"], [],
4.60 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.61 - errpats = [], nrls = Rule_Set.empty},
4.62 - @{thm refl}),
4.63 - MethodC.prep_input @{theory} "met_biege2" [] MethodC.id_empty
4.64 - (["Biegelinien"], [],
4.65 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.66 - errpats = [], nrls = Rule_Set.empty},
4.67 - @{thm refl})]
4.68 -\<close>
4.69 +
4.70 +method met_biege_2 : "IntegrierenUndKonstanteBestimmen2" =
4.71 + \<open>{rew_ord'="tless_true",
4.72 + rls' = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
4.73 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.74 + \<^rule_thm>\<open>not_true\<close>,
4.75 + \<^rule_thm>\<open>not_false\<close>],
4.76 + calc = [],
4.77 + srls = Rule_Set.append_rules "erls_IntegrierenUndK.." Rule_Set.empty
4.78 + [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
4.79 + \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.80 + \<^rule_thm>\<open>last_thmI\<close>,
4.81 + \<^rule_thm>\<open>if_True\<close>,
4.82 + \<^rule_thm>\<open>if_False\<close>],
4.83 + prls = Rule_Set.Empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.Empty}\<close>
4.84 + Program: biegelinie.simps
4.85 + Given: "Traegerlaenge beam" "Streckenlast load"
4.86 + "FunktionsVariable fun_var" "GleichungsVariablen vs" "AbleitungBiegelinie id_der"
4.87 + (* Where: "0 < beam" ...wait for < and handling Arbfix*)
4.88 + Find: "Biegelinie id_fun"
4.89 + Relate: "Randbedingungen side_conds"
4.90 +
4.91 +method met_biege_intconst_2 : "IntegrierenUndKonstanteBestimmen/2xIntegrieren" =
4.92 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.93 + errpats = [], nrls = Rule_Set.empty}\<close>
4.94 +
4.95 +method met_biege_intconst_4 : "IntegrierenUndKonstanteBestimmen/4x4System" =
4.96 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.97 + errpats = [], nrls = Rule_Set.empty}\<close>
4.98 +
4.99 +method met_biege_intconst_1 : "IntegrierenUndKonstanteBestimmen/1xIntegrieren" =
4.100 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.101 + errpats = [], nrls = Rule_Set.empty}\<close>
4.102 +
4.103 +method met_biege2 : "Biegelinien" =
4.104 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
4.105 + errpats = [], nrls = Rule_Set.empty}\<close>
4.106 +
4.107 +
4.108 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
4.109
4.110 partial_function (tailrec) belastung_zu_biegelinie ::
4.111 @@ -320,23 +310,21 @@
4.112 [''diff'', ''integration'', ''named'']) [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
4.113 in
4.114 [Q__Q, M__M, N__N, B__B])" (*..Q is Const Querkraft -------------------------^ *)
4.115 -setup \<open>KEStore_Elems.add_mets
4.116 - [MethodC.prep_input @{theory} "met_biege_ausbelast" [] MethodC.id_empty
4.117 - (["Biegelinien", "ausBelastung"],
4.118 - [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v",
4.119 - "Biegelinie id_fun", "AbleitungBiegelinie id_der"]),
4.120 - ("#Find" ,["Funktionen fun_s"])],
4.121 - {rew_ord'="tless_true",
4.122 - rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty
4.123 - [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.124 - \<^rule_thm>\<open>not_true\<close>,
4.125 - \<^rule_thm>\<open>not_false\<close>],
4.126 - calc = [],
4.127 - srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty
4.128 - [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],
4.129 - prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
4.130 - @{thm belastung_zu_biegelinie.simps})]
4.131 -\<close>
4.132 +
4.133 +method met_biege_ausbelast : "Biegelinien/ausBelastung" =
4.134 + \<open>{rew_ord'="tless_true",
4.135 + rls' = Rule_Set.append_rules "erls_ausBelastung" Rule_Set.empty
4.136 + [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
4.137 + \<^rule_thm>\<open>not_true\<close>,
4.138 + \<^rule_thm>\<open>not_false\<close>],
4.139 + calc = [],
4.140 + srls = Rule_Set.append_rules "srls_ausBelastung" Rule_Set.empty
4.141 + [\<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_")],
4.142 + prls = Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
4.143 + Program: belastung_zu_biegelinie.simps
4.144 + Given: "Streckenlast q__q" "FunktionsVariable v_v" "Biegelinie id_fun" "AbleitungBiegelinie id_der"
4.145 + Find: "Funktionen fun_s"
4.146 +
4.147 subsection \<open>Substitute the constraints into the equations\<close>
4.148
4.149 partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
4.150 @@ -361,15 +349,15 @@
4.151 [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
4.152 in
4.153 [e_1, e_2, e_3, e_4])"
4.154 -setup \<open>KEStore_Elems.add_mets
4.155 - [MethodC.prep_input @{theory} "met_biege_setzrand" [] MethodC.id_empty
4.156 - (["Biegelinien", "setzeRandbedingungenEin"],
4.157 - [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
4.158 - ("#Find" , ["Gleichungen equs'''"])],
4.159 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = srls2, prls=Rule_Set.empty, crls = Atools_erls,
4.160 - errpats = [], nrls = Rule_Set.empty},
4.161 - @{thm setzte_randbedingungen.simps})]
4.162 -\<close>
4.163 +
4.164 +method met_biege_setzrand : "Biegelinien/setzeRandbedingungenEin" =
4.165 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = srls2, prls=Rule_Set.empty, crls = Atools_erls,
4.166 + errpats = [], nrls = Rule_Set.empty}\<close>
4.167 + Program: setzte_randbedingungen.simps
4.168 + Given: "Funktionen fun_s" "Randbedingungen r_b"
4.169 + Find: "Gleichungen equs'''"
4.170 +
4.171 +
4.172 subsection \<open>Transform an equality into a function\<close>
4.173
4.174 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
4.175 @@ -385,20 +373,19 @@
4.176 eq_u = Substitute [su_b] eq_u
4.177 in
4.178 (Rewrite_Set ''norm_Rational'') eq_u)"
4.179 -setup \<open>KEStore_Elems.add_mets
4.180 - [MethodC.prep_input @{theory} "met_equ_fromfun" [] MethodC.id_empty
4.181 - (["Equation", "fromFunction"],
4.182 - [("#Given" ,["functionEq fu_n", "substitution su_b"]),
4.183 - ("#Find" ,["equality equ'''"])],
4.184 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],
4.185 - srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty
4.186 - [\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
4.187 - \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
4.188 - prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
4.189 - (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
4.190 - 0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
4.191 - @{thm function_to_equality.simps})]
4.192 -\<close>
4.193 +
4.194 +method met_equ_fromfun : "Equation/fromFunction" =
4.195 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],
4.196 + srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty
4.197 + [\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
4.198 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
4.199 + prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
4.200 + Program: function_to_equality.simps
4.201 + (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
4.202 + 0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
4.203 + Given: "functionEq fu_n" "substitution su_b"
4.204 + Find: "equality equ'''"
4.205 +
4.206 ML \<open>
4.207 \<close> ML \<open>
4.208 \<close> ML \<open>
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sat Jun 12 18:33:15 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Jun 15 22:24:20 2021 +0200
5.3 @@ -269,13 +269,10 @@
5.4 ]
5.5 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
5.6 \<close>
5.7 -setup \<open>KEStore_Elems.add_mets
5.8 - [MethodC.prep_input @{theory} "met_diff" [] MethodC.id_empty
5.9 - (["diff"], [],
5.10 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.11 - crls = Atools_erls, errpats = [], nrls = norm_diff},
5.12 - @{thm refl})]
5.13 -\<close>
5.14 +
5.15 +method met_diff : "diff" =
5.16 + \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.17 + crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
5.18
5.19 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
5.20 where
5.21 @@ -304,15 +301,13 @@
5.22 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
5.23 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
5.24 ) f_f')"
5.25 -setup \<open>KEStore_Elems.add_mets
5.26 - [MethodC.prep_input @{theory} "met_diff_onR" [] MethodC.id_empty
5.27 - (["diff", "differentiate_on_R"],
5.28 - [("#Given" ,["functionTerm f_f", "differentiateFor v_v"]),
5.29 - ("#Find" ,["derivative f_f'"])],
5.30 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.31 - crls = Atools_erls, errpats = [], nrls = norm_diff},
5.32 - @{thm differentiate_on_R.simps})]
5.33 -\<close>
5.34 +
5.35 +method met_diff_onR : "diff/differentiate_on_R" =
5.36 + \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.37 + crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
5.38 + Program: differentiate_on_R.simps
5.39 + Given: "functionTerm f_f" "differentiateFor v_v"
5.40 + Find: "derivative f_f'"
5.41
5.42 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
5.43 where
5.44 @@ -339,15 +334,13 @@
5.45 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
5.46 (Repeat (Rewrite_Set ''make_polynomial'')))
5.47 ) f_f')"
5.48 -setup \<open>KEStore_Elems.add_mets
5.49 - [MethodC.prep_input @{theory} "met_diff_simpl" [] MethodC.id_empty
5.50 - (["diff", "diff_simpl"],
5.51 - [("#Given", ["functionTerm f_f", "differentiateFor v_v"]),
5.52 - ("#Find" , ["derivative f_f'"])],
5.53 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.54 - crls = Atools_erls, errpats = [], nrls = norm_diff},
5.55 - @{thm differentiateX.simps})]
5.56 -\<close>
5.57 +
5.58 +method met_diff_simpl : "diff/diff_simpl" =
5.59 + \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.60 + crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
5.61 + Program: differentiateX.simps
5.62 + Given: "functionTerm f_f" " differentiateFor v_v"
5.63 + Find: "derivative f_f'"
5.64
5.65 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
5.66 where
5.67 @@ -377,15 +370,13 @@
5.68 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
5.69 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
5.70 ) f_f')"
5.71 -setup \<open>KEStore_Elems.add_mets
5.72 - [MethodC.prep_input @{theory} "met_diff_equ" [] MethodC.id_empty
5.73 - (["diff", "differentiate_equality"],
5.74 - [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),
5.75 - ("#Find" ,["derivativeEq f_f'"])],
5.76 - {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule_Set.empty,
5.77 - crls=Atools_erls, errpats = [], nrls = norm_diff},
5.78 - @{thm differentiate_equality.simps})]
5.79 -\<close>
5.80 +
5.81 +method met_diff_equ : "diff/differentiate_equality" =
5.82 + \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule_Set.empty,
5.83 + crls=Atools_erls, errpats = [], nrls = norm_diff}\<close>
5.84 + Program: differentiate_equality.simps
5.85 + Given: "functionEq f_f" "differentiateFor v_v"
5.86 + Find: "derivativeEq f_f'"
5.87
5.88 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
5.89 where
5.90 @@ -400,15 +391,13 @@
5.91 (Try (Rewrite_Set ''norm_Rational''))
5.92 ) term')"
5.93
5.94 -setup \<open>KEStore_Elems.add_mets
5.95 - [MethodC.prep_input @{theory} "met_diff_after_simp" [] MethodC.id_empty
5.96 - (["diff", "after_simplification"],
5.97 - [("#Given" ,["functionTerm term", "differentiateFor bound_variable"]),
5.98 - ("#Find" ,["derivative term'"])],
5.99 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.100 - crls=Atools_erls, errpats = [], nrls = norm_Rational},
5.101 - @{thm simplify_derivative.simps})]
5.102 -\<close>
5.103 +method met_diff_after_simp : "diff/after_simplification" =
5.104 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
5.105 + crls=Atools_erls, errpats = [], nrls = norm_Rational}\<close>
5.106 + Program: simplify_derivative.simps
5.107 + Given: "functionTerm term" "differentiateFor bound_variable"
5.108 + Find: "derivative term'"
5.109 +
5.110 setup \<open>KEStore_Elems.add_cas
5.111 [((Thm.term_of o the o (TermC.parse @{theory})) "Diff",
5.112 (("Isac_Knowledge", ["derivative_of", "function"], ["no_met"]), argl2dtss))]\<close>
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Jun 12 18:33:15 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Jun 15 22:24:20 2021 +0200
6.3 @@ -100,13 +100,10 @@
6.4
6.5
6.6 (** methods, scripts not yet implemented **)
6.7 -setup \<open>KEStore_Elems.add_mets
6.8 - [MethodC.prep_input @{theory} "met_diffapp" [] MethodC.id_empty
6.9 - (["DiffApp"], [],
6.10 - {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
6.11 - crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.12 - @{thm refl})]
6.13 -\<close>
6.14 +
6.15 +method met_diffapp : "DiffApp" =
6.16 + \<open>{rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
6.17 + crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
6.18
6.19 partial_function (tailrec) maximum_value ::
6.20 "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
6.21 @@ -122,17 +119,15 @@
6.22 [BOOL t_t, REAL v_v, REAL_SET itv_v]
6.23 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
6.24 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
6.25 -setup \<open>KEStore_Elems.add_mets
6.26 - [MethodC.prep_input @{theory} "met_diffapp_max" [] MethodC.id_empty
6.27 - (["DiffApp", "max_by_calculus"],
6.28 - [("#Given" ,["fixedValues f_ix", "maximum m_m", "relations r_s", "boundVariable v_v",
6.29 - "interval i_tv", "errorBound e_rr"]),
6.30 - ("#Find" ,["valuesFor v_s"]),
6.31 - ("#Relate",[])],
6.32 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
6.33 - errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.34 - @{thm maximum_value.simps})]
6.35 -\<close>
6.36 +
6.37 +method met_diffapp_max : "DiffApp/max_by_calculus" =
6.38 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
6.39 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
6.40 + Program: maximum_value.simps
6.41 + Given: "fixedValues f_ix" "maximum m_m" "relations r_s" "boundVariable v_v"
6.42 + "interval i_tv" "errorBound e_rr"
6.43 + Find: "valuesFor v_s"
6.44 + Relate:
6.45
6.46 partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
6.47 where
6.48 @@ -149,15 +144,13 @@
6.49 s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
6.50 [BOOL e_2, REAL v_2]
6.51 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
6.52 -setup \<open>KEStore_Elems.add_mets
6.53 - [MethodC.prep_input @{theory} "met_diffapp_funnew" [] MethodC.id_empty
6.54 - (["DiffApp", "make_fun_by_new_variable"],
6.55 - [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
6.56 - ("#Find" ,["functionEq f_1"])],
6.57 - {rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,
6.58 - errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)},
6.59 - @{thm make_fun_by_new_variable.simps})]
6.60 -\<close>
6.61 +
6.62 +method met_diffapp_funnew : "DiffApp/make_fun_by_new_variable" =
6.63 + \<open>{rew_ord'="tless_true",rls'=eval_rls,srls=prog_expr,prls=Rule_Set.empty, calc=[], crls = eval_rls,
6.64 + errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}\<close>
6.65 + Program: make_fun_by_new_variable.simps
6.66 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
6.67 + Find: "functionEq f_1"
6.68
6.69 partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
6.70 where
6.71 @@ -169,29 +162,24 @@
6.72 s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])
6.73 [BOOL e_1, REAL v_1]
6.74 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
6.75 -setup \<open>KEStore_Elems.add_mets
6.76 - [MethodC.prep_input @{theory} "met_diffapp_funexp" [] MethodC.id_empty
6.77 - (["DiffApp", "make_fun_by_explicit"],
6.78 - [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
6.79 - ("#Find" ,["functionEq f_1"])],
6.80 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
6.81 - errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.82 - @{thm make_fun_by_explicit.simps})]
6.83 -\<close>
6.84 -setup \<open>KEStore_Elems.add_mets
6.85 - [MethodC.prep_input @{theory} "met_diffapp_max_oninterval" [] MethodC.id_empty
6.86 - (["DiffApp", "max_on_interval_by_calculus"],
6.87 - [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"(*, "errorBound e_rr"*)]),
6.88 - ("#Find" ,["maxArgument v_0"])],
6.89 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
6.90 - errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
6.91 - @{thm refl}),
6.92 - MethodC.prep_input @{theory} "met_diffapp_findvals" [] MethodC.id_empty
6.93 - (["DiffApp", "find_values"], [],
6.94 - {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
6.95 - errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
6.96 - @{thm refl})]
6.97 -\<close>
6.98 +
6.99 +method met_diffapp_funexp : "DiffApp/make_fun_by_explicit" =
6.100 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=prog_expr,prls=Rule_Set.empty, crls = eval_rls,
6.101 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
6.102 + Program: make_fun_by_explicit.simps
6.103 + Given: "functionOf f_f" "boundVariable v_v" "equalities eqs"
6.104 + Find: "functionEq f_1"
6.105 +
6.106 +method met_diffapp_max_oninterval : "DiffApp/max_on_interval_by_calculus" =
6.107 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
6.108 + errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}\<close>
6.109 + Given: "functionEq t_t" "boundVariable v_v" "interval i_tv" (*"errorBound e_rr"*)
6.110 + Find: "maxArgument v_0"
6.111 +
6.112 +method met_diffapp_findvals : "DiffApp/find_values" =
6.113 + \<open>{rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
6.114 + errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}\<close>
6.115 +
6.116 ML \<open>
6.117 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr
6.118 [\<^rule_thm>\<open>filterVar_Const\<close>,
7.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Sat Jun 12 18:33:15 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Tue Jun 15 22:24:20 2021 +0200
7.3 @@ -30,17 +30,16 @@
7.4 (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
7.5 (Try (Calculate ''PLUS'')) #>
7.6 (Try (Calculate ''TIMES''))) e_e)"
7.7 -setup \<open>KEStore_Elems.add_mets
7.8 - [MethodC.prep_input @{theory} "met_test_diophant" [] MethodC.id_empty
7.9 - (["Test", "solve_diophant"],
7.10 - [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
7.11 - (* TODO: drop ^^^^^*)
7.12 - ("#Where" ,[]),
7.13 - ("#Find" ,["boolTestFind s_s"])],
7.14 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
7.15 - crls = tval_rls, errpats = [], nrls = Test_simplify},
7.16 - @{thm diophant_equation.simps})]
7.17 -\<close> ML \<open>
7.18 +
7.19 +method met_test_diophant : "Test/solve_diophant" =
7.20 + \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
7.21 + crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
7.22 + Program: diophant_equation.simps
7.23 + Given: "boolTestGiven e_e" "intTestGiven (v_v::int)"
7.24 +(* TODO: drop ^^^^^*)
7.25 + Where:
7.26 + Find: "boolTestFind s_s"
7.27 +ML \<open>
7.28 \<close> ML \<open>
7.29 \<close>
7.30
8.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 12 18:33:15 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Jun 15 22:24:20 2021 +0200
8.3 @@ -499,18 +499,13 @@
8.4
8.5 section \<open>Methods\<close>
8.6
8.7 -setup \<open>KEStore_Elems.add_mets
8.8 - [MethodC.prep_input @{theory} "met_eqsys" [] MethodC.id_empty
8.9 - (["EqSystem"], [],
8.10 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
8.11 - errpats = [], nrls = Rule_Set.Empty},
8.12 - @{thm refl}),
8.13 - MethodC.prep_input @{theory} "met_eqsys_topdown" [] MethodC.id_empty
8.14 - (["EqSystem", "top_down_substitution"], [],
8.15 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
8.16 - errpats = [], nrls = Rule_Set.Empty},
8.17 - @{thm refl})]
8.18 -\<close>
8.19 +method met_eqsys : "EqSystem" =
8.20 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
8.21 + errpats = [], nrls = Rule_Set.Empty}\<close>
8.22 +
8.23 +method met_eqsys_topdown : "EqSystem/top_down_substitution" =
8.24 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
8.25 + errpats = [], nrls = Rule_Set.Empty}\<close>
8.26
8.27 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
8.28 where
8.29 @@ -531,29 +526,24 @@
8.30 e__s = Take [e_1, e_2]
8.31 in
8.32 Try (Rewrite_Set ''order_system'' ) e__s) "
8.33 -setup \<open>KEStore_Elems.add_mets
8.34 - [MethodC.prep_input @{theory} "met_eqsys_topdown_2x2" [] MethodC.id_empty
8.35 - (["EqSystem", "top_down_substitution", "2x2"],
8.36 - [("#Given", ["equalities e_s", "solveForVars v_s"]),
8.37 - ("#Where",
8.38 - ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
8.39 - " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
8.40 - ("#Find" ,["solution ss'''"])],
8.41 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
8.42 - srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
8.43 - [\<^rule_thm>\<open>hd_thm\<close>,
8.44 - \<^rule_thm>\<open>tl_Cons\<close>,
8.45 - \<^rule_thm>\<open>tl_Nil\<close>],
8.46 - prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
8.47 - @{thm solve_system.simps})]
8.48 -\<close>
8.49 -setup \<open>KEStore_Elems.add_mets
8.50 - [MethodC.prep_input @{theory} "met_eqsys_norm" [] MethodC.id_empty
8.51 - (["EqSystem", "normalise"], [],
8.52 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
8.53 - errpats = [], nrls = Rule_Set.Empty},
8.54 - @{thm refl})]
8.55 -\<close>
8.56 +
8.57 +method met_eqsys_topdown_2x2 : "EqSystem/top_down_substitution/2x2" =
8.58 + \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
8.59 + srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
8.60 + [\<^rule_thm>\<open>hd_thm\<close>,
8.61 + \<^rule_thm>\<open>tl_Cons\<close>,
8.62 + \<^rule_thm>\<open>tl_Nil\<close>],
8.63 + prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
8.64 + Program: solve_system.simps
8.65 + Given: "equalities e_s" "solveForVars v_s"
8.66 + Where:
8.67 + "(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"
8.68 + " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"
8.69 + Find: "solution ss'''"
8.70 +
8.71 +method met_eqsys_norm : "EqSystem/normalise" =
8.72 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
8.73 + errpats = [], nrls = Rule_Set.Empty}\<close>
8.74
8.75 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
8.76 where
8.77 @@ -569,19 +559,17 @@
8.78 in
8.79 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
8.80 [BOOL_LIST e__s, REAL_LIST v_s])"
8.81 -setup \<open>KEStore_Elems.add_mets
8.82 - [MethodC.prep_input @{theory} "met_eqsys_norm_2x2" [] MethodC.id_empty
8.83 - (["EqSystem", "normalise", "2x2"],
8.84 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.85 - ("#Find" ,["solution ss'''"])],
8.86 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
8.87 - srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
8.88 - [\<^rule_thm>\<open>hd_thm\<close>,
8.89 - \<^rule_thm>\<open>tl_Cons\<close>,
8.90 - \<^rule_thm>\<open>tl_Nil\<close>],
8.91 - prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
8.92 - @{thm solve_system2.simps})]
8.93 -\<close>
8.94 +
8.95 +method met_eqsys_norm_2x2 : "EqSystem/normalise/2x2" =
8.96 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
8.97 + srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
8.98 + [\<^rule_thm>\<open>hd_thm\<close>,
8.99 + \<^rule_thm>\<open>tl_Cons\<close>,
8.100 + \<^rule_thm>\<open>tl_Nil\<close>],
8.101 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
8.102 + Program: solve_system2.simps
8.103 + Given: "equalities e_s" "solveForVars v_s"
8.104 + Find: "solution ss'''"
8.105
8.106 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
8.107 where
8.108 @@ -601,20 +589,17 @@
8.109 in
8.110 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
8.111 [BOOL_LIST e__s, REAL_LIST v_s])"
8.112 -setup \<open>KEStore_Elems.add_mets
8.113 - [MethodC.prep_input @{theory} "met_eqsys_norm_4x4" [] MethodC.id_empty
8.114 - (["EqSystem", "normalise", "4x4"],
8.115 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.116 - ("#Find" ,["solution ss'''"])],
8.117 - {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
8.118 - srls = Rule_Set.append_rules "srls_normalise_4x4" srls
8.119 - [\<^rule_thm>\<open>hd_thm\<close>,
8.120 - \<^rule_thm>\<open>tl_Cons\<close>,
8.121 - \<^rule_thm>\<open>tl_Nil\<close>],
8.122 - prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
8.123 - (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
8.124 - @{thm solve_system3.simps})]
8.125 -\<close>
8.126 +
8.127 +method met_eqsys_norm_4x4 : "EqSystem/normalise/4x4" =
8.128 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
8.129 + srls =
8.130 + Rule_Set.append_rules "srls_normalise_4x4" srls
8.131 + [\<^rule_thm>\<open>hd_thm\<close>, \<^rule_thm>\<open>tl_Cons\<close>, \<^rule_thm>\<open>tl_Nil\<close>],
8.132 + prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
8.133 + Program: solve_system3.simps
8.134 + Given: "equalities e_s" "solveForVars v_s"
8.135 + Find: "solution ss'''"
8.136 + (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
8.137
8.138 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
8.139 where
8.140 @@ -633,24 +618,24 @@
8.141 ) e_2
8.142 in
8.143 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
8.144 -setup \<open>KEStore_Elems.add_mets
8.145 - [MethodC.prep_input @{theory} "met_eqsys_topdown_4x4" [] MethodC.id_empty
8.146 - (["EqSystem", "top_down_substitution", "4x4"],
8.147 - [("#Given" ,["equalities e_s", "solveForVars v_s"]),
8.148 - ("#Where" , (*accepts missing variables up to diagonal form*)
8.149 - ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",
8.150 - "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
8.151 - "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
8.152 - "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
8.153 - ("#Find", ["solution ss'''"])],
8.154 - {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
8.155 - srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
8.156 - prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
8.157 - [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
8.158 - crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
8.159 - (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
8.160 - @{thm solve_system4.simps})]
8.161 -\<close> ML \<open>
8.162 +
8.163 +method met_eqsys_topdown_4x4 : "EqSystem/top_down_substitution/4x4" =
8.164 + \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
8.165 + srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
8.166 + prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
8.167 + [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")],
8.168 + crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
8.169 + (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
8.170 + Program: solve_system4.simps
8.171 + Given: "equalities e_s" "solveForVars v_s"
8.172 + Where: (*accepts missing variables up to diagonal form*)
8.173 + "(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))"
8.174 + "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))"
8.175 + "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))"
8.176 + "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
8.177 + Find: "solution ss'''"
8.178 +
8.179 +ML \<open>
8.180 \<close> ML \<open>
8.181 \<close> ML \<open>
8.182 \<close>
9.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sat Jun 12 18:33:15 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Tue Jun 15 22:24:20 2021 +0200
9.3 @@ -76,14 +76,11 @@
9.4 ((Thm.term_of o the o (TermC.parse @{theory})) "solve",
9.5 (("Isac_Knowledge", ["univariate", "equation"], ["no_met"]), argl2dtss))]\<close>
9.6
9.7 +method met_equ : "Equation" =
9.8 + \<open>{rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
9.9 + errpats = [], nrls = Rule_Set.empty}\<close>
9.10
9.11 -setup \<open>KEStore_Elems.add_mets
9.12 - [MethodC.prep_input @{theory} "met_equ" [] MethodC.id_empty
9.13 - (["Equation"], [],
9.14 - {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
9.15 - errpats = [], nrls = Rule_Set.empty},
9.16 - @{thm refl})]
9.17 -\<close> ML \<open>
9.18 +ML \<open>
9.19 \<close> ML \<open>
9.20 \<close>
9.21 end
9.22 \ No newline at end of file
10.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sat Jun 12 18:33:15 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Tue Jun 15 22:24:20 2021 +0200
10.3 @@ -84,17 +84,14 @@
10.4
10.5 section \<open>methods\<close>
10.6 (* TODO: implementation needs extra object-level lists ?!?*)
10.7 -setup \<open>KEStore_Elems.add_mets
10.8 - [ MethodC.prep_input @{theory} "met_Programming" [] MethodC.id_empty
10.9 - (["Programming"], [],
10.10 - {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.11 - crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
10.12 - MethodC.prep_input @{theory} "met_Prog_sort" [] MethodC.id_empty
10.13 - (["Programming", "SORT"], [],
10.14 - {rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.15 - crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},
10.16 - @{thm refl})]
10.17 -\<close>
10.18 +
10.19 +method met_Programming : "Programming" =
10.20 + \<open>{rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.21 + crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}\<close>
10.22 +
10.23 +method met_Prog_sort : "Programming/SORT" =
10.24 + \<open>{rew_ord'="tless_true",rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.25 + crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}\<close>
10.26
10.27 partial_function (tailrec) sort_program :: "int xlist => int xlist"
10.28 where
10.29 @@ -103,14 +100,13 @@
10.30 uns = Take (sort unso)
10.31 in
10.32 (Rewrite_Set ''ins_sort'') uns)"
10.33 -setup \<open>KEStore_Elems.add_mets
10.34 - [MethodC.prep_input @{theory} "met_Prog_sort_ins" [] MethodC.id_empty
10.35 - (["Programming", "SORT", "insertion"],
10.36 - [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
10.37 - {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.38 - crls = Atools_crls, errpats = [], nrls = norm_Rational},
10.39 - @{thm sort_program.simps})]
10.40 -\<close>
10.41 +
10.42 +method met_Prog_sort_ins : "Programming/SORT/insertion" =
10.43 + \<open>{rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.44 + crls = Atools_crls, errpats = [], nrls = norm_Rational}\<close>
10.45 + Program: sort_program.simps
10.46 + Given: "unsorted u_u"
10.47 + Find: "sorted s_s"
10.48
10.49 partial_function (tailrec) sort_program2 :: "int xlist => int xlist"
10.50 where
10.51 @@ -133,14 +129,13 @@
10.52 (Repeat (Rewrite ''if_True'')) Or
10.53 (Repeat (Rewrite ''if_False'')))
10.54 ) uns)"
10.55 -setup \<open>KEStore_Elems.add_mets
10.56 - [MethodC.prep_input @{theory} "met_Prog_sort_ins_steps" [] MethodC.id_empty
10.57 - (["Programming", "SORT", "insertion_steps"],
10.58 - [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
10.59 - {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.60 - crls = Atools_crls, errpats = [], nrls = norm_Rational},
10.61 - @{thm sort_program2.simps})]
10.62 -\<close>
10.63 +
10.64 +method met_Prog_sort_ins_steps : "Programming/SORT/insertion_steps" =
10.65 + \<open>{rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
10.66 + crls = Atools_crls, errpats = [], nrls = norm_Rational}\<close>
10.67 + Program: sort_program2.simps
10.68 + Given: "unsorted u_u"
10.69 + Find: "sorted s_s"
10.70
10.71 subsection \<open>CAS-commands\<close>
10.72 ML \<open>
11.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 12 18:33:15 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Jun 15 22:24:20 2021 +0200
11.3 @@ -346,14 +346,13 @@
11.4 t_t = Take (Integral f_f D v_v)
11.5 in
11.6 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
11.7 -setup \<open>KEStore_Elems.add_mets
11.8 - [MethodC.prep_input @{theory} "met_diffint" [] MethodC.id_empty
11.9 - (["diff", "integration"],
11.10 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
11.11 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
11.12 - crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
11.13 - @{thm integrate.simps})]
11.14 -\<close>
11.15 +
11.16 +method met_diffint : "diff/integration" =
11.17 + \<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
11.18 + crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
11.19 + Program: integrate.simps
11.20 + Given: "functionTerm f_f" "integrateBy v_v"
11.21 + Find: "antiDerivative F_F"
11.22
11.23 partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
11.24 where
11.25 @@ -364,15 +363,15 @@
11.26 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
11.27 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
11.28 ) t_t)"
11.29 -setup \<open>KEStore_Elems.add_mets
11.30 - [MethodC.prep_input @{theory} "met_diffint_named" [] MethodC.id_empty
11.31 - (["diff", "integration", "named"],
11.32 - [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
11.33 - ("#Find" ,["antiDerivativeName F_F"])],
11.34 - {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
11.35 - crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
11.36 - @{thm intergrate_named.simps})]
11.37 -\<close> ML \<open>
11.38 +
11.39 +method met_diffint_named : "diff/integration/named" =
11.40 + \<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
11.41 + crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
11.42 + Program: intergrate_named.simps
11.43 + Given: "functionTerm f_f" "integrateBy v_v"
11.44 + Find: "antiDerivativeName F_F"
11.45 +
11.46 +ML \<open>
11.47 \<close> ML \<open>
11.48 \<close>
11.49
12.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 12 18:33:15 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Jun 15 22:24:20 2021 +0200
12.3 @@ -56,16 +56,13 @@
12.4
12.5 subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
12.6
12.7 -setup \<open>KEStore_Elems.add_mets
12.8 - [MethodC.prep_input @{theory} "met_SP" [] MethodC.id_empty
12.9 - (["SignalProcessing"], [],
12.10 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
12.11 - errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
12.12 - MethodC.prep_input @{theory} "met_SP_Ztrans" [] MethodC.id_empty
12.13 - (["SignalProcessing", "Z_Transform"], [],
12.14 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
12.15 - errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
12.16 -\<close>
12.17 +method met_SP : "SignalProcessing" =
12.18 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
12.19 + errpats = [], nrls = Rule_Set.empty}\<close>
12.20 +
12.21 +method met_SP_Ztrans : "SignalProcessing/Z_Transform" =
12.22 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
12.23 + errpats = [], nrls = Rule_Set.empty}\<close>
12.24
12.25 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
12.26 where
12.27 @@ -84,15 +81,13 @@
12.28 SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''], [''Test'',''solve_linear''])
12.29 [BOOL equ, REAL X_z]
12.30 in X) "
12.31 -setup \<open>KEStore_Elems.add_mets
12.32 - [MethodC.prep_input @{theory} "met_SP_Ztrans_inv" [] MethodC.id_empty
12.33 - (["SignalProcessing", "Z_Transform", "Inverse"],
12.34 - [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
12.35 - ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
12.36 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
12.37 - errpats = [], nrls = Rule_Set.empty},
12.38 - @{thm inverse_ztransform.simps})]
12.39 -\<close>
12.40 +
12.41 +method met_SP_Ztrans_inv : "SignalProcessing/Z_Transform/Inverse" =
12.42 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
12.43 + errpats = [], nrls = Rule_Set.empty}\<close>
12.44 + Program: inverse_ztransform.simps
12.45 + Given: "filterExpression X_eq" "functionName X_z"
12.46 + Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
12.47
12.48 partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> real \<Rightarrow> bool"
12.49 where
12.50 @@ -112,33 +107,32 @@
12.51 X_zeq = Take (X_z = rhs pbz_eq);
12.52 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
12.53 in n_eq)"
12.54 -setup \<open>KEStore_Elems.add_mets
12.55 - [MethodC.prep_input @{theory} "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
12.56 - (["SignalProcessing", "Z_Transform", "Inverse_sub"],
12.57 - [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
12.58 - ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
12.59 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
12.60 - srls = Rule_Def.Repeat {id="srls_partial_fraction",
12.61 - preconds = [], rew_ord = ("termlessI",termlessI),
12.62 - erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
12.63 - [(*for asm in NTH_CONS ...*)
12.64 - \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
12.65 - (*2nd NTH_CONS pushes n+-1 into asms*)
12.66 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
12.67 - srls = Rule_Set.Empty, calc = [], errpatts = [],
12.68 - rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
12.69 - \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
12.70 - \<^rule_thm>\<open>NTH_NIL\<close>,
12.71 - \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
12.72 - \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
12.73 - \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
12.74 - \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
12.75 - \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
12.76 - \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
12.77 - ], scr = Rule.Empty_Prog},
12.78 - prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational},
12.79 - @{thm inverse_ztransform2.simps})]
12.80 -\<close>
12.81 +
12.82 +method met_SP_Ztrans_inv_sub : "SignalProcessing/Z_Transform/Inverse_sub" =
12.83 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [],
12.84 + srls = Rule_Def.Repeat {id="srls_partial_fraction",
12.85 + preconds = [], rew_ord = ("termlessI",termlessI),
12.86 + erls = Rule_Set.append_rules "erls_in_srls_partial_fraction" Rule_Set.empty
12.87 + [(*for asm in NTH_CONS ...*)
12.88 + \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
12.89 + (*2nd NTH_CONS pushes n+-1 into asms*)
12.90 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
12.91 + srls = Rule_Set.Empty, calc = [], errpatts = [],
12.92 + rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
12.93 + \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
12.94 + \<^rule_thm>\<open>NTH_NIL\<close>,
12.95 + \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
12.96 + \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
12.97 + \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
12.98 + \<^rule_eval>\<open>get_denominator\<close> (eval_get_denominator "#get_denominator"),
12.99 + \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
12.100 + \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")
12.101 + ], scr = Rule.Empty_Prog},
12.102 + prls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], nrls = norm_Rational}\<close>
12.103 + Program: inverse_ztransform2.simps
12.104 + Given: "filterExpression X_eq" "functionName X_z"
12.105 + Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
12.106 +
12.107 ML \<open>
12.108 \<close> ML \<open>
12.109 \<close> ML \<open>
13.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sat Jun 12 18:33:15 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Jun 15 22:24:20 2021 +0200
13.3 @@ -121,13 +121,9 @@
13.4 LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))]\<close>
13.5
13.6 (*-------------- methods------------------------------------------------------*)
13.7 -setup \<open>KEStore_Elems.add_mets
13.8 - [MethodC.prep_input @{theory} "met_eqlin" [] MethodC.id_empty
13.9 - (["LinEq"], [],
13.10 - {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
13.11 - crls = LinEq_crls, errpats = [], nrls = norm_Poly},
13.12 - @{thm refl})]
13.13 -\<close>
13.14 +method met_eqlin : "LinEq" =
13.15 + \<open>{rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
13.16 + crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
13.17 (* ansprechen mit ["LinEq", "solve_univar_equation"] *)
13.18
13.19 partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
13.20 @@ -145,16 +141,15 @@
13.21 (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
13.22 in
13.23 Or_to_List e_e)"
13.24 -setup \<open>KEStore_Elems.add_mets
13.25 - [MethodC.prep_input @{theory} "met_eq_lin" [] MethodC.id_empty
13.26 - (["LinEq", "solve_lineq_equation"],
13.27 - [("#Given", ["equality e_e", "solveFor v_v"]),
13.28 - ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]),
13.29 - ("#Find", ["solutions v_v'i'"])],
13.30 - {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
13.31 - crls = LinEq_crls, errpats = [], nrls = norm_Poly},
13.32 - @{thm solve_linear_equation.simps})]
13.33 -\<close>
13.34 +
13.35 +method met_eq_lin : "LinEq/solve_lineq_equation" =
13.36 + \<open>{rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
13.37 + crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
13.38 + Program: solve_linear_equation.simps
13.39 + Given: "equality e_e" "solveFor v_v"
13.40 + Where: "Not ((lhs e_e) is_polyrat_in v_v)" "((lhs e_e) has_degree_in v_v) = 1"
13.41 + Find: "solutions v_v'i'"
13.42 +
13.43 ML \<open>
13.44 MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];
13.45 \<close> ML \<open>
14.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Sat Jun 12 18:33:15 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Jun 15 22:24:20 2021 +0200
14.3 @@ -39,16 +39,16 @@
14.4 (Rewrite_Set ''norm_Poly'') ) e_e
14.5 in
14.6 [e_e])"
14.7 -setup \<open>KEStore_Elems.add_mets
14.8 - [MethodC.prep_input @{theory} "met_equ_log" [] MethodC.id_empty
14.9 - (["Equation", "solve_log"],
14.10 - [("#Given" ,["equality e_e", "solveFor v_v"]),
14.11 - ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
14.12 - ("#Find" ,["solutions v_v'i'"])],
14.13 - {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule_Set.empty, prls = PolyEq_prls, calc = [],
14.14 - crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
14.15 - @{thm solve_log.simps})]
14.16 -\<close> ML \<open>
14.17 +
14.18 +method met_equ_log : "Equation/solve_log" =
14.19 + \<open>{rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule_Set.empty, prls = PolyEq_prls, calc = [],
14.20 + crls = PolyEq_crls, errpats = [], nrls = norm_Rational}\<close>
14.21 + Program: solve_log.simps
14.22 + Given: "equality e_e" "solveFor v_v"
14.23 + Where: "matches ((?a log ?v_v) = ?b) e_e"
14.24 + Find: "solutions v_v'i'"
14.25 +
14.26 +ML \<open>
14.27 \<close> ML \<open>
14.28 \<close>
14.29 end
14.30 \ No newline at end of file
15.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 12 18:33:15 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Jun 15 22:24:20 2021 +0200
15.3 @@ -227,19 +227,18 @@
15.4 pbz = Take eqr; \<comment> \<open>([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
15.5 pbz = Substitute [AA = a, BB = b] pbz \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
15.6 in pbz) "
15.7 -setup \<open>KEStore_Elems.add_mets
15.8 - [MethodC.prep_input @{theory} "met_partial_fraction" [] MethodC.id_empty
15.9 - (["simplification", "of_rationals", "to_partial_fraction"],
15.10 - [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
15.11 - (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) <
15.12 - ((get_denominator t_t) has_degree_in v_v)"]), TODO*)
15.13 - ("#Find" ,["decomposedFunction p_p'''"])],
15.14 - (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
15.15 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = srls_partial_fraction, prls = Rule_Set.empty,
15.16 - crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty},
15.17 - (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
15.18 - @{thm partial_fraction.simps})]
15.19 -\<close>
15.20 +
15.21 +method met_partial_fraction : "simplification/of_rationals/to_partial_fraction" =
15.22 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = srls_partial_fraction, prls = Rule_Set.empty,
15.23 + crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.empty}\<close>
15.24 + (*f_f = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
15.25 + (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
15.26 + Program: partial_fraction.simps
15.27 + Given: "functionTerm t_t" "solveFor v_v"
15.28 + (* Where: "((get_numerator t_t) has_degree_in v_v) <
15.29 + ((get_denominator t_t) has_degree_in v_v)" TODO *)
15.30 + Find: "decomposedFunction p_p'''"
15.31 +
15.32 ML \<open>
15.33 (*
15.34 val fmz =
16.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 12 18:33:15 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Jun 15 22:24:20 2021 +0200
16.3 @@ -1413,19 +1413,17 @@
16.4 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
16.5 where
16.6 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
16.7 -setup \<open>KEStore_Elems.add_mets
16.8 - [MethodC.prep_input @{theory} "met_simp_poly" [] MethodC.id_empty
16.9 - (["simplification", "for_polynomials"],
16.10 - [("#Given" ,["Term t_t"]),
16.11 - ("#Where" ,["t_t is_polyexp"]),
16.12 - ("#Find" ,["normalform n_n"])],
16.13 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.14 - prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
16.15 - [(*for preds in where_*)
16.16 - \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
16.17 - crls = Rule_Set.empty, errpats = [], nrls = norm_Poly},
16.18 - @{thm simplify.simps})]
16.19 -\<close>
16.20 +
16.21 +method met_simp_poly : "simplification/for_polynomials" =
16.22 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
16.23 + prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
16.24 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
16.25 + crls = Rule_Set.empty, errpats = [], nrls = norm_Poly}\<close>
16.26 + Program: simplify.simps
16.27 + Given: "Term t_t"
16.28 + Where: "t_t is_polyexp"
16.29 + Find: "normalform n_n"
16.30 +
16.31 ML \<open>
16.32 \<close> ML \<open>
16.33 \<close>
17.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 12 18:33:15 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Jun 15 22:24:20 2021 +0200
17.3 @@ -888,13 +888,10 @@
17.4 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "complete_square"]]))]\<close>
17.5
17.6 text \<open>"-------------------------methods-----------------------"\<close>
17.7 -setup \<open>KEStore_Elems.add_mets
17.8 - [MethodC.prep_input @{theory} "met_polyeq" [] MethodC.id_empty
17.9 - (["PolyEq"], [],
17.10 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
17.11 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.12 - @{thm refl})]
17.13 -\<close>
17.14 +
17.15 +method met_polyeq : "PolyEq" =
17.16 + \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
17.17 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational}\<close>
17.18
17.19 partial_function (tailrec) normalize_poly_eq :: "bool \<Rightarrow> real \<Rightarrow> bool"
17.20 where
17.21 @@ -909,16 +906,14 @@
17.22 in
17.23 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
17.24 [BOOL e_e, REAL v_v])"
17.25 -setup \<open>KEStore_Elems.add_mets
17.26 - [MethodC.prep_input @{theory} "met_polyeq_norm" [] MethodC.id_empty
17.27 - (["PolyEq", "normalise_poly"],
17.28 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.29 - ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
17.30 - ("#Find" ,["solutions v_v'i'"])],
17.31 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, calc=[],
17.32 - crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
17.33 - @{thm normalize_poly_eq.simps})]
17.34 -\<close>
17.35 +
17.36 +method met_polyeq_norm : "PolyEq/normalise_poly" =
17.37 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, calc=[],
17.38 + crls=PolyEq_crls, errpats = [], nrls = norm_Rational}\<close>
17.39 + Program: normalize_poly_eq.simps
17.40 + Given: "equality e_e" "solveFor v_v"
17.41 + Where: "(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"
17.42 + Find: "solutions v_v'i'"
17.43
17.44 partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.45 where
17.46 @@ -927,17 +922,15 @@
17.47 e_e = (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d0_polyeq_simplify'')) e_e
17.48 in
17.49 Or_to_List e_e)"
17.50 -setup \<open>KEStore_Elems.add_mets
17.51 - [MethodC.prep_input @{theory} "met_polyeq_d0" [] MethodC.id_empty
17.52 - (["PolyEq", "solve_d0_polyeq_equation"],
17.53 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.54 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
17.55 - ("#Find" ,["solutions v_v'i'"])],
17.56 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.57 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.58 - nrls = norm_Rational},
17.59 - @{thm solve_poly_equ.simps})]
17.60 -\<close>
17.61 +
17.62 +method met_polyeq_d0 : "PolyEq/solve_d0_polyeq_equation" =
17.63 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.64 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.65 + nrls = norm_Rational}\<close>
17.66 + Program: solve_poly_equ.simps
17.67 + Given: "equality e_e" "solveFor v_v"
17.68 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 0"
17.69 + Find: "solutions v_v'i'"
17.70
17.71 partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.72 where
17.73 @@ -950,17 +943,15 @@
17.74 L_L = Or_to_List e_e
17.75 in
17.76 Check_elementwise L_L {(v_v::real). Assumptions})"
17.77 -setup \<open>KEStore_Elems.add_mets
17.78 - [MethodC.prep_input @{theory} "met_polyeq_d1" [] MethodC.id_empty
17.79 - (["PolyEq", "solve_d1_polyeq_equation"],
17.80 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.81 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
17.82 - ("#Find" ,["solutions v_v'i'"])],
17.83 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.84 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.85 - nrls = norm_Rational},
17.86 - @{thm solve_poly_eq1.simps})]
17.87 -\<close>
17.88 +
17.89 +method met_polyeq_d1 : "PolyEq/solve_d1_polyeq_equation" =
17.90 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.91 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.92 + nrls = norm_Rational}\<close>
17.93 + Program: solve_poly_eq1.simps
17.94 + Given: "equality e_e" "solveFor v_v"
17.95 + Where: "(lhs e_e) is_poly_in v_v" "((lhs e_e) has_degree_in v_v) = 1"
17.96 + Find: "solutions v_v'i'"
17.97
17.98 partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.99 where
17.100 @@ -975,17 +966,15 @@
17.101 L_L = Or_to_List e_e
17.102 in
17.103 Check_elementwise L_L {(v_v::real). Assumptions})"
17.104 -setup \<open>KEStore_Elems.add_mets
17.105 - [MethodC.prep_input @{theory} "met_polyeq_d22" [] MethodC.id_empty
17.106 - (["PolyEq", "solve_d2_polyeq_equation"],
17.107 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.108 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.109 - ("#Find" ,["solutions v_v'i'"])],
17.110 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.111 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.112 - nrls = norm_Rational},
17.113 - @{thm solve_poly_equ2.simps})]
17.114 -\<close>
17.115 +
17.116 +method met_polyeq_d22 : "PolyEq/solve_d2_polyeq_equation" =
17.117 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.118 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.119 + nrls = norm_Rational}\<close>
17.120 + Program: solve_poly_equ2.simps
17.121 + Given: "equality e_e" "solveFor v_v"
17.122 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
17.123 + Find: "solutions v_v'i'"
17.124
17.125 partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.126 where
17.127 @@ -1000,17 +989,15 @@
17.128 L_L = Or_to_List e_e
17.129 in
17.130 Check_elementwise L_L {(v_v::real). Assumptions})"
17.131 -setup \<open>KEStore_Elems.add_mets
17.132 - [MethodC.prep_input @{theory} "met_polyeq_d2_bdvonly" [] MethodC.id_empty
17.133 - (["PolyEq", "solve_d2_polyeq_bdvonly_equation"],
17.134 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.135 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.136 - ("#Find" ,["solutions v_v'i'"])],
17.137 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.138 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.139 - nrls = norm_Rational},
17.140 - @{thm solve_poly_equ0.simps})]
17.141 -\<close>
17.142 +
17.143 +method met_polyeq_d2_bdvonly : "PolyEq/solve_d2_polyeq_bdvonly_equation" =
17.144 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.145 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.146 + nrls = norm_Rational}\<close>
17.147 + Program: solve_poly_equ0.simps
17.148 + Given: "equality e_e" "solveFor v_v"
17.149 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
17.150 + Find: "solutions v_v'i'"
17.151
17.152 partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.153 where
17.154 @@ -1023,17 +1010,15 @@
17.155 L_L = Or_to_List e_e
17.156 in
17.157 Check_elementwise L_L {(v_v::real). Assumptions})"
17.158 -setup \<open>KEStore_Elems.add_mets
17.159 - [MethodC.prep_input @{theory} "met_polyeq_d2_sqonly" [] MethodC.id_empty
17.160 - (["PolyEq", "solve_d2_polyeq_sqonly_equation"],
17.161 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.162 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.163 - ("#Find" ,["solutions v_v'i'"])],
17.164 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.165 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.166 - nrls = norm_Rational},
17.167 - @{thm solve_poly_equ_sqrt.simps})]
17.168 -\<close>
17.169 +
17.170 +method met_polyeq_d2_sqonly : "PolyEq/solve_d2_polyeq_sqonly_equation" =
17.171 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.172 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.173 + nrls = norm_Rational}\<close>
17.174 + Program: solve_poly_equ_sqrt.simps
17.175 + Given: "equality e_e" "solveFor v_v"
17.176 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
17.177 + Find: "solutions v_v'i'"
17.178
17.179 partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.180 where
17.181 @@ -1046,17 +1031,15 @@
17.182 L_L = Or_to_List e_e
17.183 in
17.184 Check_elementwise L_L {(v_v::real). Assumptions})"
17.185 -setup \<open>KEStore_Elems.add_mets
17.186 - [MethodC.prep_input @{theory} "met_polyeq_d2_pq" [] MethodC.id_empty
17.187 - (["PolyEq", "solve_d2_polyeq_pq_equation"],
17.188 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.189 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.190 - ("#Find" ,["solutions v_v'i'"])],
17.191 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.192 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.193 - nrls = norm_Rational},
17.194 - @{thm solve_poly_equ_pq.simps})]
17.195 -\<close>
17.196 +
17.197 +method met_polyeq_d2_pq : "PolyEq/solve_d2_polyeq_pq_equation" =
17.198 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.199 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.200 + nrls = norm_Rational}\<close>
17.201 + Program: solve_poly_equ_pq.simps
17.202 + Given: "equality e_e" "solveFor v_v"
17.203 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
17.204 + Find: "solutions v_v'i'"
17.205
17.206 partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.207 where
17.208 @@ -1068,17 +1051,15 @@
17.209 (Try (Rewrite_Set ''norm_Rational_parenthesized'')) ) e_e;
17.210 L_L = Or_to_List e_e
17.211 in Check_elementwise L_L {(v_v::real). Assumptions})"
17.212 -setup \<open>KEStore_Elems.add_mets
17.213 - [MethodC.prep_input @{theory} "met_polyeq_d2_abc" [] MethodC.id_empty
17.214 - (["PolyEq", "solve_d2_polyeq_abc_equation"],
17.215 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.216 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
17.217 - ("#Find" ,["solutions v_v'i'"])],
17.218 - {rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule_Set.empty, prls=PolyEq_prls,
17.219 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.220 - nrls = norm_Rational},
17.221 - @{thm solve_poly_equ_abc.simps})]
17.222 -\<close>
17.223 +
17.224 +method met_polyeq_d2_abc : "PolyEq/solve_d2_polyeq_abc_equation" =
17.225 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule_Set.empty, prls=PolyEq_prls,
17.226 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.227 + nrls = norm_Rational}\<close>
17.228 + Program: solve_poly_equ_abc.simps
17.229 + Given: "equality e_e" "solveFor v_v"
17.230 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2"
17.231 + Find: "solutions v_v'i'"
17.232
17.233 partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.234 where
17.235 @@ -1095,18 +1076,17 @@
17.236 L_L = Or_to_List e_e
17.237 in
17.238 Check_elementwise L_L {(v_v::real). Assumptions})"
17.239 -setup \<open>KEStore_Elems.add_mets
17.240 - [MethodC.prep_input @{theory} "met_polyeq_d3" [] MethodC.id_empty
17.241 - (["PolyEq", "solve_d3_polyeq_equation"],
17.242 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.243 - ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
17.244 - ("#Find" ,["solutions v_v'i'"])],
17.245 - {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.246 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.247 - nrls = norm_Rational},
17.248 - @{thm solve_poly_equ3.simps})]
17.249 -\<close>
17.250 - (*.solves all expanded (ie. normalised) terms of degree 2.*)
17.251 +
17.252 +method met_polyeq_d3 : "PolyEq/solve_d3_polyeq_equation" =
17.253 + \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls,
17.254 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.255 + nrls = norm_Rational}\<close>
17.256 + Program: solve_poly_equ3.simps
17.257 + Given: "equality e_e" "solveFor v_v"
17.258 + Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 3"
17.259 + Find: "solutions v_v'i'"
17.260 +
17.261 + (*.solves all expanded (ie. normalised) terms of degree 2.*)
17.262 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
17.263 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
17.264 partial_function (tailrec) solve_by_completing_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
17.265 @@ -1125,17 +1105,15 @@
17.266 (Try (Repeat (Calculate ''SQRT'')))) e_e
17.267 in
17.268 Or_to_List e_e)"
17.269 -setup \<open>KEStore_Elems.add_mets
17.270 - [MethodC.prep_input @{theory} "met_polyeq_complsq" [] MethodC.id_empty
17.271 - (["PolyEq", "complete_square"],
17.272 - [("#Given" ,["equality e_e", "solveFor v_v"]),
17.273 - ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
17.274 - ("#Find" ,["solutions v_v'i'"])],
17.275 - {rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule_Set.empty,prls=PolyEq_prls,
17.276 - calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.277 - nrls = norm_Rational},
17.278 - @{thm solve_by_completing_square.simps})]
17.279 -\<close>
17.280 +
17.281 +method met_polyeq_complsq : "PolyEq/complete_square" =
17.282 + \<open>{rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule_Set.empty,prls=PolyEq_prls,
17.283 + calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
17.284 + nrls = norm_Rational}\<close>
17.285 + Program: solve_by_completing_square.simps
17.286 + Given: "equality e_e" "solveFor v_v"
17.287 + Where: "matches (?a = 0) e_e" "((lhs e_e) has_degree_in v_v) = 2"
17.288 + Find: "solutions v_v'i'"
17.289
17.290 ML\<open>
17.291
18.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sat Jun 12 18:33:15 2021 +0200
18.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Jun 15 22:24:20 2021 +0200
18.3 @@ -474,31 +474,31 @@
18.4 (Try (Rewrite_Set ''fasse_zusammen'')) #>
18.5 (Try (Rewrite_Set ''verschoenere'')))
18.6 ) t_t)"
18.7 -setup \<open>KEStore_Elems.add_mets
18.8 - [MethodC.prep_input @{theory} "met_simp_poly_minus" [] MethodC.id_empty
18.9 - (["simplification", "for_polynomials", "with_minus"],
18.10 - [("#Given" ,["Term t_t"]),
18.11 - ("#Where" ,["t_t is_polyexp",
18.12 - "Not (matchsub (?a + (?b + ?c)) t_t | " ^
18.13 - " matchsub (?a + (?b - ?c)) t_t | " ^
18.14 - " matchsub (?a - (?b + ?c)) t_t | " ^
18.15 - " matchsub (?a + (?b - ?c)) t_t )"]),
18.16 - ("#Find" ,["normalform n_n"])],
18.17 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.18 - prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
18.19 - [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
18.20 - \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
18.21 - \<^rule_thm>\<open>and_true\<close>,
18.22 - (*"(?a & True) = ?a"*)
18.23 - \<^rule_thm>\<open>and_false\<close>,
18.24 - (*"(?a & False) = False"*)
18.25 - \<^rule_thm>\<open>not_true\<close>,
18.26 - (*"(~ True) = False"*)
18.27 - \<^rule_thm>\<open>not_false\<close>
18.28 - (*"(~ False) = True"*)],
18.29 - crls = Rule_Set.empty, errpats = [], nrls = rls_p_33},
18.30 - @{thm simplify.simps})]
18.31 -\<close>
18.32 +
18.33 +method met_simp_poly_minus : "simplification/for_polynomials/with_minus" =
18.34 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.35 + prls =
18.36 + Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
18.37 + [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
18.38 + \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
18.39 + \<^rule_thm>\<open>and_true\<close>,
18.40 + (*"(?a & True) = ?a"*)
18.41 + \<^rule_thm>\<open>and_false\<close>,
18.42 + (*"(?a & False) = False"*)
18.43 + \<^rule_thm>\<open>not_true\<close>,
18.44 + (*"(~ True) = False"*)
18.45 + \<^rule_thm>\<open>not_false\<close>
18.46 + (*"(~ False) = True"*)],
18.47 + crls = Rule_Set.empty, errpats = [], nrls = rls_p_33}\<close>
18.48 + Program: simplify.simps
18.49 + Given: "Term t_t"
18.50 + Where:
18.51 + "t_t is_polyexp"
18.52 + "Not (matchsub (?a + (?b + ?c)) t_t |
18.53 + matchsub (?a + (?b - ?c)) t_t |
18.54 + matchsub (?a - (?b + ?c)) t_t |
18.55 + matchsub (?a + (?b - ?c)) t_t)"
18.56 + Find: "normalform n_n"
18.57
18.58 partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
18.59 where
18.60 @@ -509,18 +509,16 @@
18.61 (Try (Rewrite_Set ''fasse_zusammen'')) #>
18.62 (Try (Rewrite_Set ''verschoenere'')))
18.63 ) t_t)"
18.64 -setup \<open>KEStore_Elems.add_mets
18.65 - [MethodC.prep_input @{theory} "met_simp_poly_parenth" [] MethodC.id_empty
18.66 - (["simplification", "for_polynomials", "with_parentheses"],
18.67 - [("#Given" ,["Term t_t"]),
18.68 - ("#Where" ,["t_t is_polyexp"]),
18.69 - ("#Find" ,["normalform n_n"])],
18.70 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.71 - prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
18.72 - [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
18.73 - crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
18.74 - @{thm simplify2.simps})]
18.75 -\<close>
18.76 +
18.77 +method met_simp_poly_parenth : "simplification/for_polynomials/with_parentheses" =
18.78 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.79 + prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
18.80 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
18.81 + crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
18.82 + Program: simplify2.simps
18.83 + Given: "Term t_t"
18.84 + Where: "t_t is_polyexp"
18.85 + Find: "normalform n_n"
18.86
18.87 partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
18.88 where
18.89 @@ -534,23 +532,20 @@
18.90 (Try (Rewrite_Set ''fasse_zusammen'')) #>
18.91 (Try (Rewrite_Set ''verschoenere'')))
18.92 ) t_t)"
18.93 -setup \<open>KEStore_Elems.add_mets
18.94 - [MethodC.prep_input @{theory} "met_simp_poly_parenth_mult" [] MethodC.id_empty
18.95 - (["simplification", "for_polynomials", "with_parentheses_mult"],
18.96 - [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
18.97 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.98 - prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
18.99 - [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
18.100 - crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
18.101 - @{thm simplify3.simps})]
18.102 -\<close>
18.103 -setup \<open>KEStore_Elems.add_mets
18.104 - [MethodC.prep_input @{theory} "met_probe" [] MethodC.id_empty
18.105 - (["probe"], [],
18.106 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
18.107 - errpats = [], nrls = Rule_Set.Empty},
18.108 - @{thm refl})]
18.109 -\<close>
18.110 +
18.111 +method met_simp_poly_parenth_mult : "simplification/for_polynomials/with_parentheses_mult" =
18.112 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.113 + prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
18.114 + [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
18.115 + crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
18.116 + Program: simplify3.simps
18.117 + Given: "Term t_t"
18.118 + Where: "t_t is_polyexp"
18.119 + Find: "normalform n_n"
18.120 +
18.121 +method met_probe : "probe" =
18.122 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
18.123 + errpats = [], nrls = Rule_Set.Empty}\<close>
18.124
18.125 partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
18.126 where
18.127 @@ -564,30 +559,27 @@
18.128 (Try (Repeat (Calculate ''PLUS'' ))) #>
18.129 (Try (Repeat (Calculate ''MINUS''))))
18.130 ) e_e)"
18.131 -setup \<open>KEStore_Elems.add_mets
18.132 - [MethodC.prep_input @{theory} "met_probe_poly" [] MethodC.id_empty
18.133 - (["probe", "fuer_polynom"],
18.134 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.135 - ("#Where" ,["e_e is_polyexp"]),
18.136 - ("#Find" ,["Geprueft p_p"])],
18.137 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.138 - prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
18.139 - [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
18.140 - crls = Rule_Set.empty, errpats = [], nrls = rechnen},
18.141 - @{thm mache_probe.simps})]
18.142 -\<close>
18.143 -setup \<open>KEStore_Elems.add_mets
18.144 - [MethodC.prep_input @{theory} "met_probe_bruch" [] MethodC.id_empty
18.145 - (["probe", "fuer_bruch"],
18.146 - [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
18.147 - ("#Where" ,["e_e is_ratpolyexp"]),
18.148 - ("#Find" ,["Geprueft p_p"])],
18.149 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.150 - prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
18.151 - [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
18.152 - crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty},
18.153 - @{thm refl})]
18.154 -\<close> ML \<open>
18.155 +
18.156 +method met_probe_poly : "probe/fuer_polynom" =
18.157 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.158 + prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
18.159 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
18.160 + crls = Rule_Set.empty, errpats = [], nrls = rechnen}\<close>
18.161 + Program: mache_probe.simps
18.162 + Given: "Pruefe e_e" "mitWert w_w"
18.163 + Where: "e_e is_polyexp"
18.164 + Find: "Geprueft p_p"
18.165 +
18.166 +method met_probe_bruch : "probe/fuer_bruch" =
18.167 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
18.168 + prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
18.169 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
18.170 + crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}\<close>
18.171 + Given: "Pruefe e_e" "mitWert w_w"
18.172 + Where: "e_e is_ratpolyexp"
18.173 + Find: "Geprueft p_p"
18.174 +
18.175 +ML \<open>
18.176 \<close> ML \<open>
18.177 \<close>
18.178
19.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Jun 12 18:33:15 2021 +0200
19.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Jun 15 22:24:20 2021 +0200
19.3 @@ -167,11 +167,10 @@
19.4 RatEq_prls, SOME "solve (e_e::bool, v_v)", [["RatEq", "solve_rat_equation"]]))]\<close>
19.5
19.6 subsection \<open>methods\<close>
19.7 -setup \<open>KEStore_Elems.add_mets
19.8 - [MethodC.prep_input @{theory} "met_rateq" [] MethodC.id_empty
19.9 - (["RatEq"], [],
19.10 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
19.11 - crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>
19.12 +
19.13 +method met_rateq : "RatEq" =
19.14 + \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
19.15 + crls=RatEq_crls, errpats = [], nrls = norm_Rational}\<close>
19.16
19.17 partial_function (tailrec) solve_rational_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
19.18 where
19.19 @@ -185,16 +184,15 @@
19.20 L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v]
19.21 in
19.22 Check_elementwise L_L {(v_v::real). Assumptions})"
19.23 -setup \<open>KEStore_Elems.add_mets
19.24 - [MethodC.prep_input @{theory} "met_rat_eq" [] MethodC.id_empty
19.25 - (["RatEq", "solve_rat_equation"],
19.26 - [("#Given" ,["equality e_e", "solveFor v_v"]),
19.27 - ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
19.28 - ("#Find" ,["solutions v_v'i'"])],
19.29 - {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule_Set.empty, prls=RatEq_prls, calc=[],
19.30 - crls=RatEq_crls, errpats = [], nrls = norm_Rational},
19.31 - @{thm solve_rational_equ.simps})]
19.32 -\<close>
19.33 +
19.34 +method met_rat_eq : "RatEq/solve_rat_equation" =
19.35 + \<open>{rew_ord'="termlessI", rls'=rateq_erls, srls=Rule_Set.empty, prls=RatEq_prls, calc=[],
19.36 + crls=RatEq_crls, errpats = [], nrls = norm_Rational}\<close>
19.37 + Program: solve_rational_equ.simps
19.38 + Given: "equality e_e" "solveFor v_v"
19.39 + Where: "(e_e::bool) is_ratequation_in (v_v::real)"
19.40 + Find: "solutions v_v'i'"
19.41 +
19.42 ML \<open>
19.43 \<close> ML \<open>
19.44 \<close> ML \<open>
20.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jun 12 18:33:15 2021 +0200
20.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Jun 15 22:24:20 2021 +0200
20.3 @@ -903,18 +903,18 @@
20.4 Try (Rewrite_Set ''rat_reduce_1''))) #>
20.5 Try (Rewrite_Set ''discard_parentheses1''))
20.6 term)"
20.7 -setup \<open>KEStore_Elems.add_mets
20.8 - [MethodC.prep_input @{theory} "met_simp_rat" [] MethodC.id_empty
20.9 - (["simplification", "of_rationals"],
20.10 - [("#Given" ,["Term t_t"]),
20.11 - ("#Where" ,["t_t is_ratpolyexp"]),
20.12 - ("#Find" ,["normalform n_n"])],
20.13 - {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
20.14 - prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
20.15 - [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
20.16 - crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
20.17 - @{thm simplify.simps})]
20.18 -\<close> ML \<open>
20.19 +
20.20 +
20.21 +method met_simp_rat : "simplification/of_rationals" =
20.22 + \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
20.23 + prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
20.24 + [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
20.25 + crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}\<close>
20.26 + Program: simplify.simps
20.27 + Given: "Term t_t"
20.28 + Where: "t_t is_ratpolyexp"
20.29 + Find: "normalform n_n"
20.30 +ML \<open>
20.31 \<close> ML \<open>
20.32 \<close>
20.33 end
21.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 12 18:33:15 2021 +0200
21.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Jun 15 22:24:20 2021 +0200
21.3 @@ -455,12 +455,11 @@
21.4 (*Ambiguous input produces 5 parse trees -----------------------------------------------------//*)
21.5
21.6 subsection \<open>methods\<close>
21.7 -setup \<open>KEStore_Elems.add_mets
21.8 - [MethodC.prep_input @{theory} "met_rooteq" [] MethodC.id_empty
21.9 - (["RootEq"], [],
21.10 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
21.11 - crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
21.12 -\<close>
21.13 +
21.14 +method met_rooteq : "RootEq" =
21.15 + \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
21.16 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
21.17 +
21.18 (*-- normalise 20.10.02 --*)
21.19 partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
21.20 where
21.21 @@ -476,19 +475,17 @@
21.22 in
21.23 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
21.24 [BOOL e_e, REAL v_v])"
21.25 -setup \<open>KEStore_Elems.add_mets
21.26 - [MethodC.prep_input @{theory} "met_rooteq_norm" [] MethodC.id_empty
21.27 - (["RootEq", "norm_sq_root_equation"],
21.28 - [("#Given" ,["equality e_e", "solveFor v_v"]),
21.29 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.30 - " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
21.31 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
21.32 - " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.33 - ("#Find" ,["solutions v_v'i'"])],
21.34 - {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
21.35 - crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.36 - @{thm norm_sqrt_equ.simps})]
21.37 -\<close>
21.38 +
21.39 +method met_rooteq_norm : "RootEq/norm_sq_root_equation" =
21.40 + \<open>{rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
21.41 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
21.42 + Program: norm_sqrt_equ.simps
21.43 + Given: "equality e_e" "solveFor v_v"
21.44 + Where: "( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &
21.45 + Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
21.46 + ( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &
21.47 + Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
21.48 + Find: "solutions v_v'i'"
21.49
21.50 partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
21.51 where
21.52 @@ -509,19 +506,18 @@
21.53 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
21.54 [BOOL e_e, REAL v_v])
21.55 in Check_elementwise L_L {(v_v::real). Assumptions})"
21.56 -setup \<open>KEStore_Elems.add_mets
21.57 - [MethodC.prep_input @{theory} "met_rooteq_sq" [] MethodC.id_empty
21.58 - (["RootEq", "solve_sq_root_equation"],
21.59 - [("#Given" ,["equality e_e", "solveFor v_v"]),
21.60 - ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
21.61 - " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
21.62 - "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
21.63 - " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
21.64 - ("#Find" ,["solutions v_v'i'"])],
21.65 - {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
21.66 - crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.67 - @{thm solve_sqrt_equ.simps})]
21.68 -\<close>
21.69 +
21.70 +method met_rooteq_sq : "RootEq/solve_sq_root_equation" =
21.71 + \<open>{rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls, prls = RootEq_prls, calc = [],
21.72 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
21.73 + Program: solve_sqrt_equ.simps
21.74 + Given: "equality e_e" "solveFor v_v"
21.75 + Where: "(((lhs e_e) is_sqrtTerm_in (v_v::real)) &
21.76 + ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |
21.77 + (((rhs e_e) is_sqrtTerm_in (v_v::real)) &
21.78 + ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"
21.79 + Find: "solutions v_v'i'"
21.80 +
21.81 (*-- right 28.08.02 --*)
21.82 partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
21.83 where
21.84 @@ -541,16 +537,15 @@
21.85 else
21.86 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
21.87 [BOOL e_e, REAL v_v])"
21.88 -setup \<open>KEStore_Elems.add_mets
21.89 - [MethodC.prep_input @{theory} "met_rooteq_sq_right" [] MethodC.id_empty
21.90 - (["RootEq", "solve_right_sq_root_equation"],
21.91 - [("#Given" ,["equality e_e", "solveFor v_v"]),
21.92 - ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
21.93 - ("#Find" ,["solutions v_v'i'"])],
21.94 - {rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [],
21.95 - crls = RootEq_crls, errpats = [], nrls = norm_Poly},
21.96 - @{thm solve_sqrt_equ_right.simps})]
21.97 -\<close>
21.98 +
21.99 +method met_rooteq_sq_right : "RootEq/solve_right_sq_root_equation" =
21.100 + \<open>{rew_ord' = "termlessI", rls' = RootEq_erls, srls = Rule_Set.empty, prls = RootEq_prls, calc = [],
21.101 + crls = RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
21.102 + Program: solve_sqrt_equ_right.simps
21.103 + Given: "equality e_e" "solveFor v_v"
21.104 + Where: "(rhs e_e) is_sqrtTerm_in v_v"
21.105 + Find: "solutions v_v'i'"
21.106 +
21.107 (*-- left 28.08.02 --*)
21.108 partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
21.109 where
21.110 @@ -570,16 +565,15 @@
21.111 else
21.112 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
21.113 [BOOL e_e, REAL v_v])"
21.114 -setup \<open>KEStore_Elems.add_mets
21.115 - [MethodC.prep_input @{theory} "met_rooteq_sq_left" [] MethodC.id_empty
21.116 - (["RootEq", "solve_left_sq_root_equation"],
21.117 - [("#Given" ,["equality e_e", "solveFor v_v"]),
21.118 - ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
21.119 - ("#Find" ,["solutions v_v'i'"])],
21.120 - {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
21.121 - crls=RootEq_crls, errpats = [], nrls = norm_Poly},
21.122 - @{thm solve_sqrt_equ_left.simps})]
21.123 -\<close>
21.124 +
21.125 +method met_rooteq_sq_left : "RootEq/solve_left_sq_root_equation" =
21.126 + \<open>{rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule_Set.empty, prls=RootEq_prls, calc=[],
21.127 + crls=RootEq_crls, errpats = [], nrls = norm_Poly}\<close>
21.128 + Program: solve_sqrt_equ_left.simps
21.129 + Given: "equality e_e" "solveFor v_v"
21.130 + Where: "(lhs e_e) is_sqrtTerm_in v_v"
21.131 + Find: "solutions v_v'i'"
21.132 +
21.133 ML \<open>
21.134 \<close> ML \<open>
21.135 \<close>
22.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jun 12 18:33:15 2021 +0200
22.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Jun 15 22:24:20 2021 +0200
22.3 @@ -130,6 +130,7 @@
22.4 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", [["RootRatEq", "elim_rootrat_equation"]]))]\<close>
22.5
22.6 subsection \<open>methods\<close>
22.7 +
22.8 setup \<open>KEStore_Elems.add_mets
22.9 [MethodC.prep_input @{theory LinEq} "met_rootrateq" [] MethodC.id_empty
22.10 (["RootRatEq"], [],
22.11 @@ -148,17 +149,17 @@
22.12 (Try (Rewrite_Set ''rooteq_simplify'')) #>
22.13 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
22.14 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
22.15 -setup \<open>KEStore_Elems.add_mets
22.16 - [MethodC.prep_input @{theory} "met_rootrateq_elim" [] MethodC.id_empty
22.17 - (["RootRatEq", "elim_rootrat_equation"],
22.18 - [("#Given" ,["equality e_e", "solveFor v_v"]),
22.19 - ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
22.20 - "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
22.21 - ("#Find" ,["solutions v_v'i'"])],
22.22 - {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule_Set.empty, prls=RootRatEq_prls, calc=[],
22.23 - crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
22.24 - @{thm solve_rootrat_equ.simps})]
22.25 -\<close> ML \<open>
22.26 +
22.27 +method met_rootrateq_elim : "RootRatEq/elim_rootrat_equation" =
22.28 + \<open>{rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule_Set.empty, prls=RootRatEq_prls, calc=[],
22.29 + crls=RootRatEq_crls, errpats = [], nrls = norm_Rational}\<close>
22.30 + Program: solve_rootrat_equ.simps
22.31 + Given: "equality e_e" "solveFor v_v"
22.32 + Where: "( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) |
22.33 + ( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"
22.34 + Find: "solutions v_v'i'"
22.35 +
22.36 +ML \<open>
22.37 \<close> ML \<open>
22.38 \<close>
22.39 end
23.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Sat Jun 12 18:33:15 2021 +0200
23.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Tue Jun 15 22:24:20 2021 +0200
23.3 @@ -34,15 +34,12 @@
23.4 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close>
23.5
23.6 (** methods **)
23.7 -setup \<open>KEStore_Elems.add_mets
23.8 - [MethodC.prep_input @{theory} "met_tsimp" [] MethodC.id_empty
23.9 - (["simplification"],
23.10 - [("#Given" ,["Term t_t"]),
23.11 - ("#Find" ,["normalform n_n"])],
23.12 - {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,
23.13 - errpats = [], nrls = Rule_Set.empty},
23.14 - @{thm refl})]
23.15 -\<close>
23.16 +
23.17 +method met_tsimp : "simplification" =
23.18 + \<open>{rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,
23.19 + errpats = [], nrls = Rule_Set.empty}\<close>
23.20 + Given: "Term t_t"
23.21 + Find: "normalform n_n"
23.22
23.23 ML \<open>
23.24
24.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jun 12 18:33:15 2021 +0200
24.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Jun 15 22:24:20 2021 +0200
24.3 @@ -843,17 +843,15 @@
24.4 (Rewrite_Set ''Test_simplify'')) e_e
24.5 in
24.6 [e_e])"
24.7 -setup \<open>KEStore_Elems.add_mets
24.8 - [MethodC.prep_input @{theory} "met_test_solvelin" [] MethodC.id_empty
24.9 - (["Test", "solve_linear"],
24.10 - [("#Given" ,["equality e_e", "solveFor v_v"]),
24.11 - ("#Where" ,["matches (?a = ?b) e_e"]),
24.12 - ("#Find" ,["solutions v_v'i'"])],
24.13 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
24.14 - prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
24.15 - nrls = Test_simplify},
24.16 - @{thm solve_linear.simps})]
24.17 -\<close>
24.18 +method met_test_solvelin : "Test/solve_linear" =
24.19 + \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
24.20 + prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
24.21 + nrls = Test_simplify}\<close>
24.22 + Program: solve_linear.simps
24.23 + Given: "equality e_e" "solveFor v_v"
24.24 + Where: "matches (?a = ?b) e_e"
24.25 + Find: "solutions v_v'i'"
24.26 +
24.27 subsection \<open>root equation\<close>
24.28
24.29 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.30 @@ -874,22 +872,20 @@
24.31 ) e_e
24.32 in
24.33 [e_e])"
24.34 -setup \<open>KEStore_Elems.add_mets
24.35 - [MethodC.prep_input @{theory} "met_test_sqrt" [] MethodC.id_empty
24.36 - (*root-equation, version for tests before 8.01.01*)
24.37 - (["Test", "sqrt-equ-test"],
24.38 - [("#Given" ,["equality e_e", "solveFor v_v"]),
24.39 - ("#Where" ,["contains_root (e_e::bool)"]),
24.40 - ("#Find" ,["solutions v_v'i'"])],
24.41 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.42 - srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.43 - [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
24.44 - prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
24.45 - [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
24.46 - calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
24.47 - asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
24.48 - @{thm solve_root_equ.simps})]
24.49 -\<close>
24.50 +
24.51 +method met_test_sqrt : "Test/sqrt-equ-test" =
24.52 + (*root-equation, version for tests before 8.01.01*)
24.53 + \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
24.54 + srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.55 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
24.56 + prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
24.57 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
24.58 + calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
24.59 + asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close>
24.60 + Program: solve_root_equ.simps
24.61 + Given: "equality e_e" "solveFor v_v"
24.62 + Where: "contains_root (e_e::bool)"
24.63 + Find: "solutions v_v'i'"
24.64
24.65 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.66 where
24.67 @@ -902,19 +898,17 @@
24.68 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
24.69 in
24.70 Check_elementwise L_L {(v_v::real). Assumptions})"
24.71 -setup \<open>KEStore_Elems.add_mets
24.72 - [MethodC.prep_input @{theory} "met_test_squ_sub" [] MethodC.id_empty
24.73 - (*tests subproblem fixed linear*)
24.74 - (["Test", "squ-equ-test-subpbl1"],
24.75 - [("#Given" ,["equality e_e", "solveFor v_v"]),
24.76 - ("#Where" ,["precond_rootmet v_v"]),
24.77 - ("#Find" ,["solutions v_v'i'"])],
24.78 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
24.79 +
24.80 +method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
24.81 + (*tests subproblem fixed linear*)
24.82 + \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
24.83 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
24.84 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
24.85 - calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
24.86 - @{thm minisubpbl.simps})]
24.87 -\<close>
24.88 + calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
24.89 + Program: minisubpbl.simps
24.90 + Given: "equality e_e" "solveFor v_v"
24.91 + Where: "precond_rootmet v_v"
24.92 + Find: "solutions v_v'i'"
24.93
24.94 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.95 where
24.96 @@ -934,19 +928,17 @@
24.97 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
24.98 in
24.99 Check_elementwise L_L {(v_v::real). Assumptions}) "
24.100 -setup \<open>KEStore_Elems.add_mets
24.101 - [MethodC.prep_input @{theory} "met_test_eq1" [] MethodC.id_empty
24.102 - (*root-equation1:*)
24.103 - (["Test", "square_equation1"],
24.104 - [("#Given" ,["equality e_e", "solveFor v_v"]),
24.105 - ("#Find" ,["solutions v_v'i'"])],
24.106 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.107 - srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.108 - [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
24.109 - errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),
24.110 - ("square_equation_right", "")]*)},
24.111 - @{thm solve_root_equ2.simps})]
24.112 -\<close>
24.113 +
24.114 +method met_test_eq1 : "Test/square_equation1" =
24.115 + (*root-equation1:*)
24.116 + \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
24.117 + srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.118 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
24.119 + errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),
24.120 + ("square_equation_right", "")]*)}\<close>
24.121 + Program: solve_root_equ2.simps
24.122 + Given: "equality e_e" "solveFor v_v"
24.123 + Find: "solutions v_v'i'"
24.124
24.125 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.126 where
24.127 @@ -967,19 +959,17 @@
24.128 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
24.129 in
24.130 Check_elementwise L_L {(v_v::real). Assumptions})"
24.131 -setup \<open>KEStore_Elems.add_mets
24.132 - [MethodC.prep_input @{theory} "met_test_squ2" [] MethodC.id_empty
24.133 - (*root-equation2*)
24.134 - (["Test", "square_equation2"],
24.135 - [("#Given" ,["equality e_e", "solveFor v_v"]),
24.136 - ("#Find" ,["solutions v_v'i'"])],
24.137 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.138 - srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.139 - [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
24.140 - prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
24.141 - asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
24.142 - @{thm solve_root_equ3.simps})]
24.143 -\<close>
24.144 +
24.145 +method met_test_squ2 : "Test/square_equation2" =
24.146 + (*root-equation2*)
24.147 + \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
24.148 + srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.149 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
24.150 + prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
24.151 + asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close>
24.152 + Program: solve_root_equ3.simps
24.153 + Given: "equality e_e" "solveFor v_v"
24.154 + Find: "solutions v_v'i'"
24.155
24.156 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.157 where
24.158 @@ -1000,19 +990,17 @@
24.159 [''no_met'']) [BOOL e_e, REAL v_v]
24.160 in
24.161 Check_elementwise L_L {(v_v::real). Assumptions})"
24.162 -setup \<open>KEStore_Elems.add_mets
24.163 - [MethodC.prep_input @{theory} "met_test_squeq" [] MethodC.id_empty
24.164 - (*root-equation*)
24.165 - (["Test", "square_equation"],
24.166 - [("#Given" ,["equality e_e", "solveFor v_v"]),
24.167 - ("#Find" ,["solutions v_v'i'"])],
24.168 - {rew_ord'="e_rew_ord",rls'=tval_rls,
24.169 - srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.170 - [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
24.171 - prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
24.172 - asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
24.173 - @{thm solve_root_equ4.simps})]
24.174 -\<close>
24.175 +
24.176 +method met_test_squeq : "Test/square_equation" =
24.177 + (*root-equation*)
24.178 + \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
24.179 + srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
24.180 + [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
24.181 + prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
24.182 + asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close>
24.183 + Program: solve_root_equ4.simps
24.184 + Given: "equality e_e" "solveFor v_v"
24.185 + Find: "solutions v_v'i'"
24.186
24.187 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.188 where
24.189 @@ -1026,21 +1014,22 @@
24.190 (Try (Rewrite_Set ''tval_rls'' ))) e_e
24.191 in
24.192 Or_to_List e_e)"
24.193 -setup \<open>KEStore_Elems.add_mets
24.194 - [MethodC.prep_input @{theory} "met_test_eq_plain" [] MethodC.id_empty
24.195 - (*solve_plain_square*)
24.196 - (["Test", "solve_plain_square"],
24.197 - [("#Given",["equality e_e", "solveFor v_v"]),
24.198 - ("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
24.199 - "(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^
24.200 - "(matches (?a + v_v \<up> 2 = 0) e_e) |" ^
24.201 - "(matches ( v_v \<up> 2 = 0) e_e)"]),
24.202 - ("#Find" ,["solutions v_v'i'"])],
24.203 - {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
24.204 - prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
24.205 - asm_rls=[],asm_thm=[]*)},
24.206 - @{thm solve_plain_square.simps})]
24.207 -\<close>
24.208 +
24.209 +method met_test_eq_plain : "Test/solve_plain_square" =
24.210 + (*solve_plain_square*)
24.211 + \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
24.212 + prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
24.213 + asm_rls=[],asm_thm=[]*)}\<close>
24.214 + Program: solve_plain_square.simps
24.215 + Given: "equality e_e" "solveFor v_v"
24.216 + Where:
24.217 + "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |
24.218 + (matches ( ?b*v_v \<up> 2 = 0) e_e) |
24.219 + (matches (?a + v_v \<up> 2 = 0) e_e) |
24.220 + (matches ( v_v \<up> 2 = 0) e_e)"
24.221 + Find: "solutions v_v'i'"
24.222 +
24.223 +
24.224 subsection \<open>polynomial equation\<close>
24.225
24.226 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
24.227 @@ -1053,16 +1042,16 @@
24.228 in
24.229 SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
24.230 [''no_met'']) [BOOL e_e, REAL v_v])"
24.231 -setup \<open>KEStore_Elems.add_mets
24.232 - [MethodC.prep_input @{theory} "met_test_norm_univ" [] MethodC.id_empty
24.233 - (["Test", "norm_univar_equation"],
24.234 - [("#Given",["equality e_e", "solveFor v_v"]),
24.235 - ("#Where" ,[]),
24.236 - ("#Find" ,["solutions v_v'i'"])],
24.237 - {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
24.238 - errpats = [], nrls = Rule_Set.empty},
24.239 - @{thm norm_univariate_equ.simps})]
24.240 -\<close>
24.241 +
24.242 +method met_test_norm_univ : "Test/norm_univar_equation" =
24.243 + \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
24.244 + errpats = [], nrls = Rule_Set.empty}\<close>
24.245 + Program: norm_univariate_equ.simps
24.246 + Given: "equality e_e" "solveFor v_v"
24.247 + Where:
24.248 + Find: "solutions v_v'i'"
24.249 +
24.250 +
24.251 subsection \<open>diophantine equation\<close>
24.252
24.253 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
24.254 @@ -1071,16 +1060,16 @@
24.255 Repeat (
24.256 (Try (Calculate ''PLUS'')) #>
24.257 (Try (Calculate ''TIMES''))) t_t)"
24.258 -setup \<open>KEStore_Elems.add_mets
24.259 - [MethodC.prep_input @{theory} "met_test_intsimp" [] MethodC.id_empty
24.260 - (["Test", "intsimp"],
24.261 - [("#Given" ,["intTestGiven t_t"]),
24.262 - ("#Where" ,[]),
24.263 - ("#Find" ,["intTestFind s_s"])],
24.264 - {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
24.265 - crls = tval_rls, errpats = [], nrls = Test_simplify},
24.266 - @{thm test_simplify.simps})]
24.267 -\<close> ML \<open>
24.268 +
24.269 +method met_test_intsimp : "Test/intsimp" =
24.270 + \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
24.271 + crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
24.272 + Program: test_simplify.simps
24.273 + Given: "intTestGiven t_t"
24.274 + Where:
24.275 + Find: "intTestFind s_s"
24.276 +
24.277 +ML \<open>
24.278 \<close>
24.279
24.280 end
25.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Sat Jun 12 18:33:15 2021 +0200
25.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Jun 15 22:24:20 2021 +0200
25.3 @@ -5,7 +5,9 @@
25.4 Defitions required for both, for Specify and for the Lucas-Interpreter.
25.5 *)
25.6 theory MathEngBasic
25.7 -imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
25.8 + imports "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
25.9 + keywords "method" :: thy_decl
25.10 + and "Author" "Program" "Given" "Where" "Find" "Relate"
25.11 begin
25.12 ML_file thmC.sml
25.13 ML_file problem.sml
26.1 --- a/src/Tools/isac/MathEngBasic/method.sml Sat Jun 12 18:33:15 2021 +0200
26.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Jun 15 22:24:20 2021 +0200
26.3 @@ -17,6 +17,9 @@
26.4 val prep_input : theory -> Check_Unique.id -> string list -> id ->
26.5 id * Problem.model_input * input * thm -> T * id
26.6
26.7 + val set_input: input -> theory -> theory
26.8 + val the_input: theory -> input
26.9 +
26.10 val from_store: id -> T
26.11 val from_store': theory -> id -> T
26.12 end
26.13 @@ -41,7 +44,7 @@
26.14 {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
26.15 prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
26.16
26.17 -fun prep_input thy guh maa init
26.18 +fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
26.19 (metID, ppc,
26.20 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
26.21 errpats = ep, nrls = nr}, scr) =
26.22 @@ -88,12 +91,68 @@
26.23 val sc = Program.prep_program scr
26.24 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
26.25 in
26.26 - ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro,
26.27 - erls = rls, srls = srls, prls = prls, calc = calc,
26.28 + ({guh = guh, mathauthors = mathauthors, init = init, ppc = gi @ fi @ re, pre = wh,
26.29 + rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
26.30 crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
26.31 end;
26.32
26.33
26.34 +(** Isar command **)
26.35 +
26.36 +structure Data = Theory_Data
26.37 +(
26.38 + type T = input option;
26.39 + val empty = NONE;
26.40 + val extend = I;
26.41 + fun merge _ = NONE;
26.42 +);
26.43 +
26.44 +val set_input = Data.put o SOME;
26.45 +val the_input = the o Data.get;
26.46 +
26.47 +local
26.48 +
26.49 +fun parse_item keyword parse = (keyword -- Args.colon) |-- Parse.!!! parse;
26.50 +
26.51 +val parse_authors =
26.52 + Scan.optional (parse_item \<^keyword>\<open>Author\<close> (Scan.repeat1 Parse.name)) [];
26.53 +
26.54 +val parse_program =
26.55 + Scan.option (parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
26.56 +
26.57 +fun parse_terms keyword (tag: string) =
26.58 + Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
26.59 +
26.60 +val parse_ppc =
26.61 + parse_terms \<^keyword>\<open>Given\<close> "#Given" @@@
26.62 + parse_terms \<^keyword>\<open>Where\<close> "#Where" @@@
26.63 + parse_terms \<^keyword>\<open>Find\<close> "#Find" @@@
26.64 + parse_terms \<^keyword>\<open>Relate\<close> "#Relate";
26.65 +
26.66 +val ml = ML_Lex.read;
26.67 +
26.68 +val _ =
26.69 + Outer_Syntax.command \<^command_keyword>\<open>method\<close>
26.70 + "prepare ISAC method and register it to Knowledge Store"
26.71 + (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
26.72 + Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors -- parse_program -- parse_ppc)) >>
26.73 + (fn (name, (id, (((source, mathauthors), simp), ppc))) => Toplevel.theory (fn thy =>
26.74 + let
26.75 + val metID = References_Def.explode_id id;
26.76 + val eval_input =
26.77 + ML_Context.expression (Input.pos_of source)
26.78 + (ml "Theory.setup (MethodC.set_input (" @ ML_Lex.read_source source @ ml "))")
26.79 + |> Context.theory_map;
26.80 + val input = the_input (eval_input thy);
26.81 + val thm =
26.82 + (case simp of
26.83 + NONE => @{thm refl}
26.84 + | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
26.85 + val arg = prep_input thy name mathauthors id_empty (metID, ppc, input, thm);
26.86 + in KEStore_Elems.add_mets [arg] thy end)))
26.87 +
26.88 +in end;
26.89 +
26.90 (** get MethodC from Store **)
26.91
26.92 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)