15 "-----------------------------------------------------------------"; |
15 "-----------------------------------------------------------------"; |
16 "table of contents -----------------------------------------------"; |
16 "table of contents -----------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
18 "--------- interSteps on norm_Rational ---------------------------"; |
18 "--------- interSteps on norm_Rational ---------------------------"; |
19 (*---vvv NOT working after meNEW.04mmdd*) |
19 (*---vvv NOT working after meNEW.04mmdd*) |
20 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
20 "###### val intermediate_ptyps = !ptyps; val intermediate_mets = !mets"; |
21 "--------- prepare pbl, met --------------------------------------"; |
21 "--------- prepare pbl, met --------------------------------------"; |
22 "-------- cancel, without detail ------------------------------"; |
22 "-------- cancel, without detail ------------------------------"; |
23 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
23 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
24 "-------------- cancel_p, without detail ------------------------------"; |
24 "-------------- cancel_p, without detail ------------------------------"; |
25 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; |
25 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; |
28 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---"; |
28 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---"; |
29 "------ interSteps'detailrls' after CompleteCalc -----------------"; |
29 "------ interSteps'detailrls' after CompleteCalc -----------------"; |
30 "------ interSteps after appendFormula ---------------------------"; |
30 "------ interSteps after appendFormula ---------------------------"; |
31 (*---vvv not brought to work 0403*) |
31 (*---vvv not brought to work 0403*) |
32 "------ Detail_Set -----------------------------------------------"; |
32 "------ Detail_Set -----------------------------------------------"; |
33 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######"; |
33 "###### ptyps:= intermediate_ptyps; met:= intermediate_mets;#######"; |
34 "-----------------------------------------------------------------"; |
34 "-----------------------------------------------------------------"; |
35 "-----------------------------------------------------------------"; |
35 "-----------------------------------------------------------------"; |
36 "-----------------------------------------------------------------"; |
36 "-----------------------------------------------------------------"; |
37 |
37 |
38 val thy= @{theory Isac}; |
38 val thy= @{theory Isac}; |
39 "--------- interSteps on norm_Rational ---------------------------"; |
39 "--------- interSteps on norm_Rational ---------------------------"; |
40 "--------- interSteps on norm_Rational ---------------------------"; |
40 "--------- interSteps on norm_Rational ---------------------------"; |
41 "--------- interSteps on norm_Rational ---------------------------"; |
41 "--------- interSteps on norm_Rational ---------------------------"; |
42 states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*) |
42 states := []; (*exp_IsacCore_Simp_Rat_Double_No-7.xml*) |
43 CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"], |
43 CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))", "normalform N"], |
44 ("Rational", |
44 ("Rational", ["rational","simplification"], ["simplification","of_rationals"]))]; |
45 ["rational","simplification"], |
45 moveActiveRoot 1; |
46 ["simplification","of_rationals"]))]; |
46 autoCalculate 1 CompleteCalc; |
47 moveActiveRoot 1; |
47 val ((pt, _), _) = get_calc 1; show_pt pt; |
48 autoCalculate 1 CompleteCalc; |
|
49 val ((pt,_),_) = get_calc 1; show_pt pt; |
|
50 |
|
51 (*with "Script SimplifyScript (t_::real) = ----------------- |
|
52 \ ((Rewrite_Set norm_Rational False) t_)" |
|
53 case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*)) |
|
54 | _ => error "solve.sml: interSteps on norm_Rational 1"; |
|
55 interSteps 1 ([1], Res); |
|
56 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false; |
|
57 interSteps 1 ([1,3], Res); |
|
58 |
|
59 getTactic 1 ([1,4], Res) (*here get the tactic, and ...*); |
|
60 interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*); |
|
61 |
|
62 getTactic 1 ([1,5,1], Frm); |
|
63 val ((pt,_),_) = get_calc 1; show_pt pt; |
|
64 |
|
65 getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *); |
|
66 interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*); |
|
67 --------------------------------------------------------------------*) |
|
68 |
|
69 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => () |
48 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => () |
70 | _ => error "solve.sml: interSteps on norm_Rational 1"; |
49 | _ => error "solve.sml: interSteps on norm_Rational 1"; |
71 (*these have been done now by the script ^^^ immediately... |
|
72 interSteps 1 ([1], Res); |
|
73 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false; |
|
74 *) |
|
75 interSteps 1 ([6], Res); |
50 interSteps 1 ([6], Res); |
76 |
51 |
77 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*); |
52 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*); |
78 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*); |
53 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*); |
79 |
54 |
80 getTactic 1 ([3,4,1], Frm); |
55 getTactic 1 ([6,1,1], Frm); (*WN130909 <ERROR> syserror in getTactic </ERROR>*) |
81 val ((pt,_),_) = get_calc 1; show_pt pt; |
56 val ((pt,_),_) = get_calc 1; show_pt pt; |
82 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res)); |
57 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res)); |
83 case (term2str form, tac, terms2strs asm) of |
58 case (term2str form, tac, terms2strs asm) of |
84 ("1 / 2", Check_Postcond ["rational", "simplification"], |
59 ("1 / 2", Check_Postcond ["rational", "simplification"], []) => () |
85 ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => () |
|
86 | _ => error "solve.sml: interSteps on norm_Rational 2"; |
60 | _ => error "solve.sml: interSteps on norm_Rational 2"; |
87 |
61 get_obj g_res pt []; |
|
62 val (t, asm) = get_obj g_result pt []; |
|
63 if terms2str asm = "[\"8 * x ~= 0\",\"-9 + x ^^^ 2 ~= 0\"," ^ |
|
64 "\"(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9)) is_ratpolyexp\"]" |
|
65 then () else error "solve.sml: interSteps on norm_Rational 2, asms"; |
88 |
66 |
89 |
67 |
90 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
68 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
91 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
69 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
92 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
70 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets"; |
95 |
73 |
96 "--------- prepare pbl, met --------------------------------------"; |
74 "--------- prepare pbl, met --------------------------------------"; |
97 "--------- prepare pbl, met --------------------------------------"; |
75 "--------- prepare pbl, met --------------------------------------"; |
98 "--------- prepare pbl, met --------------------------------------"; |
76 "--------- prepare pbl, met --------------------------------------"; |
99 store_pbt |
77 store_pbt |
100 (prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID |
78 (prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID |
101 (["test"], |
79 (["test"], [], e_rls, NONE, [])); |
102 [], |
|
103 e_rls, NONE, [])); |
|
104 store_pbt |
80 store_pbt |
105 (prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID |
81 (prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID |
106 (["detail","test"], |
82 (["detail","test"], |
107 [("#Given" ,["realTestGiven t_t"]), |
83 [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])], |
108 ("#Find" ,["realTestFind s_s"]) |
84 e_rls, NONE, [["Test","test_detail"]])); |
109 ], |
|
110 e_rls, NONE, [["Test","test_detail"]])); |
|
111 |
85 |
112 store_met |
86 store_met |
113 (prep_met @{theory Test} "met_detbin" [] e_metID |
87 (prep_met @{theory Test} "met_detbin" [] e_metID |
114 (["Test","test_detail_binom"]:metID, |
88 (["Test", "test_detail_binom"] : metID, |
115 [("#Given" ,["realTestGiven t_t"]), |
89 [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])], |
116 ("#Find" ,["realTestFind s_s"]) |
90 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls, |
117 ], |
91 crls = tval_rls, errpats = [], nrls = e_rls}, |
118 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls, |
92 "Script Testterm (g_g::real) =" ^ |
119 crls = tval_rls, errpats = [], nrls = e_rls(*, |
93 "(((Rewrite_Set expand_binoms False) @@" ^ |
120 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)}, |
94 "(Rewrite_Set cancel_p False)) g_g)")); |
121 "Script Testterm (g_g::real) = \ |
|
122 \(((Rewrite_Set expand_binoms False) @@\ |
|
123 \ (Rewrite_Set cancel False)) g_g)" |
|
124 )); |
|
125 store_met |
95 store_met |
126 (prep_met @{theory Test} "met_detpoly" [] e_metID |
96 (prep_met @{theory Test} "met_detpoly" [] e_metID |
127 (["Test","test_detail_poly"]:metID, |
97 (["Test","test_detail_poly"] : metID, |
128 [("#Given" ,["realTestGiven t_t"]), |
98 [("#Given", ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])], |
129 ("#Find" ,["realTestFind s_s"]) |
99 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls, |
130 ], |
100 crls = tval_rls, errpats = [], nrls = e_rls}, |
131 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls, |
101 "Script Testterm (g_g::real) =" ^ |
132 crls = tval_rls, errpats = [], nrls = e_rls(*, |
102 "(((Rewrite_Set make_polynomial False) @@" ^ |
133 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)}, |
103 "(Rewrite_Set cancel_p False)) g_g)")); |
134 "Script Testterm (g_g::real) = \ |
|
135 \(((Rewrite_Set make_polynomial False) @@\ |
|
136 \ (Rewrite_Set cancel_p False)) g_g)" |
|
137 )); |
|
138 |
|
139 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) |
|
140 |
104 |
141 "-------- cancel, without detail ------------------------------"; |
105 "-------- cancel, without detail ------------------------------"; |
142 "-------- cancel, without detail ------------------------------"; |
106 "-------- cancel, without detail ------------------------------"; |
143 "-------- cancel, without detail ------------------------------"; |
107 "-------- cancel, without detail ------------------------------"; |
144 val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))", |
108 val fmz = ["realTestGiven (((3 + x) * (3 + -1*x)) / ((3 + x) * (3 + x)))", "realTestFind s"]; |
145 "realTestFind s"]; |
109 val (dI',pI',mI') = ("Test", ["detail", "test"], ["Test", "test_detail_binom"]); |
146 val (dI',pI',mI') = |
|
147 ("Test",["detail","test"],["Test","test_detail_binom"]); |
|
148 |
110 |
149 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
111 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
150 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
112 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
151 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
113 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
152 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
114 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
156 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*) |
118 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*) |
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
119 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
120 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
121 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
160 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
122 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
161 (*"(3 + -1 * x) / (3 + x)"*) |
123 (*WN130909: detail will be discontinued |
162 if nxt = ("End_Proof'",End_Proof') then () |
124 if nxt = ("End_Proof'",End_Proof') then () |
163 else error "details.sml, changed behaviour in: without detail"; |
125 else error "details.sml, changed behaviour in: without detail"; |
164 |
126 *) |
165 val str = pr_ptree pr_short pt; |
127 val str = pr_ptree pr_short pt; |
166 writeln str; |
|
167 |
|
168 |
128 |
169 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
129 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
170 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
130 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
171 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
131 "-------- cancel, detail rev-rew (cancel) afterwards ----------"; |
172 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
132 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
194 val p = ([2, 1], Res) : pos' |
154 val p = ([2, 1], Res) : pos' |
195 ######################################################################### |
155 ######################################################################### |
196 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
156 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
197 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
198 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
199 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt;src |
200 (*val nxt = ("End_Detail",End_Detail)*) |
160 (*val nxt = ("End_Detail",End_Detail)*) |
201 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
161 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
202 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*) |
162 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)src |
203 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
163 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) |
204 val nxt = ("Detail",Detail);"----------------------"; |
164 val nxt = ("Detail",Detail);"----------------------"; |
205 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e; |
165 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e; |
206 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
166 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
207 |
167 |