1.1 --- a/src/Tools/isac/Frontend/states.sml Thu Dec 20 18:02:25 2018 +0100
1.2 +++ b/src/Tools/isac/Frontend/states.sml Wed Dec 26 14:24:05 2018 +0100
1.3 @@ -26,13 +26,13 @@
1.4 if c = k then is_ch cs ks else false
1.5 in is_ch (rev child) (rev key) end;
1.6 (*
1.7 -is_child_of ["root'","univar","equation"] ["univar","equation"];
1.8 +is_child_of ["rootX","univar","equation"] ["univar","equation"];
1.9 val it = true : bool
1.10 -is_child_of ["root'","univar","equation"] ["system","equation"];
1.11 +is_child_of ["rootX","univar","equation"] ["system","equation"];
1.12 val it = false : bool
1.13 is_child_of ["equation"] ["system","equation"];
1.14 val it = false : bool
1.15 -is_child_of ["root'","univar","equation"] ["linear","univar","equation"];
1.16 +is_child_of ["rootX","univar","equation"] ["linear","univar","equation"];
1.17 val it = false : bool
1.18 *)
1.19
1.20 @@ -75,7 +75,7 @@
1.21 val it = Show
1.22 is_hid ["any","problem"] "Refine_Tacitly" hide;
1.23 val it = Htac
1.24 -is_hid ["root'","univar","equation"] "Apply_Method" hide;
1.25 +is_hid ["rootX","univar","equation"] "Apply_Method" hide;
1.26 val it = Show
1.27 is_hid ["univar","equation"] "Apply_Method" hide;
1.28 val it = Htac
1.29 @@ -103,7 +103,7 @@
1.30 val it = Show
1.31 is_hide ["any","problem"] (Refine_Tacitly []) hide;
1.32 val it = Htac
1.33 -is_hide ["root'","univar","equation"] (Apply_Method []) hide;
1.34 +is_hide ["rootX","univar","equation"] (Apply_Method []) hide;
1.35 val it = Show
1.36 is_hide ["univar","equation"] (Apply_Method []) hide;
1.37 val it = Htac
2.1 --- a/src/Tools/isac/Interpret/specification-elems.sml Thu Dec 20 18:02:25 2018 +0100
2.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml Wed Dec 26 14:24:05 2018 +0100
2.3 @@ -121,11 +121,12 @@
2.4
2.5 type subst' = term (* decomposes to "(char list * term) list", where term is Free ("xxx", _)
2.6 e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *)
2.7 -fun subst'_to_sube sub = sub
2.8 +fun subst'_to_sube sub = (sub
2.9 |> HOLogic.dest_list
2.10 |> map HOLogic.dest_prod
2.11 |> map (fn (e1, e2) => (HOLogic.dest_string e1, Rule.term2str e2))
2.12 - |> map (fn (e1, e2) => "(" ^ e1 ^ ", " ^ e2 ^ ")"): Rule.cterm' list
2.13 + |> map (fn (e1, e2) => "(" ^ e1 ^ ", " ^ e2 ^ ")"): Rule.cterm' list)
2.14 + handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])
2.15
2.16 val subte2sube = map Rule.term2str;
2.17 val subst2subs = map (pair2str o (apfst Rule.term2str) o (apsnd Rule.term2str));
3.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Thu Dec 20 18:02:25 2018 +0100
3.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Wed Dec 26 14:24:05 2018 +0100
3.3 @@ -64,18 +64,18 @@
3.4 " t_t = Substitute [oben = su_m] t_t; " ^
3.5 " t_t = Substitute o_o t_t; " ^
3.6 " t_t = Substitute [k_k, q__q] t_t; " ^
3.7 - " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.8 + " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
3.9 " su_m = boollist2sum s_s; " ^
3.10 " t_t = Substitute [senkrecht = su_m] t_t; " ^
3.11 " t_t = Substitute s_s t_t; " ^
3.12 " t_t = Substitute [k_k, q__q] t_t; " ^
3.13 - " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.14 + " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
3.15 " su_m = boollist2sum u_u; " ^
3.16 " t_t = Substitute [unten = su_m] t_t; " ^
3.17 " t_t = Substitute u_u t_t; " ^
3.18 " t_t = Substitute [k_k, q__q] t_t; " ^
3.19 - " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t " ^
3.20 - " in (Try (Rewrite_Set norm_Poly False)) t_t) ")]
3.21 + " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t " ^
3.22 + " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) ")]
3.23 \<close>
3.24 setup \<open>KEStore_Elems.add_mets
3.25 [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
3.26 @@ -93,17 +93,17 @@
3.27 " su_m = boollist2sum o_o; " ^
3.28 " t_t = Substitute [oben = su_m] t_t; " ^
3.29 " t_t = Substitute o_o t_t; " ^
3.30 - " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.31 + " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
3.32 " su_m = boollist2sum s_s; " ^
3.33 " t_t = Substitute [senkrecht = su_m] t_t; " ^
3.34 " t_t = Substitute s_s t_t; " ^
3.35 - " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.36 + " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
3.37 " su_m = boollist2sum u_u; " ^
3.38 " t_t = Substitute [unten = su_m] t_t; " ^
3.39 " t_t = Substitute u_u t_t; " ^
3.40 - " t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t; " ^
3.41 + " t_t = (Repeat (Try (Rewrite_Set ''norm_Poly'' False))) t_t; " ^
3.42 " t_t = Substitute [k_k, q__q] t_t " ^
3.43 - " in (Try (Rewrite_Set norm_Poly False)) t_t) ")]
3.44 + " in (Try (Rewrite_Set ''norm_Poly'' False)) t_t) ")]
3.45 \<close>
3.46
3.47 end
4.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu Dec 20 18:02:25 2018 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Dec 26 14:24:05 2018 +0100
4.3 @@ -205,16 +205,16 @@
4.4 "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) " ^
4.5 "(r_b::bool list) (r_m::bool list) = " ^
4.6 " (let q___q = Take (qq v_v = q__q); " ^
4.7 - " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
4.8 - " (Rewrite Belastung_Querkraft True)) q___q; " ^
4.9 + " q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@ " ^
4.10 + " (Rewrite ''Belastung_Querkraft'' True)) q___q; " ^
4.11 " (Q__Q:: bool) = " ^
4.12 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.13 - " [diff,integration,named]) " ^
4.14 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.15 + " [''diff'',''integration'',''named'']) " ^
4.16 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.17 - " Q__Q = Rewrite Querkraft_Moment True Q__Q; " ^
4.18 + " Q__Q = Rewrite ''Querkraft_Moment'' True Q__Q; " ^
4.19 " (M__M::bool) = " ^
4.20 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.21 - " [diff,integration,named]) " ^
4.22 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.23 + " [''diff'',''integration'',''named'']) " ^
4.24 " [REAL (rhs Q__Q), REAL v_v, REAL_REAL M_b]); " ^
4.25 (*([5], Res), M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2*)
4.26 " e__1 = NTH 1 r_m; " ^
4.27 @@ -232,22 +232,22 @@
4.28 (*([8], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.29 " M__2 = (Substitute [e__2]) M__2; " ^
4.30 " (c_1_2::bool list) = " ^
4.31 - " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
4.32 + " (SubProblem (''Biegelinie'',[''LINEAR'',''system''],[''no_met'']) " ^
4.33 " [BOOL_LIST [M__1, M__2], REAL_LIST [c,c_2]]); " ^
4.34 " M__M = Take M__M; " ^
4.35 " M__M = ((Substitute c_1_2) @@ " ^
4.36 - " (Try (Rewrite_Set_Inst [(bdv_1, c),(bdv_2, c_2)] " ^
4.37 - " simplify_System False)) @@ " ^
4.38 - " (Rewrite Moment_Neigung False) @@ " ^
4.39 - " (Rewrite make_fun_explicit False)) M__M; " ^
4.40 + " (Try (Rewrite_Set_Inst [(''bdv_1'', c),(bdv_2, c_2)] " ^
4.41 + " ''simplify_System'' False)) @@ " ^
4.42 + " (Rewrite ''Moment_Neigung'' False) @@ " ^
4.43 + " (Rewrite ''make_fun_explicit'' False)) M__M; " ^
4.44 (*----------------------- and the same once more ------------------------*)
4.45 " (N__N:: bool) = " ^
4.46 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.47 - " [diff,integration,named]) " ^
4.48 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.49 + " [''diff'',''integration'',''named'']) " ^
4.50 " [REAL (rhs M__M), REAL v_v, REAL_REAL y']); " ^
4.51 " (B__B:: bool) = " ^
4.52 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.53 - " [diff,integration,named]) " ^
4.54 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.55 + " [''diff'',''integration'',''named'']) " ^
4.56 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]); " ^
4.57 " e__1 = NTH 1 r_b; " ^
4.58 " (x__1::real) = argument_in (lhs e__1); " ^
4.59 @@ -259,11 +259,11 @@
4.60 " (B__2::bool) = (Substitute [v_v = x__2]) B__B; " ^
4.61 " B__2 = (Substitute [e__2]) B__2 ; " ^
4.62 " (c_1_2::bool list) = " ^
4.63 - " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
4.64 + " (SubProblem (''Biegelinie'',[''LINEAR'',''system''],[''no_met'']) " ^
4.65 " [BOOL_LIST [B__1, B__2], REAL_LIST [c,c_2]]); " ^
4.66 " B__B = Take B__B; " ^
4.67 " B__B = ((Substitute c_1_2) @@ " ^
4.68 - " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
4.69 + " (Rewrite_Set_Inst [(''bdv'', x)] ''make_ratpoly_in'' False)) B__B " ^
4.70 " in B__B)")]
4.71 \<close>
4.72 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
4.73 @@ -319,18 +319,18 @@
4.74 "Script Biegelinie2Script " ^
4.75 "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) = " ^
4.76 " (let " ^
4.77 - " (funs :: bool list) = (SubProblem (Biegelinie', " ^
4.78 - " [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung]) " ^
4.79 + " (funs :: bool list) = (SubProblem (''Biegelinie'', " ^
4.80 + " [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung'']) " ^
4.81 " [REAL q, REAL v]); " ^
4.82 - " (equs :: bool list) = (SubProblem (Biegelinie', " ^
4.83 - " [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin]) " ^
4.84 + " (equs :: bool list) = (SubProblem (''Biegelinie'', " ^
4.85 + " [''setzeRandbedingungen'', ''Biegelinien''], [''Biegelinien'', ''setzeRandbedingungenEin'']) " ^
4.86 " [BOOL_LIST funs, BOOL_LIST s]); " ^
4.87 - " (cons :: bool list) = (SubProblem (Biegelinie', " ^
4.88 - " [LINEAR, system], [no_met]) " ^
4.89 + " (cons :: bool list) = (SubProblem (''Biegelinie'', " ^
4.90 + " [''LINEAR'', ''system''], [''no_met'']) " ^
4.91 " [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]); " ^
4.92 " B = Take (lastI funs); " ^
4.93 " B = ((Substitute cons) @@ " ^
4.94 - " (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B " ^
4.95 + " (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B " ^
4.96 " in B) ")]
4.97 \<close>
4.98 setup \<open>KEStore_Elems.add_mets
4.99 @@ -373,26 +373,26 @@
4.100 prls = Rule.e_rls, crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
4.101 "Script Belastung2BiegelScript (q__q::real) (v_v::real) = " ^
4.102 " (let q___q = Take (qq v_v = q__q); " ^
4.103 - " q___q = ((Rewrite sym_neg_equal_iff_equal True) @@ " ^
4.104 - " (Rewrite Belastung_Querkraft True)) q___q; " ^
4.105 + " q___q = ((Rewrite ''sym_neg_equal_iff_equal'' True) @@ " ^
4.106 + " (Rewrite ''Belastung_Querkraft'' True)) q___q; " ^
4.107 " (Q__Q:: bool) = " ^
4.108 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.109 - " [diff,integration,named]) " ^
4.110 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.111 + " [''diff'',''integration'',''named'']) " ^
4.112 " [REAL (rhs q___q), REAL v_v, REAL_REAL Q]); " ^
4.113 - " M__M = Rewrite Querkraft_Moment True Q__Q; " ^
4.114 + " M__M = Rewrite ''Querkraft_Moment'' True Q__Q; " ^
4.115 " (M__M::bool) = " ^
4.116 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.117 - " [diff,integration,named]) " ^
4.118 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.119 + " [''diff'',''integration'',''named'']) " ^
4.120 " [REAL (rhs M__M), REAL v_v, REAL_REAL M_b]); " ^
4.121 - " N__N = ((Rewrite Moment_Neigung False) @@ " ^
4.122 + " N__N = ((Rewrite ''Moment_Neigung'' False) @@ " ^
4.123 " (Rewrite make_fun_explicit False)) M__M; " ^
4.124 " (N__N:: bool) = " ^
4.125 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.126 - " [diff,integration,named]) " ^
4.127 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.128 + " [''diff'',''integration'',named'']) " ^
4.129 " [REAL (rhs N__N), REAL v_v, REAL_REAL y']); " ^
4.130 " (B__B:: bool) = " ^
4.131 - " (SubProblem (Biegelinie',[named,integrate,function], " ^
4.132 - " [diff,integration,named]) " ^
4.133 + " (SubProblem (''Biegelinie'',[''named'',''integrate'',''function''], " ^
4.134 + " [''diff'',''integration'',''named'']) " ^
4.135 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
4.136 " in [Q__Q, M__M, N__N, B__B])")]
4.137 \<close>
4.138 @@ -409,26 +409,26 @@
4.139 " (let b_1 = NTH 1 r_b; " ^
4.140 " f_s = filter_sameFunId (lhs b_1) fun_s; " ^
4.141 " (e_1::bool) = " ^
4.142 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.143 - " [Equation,fromFunction]) " ^
4.144 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.145 + " [''Equation'',''fromFunction'']) " ^
4.146 " [BOOL (hd f_s), BOOL b_1]); " ^
4.147 " b_2 = NTH 2 r_b; " ^
4.148 " f_s = filter_sameFunId (lhs b_2) fun_s; " ^
4.149 " (e_2::bool) = " ^
4.150 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.151 - " [Equation,fromFunction]) " ^
4.152 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.153 + " [''Equation'',''fromFunction'']) " ^
4.154 " [BOOL (hd f_s), BOOL b_2]); " ^
4.155 " b_3 = NTH 3 r_b; " ^
4.156 " f_s = filter_sameFunId (lhs b_3) fun_s; " ^
4.157 " (e_3::bool) = " ^
4.158 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.159 - " [Equation,fromFunction]) " ^
4.160 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.161 + " [''Equation'',''fromFunction'']) " ^
4.162 " [BOOL (hd f_s), BOOL b_3]); " ^
4.163 " b_4 = NTH 4 r_b; " ^
4.164 " f_s = filter_sameFunId (lhs b_4) fun_s; " ^
4.165 " (e_4::bool) = " ^
4.166 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.167 - " [Equation,fromFunction]) " ^
4.168 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.169 + " [''Equation'',''fromFunction'']) " ^
4.170 " [BOOL (hd f_s), BOOL b_4]) " ^
4.171 " in [e_1, e_2, e_3, e_4])"
4.172 (* filter requires more than 1 sec !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4.173 @@ -436,26 +436,26 @@
4.174 " (let b_1 = NTH 1 r_b; " ^
4.175 " f_s = filter (sameFunId (lhs b_1)) fun_s; " ^
4.176 " (e_1::bool) = " ^
4.177 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.178 - " [Equation,fromFunction]) " ^
4.179 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.180 + " [''Equation'',''fromFunction'']) " ^
4.181 " [BOOL (hd f_s), BOOL b_1]); " ^
4.182 " b_2 = NTH 2 r_b; " ^
4.183 " f_s = filter (sameFunId (lhs b_2)) fun_s; " ^
4.184 " (e_2::bool) = " ^
4.185 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.186 - " [Equation,fromFunction]) " ^
4.187 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.188 + " [''Equation'',''fromFunction'']) " ^
4.189 " [BOOL (hd f_s), BOOL b_2]); " ^
4.190 " b_3 = NTH 3 r_b; " ^
4.191 " f_s = filter (sameFunId (lhs b_3)) fun_s; " ^
4.192 " (e_3::bool) = " ^
4.193 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.194 - " [Equation,fromFunction]) " ^
4.195 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.196 + " [''Equation'',''fromFunction'']) " ^
4.197 " [BOOL (hd f_s), BOOL b_3]); " ^
4.198 " b_4 = NTH 4 r_b; " ^
4.199 " f_s = filter (sameFunId (lhs b_4)) fun_s; " ^
4.200 " (e_4::bool) = " ^
4.201 - " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
4.202 - " [Equation,fromFunction]) " ^
4.203 + " (SubProblem (''Biegelinie'',[''makeFunctionTo'',''equation'']," ^
4.204 + " [''Equation'',''fromFunction'']) " ^
4.205 " [BOOL (hd f_s), BOOL b_4]) " ^
4.206 " in [e_1,e_2,e_3,e_4])"*))]
4.207 \<close>
4.208 @@ -480,7 +480,7 @@
4.209 " eq_u = (Substitute [bd_v = va_l]) fu_n; " ^
4.210 (*([1], Res), M_b L = c_2 + c * L + -1 * q_0 / 2 * L ^^^ 2*)
4.211 " eq_u = (Substitute [su_b]) eq_u " ^
4.212 - " in (Rewrite_Set norm_Rational False) eq_u) ")]
4.213 + " in (Rewrite_Set ''norm_Rational'' False) eq_u) ")]
4.214 \<close>
4.215
4.216 end
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Dec 20 18:02:25 2018 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed Dec 26 14:24:05 2018 +0100
5.3 @@ -298,24 +298,24 @@
5.4 " (let f_f' = Take (d_d v_v f_f) " ^
5.5 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.6 " (Repeat " ^
5.7 - " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.8 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.9 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.10 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.11 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.12 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.13 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.14 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.15 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.16 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.17 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.18 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.19 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.20 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.21 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.22 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.23 - " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
5.24 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')")]
5.25 + " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
5.26 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
5.27 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^
5.28 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or " ^
5.29 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^
5.30 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^
5.31 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^
5.32 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^
5.33 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^
5.34 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^
5.35 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^
5.36 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^
5.37 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^
5.38 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^
5.39 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
5.40 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
5.41 + " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
5.42 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')")]
5.43 \<close>
5.44 setup \<open>KEStore_Elems.add_mets
5.45 [Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
5.46 @@ -328,23 +328,23 @@
5.47 " (let f_f' = Take (d_d v_v f_f) " ^
5.48 " in (( " ^
5.49 " (Repeat " ^
5.50 - " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.51 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.52 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.53 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot False)) Or " ^
5.54 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.55 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.56 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.57 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.58 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.59 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.60 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.61 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.62 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.63 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.64 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.65 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.66 - " (Repeat (Rewrite_Set make_polynomial False)))) " ^
5.67 + " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
5.68 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
5.69 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^
5.70 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' False)) Or " ^
5.71 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^
5.72 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^
5.73 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^
5.74 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^
5.75 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^
5.76 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^
5.77 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^
5.78 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^
5.79 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^
5.80 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^
5.81 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
5.82 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
5.83 + " (Repeat (Rewrite_Set ''make_polynomial'' False)))) " ^
5.84 " )) f_f')")]
5.85 \<close>
5.86 setup \<open>KEStore_Elems.add_mets
5.87 @@ -358,25 +358,25 @@
5.88 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
5.89 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.90 " (Repeat " ^
5.91 - " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
5.92 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^
5.93 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
5.94 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
5.95 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
5.96 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
5.97 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
5.98 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
5.99 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
5.100 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
5.101 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
5.102 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
5.103 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
5.104 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
5.105 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
5.106 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
5.107 - " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
5.108 - " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
5.109 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')")]
5.110 + " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
5.111 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_dif'' False)) Or " ^
5.112 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
5.113 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^
5.114 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or " ^
5.115 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^
5.116 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^
5.117 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^
5.118 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^
5.119 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^
5.120 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^
5.121 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^
5.122 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^
5.123 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^
5.124 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^
5.125 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
5.126 + " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
5.127 + " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
5.128 + " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f') ")]
5.129 \<close>
5.130 setup \<open>KEStore_Elems.add_mets
5.131 [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
5.132 @@ -387,11 +387,11 @@
5.133 crls=Atools_erls, errpats = [], nrls = norm_Rational},
5.134 "Script DiffScr (f_f::real) (v_v::real) = " ^
5.135 " (let f_f' = Take (d_d v_v f_f) " ^
5.136 - " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
5.137 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
5.138 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
5.139 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
5.140 - " (Try (Rewrite_Set norm_Rational False))) f_f')")]
5.141 + " in ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
5.142 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
5.143 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@ " ^
5.144 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@ " ^
5.145 + " (Try (Rewrite_Set ''norm_Rational'' False))) f_f')")]
5.146 \<close>
5.147 setup \<open>KEStore_Elems.add_cas
5.148 [((Thm.term_of o the o (TermC.parse thy)) "Diff",
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Dec 20 18:02:25 2018 +0100
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Wed Dec 26 14:24:05 2018 +0100
6.3 @@ -543,20 +543,20 @@
6.4 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
6.5 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
6.6 " (let e_1 = Take (hd e_s); " ^
6.7 - " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.8 - " isolate_bdvs False)) @@ " ^
6.9 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.10 - " simplify_System False))) e_1; " ^
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 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.24 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.25 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.26 + " ''isolate_bdvs'' False)) @@ " ^
6.27 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.28 + " ''simplify_System'' False))) e_2; " ^
6.29 " e__s = Take [e_1, e_2] " ^
6.30 - " in (Try (Rewrite_Set order_system False)) e__s)"
6.31 + " in (Try (Rewrite_Set ''order_system'' False)) e__s)"
6.32 (*---------------------------------------------------------------------------
6.33 this script does NOT separate the equations as above,
6.34 but it does not yet work due to preliminary script-interpreter,
6.35 @@ -567,12 +567,12 @@
6.36 " e_1 = hd e__s; " ^
6.37 " e_2 = hd (tl e__s); " ^
6.38 " e__s = [e_1, Substitute [e_1] e_2] " ^
6.39 - " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.40 - " simplify_System_parenthesized False)) @@ " ^
6.41 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^
6.42 - " isolate_bdvs False)) @@ " ^
6.43 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.44 - " simplify_System False))) e__s)"
6.45 + " in ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.46 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.47 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] " ^
6.48 + " ''isolate_bdvs'' False)) @@ " ^
6.49 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.50 + " ''simplify_System'' False))) e__s)"
6.51 ---------------------------------------------------------------------------*))]
6.52 \<close>
6.53 setup \<open>KEStore_Elems.add_mets
6.54 @@ -594,15 +594,15 @@
6.55 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})],
6.56 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
6.57 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
6.58 - " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^
6.59 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.60 - " simplify_System_parenthesized False)) @@ " ^
6.61 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.62 - " isolate_bdvs False)) @@ " ^
6.63 - " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
6.64 - " simplify_System_parenthesized False)) @@ " ^
6.65 - " (Try (Rewrite_Set order_system False))) e_s " ^
6.66 - " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
6.67 + " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
6.68 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.69 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.70 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.71 + " ''isolate_bdvs'' False)) @@ " ^
6.72 + " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
6.73 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.74 + " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
6.75 + " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
6.76 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
6.77 \<close>
6.78 setup \<open>KEStore_Elems.add_mets
6.79 @@ -619,19 +619,19 @@
6.80 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
6.81 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^
6.82 " (let e__s = " ^
6.83 - " ((Try (Rewrite_Set norm_Rational False)) @@ " ^
6.84 - " (Repeat (Rewrite commute_0_equality False)) @@ " ^
6.85 - " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
6.86 - " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
6.87 - " simplify_System_parenthesized False)) @@ " ^
6.88 - " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
6.89 - " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
6.90 - " isolate_bdvs_4x4 False)) @@ " ^
6.91 - " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^
6.92 - " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^
6.93 - " simplify_System_parenthesized False)) @@ " ^
6.94 - " (Try (Rewrite_Set order_system False))) e_s " ^
6.95 - " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^
6.96 + " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^
6.97 + " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^
6.98 + " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
6.99 + " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
6.100 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.101 + " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
6.102 + " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
6.103 + " ''isolate_bdvs_4x4'' False)) @@ " ^
6.104 + " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^
6.105 + " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^
6.106 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.107 + " (Try (Rewrite_Set ''order_system'' False))) e_s " ^
6.108 + " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^
6.109 " [BOOL_LIST e__s, REAL_LIST v_s]))")]
6.110 \<close>
6.111 setup \<open>KEStore_Elems.add_mets
6.112 @@ -654,15 +654,15 @@
6.113 " (let e_1 = NTH 1 e_s; " ^
6.114 " e_2 = Take (NTH 2 e_s); " ^
6.115 " e_2 = ((Substitute [e_1]) @@ " ^
6.116 - " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
6.117 - " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
6.118 - " simplify_System_parenthesized False)) @@ " ^
6.119 - " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
6.120 - " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
6.121 - " isolate_bdvs False)) @@ " ^
6.122 - " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^
6.123 - " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^
6.124 - " norm_Rational False))) e_2 " ^
6.125 + " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
6.126 + " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
6.127 + " ''simplify_System_parenthesized'' False)) @@ " ^
6.128 + " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
6.129 + " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
6.130 + " ''isolate_bdvs'' False)) @@ " ^
6.131 + " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
6.132 + " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
6.133 + " ''norm_Rational'' False))) e_2 " ^
6.134 " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
6.135 \<close>
6.136
7.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Thu Dec 20 18:02:25 2018 +0100
7.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Wed Dec 26 14:24:05 2018 +0100
7.3 @@ -112,7 +112,7 @@
7.4 "Script Sortprog (unso :: int xlist) = " ^
7.5 " (let uns = Take (sort unso) " ^
7.6 " in " ^
7.7 - " (Rewrite_Set ins_sort False) uns" ^
7.8 + " (Rewrite_Set ''ins_sort ''False) uns" ^
7.9 " )")]
7.10 \<close>
7.11 setup \<open>KEStore_Elems.add_mets
8.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Dec 20 18:02:25 2018 +0100
8.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Dec 26 14:24:05 2018 +0100
8.3 @@ -91,17 +91,17 @@
8.4 errpats = [], nrls = Rule.e_rls},
8.5 "Script InverseZTransform (X_eq::bool) =" ^ (*(1/z) instead of z ^^^ -1*)
8.6 " (let X = Take X_eq;" ^
8.7 - " X' = Rewrite ruleZY False X;" ^ (*z * denominator*)
8.8 - " X' = (Rewrite_Set norm_Rational False) X';" ^ (*simplify*)
8.9 + " X' = Rewrite ''ruleZY'' False X;" ^ (*z * denominator*)
8.10 + " X' = (Rewrite_Set ''norm_Rational'' False) X';" ^ (*simplify*)
8.11 " funterm = Take (rhs X');" ^ (*drop X' z = for equation solving*)
8.12 - " denom = (Rewrite_Set partial_fraction False) funterm;" ^ (*get_denominator*)
8.13 + " denom = (Rewrite_Set ''partial_fraction'' False) funterm;" ^ (*get_denominator*)
8.14 " equ = (denom = (0::real));" ^
8.15 " fun_arg = Take (lhs X');" ^
8.16 - " arg = (Rewrite_Set partial_fraction False) X';" ^ (*get_argument TODO*)
8.17 + " arg = (Rewrite_Set ''partial_fraction'' False) X';" ^ (*get_argument TODO*)
8.18 " (L_L::bool list) = " ^
8.19 - " (SubProblem (Test', " ^
8.20 - " [LINEAR,univariate,equation,test]," ^
8.21 - " [Test,solve_linear]) " ^
8.22 + " (SubProblem (''Test'', " ^
8.23 + " [''LINEAR'',''univariate'',''equation'',''test'']," ^
8.24 + " [''Test'',''solve_linear'']) " ^
8.25 " [BOOL equ, REAL z]) " ^
8.26 " in X)")]
8.27 \<close>
8.28 @@ -115,10 +115,10 @@
8.29 "Script InverseZTransform (X_eq::bool) = "^
8.30 (*(1/z) instead of z ^^^ -1*)
8.31 "(let X = Take X_eq; "^
8.32 - " X' = Rewrite ruleZY False X; "^
8.33 + " X' = Rewrite ''ruleZY'' False X; "^
8.34 (*z * denominator*)
8.35 " (num_orig::real) = get_numerator (rhs X'); "^
8.36 - " X' = (Rewrite_Set norm_Rational False) X'; "^
8.37 + " X' = (Rewrite_Set ''norm_Rational'' False) X'; "^
8.38 (*simplify*)
8.39 " (X'_z::real) = lhs X'; "^
8.40 " (zzz::real) = argument_in X'_z; "^
8.41 @@ -129,9 +129,9 @@
8.42 " (num::real) = get_numerator funterm; "^
8.43 (*get_numerator*)
8.44 " (equ::bool) = (denom = (0::real)); "^
8.45 - " (L_L::bool list) = (SubProblem (PolyEq', "^
8.46 - " [abcFormula,degree_2,polynomial,univariate,equation], "^
8.47 - " [no_met]) "^
8.48 + " (L_L::bool list) = (SubProblem (''PolyEq'', "^
8.49 + " [''abcFormula'',''degree_2'',''polynomial'',''univariate'',''equation''], "^
8.50 + " [''no_met'']) "^
8.51 " [BOOL equ, REAL zzz]); "^
8.52 " (facs::real) = factors_from_solution L_L; "^
8.53 " (eql::real) = Take (num_orig / facs); "^
8.54 @@ -140,7 +140,7 @@
8.55
8.56 " (eq::bool) = Take (eql = eqr); "^
8.57 (*Maybe possible to use HOLogic.mk_eq ??*)
8.58 - " eq = (Try (Rewrite_Set equival_trans False)) eq; "^
8.59 + " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq; "^
8.60
8.61 " eq = drop_questionmarks eq; "^
8.62 " (z1::real) = (rhs (NTH 1 L_L)); "^
8.63 @@ -154,17 +154,17 @@
8.64 " eq_a = (Substitute [zzz=z1]) eq; "^
8.65 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
8.66 " (sol_a::bool list) = "^
8.67 - " (SubProblem (Isac', "^
8.68 - " [univariate,equation],[no_met]) "^
8.69 + " (SubProblem (''Isac'', "^
8.70 + " [''univariate'',''equation''],[''no_met'']) "^
8.71 " [BOOL eq_a, REAL (A::real)]); "^
8.72 " (a::real) = (rhs(NTH 1 sol_a)); "^
8.73
8.74 " (eq_b::bool) = Take eq; "^
8.75 " eq_b = (Substitute [zzz=z2]) eq_b; "^
8.76 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
8.77 + " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; "^
8.78 " (sol_b::bool list) = "^
8.79 - " (SubProblem (Isac', "^
8.80 - " [univariate,equation],[no_met]) "^
8.81 + " (SubProblem (''Isac'', "^
8.82 + " [''univariate'',''equation''],[''no_met'']) "^
8.83 " [BOOL eq_b, REAL (B::real)]); "^
8.84 " (b::real) = (rhs(NTH 1 sol_b)); "^
8.85
8.86 @@ -172,11 +172,11 @@
8.87 " (pbz::real) = Take eqr; "^
8.88 " pbz = ((Substitute [A=a, B=b]) pbz); "^
8.89
8.90 - " pbz = Rewrite ruleYZ False pbz; "^
8.91 + " pbz = Rewrite ''ruleYZ'' False pbz; "^
8.92 " pbz = drop_questionmarks pbz; "^
8.93
8.94 " (X_z::bool) = Take (X_z = pbz); "^
8.95 - " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
8.96 + " (n_eq::bool) = (Rewrite_Set ''inverse_z'' False) X_z; "^
8.97 " n_eq = drop_questionmarks n_eq "^
8.98 "in n_eq)")]
8.99 \<close>
8.100 @@ -212,7 +212,7 @@
8.101 (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
8.102 "(let X = Take X_eq; "^
8.103 (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
8.104 - " X' = Rewrite ruleZY False X; "^
8.105 + " X' = Rewrite ''ruleZY'' False X; "^
8.106 (* ?X' z*)
8.107 " (X'_z::real) = lhs X'; "^
8.108 (* z *)
8.109 @@ -220,22 +220,22 @@
8.110 (* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
8.111 " (funterm::real) = rhs X'; "^
8.112
8.113 - " (pbz::real) = (SubProblem (Isac', "^
8.114 - " [partial_fraction,rational,simplification], "^
8.115 - " [simplification,of_rationals,to_partial_fraction]) "^
8.116 + " (pbz::real) = (SubProblem (''Isac'', "^
8.117 + " [''partial_fraction'',''rational'',''simplification''], "^
8.118 + " [''simplification'',''of_rationals'',''to_partial_fraction'']) "^
8.119 (*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
8.120 " [REAL funterm, REAL zzz]); "^
8.121
8.122 (*([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
8.123 " (pbz_eq::bool) = Take (X'_z = pbz); "^
8.124 (*([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))*)
8.125 - " pbz_eq = Rewrite ruleYZ False pbz_eq; "^
8.126 + " pbz_eq = Rewrite ''ruleYZ'' False pbz_eq; "^
8.127 (* 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
8.128 " pbz_eq = drop_questionmarks pbz_eq; "^
8.129 (*([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))*)
8.130 " (X_zeq::bool) = Take (X_z = rhs pbz_eq); "^
8.131 (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
8.132 - " n_eq = (Rewrite_Set inverse_z False) X_zeq; "^
8.133 + " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq; "^
8.134 (* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
8.135 " n_eq = drop_questionmarks n_eq "^
8.136 (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Dec 20 18:02:25 2018 +0100
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Dec 26 14:24:05 2018 +0100
9.3 @@ -149,15 +149,15 @@
9.4 {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
9.5 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
9.6 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
9.7 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
9.8 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
9.9 - " (Try (Rewrite_Set expand_binoms False)) @@ " ^
9.10 - " (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
9.11 - " make_ratpoly_in False))) @@ " ^
9.12 - " (Try (Repeat (Rewrite_Set LinPoly_simplify False))))e_e;" ^
9.13 - " e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
9.14 - " LinEq_simplify True)) @@ " ^
9.15 - " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
9.16 + "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
9.17 + " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
9.18 + " (Try (Rewrite_Set ''expand_binoms'' False)) @@ " ^
9.19 + " (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
9.20 + " ''make_ratpoly_in'' False))) @@ " ^
9.21 + " (Try (Repeat (Rewrite_Set ''LinPoly_simplify'' False))))e_e;" ^
9.22 + " e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
9.23 + " ''LinEq_simplify'' True)) @@ " ^
9.24 + " (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e " ^
9.25 " in ((Or_to_List e_e)::bool list))")]
9.26 \<close>
9.27 ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
10.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Thu Dec 20 18:02:25 2018 +0100
10.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Dec 26 14:24:05 2018 +0100
10.3 @@ -48,9 +48,9 @@
10.4 {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule.e_rls, prls = PolyEq_prls, calc = [],
10.5 crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
10.6 "Script Solve_log (e_e::bool) (v_v::real) = " ^
10.7 - "(let e_e = ((Rewrite equality_power False) @@ " ^
10.8 - " (Rewrite exp_invers_log False) @@ " ^
10.9 - " (Rewrite_Set norm_Poly False)) e_e " ^
10.10 + "(let e_e = ((Rewrite ''equality_power'' False) @@ " ^
10.11 + " (Rewrite ''exp_invers_log'' False) @@ " ^
10.12 + " (Rewrite_Set ''norm_Poly'' False)) e_e " ^
10.13 " in [e_e])")]
10.14 \<close>
10.15
11.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Dec 20 18:02:25 2018 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Dec 26 14:24:05 2018 +0100
11.3 @@ -239,27 +239,27 @@
11.4 (* num_orig = 3*)
11.5 " (num_orig::real) = get_numerator f_f; " ^
11.6 (*([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
11.7 - " f_f = (Rewrite_Set norm_Rational False) f_f; " ^
11.8 + " f_f = (Rewrite_Set ''norm_Rational'' False) f_f; " ^
11.9 (* denom = -1 + -2 * z + 8 * z ^^^ 2*)
11.10 " (denom::real) = get_denominator f_f; " ^
11.11 (* equ = -1 + -2 * z + 8 * z ^^^ 2 = 0*)
11.12 " (equ::bool) = (denom = (0::real)); " ^
11.13
11.14 (*([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)*)
11.15 - " (L_L::bool list) = (SubProblem (PolyEq', " ^
11.16 - " [abcFormula, degree_2, polynomial, univariate, equation], " ^
11.17 + " (L_L::bool list) = (SubProblem (''PolyEq'', " ^
11.18 + " [''abcFormula'', ''degree_2'', ''polynomial'', ''univariate'', ''equation''], " ^
11.19 (*([2], Res), [z = 1 / 2, z = -1 / 4]*)
11.20 - " [no_met]) [BOOL equ, REAL zzz]); " ^
11.21 + " [''no_met'']) [BOOL equ, REAL zzz]); " ^
11.22 (* facs: (z - 1 / 2) * (z - -1 / 4)*)
11.23 " (facs::real) = factors_from_solution L_L; " ^
11.24 (*([3], Frm), 33 / ((z - 1 / 2) * (z - -1 / 4)) *)
11.25 " (eql::real) = Take (num_orig / facs); " ^
11.26 (*([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
11.27 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^
11.28 + " (eqr::real) = (Try (Rewrite_Set ''ansatz_rls'' False)) eql; " ^
11.29 (*([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
11.30 " (eq::bool) = Take (eql = eqr); " ^
11.31 (*([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
11.32 - " eq = (Try (Rewrite_Set equival_trans False)) eq;" ^
11.33 + " eq = (Try (Rewrite_Set ''equival_trans'' False)) eq;" ^
11.34 (* eq = 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
11.35 " eq = drop_questionmarks eq; " ^
11.36 (* z1 = 1 / 2*)
11.37 @@ -271,11 +271,11 @@
11.38 (*([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
11.39 " eq_a = (Substitute [zzz = z1]) eq; " ^
11.40 (*([6], Res), 3 = 3 * A / 4*)
11.41 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^
11.42 + " eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a; " ^
11.43
11.44 (*([7], Pbl), solve (3 = 3 * A / 4, A)*)
11.45 " (sol_a::bool list) = " ^
11.46 - " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
11.47 + " (SubProblem (''Isac'', [''univariate'',''equation''], [''no_met'']) " ^
11.48 (*([7], Res), [A = 4]*)
11.49 " [BOOL eq_a, REAL (A::real)]); " ^
11.50 (* a = 4*)
11.51 @@ -285,10 +285,10 @@
11.52 (*([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)*)
11.53 " eq_b = (Substitute [zzz = z2]) eq_b; " ^
11.54 (*([9], Res), 3 = -3 * B / 4*)
11.55 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^
11.56 + " eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; " ^
11.57 (*([10], Pbl), solve (3 = -3 * B / 4, B)*)
11.58 " (sol_b::bool list) = " ^
11.59 - " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
11.60 + " (SubProblem (''Isac'', [''univariate'',''equation''], [''no_met'']) " ^
11.61 (*([10], Res), [B = -4]*)
11.62 " [BOOL eq_b, REAL (B::real)]); " ^
11.63 (* b = -4*)
12.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Dec 20 18:02:25 2018 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Dec 26 14:24:05 2018 +0100
12.3 @@ -918,38 +918,38 @@
12.4 val scr_make_polynomial =
12.5 "Script Expand_binoms t_t = " ^
12.6 "(Repeat " ^
12.7 -"((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
12.8 +"((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@ " ^
12.9
12.10 -" (Try (Repeat (Rewrite distrib_right False))) @@ " ^
12.11 -" (Try (Repeat (Rewrite distrib_left False))) @@ " ^
12.12 -" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
12.13 -" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
12.14 +" (Try (Repeat (Rewrite ''distrib_right'' False))) @@ " ^
12.15 +" (Try (Repeat (Rewrite ''distrib_left'' False))) @@ " ^
12.16 +" (Try (Repeat (Rewrite ''left_diff_distrib'' False))) @@ " ^
12.17 +" (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@ " ^
12.18
12.19 -" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
12.20 -" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
12.21 -" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
12.22 +" (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
12.23 +" (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
12.24 +" (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
12.25
12.26 -" (Try (Repeat (Rewrite mult_commute False))) @@ " ^
12.27 -" (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
12.28 -" (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
12.29 -" (Try (Repeat (Rewrite add_commute False))) @@ " ^
12.30 -" (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
12.31 -" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
12.32 +" (Try (Repeat (Rewrite ''mult_commute'' False))) @@ " ^
12.33 +" (Try (Repeat (Rewrite ''real_mult_left_commute'' False))) @@ " ^
12.34 +" (Try (Repeat (Rewrite ''mult_assoc'' False))) @@ " ^
12.35 +" (Try (Repeat (Rewrite ''add_commute'' False))) @@ " ^
12.36 +" (Try (Repeat (Rewrite ''add_left_commute'' False))) @@ " ^
12.37 +" (Try (Repeat (Rewrite ''add_assoc'' False))) @@ " ^
12.38
12.39 -" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
12.40 -" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
12.41 -" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
12.42 -" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
12.43 +" (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
12.44 +" (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
12.45 +" (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
12.46 +" (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
12.47
12.48 -" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
12.49 -" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
12.50 +" (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
12.51 +" (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
12.52
12.53 -" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
12.54 -" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
12.55 +" (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
12.56 +" (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
12.57
12.58 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
12.59 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
12.60 -" (Try (Repeat (Calculate POWER)))) " ^
12.61 +" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
12.62 +" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
12.63 +" (Try (Repeat (Calculate ''POWER'')))) " ^
12.64 " t_t)";
12.65
12.66 (*version used by MG.02/03, overwritten by version AG in 04 below
12.67 @@ -973,35 +973,35 @@
12.68 val scr_expand_binoms =
12.69 "Script Expand_binoms t_t =" ^
12.70 "(Repeat " ^
12.71 -"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
12.72 -" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
12.73 -" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
12.74 -" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
12.75 -" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
12.76 -" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
12.77 +"((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@ " ^
12.78 +" (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@ " ^
12.79 +" (Try (Repeat (Rewrite ''real_minus_binom_pow2'' False))) @@ " ^
12.80 +" (Try (Repeat (Rewrite ''real_minus_binom_times'' False))) @@ " ^
12.81 +" (Try (Repeat (Rewrite ''real_plus_minus_binom1'' False))) @@ " ^
12.82 +" (Try (Repeat (Rewrite ''real_plus_minus_binom2'' False))) @@ " ^
12.83
12.84 -" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
12.85 -" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
12.86 -" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
12.87 +" (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
12.88 +" (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
12.89 +" (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
12.90
12.91 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
12.92 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
12.93 -" (Try (Repeat (Calculate POWER))) @@ " ^
12.94 +" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
12.95 +" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
12.96 +" (Try (Repeat (Calculate ''POWER''))) @@ " ^
12.97
12.98 -" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
12.99 -" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
12.100 -" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
12.101 -" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
12.102 +" (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
12.103 +" (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
12.104 +" (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
12.105 +" (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
12.106
12.107 -" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
12.108 -" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
12.109 +" (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
12.110 +" (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
12.111
12.112 -" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
12.113 -" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
12.114 +" (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
12.115 +" (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
12.116
12.117 -" (Try (Repeat (Calculate PLUS ))) @@ " ^
12.118 -" (Try (Repeat (Calculate TIMES ))) @@ " ^
12.119 -" (Try (Repeat (Calculate POWER)))) " ^
12.120 +" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
12.121 +" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
12.122 +" (Try (Repeat (Calculate ''POWER'')))) " ^
12.123 " t_t)";
12.124
12.125 val expand_binoms =
12.126 @@ -1614,7 +1614,7 @@
12.127 norm_Poly :: ID
12.128 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
12.129 where
12.130 - "simplify term = ((Rewrite_Set norm_Poly False) term)"
12.131 + "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
12.132
12.133 -----*)
12.134 setup \<open>KEStore_Elems.add_mets
12.135 @@ -1629,7 +1629,7 @@
12.136 Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
12.137 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
12.138 "Script SimplifyScript (t_t::real) = " ^
12.139 - " ((Rewrite_Set norm_Poly False) t_t)")]
12.140 + " ((Rewrite_Set ''norm_Poly'' False) t_t)")]
12.141 \<close>
12.142
12.143 ML \<open>
13.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Dec 20 18:02:25 2018 +0100
13.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Wed Dec 26 14:24:05 2018 +0100
13.3 @@ -955,13 +955,13 @@
13.4 ML\<open>
13.5 val scr =
13.6 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
13.7 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
13.8 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
13.9 - " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
13.10 - " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.11 - " make_ratpoly_in False))) @@ " ^
13.12 - " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
13.13 - " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
13.14 + "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
13.15 + " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
13.16 + " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
13.17 + " (Try (Repeat (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.18 + " ''make_ratpoly_in'' False))) @@ " ^
13.19 + " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
13.20 + " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
13.21 " [BOOL e_e, REAL v_v]))";
13.22 TermC.parse thy scr;
13.23 \<close>
13.24 @@ -983,13 +983,13 @@
13.25 {rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule.e_rls, prls=PolyEq_prls, calc=[],
13.26 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
13.27 "Script Normalize_poly (e_e::bool) (v_v::real) = " ^
13.28 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
13.29 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
13.30 - " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
13.31 - " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.32 - " make_ratpoly_in False))) @@ " ^
13.33 - " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
13.34 - " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
13.35 + "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
13.36 + " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
13.37 + " (Try (Repeat (Rewrite_Set ''expand_binoms'' False))) @@ " ^
13.38 + " (Try (Repeat (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.39 + " ''make_ratpoly_in'' False))) @@ " ^
13.40 + " (Try (Repeat (Rewrite_Set ''polyeq_simplify'' False)))) e_e " ^
13.41 + " in (SubProblem (''PolyEq'',[''polynomial'',''univariate'',''equation''], [''no_met'']) " ^
13.42 " [BOOL e_e, REAL v_v]))")]
13.43 \<close>
13.44 setup \<open>KEStore_Elems.add_mets
13.45 @@ -1016,10 +1016,10 @@
13.46 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.47 nrls = norm_Rational},
13.48 "Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
13.49 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.50 - " d1_polyeq_simplify True)) @@ " ^
13.51 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.52 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
13.53 + "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.54 + " ''d1_polyeq_simplify'' True)) @@ " ^
13.55 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.56 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
13.57 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.58 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.59 \<close>
13.60 @@ -1033,13 +1033,13 @@
13.61 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.62 nrls = norm_Rational},
13.63 "Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
13.64 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.65 - " d2_polyeq_simplify True)) @@ " ^
13.66 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.67 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.68 - " d1_polyeq_simplify True)) @@ " ^
13.69 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.70 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
13.71 + " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.72 + " ''d2_polyeq_simplify'' True)) @@ " ^
13.73 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.74 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.75 + " ''d1_polyeq_simplify'' True)) @@ " ^
13.76 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.77 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
13.78 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.79 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.80 \<close>
13.81 @@ -1053,13 +1053,13 @@
13.82 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.83 nrls = norm_Rational},
13.84 "Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
13.85 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.86 - " d2_polyeq_bdv_only_simplify True)) @@ " ^
13.87 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.88 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.89 - " d1_polyeq_simplify True)) @@ " ^
13.90 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.91 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
13.92 + " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.93 + " ''d2_polyeq_bdv_only_simplify'' True)) @@ " ^
13.94 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.95 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.96 + " ''d1_polyeq_simplify'' True)) @@ " ^
13.97 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.98 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
13.99 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.100 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.101 \<close>
13.102 @@ -1073,10 +1073,10 @@
13.103 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.104 nrls = norm_Rational},
13.105 "Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
13.106 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.107 - " d2_polyeq_sq_only_simplify True)) @@ " ^
13.108 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.109 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
13.110 + " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.111 + " ''d2_polyeq_sq_only_simplify'' True)) @@ " ^
13.112 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.113 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e; " ^
13.114 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.115 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.116 \<close>
13.117 @@ -1090,10 +1090,10 @@
13.118 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.119 nrls = norm_Rational},
13.120 "Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
13.121 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.122 - " d2_polyeq_pqFormula_simplify True)) @@ " ^
13.123 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.124 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
13.125 + " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.126 + " ''d2_polyeq_pqFormula_simplify'' True)) @@ " ^
13.127 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.128 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
13.129 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.130 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.131 \<close>
13.132 @@ -1107,10 +1107,10 @@
13.133 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.134 nrls = norm_Rational},
13.135 "Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
13.136 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.137 - " d2_polyeq_abcFormula_simplify True)) @@ " ^
13.138 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.139 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
13.140 + " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.141 + " ''d2_polyeq_abcFormula_simplify'' True)) @@ " ^
13.142 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.143 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
13.144 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.145 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.146 \<close>
13.147 @@ -1124,16 +1124,16 @@
13.148 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
13.149 nrls = norm_Rational},
13.150 "Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
13.151 - " (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.152 - " d3_polyeq_simplify True)) @@ " ^
13.153 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.154 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.155 - " d2_polyeq_simplify True)) @@ " ^
13.156 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.157 - " (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
13.158 - " d1_polyeq_simplify True)) @@ " ^
13.159 - " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
13.160 - " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
13.161 + " (let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.162 + " ''d3_polyeq_simplify'' True)) @@ " ^
13.163 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.164 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.165 + " ''d2_polyeq_simplify'' True)) @@ " ^
13.166 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.167 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
13.168 + " ''d1_polyeq_simplify'' True)) @@ " ^
13.169 + " (Try (Rewrite_Set ''polyeq_simplify'' False)) @@ " ^
13.170 + " (Try (Rewrite_Set ''norm_Rational_parenthesized'' False))) e_e;" ^
13.171 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
13.172 " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
13.173 \<close>
14.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Dec 20 18:02:25 2018 +0100
14.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Wed Dec 26 14:24:05 2018 +0100
14.3 @@ -206,11 +206,11 @@
14.4 {rew_ord'="termlessI", rls'=rateq_erls, srls=Rule.e_rls, prls=RatEq_prls, calc=[],
14.5 crls=RatEq_crls, errpats = [], nrls = norm_Rational},
14.6 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^
14.7 - "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^
14.8 - " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^
14.9 - " (Repeat(Try (Rewrite_Set add_fractions_p False))) @@ " ^
14.10 - " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^
14.11 - " (L_L::bool list) = (SubProblem (RatEq',[univariate,equation], [no_met])" ^
14.12 + "(let e_e = ((Repeat(Try (Rewrite_Set ''RatEq_simplify'' True))) @@ " ^
14.13 + " (Repeat(Try (Rewrite_Set ''norm_Rational'' False))) @@ " ^
14.14 + " (Repeat(Try (Rewrite_Set ''add_fractions_p'' False))) @@ " ^
14.15 + " (Repeat(Try (Rewrite_Set ''RatEq_eliminate'' True)))) e_e;" ^
14.16 + " (L_L::bool list) = (SubProblem (''RatEq'',[''univariate'',''equation''], [''no_met''])" ^
14.17 " [BOOL e_e, REAL v_v]) " ^
14.18 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
14.19 \<close>
15.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Dec 20 18:02:25 2018 +0100
15.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Dec 26 14:24:05 2018 +0100
15.3 @@ -908,17 +908,17 @@
15.4 [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
15.5 crls = Rule.e_rls, errpats = [], nrls = norm_Rational_rls},
15.6 "Script SimplifyScript (t_t::real) = " ^
15.7 - " ((Try (Rewrite_Set discard_minus False) @@ " ^
15.8 - " Try (Rewrite_Set rat_mult_poly False) @@ " ^
15.9 - " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
15.10 - " Try (Rewrite_Set cancel_p_rls False) @@ " ^
15.11 + " ((Try (Rewrite_Set ''discard_minus'' False) @@ " ^
15.12 + " Try (Rewrite_Set ''rat_mult_poly'' False) @@ " ^
15.13 + " Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@ " ^
15.14 + " Try (Rewrite_Set ''cancel_p_rls'' False) @@ " ^
15.15 " (Repeat " ^
15.16 - " ((Try (Rewrite_Set add_fractions_p_rls False) @@ " ^
15.17 - " Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
15.18 - " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
15.19 - " Try (Rewrite_Set cancel_p_rls False) @@ " ^
15.20 - " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
15.21 - " Try (Rewrite_Set discard_parentheses1 False)) " ^
15.22 + " ((Try (Rewrite_Set ''add_fractions_p_rls'' False) @@ " ^
15.23 + " Try (Rewrite_Set ''rat_mult_div_pow'' False) @@ " ^
15.24 + " Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@" ^
15.25 + " Try (Rewrite_Set ''cancel_p_rls'' False) @@ " ^
15.26 + " Try (Rewrite_Set ''rat_reduce_1'' False)))) @@ " ^
15.27 + " Try (Rewrite_Set ''discard_parentheses1'' False)) " ^
15.28 " t_t)")]
15.29 \<close>
15.30
16.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Dec 20 18:02:25 2018 +0100
16.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Dec 26 14:24:05 2018 +0100
16.3 @@ -478,14 +478,14 @@
16.4
16.5 (*-------------------------Problem-----------------------*)
16.6 (*
16.7 -(get_pbt ["root'","univariate","equation"]);
16.8 +(get_pbt ["rootX","univariate","equation"]);
16.9 show_ptyps();
16.10 *)
16.11 \<close>
16.12 setup \<open>KEStore_Elems.add_pbts
16.13 (* ---------root----------- *)
16.14 [(Specify.prep_pbt thy "pbl_equ_univ_root" [] Celem.e_pblID
16.15 - (["root'","univariate","equation"],
16.16 + (["rootX","univariate","equation"],
16.17 [("#Given" ,["equality e_e","solveFor v_v"]),
16.18 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
16.19 "(rhs e_e) is_rootTerm_in (v_v::real)"]),
16.20 @@ -493,7 +493,7 @@
16.21 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
16.22 (* ---------sqrt----------- *)
16.23 (Specify.prep_pbt thy "pbl_equ_univ_root_sq" [] Celem.e_pblID
16.24 - (["sq","root'","univariate","equation"],
16.25 + (["sq","rootX","univariate","equation"],
16.26 [("#Given" ,["equality e_e","solveFor v_v"]),
16.27 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
16.28 " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
16.29 @@ -503,7 +503,7 @@
16.30 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq","solve_sq_root_equation"]])),
16.31 (* ---------normalise----------- *)
16.32 (Specify.prep_pbt thy "pbl_equ_univ_root_norm" [] Celem.e_pblID
16.33 - (["normalise","root'","univariate","equation"],
16.34 + (["normalise","rootX","univariate","equation"],
16.35 [("#Given" ,["equality e_e","solveFor v_v"]),
16.36 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
16.37 " Not((lhs e_e) is_normSqrtTerm_in (v_v::real))) | " ^
16.38 @@ -533,12 +533,12 @@
16.39 {rew_ord'="termlessI", rls'=RootEq_erls, srls=Rule.e_rls, prls=RootEq_prls, calc=[],
16.40 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
16.41 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
16.42 - "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
16.43 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
16.44 - " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
16.45 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
16.46 - " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
16.47 - " in ((SubProblem (RootEq',[univariate,equation], " ^
16.48 + "(let e_e = ((Repeat(Try (Rewrite ''makex1_x'' False))) @@ " ^
16.49 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
16.50 + " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
16.51 + " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
16.52 + " (Try (Rewrite_Set ''rooteq_simplify'' True))) e_e " ^
16.53 + " in ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
16.54 " [no_met]) [BOOL e_e, REAL v_v])))")]
16.55 \<close>
16.56 setup \<open>KEStore_Elems.add_mets
16.57 @@ -554,16 +554,16 @@
16.58 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
16.59 "Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
16.60 "(let e_e = " ^
16.61 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
16.62 - " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
16.63 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
16.64 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
16.65 - " (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
16.66 + " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''sqrt_isolate'' True)) @@ " ^
16.67 + " (Try (Rewrite_Set ''rooteq_simplify'' True)) @@ " ^
16.68 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
16.69 + " (Try (Repeat (Rewrite_Set ''make_rooteq '' False))) @@ " ^
16.70 + " (Try (Rewrite_Set ''rooteq_simplify'' True)) ) e_e; " ^
16.71 " (L_L::bool list) = " ^
16.72 " (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
16.73 - " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
16.74 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
16.75 - " else (SubProblem (RootEq',[univariate,equation], [no_met]) " ^
16.76 + " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
16.77 + " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
16.78 + " else (SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met'']) " ^
16.79 " [BOOL e_e, REAL v_v])) " ^
16.80 "in Check_elementwise L_L {(v_v::real). Assumptions})")]
16.81 \<close>
16.82 @@ -578,15 +578,15 @@
16.83 crls = RootEq_crls, errpats = [], nrls = norm_Poly},
16.84 "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
16.85 "(let e_e = " ^
16.86 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
16.87 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
16.88 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
16.89 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
16.90 - " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
16.91 + " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''r_sqrt_isolate'' False)) @@ " ^
16.92 + " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
16.93 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
16.94 + " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
16.95 + " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
16.96 " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
16.97 - " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
16.98 + " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
16.99 " [no_met]) [BOOL e_e, REAL v_v]) " ^
16.100 - " else ((SubProblem (RootEq',[univariate,equation], " ^
16.101 + " else ((SubProblem (''RootEq'',[''univariate'',equation''], " ^
16.102 " [no_met]) [BOOL e_e, REAL v_v])))")]
16.103 \<close>
16.104 (*-- left 28.08.02 --*)
16.105 @@ -600,16 +600,16 @@
16.106 crls=RootEq_crls, errpats = [], nrls = norm_Poly},
16.107 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
16.108 "(let e_e = " ^
16.109 - " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
16.110 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
16.111 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
16.112 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
16.113 - " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
16.114 + " ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''l_sqrt_isolate'' False)) @@ " ^
16.115 + " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
16.116 + " (Try (Repeat (Rewrite_Set ''expand_rootbinoms'' False))) @@ " ^
16.117 + " (Try (Repeat (Rewrite_Set ''make_rooteq'' False))) @@ " ^
16.118 + " (Try (Rewrite_Set ''rooteq_simplify'' False))) e_e " ^
16.119 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
16.120 - " then (SubProblem (RootEq',[normalise,root',univariate,equation], " ^
16.121 - " [no_met]) [BOOL e_e, REAL v_v]) " ^
16.122 - " else ((SubProblem (RootEq',[univariate,equation], " ^
16.123 - " [no_met]) [BOOL e_e, REAL v_v])))")]
16.124 + " then (SubProblem (''RootEq'',[''normalise'',''rootX'',''univariate'',''equation''], " ^
16.125 + " [''no_met'']) [BOOL e_e, REAL v_v]) " ^
16.126 + " else ((SubProblem (''RootEq'',[''univariate'',''equation''], " ^
16.127 + " [''no_met'']) [BOOL e_e, REAL v_v])))")]
16.128 \<close>
16.129
16.130 setup \<open>KEStore_Elems.add_calcs
17.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Dec 20 18:02:25 2018 +0100
17.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Wed Dec 26 14:24:05 2018 +0100
17.3 @@ -134,13 +134,13 @@
17.4 ML \<open>
17.5 (*-----------------------probleme------------------------*)
17.6 (*
17.7 -(get_pbt ["rat","root'","univariate","equation"]);
17.8 +(get_pbt ["rat","rootX","univariate","equation"]);
17.9 show_ptyps();
17.10 *)
17.11 \<close>
17.12 setup \<open>KEStore_Elems.add_pbts
17.13 [(Specify.prep_pbt thy "pbl_equ_univ_root_sq_rat" [] Celem.e_pblID
17.14 - (["rat","sq","root'","univariate","equation"],
17.15 + (["rat","sq","rootX","univariate","equation"],
17.16 [("#Given" ,["equality e_e","solveFor v_v"]),
17.17 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
17.18 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]),
17.19 @@ -165,13 +165,13 @@
17.20 {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule.e_rls, prls=RootRatEq_prls, calc=[],
17.21 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
17.22 "Script Elim_rootrat_equation (e_e::bool) (v_v::real) = " ^
17.23 - "(let e_e = ((Try (Rewrite_Set expand_rootbinoms False)) @@ " ^
17.24 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
17.25 - " (Try (Rewrite_Set make_rooteq False)) @@ " ^
17.26 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
17.27 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] " ^
17.28 - " rootrat_solve False))) e_e " ^
17.29 - " in (SubProblem (RootEq',[univariate,equation], " ^
17.30 + "(let e_e = ((Try (Rewrite_Set ''expand_rootbinoms'' False)) @@ " ^
17.31 + " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
17.32 + " (Try (Rewrite_Set ''make_rooteq'' False)) @@ " ^
17.33 + " (Try (Rewrite_Set ''rooteq_simplify'' False)) @@ " ^
17.34 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] " ^
17.35 + " ''rootrat_solve'' False))) e_e " ^
17.36 + " in (SubProblem (''RootEq'',[''univariate'',''equation''], " ^
17.37 " [no_met]) [BOOL e_e, REAL v_v]))")]
17.38 \<close>
17.39
18.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Dec 20 18:02:25 2018 +0100
18.2 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Dec 26 14:24:05 2018 +0100
18.3 @@ -905,15 +905,15 @@
18.4 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
18.5 "(let e_e = " ^
18.6 " ((While (contains_root e_e) Do" ^
18.7 - " ((Rewrite square_equation_left True) @@" ^
18.8 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.9 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
18.10 - " (Try (Rewrite_Set isolate_root False)) @@" ^
18.11 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
18.12 - " (Try (Rewrite_Set norm_equation False)) @@" ^
18.13 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.14 - " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
18.15 - " (Try (Rewrite_Set Test_simplify False)))" ^
18.16 + " ((Rewrite ''square_equation_left'' True) @@" ^
18.17 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.18 + " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
18.19 + " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
18.20 + " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
18.21 + " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
18.22 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.23 + " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
18.24 + " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
18.25 " e_e" ^
18.26 " in [e_e::bool])")]
18.27 \<close>
18.28 @@ -933,15 +933,15 @@
18.29 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
18.30 "(let e_e = " ^
18.31 " ((While (contains_root e_e) Do" ^
18.32 - " ((Rewrite square_equation_left True) @@" ^
18.33 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.34 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
18.35 - " (Try (Rewrite_Set isolate_root False)) @@" ^
18.36 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
18.37 - " (Try (Rewrite_Set norm_equation False)) @@" ^
18.38 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.39 - " (Rewrite_Set_Inst [(bdv,v_v::real)] isolate_bdv False) @@" ^
18.40 - " (Try (Rewrite_Set Test_simplify False)))" ^
18.41 + " ((Rewrite ''square_equation_left'' True) @@" ^
18.42 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.43 + " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
18.44 + " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
18.45 + " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
18.46 + " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
18.47 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.48 + " (Rewrite_Set_Inst [(''bdv'',v_v::real)] ''isolate_bdv'' False) @@" ^
18.49 + " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
18.50 " e_e;" ^
18.51 " (L_L::bool list) = Tac subproblem_equation_dummy; " ^
18.52 " L_L = Tac solve_equation_dummy " ^
18.53 @@ -1007,16 +1007,16 @@
18.54 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
18.55 "(let e_e = " ^
18.56 " ((While (contains_root e_e) Do" ^
18.57 - " ((Rewrite square_equation_left True) @@" ^
18.58 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.59 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
18.60 - " (Try (Rewrite_Set isolate_root False)) @@" ^
18.61 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
18.62 - " (Try (Rewrite_Set norm_equation False)) @@" ^
18.63 - " (Try (Rewrite_Set Test_simplify False)))" ^
18.64 + " ((Rewrite ''square_equation_left'' True) @@" ^
18.65 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.66 + " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
18.67 + " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
18.68 + " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
18.69 + " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
18.70 + " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
18.71 " e_e;" ^
18.72 - " (L_L::bool list) = (SubProblem (Test',[LINEAR,univariate,equation,test]," ^
18.73 - " [Test,solve_linear]) [BOOL e_e, REAL v_v])" ^
18.74 + " (L_L::bool list) = (SubProblem (''Test'',[''LINEAR'',''univariate'',''equation'',''test'']," ^
18.75 + " [''Test'',''solve_linear'']) [BOOL e_e, REAL v_v])" ^
18.76 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
18.77 \<close>
18.78 partial_function (tailrec) dummy8 :: "real \<Rightarrow> real"
18.79 @@ -1035,17 +1035,17 @@
18.80 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
18.81 "(let e_e = " ^
18.82 " ((While (contains_root e_e) Do" ^
18.83 - " (((Rewrite square_equation_left True) Or " ^
18.84 - " (Rewrite square_equation_right True)) @@" ^
18.85 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.86 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
18.87 - " (Try (Rewrite_Set isolate_root False)) @@" ^
18.88 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
18.89 - " (Try (Rewrite_Set norm_equation False)) @@" ^
18.90 - " (Try (Rewrite_Set Test_simplify False)))" ^
18.91 + " (((Rewrite ''square_equation_left'' True) Or " ^
18.92 + " (Rewrite ''square_equation_right'' True)) @@" ^
18.93 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.94 + " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
18.95 + " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
18.96 + " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
18.97 + " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
18.98 + " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
18.99 " e_e;" ^
18.100 - " (L_L::bool list) = (SubProblem (Test',[plain_square,univariate,equation,test]," ^
18.101 - " [Test,solve_plain_square]) [BOOL e_e, REAL v_v])" ^
18.102 + " (L_L::bool list) = (SubProblem (''Test'',[''plain_square'',''univariate'',''equation'',''test'']," ^
18.103 + " [''Test'',''solve_plain_square'']) [BOOL e_e, REAL v_v])" ^
18.104 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
18.105 \<close>
18.106 partial_function (tailrec) dummy9 :: "real \<Rightarrow> real"
18.107 @@ -1064,17 +1064,17 @@
18.108 "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
18.109 "(let e_e = " ^
18.110 " ((While (contains_root e_e) Do" ^
18.111 - " (((Rewrite square_equation_left True) Or" ^
18.112 - " (Rewrite square_equation_right True)) @@" ^
18.113 - " (Try (Rewrite_Set Test_simplify False)) @@" ^
18.114 - " (Try (Rewrite_Set rearrange_assoc False)) @@" ^
18.115 - " (Try (Rewrite_Set isolate_root False)) @@" ^
18.116 - " (Try (Rewrite_Set Test_simplify False)))) @@" ^
18.117 - " (Try (Rewrite_Set norm_equation False)) @@" ^
18.118 - " (Try (Rewrite_Set Test_simplify False)))" ^
18.119 + " (((Rewrite ''square_equation_left'' True) Or" ^
18.120 + " (Rewrite ''square_equation_right'' True)) @@" ^
18.121 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@" ^
18.122 + " (Try (Rewrite_Set ''rearrange_assoc'' False)) @@" ^
18.123 + " (Try (Rewrite_Set ''isolate_root'' False)) @@" ^
18.124 + " (Try (Rewrite_Set ''Test_simplify'' False)))) @@" ^
18.125 + " (Try (Rewrite_Set ''norm_equation'' False)) @@" ^
18.126 + " (Try (Rewrite_Set ''Test_simplify'' False)))" ^
18.127 " e_e;" ^
18.128 - " (L_L::bool list) = (SubProblem (Test',[univariate,equation,test]," ^
18.129 - " [no_met]) [BOOL e_e, REAL v_v])" ^
18.130 + " (L_L::bool list) = (SubProblem (''Test'',[''univariate'',''equation'',''test'']," ^
18.131 + " [''no_met'']) [BOOL e_e, REAL v_v])" ^
18.132 " in Check_elementwise L_L {(v_v::real). Assumptions})")]
18.133 \<close>
18.134 partial_function (tailrec) dummy10 :: "real \<Rightarrow> real"
18.135 @@ -1093,11 +1093,11 @@
18.136 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule.e_rls(*,
18.137 asm_rls=[],asm_thm=[]*)},
18.138 "Script Solve_plain_square (e_e::bool) (v_v::real) = " ^
18.139 - " (let e_e = ((Try (Rewrite_Set isolate_bdv False)) @@ " ^
18.140 - " (Try (Rewrite_Set Test_simplify False)) @@ " ^
18.141 - " ((Rewrite square_equality_0 False) Or " ^
18.142 - " (Rewrite square_equality True)) @@ " ^
18.143 - " (Try (Rewrite_Set tval_rls False))) e_e " ^
18.144 + " (let e_e = ((Try (Rewrite_Set ''isolate_bdv'' False)) @@ " ^
18.145 + " (Try (Rewrite_Set ''Test_simplify'' False)) @@ " ^
18.146 + " ((Rewrite ''square_equality_0'' False) Or " ^
18.147 + " (Rewrite ''square_equality'' True)) @@ " ^
18.148 + " (Try (Rewrite_Set ''tval_rls'' False))) e_e " ^
18.149 " in ((Or_to_List e_e)::bool list))")]
18.150 \<close>
18.151 subsection \<open>polynomial equation\<close>
18.152 @@ -1112,10 +1112,10 @@
18.153 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule.e_rls,prls=Rule.e_rls, calc=[], crls=tval_rls,
18.154 errpats = [], nrls = Rule.e_rls},
18.155 "Script Norm_univar_equation (e_e::bool) (v_v::real) = " ^
18.156 - " (let e_e = ((Try (Rewrite rnorm_equation_add False)) @@ " ^
18.157 - " (Try (Rewrite_Set Test_simplify False))) e_e " ^
18.158 - " in (SubProblem (Test',[univariate,equation,test], " ^
18.159 - " [no_met]) [BOOL e_e, REAL v_v]))")]
18.160 + " (let e_e = ((Try (Rewrite ''rnorm_equation_add'' False)) @@ " ^
18.161 + " (Try (Rewrite_Set ''Test_simplify'' False))) e_e " ^
18.162 + " in (SubProblem (''Test'',[''univariate'',''equation'',''test''], " ^
18.163 + " [''no_met'']) [BOOL e_e, REAL v_v]))")]
18.164 \<close>
18.165 subsection \<open>diophantine equation\<close>
18.166 partial_function (tailrec) dummy12 :: "real \<Rightarrow> real"
19.1 --- a/test/Tools/isac/Interpret/inform.sml Thu Dec 20 18:02:25 2018 +0100
19.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Dec 26 14:24:05 2018 +0100
19.3 @@ -1400,7 +1400,7 @@
19.4 1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
19.5 ...
19.6 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
19.7 - Subproblem["sq", "root'", "univariate", "equation"]
19.8 + Subproblem["sq", "rootX", "univariate", "equation"]
19.9 ...
19.10 6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
19.11 Subproblem["normalise", "polynomial", "univariate", "equation"]
20.1 --- a/test/Tools/isac/Knowledge/rlang.sml Thu Dec 20 18:02:25 2018 +0100
20.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Wed Dec 26 14:24:05 2018 +0100
20.3 @@ -873,13 +873,13 @@
20.4 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
20.5 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
20.6 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.7 -(* val nxt = ("Model_Problem",Model_Problem ["normalise","root'","univariate","equation"])*)
20.8 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.9 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.10 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.11 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.12 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.13 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
20.14 +(* val nxt = ("Model_Problem",Model_Problem ["normalise","rootX","univariate","equation"])*)
20.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.20 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"]) *)
20.21 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.24 @@ -887,7 +887,7 @@
20.25 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.26 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.28 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
20.29 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"]) *)
20.30 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.32 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.33 @@ -1055,15 +1055,15 @@
20.34 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
20.35
20.36 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.37 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
20.38 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.39 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.40 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.41 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.42 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.43 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.44 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.45 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
20.46 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"]) *)
20.47 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.48 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.49 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.50 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.51 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.52 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.53 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.54 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"]) *)
20.55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.58 @@ -1072,7 +1072,7 @@
20.59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
20.61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.62 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
20.63 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"]) *)
20.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.67 @@ -1520,15 +1520,15 @@
20.68 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
20.69
20.70 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.71 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
20.72 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.73 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.74 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.75 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.76 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.77 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.78 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.79 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
20.80 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"])*)
20.81 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.82 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.83 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.85 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.88 +(* val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"])*)
20.89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.92 @@ -1581,7 +1581,7 @@
20.93 "solveFor x","solutions L"];
20.94 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
20.95 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.96 -(*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
20.97 +(*val nxt = ("Model_Problem",Model_Problem ["sq","rootX","univariate","equation"]) *)
20.98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.101 @@ -1740,7 +1740,7 @@
20.102 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
20.103
20.104 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.105 -(* Model_Problem ["normalise","root'","univariate","equation"])*)
20.106 +(* Model_Problem ["normalise","rootX","univariate","equation"])*)
20.107 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.108 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.109 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.110 @@ -1749,7 +1749,7 @@
20.111 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.112 (*val nxt = Subproblem ("RootEq",["univariate","equation"]))*)
20.113 val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.114 -(*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
20.115 +(*val nxt = Model_Problem ["sq","rootX","univariate","equation"]) *)
20.116 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.117 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
20.118 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Thu Dec 20 18:02:25 2018 +0100
21.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Wed Dec 26 14:24:05 2018 +0100
21.3 @@ -86,11 +86,11 @@
21.4
21.5
21.6 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
21.7 - (get_pbt ["root'","univariate","equation"]);
21.8 + (get_pbt ["rootX","univariate","equation"]);
21.9 case result of Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
21.10
21.11 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
21.12 - (get_pbt ["root'","univariate","equation"]);
21.13 + (get_pbt ["rootX","univariate","equation"]);
21.14 case result of NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
21.15
21.16 (*---------rooteq---- 23.8.02 ---------------------*)
21.17 @@ -218,7 +218,7 @@
21.18 val (dI',pI',mI') = ("RootEq",["univariate","equation"],["no_met"]);
21.19
21.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
21.21 -(*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
21.22 +(*val nxt = Model_Problem ["sq","rootX","univariate","equation"]) *)
21.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.25 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.26 @@ -229,7 +229,7 @@
21.27 (*"13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"))
21.28 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
21.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.30 -(*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
21.31 +(*val nxt = Model_Problem ["sq","rootX","univariate","equation"]) *)
21.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.35 @@ -268,7 +268,7 @@
21.36 val fmz =
21.37 ["equality (13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x)",
21.38 "solveFor x","solutions L"];
21.39 -val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
21.40 +val (dI',pI',mI') = ("RootEq",["sq","rootX","univariate","equation"],
21.41 ["RootEq","solve_sq_root_equation"]);
21.42 (*val p = e_pos'; val c = [];
21.43 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
21.44 @@ -319,7 +319,7 @@
21.45
21.46 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- OKversion----";
21.47 val fmz = ["equality (sqrt(x) = 1)","solveFor x","solutions L"];
21.48 -val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
21.49 +val (dI',pI',mI') = ("RootEq",["sq","rootX","univariate","equation"],
21.50 ["RootEq","solve_sq_root_equation"]);
21.51 (*val p = e_pos'; val c = [];
21.52 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
21.53 @@ -371,7 +371,7 @@
21.54 --------------------------------*)
21.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.56 (*val p = ([4],Res) val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 1]"))
21.57 -val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *)
21.58 +val nxt = Check_Postcond ["sq","rootX","univariate","equation"]) *)
21.59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.60 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
21.61 then () else error "diff.behav. in rooteq.sml: sqrt(x) = 1";
21.62 @@ -380,7 +380,7 @@
21.63 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
21.64 \ with same error";
21.65 val fmz = ["equality (sqrt x = sqrt x)","solveFor x","solutions L"];
21.66 -val (dI',pI',mI') = ("RootEq",["sq","root'","univariate","equation"],
21.67 +val (dI',pI',mI') = ("RootEq",["sq","rootX","univariate","equation"],
21.68 ["RootEq","solve_sq_root_equation"]);
21.69 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
21.70 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.71 @@ -420,7 +420,7 @@
21.72 val nxt = Check_elementwise "Assumptions"*)
21.73 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.74 (*val p = ([3],Res) val f = (FormKF (~1,EdUndef,1,Nundef,"UniversalList"))
21.75 -val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *)
21.76 +val nxt = Check_Postcond ["sq","rootX","univariate","equation"]) *)
21.77 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.78 if p = ([],Res) andalso f = Form'(FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
21.79 then () else error "new behav. in rooteq.sml: sqrt x = sqrt x";
21.80 @@ -441,7 +441,7 @@
21.81 (* "6 + x = 60 + 13 * x + -6 * sqrt ((3 + x) * (33 + 4 * x))")) : mout
21.82 val nxt = ("Subproblem",Subproblem ("RootEq",["univariate","equation"]))*)
21.83 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.84 -(*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
21.85 +(*val nxt = Model_Problem ["sq","rootX","univariate","equation"]) *)
21.86 val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.87 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
21.88 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Thu Dec 20 18:02:25 2018 +0100
22.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Wed Dec 26 14:24:05 2018 +0100
22.3 @@ -75,7 +75,7 @@
22.4 *)
22.5 if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then ()
22.6 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
22.7 -(*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*)
22.8 +(*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"])*)
22.9 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.10 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.11 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.12 @@ -98,7 +98,7 @@
22.13 val pIopt = get_pblID (pt,ip);
22.14 ip; (*= ([3, 2], Res)*)
22.15 tacis; (*= []*)
22.16 -pIopt; (*= SOME ["sq", "root'", "univariate", "equation"]*)
22.17 +pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
22.18 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
22.19 "~~~~~ fun nxt_solve_, args:"; (*stopped due to strange exn
22.20 "check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
22.21 @@ -109,7 +109,7 @@
22.22 " ((rhs (1 = 2 * (1 + -1 * sqrt x))) is_sqrtTerm_in x)");
22.23 val SOME (t, _) = rewrite_set_ thy true rooteq_srls t;
22.24 term2str t = "True | True"; (*...was same in 2002 (NOT "True"); so program seems to take
22.25 - [univariate,equation] and to refine to ["sq", "root'", "univariate", "equation"] in 2002*)
22.26 + [univariate,equation] and to refine to ["sq", "rootX", "univariate", "equation"] in 2002*)
22.27
22.28 (*(*these are the errors during stepping into the code:*)
22.29 nxt_solve_ (pt,ip); (*check_elementwise: no set 1 = 2 + -2 * sqrt x: fun mk_set raises
22.30 @@ -126,7 +126,7 @@
22.31
22.32 if f2str f = "1 = 2 + -2 * sqrt x" then ()
22.33 else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 b";
22.34 -(*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"]) ?!? the SAME as above*)
22.35 +(*-> Subproblem ("RootRatEq", ["sq", "rootX", "univariate", "equation"]) ?!? the SAME as above*)
22.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
22.37 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
22.38 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
23.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Thu Dec 20 18:02:25 2018 +0100
23.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Wed Dec 26 14:24:05 2018 +0100
23.3 @@ -57,7 +57,7 @@
23.4
23.5 KEStore_Elems.add_pbts
23.6 [prep_pbt (*Test.thy*) (theory "Isac")
23.7 - (["root'","univariate","equation","test"],
23.8 + (["rootX","univariate","equation","test"],
23.9 [("#Given" ,["equality e_e","solveFor v_v"]),
23.10 ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
23.11 ("#Find" ,["solutions v_i_"])],
23.12 @@ -65,7 +65,7 @@
23.13 [("Test","methode")])]
23.14 thy;
23.15
23.16 -match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root'","univariate","equation","test"]);
23.17 +match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["rootX","univariate","equation","test"]);
23.18
23.19 KEStore_Elems.add_pbts
23.20 [prep_pbt (theory "Isac")
24.1 --- a/test/Tools/isac/Test_Some.thy Thu Dec 20 18:02:25 2018 +0100
24.2 +++ b/test/Tools/isac/Test_Some.thy Wed Dec 26 14:24:05 2018 +0100
24.3 @@ -27,15 +27,14 @@
24.4 open Rule; string_of_thm;
24.5 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
24.6 \<close>
24.7 -ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
24.8 -ML_file "Interpret/mstools.sml"
24.9 +ML_file "ProgLang/scrtools.sml"
24.10
24.11 section \<open>code for copy & paste ===============================================================\<close>
24.12 ML \<open>
24.13 -"~~~~~ fun , args:"; val () = ();
24.14 -"~~~~~ and , args:"; val () = ();
24.15 +"~~~~~ fun xxx, args:"; val () = ();
24.16 +"~~~~~ and xxx, args:"; val () = ();
24.17
24.18 -"~~~~~ to return val:"; val () = ();
24.19 +"~~~~~ to xxx return val:"; val () = ();
24.20
24.21 \<close>
24.22 text \<open>
24.23 @@ -60,9 +59,137 @@
24.24
24.25 section \<open>===================================================================================\<close>
24.26 ML \<open>
24.27 +"~~~~~ fun , args:"; val () = ();
24.28 \<close> ML \<open>
24.29 +"-------- test the same called by interSteps norm_Rational -------";
24.30 +"-------- test the same called by interSteps norm_Rational -------";
24.31 +"-------- test the same called by interSteps norm_Rational -------";
24.32 +
24.33 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
24.34 +writeln(term2str auto_script);
24.35 +atomty auto_script;
24.36 +(***
24.37 +*** Const (Script.Stepwise, 'z => 'z => 'z)
24.38 +*** . Free (t_t, 'z)
24.39 +*** . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
24.40 +*** . . Const (Script.Try, ('a => 'a) => 'a => 'a)
24.41 +*** . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
24.42 +*** . . . . Free (discard_minus, ID)
24.43 +*** . . . . Const (HOL.False, bool)
24.44 +*** . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
24.45 +*** . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
24.46 +*** . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
24.47 +*** . . . . . Free (rat_mult_poly, ID)
24.48 +*** . . . . . Const (HOL.False, bool)
24.49 +*** . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
24.50 +*** . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
24.51 +*** . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
24.52 +*** . . . . . . Free (make_rat_poly_with_parentheses, ID)
24.53 +*** . . . . . . Const (HOL.False, bool)
24.54 +*** . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
24.55 +*** . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
24.56 +*** . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
24.57 +*** . . . . . . . Free (cancel_p_rls, ID)
24.58 +*** . . . . . . . Const (HOL.False, bool)
24.59 +*** . . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
24.60 +*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
24.61 +*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
24.62 +*** . . . . . . . . Free (norm_Rational_rls, ID)
24.63 +*** . . . . . . . . Const (HOL.False, bool)
24.64 +*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)
24.65 +*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)
24.66 +*** . . . . . . . . Free (discard_parentheses1, ID)
24.67 +*** . . . . . . . . Const (HOL.False, bool)
24.68 +*** . . Const (empty, 'a)
24.69 +***)
24.70 \<close> ML \<open>
24.71 +reset_states ();
24.72 +CalcTree
24.73 +[(["Term (b + a - b)", "normalform N"],
24.74 + ("Poly",["polynomial","simplification"],
24.75 + ["simplification","of_rationals"]))];
24.76 +Iterator 1;
24.77 +moveActiveRoot 1;
24.78 \<close> ML \<open>
24.79 +autoCalculate 1 CompleteCalc;
24.80 +
24.81 +\<close> ML \<open>
24.82 +"~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
24.83 +\<close> ML \<open>
24.84 + val pold = get_pos cI 1
24.85 +\<close> ML \<open>
24.86 + val x = Math_Engine.autocalc [] pold (get_calc cI) auto
24.87 +\<close> ML \<open>
24.88 +"~~~~~ fun autocalc, args:"; val (c: pos' list, (pos as (_, p_)), ((pt, _), _), auto) =
24.89 + ([], pold, (get_calc cI), auto);
24.90 +\<close> ML \<open>
24.91 +(*if*) Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos) (* = true*)
24.92 +\<close> ML \<open>
24.93 +val ptp = Chead.all_modspec (pt, pos);
24.94 +\<close> ML \<open>
24.95 +Solve.all_solve auto c ptp
24.96 +\<close> ML \<open>
24.97 +"~~~~~ fun all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)): ctree * pos')) = (auto, c, ptp);
24.98 +\<close> ML \<open>
24.99 + val (_, _, mI) = get_obj g_spec pt p
24.100 + val ctxt = get_ctxt pt pos
24.101 +\<close> ML \<open>
24.102 + val (_, c', ptp) = nxt_solv (Tac.Apply_Method' (mI, NONE, Selem.e_istate, ctxt)) (Selem.e_istate, ctxt) ptp
24.103 +\<close> ML \<open>
24.104 + complete_solve auto (c @ c') ptp
24.105 +\<close> ML \<open>
24.106 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) = (auto, (c @ c'), ptp);
24.107 +\<close> ML \<open>
24.108 +(*if*) p = ([], Res) (* = false*)
24.109 +\<close> ML \<open>
24.110 +(*if*) member op = [Pbl,Met] p_ (* = false*)
24.111 +\<close> ML \<open>
24.112 +nxt_solve_ ptp
24.113 +\<close> ML \<open>
24.114 +"~~~~~ fun nxt_solve_, args:"; val ((ptp as (pt, pos as (p, p_)))) = (ptp);
24.115 +\<close> ML \<open>
24.116 +(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*)
24.117 +\<close> ML \<open>
24.118 + val thy' = get_obj g_domID pt (par_pblobj pt p);
24.119 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
24.120 +\<close> ML \<open>
24.121 + val (tac_, is, (t, _)) = Lucin.next_tac (thy', srls) (pt, pos) sc is;
24.122 +\<close> ML \<open>
24.123 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
24.124 + (Selem.ScrState (E,l,a,v,s,_), ctxt)) =
24.125 + ((thy', srls), (pt, pos), sc, is);
24.126 +\<close> ML \<open>
24.127 +(*if*) l = [] (* = true*)
24.128 +\<close> ML \<open>
24.129 +appy thy ptp E [Celem.R] body NONE v
24.130 +\<close> ML \<open>
24.131 +"~~~~~ fun , args:"; val () = ();
24.132 +\<close> ML \<open>
24.133 +\<close> ML \<open>
24.134 +\<close> ML \<open>
24.135 +\<close> ML \<open>
24.136 +\<close> ML \<open>
24.137 +\<close> ML \<open>
24.138 +\<close> ML \<open>
24.139 +interSteps 1 ([], Res);
24.140 +val ((pt,p),_) = get_calc 1; show_pt pt;
24.141 +
24.142 +interSteps 1 ([1], Res);
24.143 +val ((pt,p),_) = get_calc 1; show_pt pt;
24.144 +
24.145 +(*with "Script SimplifyScript (t_::real) = \
24.146 + \ ((Rewrite_Set norm_Rational False) t_)"
24.147 +val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
24.148 +*)
24.149 +val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
24.150 +case (term2str form, tac, terms2strs asm) of
24.151 + ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
24.152 + | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
24.153 +
24.154 +
24.155 +\<close> ML \<open>
24.156 +\<close> ML \<open>
24.157 +"~~~~~ fun , args:"; val () = ();
24.158 \<close>
24.159
24.160 section \<open>===================================================================================\<close>