(* 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";

   *)