1.1 --- a/doc-src/isac/jrocnik/Test_Z_Transform.thy Wed Sep 07 12:55:28 2011 +0200
1.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy Sat Sep 10 10:37:24 2011 +0200
1.3 @@ -36,9 +36,9 @@
1.4 rule1: "1 = \<delta>[n]" and
1.5 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
1.6 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
1.7 - rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^n * u [n]" and
1.8 - rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^n) * u [-n - 1]" and
1.9 - rule6: "|| z || > 1 ==> z/(z - 1)^2 = n * u [n]"
1.10 + rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
1.11 + rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
1.12 + rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
1.13 ML {*
1.14 @{thm rule1};
1.15 @{thm rule2};
1.16 @@ -68,12 +68,12 @@
1.17 *}
1.18 ML {*
1.19 val SOME (t, asm2) = rewrite_ thy ro er true (num_str @{thm rule4}) t;
1.20 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^ ?n * ?u [?n] + 1"; (*- real *)
1.21 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + 1"; (*- real *)
1.22 term2str t;
1.23 *}
1.24 ML {*
1.25 val SOME (t, asm3) = rewrite_ thy ro er true (num_str @{thm rule1}) t;
1.26 -term2str t = "- ?u [- ?n - 1] + \<alpha> ^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
1.27 +term2str t = "- ?u [- ?n - 1] + \<alpha> ^^^ ?n * ?u [?n] + ?\<delta> [?n]"; (*- real *)
1.28 term2str t;
1.29 *}
1.30 ML {*
1.31 @@ -87,7 +87,7 @@
1.32 val ctxt = ProofContext.init_global @{theory};
1.33 val ctxt = declare_constraints' [@{term "z::real"}] ctxt;
1.34
1.35 -val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^ -1)"; term2str fun1;
1.36 +val SOME fun1 = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
1.37 val SOME fun1' = parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * (1/z))"; term2str fun1';
1.38 *}
1.39
1.40 @@ -100,7 +100,7 @@
1.41 val SOME (fun2', asm1) = rewrite_ thy ro er true @{thm ruleZY} fun1'; term2str fun2';
1.42
1.43 val SOME (fun3,_) = rewrite_set_ @{theory Isac} false norm_Rational fun2;
1.44 -term2str fun3; (*fails on x^(-1) TODO*)
1.45 +term2str fun3; (*fails on x^^^(-1) TODO*)
1.46 val SOME (fun3',_) = rewrite_set_ @{theory Isac} false norm_Rational fun2';
1.47 term2str fun3'; (*OK*)
1.48
1.49 @@ -108,40 +108,53 @@
1.50 *}
1.51
1.52 subsection {*solve equation*}
1.53 -ML {*(*from test/Tools/isac/Minisubpbl/100-init-rootpbl.sml*)
1.54 +text {*this type of equation if too general for the present program*}
1.55 +ML {*
1.56 "----------- Minisubplb/100-init-rootp (*OK*)bl.sml ---------------------";
1.57 -val denominator = parseNEW ctxt "z^2 - 1/4*z - 1/8 = 0";
1.58 -val fmz = ["equality (z^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"];
1.59 +val denominator = parseNEW ctxt "z^^^2 - 1/4*z - 1/8 = 0";
1.60 +val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))", "solveFor z","solutions L"];
1.61 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.62 (* ^^^^^^^^^^^^^^^^^^^^^^ TODO: ISAC determines type of eq*)
1.63 *}
1.64 +text {*Does the Equation Match the Specification ?*}
1.65 +ML {*
1.66 +match_pbl fmz (get_pbt ["univariate","equation"]);
1.67 +*}
1.68 +
1.69 +ML {*
1.70 +val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^^^2 = 0";
1.71 +val fmz = (*specification*)
1.72 + ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", (*equality*)
1.73 + "solveFor z", (*bound variable*)
1.74 + "solutions L"]; (*identifier for solution*)
1.75 +(*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*)
1.76 +val (dI',pI',mI') =
1.77 + ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
1.78 +*}
1.79 +text {*Does the Other Equation Match the Specification ?*}
1.80 +ML {*
1.81 +match_pbl fmz (get_pbt ["pqFormula","degree_2","polynomial","univariate","equation"]);
1.82 +*}
1.83 +text {*Solve Equation Stepwise*}
1.84 ML {*
1.85 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.86 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.87 -(*[
1.88 -(([], Frm), solve (z ^ 2 - 1 / 4 * z - 1 / 8 = 0, z)),
1.89 -(([1], Frm), z ^ 2 - 1 / 4 * z - 1 / 8 = 0), bad rewrite order
1.90 -(([1], Res), -1 / 8 + z ^ 2 + -1 / 4 * z = 0), bad pattern
1.91 -(([2], Pbl), solve (-1 / 8 + z ^ 2 + -1 / 4 * z = 0, z)),
1.92 -(([2,1], Pbl), solve (-1 / 8 + z ^ 2 + -1 / 4 * z = 0, z)),
1.93 -(([2,1,1], Pbl), solve (-1 / 8 + z ^ 2 + -1 / 4 * z = 0, z)),
1.94 -(([2,1,1,1], Frm), -1 / 8 + z ^ 2 + -1 / 4 * z = 0)]
1.95 -*)
1.96 -*}
1.97 -ML {*
1.98 -val denominator = parseNEW ctxt "-1/8 + -1/4*z + z^2 = 0";
1.99 -(*ergebnis: [gleichung, was tun?, lösung]*)
1.100 -val fmz = ["equality (-1/8 + -1/4*z + z^2 = (0::real))", "solveFor z","solutions L"];
1.101 -(*liste der theoreme die zum lösen benötigt werden, aus isac, keine spezielle methode (no met)*)
1.102 -val (dI',pI',mI') =
1.103 - ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
1.104 -(*schritte abarbeiten*)
1.105 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.106 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.107 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.108 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*val nxt = ("Empty_Tac", ...): tac'_*)
1.110 -show_pt pt;
1.111 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.112 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.113 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.114 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.115 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.116 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.117 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.118 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
1.119 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.120 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
1.121 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.122 +show_pt pt;
1.123 +val SOME f = parseNEW ctxt "[z = 1 / 8 + 3 / 8, z = 1 / 8 + -3 / 8]";
1.124 *}
1.125
1.126 subsection {*partial fraction decomposition*}
1.127 @@ -190,8 +203,7 @@
1.128 ML {*
1.129 (*we use our ansatz2 to rewrite our expression and get an equilation with our expression on the left and the partial fractions of it on the right side*)
1.130 val SOME (t1,_) = rewrite_ @{theory Isac} e_rew_ord e_rls false @{thm ansatz2} expr';
1.131 -term2str t1;
1.132 -atomty t1;
1.133 +term2str t1; atomty t1;
1.134 val eq1 = HOLogic.mk_eq (expr', t1);
1.135 term2str eq1;
1.136 *}
1.137 @@ -216,8 +228,7 @@
1.138 val (numerator, denominator) = HOLogic.dest_eq eq3;
1.139 val eq3' = HOLogic.mk_eq (numerator, fract1); (*A B !*)
1.140 term2str eq3';
1.141 -*}
1.142 -ML {* (*MANDATORY: otherwise 3 = 0*)
1.143 +(*MANDATORY: simplify (and remove denominator) otherwise 3 = 0*)
1.144 val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';
1.145 term2str eq3'';
1.146 *}
1.147 @@ -228,17 +239,12 @@
1.148 (*substitude z with the first zeropoint to get A*)
1.149 val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
1.150 term2str eq4_1;
1.151 -*}
1.152 -ML {*
1.153 +
1.154 val SOME (eq4_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4_1;
1.155 term2str eq4_2;
1.156 -*}
1.157 -ML {*
1.158 +
1.159 val fmz = ["equality (3 = 3 * A / (4::real))", "solveFor A","solutions L"];
1.160 val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
1.161 -
1.162 -*}
1.163 -ML {*
1.164 (*solve the simple linear equilation for A TODO: return eq, not list of eq*)
1.165 val (p,_,fa,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.166 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.167 @@ -267,8 +273,6 @@
1.168 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.169 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.170 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.171 -*}
1.172 -ML {*
1.173 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
1.174 f2str fa;
1.175 *}
1.176 @@ -279,13 +283,10 @@
1.177 (*substitude z with the second zeropoint to get B*)
1.178 val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
1.179 term2str eq4b_1;
1.180 -*}
1.181
1.182 -ML {*
1.183 val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
1.184 term2str eq4b_2;
1.185 *}
1.186 -
1.187 ML {*
1.188 (*solve the simple linear equilation for B TODO: return eq, not list of eq*)
1.189 val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
1.190 @@ -382,20 +383,21 @@
1.191 crls = e_rls, nrls = e_rls},
1.192 "empty_script"
1.193 ));
1.194 -*}
1.195 -ML {*
1.196 +val thy = @{theory}; (*latest version of thy required*)
1.197 store_met
1.198 (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.199 - (["SignalProcessing", "Z_Transform", "inverse"], [],
1.200 + (["SignalProcessing", "Z_Transform", "inverse"],
1.201 + [("#Given" ,["equality X_eq"]),
1.202 + ("#Find" ,["equality n_eq"])
1.203 + ],
1.204 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
1.205 - crls = e_rls, nrls = e_rls},
1.206 + crls = e_rls, nrls = e_rls},
1.207 "Script InverseZTransform (Xeq::bool) =" ^
1.208 " (let X = Take Xeq;" ^
1.209 " X = Rewrite ruleZY False X" ^
1.210 " in X)"
1.211 ));
1.212 -*}
1.213 -ML {*
1.214 +
1.215 show_mets();
1.216 get_met ["SignalProcessing","Z_Transform","inverse"];
1.217 *}
1.218 @@ -425,6 +427,25 @@
1.219 atomty sc
1.220 *}
1.221
1.222 +
1.223 +subsection {*Store Final Version of Program for Execution*}
1.224 +ML {*
1.225 +store_met
1.226 + (prep_met thy "met_SP_Ztrans_inv" [] e_metID
1.227 + (["SignalProcessing", "Z_Transform", "inverse"],
1.228 + [("#Given" ,["equality X_eq"]),
1.229 + ("#Find" ,["equality n_eq"])
1.230 + ],
1.231 + {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls,
1.232 + crls = e_rls, nrls = e_rls},
1.233 + "Script InverseZTransform (Xeq::bool) =" ^
1.234 + " (let X = Take Xeq;" ^
1.235 + " X = Rewrite ruleZY False X" ^
1.236 + " in X)"
1.237 + ));
1.238 +*}
1.239 +
1.240 +
1.241 subsection {*Stepwise Execute the Program*}
1.242
1.243
2.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed Sep 07 12:55:28 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Sat Sep 10 10:37:24 2011 +0200
2.3 @@ -658,7 +658,7 @@
2.4 (*val thy = (assoc_thy o fst) metID*)
2.5 val gi = filter (eq "#Given") ppc;
2.6 val gi = (case gi of
2.7 - [] => []
2.8 + [] => (writeln ("prep_met: in " ^ guh ^ " #Given is empty ?!?"); [])
2.9 | ((_,gi')::[]) =>
2.10 ((map (split_did o term_of o the o (parse thy)) gi')
2.11 handle _ => error
2.12 @@ -671,8 +671,7 @@
2.13
2.14 val fi = filter (eq "#Find") ppc;
2.15 val fi = (case fi of
2.16 - [] => [](*28.8.01: ["tool"] ...// error
2.17 - ("prep_pbt: no '#Find' in "^(strs2str metID))*)
2.18 + [] => (writeln ("prep_met: in " ^ guh ^ " #Find is empty ?!?"); [])
2.19 | ((_,fi')::[]) =>
2.20 ((map (split_did o term_of o the o (parse thy)) fi')
2.21 handle _ => error
2.22 @@ -685,7 +684,7 @@
2.23
2.24 val re = filter (eq "#Relate") ppc;
2.25 val re = (case re of
2.26 - [] => []
2.27 + [] => (writeln ("prep_met: in " ^ guh ^ " #Relate is empty ?!?"); [])
2.28 | ((_,re')::[]) =>
2.29 ((map (split_did o term_of o the o (parse thy)) re')
2.30 handle _ => error
2.31 @@ -698,7 +697,7 @@
2.32
2.33 val wh = filter (eq "#Where") ppc;
2.34 val wh = (case wh of
2.35 - [] => []
2.36 + [] => (writeln ("prep_met: in " ^ guh ^ " #Where is empty ?!?"); [])
2.37 | ((_,wh')::[]) =>
2.38 ((map (parse_patt thy) wh')
2.39 handle _ => error
3.1 --- a/src/Tools/isac/Interpret/script.sml Wed Sep 07 12:55:28 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Sep 10 10:37:24 2011 +0200
3.3 @@ -1225,8 +1225,7 @@
3.4 else Steps (ScrState is, ss))
3.5
3.6 | NasApp _ => NotLocatable
3.7 - | err => (writeln ("*** " ^ PolyML.makestring err); NotLocatable)
3.8 - end
3.9 + | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err) end
3.10
3.11 | locate_gen _ m _ (sc,_) (is, _) =
3.12 error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
4.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Wed Sep 07 12:55:28 2011 +0200
4.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sat Sep 10 10:37:24 2011 +0200
4.3 @@ -1221,7 +1221,7 @@
4.4 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
4.5 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
4.6 " (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
4.7 - " in Check_elementwise L_LL {(v_v::real). Assumptions} )"
4.8 + " in Check_elementwise L_L {(v_v::real). Assumptions} )"
4.9 ));
4.10 *}
4.11 ML{*
5.1 --- a/test/Tools/isac/Frontend/interface.sml Wed Sep 07 12:55:28 2011 +0200
5.2 +++ b/test/Tools/isac/Frontend/interface.sml Sat Sep 10 10:37:24 2011 +0200
5.3 @@ -631,67 +631,9 @@
5.4 autoCalculate 1 (Step 1); fetchProposedTactic 1;
5.5 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
5.6 autoCalculate 1 (Step 1); fetchProposedTactic 1;
5.7 - (*==================================================================*)
5.8 setNextTactic 1 Or_to_List;
5.9 autoCalculate 1 (Step 1); fetchProposedTactic 1;
5.10 setNextTactic 1 (Check_elementwise "Assumptions");
5.11 - (*WAS: exception Match raised (line 1218 of ".../script.sml")*)
5.12 -"~~~~~ fun setNextTactic, args:"; val ((cI:calcID), tac) = (1, (Check_elementwise "Assumptions"));
5.13 -val ((pt, _), _) = get_calc cI;
5.14 -val ip = get_pos cI 1;
5.15 -(*locatetac tac (pt, ip) WAS: exception Match raised (line 1218 of ".../script.sml")*)
5.16 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
5.17 -val (mI,m) = mk_tac'_ tac;
5.18 -val Appl m = applicable_in p pt m;
5.19 -member op = specsteps mI (*false*);
5.20 -(* loc_solve_ (mI,m) ptp WAS: exception Match raised (line 1218 of ".../script.sml")*)
5.21 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
5.22 -(*solve m (pt, pos); WAS: exception Match raised (line 1218 of ".../script.sml")*)
5.23 -"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
5.24 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
5.25 - val thy' = get_obj g_domID pt (par_pblobj pt p);
5.26 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
5.27 - val d = e_rls;
5.28 -(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
5.29 - WAS: exception Match raised (line 1218 of "isabisac/src/Tools/isac/Interpret/script.sml"*)
5.30 -"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
5.31 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
5.32 - ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
5.33 -val thy = assoc_thy thy';
5.34 -l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
5.35 -(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
5.36 - ... Assoc ... is correct*)
5.37 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
5.38 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
5.39 -1 < length l (*true*);
5.40 -val up = drop_last l;
5.41 - term2str (go up sc);
5.42 - (go up sc);
5.43 -(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
5.44 - ... ???? ... is correct*)
5.45 -"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
5.46 - (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
5.47 - val l = drop_last l; (*comes from e, goes to Abs*)
5.48 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
5.49 - val i = mk_Free (i, T);
5.50 - val E = upd_env E (i, v);
5.51 -(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
5.52 -val [(tac_, mout, ptree, pos', xxx)] = ss;
5.53 -val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
5.54 -(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
5.55 - ... Assoc ... is correct*)
5.56 -"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
5.57 - ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
5.58 -val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
5.59 - val ctxt = get_ctxt pt (p,p_)
5.60 - val p' = lev_on p : pos;
5.61 -(* WAS val NotAss = assod pt d m stac
5.62 - ... Ass ... is correct*)
5.63 -"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
5.64 - (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
5.65 -consts = consts' (*WAS false*);
5.66 -(*==================================================================*)
5.67 -
5.68 autoCalculate 1 (Step 1); fetchProposedTactic 1;
5.69 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
5.70 "univariate","equation"]);
6.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 07 12:55:28 2011 +0200
6.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Sat Sep 10 10:37:24 2011 +0200
6.3 @@ -146,33 +146,89 @@
6.4 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.5 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.6 "----- d2_pqformula1 ------!!!!";
6.7 -val fmz = ["equality (-2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
6.8 -val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
6.9 -(*val p = e_pos'; val c = [];
6.10 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.11 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.12 +val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
6.13 +val (dI',pI',mI') =
6.14 + ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
6.15 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.16 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.17 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.18 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.19 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.20 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.21 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.22 -(*### or2list _ | _
6.23 - ([3],Res) "x = 2 | x = -1" Or_to_List*)
6.24 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.25 -(*### or2list _ | _
6.26 - ### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
6.27 - ([4],Res) "[x = 2, x = -1]" Check_elementwise "Assumptions"*)
6.28 -
6.29 -(*============ inhibit exn WN110906 ==============================================
6.30 -GOON WN110906
6.31 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.32 -(*### applicable_in Check_elementwise: --> ([x = 2, x = -1], [])
6.33 - ([5],Res) "[x = 2, x = -1]" Check_Postcond*)
6.34 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.35 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
6.36 - | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
6.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Apply_Method ["PolyEq", "solve_d2_polyeq_pq_equation"]*)
6.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.48 +(*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
6.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
6.50 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
6.51 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.52 +val (mI,m) = mk_tac'_ tac;
6.53 +val Appl m = applicable_in p pt m;
6.54 +val Check_elementwise' (trm1, str, (trm2, trms)) = m;
6.55 +term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
6.56 +str = "Assumptions";
6.57 +term2str trm2 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
6.58 +terms2str trms = "[\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n "^
6.59 + " (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + sqrt (9 / 16) / 2\","^
6.60 + "\"lhs (-1 / 8 + -1 * (1 / 8 + sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + sqrt (9 / 16) / 2) ^^^ 2 =\n 0) "^
6.61 + "has_degree_in 1 / 8 + sqrt (9 / 16) / 2 =\n2\","^
6.62 + "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) is_poly_in 1 / 8 + -1 * sqrt (9 / 16) / 2\","^
6.63 + "\"lhs (-1 / 8 + -1 * (1 / 8 + -1 * sqrt (9 / 16) / 2) / 4 +\n (1 / 8 + -1 * sqrt (9 / 16) / 2) ^^^ 2 =\n 0) has_degree_in 1 / 8 + -1 * sqrt (9 / 16) / 2 =\n2\"]";
6.64 +(*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
6.65 +member op = specsteps mI (*false*);
6.66 +(*loc_solve_ (mI,m) ptp;
6.67 + WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
6.68 +"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
6.69 +(*solve m (pt, pos);
6.70 + WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
6.71 +"~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
6.72 +e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
6.73 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.74 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
6.75 + val d = e_rls;
6.76 +(*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
6.77 + WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
6.78 +"~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
6.79 + (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
6.80 + ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
6.81 +val thy = assoc_thy thy';
6.82 +l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
6.83 +(*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
6.84 + ... Assoc ... is correct*)
6.85 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
6.86 + ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
6.87 +1 < length l (*true*);
6.88 +val up = drop_last l;
6.89 + term2str (go up sc);
6.90 + (go up sc);
6.91 +(*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
6.92 + ... ???? ... is correct*)
6.93 +"~~~~~ fun ass_up, args:"; val ((ys as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
6.94 + (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
6.95 + val l = drop_last l; (*comes from e, goes to Abs*)
6.96 + val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
6.97 + val i = mk_Free (i, T);
6.98 + val E = upd_env E (i, v);
6.99 +(*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
6.100 +val [(tac_, mout, ptree, pos', xxx)] = ss;
6.101 +val ss = [(tac_, mout, ptree, pos', []:(pos * pos_) list)];
6.102 +(*WAS val NasApp iss = assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
6.103 + ... Assoc ... is correct*)
6.104 +"~~~~~ fun assy, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
6.105 + ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
6.106 +val (a', STac stac) = handle_leaf "locate" thy' sr E a v t
6.107 + val ctxt = get_ctxt pt (p,p_)
6.108 + val p' = lev_on p : pos;
6.109 +(* WAS val NotAss = assod pt d m stac
6.110 + ... Ass ... is correct*)
6.111 +"~~~~~ fun assod, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
6.112 + (Const ("Script.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
6.113 +term2str consts;
6.114 +term2str consts';
6.115 +if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
6.116
6.117 "----- d2_pqformula1_neg ------";
6.118 (*EP-8*)
7.1 --- a/test/Tools/isac/Test_Some.thy Wed Sep 07 12:55:28 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Sat Sep 10 10:37:24 2011 +0200
7.3 @@ -7,121 +7,20 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 -text{*
7.8 -use"../../../test/Tools/isac/Knowledge/polyeq.sml"
7.9 -*}
7.10 +use"../../../test/Tools/isac/Frontend/interface.sml"
7.11
7.12 ML {*
7.13 val c = [];
7.14 print_depth 5;
7.15 *}
7.16 +ML {*
7.17
7.18 -ML {*
7.19 -"----------- test thm's d2_pq_formulsxx[_neg]---------------------";
7.20 -"----- d2_pqformula1 ------!!!!";
7.21 -val fmz = ["equality (-2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
7.22 -val (dI',pI',mI') =
7.23 - ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
7.24 - ["PolyEq","solve_d2_polyeq_pq_equation"]);
7.25 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.26 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.27 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.28 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.29 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.30 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.31 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.32 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*f = .. "x = 2 | x = -1", nxt = (". ", Or_to_List)*)
7.33 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.34 - (*f = "..[x = 2, x = -1]", nxt = ("..Check_elementwise "Assumptions")*)
7.35 -*}
7.36 -ML{*
7.37 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
7.38 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
7.39 -val (mI,m) = mk_tac'_ tac; (*m = Check_elementwise "Assumptions"*)
7.40 -val Appl m = applicable_in p pt m
7.41 -*}
7.42 -ML{*
7.43 -print_depth 5; PolyML.makestring m
7.44 -*}
7.45 -ML{*
7.46 -val Check_elementwise' (a,b,(c,d)) = m;
7.47 -term2str a;
7.48 -term2str c;
7.49 -terms2str d;
7.50 -*}
7.51 -ML{*
7.52 -print_depth 99; m;
7.53 *}
7.54 ML{*
7.55 *}
7.56 ML{*
7.57 *}
7.58 -ML{*
7.59 -locatetac tac (pt,p)
7.60 -val it = ("failure", ([], [], (Nd (PblObj {...}, [...]), ([4], ...)))): string *
7.61 -*}
7.62 -ML{* (*error*)
7.63 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.64 -
7.65 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.66 -case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
7.67 - | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
7.68 -
7.69 -"----- d2_pqformula1_neg ------";
7.70 -
7.71 -*}
7.72 -ML{*
7.73 -val xxx = @{theory};
7.74 -(writeln o PolyML.makestring) xxx;
7.75 -*}
7.76 -ML {*
7.77 -NotLocatable
7.78 -*}
7.79 -ML {*
7.80 -NasApp (e_scrstate,[])
7.81 -*}
7.82 -ML{*
7.83 -((writeln o PolyML.makestring) xxx; NasApp (e_scrstate,[]))
7.84 -*}
7.85 -text{*
7.86 -*** NasNap
7.87 -(Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $
7.88 - (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $
7.89 - Free ("x", "RealDef.real") $
7.90 - Free ("2", "RealDef.real")) $
7.91 - (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $
7.92 - (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $
7.93 - Free ("x", "RealDef.real") $
7.94 - Free ("-1", "RealDef.real")) $
7.95 - Const ("List.list.Nil", "HOL.bool List.list")),
7.96 -
7.97 -[(Free ("e_e", "HOL.bool"),
7.98 - Const ("HOL.disj", "HOL.bool \<Rightarrow> HOL.bool \<Rightarrow> HOL.bool") $
7.99 - (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $
7.100 - Free ("x", "RealDef.real") $
7.101 - Free ("2", "RealDef.real")) $
7.102 - (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $
7.103 - Free ("x", "RealDef.real") $
7.104 - Free ("-1", "RealDef.real"))),
7.105 - (Free ("v_v", "RealDef.real"), Free ("x", "RealDef.real")),
7.106 - (Free ("L_L", "HOL.bool List.list"),
7.107 - Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $
7.108 - (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $
7.109 - Free ("x", "RealDef.real") $
7.110 - Free ("2", "RealDef.real")) $
7.111 - (Const ("List.list.Cons", "HOL.bool \<Rightarrow> HOL.bool List.list \<Rightarrow> HOL.bool List.list") $
7.112 - (Const ("HOL.eq", "RealDef.real \<Rightarrow> RealDef.real \<Rightarrow> HOL.bool") $
7.113 - Free ("x", "RealDef.real") $
7.114 - Free ("-1", "RealDef.real")) $
7.115 - Const ("List.list.Nil", "HOL.bool List.list")))])
7.116 -*}
7.117 -ML{*
7.118 -*}
7.119 -ML{*
7.120 -*}
7.121 -ML{*
7.122 -*}
7.123 -ML{*
7.124 +ML {* (*=================*)
7.125 *}
7.126 ML{*
7.127 "~~~~~ fun , args:"; val () = ();