# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1318511008 -7200
# Node ID c2e6ac4a5d048a043a68665db754404e2adcda0c
# Parent  4c05940462a0fa50b79273fde3c5304b0d0f430d
Build_Inverse_Z_Transform 1 step further

the expected error in isac:
	prep. repair Apply_Method without init_form
was a simple error in the CTP-based program

diff -r 4c05940462a0 -r c2e6ac4a5d04 test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
--- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Oct 13 13:46:30 2011 +0200
+++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Oct 13 15:03:28 2011 +0200
@@ -596,7 +596,7 @@
 "      (equ::bool) = (denom = (0::real));" ^
 
 "      (L_L::bool list) = (SubProblem (PolyEq'," ^
-"          [abcFormula,degree_2,polynomial,univariate,equation],[no_meth])" ^
+"          [abcFormula,degree_2,polynomial,univariate,equation],[no_met])" ^
 "        [BOOL equ, REAL zzz])              " ^
 "  in X)"
  ));
@@ -641,9 +641,7 @@
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))"; (*TODO naming!*)
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
-*}
-ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Empty_Tac instead of SubProblem";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = SubProblem";
 *}
 text {* Instead of nxt = Subproblem above we had Empty_Tac; the search for the reason 
   considered the following points:
@@ -666,39 +664,24 @@
     ... shows the right script.difference in the arguments
   # test --- why helpless here ? --- shows: replace no_meth by [no_meth] in Script
 *}
+
 ML {*
-print_depth 9999;
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Empty_Tac instead Model_Problem";
-print_depth 9999;
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Model_Problem";
 *}
 text {* Instead of nxt = Model_Problem above we had Empty_Tac; the search for the reason 
   considered the following points:difference in the arguments
   # comparison with subsection { *solve equation* }: there solving this equation works,
-    so there must be some difference in the arguments of the Subproblem.
-
+    so there must be some difference in the arguments of the Subproblem:
+    RIGHT: we had [no_meth] instead of [no_met] ;-))
 *}
 ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Given equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Given solveFor z";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find solutions z_i";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Theory Isac";
 *}
-ML {*
-
-*}
-ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "solveFor z";
-*}
-ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Add_Find";
-*}
-ML {*
-show_pt pt;
-*}
-ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = (Empty_Tac";
-*}
-ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = (Empty_Tac instead Specify_Theory";
-*}
-text {* We had "nxt = (Empty_Tac"; the search for the reason considered the following points:
+text {* We had "nxt = Empty_Tac instead Specify_Theory; 
+  the search for the reason considered the following points:
   # was there an error message ? NO --ok
   # has "nxt = Add_Find" been inserted in pt: get_obj g_pbl pt (fst p); YES --ok
   # what is the returned "formula": print_depth 999; f; print_depth 999; --
@@ -721,50 +704,20 @@
   Or you leave the selection of the appropriate type to isac as done in the final Script ;-))
 *}
 ML {*
-val (p,_,f,nxt,_,pt) = me nxt p [] pt;
-*}
-ML {*
-
-*}
-ML {*
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Problem [abcFormula,...";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Specify_Method [PolyEq,solve_d2_polyeq_abc_equation";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method [PolyEq,solve_d2_polyeq_abc_equation";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite_Set_Inst ([(bdv, z)], d2_polyeq_abcFormula_simplify";
 show_pt pt;
 *}
 ML {*
 *}
 ML {*
-
-*}
-ML {*
-
-*}
-ML {*
-
-*}
-ML {*
-
-*}
-
-ML {*
-
-*}
-ML {*
-@{theory Isac}
-*}
-
-ML {*
-*}
-ML {*
 *}
 ML {*
 *}
 
 
-
-
-
-
-
-
 section {*Write Tests for Crucial Details*}
 text{*===================================*}
 ML {*
diff -r 4c05940462a0 -r c2e6ac4a5d04 test/Tools/isac/Knowledge/partial_fractions.sml
--- a/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Oct 13 13:46:30 2011 +0200
+++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Oct 13 15:03:28 2011 +0200
@@ -27,10 +27,8 @@
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
-  "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
-val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
-  "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
+val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
+val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
 val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
 val (pt, p) = ptp;
diff -r 4c05940462a0 -r c2e6ac4a5d04 test/Tools/isac/Test_Some.thy
--- a/test/Tools/isac/Test_Some.thy	Thu Oct 13 13:46:30 2011 +0200
+++ b/test/Tools/isac/Test_Some.thy	Thu Oct 13 15:03:28 2011 +0200
@@ -1,7 +1,7 @@
  
 theory Test_Some imports Isac begin
 
-use"../../../test/Tools/isac/Knowledge/partial_fractions.sml" 
+use"../../../test/Tools/isac/Interpret/rewtools.sml" 
 
 ML {* (*=================*)
 *}