(* tools for rewriting, reverse rewriting, context to thy concerning rewriting

    authors: Walther Neuper 2002, 2006

   (c) due to copyright terms

 use"ME/rewtools.sml";

 use"rewtools.sml";

 *)

 (***.reverse rewriting.***)

 (*.derivation for insertin one level of nodes into the calctree.*)

 type deriv  = (term * rule * (term *term list)) list;

 fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str' r)^", ("^

 			    (term2str t')^", "^(terms2str a)^"))";

 fun trtas2str trtas = (strs2str o (map trta2str)) trtas;

 val deriv2str = trtas2str;

 fun rta2str (r,(t,a)) = "\n("^(rule2str' r)^", ("^

 			    (term2str t)^", "^(terms2str a)^"))";

 fun rtas2str rtas = (strs2str o (map rta2str)) rtas;

 val deri2str = rtas2str;

 (*.A1==>...==>An==>(Lhs = Rhs) goes to A1==>...==>An==>(Rhs = Lhs).*)

 fun sym_thm thm =

     let 

         val (deriv, {thy_ref = thy_ref, tags = tags, maxidx = maxidx, 

                      shyps = shyps, hyps = hyps, tpairs = tpairs, 

                      prop = prop}) = 

 	    rep_thm_G thm;

         val (lhs,rhs) = (dest_equals' o strip_trueprop 

 		         o Logic.strip_imp_concl) prop;

         val prop' = case strip_imp_prems' prop of

 		        NONE => Trueprop $ (mk_equality (rhs, lhs))

 		      | SOME cs => 

 		        ins_concl cs (Trueprop $ (mk_equality (rhs, lhs)));

     in assbl_thm deriv thy_ref tags maxidx shyps hyps tpairs prop' end;

 (*

   (sym RS real_mult_div_cancel1) handle e => print_exn e;

 Exception THM 1 raised:

 RSN: no unifiers

 "?s = ?t ==> ?t = ?s"

 "?k ~= 0 ==> ?k * ?m / (?k * ?n) = ?m / ?n"

   val thm = real_mult_div_cancel1;

   val prop = (#prop o rep_thm) thm;

   atomt prop;

   val ppp = Logic.strip_imp_concl prop;

   atomt ppp;

   ((#prop o rep_thm o sym_thm o sym_thm) thm) = (#prop o rep_thm) thm;

 val it = true : bool

   ((sym_thm o sym_thm) thm) = thm;

 val it = true : bool

   val thm = real_le_anti_sym;

   ((sym_thm o sym_thm) thm) = thm;

 val it = true : bool

   val thm = real_minus_zero;

   ((sym_thm o sym_thm) thm) = thm;

 val it = true : bool

 *)

 (*.derive normalform of a rls, or derive until SOME goal,

    and record rules applied and rewrites.

 val it = fn

   : theory

     -> rls

     -> rule list

     -> rew_ord       : the order of this rls, which 1 theorem of is used 

                        for rewriting 1 single step (?14.4.03)

     -> term option   : 040214 ??? nonsense ??? 

     -> term 

     -> (term *       : to this term ...

         rule * 	     : ... this rule is applied yielding ...

         (term *      : ... this term ...

          term list)) : ... under these assumptions.

        list          :

 returns empty list for a normal form

 FIXME.WN040214: treats rules as in Rls, _not_ as in Seq

 WN060825 too complicated for the intended use by cancel_, common_nominator_

 and unreflectedly adapted to extion of rules by Rls_: returns Rls_("sym_simpl..

  -- replaced below*)

 (* val (thy, erls, rs, ro, goal, tt) = (thy, erls, rs, ro, goal, t);

    val (thy, erls, rs, ro, goal, tt) = (thy, Atools_erls, rules, ro, NONE, tt);

    *)

 fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt = 

     let datatype switch = Appl | Noap

 	fun rew_once lim rts t Noap [] = 

 	    (case goal of 

 		 NONE => rts

 	       | SOME g => 

 		 raise error ("make_deriv: no derivation for "^(term2str t)))

 	  | rew_once lim rts t Appl [] = 

 	    (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs

 	  (*| Seq _ => rts) FIXXXXXME 14.3.03*)

 	  | rew_once lim rts t apno rs' =

 	    (case goal of 

 		 NONE => rew_or_calc lim rts t apno rs'

 	       | SOME g =>

 		 if g = t then rts

 		 else rew_or_calc lim rts t apno rs')

 	and rew_or_calc lim rts t apno (rrs' as (r::rs')) =

 	    if lim < 0 

 	    then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^

 			   "with deriv =\n"); writeln (deriv2str rts); rts)

 	    else

 	    case r of

 		Thm (thmid, tm) =>

 		(if not (!trace_rewrite) then () else

 		 writeln ("### trying thm '" ^ thmid ^ "'");

 		 case rewrite_ thy ro erls true tm t of

 		     NONE => rew_once lim rts t apno rs'

 		   | SOME (t',a') =>

 		     (if ! trace_rewrite 

 		      then writeln ("### rewrites to: "^(term2str t')) else();

 		      rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))

 	      | Calc (c as (op_,_)) => 

 		let val _ = if not (!trace_rewrite) then () else

 			    writeln ("### trying calc. '" ^ op_ ^ "'")

 		    val t = uminus_to_string t

 		in case get_calculation_ thy c t of

 		       NONE => rew_once lim rts t apno rs'

 		     | SOME (thmid, tm) => 

 		       (let val SOME (t',a') = rewrite_ thy ro erls true tm t

 			    val _ = if not (!trace_rewrite) then () else

 				    writeln("### calc. to: " ^ (term2str t'))

 			    val r' = Thm (thmid, tm)

 			in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'

 			end) 

 		       handle _ => raise error "derive_norm, Calc: no rewrite"

 		end

 (* TODO.WN080222: see rewrite__set_

    @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

       | Cal1 (cc as (op_,_)) => 

 	  (let val _= if !trace_rewrite andalso i < ! depth then

 		      writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();

 	     val ct = uminus_to_string ct

 	   in case get_calculation_ thy cc ct of

 	     NONE => (ct, asm)

 	   | SOME (thmid, thm') =>

 	       let 

 		 val pairopt = 

 		   rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)

 		   ((#erls o rep_rls) rls) put_asm thm' ct;

 		 val _ = if pairopt <> NONE then () 

 			 else raise error("rewrite_set_, rewrite_ \""^

 			 (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")

 		 val _ = if ! trace_rewrite andalso i < ! depth 

 			   then writeln((idt"="(i+1))^" cal1. to: "^

 					(term2str ((fst o the) pairopt)))

 			 else()

 	       in the pairopt end

 	   end)

 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)

 	      | Rls_ rls => 

 		(case rewrite_set_ thy true rls t of

 		     NONE => rew_once lim rts t apno rs'

 		   | SOME (t',a') =>

 		     rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');

 (*WN060829    | Rls_ rls => 

 		(case rewrite_set_ thy true rls t of

 		     NONE => rew_once lim rts t apno rs'

 		   | SOME (t',a') =>

 		     if ro [] (t, t') then rew_once lim rts t apno rs'

 		     else rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs');

 ...lead to deriv = [] with make_polynomial.

 THERE IS SOMETHING DIFFERENT beetween rewriting with the code above

 and between rewriting with rewrite_set: with rules from make_polynomial and 

 t = "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)" the actual code

 leads to cycling  Rls_ order_mult_rls_..Rls_ discard_parentheses_..Rls_ order..

 *)

     in rew_once (!lim_deriv) [] tt Noap rs end;

 (*.toggles the marker for 'fun sym_thm'.*)

 fun sym_thmID (thmID : thmID) =

     case explode thmID of

 	"s"::"y"::"m"::"_"::id => implode id : thmID

       | id => "sym_"^thmID;

 (* 

 > val thmID = "sym_real_mult_2";

 > sym_thmID thmID;

 val it = "real_mult_2" : string

 > val thmID = "real_num_collect";

 > sym_thmID thmID;

 val it = "sym_real_num_collect" : string*)

 fun sym_drop (thmID : thmID) =

     case explode thmID of

 	"s"::"y"::"m"::"_"::id => implode id : thmID

       | id => thmID;

 fun is_sym (thmID : thmID) =

     case explode thmID of

 	"s"::"y"::"m"::"_"::id => true

       | id => false;

 (*FIXXXXME.040219: detail has to handle Rls id="sym_..." 

   by applying make_deriv, rev_deriv'; see concat_deriv*)

 fun sym_rls Erls = Erls

   | sym_rls (Rls {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =

     Rls {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls, 

 	 rules=rules, rew_ord=rew_ord, preconds=preconds}

   | sym_rls (Seq {id, scr, calc, erls, srls, rules, rew_ord, preconds}) =

     Seq {id="sym_"^id, scr=scr, calc=calc, erls=erls, srls=srls, 

 	 rules=rules, rew_ord=rew_ord, preconds=preconds}

   | sym_rls (Rrls {id, scr, calc, erls, prepat, rew_ord}) = 

     Rrls {id="sym_"^id, scr=scr, calc=calc, erls=erls, prepat=prepat, 

 	  rew_ord=rew_ord};

 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm)

   | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)

   | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));

 (*

   val th =  Thm ("real_one_collect",num_str real_one_collect);

   sym_Thm th;

 val th =

   Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")

   : rule

 ML> val it =

   Thm ("sym_real_one_collect","?m is_const ==> (1 + ?m) * ?n = ?n + ?m * ?n")*)

 (*version for reverse rewrite used before 040214*)

 fun rev_deriv (t, r, (t', a)) = (sym_Thm r, (t, a));

 (* val (thy, erls, rs, ro, goal, t) = (thy, eval_rls, rules, ro, NONE, t');

    *)

 fun reverse_deriv thy erls (rs:rule list) ro(*rew_ord*) goal t =

     (rev o (map rev_deriv)) (make_deriv thy erls (rs:rule list) ro goal t);

 (*

   val rev_rew = reverse_deriv thy e_rls ; 

   writeln(rtas2str rev_rew);

 *)

 fun eq_Thm (Thm (id1,_), Thm (id2,_)) = id1 = id2

   | eq_Thm (Thm (id1,_), _) = false

   | eq_Thm (Rls_ r1, Rls_ r2) = id_rls r1 = id_rls r2

   | eq_Thm (Rls_ r1, _) = false

   | eq_Thm (r1, r2) = raise error ("eq_Thm: called with '"^

 				(rule2str r1)^"' '"^(rule2str r2)^"'");

 fun distinct_Thm r = gen_distinct eq_Thm r;

 fun eq_Thms thmIDs thm = (member op = thmIDs (id_of_thm thm))

     handle _ => false;

 (***. context to thy concerning rewriting .***)

 (*.create the unique handles and filenames for the theory-data.*)

 fun part2guh ([str]:theID) =

     (case str of

 	"Isabelle" => "thy_isab_" ^ str ^ "-part" : guh

       | "IsacScripts" => "thy_scri_" ^ str ^ "-part"

       | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"

       | str => raise error ("thy2guh: called with '"^str^"'"))

   | part2guh theID = raise error ("part2guh called with theID = "

 				  ^ theID2str theID);

 fun part2filename str = part2guh str ^ ".xml" : filename;

 fun thy2guh ([part, thyID]:theID) =

     (case part of

 	"Isabelle" => "thy_isab_" ^ thyID : guh

       | "IsacScripts" => "thy_scri_" ^ thyID

       | "IsacKnowledge" => "thy_isac_" ^ thyID

       | str => raise error ("thy2guh: called with '"^str^"'"))

   | thy2guh theID = raise error ("thy2guh called with '"^strs2str' theID^"'");

 fun thy2filename thy' = thy2guh thy' ^ ".xml" : filename;

 fun thypart2guh ([part, thyID, thypart]:theID) = 

     case part of

 	"Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : guh

       | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart

       | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart

       | str => raise error ("thypart2guh: called with '"^str^"'");

 fun thypart2filename thy' = thypart2guh thy' ^ ".xml" : filename;

 (*.convert the data got via contextToThy to a globally unique handle

    there is another way to get the guh out of the 'theID' in the hierarchy.*)

 fun thm2guh (isa, thyID:thyID) (thmID:thmID) =

     case isa of

 	"Isabelle" => 

 	"thy_isab_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh

     | "IsacKnowledge" =>

 	"thy_isac_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID

     | "IsacScripts" =>

 	"thy_scri_" ^ theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID

     | str => raise error ("thm2guh called with isa = '"^isa^

 			  "' for thm = "^thmID^"'");

 fun thm2filename (isa_thyID: string * thyID) thmID =

     (thm2guh isa_thyID thmID) ^ ".xml" : filename;

 fun rls2guh (isa, thyID:thyID) (rls':rls') =

     case isa of

 	"Isabelle" => 

 	    "thy_isab_" ^ theory'2thyID thyID ^ "-rls-" ^ rls' : guh

     | "IsacKnowledge" =>

 	    "thy_isac_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'

     | "IsacScripts" =>

 	    "thy_scri_" ^ theory'2thyID thyID ^ "-rls-" ^ rls'

     | str => raise error ("rls2guh called with isa = '"^isa^

 			  "' for rls = '"^rls'^"'");

 	fun rls2filename (isa, thyID) rls' =

     rls2guh (isa, thyID) rls' ^ ".xml" : filename;

 fun cal2guh (isa, thyID:thyID) calID =

     case isa of

 	"Isabelle" => 

 	"thy_isab_" ^ theory'2thyID thyID ^ "-cal-" ^ calID : guh

       | "IsacKnowledge" =>

 	"thy_isac_" ^ theory'2thyID thyID ^ "-cal-" ^ calID

       | "IsacScripts" =>

 	"thy_scri_" ^ theory'2thyID thyID ^ "-cal-" ^ calID

       | str => raise error ("cal2guh called with isa = '"^isa^

 			  "' for cal = '"^calID^"'");

 fun cal2filename (isa, thyID:thyID) calID = 

     cal2guh (isa, thyID:thyID) calID ^ ".xml" : filename;

 fun ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') =

     case isa of

 	"Isabelle" => 

 	"thy_isab_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh

       | "IsacKnowledge" =>

 	"thy_isac_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'

       | "IsacScripts" =>

 	"thy_scri_" ^ theory'2thyID thyID ^ "-ord-" ^ rew_ord'

       | str => raise error ("ord2guh called with isa = '"^isa^

 			  "' for ord = '"^rew_ord'^"'");

 fun ord2filename (isa, thyID:thyID) (rew_ord':rew_ord') =

     ord2guh (isa, thyID:thyID) (rew_ord':rew_ord') ^ ".xml" : filename;

 (**.set up isab_thm_thy in Isac.ML.**)

 fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));

 fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));

 (*.lookup the missing theorems in some thy (of Isabelle).*)

 fun make_isa missthms thy =

     map (pair (theory2thyID thy)) 

 	((inter eq_thmI) missthms (PureThy.all_thms_of thy))

 	: (thyID * (thmID * Thm.thm)) list;

 (*.separate handling of sym_thms.*)

 fun make_isab rlsthmsNOTisac isab_thys = 

     let fun les ((s1,_), (s2,_)) = (s1 : string) < s2

 	val notsym = filter_out (is_sym o #1) rlsthmsNOTisac

 	val notsym_isab = (flat o (map (make_isa notsym))) isab_thys

 	val sym = filter (is_sym o #1) rlsthmsNOTisac

 	val symsym = map ((apfst sym_drop) o (apsnd sym_thm)) sym

 	val symsym_isab = (flat o (map (make_isa symsym))) isab_thys

 	val sym_isab = map (((apsnd o apfst) sym_drop) o 

 			    ((apsnd o apsnd) sym_thm)) symsym_isab

 	val isab = notsym_isab @ symsym_isab @ sym_isab

     in ((map rearrange) o (gen_sort les)) isab 

        : (thmID * (thyID * Thm.thm)) list

     end;

 (*.which theory below thy' contains a theorem; this can be in isabelle !

 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)

 (* val (str, (_, thy)) = ("real_diff_minus", ("Root.thy", Root.thy));

    val (str, (_, thy)) = ("real_diff_minus", ("Poly.thy", Poly.thy));

    *)

 fun thy_contains_thm (str:xstring) (_, thy) = 

     member op = (map (strip_thy o fst) (PureThy.all_thms_of thy)) str;

 (* val (thy', str) = ("Isac.thy", "real_mult_minus1");

    val (thy', str) = ("PolyMinus.thy", "klammer_minus_plus");

    *)

 fun thy_containing_thm (thy':theory') (str:xstring) =

     let val thy' = thyID2theory' thy'

 	val str = sym_drop str

 	val startsearch = dropuntil ((curry op= thy') o 

 				     (#1:theory' * theory -> theory')) 

 				    (rev (!theory'))

     in case find_first (thy_contains_thm str) startsearch of

 	   SOME (thy',_) => ("IsacKnowledge", thy')

 	 | NONE => (case assoc (!isab_thm_thy (*see Isac.ML*), str) of

 		     SOME (thyID,_) => ("Isabelle", thyID)

 		   | NONE => 

 		     raise error ("thy_containing_thm: theorem '"^str^

 				  "' not in !theory' above thy '"^thy'^"'"))

     end;

 (*.which theory below thy' contains a ruleset;

 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)

 (* val (thy', rls') = ("PolyEq.thy", "separate_bdv");

    *)

 local infix mem; (*from Isabelle2002*)

 fun x mem [] = false

   | x mem (y :: ys) = x = y orelse x mem ys;

 in

 fun thy_containing_rls (thy':theory') (rls':rls') =

     let val rls' = strip_thy rls'

 	val thy' = thyID2theory' thy'

 	(*take thys between "Isac" and thy' not to search #1#*)

 	val dropthys = takewhile [] (not o (curry op= thy') o 

 				     (#1:theory' * theory -> theory')) 

 				 (rev (!theory'))

 	val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))

 			    dropthys

 	(*drop those rulesets which are generated in a theory found in #1#*)

 	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o

 				      ((#1 o #2) : rls' * (theory' * rls) 

 						   -> theory'))

 				     (rev (!ruleset'))

     in case assoc (startsearch, rls') of

 	   SOME (thy', _) => ("IsacKnowledge", thyID2theory' thy')

 	 | _ => raise error ("thy_containing_rls : rls '"^rls'^

 			     "' not in !rulset' above thy '"^thy'^"'")

     end;

 (* val (thy', termop) = (thyID, termop);

    *)

 fun thy_containing_cal (thy':theory') termop =

     let val thy' = thyID2theory' thy'

 	val dropthys = takewhile [] (not o (curry op= thy') o 

 				     (#1:theory' * theory -> theory')) 

 				 (rev (!theory'))

 	val dropthy's = map (get_thy o (#1 : (theory' * theory) -> theory'))

 			    dropthys

 	val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o

 				      (#1 : calc -> string)) (rev (!calclist'))

     in case assoc (startsearch, strip_thy termop) of

 	   SOME (th_termop, _) => ("IsacKnowledge", strip_thy th_termop)

 	 | _ => raise error ("thy_containing_rls : rls '"^termop^

 			     "' not in !calclist' above thy '"^thy'^"'")

     end

 end;

 (* print_depth 99; map #1 startsearch; print_depth 3;

    *)

 (*.packing return-values to matchTheory, contextToThy for xml-generation.*)

 datatype contthy =  (*also an item from KEStore on Browser ......#*)

 	 EContThy   (*not from KEStore ...........................*)

        | ContThm of (*a theorem in contex =============*)

 	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)

 	  thm     : guh,           (*theorem in the context      .*)

 	  applto  : term,	   (*applied to formula ...      .*)

 	  applat  : term,	   (*...  with lhs inserted      .*)

 	  reword  : rew_ord',      (*order used for rewrite      .*)

 	  asms    : (term          (*asumption instantiated      .*)

 		     * term) list, (*asumption evaluated         .*)

 	  lhs     : term           (*lhs of the theorem ...      #*)

 		    * term,        (*... instantiated            .*)

 	  rhs     : term           (*rhs of the theorem ...      #*)

 		    * term,        (*... instantiated            .*)

 	  result  : term,	   (*resulting from the rewrite  .*)

 	  resasms : term list,     (*... with asms stored        .*)

 	  asmrls  : rls'           (*ruleset for evaluating asms .*)

 		    }						 

 	| ContThmInst of (*a theorem with bdvs in contex ======== *)

 	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)

 	  thm     : guh,           (*theorem in the context      .*)

 	  bdvs    : subst,         (*bound variables to modify....*)

 	  thminst : term,          (*... theorem instantiated    .*)

 	  applto  : term,	   (*applied to formula ...      .*)

 	  applat  : term,	   (*...  with lhs inserted      .*)

 	  reword  : rew_ord',      (*order used for rewrite      .*)

 	  asms    : (term          (*asumption instantiated      .*)

 		     * term) list, (*asumption evaluated         .*)

 	  lhs     : term           (*lhs of the theorem ...      #*)

 		    * term,        (*... instantiated            .*)

 	  rhs     : term           (*rhs of the theorem ...      #*)

 		    * term,        (*... instantiated            .*)

 	  result  : term,	   (*resulting from the rewrite  .*)

 	  resasms : term list,     (*... with asms stored        .*)

 	  asmrls  : rls'           (*ruleset for evaluating asms .*)

 		      }						 

 	| ContRls of (*a rule set in contex ===================== *)

 	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)

 	  rls     : guh,           (*rule set in the context     .*)

 	  applto  : term,	   (*rewrite this formula        .*)

 	  result  : term,	   (*resulting from the rewrite  .*)

 	  asms    : term list      (*... with asms stored        .*)

 		    }						 

 	| ContRlsInst of (*a rule set with bdvs in contex ======= *)

 	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)

 	  rls     : guh,           (*rule set in the context     .*)

 	  bdvs    : subst,         (*for bound variables in thms .*)

 	  applto  : term,	   (*rewrite this formula        .*)

 	  result  : term,	   (*resulting from the rewrite  .*)

 	  asms    : term list      (*... with asms stored        .*)

 		    }

 	| ContNOrew of (*no rewrite for thm or rls ============== *)

 	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)

 	  thm_rls : guh,           (*thm or rls in the context   .*)

 	  applto  : term	   (*rewrite this formula        .*)

 		    }						 

 	| ContNOrewInst of (*no rewrite for some instantiation == *)

 	 {thyID   : thyID,         (*for *2guh in sub-elems here .*)

 	  thm_rls : guh,           (*thm or rls in the context   .*)

 	  bdvs    : subst,         (*for bound variables in thms .*)

 	  thminst : term,          (*... theorem instantiated    .*)

 	  applto  : term	   (*rewrite this formula        .*)

 		    };

 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718

    pass other tacs unchanged.*)

 fun get_tac_checked pt ((p,p_) : pos') = get_obj g_tac pt p;

 (*..*)

 (*.get the formula f at ptp rewritten by the Rewrite_* already applied to f.*)

 (* val (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) = tac';

    *)

 fun context_thy (pt, pos as (p,p_)) (tac as Rewrite (thmID,_)) = 

     (case applicable_in pos pt tac of

 	Appl (Rewrite' (thy', ord', erls, _, (thmID,_), f, (res,asm))) =>

 	let val thy = assoc_thy thy'

 	    val thm = (norm o #prop o rep_thm o (PureThy.get_thm thy)) thmID

     (*WN060616 the following must be done on subterm found _IN_ rew_sub

 	val (lhs,rhs) = (dest_equals' o strip_trueprop 

 			 o Logic.strip_imp_concl) thm

 	val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)

 	val thm' = ren_inst (insts, thm, lhs, f)

 	val (lhs',rhs') = (dest_equals' o strip_trueprop 

 			   o Logic.strip_imp_concl) thm'

 	val asms = map strip_trueprop (Logic.strip_imp_prems thm)

 	val asms' = map strip_trueprop (Logic.strip_imp_prems thm')

      *)

 	in ContThm {thyID   = theory'2thyID thy',

 		    thm     = thm2guh (thy_containing_thm thy' thmID) thmID,

 		    applto  = f,

 		    applat  = e_term,

 		    reword  = ord',

 		    asms    = [](*asms ~~ asms'*),

 		    lhs     = (e_term, e_term)(*(lhs, lhs')*),

 		    rhs     = (e_term, e_term)(*(rhs, rhs')*),

 		    result  = res,

 		    resasms = asm,

 		    asmrls  = id_rls erls}

 	end

       | Notappl _ =>

 	let val pp = par_pblobj pt p

 	    val 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

 	in ContNOrew {thyID   = theory'2thyID thy',

 		    thm_rls = thm2guh (thy_containing_thm thy' thmID) thmID,

 		      applto = f}

 	end)

 (* val ((pt,p), tac as Rewrite_Inst (subs, (thmID,_))) = ((pt,pos), tac);

    *)

       | context_thy (pt, pos as (p,p_)) 

 		    (tac as Rewrite_Inst (subs, (thmID,_))) =

 	(case applicable_in pos pt tac of

 (* val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), 

 			    f, (res,asm))) = applicable_in p pt tac;

    *)

 	     Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), 

 				  f, (res,(*path to subterm,*)asm))) =>

 	     let val thm = (norm o #prop o rep_thm o 

 			    (PureThy.get_thm (assoc_thy thy'))) thmID

 	    val thminst = inst_bdv subst thm

     (*WN060616 the following must be done on subterm found _IN_ rew_sub

 	val (lhs,rhs) = (dest_equals' o strip_trueprop 

 			 o Logic.strip_imp_concl) thminst

 	val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs, f)

 	val thm' = ren_inst (insts, thminst, lhs, f)

 	val (lhs',rhs') = (dest_equals' o strip_trueprop 

 			   o Logic.strip_imp_concl) thm'

 	val asms = map strip_trueprop (Logic.strip_imp_prems thminst)

 	val asms' = map strip_trueprop (Logic.strip_imp_prems thm')

      *)

 	     in ContThmInst {thyID   = theory'2thyID thy',

 		    thm     = thm2guh (thy_containing_thm 

 						    thy' thmID) thmID,

 			     bdvs    = subst,

 			     thminst = thminst,

 			     applto  = f,

 			     applat  = e_term,

 			     reword  = ord',

 			     asms    = [](*asms ~~ asms'*),

 			     lhs     = (e_term, e_term)(*(lhs, lhs')*),

 			     rhs     = (e_term, e_term)(*(rhs, rhs')*),

 			     result  = res,

 			     resasms = asm,

 			     asmrls  = id_rls erls}

 	     end

       | Notappl _ =>

 	let val pp = par_pblobj pt p

 	    val thy' = get_obj g_domID pt pp

 	    val subst = subs2subst (assoc_thy thy') subs

 	    val thm = (norm o #prop o rep_thm o 

 			    (PureThy.get_thm (assoc_thy thy'))) thmID

 	    val thminst = inst_bdv subst thm

 	    val f = case p_ of

 			Frm => get_obj g_form pt p

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

 	in ContNOrewInst {thyID   = theory'2thyID thy',

 			  thm_rls = thm2guh (thy_containing_thm 

 						 thy' thmID) thmID, 

 			  bdvs    = subst,

 			  thminst = thminst,

 			  applto = f}

 	end)

   | context_thy (pt,p) (tac as Rewrite_Set rls') =

     (case applicable_in p pt tac of

 	 Appl (Rewrite_Set' (thy', _, rls, f, (res,asm))) =>

 	 ContRls {thyID   = theory'2thyID thy',

 		  rls     = rls2guh (thy_containing_rls thy' rls') rls',

 		  applto  = f,	  

 		  result  = res,	  

 		  asms    = asm})

   | context_thy (pt,p) (tac as Rewrite_Set_Inst (subs, rls')) = 

     (case applicable_in p pt tac of

 	 Appl (Rewrite_Set_Inst' (thy', _, subst, rls, f, (res,asm))) =>

 	 ContRlsInst {thyID   = theory'2thyID thy',

 		      rls     = rls2guh (thy_containing_rls thy' rls') rls',

 		      bdvs    = subst,

 		      applto  = f,	  

 		      result  = res,	  

 		      asms    = asm});

 (*.get all theorems in a rule set (recursivley containing rule sets).*)

 fun thm_of_rule Erule = []

   | thm_of_rule (thm as Thm _) = [thm]

   | thm_of_rule (Calc _) = []

   | thm_of_rule (Cal1 _) = []

   | thm_of_rule (Rls_ rls) = thms_of_rls rls

 and thms_of_rls Erls = []

   | thms_of_rls (Rls {rules,...}) = (flat o (map  thm_of_rule)) rules

   | thms_of_rls (Seq {rules,...}) = (flat o (map  thm_of_rule)) rules

   | thms_of_rls (Rrls _) = [];

 (* val Hrls {thy_rls = (_, rls),...} =

        get_the ["IsacKnowledge", "Test", "Rulesets", "expand_binomtest"];

 > thms_of_rls rls;

    *)

 (*. check if a rule is contained in a rule-set (recursivley down in Rls_);

     this rule can even be a rule-set itself.*)

 fun contains_rule r rls = 

     let fun find (r, Rls_ rls) = finds (get_rules rls)

 	  | find r12 = eq_rule r12

 	and finds [] = false

 	  | finds (r1 :: rs) = if eq_rule (r, r1) then true else finds rs;

     in 

     (*writeln ("### contains_rule: r = "^rule2str r^", rls = "^rls2str rls);*)

     finds (get_rules rls) 

     end;

 (*. try if a rewrite-rule is applicable to a given formula; 

     in case of rule-sets (recursivley) collect all _atomic_ rewrites .*) 

 fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =

     if contains_bdv thm

     then case rewrite_inst_ thy ro erls false subst thm f of

 	      SOME (f',_) =>[rule2tac subst thm']

 	    | NONE => []

     else (case rewrite_ thy ro erls false thm f of

 	SOME (f',_) => [rule2tac [] thm']

 	    | NONE => [])

   | try_rew thy _ _ _ f (cal as Calc c) = 

     (case get_calculation_ thy c f of

 	SOME (str, _) => [rule2tac [] cal]

       | NONE => [])

   | try_rew thy _ _ _ f (cal as Cal1 c) = 

     (case get_calculation_ thy c f of

 	SOME (str, _) => [rule2tac [] cal]

       | NONE => [])

   | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls

 and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) = 

     distinct (flat (map (try_rew thy ro erls subst f) rules))

   | filter_appl_rews thy subst f (Seq {rew_ord = ro, erls, rules,...}) = 

     distinct (flat (map (try_rew thy ro erls subst f) rules))

   | filter_appl_rews thy subst f (Rrls _) = [];

 (*. decide if a tactic is applicable to a given formula; 

     in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)

 (* val 

    *)

 fun atomic_appl_tacs thy _ _ f (Calculate scrID) =

     try_rew thy e_rew_ordX e_rls [] f (Calc (snd(assoc1 (!calclist', scrID))))

   | atomic_appl_tacs thy ro erls f (Rewrite (thm' as (thmID, _))) =

     try_rew thy (ro, assoc_rew_ord ro) erls [] f 

 	    (Thm (thmID, assoc_thm' thy thm'))

   | atomic_appl_tacs thy ro erls f (Rewrite_Inst (subs, thm' as (thmID, _))) =

     try_rew thy (ro, assoc_rew_ord ro) erls (subs2subst thy subs) f 

 	    (Thm (thmID, assoc_thm' thy thm'))

   | atomic_appl_tacs thy _ _ f (Rewrite_Set rls') =

     filter_appl_rews thy [] f (assoc_rls rls')

   | atomic_appl_tacs thy _ _ f (Rewrite_Set_Inst (subs, rls')) =

     filter_appl_rews thy (subs2subst thy subs) f (assoc_rls rls')

   | atomic_appl_tacs _ _ _ _ tac = 

     (writeln ("### atomic_appl_tacs: not impl. for tac = '"^ tac2str tac ^"'");

      []);

 (*.not only for thydata, but also for thy's etc.*)

 fun theID2guh (theID:theID) =

     case length theID of

 	0 => raise error ("theID2guh: called with theID = "^strs2str' theID)

       | 1 => part2guh theID

       | 2 => thy2guh theID

       | 3 => thypart2guh theID

       | 4 => let val [isa, thyID, typ, elemID] = theID

 	     in case typ of

 		    "Theorems" => thm2guh (isa, thyID) elemID

 		  | "Rulesets" => rls2guh (isa, thyID) elemID

 		  | "Calculations" => cal2guh (isa, thyID) elemID

 		  | "Orders" => ord2guh (isa, thyID) elemID

 		  | "Theorems" => thy2guh [isa, thyID]

 		  | str => raise error ("theID2guh: called with theID = "^

 					strs2str' theID)

 	     end

       | n => raise error ("theID2guh called with theID = "^strs2str' theID);

 (*.filenames not only for thydata, but also for thy's etc.*)

 fun theID2filename (theID:theID) = theID2guh theID ^ ".xml" : filename;

 fun guh2theID (guh:guh) =

     let val guh' = explode guh

 	val part = implode (take_fromto 1 4 guh')

 	val isa = implode (take_fromto 5 9 guh')

     in if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)

        then raise error ("guh '"^guh^"' does not begin with \

 				     \exp_ | thy_ | pbl_ | met_")

        else let val chap = case isa of

 				"isab_" => "Isabelle"

 			      | "scri_" => "IsacScripts"

 			      | "isac_" => "IsacKnowledge"

 			      | _ => 

 				raise error ("guh2theID: '"^guh^

 					     "' does not have isab_ | scri_ | \

 					     \isac_ at position 5..9")

 		val rest = takerest (9, guh') 

 		val thyID = takewhile [] (not o (curry op= "-")) rest

 		val rest' = dropuntil (curry op= "-") rest

 	    in case implode rest' of

 		   "-part" => [chap] : theID

 		 | "" => [chap, implode thyID]

 		 | "-Theorems" => [chap, implode thyID, "Theorems"]

 		 | "-Rulesets" => [chap, implode thyID, "Rulesets"]

 		 | "-Operations" => [chap, implode thyID, "Operations"]

 		 | "-Orders" => [chap, implode thyID, "Orders"]

 		 | _ => 

 		   let val sect = implode (take_fromto 1 5 rest')

 		       val sect' = 

 			   case sect of

 			       "-thm-" => "Theorems"

 			     | "-rls-" => "Rulesets"

 			     | "-cal-" => "Operations"

 			     | "-ord-" => "Orders"

 			     | str => 

 			       raise error ("guh2theID: '"^guh^"' has '"^sect^

 					    "' instead -thm- | -rls- | \

 					    \-cal- | -ord-")

 		   in [chap, implode thyID, sect', implode 

 						       (takerest (5, rest'))]

 		   end

 	    end	

     end;

 (*> guh2theID "thy_isac_Biegelinie-Theorems";

 val it = ["IsacKnowledge", "Biegelinie", "Theorems"] : theID

 > guh2theID "thy_scri_ListC-thm-zip_Nil";

 val it = ["IsacScripts", "ListC", "Theorems", "zip_Nil"] : theID*)

 fun guh2filename (guh : guh) = guh ^ ".xml" : filename;

 (*..*)

 fun guh2rewtac (guh:guh) ([] : subs) =

     let val [isa, thy, sect, xstr] = guh2theID guh

     in case sect of

 	   "Theorems" => Rewrite (xstr, "")

 	 | "Rulesets" => Rewrite_Set xstr

 	 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'") 

     end

   | guh2rewtac (guh:guh) subs =

     let val [isa, thy, sect, xstr] = guh2theID guh

     in case sect of

 	   "Theorems" => Rewrite_Inst (subs, (xstr, ""))

 	 | "Rulesets" => Rewrite_Set_Inst (subs,  xstr)

 	 | str => raise error ("guh2rewtac: not impl. for '"^xstr^"'") 

     end;

 (*> guh2rewtac "thy_isac_Test-thm-constant_mult_square" [];

 val it = Rewrite ("constant_mult_square", "") : tac

 > guh2rewtac "thy_isac_Test-thm-risolate_bdv_add" ["(bdv, x)"];

 val it = Rewrite_Inst (["(bdv, x)"], ("risolate_bdv_add", "")) : tac

 > guh2rewtac "thy_isac_Test-rls-Test_simplify" [];

 val it = Rewrite_Set "Test_simplify" : tac

 > guh2rewtac "thy_isac_Test-rls-isolate_bdv" ["(bdv, x)"];

 val it = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv") : tac*)

 (*.the front-end may request a context for any element of the hierarchy.*)

 (* val guh = "thy_isac_Test-rls-Test_simplify";

    *)

 fun no_thycontext (guh : guh) = (guh2theID guh; false)

     handle _ => true;

 (*> has_thycontext  "thy_isac_Test";

 if has_thycontext  "thy_isac_Test" then "OK" else "NOTOK";

  *)

 (*.get the substitution of bound variables for matchTheory:

    # lookup the thm|rls' in the script

    # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst

    # instantiate this subs with the istates env to [(bdv, x),..]

    # otherwise [].*)

 (*WN060617 hack assuming that all scripts use only one bound variable

 and use 'v_' as the formal argument for this bound variable*)

 (* val (ScrState (env,_,_,_,_,_), _, guh) = (is, "dummy", guh);

    *)

 fun subs_from (ScrState (env,_,_,_,_,_)) _(*:Script sc*) (guh:guh) =

     let val theID as [isa, thyID, sect, xstr] = guh2theID guh

     in case sect of

 	   "Theorems" => 

 	   let val thm = PureThy.get_thm (assoc_thy (thyID2theory' thyID)) xstr

 	   in if contains_bdv thm

 	      then let val formal_arg = str2term "v_"

 		       val value = subst_atomic env formal_arg

 		   in ["(bdv," ^ term2str value ^ ")"]:subs end

 	      else []

 	   end

 	 | "Rulesets" => 

 	   let val rules = (get_rules o assoc_rls) xstr

 	   in if contain_bdv rules

 	      then let val formal_arg = str2term"v_"

 		       val value = subst_atomic env formal_arg

 		   in ["(bdv,"^term2str value^")"]:subs end

 	      else []

 	   end

     end;

 (* use"ME/rewtools.sml";

    *)