1.1 --- a/src/Tools/isac/ME/appl.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,782 +0,0 @@
1.4 -(* use"ME/appl.sml";
1.5 - use"appl.sml";
1.6 -
1.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.8 - 10 20 30 40 50 60 70 80
1.9 -*)
1.10 -val e_cterm' = empty_cterm';
1.11 -
1.12 -
1.13 -fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
1.14 - (rew_ord':rew_ord',erls,ca)
1.15 - | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
1.16 - (rew_ord',erls,ca)
1.17 - | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =
1.18 - (rew_ord',erls, ca)
1.19 - | rew_info rls = raise error ("rew_info called with '"^rls2str rls^"'");
1.20 -
1.21 -(*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
1.22 -fun from_pblobj_or_detail_thm thm' p pt =
1.23 - let val (pbl,p',rls') = par_pbl_det pt p
1.24 - in if pbl
1.25 - then let (*val _= writeln("### from_pblobj_or_detail_thm: pbl=true")*)
1.26 - val thy' = get_obj g_domID pt p'
1.27 - val {rew_ord',erls,(*asm_thm,*)...} =
1.28 - get_met (get_obj g_metID pt p')
1.29 - (*val _= writeln("### from_pblobj_or_detail_thm: metID= "^
1.30 - (metID2str(get_obj g_metID pt p')))
1.31 - val _= writeln("### from_pblobj_or_detail_thm: erls= "^erls)*)
1.32 - in ("OK",thy',rew_ord',erls,(*put_asm*)false)
1.33 - end
1.34 - else ((*writeln("### from_pblobj_or_detail_thm: pbl=false");*)
1.35 - (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!!
1.36 - NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)
1.37 - | SOME rls =>*)
1.38 - let val thy' = get_obj g_domID pt (par_pblobj pt p)
1.39 - val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'
1.40 - in ("OK",thy',rew_ord',erls,false) end)
1.41 - end;
1.42 -(*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
1.43 -fun from_pblobj_or_detail_calc scrop p pt =
1.44 -(* val (scrop, p, pt) = (op_, p, pt);
1.45 - *)
1.46 - let val (pbl,p',rls') = par_pbl_det pt p
1.47 - in if pbl
1.48 - then let val thy' = get_obj g_domID pt p'
1.49 - val {calc = scr_isa_fns,...} =
1.50 - get_met (get_obj g_metID pt p')
1.51 - val opt = assoc (scr_isa_fns, scrop)
1.52 - in case opt of
1.53 - SOME isa_fn => ("OK",thy',isa_fn)
1.54 - | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
1.55 - "",("",e_evalfn)) end
1.56 - else (*case assoc(!ruleset', rls') of
1.57 - NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))
1.58 - | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)
1.59 - (* val SOME rls = assoc(!ruleset', rls');
1.60 - *)
1.61 - let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.62 - val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
1.63 - in case assoc (scr_isa_fns, scrop) of
1.64 - SOME isa_fn => ("OK",thy',isa_fn)
1.65 - | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",
1.66 - "",("",e_evalfn)) end
1.67 - end;
1.68 -(*------------------------------------------------------------------*)
1.69 -
1.70 -val op_and = Const ("op &", [bool, bool] ---> bool);
1.71 -(*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));
1.72 -val it = "a & b" : cterm
1.73 -*)
1.74 -fun mk_and a b = op_and $ a $ b;
1.75 -(*> (cterm_of thy)
1.76 - (mk_and (Free("a",bool)) (Free("b",bool)));
1.77 -val it = "a & b" : cterm*)
1.78 -
1.79 -fun mk_and [] = HOLogic.true_const
1.80 - | mk_and (t::[]) = t
1.81 - | mk_and (t::ts) =
1.82 - let fun mk t' (t::[]) = op_and $ t' $ t
1.83 - | mk t' (t::ts) = mk (op_and $ t' $ t) ts
1.84 - in mk t ts end;
1.85 -(*> val pred = map (term_of o the o (parse thy))
1.86 - ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];
1.87 -> (cterm_of thy) (mk_and pred);
1.88 -val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)
1.89 -
1.90 -
1.91 -
1.92 -
1.93 -(*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
1.94 -fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, [])
1.95 -
1.96 - | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =
1.97 - (e_term, if pred <> Const ("Script.Assumptions",bool)
1.98 - then [pred]
1.99 - else (map fst) (get_assumptions_ pt (p,Res)))
1.100 -
1.101 -(* val pred = (term_of o the o (parse thy)) pred;
1.102 - val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;
1.103 - mk_set thy pt p consts pred;
1.104 - *)
1.105 - | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred =
1.106 - let val (bdv,_) = HOLogic.dest_eq eq;
1.107 - val pred = if pred <> Const ("Script.Assumptions",bool)
1.108 - then [pred]
1.109 - else (map fst) (get_assumptions_ pt (p,Res))
1.110 - in (bdv, pred) end
1.111 -
1.112 - | mk_set thy _ _ l _ =
1.113 - raise error ("check_elementwise: no set "^
1.114 - (Syntax.string_of_term (thy2ctxt thy) l));
1.115 -(*> val consts = str2term "[x=#4]";
1.116 -> val pred = str2term "Assumptions";
1.117 -> val pt = union_asm pt p
1.118 - [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),
1.119 - ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
1.120 -> val p = [];
1.121 -> val (sss,ttt) = mk_set thy pt p consts pred;
1.122 -> (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt);
1.123 -val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
1.124 -
1.125 - val consts = str2term "UniversalList";
1.126 - val pred = str2term "Assumptions";
1.127 -
1.128 -*)
1.129 -
1.130 -
1.131 -
1.132 -(*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)
1.133 -(* val (erls,consts,(bdv,pred)) = (erl,ft,vp);
1.134 - val (consts,(bdv,pred)) = (ft,vp);
1.135 - *)
1.136 -fun check_elementwise thy erls all_results (bdv, asm) =
1.137 - let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)
1.138 - fun check sub =
1.139 - let val inst_ = map (subst_atomic [sub]) asm
1.140 - in case eval__true thy 1 inst_ [] erls of
1.141 - (asm', true) => ([HOLogic.mk_eq sub], asm')
1.142 - | (_, false) => ([],[])
1.143 - end;
1.144 - (*val _= writeln("### check_elementwise: res= "^(term2str all_results)^
1.145 - ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)
1.146 - val c' = isalist2list all_results
1.147 - val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)
1.148 - val subs = map (pair bdv) c''
1.149 - in if asm = [] then (all_results, [])
1.150 - else ((apfst ((list2isalist bool) o flat)) o
1.151 - (apsnd flat) o split_list o (map check)) subs end;
1.152 -(* 20.5.03
1.153 -> val all_results = str2term "[x=a+b,x=b,x=3]";
1.154 -> val bdv = str2term "x";
1.155 -> val asm = str2term "(x ~= a) & (x ~= b)";
1.156 -> val erls = e_rls;
1.157 -> val (t, ts) = check_elementwise thy erls all_results (bdv, asm);
1.158 -> term2str t; writeln(terms2str ts);
1.159 -val it = "[x = a + b, x = b, x = c]" : string
1.160 -["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]
1.161 -... with appropriate erls this should be:
1.162 -val it = "[x = a + b, x = c]" : string
1.163 -["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"]
1.164 - ////// because b ~= b False*)
1.165 -
1.166 -
1.167 -
1.168 -(*before 5.03-----
1.169 -> val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
1.170 - \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
1.171 -> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
1.172 -val ct' = "True" : cterm'
1.173 -
1.174 -> val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
1.175 - \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
1.176 -> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
1.177 -val ct' = "True" : cterm'
1.178 -
1.179 -
1.180 -> val const = (term_of o the o (parse thy)) "(#3::real)";
1.181 -> val pred' = subst_atomic [(bdv,const)] pred;
1.182 -
1.183 -
1.184 -> val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";
1.185 -> val bdv = (term_of o the o (parse thy)) "(x::real)";
1.186 -> val pred = (term_of o the o (parse thy))
1.187 - "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";
1.188 -> val ttt = check_elementwise thy consts (bdv, pred);
1.189 -> (cterm_of thy) ttt;
1.190 -val it = "[x = #-3, x = #3]" : cterm
1.191 -
1.192 -> val consts = (term_of o the o (parse thy)) "[x = #4]";
1.193 -> val bdv = (term_of o the o (parse thy)) "(x::real)";
1.194 -> val pred = (term_of o the o (parse thy))
1.195 - "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";
1.196 -> val ttt = check_elementwise thy consts (bdv,pred);
1.197 -> (cterm_of thy) ttt;
1.198 -val it = "[x = #4]" : cterm
1.199 -
1.200 -> val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";
1.201 -> val bdv = (term_of o the o (parse thy)) "(x::real)";
1.202 -> val pred = (term_of o the o (parse thy))
1.203 - " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";
1.204 -> val ttt = check_elementwise thy consts (bdv,pred);
1.205 -> (cterm_of thy) ttt;
1.206 -val it = "[]" : cterm*)
1.207 -
1.208 -
1.209 -(* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)
1.210 -fun split_dummy str =
1.211 -let fun scan s' [] = (implode s', "")
1.212 - | scan s' (s::ss) = if s=" " then (implode s', implode ss)
1.213 - else scan (s'@[s]) ss;
1.214 -in ((scan []) o explode) str end;
1.215 -(* split_dummy "subproblem_equation_dummy (x=-#5//#12)";
1.216 -val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string
1.217 -> split_dummy "x=-#5//#12";
1.218 -val it = ("x=-#5//#12","") : string * string*)
1.219 -
1.220 -
1.221 -
1.222 -
1.223 -(*.applicability of a tacic wrt. a calc-state (ptree,pos').
1.224 - additionally used by next_tac in the script-interpreter for sequence-tacs.
1.225 - tests for applicability are so expensive, that results (rewrites!)
1.226 - are kept in the return-value of 'type tac_'.
1.227 -.*)
1.228 -fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
1.229 - Appl (Init_Proof' (ct', spec))
1.230 -
1.231 - | applicable_in (p,p_) pt Model_Problem =
1.232 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.233 - then Notappl ((tac2str Model_Problem)^
1.234 - " not for pos "^(pos'2str (p,p_)))
1.235 - else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
1.236 - val {ppc,...} = get_pbt pI'
1.237 - val pbl = init_pbl ppc
1.238 - in Appl (Model_Problem' (pI', pbl, [])) end
1.239 -(* val Refine_Tacitly pI = m;
1.240 - *)
1.241 - | applicable_in (p,p_) pt (Refine_Tacitly pI) =
1.242 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.243 - then Notappl ((tac2str (Refine_Tacitly pI))^
1.244 - " not for pos "^(pos'2str (p,p_)))
1.245 - else (* val Refine_Tacitly pI = m;
1.246 - *)
1.247 - let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
1.248 - val opt = refine_ori oris pI;
1.249 - in case opt of
1.250 - SOME pblID =>
1.251 - Appl (Refine_Tacitly' (pI, pblID,
1.252 - e_domID, e_metID, [](*filled in specify*)))
1.253 - | NONE => Notappl ((tac2str (Refine_Tacitly pI))^
1.254 - " not applicable") end
1.255 -(* val (p,p_) = ip;
1.256 - val Refine_Problem pI = m;
1.257 - *)
1.258 - | applicable_in (p,p_) pt (Refine_Problem pI) =
1.259 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.260 - then Notappl ((tac2str (Refine_Problem pI))^
1.261 - " not for pos "^(pos'2str (p,p_)))
1.262 - else
1.263 - let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),
1.264 - probl=itms, ...}) = get_obj I pt p;
1.265 - val thy = if dI' = e_domID then dI else dI';
1.266 - val rfopt = refine_pbl (assoc_thy thy) pI itms;
1.267 - in case rfopt of
1.268 - NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.269 - | SOME (rf as (pI',_)) =>
1.270 -(* val SOME (rf as (pI',_)) = rfopt;
1.271 - *)
1.272 - if pI' = pI
1.273 - then Notappl ((tac2str (Refine_Problem pI))^" not applicable")
1.274 - else Appl (Refine_Problem' rf)
1.275 - end
1.276 -
1.277 - (*the specify-tacs have cterm' instead term:
1.278 - parse+error here!!!: see appl_add*)
1.279 - | applicable_in (p,p_) pt (Add_Given ct') =
1.280 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.281 - then Notappl ((tac2str (Add_Given ct'))^
1.282 - " not for pos "^(pos'2str (p,p_)))
1.283 - else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))
1.284 - (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
1.285 -
1.286 - | applicable_in (p,p_) pt (Del_Given ct') =
1.287 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.288 - then Notappl ((tac2str (Del_Given ct'))^
1.289 - " not for pos "^(pos'2str (p,p_)))
1.290 - else Appl (Del_Given' ct')
1.291 -
1.292 - | applicable_in (p,p_) pt (Add_Find ct') =
1.293 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.294 - then Notappl ((tac2str (Add_Find ct'))^
1.295 - " not for pos "^(pos'2str (p,p_)))
1.296 - else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))
1.297 -
1.298 - | applicable_in (p,p_) pt (Del_Find ct') =
1.299 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.300 - then Notappl ((tac2str (Del_Find ct'))^
1.301 - " not for pos "^(pos'2str (p,p_)))
1.302 - else Appl (Del_Find' ct')
1.303 -
1.304 - | applicable_in (p,p_) pt (Add_Relation ct') =
1.305 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.306 - then Notappl ((tac2str (Add_Relation ct'))^
1.307 - " not for pos "^(pos'2str (p,p_)))
1.308 - else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))
1.309 -
1.310 - | applicable_in (p,p_) pt (Del_Relation ct') =
1.311 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.312 - then Notappl ((tac2str (Del_Relation ct'))^
1.313 - " not for pos "^(pos'2str (p,p_)))
1.314 - else Appl (Del_Relation' ct')
1.315 -
1.316 - | applicable_in (p,p_) pt (Specify_Theory dI) =
1.317 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.318 - then Notappl ((tac2str (Specify_Theory dI))^
1.319 - " not for pos "^(pos'2str (p,p_)))
1.320 - else Appl (Specify_Theory' dI)
1.321 -(* val (p,p_) = p; val Specify_Problem pID = m;
1.322 - val Specify_Problem pID = m;
1.323 - *)
1.324 - | applicable_in (p,p_) pt (Specify_Problem pID) =
1.325 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.326 - then Notappl ((tac2str (Specify_Problem pID))^
1.327 - " not for pos "^(pos'2str (p,p_)))
1.328 - else
1.329 - let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),
1.330 - probl=itms, ...}) = get_obj I pt p;
1.331 - val thy = assoc_thy (if dI' = e_domID then dI else dI');
1.332 - val {ppc,where_,prls,...} = get_pbt pID;
1.333 - val pbl = if pI'=e_pblID andalso pI=e_pblID
1.334 - then (false, (init_pbl ppc, []))
1.335 - else match_itms_oris thy itms (ppc,where_,prls) oris;
1.336 - in Appl (Specify_Problem' (pID, pbl)) end
1.337 -(* val Specify_Method mID = nxt; val (p,p_) = p;
1.338 - *)
1.339 - | applicable_in (p,p_) pt (Specify_Method mID) =
1.340 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.341 - then Notappl ((tac2str (Specify_Method mID))^
1.342 - " not for pos "^(pos'2str (p,p_)))
1.343 - else Appl (Specify_Method' (mID,[(*filled in specify*)],
1.344 - [(*filled in specify*)]))
1.345 -
1.346 - | applicable_in (p,p_) pt (Apply_Method mI) =
1.347 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.348 - then Notappl ((tac2str (Apply_Method mI))^
1.349 - " not for pos "^(pos'2str (p,p_)))
1.350 - else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*)))
1.351 -
1.352 - | applicable_in (p,p_) pt (Check_Postcond pI) =
1.353 - if member op = [Pbl,Met] p_
1.354 - then Notappl ((tac2str (Check_Postcond pI))^
1.355 - " not for pos "^(pos'2str (p,p_)))
1.356 - else Appl (Check_Postcond'
1.357 - (pI,(e_term,[(*asm in solve*)])))
1.358 - (* in solve -"- ^^^^^^ gets returnvalue of scr*)
1.359 -
1.360 - (*these are always applicable*)
1.361 - | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
1.362 - | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
1.363 -
1.364 -(* val m as Rewrite_Inst (subs, thm') = m;
1.365 - *)
1.366 - | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
1.367 - if member op = [Pbl,Met] p_
1.368 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.369 - else
1.370 - let
1.371 - val pp = par_pblobj pt p;
1.372 - val thy' = (get_obj g_domID pt pp):theory';
1.373 - val thy = assoc_thy thy';
1.374 - val {rew_ord'=ro',erls=erls,...} =
1.375 - get_met (get_obj g_metID pt pp);
1.376 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.377 - Frm => (get_obj g_form pt p, p)
1.378 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.379 - | _ => raise error ("applicable_in: call by "^
1.380 - (pos'2str (p,p_)));
1.381 - in
1.382 - let val subst = subs2subst thy subs;
1.383 - val subs' = subst2subs' subst;
1.384 - in case rewrite_inst_ thy (assoc_rew_ord ro') erls
1.385 - (*put_asm*)false subst (assoc_thm' thy thm') f of
1.386 - SOME (f',asm) => Appl (
1.387 - Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',
1.388 - (*term_of o the o (parse (assoc_thy thy'))*) f,
1.389 - (*(term_of o the o (parse (assoc_thy thy'))*) (f',
1.390 - (*map (term_of o the o (parse (assoc_thy thy')))*) asm)))
1.391 - | NONE => Notappl ((fst thm')^" not applicable") end
1.392 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
1.393 -
1.394 -(* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);
1.395 - val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
1.396 - *)
1.397 -| applicable_in (p,p_) pt (m as Rewrite thm') =
1.398 - if member op = [Pbl,Met] p_
1.399 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.400 - else
1.401 - let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;
1.402 - val thy = assoc_thy thy';
1.403 - val f = case p_ of
1.404 - Frm => get_obj g_form pt p
1.405 - | Res => (fst o (get_obj g_result pt)) p
1.406 - | _ => raise error ("applicable_in Rewrite: call by "^
1.407 - (pos'2str (p,p_)));
1.408 - in if msg = "OK"
1.409 - then
1.410 - ((*writeln("### applicable_in rls'= "^rls');*)
1.411 - (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;
1.412 - *)
1.413 - case rewrite_ thy (assoc_rew_ord ro)
1.414 - rls' false (assoc_thm' thy thm') f of
1.415 - SOME (f',asm) => Appl (
1.416 - Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))
1.417 - | NONE => Notappl ("'"^(fst thm')^"' not applicable") )
1.418 - else Notappl msg
1.419 - end
1.420 -
1.421 -| applicable_in (p,p_) pt (m as Rewrite_Asm thm') =
1.422 - if member op = [Pbl,Met] p_
1.423 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.424 - else
1.425 - let
1.426 - val pp = par_pblobj pt p;
1.427 - val thy' = (get_obj g_domID pt pp):theory';
1.428 - val thy = assoc_thy thy';
1.429 - val {rew_ord'=ro',erls=erls,...} =
1.430 - get_met (get_obj g_metID pt pp);
1.431 - (*val put_asm = true;*)
1.432 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.433 - Frm => (get_obj g_form pt p, p)
1.434 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.435 - | _ => raise error ("applicable_in: call by "^
1.436 - (pos'2str (p,p_)));
1.437 - in case rewrite_ thy (assoc_rew_ord ro') erls
1.438 - (*put_asm*)false (assoc_thm' thy thm') f of
1.439 - SOME (f',asm) => Appl (
1.440 - Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))
1.441 - | NONE => Notappl ("'"^(fst thm')^"' not applicable") end
1.442 -
1.443 - | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) =
1.444 - if member op = [Pbl,Met] p_
1.445 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.446 - else
1.447 - let
1.448 - val pp = par_pblobj pt p;
1.449 - val thy' = (get_obj g_domID pt pp):theory';
1.450 - val thy = assoc_thy thy';
1.451 - val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);
1.452 - val f = case p_ of Frm => get_obj g_form pt p
1.453 - | Res => (fst o (get_obj g_result pt)) p
1.454 - | _ => raise error ("applicable_in: call by "^
1.455 - (pos'2str (p,p_)));
1.456 - in
1.457 - let val subst = subs2subst thy subs
1.458 - val subs' = subst2subs' subst
1.459 - in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of
1.460 - SOME (f',asm) => Appl (
1.461 - Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))
1.462 - | NONE => Notappl (rls^" not applicable") end
1.463 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
1.464 -
1.465 - | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) =
1.466 - if member op = [Pbl,Met] p_
1.467 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.468 - else
1.469 - let
1.470 - val pp = par_pblobj pt p;
1.471 - val thy' = (get_obj g_domID pt pp):theory';
1.472 - val thy = assoc_thy thy';
1.473 - val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} =
1.474 - get_met (get_obj g_metID pt pp);
1.475 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.476 - Frm => (get_obj g_form pt p, p)
1.477 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.478 - | _ => raise error ("applicable_in: call by "^
1.479 - (pos'2str (p,p_)));
1.480 - in
1.481 - let val subst = subs2subst thy subs;
1.482 - val subs' = subst2subs' subst;
1.483 - in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
1.484 - SOME (f',asm) => Appl (
1.485 - Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))
1.486 - | NONE => Notappl (rls^" not applicable") end
1.487 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
1.488 -
1.489 - | applicable_in (p,p_) pt (m as Rewrite_Set rls) =
1.490 - if member op = [Pbl,Met] p_
1.491 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.492 - else
1.493 - let
1.494 - val pp = par_pblobj pt p;
1.495 - val thy' = (get_obj g_domID pt pp):theory';
1.496 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.497 - Frm => (get_obj g_form pt p, p)
1.498 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.499 - | _ => raise error ("applicable_in: call by "^
1.500 - (pos'2str (p,p_)));
1.501 - in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.502 - SOME (f',asm) =>
1.503 - ((*writeln("#.# applicable_in Rewrite_Set,2f'= "^f');*)
1.504 - Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))
1.505 - )
1.506 - | NONE => Notappl (rls^" not applicable") end
1.507 -
1.508 - | applicable_in (p,p_) pt (m as Detail_Set rls) =
1.509 - if member op = [Pbl,Met] p_
1.510 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.511 - else
1.512 - let val pp = par_pblobj pt p
1.513 - val thy' = (get_obj g_domID pt pp):theory'
1.514 - val f = case p_ of
1.515 - Frm => get_obj g_form pt p
1.516 - | Res => (fst o (get_obj g_result pt)) p
1.517 - | _ => raise error ("applicable_in: call by "^
1.518 - (pos'2str (p,p_)));
1.519 - in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of
1.520 - SOME (f',asm) =>
1.521 - Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))
1.522 - | NONE => Notappl (rls^" not applicable") end
1.523 -
1.524 -
1.525 - | applicable_in p pt (End_Ruleset) =
1.526 - raise error ("applicable_in: not impl. for "^
1.527 - (tac2str End_Ruleset))
1.528 -
1.529 -(* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);
1.530 - *)
1.531 -| applicable_in (p,p_) pt (m as Calculate op_) =
1.532 - if member op = [Pbl,Met] p_
1.533 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.534 - else
1.535 - let
1.536 - val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
1.537 - val f = case p_ of
1.538 - Frm => get_obj g_form pt p
1.539 - | Res => (fst o (get_obj g_result pt)) p
1.540 - in if msg = "OK" then
1.541 - case calculate_ (assoc_thy thy') isa_fn f of
1.542 - SOME (f', (id, thm)) =>
1.543 - Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))
1.544 - | NONE => Notappl ("'calculate "^op_^"' not applicable")
1.545 - else Notappl msg
1.546 - end
1.547 -
1.548 -(*Substitute combines two different kind of "substitution":
1.549 - (1) subst_atomic: for ?a..?z
1.550 - (2) Pattern.match: for solving equational systems
1.551 - (which raises exn for ?a..?z)*)
1.552 - | applicable_in (p,p_) pt (m as Substitute sube) =
1.553 - if member op = [Pbl,Met] p_
1.554 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.555 - else let val pp = par_pblobj pt p
1.556 - val thy = assoc_thy (get_obj g_domID pt pp)
1.557 - val f = case p_ of
1.558 - Frm => get_obj g_form pt p
1.559 - | Res => (fst o (get_obj g_result pt)) p
1.560 - val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
1.561 - val subte = sube2subte sube
1.562 - val subst = sube2subst thy sube
1.563 - in if foldl and_ (true, map contains_Var subte)
1.564 - (*1*)
1.565 - then let val f' = subst_atomic subst f
1.566 - in if f = f' then Notappl (sube2str sube^" not applicable")
1.567 - else Appl (Substitute' (subte, f, f'))
1.568 - end
1.569 - (*2*)
1.570 - else case rewrite_terms_ thy (assoc_rew_ord rew_ord')
1.571 - erls subte f of
1.572 - SOME (f', _) => Appl (Substitute' (subte, f, f'))
1.573 - | NONE => Notappl (sube2str sube^" not applicable")
1.574 - end
1.575 -(*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
1.576 - | applicable_in (p,p_) pt (m as Substitute sube) =
1.577 - if member op = [Pbl,Met] p_
1.578 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.579 - else let val pp = par_pblobj pt p
1.580 - val thy = assoc_thy (get_obj g_domID pt pp)
1.581 - val f = case p_ of
1.582 - Frm => get_obj g_form pt p
1.583 - | Res => (fst o (get_obj g_result pt)) p
1.584 - val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
1.585 - val subte = sube2subte sube
1.586 - in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of
1.587 - SOME (f', _) => Appl (Substitute' (subte, f, f'))
1.588 - | NONE => Notappl (sube2str sube^" not applicable")
1.589 - end
1.590 -------------------*)
1.591 -
1.592 - | applicable_in p pt (Apply_Assumption cts') =
1.593 - (raise error ("applicable_in: not impl. for "^
1.594 - (tac2str (Apply_Assumption cts'))))
1.595 -
1.596 - (*'logical' applicability wrt. script in locate: Inconsistent?*)
1.597 - | applicable_in (p,p_) pt (m as Take ct') =
1.598 - if member op = [Pbl,Met] p_
1.599 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.600 - else
1.601 - let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.602 - in (case parse (assoc_thy thy') ct' of
1.603 - SOME ct => Appl (Take' (term_of ct))
1.604 - | NONE => Notappl ("syntax error in "^ct'))
1.605 - end
1.606 -
1.607 - | applicable_in p pt (Take_Inst ct') =
1.608 - raise error ("applicable_in: not impl. for "^
1.609 - (tac2str (Take_Inst ct')))
1.610 -
1.611 - | applicable_in p pt (Group (con, ints)) =
1.612 - raise error ("applicable_in: not impl. for "^
1.613 - (tac2str (Group (con, ints))))
1.614 -
1.615 - | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) =
1.616 - if member op = [Pbl,Met] p_
1.617 - then (*maybe Apply_Method has already been done*)
1.618 - case get_obj g_env pt p of
1.619 - SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [],
1.620 - e_term, [], subpbl domID pblID))
1.621 - | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.622 - else (*somewhere later in the script*)
1.623 - Appl (Subproblem' ((domID, pblID, e_metID), [],
1.624 - e_term, [], subpbl domID pblID))
1.625 -
1.626 - | applicable_in p pt (End_Subproblem) =
1.627 - raise error ("applicable_in: not impl. for "^
1.628 - (tac2str (End_Subproblem)))
1.629 -
1.630 - | applicable_in p pt (CAScmd ct') =
1.631 - raise error ("applicable_in: not impl. for "^
1.632 - (tac2str (CAScmd ct')))
1.633 -
1.634 - | applicable_in p pt (Split_And) =
1.635 - raise error ("applicable_in: not impl. for "^
1.636 - (tac2str (Split_And)))
1.637 - | applicable_in p pt (Conclude_And) =
1.638 - raise error ("applicable_in: not impl. for "^
1.639 - (tac2str (Conclude_And)))
1.640 - | applicable_in p pt (Split_Or) =
1.641 - raise error ("applicable_in: not impl. for "^
1.642 - (tac2str (Split_Or)))
1.643 - | applicable_in p pt (Conclude_Or) =
1.644 - raise error ("applicable_in: not impl. for "^
1.645 - (tac2str (Conclude_Or)))
1.646 -
1.647 - | applicable_in (p,p_) pt (Begin_Trans) =
1.648 - let
1.649 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.650 - (*_____ implizit Take in gen*)
1.651 - Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
1.652 - | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
1.653 - | _ => raise error ("applicable_in: call by "^
1.654 - (pos'2str (p,p_)));
1.655 - val thy' = get_obj g_domID pt (par_pblobj pt p);
1.656 - in (Appl (Begin_Trans' f))
1.657 - handle _ => raise error ("applicable_in: Begin_Trans finds \
1.658 - \syntaxerror in '"^(term2str f)^"'") end
1.659 -
1.660 - (*TODO: check parent branches*)
1.661 - | applicable_in (p,p_) pt (End_Trans) =
1.662 - let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.663 - in if p_ = Res
1.664 - then Appl (End_Trans' (get_obj g_result pt p))
1.665 - else Notappl "'End_Trans' is not applicable at \
1.666 - \the beginning of a transitive sequence"
1.667 - (*TODO: check parent branches*)
1.668 - end
1.669 -
1.670 - | applicable_in p pt (Begin_Sequ) =
1.671 - raise error ("applicable_in: not impl. for "^
1.672 - (tac2str (Begin_Sequ)))
1.673 - | applicable_in p pt (End_Sequ) =
1.674 - raise error ("applicable_in: not impl. for "^
1.675 - (tac2str (End_Sequ)))
1.676 - | applicable_in p pt (Split_Intersect) =
1.677 - raise error ("applicable_in: not impl. for "^
1.678 - (tac2str (Split_Intersect)))
1.679 - | applicable_in p pt (End_Intersect) =
1.680 - raise error ("applicable_in: not impl. for "^
1.681 - (tac2str (End_Intersect)))
1.682 -(* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
1.683 - val (vvv,ppp) = vp;
1.684 -
1.685 - val Check_elementwise pred = m;
1.686 -
1.687 - val ((p,p_), Check_elementwise pred) = (p, m);
1.688 - *)
1.689 - | applicable_in (p,p_) pt (m as Check_elementwise pred) =
1.690 - if member op = [Pbl,Met] p_
1.691 - then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.692 - else
1.693 - let
1.694 - val pp = par_pblobj pt p;
1.695 - val thy' = (get_obj g_domID pt pp):theory';
1.696 - val thy = assoc_thy thy'
1.697 - val metID = (get_obj g_metID pt pp)
1.698 - val {crls,...} = get_met metID
1.699 - (*val _=writeln("### applicable_in Check_elementwise: crls= "^crls)
1.700 - val _=writeln("### applicable_in Check_elementwise: pred= "^pred)*)
1.701 - (*val erl = the (assoc'(!ruleset',crls))*)
1.702 - val (f,asm) = case p_ of
1.703 - Frm => (get_obj g_form pt p , [])
1.704 - | Res => get_obj g_result pt p;
1.705 - (*val _= writeln("### applicable_in Check_elementwise: f= "^f);*)
1.706 - val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred);
1.707 - (*val (v,p)=vp;val _=writeln("### applicable_in Check_elementwise: vp= "^
1.708 - pair2str(term2str v,term2str p))*)
1.709 - in case f of
1.710 - Const ("List.list.Cons",_) $ _ $ _ =>
1.711 - Appl (Check_elementwise'
1.712 - (f, pred,
1.713 - ((*writeln("### applicable_in Check_elementwise: --> "^
1.714 - (res2str (check_elementwise thy crls f vp)));*)
1.715 - check_elementwise thy crls f vp)))
1.716 - | Const ("Tools.UniversalList",_) =>
1.717 - Appl (Check_elementwise' (f, pred, (f,asm)))
1.718 - | Const ("List.list.Nil",_) =>
1.719 - (*Notappl "not applicable to empty list" 3.6.03*)
1.720 - Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))
1.721 - | _ => Notappl ("not applicable: "^(term2str f)^" should be constants")
1.722 - end
1.723 -
1.724 - | applicable_in (p,p_) pt Or_to_List =
1.725 - if member op = [Pbl,Met] p_
1.726 - then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))
1.727 - else
1.728 - let
1.729 - val pp = par_pblobj pt p;
1.730 - val thy' = (get_obj g_domID pt pp):theory';
1.731 - val thy = assoc_thy thy';
1.732 - val f = case p_ of
1.733 - Frm => get_obj g_form pt p
1.734 - | Res => (fst o (get_obj g_result pt)) p;
1.735 - in (let val ls = or2list f
1.736 - in Appl (Or_to_List' (f, ls)) end)
1.737 - handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))
1.738 - end
1.739 -
1.740 - | applicable_in p pt (Collect_Trues) =
1.741 - raise error ("applicable_in: not impl. for "^
1.742 - (tac2str (Collect_Trues)))
1.743 -
1.744 - | applicable_in p pt (Empty_Tac) =
1.745 - Notappl "Empty_Tac is not applicable"
1.746 -
1.747 - | applicable_in (p,p_) pt (Tac id) =
1.748 - let
1.749 - val pp = par_pblobj pt p;
1.750 - val thy' = (get_obj g_domID pt pp):theory';
1.751 - val thy = assoc_thy thy';
1.752 - val f = case p_ of
1.753 - Frm => get_obj g_form pt p
1.754 - | Res => (fst o (get_obj g_result pt)) p;
1.755 - in case id of
1.756 - "subproblem_equation_dummy" =>
1.757 - if is_expliceq f
1.758 - then Appl (Tac_ (thy, term2str f, id,
1.759 - "subproblem_equation_dummy ("^(term2str f)^")"))
1.760 - else Notappl "applicable only to equations made explicit"
1.761 - | "solve_equation_dummy" =>
1.762 - let (*val _= writeln("### applicable_in: solve_equation_dummy: f= "
1.763 - ^f);*)
1.764 - val (id',f') = split_dummy (term2str f);
1.765 - (*val _= writeln("### applicable_in: f'= "^f');*)
1.766 - (*val _= (term_of o the o (parse thy)) f';*)
1.767 - (*val _= writeln"### applicable_in: solve_equation_dummy";*)
1.768 - in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"
1.769 - else if is_expliceq ((term_of o the o (parse thy)) f')
1.770 - then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))
1.771 - else error ("applicable_in: f= " ^ f') end
1.772 - | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end
1.773 -
1.774 - | applicable_in p pt End_Proof' = Appl End_Proof''
1.775 -
1.776 - | applicable_in _ _ m =
1.777 - raise error ("applicable_in called for "^(tac2str m));
1.778 -
1.779 -(*WN060614 unused*)
1.780 -fun tac2tac_ pt p m =
1.781 - case applicable_in p pt m of
1.782 - Appl (m') => m'
1.783 - | Notappl _ => raise error ("tac2mstp': fails with"^
1.784 - (tac2str m));
1.785 -