11 "table of contents --------------------------------------"; |
11 "table of contents --------------------------------------"; |
12 "--------------------------------------------------------"; |
12 "--------------------------------------------------------"; |
13 "----------- change to TermC.parse ctxt -----------------------"; |
13 "----------- change to TermC.parse ctxt -----------------------"; |
14 "----------- tryrefine ----------------------------------"; |
14 "----------- tryrefine ----------------------------------"; |
15 "----------- search for Or_to_List ----------------------"; |
15 "----------- search for Or_to_List ----------------------"; |
16 "----------- check thy in CalcTreeTEST ------------------"; |
16 "----------- check thy in Test_Code.init_calc @{context} ------------------"; |
17 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
17 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
18 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
18 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
19 "--------------------------------------------------------"; |
19 "--------------------------------------------------------"; |
20 "--------------------------------------------------------"; |
20 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
32 |
32 |
33 "----------- tryrefine ----------------------------------"; |
33 "----------- tryrefine ----------------------------------"; |
34 "----------- tryrefine ----------------------------------"; |
34 "----------- tryrefine ----------------------------------"; |
35 "----------- tryrefine ----------------------------------"; |
35 "----------- tryrefine ----------------------------------"; |
36 States.reset (); |
36 States.reset (); |
37 CalcTree [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
37 CalcTree @{context} [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
38 "solveFor x", "solutions L"], |
38 "solveFor x", "solutions L"], |
39 ("RatEq",["univariate", "equation"],["no_met"]))]; |
39 ("RatEq",["univariate", "equation"],["no_met"]))]; |
40 Iterator 1; |
40 Iterator 1; |
41 moveActiveRoot 1; autoCalculate 1 CompleteCalc; |
41 moveActiveRoot 1; autoCalculate 1 CompleteCalc; |
42 |
42 |
49 "--------- search for Or_to_List ------------------------"; |
49 "--------- search for Or_to_List ------------------------"; |
50 "--------- search for Or_to_List ------------------------"; |
50 "--------- search for Or_to_List ------------------------"; |
51 "--------- search for Or_to_List ------------------------"; |
51 "--------- search for Or_to_List ------------------------"; |
52 val fmz = ["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"]; |
52 val fmz = ["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"]; |
53 val (dI',pI',mI') = ("Isac_Knowledge", ["univariate", "equation"], ["no_met"]) |
53 val (dI',pI',mI') = ("Isac_Knowledge", ["univariate", "equation"], ["no_met"]) |
54 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
54 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; |
55 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
55 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
56 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
56 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
57 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
57 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
58 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
58 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
59 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
59 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
91 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*) |
91 val Next_Step (istate, ctxt, tac) = LI.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*) |
92 case tac of Or_to_List' _ => () |
92 case tac of Or_to_List' _ => () |
93 | _ => error "Or_to_List broken ?" |
93 | _ => error "Or_to_List broken ?" |
94 |
94 |
95 |
95 |
96 "----------- check thy in CalcTreeTEST ------------------"; |
96 "----------- check thy in Test_Code.init_calc @{context} ------------------"; |
97 "----------- check thy in CalcTreeTEST ------------------"; |
97 "----------- check thy in Test_Code.init_calc @{context} ------------------"; |
98 "----------- check thy in CalcTreeTEST ------------------"; |
98 "----------- check thy in Test_Code.init_calc @{context} ------------------"; |
99 "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^ |
99 "WN1109 with Inverse_Z_Transform.thy when starting tests with Test_Code.init_calc @{context} \n" ^ |
100 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^ |
100 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^ |
101 "Below there are the steps which found out the reason: \n" ^ |
101 "Below there are the steps which found out the reason: \n" ^ |
102 "store_pbt mistakenly stored that theory."; |
102 "store_pbt mistakenly stored that theory."; |
103 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge}; |
103 val ctxt = Proof_Context.init_global @{theory Isac_Knowledge}; |
104 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))"; |
104 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))"; |
107 val fmz = ["filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))", "boundVariable z", |
107 val fmz = ["filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))", "boundVariable z", |
108 "stepResponse (x[n::real]::bool)"]; |
108 "stepResponse (x[n::real]::bool)"]; |
109 val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], |
109 val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], |
110 ["SignalProcessing", "Z_Transform", "Inverse"]); |
110 ["SignalProcessing", "Z_Transform", "Inverse"]); |
111 |
111 |
112 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; |
112 val (p,_,fb,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))]; |
113 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) |
113 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) |
114 |
114 |
115 "~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))]; |
115 "~~~~~ fun Test_Code.init_calc @{context} , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))]; |
116 (*val ((pt, p), tacis) =*) |
116 (*val ((pt, p), tacis) =*) |
117 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp); |
117 Step_Specify.nxt_specify_init_calc ctxt (fmz, sp); |
118 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); |
118 "~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); |
119 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*) |
119 (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*) |
120 initialise (fmz, (dI, pI, mI)); |
120 initialise (fmz, (dI, pI, mI)); |
148 |
148 |
149 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
149 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
150 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
150 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
151 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
151 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------"; |
152 States.reset (); |
152 States.reset (); |
153 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
153 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
154 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))]; |
154 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))]; |
155 moveActiveRoot 1; |
155 moveActiveRoot 1; |
156 autoCalculate 1 CompleteCalcHead; |
156 autoCalculate 1 CompleteCalcHead; |
157 autoCalculate 1 (Steps 1); |
157 autoCalculate 1 (Steps 1); |
158 autoCalculate 1 (Steps 1); |
158 autoCalculate 1 (Steps 1); |
271 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
271 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
272 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
272 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
273 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
273 "----------- improved fun getTactic for interSteps and numeral calculations --"; |
274 val ctxt = Proof_Context.init_global @{theory Test}; |
274 val ctxt = Proof_Context.init_global @{theory Test}; |
275 States.reset (); val cI = 1; |
275 States.reset (); val cI = 1; |
276 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
276 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"], |
277 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))]; |
277 ("Test",["sqroot-test", "univariate", "equation", "test"],["Test", "squ-equ-test-subpbl1"]))]; |
278 moveActiveRoot 1; |
278 moveActiveRoot 1; |
279 autoCalculate 1 CompleteCalcHead; |
279 autoCalculate 1 CompleteCalcHead; |
280 autoCalculate 1 (Steps 1); |
280 autoCalculate 1 (Steps 1); |
281 |
281 |