(* use"ME/appl.sml";

    use"appl.sml";

 12345678901234567890123456789012345678901234567890123456789012345678901234567890

         10        20        30        40        50        60        70        80

 *)

 val e_cterm' = empty_cterm';

 fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =

     (rew_ord':rew_ord',erls,ca)

   | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =

     (rew_ord',erls,ca)

   | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) =

     (rew_ord',erls, ca)

   | rew_info rls = error ("rew_info called with '"^rls2str rls^"'");

 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)

 fun from_pblobj_or_detail_thm thm' p pt = 

     let val (pbl,p',rls') = par_pbl_det pt p

     in if pbl

        then let (*val _= tracing("### from_pblobj_or_detail_thm: pbl=true")*)

 	        val thy' = get_obj g_domID pt p'

 		val {rew_ord',erls,(*asm_thm,*)...} = 

 		    get_met (get_obj g_metID pt p')

 		(*val _= tracing("### from_pblobj_or_detail_thm: metID= "^

 			       (metID2str(get_obj g_metID pt p')))

 		val _= tracing("### from_pblobj_or_detail_thm: erls= "^erls)*)

 	    in ("OK",thy',rew_ord',erls,(*put_asm*)false) 

 	    end

        else ((*tracing("### from_pblobj_or_detail_thm: pbl=false");*)

 	     (*case assoc(!ruleset', rls') of  !!!FIXME.3.4.03:re-organize !!!

 		NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false)

 	      | SOME rls =>*)

 		let val thy' = get_obj g_domID pt (par_pblobj pt p)

 		    val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls'

 		in ("OK",thy',rew_ord',erls,false) end)

     end;

 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)

 fun from_pblobj_or_detail_calc scrop p pt = 

 (* val (scrop, p, pt) = (op_, p, pt);

    *)

     let val (pbl,p',rls') = par_pbl_det pt p

     in if pbl

        then let val thy' = get_obj g_domID pt p'

 		val {calc = scr_isa_fns,...} = 

 		    get_met (get_obj g_metID pt p')

 		val opt = assoc (scr_isa_fns, scrop)

 	    in case opt of

 		   SOME isa_fn => ("OK",thy',isa_fn)

 		 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",

 			    "",("",e_evalfn)) end

        else (*case assoc(!ruleset', rls') of

 		NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn))

 	      | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*)

 		(* val SOME rls = assoc(!ruleset', rls');

 		   *)

 		let val thy' = get_obj g_domID pt (par_pblobj pt p);

 		    val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)

 		in case assoc (scr_isa_fns, scrop) of

 		   SOME isa_fn => ("OK",thy',isa_fn)

 		 | NONE => ("applicable_in Calculate: unknown '"^scrop^"'",

 			    "",("",e_evalfn)) end

     end;

 (*------------------------------------------------------------------*)

 val op_and = Const ("op &", [bool, bool] ---> bool);

 (*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool));

 val it = "a & b" : cterm

 *)

 fun mk_and a b = op_and $ a $ b;

 (*> (cterm_of thy) 

      (mk_and (Free("a",bool)) (Free("b",bool)));

 val it = "a & b" : cterm*)

 fun mk_and [] = HOLogic.true_const

   | mk_and (t::[]) = t

   | mk_and (t::ts) = 

     let fun mk t' (t::[]) = op_and $ t' $ t

 	  | mk t' (t::ts) = mk (op_and $ t' $ t) ts

     in mk t ts end;

 (*> val pred = map (term_of o the o (parse thy)) 

              ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"];

 > (cterm_of thy) (mk_and pred);

 val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*)

 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)

 fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, [])

   | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred =

     (e_term, if pred <> Const ("Script.Assumptions",bool)

 	     then [pred] 

 	     else get_assumptions_ pt (p,Res))

 (* val pred = (term_of o the o (parse thy)) pred;

    val consts as Const ("List.list.Cons",_) $ eq $ _ = ft;

    mk_set thy pt p consts pred;

    *)

   | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred =

   let val (bdv,_) = HOLogic.dest_eq eq;

     val pred = if pred <> Const ("Script.Assumptions",bool)

 		 then [pred] 

 	       else get_assumptions_ pt (p,Res)

   in (bdv, pred) end

   | mk_set thy _ _ l _ = 

     error ("check_elementwise: no set " ^ term2str l);

 (*> val consts = str2term "[x=#4]";

 > val pred = str2term "Assumptions";

 > val pt = union_asm pt p 

    [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]),

    ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];

 > val p = [];

 > val (sss,ttt) = mk_set thy pt p consts pred;

 > (term2str sss, term2str ttt);

 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...

  val consts = str2term "UniversalList";

  val pred = str2term "Assumptions";

 *)

 (*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*)

 (* val (erls,consts,(bdv,pred)) = (erl,ft,vp);

    val (consts,(bdv,pred)) = (ft,vp);

    *)

 fun check_elementwise thy erls all_results (bdv, asm) =

     let   (*bdv extracted from ~~~~~~~~~~~ in mk_set already*)

 	fun check sub =

 	    let val inst_ = map (subst_atomic [sub]) asm

 	    in case eval__true thy 1 inst_ [] erls of

 		   (asm', true) => ([HOLogic.mk_eq sub], asm')

 		 | (_, false) => ([],[])

 	    end;

       (*val _= tracing("### check_elementwise: res= "^(term2str all_results)^

 		       ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*)

 	val c' = isalist2list all_results

 	val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*)

 	val subs = map (pair bdv) c''

     in if asm = [] then (all_results, [])

        else ((apfst ((list2isalist bool) o flat)) o 

 	     (apsnd flat) o split_list o (map check)) subs end;

 (* 20.5.03

 > val all_results = str2term "[x=a+b,x=b,x=3]";

 > val bdv = str2term "x";

 > val asm = str2term "(x ~= a) & (x ~= b)";

 > val erls = e_rls;

 > val (t, ts) = check_elementwise thy erls all_results (bdv, asm);

 > term2str t; tracing(terms2str ts);

 val it = "[x = a + b, x = b, x = c]" : string

 ["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"]

 ... with appropriate erls this should be:

 val it = "[x = a + b,       x = c]" : string

 ["b ~= 0 & a ~= 0",         "3 ~= a & 3 ~= b"]

                     ////// because b ~= b False*)

 (*before 5.03-----

 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\

 	   \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";

 > val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;

 val ct' = "HOL.True" : cterm'

 > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\

 	   \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";

 > val SOME(ct',_) = rewrite_set "Isac"  false "eval_rls" ct;

 val ct' = "HOL.True" : cterm'

 > val const  = (term_of o the o (parse thy)) "(#3::real)";

 > val pred' = subst_atomic [(bdv,const)] pred;

 > val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]";

 > val bdv    = (term_of o the o (parse thy)) "(x::real)";

 > val pred   = (term_of o the o (parse thy)) 

   "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4";

 > val ttt = check_elementwise thy consts (bdv, pred);

 > (cterm_of thy) ttt;

 val it = "[x = #-3, x = #3]" : cterm

 > val consts = (term_of o the o (parse thy)) "[x = #4]";

 > val bdv    = (term_of o the o (parse thy)) "(x::real)";

 > val pred   = (term_of o the o (parse thy)) 

  "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x";

 > val ttt = check_elementwise thy consts (bdv,pred);

 > (cterm_of thy) ttt;

 val it = "[x = #4]" : cterm

 > val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]";

 > val bdv    = (term_of o the o (parse thy)) "(x::real)";

 > val pred   = (term_of o the o (parse thy))

  " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x";

 > val ttt = check_elementwise thy consts (bdv,pred);

 > (cterm_of thy) ttt;

 val it = "[]" : cterm*)

 (* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*)

 fun split_dummy str = 

 let fun scan s' [] = (implode s', "")

       | scan s' (s::ss) = if s=" " then (implode s', implode  ss)

 			  else scan (s'@[s]) ss;

 in ((scan []) o Symbol.explode) str end;

 (* split_dummy "subproblem_equation_dummy (x=-#5//#12)";

 val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string

 > split_dummy "x=-#5//#12";

 val it = ("x=-#5//#12","") : string * string*)

 (*.applicability of a tacic wrt. a calc-state (ptree,pos').

    additionally used by next_tac in the script-interpreter for script-tacs.

    tests for applicability are so expensive, that results (rewrites!)

    are kept in the return-value of 'type tac_'.

 .*)

 fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Appl (Init_Proof' (ct', spec))

   | applicable_in (p,p_) pt Model_Problem = 

       if not (is_pblobj (get_obj I pt p)) orelse p_ = Res

       then Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))

       else 

         let 

           val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p

 	        val {ppc,...} = get_pbt pI'

 	        val pbl = init_pbl ppc

         in Appl (Model_Problem' (pI', pbl, [])) end

   | applicable_in (p,p_) pt (Refine_Tacitly pI) = 

       if not (is_pblobj (get_obj I pt p)) orelse p_ = Res

       then Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))

       else 

         let 

           val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;

           val opt = refine_ori oris pI;

         in case opt of

 	           SOME pblID => 

 	             Appl (Refine_Tacitly' (pI, pblID, 

 				         e_domID, e_metID, [](*filled in specify*)))

 	         | NONE => Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")

         end

   | applicable_in (p,p_) pt (Refine_Problem pI) = 

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Refine_Problem pI))^

 	   " not for pos "^(pos'2str (p,p_)))

   else

     let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_),

 		     probl=itms, ...}) = get_obj I pt p;

 	val thy = if dI' = e_domID then dI else dI';

 	val rfopt = refine_pbl (assoc_thy thy) pI itms;

     in case rfopt of

 	   NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable")

 	 | SOME (rf as (pI',_)) =>

 (* val SOME (rf as (pI',_)) = rfopt;

    *)

 	   if pI' = pI

 	   then Notappl ((tac2str (Refine_Problem pI))^" not applicable")

 	   else Appl (Refine_Problem' rf)

     end

   (*the specify-tacs have cterm' instead term: 

    parse+error here!!!: see appl_add*)  

   | applicable_in (p,p_) pt (Add_Given ct') = 

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Add_Given ct'))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Add_Given' (ct', [(*filled in specify_additem*)]))

   (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)

   | applicable_in (p,p_) pt (Del_Given ct') =

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Del_Given ct'))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Del_Given' ct')

   | applicable_in (p,p_) pt (Add_Find ct') =                   

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Add_Find ct'))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Add_Find' (ct', [(*filled in specify_additem*)]))

   | applicable_in (p,p_) pt (Del_Find ct') =

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Del_Find ct'))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Del_Find' ct')

   | applicable_in (p,p_) pt (Add_Relation ct') =               

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Add_Relation ct'))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Add_Relation' (ct', [(*filled in specify_additem*)]))

   | applicable_in (p,p_) pt (Del_Relation ct') =

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Del_Relation ct'))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Del_Relation' ct')

   | applicable_in (p,p_) pt (Specify_Theory dI) =              

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Specify_Theory dI))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Specify_Theory' dI)

 (* val (p,p_) = p; val Specify_Problem pID = m;

    val Specify_Problem pID = m;

    *)

   | applicable_in (p,p_) pt (Specify_Problem pID) = 

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

     then Notappl ((tac2str (Specify_Problem pID))^

 	   " not for pos "^(pos'2str (p,p_)))

   else

     let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_),

 		     probl=itms, ...}) = get_obj I pt p;

 	val thy = assoc_thy (if dI' = e_domID then dI else dI');

         val {ppc,where_,prls,...} = get_pbt pID;

 	val pbl = if pI'=e_pblID andalso pI=e_pblID

 		  then (false, (init_pbl ppc, []))

 		  else match_itms_oris thy itms (ppc,where_,prls) oris;

     in Appl (Specify_Problem' (pID, pbl)) end

 (* val Specify_Method mID = nxt; val (p,p_) = p; 

    *)

   | applicable_in (p,p_) pt (Specify_Method mID) =              

   if not (is_pblobj (get_obj I pt p)) orelse p_ = Res               

     then Notappl ((tac2str (Specify_Method mID))^

 	   " not for pos "^(pos'2str (p,p_)))

   else Appl (Specify_Method' (mID,[(*filled in specify*)],

 			      [(*filled in specify*)]))

   | applicable_in (p,p_) pt (Apply_Method mI) =                

       if not (is_pblobj (get_obj I pt p)) orelse p_ = Res                  

       then Notappl ((tac2str (Apply_Method mI)) ^ " not for pos " ^ (pos'2str (p,p_)))

       else

         let

           val (PblObj{origin = (_, (dI, pI, _), _), probl, ctxt, ...}) = get_obj I pt p;

           val {where_, ...} = get_pbt pI

           val pres = map (mk_env probl |> subst_atomic) where_

           val ctxt = 

             if is_e_ctxt ctxt

             then assoc_thy dI |> ProofContext.init_global |> insert_assumptions pres

             else ctxt

          (*TODO.WN110416 here do evalprecond according to fun check_preconds'

          and then decide on Notappl/Appl accordingly once more.

          Implement after all tests are running, since this changes

          overall system behavior*)

       in Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*), ctxt)) end

   | applicable_in (p,p_) pt (Check_Postcond pI) =

       if member op = [Pbl,Met] p_                  

       then Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))

       else Appl (Check_Postcond' (pI, (e_term, [(*fun solve assignes the returnvalue of scr*)])))

   (*these are always applicable*)

   | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))

   | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')

   | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p;

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy';

     val {rew_ord'=ro',erls=erls,...} = 

       get_met (get_obj g_metID pt pp);

     val (f,p) = case p_ of (*p 12.4.00 unnecessary*)

               Frm => (get_obj g_form pt p, p)

 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

 	    | _ => error ("applicable_in: call by "^

 				(pos'2str (p,p_)));

   in 

     let val subst = subs2subst thy subs;

 	val subs' = subst2subs' subst;

     in case rewrite_inst_ thy (assoc_rew_ord ro') erls

 			 (*put_asm*)false subst (assoc_thm' thy thm') f of

       SOME (f',asm) => Appl (

 	  Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',

       (*term_of o the o (parse (assoc_thy thy'))*) f,

        (*(term_of o the o (parse (assoc_thy thy'))*) (f',

 	(*map (term_of o the o (parse (assoc_thy thy')))*) asm)))

     | NONE => Notappl ((fst thm')^" not applicable") end

   handle _ => Notappl ("syntax error in "^(subs2str subs)) end

 (* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);

    val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);

    *)

 | applicable_in (p,p_) pt (m as Rewrite thm') = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt;

     val thy = assoc_thy thy';

     val f = case p_ of

               Frm => get_obj g_form pt p

 	    | Res => (fst o (get_obj g_result pt)) p

 	    | _ => error ("applicable_in Rewrite: call by "^

 				(pos'2str (p,p_)));

   in if msg = "OK" 

      then

       ((*tracing("### applicable_in rls'= "^rls');*)

        (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f;

 	  *)

        case rewrite_ thy (assoc_rew_ord ro) 

 		     rls' false (assoc_thm' thy thm') f of

        SOME (f',asm) => Appl (

 	   Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm)))

      | NONE => Notappl ("'"^(fst thm')^"' not applicable") )

      else Notappl msg

   end

 | applicable_in (p,p_) pt (m as Rewrite_Asm thm') = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p; 

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy';

     val {rew_ord'=ro',erls=erls,...} = 

       get_met (get_obj g_metID pt pp);

     (*val put_asm = true;*)

     val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)

               Frm => (get_obj g_form pt p, p)

 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

 	    | _ => error ("applicable_in: call by "^

 				(pos'2str (p,p_)));

   in case rewrite_ thy (assoc_rew_ord ro') erls 

 		   (*put_asm*)false (assoc_thm' thy thm') f of

        SOME (f',asm) => Appl (

 	   Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm)))

      | NONE => Notappl ("'"^(fst thm')^"' not applicable") end

   | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p;

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy';

     val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp);

     val f = case p_ of Frm => get_obj g_form pt p

 		     | Res => (fst o (get_obj g_result pt)) p

 		     | _ => error ("applicable_in: call by "^

 					 (pos'2str (p,p_)));

   in 

       let val subst = subs2subst thy subs

 	  val subs' = subst2subs' subst

       in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of

       SOME (f',asm) => Appl (

 	  Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm)))

     | NONE => Notappl (rls^" not applicable") end

   handle _ => Notappl ("syntax error in "^(subs2str subs)) end

   | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p;

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy';

     val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} = 

       get_met (get_obj g_metID pt pp);

     val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)

               Frm => (get_obj g_form pt p, p)

 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

 	    | _ => error ("applicable_in: call by "^

 				(pos'2str (p,p_)));

   in 

     let val subst = subs2subst thy subs;

 	val subs' = subst2subs' subst;

     in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of

       SOME (f',asm) => Appl (

 	  Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm)))

     | NONE => Notappl (rls^" not applicable") end

   handle _ => Notappl ("syntax error in "^(subs2str subs)) end

   | applicable_in (p,p_) pt (m as Rewrite_Set rls) = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p; 

     val thy' = (get_obj g_domID pt pp):theory';

     val (f,p) = case p_ of  (*p 12.4.00 unnecessary*)

               Frm => (get_obj g_form pt p, p)

 	    | Res => ((fst o (get_obj g_result pt)) p, lev_on p)

 	    | _ => error ("applicable_in: call by "^

 				(pos'2str (p,p_)));

   in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of

        SOME (f',asm) => 

 	((*tracing("#.# applicable_in Rewrite_Set,2f'= "^f');*)

 	 Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm)))

 	 )

      | NONE => Notappl (rls^" not applicable") end

   | applicable_in (p,p_) pt (m as Detail_Set rls) =

     if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

     else

 	let val pp = par_pblobj pt p 

 	    val thy' = (get_obj g_domID pt pp):theory'

 	    val f = case p_ of

 			Frm => get_obj g_form pt p

 		      | Res => (fst o (get_obj g_result pt)) p

 		      | _ => error ("applicable_in: call by "^

 					  (pos'2str (p,p_)));

 	in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of

 	       SOME (f',asm) => 

 	       Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm)))

 	     | NONE => Notappl (rls^" not applicable") end

   | applicable_in p pt (End_Ruleset) = 

   error ("applicable_in: not impl. for "^

 	       (tac2str End_Ruleset))

 (* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m);

    *)

 | applicable_in (p,p_) pt (m as Calculate op_) = 

   if member op = [Pbl,Met] p_

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;

     val f = case p_ of

               Frm => get_obj g_form pt p

 	    | Res => (fst o (get_obj g_result pt)) p

   in if msg = "OK" then

 	 case calculate_ (assoc_thy thy') isa_fn f of

 	     SOME (f', (id, thm)) => 

 	     Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm))))

 	   | NONE => Notappl ("'calculate "^op_^"' not applicable") 

      else Notappl msg

   end

 (*Substitute combines two different kind of "substitution":

   (1) subst_atomic: for ?a..?z

   (2) Pattern.match: for solving equational systems 

       (which raises exn for ?a..?z)*)

   | applicable_in (p,p_) pt (m as Substitute sube) = 

   if member op = [Pbl,Met] p_ 

   then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else let val pp = par_pblobj pt p

 	   val thy = assoc_thy (get_obj g_domID pt pp)

 	   val f = case p_ of

 		       Frm => get_obj g_form pt p

 		     | Res => (fst o (get_obj g_result pt)) p

 	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)

 	   val subte = sube2subte sube

 	   val subst = sube2subst thy sube

        in if foldl and_ (true, map contains_Var subte)

 	  (*1*)

 	  then let val f' = subst_atomic subst f

 	       in if f = f' then Notappl (sube2str sube^" not applicable")

 		  else Appl (Substitute' (subte, f, f'))

 	       end

 	  (*2*)

 	  else case rewrite_terms_ thy (assoc_rew_ord rew_ord') 

 				   erls subte f of

 		   SOME (f', _) =>  Appl (Substitute' (subte, f, f'))

 		 | NONE => Notappl (sube2str sube^" not applicable")

        end

 (*-------WN08114 interrupted with error in polyminus.sml "11 = 11"

   | applicable_in (p,p_) pt (m as Substitute sube) = 

   if member op = [Pbl,Met] p_ 

   then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else let val pp = par_pblobj pt p

 	   val thy = assoc_thy (get_obj g_domID pt pp)

 	   val f = case p_ of

 		       Frm => get_obj g_form pt p

 		     | Res => (fst o (get_obj g_result pt)) p

 	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)

 	   val subte = sube2subte sube

        in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of

 	      SOME (f', _) =>  Appl (Substitute' (subte, f, f'))

 	    | NONE => Notappl (sube2str sube^" not applicable")

        end

 ------------------*)

   | applicable_in p pt (Apply_Assumption cts') = 

       (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts'))))

   (*'logical' applicability wrt. script in locate: Inconsistent?*)

   | applicable_in (p,p_) pt (m as Take ct') = 

       if member op = [Pbl,Met] p_ 

       then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_))

       else

         let val thy' = get_obj g_domID pt (par_pblobj pt p);

         in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of

 	            SOME ct => Appl (Take' ct)

 	          | NONE => Notappl ("syntax error in " ^ ct'))

         end

   | applicable_in p pt (Take_Inst ct') = 

       error ("applicable_in: not impl. for " ^ tac2str (Take_Inst ct'))

   | applicable_in p pt (Group (con, ints)) = 

       error ("applicable_in: not impl. for " ^ tac2str (Group (con, ints)))

   | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) = 

      if member op = [Pbl,Met] p_

      then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)

 	      case get_obj g_env pt p of

 	        SOME is => 

             Appl (Subproblem' ((domID, pblID, e_metID), [], 

 					    e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID))

 	      | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

      else (*somewhere later in the script*)

        Appl (Subproblem' ((domID, pblID, e_metID), [], 

 			   e_term, [], e_ctxt, subpbl domID pblID))

   | applicable_in p pt (End_Subproblem) =

       error ("applicable_in: not impl. for " ^ tac2str End_Subproblem)

   | applicable_in p pt (CAScmd ct') = 

       error ("applicable_in: not impl. for " ^ tac2str (CAScmd ct'))  

   | applicable_in p pt (Split_And) = 

       error ("applicable_in: not impl. for " ^ tac2str Split_And)

   | applicable_in p pt (Conclude_And) = 

       error ("applicable_in: not impl. for " ^ tac2str Conclude_And)

   | applicable_in p pt (Split_Or) = 

       error ("applicable_in: not impl. for " ^ tac2str Split_Or)

   | applicable_in p pt (Conclude_Or) = 

       error ("applicable_in: not impl. for " ^ tac2str Conclude_Or)

   | applicable_in (p,p_) pt (Begin_Trans) =

     let

       val (f,p) = case p_ of   (*p 12.4.00 unnecessary*)

 	                             (*_____ implizit Take in gen*)

 	Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)

       | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)

       | _ => error ("applicable_in: call by "^

 				(pos'2str (p,p_)));

       val thy' = get_obj g_domID pt (par_pblobj pt p);

     in (Appl (Begin_Trans' f))

       handle _ => error ("applicable_in: Begin_Trans finds \

                                \syntaxerror in '"^(term2str f)^"'") end

     (*TODO: check parent branches*)

   | applicable_in (p,p_) pt (End_Trans) =

     let val thy' = get_obj g_domID pt (par_pblobj pt p);

     in if p_ = Res 

 	   then Appl (End_Trans' (get_obj g_result pt p))

        else Notappl "'End_Trans' is not applicable at \

 	\the beginning of a transitive sequence"

 	 (*TODO: check parent branches*)

     end

   | applicable_in p pt (Begin_Sequ) = 

   error ("applicable_in: not impl. for "^

 	       (tac2str (Begin_Sequ)))

   | applicable_in p pt (End_Sequ) = 

   error ("applicable_in: not impl. for "^

 	       (tac2str (End_Sequ)))

   | applicable_in p pt (Split_Intersect) = 

   error ("applicable_in: not impl. for "^

 	       (tac2str (Split_Intersect)))

   | applicable_in p pt (End_Intersect) = 

   error ("applicable_in: not impl. for "^

 	       (tac2str (End_Intersect)))

 (* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;

    val (vvv,ppp) = vp;

    val Check_elementwise pred = m;

    val ((p,p_), Check_elementwise pred) = (p, m);

    *)

   | applicable_in (p,p_) pt (m as Check_elementwise pred) = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p; 

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy'

     val metID = (get_obj g_metID pt pp)

     val {crls,...} =  get_met metID

     (*val _=tracing("### applicable_in Check_elementwise: crls= "^crls)

     val _=tracing("### applicable_in Check_elementwise: pred= "^pred)*)

     (*val erl = the (assoc'(!ruleset',crls))*)

     val (f,asm) = case p_ of

               Frm => (get_obj g_form pt p , [])

 	    | Res => get_obj g_result pt p;

     (*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)

     val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;

     (*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^

 			       pair2str(term2str v,term2str p))*)

   in case f of

       Const ("List.list.Cons",_) $ _ $ _ =>

 	Appl (Check_elementwise'

 		  (f, pred, 

 		   ((*tracing("### applicable_in Check_elementwise: --> "^

 			    (res2str (check_elementwise thy crls f vp)));*)

 		   check_elementwise thy crls f vp)))

     | Const ("Tools.UniversalList",_) => 

       Appl (Check_elementwise' (f, pred, (f,asm)))

     | Const ("List.list.Nil",_) => 

       (*Notappl "not applicable to empty list" 3.6.03*) 

       Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))

     | _ => Notappl ("not applicable: "^(term2str f)^" should be constants")

   end

   | applicable_in (p,p_) pt Or_to_List = 

   if member op = [Pbl,Met] p_ 

     then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_)))

   else

   let 

     val pp = par_pblobj pt p; 

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy';

     val f = case p_ of

               Frm => get_obj g_form pt p

 	    | Res => (fst o (get_obj g_result pt)) p;

   in (let val ls = or2list f

       in Appl (Or_to_List' (f, ls)) end) 

      handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f))

   end

   | applicable_in p pt (Collect_Trues) = 

   error ("applicable_in: not impl. for "^

 	       (tac2str (Collect_Trues)))

   | applicable_in p pt (Empty_Tac) = 

   Notappl "Empty_Tac is not applicable"

   | applicable_in (p,p_) pt (Tac id) =

   let 

     val pp = par_pblobj pt p; 

     val thy' = (get_obj g_domID pt pp):theory';

     val thy = assoc_thy thy';

     val f = case p_ of

               Frm => get_obj g_form pt p

             | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"

 	    | Res => (fst o (get_obj g_result pt)) p;

   in case id of

       "subproblem_equation_dummy" =>

 	  if is_expliceq f

 	  then Appl (Tac_ (thy, term2str f, id,

 			     "subproblem_equation_dummy ("^(term2str f)^")"))

 	  else Notappl "applicable only to equations made explicit"

     | "solve_equation_dummy" =>

 	  let (*val _= tracing("### applicable_in: solve_equation_dummy: f= "

 				 ^f);*)

 	    val (id',f') = split_dummy (term2str f);

 	    (*val _= tracing("### applicable_in: f'= "^f');*)

 	    (*val _= (term_of o the o (parse thy)) f';*)

 	    (*val _= tracing"### applicable_in: solve_equation_dummy";*)

 	  in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem"

 	     else if (thy2ctxt thy, f') |-> parseNEW |> the |> is_expliceq

 		      then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]"))

 		  else error ("applicable_in: f= " ^ f') end

     | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end

   | applicable_in p pt End_Proof' = Appl End_Proof''

   | applicable_in _ _ m = 

   error ("applicable_in called for "^(tac2str m));

 (*WN060614 unused*)

 fun tac2tac_ pt p m = 

     case applicable_in p pt m of

 	Appl (m') => m' 

       | Notappl _ => error ("tac2mstp': fails with"^

 				  (tac2str m));