65 "~~~~~ fun assy [1], args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = |
65 "~~~~~ fun assy [1], args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) = |
66 (((*thy',*)ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (LTool.body_of sc)); |
66 (((*thy',*)ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (LTool.body_of sc)); |
67 |
67 |
68 (*val Assoc (scrstate, steps) = in isabisacREP*) |
68 (*val Assoc (scrstate, steps) = in isabisacREP*) |
69 (*val NasApp ((E',l,a,v,S,_),ss) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e; |
69 (*val NasApp ((E',l,a,v,S,_),ss) = in isabisac*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e; |
70 "~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss:step list), (Const ("Script.Seq"(*2[1]*),_) $e1 $ e2 $ a)) = |
70 "~~~~~ fun assy, args:"; val (ya, ((E,l,_,v,S,b),ss:step list), (Const ("Program.Seq"(*2[1]*),_) $e1 $ e2 $ a)) = |
71 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e); |
71 (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e); |
72 |
72 |
73 (*val Assoc (scrstate, steps) = in isabisacREP*) |
73 (*val Assoc (scrstate, steps) = in isabisacREP*) |
74 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*) |
74 (*val NasApp ((E,_,_,v,_,_),ss) = in isabisac*) |
75 (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 (*of*); |
75 (*case*) assy ya ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss) e1 (*of*); |
76 "~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Script.Try"(*1*),_) $ e)) = |
76 "~~~~~ fun assy, args:"; val (ya, ((E,l,a,v,S,b),ss), (Const ("Program.Try"(*1*),_) $ e)) = |
77 ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1); |
77 ( ya, ((E, l @ [Celem.L, Celem.L, Celem.R], SOME a,v,S,b),ss), e1); |
78 |
78 |
79 term2str e1 = "Try (Rewrite_Set ''norm_equation'' False)" (*in isabisac*); |
79 term2str e1 = "Try (Rewrite_Set ''norm_equation'' False)" (*in isabisac*); |
80 term2str e1 = "Try (Rewrite_Set norm_equation False)" (*in isabisacREP*); |
80 term2str e1 = "Try (Rewrite_Set norm_equation False)" (*in isabisacREP*); |
81 termopt2str a = "(SOME e_e)" (*in isabisac + isabisacREP*); |
81 termopt2str a = "(SOME e_e)" (*in isabisac + isabisacREP*); |
94 |
94 |
95 (*val Ass (m,v') = in isabisacREP*) |
95 (*val Ass (m,v') = in isabisacREP*) |
96 (*val NotAss = in isabisac*) |
96 (*val NotAss = in isabisac*) |
97 (*case*) associate pt ctxt (m, stac) (*of*); |
97 (*case*) associate pt ctxt (m, stac) (*of*); |
98 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))), |
98 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))), |
99 (Const ("Script.Rewrite'_Set", _) $ rls_ $ _ $ f_)) = (pt, d, m, stac); |
99 (Const ("Program.Rewrite'_Set", _) $ rls_ $ _ $ f_)) = (pt, d, m, stac); |
100 |
100 |
101 if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Script.associate changed"; |
101 if Rule.id_rls rls = HOLogic.dest_string rls_ then () else error "Program.associate changed"; |
102 |
102 |
103 "~~~~~ continue me[1] after locatetac"; |
103 "~~~~~ continue me[1] after locatetac"; |
104 val (pt, p) = ptp'''''; |
104 val (pt, p) = ptp'''''; |
105 (* isabisac17: val ("helpless", _) = (*case*) step p ((pt, Ctree.e_pos'),[]) (*of*)*) |
105 (* isabisac17: val ("helpless", _) = (*case*) step p ((pt, Ctree.e_pos'),[]) (*of*)*) |
106 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); |
106 "~~~~~ fun step, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); |
130 |
130 |
131 if up = [R, L, R, L, L, R] then () else error "250-Rewrite_Set: nstep_up CHANGED"; |
131 if up = [R, L, R, L, L, R] then () else error "250-Rewrite_Set: nstep_up CHANGED"; |
132 (*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v ERROR go: no [L,L,R]*) |
132 (*isabisac17: nxt_up thy ptp (Celem.Prog sc) E up ay (go up sc) a v ERROR go: no [L,L,R]*) |
133 (*isabisac17: (go up sc) ERROR go: no [L,L,R]*) |
133 (*isabisac17: (go up sc) ERROR go: no [L,L,R]*) |
134 (*isabisac15:*) |
134 (*isabisac15:*) |
135 val ttt as Const ("Script.Try", _) $ (Const ("Script.Rewrite'_Set", _) $ rls $ |
135 val ttt as Const ("Program.Try", _) $ (Const ("Program.Rewrite'_Set", _) $ rls $ |
136 Const ("HOL.False", _)) = (go up sc) |
136 Const ("HOL.False", _)) = (go up sc) |
137 val (Const ("Script.Try"(*2*), _) $ _) = ttt; |
137 val (Const ("Program.Try"(*2*), _) $ _) = ttt; |
138 if term2str ttt = "Try (Rewrite_Set ''norm_equation'' False)" |
138 if term2str ttt = "Try (Rewrite_Set ''norm_equation'' False)" |
139 then () else error "250-Rewrite_Set: (go up sc) CHANGED"; |
139 then () else error "250-Rewrite_Set: (go up sc) CHANGED"; |
140 |
140 |
141 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*2*), _) $ _), a, v) = |
141 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Program.Try"(*2*), _) $ _), a, v) = |
142 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v ); |
142 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v ); |
143 |
143 |
144 (*\\--1 end step into relevant call ----------------------------------------------------------//*) |
144 (*\\--1 end step into relevant call ----------------------------------------------------------//*) |
145 |
145 |
146 (* nxt'''_' = Rewrite_Set "Test_simplify" |
146 (* nxt'''_' = Rewrite_Set "Test_simplify" |
188 = (thy, ptp, sc, E, l, Skip_, a, v); |
188 = (thy, ptp, sc, E, l, Skip_, a, v); |
189 (*if*) 1 < length l (*then*); |
189 (*if*) 1 < length l (*then*); |
190 val up = drop_last l; |
190 val up = drop_last l; |
191 |
191 |
192 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v; |
192 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v; |
193 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*1*),_) $ _ ), a, v) |
193 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Program.Try"(*1*),_) $ _ ), a, v) |
194 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v); |
194 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v); |
195 |
195 |
196 nstep_up thy ptp scr E l Skip_ a v; |
196 nstep_up thy ptp scr E l Skip_ a v; |
197 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) |
197 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) |
198 = (thy, ptp, scr, E, l, Skip_, a, v); |
198 = (thy, ptp, scr, E, l, Skip_, a, v); |
199 (*if*) 1 < length l (*then*); |
199 (*if*) 1 < length l (*then*); |
200 val up = drop_last l; |
200 val up = drop_last l; |
201 |
201 |
202 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v; |
202 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v; |
203 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq"(*2*), _) $ _ $ _), a, v) |
203 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Program.Seq"(*2*), _) $ _ $ _), a, v) |
204 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v); |
204 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v); |
205 |
205 |
206 nstep_up thy ptp scr E l ay a v; |
206 nstep_up thy ptp scr E l ay a v; |
207 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) |
207 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) |
208 = (thy, ptp, scr, E, l, ay, a, v); |
208 = (thy, ptp, scr, E, l, ay, a, v); |
209 (*if*) 1 < length l (*then*); |
209 (*if*) 1 < length l (*then*); |
210 val up = drop_last l; |
210 val up = drop_last l; |
211 |
211 |
212 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v; |
212 nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v; |
213 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq"(*1*), _) $ _ $ _ $ _), a, v) |
213 "~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Program.Seq"(*1*), _) $ _ $ _ $ _), a, v) |
214 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v); |
214 = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v); |
215 |
215 |
216 nstep_up thy ptp scr E l ay a v; |
216 nstep_up thy ptp scr E l ay a v; |
217 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) |
217 "~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) |
218 = (thy, ptp, scr, E, l, ay, a, v); |
218 = (thy, ptp, scr, E, l, ay, a, v); |
239 "~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) |
239 "~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) |
240 = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v); |
240 = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v); |
241 val (a', LTool.STac stac) = (*case*) Lucin.handle_leaf "next " th sr E a v t (*of*); |
241 val (a', LTool.STac stac) = (*case*) Lucin.handle_leaf "next " th sr E a v t (*of*); |
242 |
242 |
243 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac; |
243 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac; |
244 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Script.SubProblem", _) $ spec' $ ags')) |
244 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Program.SubProblem", _) $ spec' $ ags')) |
245 = (pt, (Celem.assoc_thy th), stac); |
245 = (pt, (Celem.assoc_thy th), stac); |
246 val (dI, pI, mI) = LTool.dest_spec spec' |
246 val (dI, pI, mI) = LTool.dest_spec spec' |
247 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt); |
247 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt); |
248 val ags = TermC.isalist2list ags'; |
248 val ags = TermC.isalist2list ags'; |
249 (*if*) mI = ["no_met"] (*else*); |
249 (*if*) mI = ["no_met"] (*else*); |