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