val lev_up : pos -> pos

   val lev_up : pos -> pos

   val lev_of : pos' -> int

   val lev_of : pos' -> int

   val pos_plus : int -> pos' -> pos'

   val pos_plus : int -> pos' -> pos'

   val lev_back' : pos' -> pos'                                                (* for inform.sml *)

   val lev_back' : pos' -> pos'                                                (* for inform.sml *)

   val is_interpos : pos' -> bool                                           (* for interface.sml *)

   val is_interpos : pos' -> bool                                           (* for interface.sml *)

   val just_created_ : ppobj -> bool                                       (* for mathengine.sml *)

   val just_created_ : ppobj -> bool                                       (* for mathengine.sml *)

   val e_origin : ori list * spec * term                                   (* for mathengine.sml *)

   val e_origin : ori list * spec * term                                   (* for mathengine.sml *)

   val is_pblobj : ppobj -> bool

   val is_pblobj : ppobj -> bool

   val g_spec : ppobj -> spec

   val g_spec : ppobj -> spec

   val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

   val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

   val g_form : ppobj -> term

   val g_form : ppobj -> term

   val g_pbl : ppobj -> itm list

   val g_pbl : ppobj -> itm list

   val g_tac : ppobj -> tac

   val g_tac : ppobj -> tac

   val g_domID : ppobj -> domID                           (* for appl.sml TODO: replace by thyID *)

   val g_domID : ppobj -> domID                           (* for appl.sml TODO: replace by thyID *)

   val g_env : ppobj -> (istate * Proof.context) option                          (* for appl.sml *)

   val g_env : ppobj -> (istate * Proof.context) option                          (* for appl.sml *)

   val g_origin : ppobj -> ori list * spec * term                              (* for script.sml *)

   val g_origin : ppobj -> ori list * spec * term                              (* for script.sml *)

   val append_atomic :                                                          (* for solve.sml *)

   val append_atomic :                                                          (* for solve.sml *)

   val e_ctxt : Proof.context

   val e_ctxt : Proof.context

   val is_e_ctxt : Proof.context -> bool                                         (* for appl.sml *)

   val is_e_ctxt : Proof.context -> bool                                         (* for appl.sml *)

   val new_val : term -> istate -> istate

   val new_val : term -> istate -> istate

   (* for calchead.sml *)

   (* for calchead.sml *)

   type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

   type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

   datatype ptform = Form of term | ModSpec of ocalhd

   datatype ptform = Form of term | ModSpec of ocalhd

   val get_somespec' : spec -> spec -> spec

   val get_somespec' : spec -> spec -> spec

   exception PTREE of string;

   exception PTREE of string;

   (* for appl.sml *)

   (* for appl.sml *)

   (* for rewtools.sml *)

   (* for rewtools.sml *)

   val rule2tac : theory -> (term * term) list -> rule -> tac

   val rule2tac : theory -> (term * term) list -> rule -> tac

   val eq_tac : tac * tac -> bool

   val eq_tac : tac * tac -> bool

   (* for script.sml *)

   (* for script.sml *)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   val g_res : ppobj -> term

   val g_res : ppobj -> term

   val pr_short : pos -> ppobj -> string

   val pr_short : pos -> ppobj -> string

   val is_empty_tac : tac -> bool

   val is_empty_tac : tac -> bool

   val e_subs : string list

   val e_subs : string list

   val e_sube : cterm' list

   val e_sube : cterm' list

   val g_branch : ppobj -> branch

   val g_branch : ppobj -> branch

   val g_ctxt : ppobj -> Proof.context

   val g_ctxt : ppobj -> Proof.context

   val g_fmz : ppobj -> fmz

   val g_fmz : ppobj -> fmz

   val subte2subst : term list -> (term * term) list

   val subte2subst : term list -> (term * term) list

   val branch2str : branch -> string

   val branch2str : branch -> string

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 end

 (*

 (*

 structure Ctree :

 structure Ctree :

 sig

 sig

   val Ets : ets exception PTREE of string

   val Ets : ets exception PTREE of string

   val append_atomic :

   val append_atomic :

   datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB

   datatype branch = AndB | CollectB | IntersectB | MapB | NoBranch | OrB | SequenceB | TransitiveB

   val branch2str : branch -> string

   val branch2str : branch -> string

   val cappend_atomic :

   val cappend_atomic :

   val cappend_problem :

   val cappend_problem :

   eqtype cellID

   eqtype cellID

   type cid = cellID list

   type cid = cellID list

   datatype con = land | lor

   datatype con = land | lor

   val cutlevup : ppobj -> bool

   val cutlevup : ppobj -> bool

   val del_res : ppobj -> ppobj

   val del_res : ppobj -> ppobj

   val e_ctxt : Proof.context

   val e_ctxt : Proof.context

   val e_fmz : 'a list * spec

   val e_fmz : 'a list * spec

   val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec

   val e_ocalhd : bool * pos_ * term * itm list * (bool * term) list * spec

   val e_origin : ori list * spec * term

   val e_origin : ori list * spec * term

   val e_ptform : ptform

   val e_ptform : ptform

   val e_ptform' : ptform

   val e_ptform' : ptform

   val e_scrstate : scrstate

   val e_scrstate : scrstate

   val e_sube : cterm' list

   val e_sube : cterm' list

   val e_subs : string list

   val e_subs : string list

   val e_subte : term list

   val e_subte : term list

   val empty_envp : envp type env = (term * term) list

   val empty_envp : envp type env = (term * term) list

   type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list

   type envp = (int * term list) list * (int * rls) list * (int * ets) list * (string * pos) list

   val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list

   val eq_tac : tac * tac -> bool type ets = (loc_ * (tac_ * env * env * term * term * safe)) list

   val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string

   val ets2s : loc_ * (tac_ * subst * subst * term * term * safe) -> string

   val ets2str : ets -> string

   val ets2str : ets -> string

   type fmz = fmz_ * spec

   type fmz = fmz_ * spec

   type fmz_ = cterm' list

   type fmz_ = cterm' list

   val g_branch : ppobj -> branch

   val g_branch : ppobj -> branch

   val g_cell : ppobj -> lrd option

   val g_cell : ppobj -> lrd option

   val g_ctxt : ppobj -> Proof.context

   val g_ctxt : ppobj -> Proof.context

   val g_domID : ppobj -> domID

   val g_domID : ppobj -> domID

   val g_env : ppobj -> (istate * Proof.context) option

   val g_env : ppobj -> (istate * Proof.context) option

   val g_fmz : ppobj -> fmz

   val g_fmz : ppobj -> fmz

   val g_form : ppobj -> term

   val g_form : ppobj -> term

   val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

   val g_loc : ppobj -> (istate * Proof.context) option * (istate * Proof.context) option

   val g_met : ppobj -> itm list

   val g_met : ppobj -> itm list

   val g_metID : ppobj -> metID

   val g_metID : ppobj -> metID

   val g_origin : ppobj -> ori list * spec * term

   val g_origin : ppobj -> ori list * spec * term

   val g_ostate : ppobj -> ostate

   val g_ostate : ppobj -> ostate

   val g_pbl : ppobj -> itm list

   val g_pbl : ppobj -> itm list

   val g_res : ppobj -> term

   val g_res : ppobj -> term

   val g_result : ppobj -> term * term list

   val g_result : ppobj -> term * term list

   val g_spec : ppobj -> spec

   val g_spec : ppobj -> spec

   val g_tac : ppobj -> tac

   val g_tac : ppobj -> tac

   val get_somespec : spec -> spec -> spec

   val get_somespec : spec -> spec -> spec

   val get_somespec' : spec -> spec -> spec

   val get_somespec' : spec -> spec -> spec

   type iist = istate option * istate option

   type iist = istate option * istate option

   val ind : pos' -> int

   val ind : pos' -> int

   val ins_nth : int -> 'a -> 'a list -> 'a list

   val ins_nth : int -> 'a -> 'a list -> 'a list

   val is_e_ctxt : Proof.context -> bool

   val is_e_ctxt : Proof.context -> bool

   val is_empty_tac : tac -> bool

   val is_empty_tac : tac -> bool

   val is_interpos : pos' -> bool

   val is_interpos : pos' -> bool

   val is_pblobj : ppobj -> bool

   val is_pblobj : ppobj -> bool

   val is_prfobj : ppobj -> bool

   val is_prfobj : ppobj -> bool

   val is_rewset : tac -> bool

   val is_rewset : tac -> bool

   val is_rewtac : tac -> bool

   val is_rewtac : tac -> bool

   val isasub2subst : term -> (term * term) list

   val isasub2subst : term -> (term * term) list

   datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate

   datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate

   val istate2str : istate -> string

   val istate2str : istate -> string

   val istates2str : istate option * istate option -> string

   val istates2str : istate option * istate option -> string

   val just_created_ : ppobj -> bool

   val just_created_ : ppobj -> bool

   val lev_back' : pos' -> pos'

   val lev_back' : pos' -> pos'

   val lev_dn : posel list -> posel list

   val lev_dn : posel list -> posel list

   val lev_dnRes : pos' -> pos'

   val lev_dnRes : pos' -> pos'

   val lev_dn_ : pos' -> pos'

   val lev_dn_ : pos' -> pos'

   val lev_of : pos' -> int

   val lev_of : pos' -> int

   val lev_on : pos -> posel list

   val lev_on : pos -> posel list

   val lev_onFrm : pos' -> pos'

   val lev_onFrm : pos' -> pos'

   val lev_pred : pos -> pos

   val lev_pred : pos -> pos

   val lev_up : pos -> pos

   val lev_up : pos -> pos

   val lev_up_ : pos' -> pos'

   val lev_up_ : pos' -> pos'

   val new_val : term -> istate -> istate

   val new_val : term -> istate -> istate

   val nth : int -> 'a list -> 'a

   val nth : int -> 'a list -> 'a

   type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

   type ocalhd = bool * pos_ * term * itm list * (bool * term) list * spec

   val ocalhd2str : ocalhd -> string

   val ocalhd2str : ocalhd -> string

   datatype ostate = Complete | Incomplete | Inconsistent

   datatype ostate = Complete | Incomplete | Inconsistent

   val ostate2str : ostate -> string

   val ostate2str : ostate -> string

   type pos = posel list

   type pos = posel list

   type pos' = pos * pos_

   type pos' = pos * pos_

   val pos's2str : (int list * pos_) list -> string

   val pos's2str : (int list * pos_) list -> string

   val pos2str : int list -> string

   val pos2str : int list -> string

   datatype pos_ = Frm | Met | Pbl | Res | Und

   datatype pos_ = Frm | Met | Pbl | Res | Und

       cell: lrd option,

       cell: lrd option,

       form: term,

       form: term,

       loc: (istate * Proof.context) option * (istate * Proof.context) option,

       loc: (istate * Proof.context) option * (istate * Proof.context) option,

       ostate: ostate, result: term * term list, tac: tac}

       ostate: ostate, result: term * term list, tac: tac}

   val pr_pos : int list -> string

   val pr_pos : int list -> string

   val pr_short : pos -> ppobj -> string

   val pr_short : pos -> ppobj -> string

   val pre_pos : pos -> pos

   val pre_pos : pos -> pos

   val preconds2str : (bool * term) list -> string

   val preconds2str : (bool * term) list -> string

   datatype ptform = Form of term | ModSpec of ocalhd

   datatype ptform = Form of term | ModSpec of ocalhd

   val rep_pblobj :

   val rep_pblobj :

      ppobj ->

      ppobj ->

      {branch: branch,

      {branch: branch,

       cell: lrd option,

       cell: lrd option,

       ctxt: Proof.context,

       ctxt: Proof.context,

   val repl_spec : spec -> ppobj -> ppobj

   val repl_spec : spec -> ppobj -> ppobj

   val repl_tac : tac -> ppobj -> ppobj

   val repl_tac : tac -> ppobj -> ppobj

   val res2str : term * term list -> string

   val res2str : term * term list -> string

   val rls_of : tac -> rls'

   val rls_of : tac -> rls'

   val rls_of_rewset : tac -> rls' * subst option

   val rls_of_rewset : tac -> rls' * subst option

   val rta2str : rule * (term * term list) -> string

   val rta2str : rule * (term * term list) -> string

   val rule2tac : theory -> (term * term) list -> rule -> tac

   val rule2tac : theory -> (term * term) list -> rule -> tac

   val safe2str : safe -> string

   val safe2str : safe -> string

   type scrstate = env * loc_ * term option * term * safe * bool

   type scrstate = env * loc_ * term option * term * safe * bool

   val scrstate2str : subst * loc_ * term option * term * safe * bool -> string

   val scrstate2str : subst * loc_ * term option * term * safe * bool -> string

      | Take' of term | Take_Inst' of term

      | Take' of term | Take_Inst' of term

   val tac_2str : tac_ -> string

   val tac_2str : tac_ -> string

   val test_trans : ppobj -> bool

   val test_trans : ppobj -> bool

   val thm_of_rew : tac -> thmID * subst option

   val thm_of_rew : tac -> thmID * subst option

   val topt2str : term option -> string

   val topt2str : term option -> string

 *)

 *)

 (**)

 (**)

 structure Ctree(**): CALC_TREEE(**) =

 structure Ctree(**): CALC_TREEE(**) =

 struct

 struct

   | str2pos_ "Res" = Res

   | str2pos_ "Res" = Res

   | str2pos_ "Und" = Und

   | str2pos_ "Und" = Und

   | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)

   | str2pos_ str = error ("str2pos_: wrong argument = " ^ str)

 type pos' = pos * pos_;

 type pos' = pos * pos_;

 	   pos : lev_on, lev_dn, lev_up, 

 	   pos : lev_on, lev_dn, lev_up, 

            lev_onFrm, lev_dnRes (..see solve Apply_Method !) 

            lev_onFrm, lev_dnRes (..see solve Apply_Method !) 

      pos_:

      pos_:

 # generate1 sets pos_ if possible  ...?WN0502?NOT...

 # generate1 sets pos_ if possible  ...?WN0502?NOT...

 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn

 # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn

   ",\n  res= " ^ term2str res ^

   ",\n  res= " ^ term2str res ^

   ",\n  " ^ safe2str s ^ "))";

   ",\n  " ^ safe2str s ^ "))";

 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;

 fun ets2str (ets: ets) = (strs2str o (map ets2s)) ets;

    (int * term list) list * (*assoc-list: args of met*)

    (int * term list) list * (*assoc-list: args of met*)

    (int * rls) list *       (*assoc-list: tacs already done ///15.9.00*)

    (int * rls) list *       (*assoc-list: tacs already done ///15.9.00*)

    (int * ets) list *       (*assoc-list: tacs etc. already done*)

    (int * ets) list *       (*assoc-list: tacs etc. already done*)

    (string * pos) list;     (*asms * from where*)

    (string * pos) list;     (*asms * from where*)

 val empty_envp = ([], [], [], []): envp; 

 val empty_envp = ([], [], [], []): envp; 

    for the first tactic in a script generating the first formula at (p,Frm);

    for the first tactic in a script generating the first formula at (p,Frm);

    this trouble has been covered by 'init_form' and 'Take' so far,

    this trouble has been covered by 'init_form' and 'Take' so far,

    but it is crucial if the first tactic in a script is eg. 'Subproblem';

    but it is crucial if the first tactic in a script is eg. 'Subproblem';

    see 'type tac ', Apply_Method.

    see 'type tac ', Apply_Method.

 .*)

 .*)

     EmptyPtree

     EmptyPtree

 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =

 fun rep_prfobj (PrfObj {cell,form,tac,loc,branch,result,ostate}) =

   {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};

   {cell=cell,form=form,tac=tac,loc=loc,branch=branch,result=result,ostate=ostate};

 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,

 fun rep_pblobj (PblObj {cell,origin,fmz,spec,probl,meth,ctxt,

       env,loc,branch,result,ostate}) =

       env,loc,branch,result,ostate}) =

 fun lev_dn_ (p, _) = (lev_dn p, Res)

 fun lev_dn_ (p, _) = (lev_dn p, Res)

 fun ind (p,_) = length p; (*WN050108 deprecated in favour of lev_of*)

 fun ind (p,_) = length p; (*WN050108 deprecated in favour of lev_of*)

 fun lev_of (p,_) = length p;

 fun lev_of (p,_) = length p;

 (* convert a pos from list to string *)

 (* convert a pos from list to string *)

 fun pr_pos ps = (space_implode "." (map string_of_int ps))^".   ";

 fun pr_pos ps = (space_implode "." (map string_of_int ps))^".   ";

 (* show hd origin or form only *)

 (* show hd origin or form only *)

 fun pr_short p (PblObj {origin = (ori,_,_),...}) = 

 fun pr_short p (PblObj {origin = (ori,_,_),...}) = 

    "\n")

    "\n")

   | pr_cell p (PrfObj {cell = c, form = form,...}) =

   | pr_cell p (PrfObj {cell = c, form = form,...}) =

   ((ints2str c) ^"   "^ (term2str form) ^ "\n");

   ((ints2str c) ^"   "^ (term2str form) ^ "\n");

 *)

 *)

   let

   let

     fun pr_pt pfn _  EmptyPtree = ""

     fun pr_pt pfn _  EmptyPtree = ""

       | pr_pt pfn ps (Nd (b, [])) = pfn ps b

       | pr_pt pfn ps (Nd (b, [])) = pfn ps b

       | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^

       | pr_pt pfn ps (Nd (b, ts)) = (pfn ps b)^

       (prts pfn ps 1 ts)

       (prts pfn ps 1 ts)

        [Nd("xx1",[]),

        [Nd("xx1",[]),

 	Nd("xx2",

 	Nd("xx2",

 	   [Nd("xx2.1.",[]),

 	   [Nd("xx2.1.",[]),

 	    Nd("xx2.2.",[])]),

 	    Nd("xx2.2.",[])]),

 	Nd("xx3",[])]);

 	Nd("xx3",[])]);

 *)

 *)

 fun ins_nth 1 e l  = e::l

 fun ins_nth 1 e l  = e::l

   | ins_nth n e [] = raise PTREE "ins_nth n e []"

   | ins_nth n e [] = raise PTREE "ins_nth n e []"

   | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);

   | ins_nth n e (l::ls) = l::(ins_nth (n-1) e ls);

 fun repl []      _ _ = raise PTREE "repl [] _ _"

 fun repl []      _ _ = raise PTREE "repl [] _ _"

   | is_interpos _ = false;

   | is_interpos _ = false;

 fun last_onlev pt pos = not (existpt (lev_on pos) pt);

 fun last_onlev pt pos = not (existpt (lev_on pos) pt);

 fun par_pblobj pt [] = []

 fun par_pblobj pt [] = []

   | par_pblobj pt p =

   | par_pblobj pt p =

     let fun par pt [] = []

     let fun par pt [] = []

 	  | par pt p = if is_pblobj (get_obj I pt p) then p

 	  | par pt p = if is_pblobj (get_obj I pt p) then p

 		       else par pt (lev_up p)

 		       else par pt (lev_up p)

 	  | par p = let val Nd (obj, children) = get_nd pt p

 	  | par p = let val Nd (obj, children) = get_nd pt p

 		    in if is_pblobj obj then (children, p) else par (lev_up p)

 		    in if is_pblobj obj then (children, p) else par (lev_up p)

 		    end;

 		    end;

     in par (lev_up p) end; 

     in par (lev_up p) end; 

 fun children (Nd (PblObj _, cn)) = cn

 fun children (Nd (PblObj _, cn)) = cn

   | children (Nd (PrfObj _, cn)) = cn;

   | children (Nd (PrfObj _, cn)) = cn;

 (*.find the next parent, which is either a PblObj (return true)

 (*.find the next parent, which is either a PblObj (return true)

     in par pt (lev_up p) end; 

     in par pt (lev_up p) end; 

 fun get_all f EmptyPtree   = []

 fun get_all f EmptyPtree   = []

   | get_all f (Nd (b, [])) = [f b]

   | get_all f (Nd (b, [])) = [f b]

   | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)

   | get_all f (Nd (b, bs)) = [f b] @ (get_alls f bs)

 and get_alls f [] = []

 and get_alls f [] = []

   | get_alls f pts = flat (map (get_all f) pts);

   | get_alls f pts = flat (map (get_all f) pts);

 covers library.ML TODO.WN110315 rename*)

 covers library.ML TODO.WN110315 rename*)

 fun insert_pt b EmptyPtree   []  = Nd (b, [])

 fun insert_pt b EmptyPtree   []  = Nd (b, [])

   | insert_pt b EmptyPtree    _        = raise PTREE "insert_pt b Empty _"

   | insert_pt b EmptyPtree    _        = raise PTREE "insert_pt b Empty _"

   | insert_pt b (Nd ( _,  _)) []       = raise PTREE "insert_pt b _ []"

   | insert_pt b (Nd ( _,  _)) []       = raise PTREE "insert_pt b _ []"

   | insert_pt b (Nd (b', bs)) (p::[])  = 

   | insert_pt b (Nd (b', bs)) (p::[])  = 

      Nd (b', repl_app bs p (Nd (b,[]))) 

      Nd (b', repl_app bs p (Nd (b,[]))) 

   | insert_pt b (Nd (b', bs)) (p::ps)  =

   | insert_pt b (Nd (b', bs)) (p::ps)  =

      Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));

      Nd (b', repl_app bs p (insert_pt b (nth p bs) ps));

 (*

 (*

 > type ppobj = string;

 > type ppobj = string;

 (*val pt = Unsynchronized.ref Empty;*)

 (*val pt = Unsynchronized.ref Empty;*)

   pt:= insert_pt ("root'":ppobj) EmptyPtree [];

   pt:= insert_pt ("root'":ppobj) EmptyPtree [];

   pt:= insert_pt ("xx1":ppobj) (!pt) [1];

   pt:= insert_pt ("xx1":ppobj) (!pt) [1];

   pt:= insert_pt ("xx2":ppobj) (!pt) [2];

   pt:= insert_pt ("xx2":ppobj) (!pt) [2];

   pt:= insert_pt ("xx3":ppobj) (!pt) [3];

   pt:= insert_pt ("xx3":ppobj) (!pt) [3];

 datatype ptform = Form of term | ModSpec of ocalhd;

 datatype ptform = Form of term | ModSpec of ocalhd;

 val e_ptform = Form e_term;

 val e_ptform = Form e_term;

 val e_ptform' = ModSpec e_ocalhd;

 val e_ptform' = ModSpec e_ocalhd;

 (*.applies (snd f) to the branches at a pos if ((fst f) b),

 (*.applies (snd f) to the branches at a pos if ((fst f) b),

 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)

 fun appl_branch f EmptyPtree [] = (EmptyPtree, false)

   | appl_branch f EmptyPtree _  = raise PTREE "appl_branch f Empty _"

   | appl_branch f EmptyPtree _  = raise PTREE "appl_branch f Empty _"

   | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"

   | appl_branch f (Nd ( _, _)) [] = raise PTREE "appl_branch f _ []"

   | appl_branch f (Nd (b, bs)) (p::[]) = 

   | appl_branch f (Nd (b, bs)) (p::[]) = 

 >  posless [6] [6,5,2];

 >  posless [6] [6,5,2];

 true

 true

 +++ see Isabelle/../library.ML*)

 +++ see Isabelle/../library.ML*)

 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo

 (*WN0510 version stopped in favour of get_interval with !!!move_dn, getFormulaeFromTo

   actually used (inefficient) version with move_dn: see modspec.sml*)

   actually used (inefficient) version with move_dn: see modspec.sml*)

 local

 local

   | getnds i _ (b,p) q (nd::(nds as _::_)) =       (*intern, ...*)

   | getnds i _ (b,p) q (nd::(nds as _::_)) =       (*intern, ...*)

     (getnd i             (       b,[0]) [99999] nd) @

     (getnd i             (       b,[0]) [99999] nd) @

     (getnds ~99999 false (lev_on b,[0]) q nds); 

     (getnds ~99999 false (lev_on b,[0]) q nds); 

 in

 in

   where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)

   where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)

 (1) the 'f' are given 

 (1) the 'f' are given 

 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)

 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)

 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)

 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)

 (2) the 't' ar given

 (2) the 't' ar given

     let val domID = if dI = e_domID then dI' else dI

     let val domID = if dI = e_domID then dI' else dI

 	val pblID = if pI = e_pblID then pI' else pI

 	val pblID = if pI = e_pblID then pI' else pI

 	val metID = if mI = e_metID then mI' else mI

 	val metID = if mI = e_metID then mI' else mI

     in (domID, pblID, metID) end;

     in (domID, pblID, metID) end;

 fun preconds2str bts = 

 fun preconds2str bts = 

     (strs2str o (map (linefeed o pair2str o

     (strs2str o (map (linefeed o pair2str o

 		      (apsnd term2str) o 

 		      (apsnd term2str) o 

 		      (apfst bool2str)))) bts;

 		      (apfst bool2str)))) bts;

 fun ocalhd2str (b, p, hdf, itms, prec, spec) =

 fun ocalhd2str (b, p, hdf, itms, prec, spec) =

 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;

 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~##################

 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)

 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)

 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);

 (* val (Nd (c, ns), ([],p_)) = (pt, get_pos cI uI);

    *)

    *)

     if is_pblobj c 

     if is_pblobj c 

 				    then (P@[p+1], Res)

 				    then (P@[p+1], Res)

 				    else (P@[p+1,1], Frm)(*040221*)

 				    else (P@[p+1,1], Frm)(*040221*)

 			       else (P@[p+1], if is_pblnd (nth (p+1) ns) 

 			       else (P@[p+1], if is_pblnd (nth (p+1) ns) 

 					      then Pbl else Frm); 

 					      then Pbl else Frm); 

 *)

 *)

    move_dn at the end of the calc-tree raises PTREE.*)

    move_dn at the end of the calc-tree raises PTREE.*)

 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)

 fun move_dn _ (Nd (c, ns)) ([],p_) = (*root problem*)

     (case p_ of 

     (case p_ of 

 	     Res => raise PTREE "move_dn: end of calculation"

 	     Res => raise PTREE "move_dn: end of calculation"

 	   | _ => if null ns (*go down from Pbl + Met*)

 	   | _ => if null ns (*go down from Pbl + Met*)

 	     else (P @ [p, 1], 

 	     else (P @ [p, 1], 

 		   if (is_pblnd o hd o children o (nth p)) ns

 		   if (is_pblnd o hd o children o (nth p)) ns

 		   then Pbl else Frm);

 		   then Pbl else Frm);

 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)

 fun movelevel_dn [] (Nd (c, ns)) ([],p_) = (*root problem*)

     if is_pblobj c 

     if is_pblobj c 

     then if null ns 

     then if null ns 

 	 then raise PTREE "solve problem not started"

 	 then raise PTREE "solve problem not started"

 	 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)

 	 else ([1], if (is_pblnd o hd) ns then Pbl else Frm)

 			  if (is_pblnd o hd o children o (nth p)) ns

 			  if (is_pblnd o hd o children o (nth p)) ns

 			  then Pbl else Frm);

 			  then Pbl else Frm);

 fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*)

 fun move_up _ (Nd (c, ns)) ([],p_) = (*root problem*)

     if is_pblobj c 

     if is_pblobj c 

     then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)

     then case p_ of Res => if null ns then ([], Pbl) (*Res -> Pbl (not Met)!*)

 			   else ([length ns], Res)

 			   else ([length ns], Res)

 		  | _  => raise PTREE "begin of calculation"

 		  | _  => raise PTREE "begin of calculation"

 			    then (P@[p-1], Res) else (P@[p], Frm)

 			    then (P@[p-1], Res) else (P@[p], Frm)

 		       else (P @ [p, nc], Res) end; (*go down*)

 		       else (P @ [p, nc], Res) end; (*go down*)

 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)

 fun movelevel_up _ (Nd (c, ns)) (([],p_):pos') = (*root problem*)

     raise PTREE "pos not existent"

     raise PTREE "pos not existent"

   (*iterate towards end of pos*)

   (*iterate towards end of pos*)

   | movelevel_up P  (Nd (_, ns)) (p::(ps as (_::_)),p_) = 

   | movelevel_up P  (Nd (_, ns)) (p::(ps as (_::_)),p_) = 

 (**.insert into ctree and cut branches accordingly.**)

 (**.insert into ctree and cut branches accordingly.**)

 (*.get all positions of certain intervals on the ctree.*)

 (*.get all positions of certain intervals on the ctree.*)

 (*OLD VERSION without move_dn; kept for occasional redesign

 (*OLD VERSION without move_dn; kept for occasional redesign

 fun get_allpos' (_:pos, _:posel) EmptyPtree   = ([]:pos' list)

 fun get_allpos' (_:pos, _:posel) EmptyPtree   = ([]:pos' list)

   | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)

   | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)

     if g_ostate b = Incomplete 

     if g_ostate b = Incomplete 

     then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)

     then ((*tracing("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)

 	  [(p,Frm)] @ (get_allpos's (p, 1) bs)

 	  [(p,Frm)] @ (get_allpos's (p, 1) bs)

 (*.cut branches.*)

 (*.cut branches.*)

 (*before WN041019......

 (*before WN041019......

 val cut_branch = (test_trans, curry take):

 val cut_branch = (test_trans, curry take):

 .. formlery used for ...

 .. formlery used for ...

 fun cut_tree''' _ [] = EmptyPtree

 fun cut_tree''' _ [] = EmptyPtree

   | cut_tree''' pt pos = 

   | cut_tree''' pt pos = 

   let val (pt',cut) = appl_branch cut_branch pt pos

   let val (pt',cut) = appl_branch cut_branch pt pos

   in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)

   in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)

 		     then [] else [([], Res)])) end;

 		     then [] else [([], Res)])) end;

 (*########/ inserted from ctreeNEW.sml \#################################**)

 (*########/ inserted from ctreeNEW.sml \#################################**)

 val get_allp = fn : 

 val get_allp = fn : 

   pos' list -> : accumulated, start with []

   pos' list -> : accumulated, start with []

   pos ->       : the offset for subtrees wrt the root

   pos ->       : the offset for subtrees wrt the root

   pos'         : initialization (the last pos' before ...)

   pos'         : initialization (the last pos' before ...)

   -> pos' list : of positions in this (sub) tree (relative to the root)

   -> pos' list : of positions in this (sub) tree (relative to the root)

 .*)

 .*)

 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');

 (* val (cuts, P, pt, pos) = ([], [3], get_nd pt [3], ([], Frm):pos');

    val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');

    val (cuts, P, pt, pos) = ([], [2], get_nd pt [2], ([], Frm):pos');

 val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)

 val cutlevup = test_trans;(*WN060727 after summerterm tests.LK0502 withdrawn*)

 (*cut_bottom new sml603..608

 (*cut_bottom new sml603..608

 cut the level at the bottom of the pos (used by cappend_...)

 cut the level at the bottom of the pos (used by cappend_...)

 and handle the parent in order to avoid extra case for root

 and handle the parent in order to avoid extra case for root

     pos * posel ->   : the pos after split_last

     pos * posel ->   : the pos after split_last

 return

 return

      pos' list) *    : the pos's cut

      pos' list) *    : the pos's cut

      bool            : cutting shall be continued on the higher level(s)

      bool            : cutting shall be continued on the higher level(s)

 *)

 *)

 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)

 fun cut_bottom _ (pt' as Nd (b, [])) = ((pt', []), cutlevup b)

   | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =

   | cut_bottom (P:pos, p:posel) (Nd (b, bs)) =

 (*.go all levels from the bottom of 'pos' up to the root, 

 (*.go all levels from the bottom of 'pos' up to the root, 

  on each level compose the children of a node and accumulate the cut Nds

  on each level compose the children of a node and accumulate the cut Nds

 args

 args

    pos' list ->      : for accumulation

    pos' list ->      : for accumulation

    bool -> 	     : cutting shall be continued on the higher level(s)

    bool -> 	     : cutting shall be continued on the higher level(s)

    pos * posel ->    : pos=path split for convenience

    pos * posel ->    : pos=path split for convenience

 returns		     :

 returns		     :

 .*)

 .*)

 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =

 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =

     let (*divide level into 3 parts...*)

     let (*divide level into 3 parts...*)

 	val keep = take (p - 1, bs)

 	val keep = take (p - 1, bs)

 	(*val pt' comes as argument from below*)

 	(*val pt' comes as argument from below*)