(* 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 thy' = get_obj g_domID pt p'

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

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

      else 

       let

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

 		    val (rew_ord', erls, _) = 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 = 

   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,...} = Specify.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 

 		  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);

 (*> (Thm.global_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;

 (*> (Thm.global_cterm_of thy) 

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

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

 fun mk_and [] = @{term True}

   | 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 (Thm.term_of o the o (parse thy)) 

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

 > (Thm.global_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 = (Thm.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  = (Thm.term_of o the o (parse thy)) "(#3::real)";

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

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

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

 > val pred   = (Thm.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);

 > (Thm.global_cterm_of thy) ttt;

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

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

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

 > val pred   = (Thm.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);

 > (Thm.global_cterm_of thy) ttt;

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

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

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

 > val pred   = (Thm.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);

 > (Thm.global_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)) = Chead.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 Chead.Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))

       else 

         let 

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

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

 	        val pbl = Generate.init_pbl ppc

         in Chead.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 Chead.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 = Specify.refine_ori oris pI;

         in case opt of

 	           SOME pblID => 

 	             Chead.Appl (Refine_Tacitly' (pI, pblID, 

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

 	         | NONE => Chead.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 Chead.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 = Specify.refine_pbl (assoc_thy thy) pI itms;

     in case rfopt of

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

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

 	   if pI' = pI

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

 	   else Chead.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 Chead.Notappl ((tac2str (Add_Given ct'))^

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

   else Chead.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 Chead.Notappl ((tac2str (Del_Given ct'))^

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

   else Chead.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 Chead.Notappl ((tac2str (Add_Find ct'))^

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

   else Chead.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 Chead.Notappl ((tac2str (Del_Find ct'))^

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

   else Chead.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 Chead.Notappl ((tac2str (Add_Relation ct'))^

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

   else Chead.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 Chead.Notappl ((tac2str (Del_Relation ct'))^

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

   else Chead.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 Chead.Notappl ((tac2str (Specify_Theory dI))^

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

   else Chead.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 Chead.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,...} = Specify.get_pbt pID;

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

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

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

     in Chead.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 Chead.Notappl ((tac2str (Specify_Method mID))^

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

   else Chead.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 Chead.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_, ...} = Specify.get_pbt pI

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

           val ctxt = 

             if is_e_ctxt ctxt

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

             else ctxt

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

          and then decide on Chead.Notappl/Appl accordingly once more.

          Implement after all tests are running, since this changes

          overall system behavior*)

       in Chead.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 Chead.Notappl ((tac2str (Check_Postcond pI)) ^ " not for pos "^(pos'2str (p,p_)))

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

   (*these are always applicable*)

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

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

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

     if member op = [Pbl, Met] p_ 

     then Chead.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, ...} = Specify.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 false subst (snd thm'') f of

              SOME (f',asm) =>

                Chead.Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))

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

         end

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

       end

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

   if member op = [Pbl,Met] p_ 

     then Chead.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

         case rewrite_ thy (assoc_rew_ord ro) rls' false (snd thm'') f of

          SOME (f',asm) => Chead.Appl (Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))

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

      else Chead.Notappl msg

   end

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

   if member op = [Pbl,Met] p_ 

     then Chead.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,...} = Specify.get_met (get_obj g_metID pt pp);

     (*val put_asm = true;*)

     val (f, _) = case p_ of

               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 false (snd thm'') f of

        SOME (f',asm) => Chead.Appl (

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

      | NONE => Chead.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 Chead.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',...} = Specify.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) => Chead.Appl (

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

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

   handle _ => Chead.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 Chead.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,*)...} = Specify.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) => Chead.Appl (

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

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

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

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

   if member op = [Pbl,Met] p_ 

     then Chead.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');*)

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

 	 )

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

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

     if member op = [Pbl,Met] p_ 

     then Chead.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) => 

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

 	     | NONE => Chead.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 Chead.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)) => 

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

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

      else Chead.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 Chead.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,...} = Specify.get_met (get_obj g_metID pt pp)

 		      val subte = sube2subte sube

 		      val subst = sube2subst thy sube

 		      val ro = assoc_rew_ord rew_ord'

 		    in

 		      if foldl and_ (true, map contains_Var subte)

 		      (*1*)

 		      then

 		        let val f' = subst_atomic subst f

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

 		           else Chead.Appl (Substitute' (ro, erls, subte, f, f'))

 		        end

 		        (*2*)

 		      else 

 		        case rewrite_terms_ thy ro erls subte f of

 		            SOME (f', _) =>  Chead.Appl (Substitute' (ro, erls, subte, f, f'))

 		          | NONE => Chead.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 Chead.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 => Chead.Appl (Take' ct)

 	          | NONE => Chead.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 => 

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

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

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

      else (*somewhere later in the script*)

        Chead.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 (Chead.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 Chead.Appl (End_Trans' (get_obj g_result pt p))

        else Chead.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))

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

     if member op = [Pbl,Met] p_ 

     then Chead.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,...} =  Specify.get_met metID

         val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])

                                | Res => get_obj g_result pt p;

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

       in case f of

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

              Chead.Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))

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

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

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

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

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

       end

   | applicable_in (p,p_) pt Or_to_List = 

   if member op = [Pbl,Met] p_ 

     then Chead.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 Chead.Appl (Or_to_List' (f, ls)) end) 

      handle _ => Chead.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) = 

   Chead.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 Chead.Appl (Tac_ (thy, term2str f, id,

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

 	  else Chead.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 _= (Thm.term_of o the o (parse thy)) f';*)

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

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

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

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

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

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

   | applicable_in p pt End_Proof' = Chead.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

 	Chead.Appl (m') => m' 

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

 				  (tac2str m));