(* 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 sequence-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

(* val Refine_Tacitly pI = m;

   *)

  | 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 (* val Refine_Tacitly pI = m;

          *)

    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

(* val (p,p_) = ip;

   val Refine_Problem pI = m;

   *)

  | 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, ...}) = get_obj I pt p;

    val {where_, ...} = get_pbt pI

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

    val ctxt = assoc_thy dI |> ProofContext.init_global 

          |> insert_assumptions pres

    (*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,[(*asm in solve*)])))

  (* in solve -"-     ^^^^^^ gets 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')

(* val m as Rewrite_Inst (subs, thm') = m;

   *)

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

	 case get_obj g_env pt p of

	     SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [], 

					   e_term, [], 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, [], 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));