156 > get [] (eq_str "True") sss; [R,L,R,R,L,R] |
156 > get [] (eq_str "True") sss; [R,L,R,R,L,R] |
157 > get [] (eq_str "e_") sss; [R,R] |
157 > get [] (eq_str "e_") sss; [R,R] |
158 *) |
158 *) |
159 |
159 |
160 fun test_negotiable t = |
160 fun test_negotiable t = |
161 member op = ((strip_thy o (term_str Script.thy) o head_of) t) (!negotiable); |
161 member op = (!negotiable) ((strip_thy o (term_str Script.thy) o head_of) t); |
162 |
162 |
163 (*.get argument of first stactic in a script for init_form.*) |
163 (*.get argument of first stactic in a script for init_form.*) |
164 fun get_stac thy (h $ body) = |
164 fun get_stac thy (h $ body) = |
165 (* |
165 (* |
166 *) |
166 *) |
323 !: FIXXXME penv: push it here in itms2args into script-evaluation*) |
323 !: FIXXXME penv: push it here in itms2args into script-evaluation*) |
324 (* val (thy, mI, itms) = (thy, metID, itms); |
324 (* val (thy, mI, itms) = (thy, metID, itms); |
325 *) |
325 *) |
326 fun itms2args thy mI (itms:itm list) = |
326 fun itms2args thy mI (itms:itm list) = |
327 let val mvat = max_vt itms |
327 let val mvat = max_vt itms |
328 fun okv mvat (_,vats,b,_,_) = member op = mvat vats andalso b |
328 fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b |
329 val itms = filter (okv mvat) itms |
329 val itms = filter (okv mvat) itms |
330 fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_) |
330 fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_) |
331 fun itm2arg itms (_,(d,_)) = |
331 fun itm2arg itms (_,(d,_)) = |
332 case find_first (test_dsc d) itms of |
332 case find_first (test_dsc d) itms of |
333 NONE => |
333 NONE => |
507 > val s = ((term_of o the o (parse thy)) "x", |
507 > val s = ((term_of o the o (parse thy)) "x", |
508 (term_of o the o (parse thy)) "-#5//#12"); |
508 (term_of o the o (parse thy)) "-#5//#12"); |
509 > val asm = (term_of o the o (parse thy)) |
509 > val asm = (term_of o the o (parse thy)) |
510 "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)"; |
510 "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)"; |
511 > val pred = subst_atomic [s] asm; |
511 > val pred = subst_atomic [s] asm; |
512 > rewrite_set_ thy false (cterm_of (sign_of thy) pred); |
512 > rewrite_set_ thy false ((Thm.cterm thy) pred); |
513 val it = NONE : (cterm * cterm list) option !!!!!!!!!!!!!!!!!!!!!!!!!!!! |
513 val it = NONE : (cterm * cterm list) option !!!!!!!!!!!!!!!!!!!!!!!!!!!! |
514 > eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred); |
514 > eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred); |
515 val it = false : bool |
515 val it = false : bool |
516 |
516 |
517 > val s = ((term_of o the o (parse thy)) "x", |
517 > val s = ((term_of o the o (parse thy)) "x", |
518 (term_of o the o (parse thy)) "#4"); |
518 (term_of o the o (parse thy)) "#4"); |
519 > val asm = (term_of o the o (parse thy)) |
519 > val asm = (term_of o the o (parse thy)) |
520 "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#5 + x)"; |
520 "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#5 + x)"; |
521 > val pred = subst_atomic [s] asm; |
521 > val pred = subst_atomic [s] asm; |
522 > rewrite_set_ thy false (cterm_of (sign_of thy) pred); |
522 > rewrite_set_ thy false ((Thm.cterm thy) pred); |
523 val it = SOME ("True & True",[]) : (cterm * cterm list) option |
523 val it = SOME ("True & True",[]) : (cterm * cterm list) option |
524 > eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred); |
524 > eval_true' (string_of_thy thy) "eval_rls" (subst_atomic [s] pred); |
525 val it = true : bool`*) |
525 val it = true : bool`*) |
526 |
526 |
527 (*for check_elementwise: take apart the set, ev. instantiate assumptions |
527 (*for check_elementwise: take apart the set, ev. instantiate assumptions |
804 *) |
804 *) |
805 (* 13.3.01 |
805 (* 13.3.01 |
806 v |
806 v |
807 *) |
807 *) |
808 fun make_rule thy t = |
808 fun make_rule thy t = |
809 let val ct = cterm_of (sign_of thy) (Trueprop $ t) |
809 let val ct = (Thm.cterm thy) (Trueprop $ t) |
810 in Thm (string_of_cterm ct, make_thm ct) end; |
810 in Thm (string_of_cterm ct, make_thm ct) end; |
811 |
811 |
812 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m; |
812 (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m; |
813 *) |
813 *) |
814 (*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete! |
814 (*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete! |
1916 (*2*) from PblObj/PrfObj: if stac is in the middle of the script |
1916 (*2*) from PblObj/PrfObj: if stac is in the middle of the script |
1917 (*3*) from rls/PrfObj: in case of detail a ruleset.*) |
1917 (*3*) from rls/PrfObj: in case of detail a ruleset.*) |
1918 (* val (thy', (p,p_), pt) = (thy', (p,p_), pt); |
1918 (* val (thy', (p,p_), pt) = (thy', (p,p_), pt); |
1919 *) |
1919 *) |
1920 fun from_pblobj_or_detail' thy' (p,p_) pt = |
1920 fun from_pblobj_or_detail' thy' (p,p_) pt = |
1921 if member op = p_ [Pbl,Met] |
1921 if member op = [Pbl,Met] p_ |
1922 then case get_obj g_env pt p of |
1922 then case get_obj g_env pt p of |
1923 NONE => raise error "from_pblobj_or_detail': no istate" |
1923 NONE => raise error "from_pblobj_or_detail': no istate" |
1924 | SOME is => |
1924 | SOME is => |
1925 let val metID = get_obj g_metID pt p |
1925 let val metID = get_obj g_metID pt p |
1926 val {srls,...} = get_met metID |
1926 val {srls,...} = get_met metID |