73 ; |
73 ; |
74 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; |
74 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str; |
75 atomty sc'; |
75 atomty sc'; |
76 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; |
76 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; |
77 (*--------------------------------------------------------------------- |
77 (*--------------------------------------------------------------------- |
78 if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1"; |
78 if sc = sc' then () else error"script.sml, doesnt find Substitute #1"; |
79 ---------------------------------------------------------------------*) |
79 ---------------------------------------------------------------------*) |
80 |
80 |
81 val fmz = ["Traegerlaenge L", |
81 val fmz = ["Traegerlaenge L", |
82 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)", |
82 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)", |
83 "Biegelinie y", |
83 "Biegelinie y", |
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
95 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
96 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
97 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
97 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
98 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
98 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
99 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
99 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
100 | _ => raise error "script.sml, doesnt find Substitute #2"; |
100 | _ => error "script.sml, doesnt find Substitute #2"; |
101 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
101 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
102 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*) |
102 (* *** generate1: not impl.for Substitute' !!!!!!!!!!(*#1#*)!!!!!!!!!!!*) |
103 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*) |
103 (* val nxt = ("Check_Postcond",.. !!!!!!!!!!!!!!!!!!!(*#2#*)!!!!!!!!!!!*) |
104 |
104 |
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
105 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
107 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
107 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
108 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
108 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
109 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
110 (*---------------------------------------------------------------------*) |
110 (*---------------------------------------------------------------------*) |
111 case nxt of (_, End_Proof') => () |
111 case nxt of (_, End_Proof') => () |
112 | _ => raise error "script.sml, doesnt find Substitute #3"; |
112 | _ => error "script.sml, doesnt find Substitute #3"; |
113 (*---------------------------------------------------------------------*) |
113 (*---------------------------------------------------------------------*) |
114 (*the reason, that next_tac didnt find the 2nd Substitute, was that |
114 (*the reason, that next_tac didnt find the 2nd Substitute, was that |
115 the Take inbetween was missing, and thus the 2nd Substitute was applied |
115 the Take inbetween was missing, and thus the 2nd Substitute was applied |
116 the last formula in ctree, and not to argument from script*) |
116 the last formula in ctree, and not to argument from script*) |
117 |
117 |
149 \ in True)" |
149 \ in True)" |
150 ; |
150 ; |
151 |
151 |
152 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; |
152 val {scr=Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; |
153 (*--------------------------------------------------------------------- |
153 (*--------------------------------------------------------------------- |
154 if sc = sc' then () else raise error"script.sml, doesnt find Substitute #1"; |
154 if sc = sc' then () else error"script.sml, doesnt find Substitute #1"; |
155 ---------------------------------------------------------------------*) |
155 ---------------------------------------------------------------------*) |
156 val fmz = ["Traegerlaenge L", |
156 val fmz = ["Traegerlaenge L", |
157 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)", |
157 "Streckenlast (- q_0 * x^^^2 / 2 + x * c + c_2)", |
158 "Biegelinie y", |
158 "Biegelinie y", |
159 "RandbedingungenBiegung [y 0 = 0, y L = 0]", |
159 "RandbedingungenBiegung [y 0 = 0, y L = 0]", |
170 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
170 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
171 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
171 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
172 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
172 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
173 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
173 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
174 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
174 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () |
175 | _ => raise error "script.sml, doesnt find Substitute #2"; |
175 | _ => error "script.sml, doesnt find Substitute #2"; |
176 trace_rewrite:=true; |
176 trace_rewrite:=true; |
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*); |
177 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*); |
178 trace_rewrite:=false; |
178 trace_rewrite:=false; |
179 (*Exception TYPE raised: |
179 (*Exception TYPE raised: |
180 Illegal type for constant "op =" :: "[real, bool] => bool" |
180 Illegal type for constant "op =" :: "[real, bool] => bool" |
193 |
193 |
194 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; |
194 val {srls,...} = get_met ["IntegrierenUndKonstanteBestimmen"]; |
195 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]"; |
195 val e1__ = str2term"nth_ 1 [M_b 0 = 0, M_b L = 0]"; |
196 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__; |
196 val e1__ = eval_listexpr_ Biegelinie.thy srls e1__; term2str e1__; |
197 if term2str e1__ = "M_b 0 = 0" then () else |
197 if term2str e1__ = "M_b 0 = 0" then () else |
198 raise error"script.sml diff.beh. eval_listexpr_ nth_ 1 [..."; |
198 error"script.sml diff.beh. eval_listexpr_ nth_ 1 [..."; |
199 |
199 |
200 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???... |
200 (*TODO.WN050913 ??? doesnt eval_listexpr_ go into subterms ???... |
201 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))"; |
201 val x1__ = str2term"argument_in (lhs (M_b 0 = 0))"; |
202 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__; |
202 val x1__ = eval_listexpr_ Biegelinie.thy srls x1__; term2str x1__; |
203 (*no rewrite*) |
203 (*no rewrite*) |
233 val appltacs = sel_appl_atomic_tacs pt p; |
233 val appltacs = sel_appl_atomic_tacs pt p; |
234 if appltacs = |
234 if appltacs = |
235 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), |
235 [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"), |
236 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), |
236 Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), |
237 Calculate "times"] then () |
237 Calculate "times"] then () |
238 else raise error "script.sml fun sel_appl_atomic_tacs diff.behav."; |
238 else error "script.sml fun sel_appl_atomic_tacs diff.behav."; |
239 |
239 |
240 trace_script := true; |
240 trace_script := true; |
241 trace_script := false; |
241 trace_script := false; |
242 applyTactic 1 p (hd appltacs); |
242 applyTactic 1 p (hd appltacs); |
243 val ((pt, p), _) = get_calc 1; show_pt pt; |
243 val ((pt, p), _) = get_calc 1; show_pt pt; |