1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Fri Feb 15 16:52:05 2019 +0100
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Tue Feb 19 19:35:12 2019 +0100
1.3 @@ -15,6 +15,9 @@
1.4 KantenLaenge :: "bool => una"
1.5 Querschnitt :: "bool => una"
1.6 GesamtLaenge :: "real => una"
1.7 + oben :: real
1.8 + senkrecht :: real
1.9 + unten :: real
1.10
1.11 (*Script-names*)
1.12 RechnenSymbolScript :: "[bool,bool,bool list,bool list,bool list,real,
1.13 @@ -47,6 +50,26 @@
1.14 errpats = [], nrls = Rule.Erls},
1.15 "empty_script")]
1.16 \<close>
1.17 +partial_function (tailrec) symbolisch_rechnen :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
1.18 + where
1.19 +"symbolisch_rechnen k_k q__q u_u s_s o_o l_l =
1.20 + (let t_t = Take (l_l = oben + senkrecht + unten);
1.21 + su_m = boollist2sum o_o;
1.22 + t_t = Substitute [oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
1.23 + t_t = Substitute o_o t_t;
1.24 + t_t = Substitute [k_k, q__q] t_t;
1.25 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
1.26 + su_m = boollist2sum s_s;
1.27 + t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
1.28 + t_t = Substitute s_s t_t;
1.29 + t_t = Substitute [k_k, q__q] t_t;
1.30 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
1.31 + su_m = boollist2sum u_u;
1.32 + t_t = Substitute [unten = su_m] t_t; \<comment> \<open>PROG consts\<close>
1.33 + t_t = Substitute u_u t_t;
1.34 + t_t = Substitute [k_k, q__q] t_t;
1.35 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t
1.36 + in Try (Rewrite_Set ''norm_Poly'' False) t_t)"
1.37 setup \<open>KEStore_Elems.add_mets
1.38 [Specify.prep_met thy "met_algein_numsym_1num" [] Celem.e_metID
1.39 (["Berechnung","erstNumerisch"],
1.40 @@ -77,6 +100,25 @@
1.41 " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t " ^
1.42 " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) ")]
1.43 \<close>
1.44 +partial_function (tailrec) symbolisch_rechnen_2 :: "bool \<Rightarrow> bool \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> bool"
1.45 + where
1.46 +"symbolisch_rechnen (k_k::bool) (q__q::bool)
1.47 +(u_u::bool list) (s_s::bool list) (o_o::bool list) (l_l::real) =
1.48 + (let t_t = Take (l_l = oben + senkrecht + unten);
1.49 + su_m = boollist2sum o_o;
1.50 + t_t = Substitute [oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
1.51 + t_t = Substitute o_o t_t;
1.52 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
1.53 + su_m = boollist2sum s_s;
1.54 + t_t = Substitute [senkrecht = su_m] t_t; \<comment> \<open>PROG consts\<close>
1.55 + t_t = Substitute s_s t_t;
1.56 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
1.57 + su_m = boollist2sum u_u;
1.58 + t_t = Substitute [unten = su_m] t_t; \<comment> \<open>PROG consts\<close>
1.59 + t_t = Substitute u_u t_t;
1.60 + t_t = Repeat (Try (Rewrite_Set ''norm_Poly'' False)) t_t;
1.61 + t_t = Substitute [k_k, q__q] t_t
1.62 + in (Try (Rewrite_Set ''norm_Poly'' False)) t_t)"
1.63 setup \<open>KEStore_Elems.add_mets
1.64 [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
1.65 (["Berechnung","erstSymbolisch"],
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Fri Feb 15 16:52:05 2019 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Feb 19 19:35:12 2019 +0100
2.3 @@ -187,7 +187,75 @@
2.4 section \<open>Methods\<close>
2.5
2.6 subsection \<open>Sub-problem "integrate and determine constants", little modularisation\<close>
2.7 -
2.8 +(*PROG Extra variables on rhs: "x", "y", "c_2", "c"
2.9 +partial_function (tailrec) biegelinie_lang
2.10 +:: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool list \<Rightarrow> bool"
2.11 + where
2.12 +"biegelinie_lang
2.13 +(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real)
2.14 +(r_b::bool list) (r_m::bool list) =
2.15 + (let q___q = Take (qq v_v = q__q);
2.16 + q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@
2.17 + (Rewrite ''Belastung_Querkraft'' True)) q___q;
2.18 + (Q__Q:: bool) =
2.19 + (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],
2.20 + [''diff'',''integration'',''named''])
2.21 + [REAL (rhs q___q), REAL v_v, REAL_REAL Q]);
2.22 + Q__Q = Rewrite ''Querkraft_Moment'' True Q__Q;
2.23 + (M__M::bool) =
2.24 + (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],
2.25 + [''diff'',''integration'',''named''])
2.26 + [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]);
2.27 + (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
2.28 + e__1 = NTH 1 r_m;
2.29 + (x__1::real) = argument_in (lhs e__1);
2.30 + (M__1::bool) = (Substitute [v_v = x__1]) M__M;
2.31 + (*([6], Res), M_b 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
2.32 + M__1 = (Substitute [e__1]) M__1;
2.33 + (*([7], Res), 0 = c_2 + c * 0 + -1 * q_0 / 2 * 0 ^^^ 2*)
2.34 + M__2 = Take M__M;
2.35 + (*([8], Frm), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
2.36 +(*without above Take 'Substitute [v_v = x__2]' takes _last formula from ctree_*)
2.37 + e__2 = NTH 2 r_m;
2.38 + (x__2::real) = argument_in (lhs e__2);
2.39 + (M__2::bool) = (Substitute [v_v = x__2]) M__M;
2.40 + (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
2.41 + M__2 = (Substitute [e__2]) M__2;
2.42 + (c_1_2::bool list) =
2.43 + (SubProblem (''Biegelinie'',[''LINEAR'',''system''],[''no_met''])
2.44 + [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]);
2.45 + M__M = Take M__M;
2.46 + M__M = ((Substitute c_1_2) @@
2.47 + (Try (Rewrite_Set_Inst [(''bdv_1'', c),(''bdv_2'', c_2)]
2.48 + ''simplify_System'' False)) @@
2.49 + (Rewrite ''Moment_Neigung'' False) @@
2.50 + (Rewrite ''make_fun_explicit'' False)) M__M;
2.51 +(*----------------------- and the same once more ------------------------*)
2.52 + (N__N:: bool) =
2.53 + (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],
2.54 + [''diff'',''integration'',''named''])
2.55 + [REAL (rhs M__M), REAL v_v, REAL_REAL y']);
2.56 + (B__B:: bool) =
2.57 + (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''],
2.58 + [''diff'',''integration'',''named''])
2.59 + [REAL (rhs N__N), REAL v_v, REAL_REAL y]);
2.60 + e__1 = NTH 1 r_b;
2.61 + (x__1::real) = argument_in (lhs e__1);
2.62 + (B__1::bool) = (Substitute [v_v = x__1]) B__B;
2.63 + B__1 = (Substitute [e__1]) B__1 ;
2.64 + B__2 = Take B__B;
2.65 + e__2 = NTH 2 r_b;
2.66 + (x__2::real) = argument_in (lhs e__2);
2.67 + (B__2::bool) = (Substitute [v_v = x__2]) B__B;
2.68 + B__2 = (Substitute [e__2]) B__2 ;
2.69 + (c_1_2::bool list) =
2.70 + (SubProblem (''Biegelinie'',[''LINEAR'',''system''],[''no_met''])
2.71 + [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]);
2.72 + B__B = Take B__B;
2.73 + B__B = ((Substitute c_1_2) @@
2.74 + (Rewrite_Set_Inst [(''bdv'', x)] ''make_ratpoly_in'' False)) B__B
2.75 + in B__B) "
2.76 +*)
2.77 setup \<open>KEStore_Elems.add_mets
2.78 [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID
2.79 (["IntegrierenUndKonstanteBestimmen"],
2.80 @@ -274,8 +342,6 @@
2.81 no_met :: ID make_ratpoly_in :: ID
2.82 bdv :: real c :: real c_2 :: real c_3 :: real c_4 :: real
2.83
2.84 -BETTER see HOL/ex/Cartouche_Examples.thy subsection \<open>Inner syntax: string literals via cartouche\<close>
2.85 -
2.86 partial_function (tailrec) biegelinie ::
2.87 "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool"
2.88 where
2.89 @@ -295,7 +361,19 @@
2.90 in B) "
2.91
2.92 \\\------------------------------------------------------------------------------------*)
2.93 -
2.94 +partial_function (tailrec) biegelinie :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool"
2.95 + where
2.96 +"biegelinie l q v b s =
2.97 + (let
2.98 + funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
2.99 + [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v];
2.100 + equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
2.101 + [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
2.102 + cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
2.103 + [BOOL_LIST equs, STRING_LIST [''c'', ''c_2'', ''c_3'', ''c_4'']]; \<comment> \<open>PROG consts\<close>
2.104 + B = Take (lastI funs);
2.105 + B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B
2.106 + in B)"
2.107 setup \<open>KEStore_Elems.add_mets
2.108 [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
2.109 (["IntegrierenUndKonstanteBestimmen2"],
2.110 @@ -316,22 +394,22 @@
2.111 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
2.112 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
2.113 prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
2.114 - "Script Biegelinie2Script " ^
2.115 - "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) = " ^
2.116 - " (let " ^
2.117 - " (funs :: bool list) = (SubProblem (''Biegelinie'', " ^
2.118 - " [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung'']) " ^
2.119 - " [REAL q, REAL v]); " ^
2.120 - " (equs :: bool list) = (SubProblem (''Biegelinie'', " ^
2.121 + "Script Biegelinie2Script " ^
2.122 + "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) = " ^
2.123 + " (let " ^
2.124 + " (funs :: bool list) = (SubProblem (''Biegelinie'', " ^
2.125 + " [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung'']) " ^
2.126 + " [REAL q, REAL v]); " ^
2.127 + " (equs :: bool list) = (SubProblem (''Biegelinie'', " ^
2.128 " [''setzeRandbedingungen'', ''Biegelinien''], [''Biegelinien'', ''setzeRandbedingungenEin'']) " ^
2.129 - " [BOOL_LIST funs, BOOL_LIST s]); " ^
2.130 - " (cons :: bool list) = (SubProblem (''Biegelinie'', " ^
2.131 - " [''LINEAR'', ''system''], [''no_met'']) " ^
2.132 - " [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]); " ^
2.133 - " B = Take (lastI funs); " ^
2.134 - " B = ((Substitute cons) @@ " ^
2.135 - " (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B " ^
2.136 - " in B) ")]
2.137 + " [BOOL_LIST funs, BOOL_LIST s]); " ^
2.138 + " (cons :: bool list) = (SubProblem (''Biegelinie'', " ^
2.139 + " [''LINEAR'', ''system''], [''no_met'']) " ^
2.140 + " [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]); " ^
2.141 + " B = Take (lastI funs); " ^
2.142 + " B = ((Substitute cons) @@ " ^
2.143 + " (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B " ^
2.144 + " in B) ")]
2.145 \<close>
2.146 setup \<open>KEStore_Elems.add_mets
2.147 [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
2.148 @@ -357,6 +435,26 @@
2.149 \<close>
2.150 subsection \<open>Compute the general bending line\<close>
2.151
2.152 +partial_function (tailrec) belastung_zu_biegelinie :: "real \<Rightarrow> real \<Rightarrow> bool list"
2.153 + where
2.154 +"belastung_zu_biegelinie q__q v_v =
2.155 + (let q___q = Take (qq v_v = q__q);
2.156 + q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@
2.157 + (Rewrite ''Belastung_Querkraft'' True)) q___q;
2.158 + Q__Q = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.159 + [''diff'', ''integration'', ''named'']) [REAL (rhs q___q), REAL v_v, REAL_REAL Q];
2.160 + M__M = Rewrite ''Querkraft_Moment'' True Q__Q;
2.161 + M__M = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.162 + [''diff'', ''integration'', ''named'']) [REAL (rhs M__M), REAL v_v, REAL_REAL M_b];
2.163 + N__N = ((Rewrite ''Moment_Neigung'' False) @@
2.164 + (Rewrite ''make_fun_explicit'' False)) M__M;
2.165 + N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.166 + [''diff'', ''integration'', ''named''])
2.167 + [REAL (rhs N__N), REAL v_v, STRING ''dy'']; \<comment> \<open>PROG string\<close>
2.168 + B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
2.169 + [''diff'', ''integration'', ''named''])
2.170 + [REAL (rhs N__N), REAL v_v, STRING ''y''] \<comment> \<open>PROG string\<close>
2.171 + in [Q__Q, M__M, N__N, B__B])"
2.172 setup \<open>KEStore_Elems.add_mets
2.173 [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
2.174 (["Biegelinien", "ausBelastung"],
2.175 @@ -398,6 +496,26 @@
2.176 \<close>
2.177 subsection \<open>Substitute the constraints into the equations\<close>
2.178
2.179 +partial_function (tailrec) setzte_randbedingungen :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
2.180 + where
2.181 +"setzte_randbedingungen fun_s r_b =
2.182 + (let b_1 = NTH 1 r_b;
2.183 + f_s = filter_sameFunId (lhs b_1) fun_s;
2.184 + e_1 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
2.185 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_1];
2.186 + b_2 = NTH 2 r_b;
2.187 + f_s = filter_sameFunId (lhs b_2) fun_s;
2.188 + e_2 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
2.189 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_2];
2.190 + b_3 = NTH 3 r_b;
2.191 + f_s = filter_sameFunId (lhs b_3) fun_s;
2.192 + e_3 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
2.193 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_3];
2.194 + b_4 = NTH 4 r_b;
2.195 + f_s = filter_sameFunId (lhs b_4) fun_s;
2.196 + e_4 = SubProblem (''Biegelinie'', [''makeFunctionTo'', ''equation''],
2.197 + [''Equation'', ''fromFunction'']) [BOOL (hd f_s), BOOL b_4]
2.198 + in [e_1, e_2, e_3, e_4])"
2.199 setup \<open>KEStore_Elems.add_mets
2.200 [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
2.201 (["Biegelinien", "setzeRandbedingungenEin"],
2.202 @@ -461,6 +579,18 @@
2.203 \<close>
2.204 subsection \<open>Transform an equality into a function\<close>
2.205
2.206 + (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2) (M_b L = 0) -->
2.207 + 0 = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
2.208 +partial_function (tailrec) function_to_equality :: "bool \<Rightarrow> bool \<Rightarrow> bool"
2.209 + where
2.210 +"function_to_equality fu_n su_b =
2.211 + (let fu_n = Take fu_n;
2.212 + bd_v = argument_in (lhs fu_n);
2.213 + va_l = argument_in (lhs su_b);
2.214 + eq_u = Substitute [bd_v = va_l] fu_n;
2.215 + \<comment> \<open>([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2\<close>
2.216 + eq_u = Substitute [su_b] eq_u
2.217 + in (Rewrite_Set ''norm_Rational'' False) eq_u)"
2.218 setup \<open>KEStore_Elems.add_mets
2.219 [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
2.220 (["Equation","fromFunction"],
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri Feb 15 16:52:05 2019 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Feb 19 19:35:12 2019 +0100
3.3 @@ -287,6 +287,30 @@
3.4 crls = Atools_erls, errpats = [], nrls = norm_diff},
3.5 "empty_script")]
3.6 \<close>
3.7 +partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
3.8 + where
3.9 +"differentiate_on_R f_f v_v =
3.10 + (let f_f' = Take (d_d v_v f_f)
3.11 + in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
3.12 + (Repeat
3.13 + ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or
3.14 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or
3.15 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or
3.16 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or
3.17 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or
3.18 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or
3.19 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or
3.20 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or
3.21 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or
3.22 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or
3.23 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or
3.24 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or
3.25 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or
3.26 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or
3.27 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or
3.28 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
3.29 + (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
3.30 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"
3.31 setup \<open>KEStore_Elems.add_mets
3.32 [Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
3.33 (["diff","differentiate_on_R"],
3.34 @@ -317,6 +341,30 @@
3.35 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
3.36 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')")]
3.37 \<close>
3.38 +partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
3.39 + where
3.40 +"differentiateX f_f v_v =
3.41 + (let f_f' = Take (d_d v_v f_f)
3.42 + in ((
3.43 + (Repeat
3.44 + ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or
3.45 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or
3.46 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or
3.47 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' False)) Or
3.48 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or
3.49 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or
3.50 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or
3.51 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or
3.52 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or
3.53 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or
3.54 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or
3.55 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or
3.56 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or
3.57 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or
3.58 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or
3.59 + (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or
3.60 + (Repeat (Rewrite_Set ''make_polynomial'' False))))
3.61 + )) f_f')"
3.62 setup \<open>KEStore_Elems.add_mets
3.63 [Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
3.64 (["diff","diff_simpl"],
3.65 @@ -347,6 +395,33 @@
3.66 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) " ^
3.67 " )) f_f')")]
3.68 \<close>
3.69 +partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
3.70 + where
3.71 +"differentiate_equality f_f v_v =
3.72 + (let
3.73 + f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
3.74 + in
3.75 + (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
3.76 + (Repeat
3.77 + ((Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'' False)) Or
3.78 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' False)) Or
3.79 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'' False)) Or
3.80 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'' False)) Or
3.81 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'' True )) Or
3.82 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'' False)) Or
3.83 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'' False)) Or
3.84 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'' False)) Or
3.85 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'' False)) Or
3.86 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'' False)) Or
3.87 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'' False)) Or
3.88 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'' False)) Or
3.89 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'' False)) Or
3.90 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'' False)) Or
3.91 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'' False)) Or
3.92 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'' False)) Or
3.93 + (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'' False)) Or
3.94 + (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@
3.95 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' False)))) f_f')"
3.96 setup \<open>KEStore_Elems.add_mets
3.97 [Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
3.98 (["diff","differentiate_equality"],
3.99 @@ -378,6 +453,16 @@
3.100 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
3.101 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') ")]
3.102 \<close>
3.103 +partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
3.104 + where
3.105 +"simplify_derivative f_f v_v =
3.106 + (let
3.107 + f_f' = Take (d_d v_v f_f)
3.108 + in ((Try (Rewrite_Set ''norm_Rational'' False)) @@
3.109 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
3.110 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@
3.111 + (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@
3.112 + (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"
3.113 setup \<open>KEStore_Elems.add_mets
3.114 [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
3.115 (["diff","after_simplification"],
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Fri Feb 15 16:52:05 2019 +0100
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Feb 19 19:35:12 2019 +0100
4.3 @@ -123,6 +123,20 @@
4.4 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
4.5 "empty_script")]
4.6 \<close>
4.7 +partial_function (tailrec) maximum_value ::
4.8 + "bool list \<Rightarrow> real \<Rightarrow> bool list \<Rightarrow> real \<Rightarrow> real set \<Rightarrow> bool \<Rightarrow> bool list"
4.9 + where
4.10 +"maximum_value f_ix m_m r_s v_v itv_v e_rr =
4.11 + (let e_e = (hd o (filterVar m_m)) r_s;
4.12 + t_t = if 1 < LENGTH r_s
4.13 + then SubProblem (''DiffApp'', [''make'', ''function''],[''no_met''])
4.14 + [REAL m_m, REAL v_v, BOOL_LIST r_s]
4.15 + else (hd r_s);
4.16 + m_x = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],
4.17 + [''DiffApp'', ''max_on_interval_by_calculus''])
4.18 + [BOOL t_t, REAL v_v, REAL_SET itv_v]
4.19 + in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac'', ''find_values''])
4.20 + [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
4.21 setup \<open>KEStore_Elems.add_mets
4.22 [Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID
4.23 (["DiffApp","max_by_calculus"],
4.24 @@ -147,6 +161,21 @@
4.25 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^
4.26 " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) ")]
4.27 \<close>
4.28 +partial_function (tailrec) make_fun_by_new_variable :: "real => real => bool list => bool"
4.29 + where
4.30 +"make_fun_by_new_variable f_f v_v eqs =
4.31 + (let h_h = (hd o (filterVar f_f)) eqs;
4.32 + e_s = dropWhile (ident h_h) eqs;
4.33 + v_s = dropWhile (ident f_f) (Vars h_h);
4.34 + v_1 = NTH 1 v_s;
4.35 + v_2 = NTH 2 v_s;
4.36 + e_1 = (hd o (filterVar v_1)) e_s;
4.37 + e_2 = (hd o (filterVar v_2)) e_s;
4.38 + s_1 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
4.39 + [BOOL e_1, REAL v_1];
4.40 + s_2 = SubProblem (''DiffApp'', [''univariate'', ''equation''], [''no_met''])
4.41 + [BOOL e_2, REAL v_2]
4.42 + in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
4.43 setup \<open>KEStore_Elems.add_mets
4.44 [Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID
4.45 (["DiffApp","make_fun_by_new_variable"],
4.46 @@ -171,6 +200,16 @@
4.47 " [BOOL e_2, REAL v_2])" ^
4.48 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)")]
4.49 \<close>
4.50 +partial_function (tailrec) make_fun_by_explicit :: "real => real => bool list => bool"
4.51 + where
4.52 +"make_fun_by_explicit f_f v_v eqs =
4.53 + (let h_h = (hd o (filterVar f_f)) eqs;
4.54 + e_1 = hd (dropWhile (ident h_h) eqs);
4.55 + v_s = dropWhile (ident f_f) (Vars h_h);
4.56 + v_1 = hd (dropWhile (ident v_v) v_s);
4.57 + s_1 = SubProblem(''DiffApp'', [''univariate'', ''equation''], [''no_met''])
4.58 + [BOOL e_1, REAL v_1]
4.59 + in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
4.60 setup \<open>KEStore_Elems.add_mets
4.61 [Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID
4.62 (["DiffApp","make_fun_by_explicit"],
5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Fri Feb 15 16:52:05 2019 +0100
5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Tue Feb 19 19:35:12 2019 +0100
5.3 @@ -29,6 +29,13 @@
5.4 Rule.e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))]\<close>
5.5
5.6 text \<open>method solving the usecase\<close>
5.7 +partial_function (tailrec) diophant_equation :: "bool => int => bool"
5.8 + where
5.9 +"diophant_equation e_e v_v =
5.10 + (Repeat
5.11 + ((Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' False)) @@
5.12 + (Try (Calculate ''PLUS'')) @@
5.13 + (Try (Calculate ''TIMES''))) e_e)"
5.14 setup \<open>KEStore_Elems.add_mets
5.15 [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
5.16 (["Test","solve_diophant"],
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Feb 15 16:52:05 2019 +0100
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Feb 19 19:35:12 2019 +0100
6.3 @@ -527,6 +527,24 @@
6.4 errpats = [], nrls = Rule.Erls},
6.5 "empty_script")]
6.6 \<close>
6.7 +partial_function (tailrec) solve_system :: "bool list => real list => bool list"
6.8 + where
6.9 +"solve_system e_s v_s =
6.10 + (let e_1 = Take (hd e_s);
6.11 + e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.12 + ''isolate_bdvs'' False)) @@
6.13 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.14 + ''simplify_System'' False))) e_1;
6.15 + e_2 = Take (hd (tl e_s));
6.16 + e_2 = ((Substitute [e_1]) @@
6.17 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.18 + ''simplify_System_parenthesized'' False)) @@
6.19 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.20 + ''isolate_bdvs'' False)) @@
6.21 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]
6.22 + ''simplify_System'' False))) e_2;
6.23 + e__s = Take [e_1, e_2]
6.24 + in Try (Rewrite_Set ''order_system'' False) e__s) "
6.25 setup \<open>KEStore_Elems.add_mets
6.26 [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
6.27 (["EqSystem", "top_down_substitution", "2x2"],
6.28 @@ -582,6 +600,19 @@
6.29 errpats = [], nrls = Rule.Erls},
6.30 "empty_script")]
6.31 \<close>
6.32 +partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
6.33 + where
6.34 +"solve_system e_s v_s =
6.35 + (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
6.36 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
6.37 + ''simplify_System_parenthesized'' False)) @@
6.38 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
6.39 + ''isolate_bdvs'' False)) @@
6.40 + (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
6.41 + ''simplify_System_parenthesized'' False)) @@
6.42 + (Try (Rewrite_Set ''order_system'' False))) e_s
6.43 + in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.44 + [BOOL_LIST e__s, REAL_LIST v_s]))"
6.45 setup \<open>KEStore_Elems.add_mets
6.46 [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
6.47 (["EqSystem","normalise","2x2"],
6.48 @@ -605,6 +636,24 @@
6.49 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
6.50 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
6.51 \<close>
6.52 +partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
6.53 + where
6.54 +"solve_system e_s v_s =
6.55 + (let e__s =
6.56 + ((Try (Rewrite_Set ''norm_Rational'' False)) @@
6.57 + (Repeat (Rewrite ''commute_0_equality'' False)) @@
6.58 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
6.59 + (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
6.60 + ''simplify_System_parenthesized'' False)) @@
6.61 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
6.62 + (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
6.63 + ''isolate_bdvs_4x4'' False)) @@
6.64 + (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ),
6.65 + (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )]
6.66 + ''simplify_System_parenthesized'' False)) @@
6.67 + (Try (Rewrite_Set ''order_system'' False))) e_s
6.68 + in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
6.69 + [BOOL_LIST e__s, REAL_LIST v_s]))"
6.70 setup \<open>KEStore_Elems.add_mets
6.71 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
6.72 (["EqSystem","normalise","4x4"],
6.73 @@ -634,6 +683,22 @@
6.74 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
6.75 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
6.76 \<close>
6.77 +partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
6.78 + where
6.79 +"solve_system e_s v_s =
6.80 + (let e_1 = NTH 1 e_s;
6.81 + e_2 = Take (NTH 2 e_s);
6.82 + e_2 = ((Substitute [e_1]) @@
6.83 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
6.84 + (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
6.85 + ''simplify_System_parenthesized'' False)) @@
6.86 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
6.87 + (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
6.88 + ''isolate_bdvs'' False)) @@
6.89 + (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s),
6.90 + (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
6.91 + ''norm_Rational'' False))) e_2
6.92 + in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
6.93 setup \<open>KEStore_Elems.add_mets
6.94 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
6.95 (["EqSystem","top_down_substitution","4x4"],
7.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Fri Feb 15 16:52:05 2019 +0100
7.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Tue Feb 19 19:35:12 2019 +0100
7.3 @@ -103,6 +103,13 @@
7.4 crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
7.5 "empty_script")]
7.6 \<close>
7.7 +partial_function (tailrec) sort_program :: "int xlist => int xlist"
7.8 + where
7.9 +"sort_program unso =
7.10 + (let
7.11 + uns = Take (sort unso)
7.12 + in
7.13 + (Rewrite_Set ''ins_sort'' False) uns)"
7.14 setup \<open>KEStore_Elems.add_mets
7.15 [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
7.16 (["Programming","SORT","insertion"],
7.17 @@ -115,6 +122,24 @@
7.18 " (Rewrite_Set ''ins_sort'' False) uns" ^
7.19 " )")]
7.20 \<close>
7.21 +partial_function (tailrec) sort_program2 :: "int xlist => int xlist"
7.22 + where
7.23 +"sort_program2 unso =
7.24 + (let uns = Take (sort unso)
7.25 + in (Repeat
7.26 + ((Repeat (Rewrite ''xfoldr_Nil'' False)) Or
7.27 + (Repeat (Rewrite ''xfoldr_Cons'' False)) Or
7.28 + (Repeat (Rewrite ''ins_Nil'' False)) Or
7.29 + (Repeat (Rewrite ''ins_Cons'' False)) Or
7.30 + (Repeat (Rewrite ''sort_deff'' False)) Or
7.31 + (Repeat (Rewrite ''o_id'' False)) Or
7.32 + (Repeat (Rewrite ''o_assoc'' False)) Or
7.33 + (Repeat (Rewrite ''o_apply'' False)) Or
7.34 + (Repeat (Rewrite ''id_apply'' False)) Or
7.35 + (Repeat (Calculate ''le'' )) Or
7.36 + (Repeat (Rewrite ''If_def'' False)) Or
7.37 + (Repeat (Rewrite ''if_True'' False)) Or
7.38 + (Repeat (Rewrite ''if_False'' False)))) uns)"
7.39 setup \<open>KEStore_Elems.add_mets
7.40 [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
7.41 (["Programming","SORT","insertion_steps"],
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri Feb 15 16:52:05 2019 +0100
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Feb 19 19:35:12 2019 +0100
8.3 @@ -355,6 +355,11 @@
8.4 [["diff","integration","named"]]))]\<close>
8.5
8.6 (** methods **)
8.7 +partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
8.8 + where
8.9 +"integrate f_f v_v =
8.10 + (let t_t = Take (Integral f_f D v_v)
8.11 + in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
8.12 setup \<open>KEStore_Elems.add_mets
8.13 [Specify.prep_met thy "met_diffint" [] Celem.e_metID
8.14 (["diff","integration"],
8.15 @@ -365,6 +370,11 @@
8.16 " (let t_t = Take (Integral f_f D v_v) " ^
8.17 " in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))")]
8.18 \<close>
8.19 +partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
8.20 + where "intergrate_named f_f v_v F_F =
8.21 + (let t_t = Take (F_F v_v = Integral f_f D v_v)
8.22 + in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
8.23 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
8.24 setup \<open>KEStore_Elems.add_mets
8.25 [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
8.26 (["diff","integration","named"],
9.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri Feb 15 16:52:05 2019 +0100
9.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Tue Feb 19 19:35:12 2019 +0100
9.3 @@ -82,6 +82,20 @@
9.4 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
9.5 errpats = [], nrls = Rule.e_rls}, "empty_script")]
9.6 \<close>
9.7 +partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> bool"
9.8 + where
9.9 +"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
9.10 + (let X = Take X_eq;
9.11 + X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
9.12 + X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
9.13 + funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
9.14 + denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
9.15 + equ = (denom = (0::real));
9.16 + fun_arg = Take (lhs X');
9.17 + arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
9.18 + L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
9.19 + [''Test'',''solve_linear'']) [BOOL equ, STRING ''z''] \<comment> \<open>PROG string\<close>
9.20 + in X) "
9.21 setup \<open>KEStore_Elems.add_mets
9.22 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
9.23 (["SignalProcessing", "Z_Transform", "Inverse"],
9.24 @@ -105,6 +119,64 @@
9.25 " [BOOL equ, REAL z]) " ^
9.26 " in X)")]
9.27 \<close>
9.28 +(*
9.29 +Type unification failed: Clash of types "bool" and "_ itself"
9.30 +Type error in application: incompatible operand type
9.31 +Operator: Let (Take X_eq) :: (??'a itself \<Rightarrow> ??'b) \<Rightarrow> ??'b
9.32 +Operand:
9.33 + \<lambda>X. let X' = Rewrite ''ruleZY'' ...
9.34 +:
9.35 +:partial_function (tailrec) inverse_ztransform2 :: "bool \<Rightarrow> bool"
9.36 + where
9.37 +"inverse_ztransform X_eq = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
9.38 + (let X = Take X_eq;
9.39 + X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
9.40 + (num_orig::real) = get_numerator (rhs X');
9.41 + X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
9.42 + (X'_z::real) = lhs X';
9.43 + (zzz::real) = argument_in X'_z;
9.44 + (funterm::real) = rhs X'; \<comment> \<open>drop X' z = for equation solving\<close>
9.45 + (denom::real) = get_denominator funterm; \<comment> \<open>get_denominator\<close>
9.46 + (num::real) = get_numerator funterm; \<comment> \<open>get_numerator\<close>
9.47 + (equ::bool) = (denom = (0::real));
9.48 + (L_L::bool list) = (SubProblem (''PolyEq'',
9.49 + [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''],
9.50 + [''no_met''])
9.51 + [BOOL equ, REAL zzz]);
9.52 + (facs::real) = factors_from_solution L_L;
9.53 + (eql::real) = Take (num_orig / facs); \<comment> \<open>---\<close>
9.54 + (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; \<comment> \<open>---\<close>
9.55 + (eq::bool) = Take (eql = eqr); \<comment> \<open>Maybe possible to use HOLogic.mk_eq ??\<close>
9.56 + eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; \<comment> \<open>---\<close>
9.57 + eq = drop_questionmarks eq;
9.58 + (z1::real) = (rhs (NTH 1 L_L)); \<comment> \<open>prepare equation for a - eq_a therefor substitute z with solution 1 - z1\<close>
9.59 + (z2::real) = (rhs (NTH 2 L_L)); \<comment> \<open>---\<close>
9.60 + (eq_a::bool) = Take eq;
9.61 + eq_a = (Substitute [zzz=z1]) eq;
9.62 + eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;
9.63 + (sol_a::bool list) =
9.64 + (SubProblem (''Isac'',
9.65 + [''univariate'',''equation''],[''no_met''])
9.66 + [BOOL eq_a, REAL (A::real)]);
9.67 + (a::real) = (rhs(NTH 1 sol_a)); \<comment> \<open>---\<close>
9.68 + (eq_b::bool) = Take eq;
9.69 + eq_b = (Substitute [zzz=z2]) eq_b;
9.70 + eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b;
9.71 + (sol_b::bool list) =
9.72 + (SubProblem (''Isac'',
9.73 + [''univariate'',''equation''],[''no_met''])
9.74 + [BOOL eq_b, REAL (B::real)]);
9.75 + (b::real) = (rhs(NTH 1 sol_b)); \<comment> \<open>---\<close>
9.76 + eqr = drop_questionmarks eqr;
9.77 + (pbz::real) = Take eqr;
9.78 + pbz = ((Substitute [A=a, B=b]) pbz); \<comment> \<open>---\<close>
9.79 + pbz = Rewrite ''ruleYZ'' False pbz;
9.80 + pbz = drop_questionmarks pbz; \<comment> \<open>---\<close>
9.81 + (X_z::bool) = Take (X_z = pbz);
9.82 + (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z;
9.83 + n_eq = drop_questionmarks n_eq
9.84 +in n_eq)"
9.85 +*)
9.86 setup \<open>KEStore_Elems.add_mets
9.87 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
9.88 (["SignalProcessing", "Z_Transform", "Inverse"],
9.89 @@ -180,6 +252,42 @@
9.90 " n_eq = drop_questionmarks n_eq "^
9.91 "in n_eq)")]
9.92 \<close>
9.93 +(* same error as in inverse_ztransform2
9.94 +:partial_function (tailrec) inverse_ztransform3 :: "bool \<Rightarrow> bool"
9.95 + where
9.96 +"inverse_ztransform X_eq =
9.97 +(*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
9.98 +(let X = Take X_eq;
9.99 +(*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
9.100 + X' = Rewrite ''ruleZY'' False X;
9.101 +(* ?X' z*)
9.102 + (X'_z::real) = lhs X';
9.103 +(* z *)
9.104 + (zzz::real) = argument_in X'_z;
9.105 +(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
9.106 + (funterm::real) = rhs X';
9.107 +(*-----*)
9.108 + (pbz::real) = (SubProblem (''Isac'',
9.109 + [''partial_fraction'',''rational'',''simplification''],
9.110 + [''simplification'',''of_rationals'',''to_partial_fraction''])
9.111 +(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
9.112 + [REAL funterm, REAL zzz]);
9.113 +(*-----*)
9.114 +(*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
9.115 + (pbz_eq::bool) = Take (X'_z = pbz);
9.116 +(*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
9.117 + pbz_eq = Rewrite ''ruleYZ'' False pbz_eq;
9.118 +(* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
9.119 + pbz_eq = drop_questionmarks pbz_eq;
9.120 +(*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
9.121 + (X_zeq::bool) = Take (X_z = rhs pbz_eq);
9.122 +(*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
9.123 + n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq;
9.124 +(* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
9.125 + n_eq = drop_questionmarks n_eq
9.126 +(*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
9.127 +in n_eq) "
9.128 +*)
9.129 setup \<open>KEStore_Elems.add_mets
9.130 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
9.131 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
10.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri Feb 15 16:52:05 2019 +0100
10.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Feb 19 19:35:12 2019 +0100
10.3 @@ -140,6 +140,19 @@
10.4 "empty_script")]
10.5 \<close>
10.6 (* ansprechen mit ["LinEq","solve_univar_equation"] *)
10.7 +partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
10.8 + where
10.9 +"solve_linear_equation e_e v_v =
10.10 +(let e_e =((Try (Rewrite ''all_left'' False)) @@
10.11 + (Try (Repeat (Rewrite ''makex1_x'' False))) @@
10.12 + (Try (Rewrite_Set ''expand_binoms'' False)) @@
10.13 + (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)]
10.14 + ''make_ratpoly_in'' False))) @@
10.15 + (Try (Repeat (Rewrite_Set ''LinPoly_simplify'' False))))e_e;
10.16 + e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]
10.17 + ''LinEq_simplify'' True)) @@
10.18 + (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e
10.19 + in Or_to_List e_e)"
10.20 setup \<open>KEStore_Elems.add_mets
10.21 [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
10.22 (["LinEq","solve_lineq_equation"],
11.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Fri Feb 15 16:52:05 2019 +0100
11.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Tue Feb 19 19:35:12 2019 +0100
11.3 @@ -39,6 +39,13 @@
11.4 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]]))]\<close>
11.5
11.6 (** methods **)
11.7 +partial_function (tailrec) solve_log :: "bool \<Rightarrow> real \<Rightarrow> bool list"
11.8 + where
11.9 +"solve_log e_e v_v =
11.10 +(let e_e = ((Rewrite ''equality_power'' False) @@
11.11 + (Rewrite ''exp_invers_log'' False) @@
11.12 + (Rewrite_Set ''norm_Poly'' False)) e_e
11.13 + in [e_e])"
11.14 setup \<open>KEStore_Elems.add_mets
11.15 [Specify.prep_met thy "met_equ_log" [] Celem.e_metID
11.16 (["Equation","solve_log"],
12.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri Feb 15 16:52:05 2019 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Tue Feb 19 19:35:12 2019 +0100
12.3 @@ -22,6 +22,8 @@
12.4 consts
12.5 factors_from_solution :: "bool list => real"
12.6 drop_questionmarks :: "'a => 'a"
12.7 + A :: real \<comment> \<open>PROG redesign (Substitute [A = a, B = b]) pbz ?\<close>
12.8 + B :: real \<comment> \<open>PROG redesign (Substitute [A = a, B = b]) pbz ?\<close>
12.9
12.10 text \<open>these might be used for variants of fac_from_sol\<close>
12.11 ML \<open>
12.12 @@ -222,6 +224,47 @@
12.13 \<close>
12.14
12.15 (* current version, error outcommented *)
12.16 +partial_function (tailrec) partial_fraction :: "real \<Rightarrow> real \<Rightarrow> real"
12.17 + where
12.18 +"partial_fraction f_f zzz = \<comment> \<open>([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))\<close>
12.19 +(let f_f = Take f_f; \<comment> \<open>num_orig = 3\<close>
12.20 + num_orig = get_numerator f_f; \<comment> \<open>([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)\<close>
12.21 + f_f = (Rewrite_Set ''norm_Rational'' False) f_f; \<comment> \<open>denom = -1 + -2 * z + 8 * z ^^^ 2\<close>
12.22 + denom = get_denominator f_f; \<comment> \<open>equ = -1 + -2 * z + 8 * z ^^^ 2 = 0\<close>
12.23 + equ = denom = (0::real);
12.24 + \<comment> \<open>----- ([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)\<close>
12.25 + L_L = SubProblem (''PolyEq'', \<comment> \<open>([2], Res), [z = 1 / 2, z = -1 / 4\<close>
12.26 + [''abcFormula'', ''degree_2'', ''polynomial'', ''univariate'', ''equation''],
12.27 + [''no_met'']) [BOOL equ, REAL zzz]; \<comment> \<open>facs: (z - 1 / 2) * (z - -1 / 4)\<close>
12.28 + facs = factors_from_solution L_L; \<comment> \<open>([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4))\<close>
12.29 + eql = Take (num_orig / facs); \<comment> \<open>([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)\<close>
12.30 + eqr = (Try (Rewrite_Set ''ansatz_rls'' False)) eql;
12.31 + \<comment> \<open>([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)\<close>
12.32 + eq = Take (eql = eqr); \<comment> \<open>([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)\<close>
12.33 + eq = (Try (Rewrite_Set ''equival_trans'' False)) eq;
12.34 + \<comment> \<open>eq = 3 = A * (z - -1 / 4) + B * (z - 1 / 2)\<close>
12.35 + eq = drop_questionmarks eq; \<comment> \<open>z1 = 1 / 2)\<close>
12.36 + z1 = rhs (NTH 1 L_L); \<comment> \<open>z2 = -1 / 4\<close>
12.37 + z2 = rhs (NTH 2 L_L); \<comment> \<open>([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)\<close>
12.38 + eq_a = Take eq; \<comment> \<open>([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)\<close>
12.39 + eq_a = Substitute [zzz = z1] eq; \<comment> \<open>([6], Res), 3 = 3 * A / 4\<close>
12.40 + eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;
12.41 +\<comment> \<open>----- ([7], Pbl), solve (3 = 3 * A / 4, A)\<close>
12.42 + \<comment> \<open>([7], Res), [A = 4]\<close>
12.43 + sol_a = SubProblem (''Isac'', [''univariate'',''equation''], [''no_met''])
12.44 + [BOOL eq_a, REAL (A::real)] ; \<comment> \<open>a = 4\<close>
12.45 + a = rhs (NTH 1 sol_a); \<comment> \<open>([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)\<close>
12.46 + eq_b = Take eq; \<comment> \<open>([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)\<close>
12.47 + eq_b = Substitute [zzz = z2] eq_b; \<comment> \<open>([9], Res), 3 = -3 * B / 4\<close>
12.48 + eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; \<comment> \<open>([10], Pbl), solve (3 = -3 * B / 4, B)\<close>
12.49 + sol_b = SubProblem (''Isac'', \<comment> \<open>([10], Res), [B = -4]\<close>
12.50 + [''univariate'',''equation''], [''no_met''])
12.51 + [BOOL eq_b, REAL (B::real)]; \<comment> \<open>b = -4\<close>
12.52 + b = rhs (NTH 1 sol_b); \<comment> \<open>eqr = A / (z - 1 / 2) + B / (z - -1 / 4)\<close>
12.53 + eqr = drop_questionmarks eqr; \<comment> \<open>([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)\<close>
12.54 + pbz = Take eqr; \<comment> \<open>([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
12.55 + pbz = Substitute [A = a, B = b] pbz \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
12.56 +in pbz) "
12.57 setup \<open>KEStore_Elems.add_mets
12.58 [Specify.prep_met @{theory} "met_partial_fraction" [] Celem.e_metID
12.59 (["simplification","of_rationals","to_partial_fraction"],
12.60 @@ -316,8 +359,4 @@
12.61 *)
12.62 \<close>
12.63
12.64 -
12.65 -
12.66 -subsection \<open>\<close>
12.67 -
12.68 end
12.69 \ No newline at end of file
13.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Feb 15 16:52:05 2019 +0100
13.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Feb 19 19:35:12 2019 +0100
13.3 @@ -1609,14 +1609,9 @@
13.4 [["simplification","for_polynomials"]]))]\<close>
13.5
13.6 (** methods **)
13.7 -(*-----
13.8 -consts
13.9 - norm_Poly :: ID
13.10 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
13.11 where
13.12 - "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
13.13 -
13.14 ------*)
13.15 +"simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
13.16 setup \<open>KEStore_Elems.add_mets
13.17 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
13.18 (["simplification","for_polynomials"],
14.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri Feb 15 16:52:05 2019 +0100
14.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Feb 19 19:35:12 2019 +0100
14.3 @@ -974,6 +974,16 @@
14.4 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
14.5 "empty_script")]
14.6 \<close>
14.7 +partial_function (tailrec) normalize_poly_eq :: "bool \<Rightarrow> real \<Rightarrow> bool"
14.8 + where
14.9 +"normalize_poly_eq e_e v_v =
14.10 +(let e_e = ((Try (Rewrite ''all_left'' False)) @@
14.11 + (Try (Repeat (Rewrite ''makex1_x'' False))) @@
14.12 + (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@
14.13 + (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in'' False))) @@
14.14 + (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e
14.15 + in SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
14.16 + [BOOL e_e, REAL v_v])"
14.17 setup \<open>KEStore_Elems.add_mets
14.18 [Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID
14.19 (["PolyEq","normalise_poly"],
14.20 @@ -992,6 +1002,11 @@
14.21 " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
14.22 " [BOOL e_e, REAL v_v]))")]
14.23 \<close>
14.24 +partial_function (tailrec) solve_poly_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.25 + where
14.26 +"solve_poly_equ e_e v_v =
14.27 +(let e_e = (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d0_polyeq_simplify'' False)) e_e
14.28 + in Or_to_List e_e)"
14.29 setup \<open>KEStore_Elems.add_mets
14.30 [Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID
14.31 (["PolyEq","solve_d0_polyeq_equation"],
14.32 @@ -1006,6 +1021,13 @@
14.33 " ''d0_polyeq_simplify'' False))) e_e " ^
14.34 " in ((Or_to_List e_e)::bool list))")]
14.35 \<close>
14.36 +partial_function (tailrec) solve_poly_eq1 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.37 + where "solve_poly_eq1 e_e v_v =
14.38 +(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'' True)) @@
14.39 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.40 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.41 + L_L = Or_to_List e_e
14.42 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.43 setup \<open>KEStore_Elems.add_mets
14.44 [Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID
14.45 (["PolyEq","solve_d1_polyeq_equation"],
14.46 @@ -1023,6 +1045,16 @@
14.47 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
14.48 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
14.49 \<close>
14.50 +partial_function (tailrec) solve_poly_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.51 + where
14.52 +"solve_poly_equ2 e_e v_v =
14.53 + (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'' True)) @@
14.54 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.55 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d1_polyeq_simplify'' True)) @@
14.56 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.57 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.58 + L_L = Or_to_List e_e
14.59 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.60 setup \<open>KEStore_Elems.add_mets
14.61 [Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID
14.62 (["PolyEq","solve_d2_polyeq_equation"],
14.63 @@ -1043,6 +1075,16 @@
14.64 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
14.65 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
14.66 \<close>
14.67 +partial_function (tailrec) solve_poly_equ0 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.68 + where "solve_poly_equ0 e_e v_v =
14.69 + (let
14.70 + e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_bdv_only_simplify'' True)) @@
14.71 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.72 + (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'' True)) @@
14.73 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.74 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.75 + L_L = Or_to_List e_e
14.76 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.77 setup \<open>KEStore_Elems.add_mets
14.78 [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID
14.79 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
14.80 @@ -1063,6 +1105,15 @@
14.81 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
14.82 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
14.83 \<close>
14.84 +partial_function (tailrec) solve_poly_equ_sqrt :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.85 + where
14.86 +"solve_poly_equ_sqrt e_e v_v =
14.87 + (let
14.88 + e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_sq_only_simplify'' True)) @@
14.89 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.90 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.91 + L_L = Or_to_List e_e
14.92 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.93 setup \<open>KEStore_Elems.add_mets
14.94 [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID
14.95 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
14.96 @@ -1080,6 +1131,13 @@
14.97 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
14.98 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
14.99 \<close>
14.100 +partial_function (tailrec) solve_poly_equ_pq :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.101 + where "solve_poly_equ_pq e_e v_v =
14.102 + (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_pqFormula_simplify'' True)) @@
14.103 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.104 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.105 + L_L = Or_to_List e_e
14.106 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.107 setup \<open>KEStore_Elems.add_mets
14.108 [Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID
14.109 (["PolyEq","solve_d2_polyeq_pq_equation"],
14.110 @@ -1097,6 +1155,14 @@
14.111 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
14.112 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
14.113 \<close>
14.114 +partial_function (tailrec) solve_poly_equ_abc :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.115 + where
14.116 +"solve_poly_equ_abc e_e v_v =
14.117 + (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_abcFormula_simplify'' True)) @@
14.118 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.119 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.120 + L_L = Or_to_List e_e
14.121 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.122 setup \<open>KEStore_Elems.add_mets
14.123 [Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID
14.124 (["PolyEq","solve_d2_polyeq_abc_equation"],
14.125 @@ -1114,6 +1180,17 @@
14.126 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
14.127 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
14.128 \<close>
14.129 +partial_function (tailrec) solve_poly_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.130 + where "solve_poly_equ3 e_e v_v =
14.131 + (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d3_polyeq_simplify'' True)) @@
14.132 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.133 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''d2_polyeq_simplify'' True)) @@
14.134 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.135 + (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''d1_polyeq_simplify'' True)) @@
14.136 + (Try (Rewrite_Set ''polyeq_simplify'' False)) @@
14.137 + (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;
14.138 + L_L = Or_to_List e_e
14.139 + in Check_elementwise L_L {(v_v::real). Assumptions})"
14.140 setup \<open>KEStore_Elems.add_mets
14.141 [Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID
14.142 (["PolyEq","solve_d3_polyeq_equation"],
14.143 @@ -1140,6 +1217,21 @@
14.144 (*.solves all expanded (ie. normalised) terms of degree 2.*)
14.145 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
14.146 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
14.147 +partial_function (tailrec) solve_by_completing_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
14.148 + where
14.149 +"solve_by_completing_square e_e v_v =
14.150 + (let e_e =
14.151 + ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''cancel_leading_coeff'' True)) @@
14.152 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''complete_square'' True)) @@
14.153 + (Try (Rewrite ''square_explicit1'' False)) @@
14.154 + (Try (Rewrite ''square_explicit2'' False)) @@
14.155 + (Rewrite ''root_plus_minus'' True) @@
14.156 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit1'' False))) @@
14.157 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit2'' False))) @@
14.158 + (Try (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''bdv_explicit3'' False))) @@
14.159 + (Try (Rewrite_Set ''calculate_RootRat'' False)) @@
14.160 + (Try (Repeat (Calculate ''SQRT'')))) e_e
14.161 + in Or_to_List e_e)"
14.162 setup \<open>KEStore_Elems.add_mets
14.163 [Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID
14.164 (["PolyEq","complete_square"],
15.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri Feb 15 16:52:05 2019 +0100
15.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Feb 19 19:35:12 2019 +0100
15.3 @@ -475,6 +475,12 @@
15.4 SOME "Probe e_e w_w", [["probe","fuer_bruch"]]))]\<close>
15.5
15.6 (** methods **)
15.7 +partial_function (tailrec) simplify :: "real \<Rightarrow> real"
15.8 + where
15.9 +"simplify t_t =
15.10 + ((Repeat((Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
15.11 + (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
15.12 + (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
15.13 setup \<open>KEStore_Elems.add_mets
15.14 [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID
15.15 (["simplification","for_polynomials","with_minus"],
15.16 @@ -503,6 +509,13 @@
15.17 " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
15.18 " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)")]
15.19 \<close>
15.20 +partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
15.21 + where
15.22 +"simplify t_t =
15.23 + ((Repeat((Try (Rewrite_Set ''klammern_aufloesen'' False)) @@
15.24 + (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
15.25 + (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
15.26 + (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
15.27 setup \<open>KEStore_Elems.add_mets
15.28 [Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID
15.29 (["simplification","for_polynomials","with_parentheses"],
15.30 @@ -519,6 +532,16 @@
15.31 " (Try (Rewrite_Set ''fasse_zusammen'' False)) @@ " ^
15.32 " (Try (Rewrite_Set ''verschoenere'' False)))) t_t)")]
15.33 \<close>
15.34 +partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
15.35 + where
15.36 +"simplify t_t =
15.37 + ((Repeat((Try (Rewrite_Set ''klammern_ausmultiplizieren'' False)) @@
15.38 + (Try (Rewrite_Set ''discard_parentheses'' False)) @@
15.39 + (Try (Rewrite_Set ''ordne_monome'' False)) @@
15.40 + (Try (Rewrite_Set ''klammern_aufloesen'' False)) @@
15.41 + (Try (Rewrite_Set ''ordne_alphabetisch'' False)) @@
15.42 + (Try (Rewrite_Set ''fasse_zusammen'' False)) @@
15.43 + (Try (Rewrite_Set ''verschoenere'' False)))) t_t)"
15.44 setup \<open>KEStore_Elems.add_mets
15.45 [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID
15.46 (["simplification","for_polynomials","with_parentheses_mult"],
15.47 @@ -543,6 +566,14 @@
15.48 errpats = [], nrls = Rule.Erls},
15.49 "empty_script")]
15.50 \<close>
15.51 +partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
15.52 + where
15.53 +"mache_probe e_e w_w =
15.54 + (let e_e = Take e_e;
15.55 + e_e = Substitute w_w e_e
15.56 + in (Repeat ((Try (Repeat (Calculate ''TIMES''))) @@
15.57 + (Try (Repeat (Calculate ''PLUS'' ))) @@
15.58 + (Try (Repeat (Calculate ''MINUS''))))) e_e)"
15.59 setup \<open>KEStore_Elems.add_mets
15.60 [Specify.prep_met thy "met_probe_poly" [] Celem.e_metID
15.61 (["probe","fuer_polynom"],
16.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Fri Feb 15 16:52:05 2019 +0100
16.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Feb 19 19:35:12 2019 +0100
16.3 @@ -197,6 +197,16 @@
16.4 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
16.5 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script")]
16.6 \<close>
16.7 +partial_function (tailrec) solve_rational_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
16.8 + where
16.9 +"solve_rational_equ e_e v_v =
16.10 +(let e_e = ((Repeat(Try (Rewrite_Set ''RatEq_simplify'' True))) @@
16.11 + (Repeat(Try (Rewrite_Set ''norm_Rational'' False))) @@
16.12 + (Repeat(Try (Rewrite_Set ''add_fractions_p'' False))) @@
16.13 + (Repeat(Try (Rewrite_Set ''RatEq_eliminate'' True)))) e_e;
16.14 + L_L = SubProblem (''RatEq'', [''univariate'', ''equation''], [''no_met''])
16.15 + [BOOL e_e, REAL v_v]
16.16 + in Check_elementwise L_L {(v_v::real). Assumptions})"
16.17 setup \<open>KEStore_Elems.add_mets
16.18 [Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
16.19 (["RatEq", "solve_rat_equation"],
17.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Feb 15 16:52:05 2019 +0100
17.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Feb 19 19:35:12 2019 +0100
17.3 @@ -897,6 +897,21 @@
17.4 section \<open>A methods for simplification of rationals\<close>
17.5 (*WN061025 this methods script is copied from (auto-generated) script
17.6 of norm_Rational in order to ease repair on inform*)
17.7 +partial_function (tailrec) simplify :: "real \<Rightarrow> real"
17.8 + where
17.9 +"simplify t_t =
17.10 + ((Try (Rewrite_Set ''discard_minus'' False) @@
17.11 + Try (Rewrite_Set ''rat_mult_poly'' False) @@
17.12 + Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@
17.13 + Try (Rewrite_Set ''cancel_p_rls'' False) @@
17.14 + (Repeat
17.15 + ((Try (Rewrite_Set ''add_fractions_p_rls'' False) @@
17.16 + Try (Rewrite_Set ''rat_mult_div_pow'' False) @@
17.17 + Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@
17.18 + Try (Rewrite_Set ''cancel_p_rls'' False) @@
17.19 + Try (Rewrite_Set ''rat_reduce_1'' False)))) @@
17.20 + Try (Rewrite_Set ''discard_parentheses1'' False))
17.21 + t_t)"
17.22 setup \<open>KEStore_Elems.add_mets
17.23 [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
17.24 (["simplification","of_rationals"],
18.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri Feb 15 16:52:05 2019 +0100
18.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Feb 19 19:35:12 2019 +0100
18.3 @@ -521,6 +521,16 @@
18.4 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script")]
18.5 \<close>
18.6 (*-- normalise 20.10.02 --*)
18.7 +partial_function (tailrec) norm_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.8 + where
18.9 +"norm_sqrt_equ e_e v_v =
18.10 + (let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@
18.11 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.12 + (Try (Rewrite_Set ''rooteq_simplify'' True)) @@
18.13 + (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@
18.14 + (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e
18.15 + in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
18.16 + [BOOL e_e, REAL v_v])"
18.17 setup \<open>KEStore_Elems.add_mets
18.18 [Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID
18.19 (["RootEq","norm_sq_root_equation"],
18.20 @@ -541,6 +551,23 @@
18.21 " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
18.22 " [''no_met'']) [BOOL e_e, REAL v_v])))")]
18.23 \<close>
18.24 +partial_function (tailrec) solve_sqrt_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.25 + where
18.26 +"solve_sqrt_equ e_e v_v =
18.27 + (let
18.28 + e_e =
18.29 + ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''sqrt_isolate'' True)) @@
18.30 + (Try (Rewrite_Set ''rooteq_simplify'' True)) @@
18.31 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.32 + (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@
18.33 + (Try (Rewrite_Set ''rooteq_simplify'' True)) ) e_e;
18.34 + L_L =
18.35 + (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))
18.36 + then SubProblem (''RootEq'', [''normalise'', ''rootX'', ''univariate'', ''equation''],
18.37 + [''no_met'']) [BOOL e_e, REAL v_v]
18.38 + else SubProblem (''RootEq'',[''univariate'',''equation''],
18.39 + [''no_met'']) [BOOL e_e, REAL v_v])
18.40 + in Check_elementwise L_L {(v_v::real). Assumptions})"
18.41 setup \<open>KEStore_Elems.add_mets
18.42 [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID
18.43 (["RootEq","solve_sq_root_equation"],
18.44 @@ -568,6 +595,20 @@
18.45 "in Check_elementwise L_L {(v_v::real). Assumptions})")]
18.46 \<close>
18.47 (*-- right 28.08.02 --*)
18.48 +partial_function (tailrec) solve_sqrt_equ_right :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.49 + where "solve_sqrt_equ_right e_e v_v =
18.50 +(let e_e =
18.51 + ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''r_sqrt_isolate'' False)) @@
18.52 + (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
18.53 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.54 + (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@
18.55 + (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e
18.56 + in
18.57 + if (rhs e_e) is_sqrtTerm_in v_v
18.58 + then SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''],
18.59 + [''no_met'']) [BOOL e_e, REAL v_v]
18.60 + else SubProblem (''RootEq'',[''univariate'', ''equation''],
18.61 + [''no_met'']) [BOOL e_e, REAL v_v])"
18.62 setup \<open>KEStore_Elems.add_mets
18.63 [Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID
18.64 (["RootEq","solve_right_sq_root_equation"],
18.65 @@ -590,6 +631,21 @@
18.66 " [''no_met'']) [BOOL e_e, REAL v_v])))")]
18.67 \<close>
18.68 (*-- left 28.08.02 --*)
18.69 +partial_function (tailrec) solve_sqrt_equ_left :: "bool \<Rightarrow> real \<Rightarrow> bool list"
18.70 + where
18.71 +"solve_sqrt_equ_left e_e v_v =
18.72 +(let e_e =
18.73 + ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''l_sqrt_isolate'' False)) @@
18.74 + (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
18.75 + (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@
18.76 + (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@
18.77 + (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e
18.78 + in
18.79 + if (lhs e_e) is_sqrtTerm_in v_v
18.80 + then SubProblem (''RootEq'', [''normalise'',''rootX'',''univariate'',''equation''],
18.81 + [''no_met'']) [BOOL e_e, REAL v_v]
18.82 + else SubProblem (''RootEq'',[''univariate'',''equation''],
18.83 + [''no_met'']) [BOOL e_e, REAL v_v])"
18.84 setup \<open>KEStore_Elems.add_mets
18.85 [Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID
18.86 (["RootEq","solve_left_sq_root_equation"],
19.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Fri Feb 15 16:52:05 2019 +0100
19.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Feb 19 19:35:12 2019 +0100
19.3 @@ -155,6 +155,15 @@
19.4 crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script")]
19.5 \<close>
19.6 (*-- left 20.10.02 --*)
19.7 +partial_function (tailrec) solve_rootrat_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
19.8 + where
19.9 +"solve_rootrat_equ e_e v_v =
19.10 +(let e_e = ((Try (Rewrite_Set ''expand_rootbinoms'' False)) @@
19.11 + (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
19.12 + (Try (Rewrite_Set ''make_rooteq'' False)) @@
19.13 + (Try (Rewrite_Set ''rooteq_simplify'' False)) @@
19.14 + (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'' False))) e_e
19.15 + in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
19.16 setup \<open>KEStore_Elems.add_mets
19.17 [Specify.prep_met thy "met_rootrateq_elim" [] Celem.e_metID
19.18 (["RootRatEq","elim_rootrat_equation"],
20.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri Feb 15 16:52:05 2019 +0100
20.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Feb 19 19:35:12 2019 +0100
20.3 @@ -861,14 +861,20 @@
20.4
20.5 section \<open>methods\<close>
20.6 subsection \<open>differentiate\<close>
20.7 -partial_function (tailrec) dummy1 :: "real \<Rightarrow> real"
20.8 - where "dummy1 xxx = xxx"
20.9 setup \<open>KEStore_Elems.add_mets
20.10 [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
20.11 (["Test"], [],
20.12 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
20.13 crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")]
20.14 \<close>
20.15 +partial_function (tailrec) solve_linear :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.16 + where
20.17 +"solve_linear e_e v_v =
20.18 + (let e_e =
20.19 + Repeat
20.20 + (((Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
20.21 + (Rewrite_Set ''Test_simplify'' False))) e_e
20.22 + in [e_e])"
20.23 setup \<open>KEStore_Elems.add_mets
20.24 [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
20.25 (["Test","solve_linear"],
20.26 @@ -886,8 +892,21 @@
20.27 " in [e_e::bool])")]
20.28 \<close>
20.29 subsection \<open>root equation\<close>
20.30 -partial_function (tailrec) dummy2 :: "real \<Rightarrow> real"
20.31 - where "dummy2 xxx = xxx"
20.32 +partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.33 + where
20.34 +"solve_root_equ e_e v_v =
20.35 + (let e_e =
20.36 + ((While (contains_root e_e) Do
20.37 + ((Rewrite ''square_equation_left'' True) @@
20.38 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.39 + (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.40 + (Try (Rewrite_Set ''isolate_root'' False)) @@
20.41 + (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.42 + (Try (Rewrite_Set ''norm_equation'' False)) @@
20.43 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.44 + (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' False) @@
20.45 + (Try (Rewrite_Set ''Test_simplify'' False))) e_e
20.46 + in [e_e])"
20.47 setup \<open>KEStore_Elems.add_mets
20.48 [Specify.prep_met thy "met_test_sqrt" [] Celem.e_metID
20.49 (*root-equation, version for tests before 8.01.01*)
20.50 @@ -917,8 +936,24 @@
20.51 " e_e" ^
20.52 " in [e_e::bool])")]
20.53 \<close>
20.54 -partial_function (tailrec) dummy3 :: "real \<Rightarrow> real"
20.55 - where "dummy3 xxx = xxx"
20.56 +(* UNUSED?
20.57 +partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.58 + where "solve_root_equ e_e v_v =
20.59 +(let e_e =
20.60 + ((While (contains_root e_e) Do
20.61 + ((Rewrite ''square_equation_left'' True) @@
20.62 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.63 + (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.64 + (Try (Rewrite_Set ''isolate_root'' False)) @@
20.65 + (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.66 + (Try (Rewrite_Set ''norm_equation'' False)) @@
20.67 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.68 + (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@
20.69 + (Try (Rewrite_Set ''Test_simplify'' False)))
20.70 + e_e;
20.71 + (L_L::bool list) = Tac ''subproblem_equation_dummy'';
20.72 + L_L = Tac ''solve_equation_dummy''
20.73 + in Check_elementwise L_L {(v_v::real). Assumptions}) "
20.74 setup \<open>KEStore_Elems.add_mets
20.75 [Specify.prep_met thy "met_test_sqrt2" [] Celem.e_metID
20.76 (*root-equation ... for test-*.sml until 8.01*)
20.77 @@ -947,6 +982,7 @@
20.78 " L_L = Tac solve_equation_dummy " ^
20.79 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
20.80 \<close>
20.81 +*)
20.82
20.83 partial_function (tailrec) solve_root_equation ::
20.84 "bool \<Rightarrow> real \<Rightarrow> bool list"
20.85 @@ -954,10 +990,8 @@
20.86 (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
20.87 (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.88 (L_L::bool list) =
20.89 - (SubProblem (''TestX'',
20.90 - [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.91 - [''Test'', ''solve_linear''])
20.92 - [BOOL e_e, REAL v_v])
20.93 + SubProblem (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.94 + [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
20.95 in Check_elementwise L_L {(v_v::real). Assumptions})"
20.96
20.97 (* ^^^used for test/../Minisubpbl/
20.98 @@ -991,8 +1025,20 @@
20.99 " [BOOL e_e, REAL v_v]) " ^
20.100 " in Check_elementwise L_L {(v_v::real). Assumptions}) ")]
20.101 \<close>
20.102 -partial_function (tailrec) dummy7 :: "real \<Rightarrow> real"
20.103 - where "dummy7 xxx = xxx"
20.104 +partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.105 + where "solve_root_equ e_e v_v =
20.106 +(let e_e =
20.107 + ((While (contains_root e_e) Do
20.108 + ((Rewrite ''square_equation_left'' True) @@
20.109 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.110 + (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.111 + (Try (Rewrite_Set ''isolate_root'' False)) @@
20.112 + (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.113 + (Try (Rewrite_Set ''norm_equation'' False)) @@
20.114 + (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.115 + L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],
20.116 + [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v]
20.117 + in Check_elementwise L_L {(v_v::real). Assumptions}) "
20.118 setup \<open>KEStore_Elems.add_mets
20.119 [Specify.prep_met thy "met_test_eq1" [] Celem.e_metID
20.120 (*root-equation1:*)
20.121 @@ -1019,8 +1065,22 @@
20.122 " [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^
20.123 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
20.124 \<close>
20.125 -partial_function (tailrec) dummy8 :: "real \<Rightarrow> real"
20.126 - where "dummy8 xxx = xxx"
20.127 +partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.128 + where
20.129 +"solve_root_equ e_e v_v =
20.130 + (let e_e =
20.131 + ((While (contains_root e_e) Do
20.132 + (((Rewrite ''square_equation_left'' True) Or
20.133 + (Rewrite ''square_equation_right'' True)) @@
20.134 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.135 + (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.136 + (Try (Rewrite_Set ''isolate_root'' False)) @@
20.137 + (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.138 + (Try (Rewrite_Set ''norm_equation'' False)) @@
20.139 + (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.140 + L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''],
20.141 + [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v]
20.142 + in Check_elementwise L_L {(v_v::real). Assumptions})"
20.143 setup \<open>KEStore_Elems.add_mets
20.144 [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
20.145 (*root-equation2*)
20.146 @@ -1048,8 +1108,22 @@
20.147 " [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^
20.148 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
20.149 \<close>
20.150 -partial_function (tailrec) dummy9 :: "real \<Rightarrow> real"
20.151 - where "dummy9 xxx = xxx"
20.152 +partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.153 + where
20.154 +"solve_root_equ e_e v_v =
20.155 +(let e_e =
20.156 + ((While (contains_root e_e) Do
20.157 + (((Rewrite ''square_equation_left'' True) Or
20.158 + (Rewrite ''square_equation_right'' True)) @@
20.159 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.160 + (Try (Rewrite_Set ''rearrange_assoc'' False)) @@
20.161 + (Try (Rewrite_Set ''isolate_root'' False)) @@
20.162 + (Try (Rewrite_Set ''Test_simplify'' False)))) @@
20.163 + (Try (Rewrite_Set ''norm_equation'' False)) @@
20.164 + (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
20.165 + L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
20.166 + [''no_met'']) [BOOL e_e, REAL v_v]
20.167 + in Check_elementwise L_L {(v_v::real). Assumptions})"
20.168 setup \<open>KEStore_Elems.add_mets
20.169 [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
20.170 (*root-equation*)
20.171 @@ -1077,8 +1151,15 @@
20.172 " [''no_met'']) [BOOL e_e, REAL v_v])" ^
20.173 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
20.174 \<close>
20.175 -partial_function (tailrec) dummy10 :: "real \<Rightarrow> real"
20.176 - where "dummy10 xxx = xxx"
20.177 +partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.178 + where
20.179 +"solve_plain_square e_e v_v =
20.180 + (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@
20.181 + (Try (Rewrite_Set ''Test_simplify'' False)) @@
20.182 + ((Rewrite ''square_equality_0'' False) Or
20.183 + (Rewrite ''square_equality'' True)) @@
20.184 + (Try (Rewrite_Set ''tval_rls'' False))) e_e
20.185 + in Or_to_List e_e)"
20.186 setup \<open>KEStore_Elems.add_mets
20.187 [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
20.188 (*solve_plain_square*)
20.189 @@ -1101,8 +1182,13 @@
20.190 " in ((Or_to_List e_e)::bool list))")]
20.191 \<close>
20.192 subsection \<open>polynomial equation\<close>
20.193 -partial_function (tailrec) dummy11 :: "real \<Rightarrow> real"
20.194 - where "dummy11 xxx = xxx"
20.195 +partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list"
20.196 + where
20.197 +"norm_univariate_equ e_e v_v =
20.198 + (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@
20.199 + (Try (Rewrite_Set ''Test_simplify'' False))) e_e
20.200 + in SubProblem (''Test'', [''univariate'', ''equation'', ''test''],
20.201 + [''no_met'']) [BOOL e_e, REAL v_v])"
20.202 setup \<open>KEStore_Elems.add_mets
20.203 [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
20.204 (["Test","norm_univar_equation"],
20.205 @@ -1118,8 +1204,12 @@
20.206 " [''no_met'']) [BOOL e_e, REAL v_v]))")]
20.207 \<close>
20.208 subsection \<open>diophantine equation\<close>
20.209 -partial_function (tailrec) dummy12 :: "real \<Rightarrow> real"
20.210 - where "dummy12 xxx = xxx"
20.211 +partial_function (tailrec) test_simplify :: "int \<Rightarrow> int"
20.212 + where
20.213 +"test_simplify t_t =
20.214 + (Repeat
20.215 + ((Try (Calculate ''PLUS'')) @@
20.216 + (Try (Calculate ''TIMES''))) t_t)"
20.217 setup \<open>KEStore_Elems.add_mets
20.218 [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
20.219 (["Test","intsimp"],
21.1 --- a/src/Tools/isac/ProgLang/Script.thy Fri Feb 15 16:52:05 2019 +0100
21.2 +++ b/src/Tools/isac/ProgLang/Script.thy Tue Feb 19 19:35:12 2019 +0100
21.3 @@ -17,6 +17,8 @@
21.4 BOOL :: "bool => arg"
21.5 BOOL_LIST :: "(bool list) => arg"
21.6 REAL_REAL :: "(real => real) => arg"
21.7 + STRING :: "(char list) => arg"
21.8 + STRING_LIST :: "(char list list) => arg"
21.9
21.10 (*tactics*)
21.11 Rewrite :: "[char list, bool, 'a] => 'a"
22.1 --- a/src/Tools/isac/TODO.thy Fri Feb 15 16:52:05 2019 +0100
22.2 +++ b/src/Tools/isac/TODO.thy Tue Feb 19 19:35:12 2019 +0100
22.3 @@ -1,34 +1,65 @@
22.4 -theory TODO imports Pure begin
22.5 -
22.6 (* Title: todo's for isac core
22.7 Author: Walther Neuper 111013
22.8 (c) copyright due to lincense terms.
22.9 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
22.10 - 10 20 30 40 50 60 70 80
22.11 *)
22.12 +theory TODO
22.13 +imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
22.14 +begin
22.15
22.16 -section \<open>\<close>
22.17 -subsection \<open>\<close>
22.18 -text \<open>
22.19 ---------------------------------------------------------------------------------
22.20 -WN131021: adopt Isabelle's numerals for Isac
22.21 ---------------------------------------------------------------------------------
22.22 +section \<open>TODOs from current development\<close>
22.23 +
22.24 +subsection \<open>Shift programs for Lucas-Interpretation from strings to partial_function\<close>
22.25 +text\<open>
22.26 +String constants have already bee introduced to old string-programs.
22.27 +Shifting this program code into partial_function reveals further issues:
22.28 +\begin{itemize}
22.29 +\item "partial_function xxx .." introduces a constant "xxx" (see xxx.simps), might break tests
22.30 +\item AlgEin.thy: oben = su_m] t_t; \<comment> \<open>PROG consts\<close>
22.31 +\item Biegelinie.thy
22.32 + \begin{itemize}
22.33 + \item ?drop biegelinie_lang?
22.34 + \item repair subpbl [''LINEAR'', ''system'']
22.35 + \end{itemize}
22.36 +\item Diff.thy
22.37 + \begin{itemize}
22.38 + \item differentiateX --> differentiate after removal of script-constant
22.39 + \end{itemize}
22.40 +\item Inverse_Z_Transform.thy:
22.41 + \begin{itemize}
22.42 + \item inverse_ztransform2, inverse_ztransform3 --- what can be dropped?
22.43 + Type unification failed: Clash of types "bool" and "_ itself"
22.44 + Type error in application: incompatible operand type
22.45 + Operator: Let (Take X_eq) :: (??'a itself \<Rightarrow> ??'b) \<Rightarrow> ??'b
22.46 + Operand:
22.47 + \<lambda>X. let X' = Rewrite ''ruleZY'' ...
22.48 + \item ''z''] \<comment> \<open>PROG string\<close>
22.49 + \end{itemize}
22.50 +\item Partial_Fractions.thy: reconsider Substitute [A = a, B = b]) pbz \<comment> \<open>PROG string A, B\<close>
22.51 +\item Test.thy: met_test_sqrt2: deleted?!
22.52 +\item
22.53 + \begin{itemize}
22.54 + \item
22.55 + \end{itemize}
22.56 +\end{itemize}
22.57 +\<close>
22.58 +subsubsection \<open>\<close>
22.59 +
22.60 +section \<open>TODOs shifted here from above\<close>
22.61 +
22.62 +subsection \<open>adopt Isabelle's numerals for Isac\<close>
22.63 +text \<open>WN131021:
22.64 intermediate states:
22.65 # replace numerals of type "real" by "nat" in some specific functions from ListC.thy
22.66 and have both representations in parallel for "nat".
22.67 -\<close>
22.68 -text \<open>
22.69 ---------------------------------------------------------------------------------
22.70 -WN140808: finetunig required for xmldata
22.71 ---------------------------------------------------------------------------------
22.72 +\<close>subsection \<open>finetunig required for xmldata\<close>
22.73 +text \<open>WN140808:
22.74 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
22.75 and in kbase html-representation generated from these xmldata.
22.76 Notes in ~~/xmldata/TODO.txt.
22.77 \<close>
22.78 -text \<open>
22.79 ---------------------------------------------------------------------------------
22.80 ---------------------------------------------------------------------------------
22.81 -\<close>
22.82 +
22.83 section \<open>\<close>
22.84 subsection \<open>\<close>
22.85 +subsubsection \<open>\<close>
22.86 +text \<open>\<close>
22.87 end