(* isac's rewriter

    (c) Walther Neuper 2000

 *)

 signature REWRITE =

   sig

     val assoc_thm': theory -> thm' -> thm

     val assoc_thm'': theory -> thmID -> thm

     val calculate_: theory -> string * eval_fn -> term -> (term * (string * thm)) option

     val eval__true: theory -> int -> term list -> (term * term) list -> rls -> term list * bool

     val eval_listexpr_: theory -> rls -> term -> term

     val eval_true: theory -> term list -> rls -> bool

     val eval_true_: theory' -> rls -> term -> bool

     val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> lrd list -> term -> term -> term * term list * lrd list * bool

     val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option

     val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> rls -> bool -> (term * term) list -> thm -> term -> (term * term list) option

     val rewrite_set_: theory -> bool -> rls -> term -> (term * term list) option

     val rewrite_set_inst_: theory -> bool -> (term * term) list -> rls -> term -> (term * term list) option

     val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> rls -> term list -> term -> (term * term list) option

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (* NONE *)

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

   (* NONE *)

 (* probably shift up ---------------

     exception NO_REWRITE

     exception STOP_REW_SUB

     val adhoc_thm': theory' -> string * eval_fn -> cterm' -> thm' option

     val app_rev: theory -> int -> rls -> term -> term * term list * bool

     val app_sub: theory -> int -> rls -> term -> term * term list * bool

     val calculate: theory' -> string * eval_fn -> cterm' -> (string * thm') option

     val convert: 'a -> string -> string

     val convert_metaview_to_thmid: theory -> string -> thm

     val eval_true': theory' -> rls' -> term -> bool

     val get_rls_scr: rls' -> scr

     val mk_thm: theory -> string -> thm

     val mk_thm'': theory -> term -> thm

     val parse': theory' -> cterm' -> cterm' option

     val rewrite: theory' -> rew_ord' -> rls' -> bool -> thm' -> cterm' -> (string * string) option

     val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option

     val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option

     val rewrite_inst: theory' -> rew_ord' -> rls' -> bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) option

     val rewrite_set: theory' -> bool -> rls' -> cterm' -> (string * string) option

     val rewrite_set_inst: theory' -> bool -> subs' -> rls' -> cterm' -> (string * string) option

     val subs'2subst: theory -> subs' -> subst

     val trace: int -> string -> unit

     val trace1: int -> string -> unit

 --------------------------------------*)

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

   end

 (**)

 structure Rewrite(**): REWRITE(**) =

 struct

 (**)

 exception NO_REWRITE;

 exception STOP_REW_SUB; (*WN050820 quick and dirty*)

 fun trace i str = 

   if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()

 fun trace1 i str = 

   if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()

 (* 

 Synopsis rewriting (prep for reference manual):

 ----------------------------------------------

 Rewriting uses theorems for transforming terms. However, not all kinds

 of such transformations can be done by rewriting. Examples are

 calculation with numerals or cancellation of fractions. 

 Isac tries to present transformations like calculations or cancellation 

 as simple rewrite steps for the naive user. However, some of such

 transformations should be transparent to the user by single-stepping.

 For instance, cancellation involves interesting CA algorithms like 

 GCD of multivariate polynomials.

 Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",

 the former for steps which are not meant to be inspected by single-stepping

 the latter meant for single-stepping and providing respective mechanisms.

 (1) Inclusion by "thm Calc" for 1-step execution

 TODO

 (2) Inclusion by "Rrls" for multi-step execution

 TODO

 In multi-step execution "reverse rewriting" worked only as passive presentation

 without any interaction. So the functions init_state, locate_rule etc are just dummies.

 TODO

 ? multi-step execution did never work.

 what worked is "reverse rewriting", 

 i.e. presentation of intermediate steps *without* interaction

 TODO

 # type rule and scr | Rfuns

 # type rrlsstate = (*state for reverse rewriting*) 

 # type and rls | Rrls

 all in calcelems.sml

 TODO

 *)

 fun rewrite__ thy i bdv tless rls put_asm thm ct =

   (let

     val (t',asms,lrd,rew) = 

 	rew_sub thy i bdv tless rls put_asm [(*root of the term*)]

 		(((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm) ct;

   in if rew then SOME (t', distinct asms)

      else NONE end)

 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)

 and rew_sub thy i bdv tless rls put_asm lrd r t = 

   ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));

    tracing ("@@@ rew_sub begin: bdv = "^(@{make_string} bdv));

    tracing ("@@@ rew_sub begin: r = "^(term2str r));*)

     let                  (* copy from Pure/thm.ML: fun rewritec *)

      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop

                        o Logic.strip_imp_concl) r;

      (*?alternative Unify.matchers:

        http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)

      val r' = Envir.subst_term (Pattern.match thy (lhs, t) 

 					      (Vartab.empty, Vartab.empty)) r;

      val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 

                                              (Logic.count_prems r', [], r'));

      val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 

                o Logic.strip_imp_concl) r';

      (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)

      val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []

 	    then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else();

      val (t'',p'') =                                   (*conditional rewriting*)

 	 let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls 	     

 	 in if nofalse

 	    then (if ! trace_rewrite andalso i < ! depth andalso p' <> []

 		  then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^

 			       "   stored: "^(terms2str simpl_p'))

 		  else(); (t',simpl_p'))             (* uncond.rew. from above*)

 	    else 

 		(if ! trace_rewrite andalso i < ! depth 

 		 then tracing((idt"#"(i+1))^" asms false: "^(terms2str p')) 

 		 else(); raise STOP_REW_SUB (*dont go into subterms of cond*))

 	 end

    in if perm lhs rhs andalso not (tless bdv (t',t))       (*ordered rewriting*)

 	then (if ! trace_rewrite andalso i < ! depth 

 	      then tracing((idt"#"i)^" not: \""^

 	      (term2str t)^"\" > \""^

 	      (term2str t')^"\"") else (); 

 	      raise NO_REWRITE )

 	else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^

 		      ", p'' ="^(terms2str p'')^", true)");*)

 	      (t'',p'',[],true))

    end

    ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) => 

      ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)

       case t of

 	Const(s,T) => (Const(s,T),[],lrd,false)

       | Free(s,T) => (Free(s,T),[],lrd,false)

       | Var(n,T) => (Var(n,T),[],lrd,false)

       | Bound i => (Bound i,[],lrd,false)

       | Abs(s,T,body) => 

 	  let val (t', asms, lrd, rew) = 

 		  rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body

 	  in (Abs(s,T,t'), asms, [], rew) end

       | t1 $ t2 => 

 	  let val (t2', asm2, lrd, rew2) = 

 		  rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2

 	  in if rew2 then (t1 $ t2', asm2, lrd, true)

 	     else let val (t1', asm1, lrd, rew1) = 

 	       rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1

 		  in if rew1 then (t1' $ t2, asm1, lrd, true)

 		     else (t1 $ t2,[], lrd, false) end

 	  end)

 (* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)

 and eval__true thy i asms bdv rls =

   if asms = [@{term True}] orelse asms = [] then ([], true)

   (* this allows to check Rrls with prepat = ([@{term True}], pat) *)

   else if asms = [@{term False}] then ([], false) else

     let                            

       fun chk indets [] = (indets, true)(*return asms<>True until false*)

         | chk indets (a::asms) =

           (case rewrite__set_ thy (i + 1) false bdv rls a of

             NONE => (chk (indets @ [a]) asms)

           | SOME (t, a') =>

             if t = @{term True} then (chk (indets @ a') asms) 

             else if t = @{term False} then ([], false)

           (*asm false .. thm not applied ^^^; continue until False vvv*)

           else chk (indets @ [t] @ a') asms);

     in chk [] asms end

 (* rewrite with a rule set, which must not be the empty Erls *)

 and rewrite__set_ _ _ __ Erls t = 

     error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")

   (* rewrite with a 'reverse rule set' implemented by ML code *)

   | rewrite__set_ thy i _ _ (rrls as Rrls _) t =

     let

       val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)

 	    val (t', asm, rew) = app_rev thy (i + 1) rrls t

     in if rew then SOME (t', distinct asm) else NONE end

   (* rewrite with a rule set containing Thms or Calculations *)

   | rewrite__set_ thy i put_asm bdv rls ct =

     let

       datatype switch = Appl | Noap;

       fun rew_once ruls asm ct Noap [] = (ct, asm) (* unify with version in rewtools.sml *)

         | rew_once ruls asm ct Appl [] = 

           (case rls of Rls _ => rew_once ruls asm ct Noap ruls

           | Seq _ => (ct, asm))

         | rew_once ruls asm ct apno (rul::thms) =

           case rul of

             Thm (thmid, thm) =>

               (trace1 i (" try thm: " ^ thmid);

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

                   ((#erls o rep_rls) rls) put_asm thm ct of

                 NONE => rew_once ruls asm ct apno thms

               | SOME (ct',asm') => 

                 (trace1 i (" rewrites to: " ^ term2str ct');

                 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))

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

             let val _= trace1 i (" try calc: " ^ op_ ^ "'")

               val ct = uminus_to_string ct

             in case adhoc_thm thy cc ct of

                 NONE => rew_once ruls asm ct apno thms

               | 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 error ("rewrite_set_, rewrite_ \"" ^ 

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

                   val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))

                 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end

             end

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

             let val _= trace1 i (" try cal1: " ^ op_ ^ "'");

               val ct = uminus_to_string ct

             in case adhoc_thm1_ 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 error ("rewrite_set_, rewrite_ \"" ^

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

                   val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))

                 in the pairopt end

             end

           | Rls_ rls' => 

             (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of

               SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms

             | NONE => rew_once ruls asm ct apno thms);

       val ruls = (#rules o rep_rls) rls;

       val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)

       val (ct', asm') = rew_once ruls [] ct Noap ruls;

 	  in if ct = ct' then NONE else SOME (ct', distinct asm') end

 (* apply an Rrls; if not applicable proceed with subterms *)

 and app_rev thy i rrls t = 

   let (* check a (precond, pattern) of a rev-set; stops with 1st true *)

     fun chk_prepat thy erls [] t = true

       | chk_prepat thy erls prepat t =

         let

           fun chk (pres, pat) =

             (let 

               val subst: Type.tyenv * Envir.tenv =

                 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)

              in

               snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)

              end) handle _ => false

            fun scan_ f [] = false (*scan_ NEVER called by []*)

              | scan_ f (pp::pps) =

                if f pp then true else scan_ f pps;

         in scan_ chk prepat end;

     (* apply the normal_form of a rev-set *)

     fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =

       if chk_prepat thy erls prepat t then normal_form t else NONE;

     val opt = app_rev' thy rrls t

   in

     case opt of

       SOME (t', asm) => (t', asm, true)

     | NONE => app_sub thy i rrls t

   end

 (* apply an Rrls to subterms *)

 and app_sub thy i rrls t =

   ((*tracing("### app_sub: subterm = "^(term2str t));*)

   case t of

     Const (s, T) => (Const(s, T), [], false)

   | Free (s, T) => (Free(s, T), [], false)

   | Var (n, T) => (Var(n, T), [], false)

   | Bound i => (Bound i, [], false)

   | Abs (s, T, body) => 

 	  let val (t', asm, rew) = app_rev thy i rrls body

 	  in (Abs(s, T, t'), asm, rew) end

   | t1 $ t2 => 

     let val (t2', asm2, rew2) = app_rev thy i rrls t2

     in

       if rew2 then (t1 $ t2', asm2, true)

       else

         let val (t1', asm1, rew1) = app_rev thy i rrls t1

         in if rew1 then (t1' $ t2, asm1, true)

            else (t1 $ t2, [], false)

         end

     end);

 (*.rewriting without argument [] for rew_ord.*)

 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)

 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;

 (* rewriting without internal argument [] *)

 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;

 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;

 fun subs'2subst thy (s:subs') = 

     (((map (apfst (Thm.term_of o the o (parse thy)))) 

      o (map (apsnd (Thm.term_of o the o (parse thy))))) s):subst;

 (*.variants of rewrite.*)

 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst,

   thus the argument put_asm  IS NOT NECESSARY -- FIXME*)

 (* val (rew_ord,rls,put_asm,thm,ct)=

        (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);

    *)

 fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool) 

 		  (subst:(term * term) list) (thm:thm) (ct:term) =

     rewrite__ thy 1 subst rew_ord rls put_asm thm ct;

 fun rewrite_set_inst_ (thy:theory) 

   (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =

   (*let 

     val subst = subs'2subst thy subs';

     val subrls = instantiate_rls subs' rls

   in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct

   (*end*);

 (* given a list of equalities (lhs = rhs) and a term, 

    replace all occurrences of lhs in the term with rhs;

    thus the order or equalities matters: put variables in lhs first. *)

 fun rewrite_terms_ thy ord erls equs t =

   let

 	  fun rew_ (t', asm') [] _ = (t', asm')

 	    | rew_ (t', asm') (rules as r::rs) t =

 	        let

 	          val (t'', asm'', lrd, rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t

 	        in 

 	          if rew 

 	          then rew_ (t'', asm' @ asm'') rules t''

 	          else rew_ (t', asm') rs t'

 	        end

 	  val (t'', asm'') = rew_ (e_term, []) equs t

     in if t'' = e_term then NONE else SOME (t'', asm'')

     end;

 (*. search ct for adjacent numerals and calculate them by operator isa_fn .*)

 fun calculate_ thy isa_fn ct =

   let val ct = uminus_to_string ct

     in case adhoc_thm thy isa_fn ct of

 	   NONE => NONE

 	 | SOME (thmID, thm) => 

 	   (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct

     in SOME (rew,(thmID, thm)) end)

 	   handle _ => error ("calculate_: "^thmID^" does not rewrite")

   end;

 (*

 > val thy = InsSort.thy;

 > val op_ = "le";      (* < *)

 > val ct = (the o (parse thy)) 

    "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";

 > calculate_ thy op_ ct;

   SOME

     ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",

      "(#1 < #3) = True") : (cterm * thm) option  *)

 fun get_rls_scr rls' = ((#scr o rep_rls o assoc_rls) rls')

   handle _ => error ("get_rls_scr: no script for " ^ rls');

 (*Thm.make_thm added to Pure/thm.ML*)

 fun mk_thm'' thy t = 

     let val t' = case t of

 		     Const ("==>",_) $ _ $ _ => t

 		   | _ => Trueprop $ t

     in Thm.make_thm (Thm.global_cterm_of thy t') end;

 fun mk_thm thy str = 

     let val t = (Thm.term_of o the o (parse thy)) str

 	val t' = case t of

 		     Const ("==>",_) $ _ $ _ => t

 		   | _ => Trueprop $ t

     in Thm.make_thm (Thm.global_cterm_of thy t') end;

 (*

   val str = "?r ^^^ 2 = ?r * ?r";

   val thm = realpow_twoI;

   val t1 = (#prop o rep_thm) (num_str thm);

   val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);

   t1 = t2;

 val it = true : bool      ... !!!

   val th1 = (num_str thm);

   val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;

   th1 = th2;

 ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   val str = "k ~= 0 ==> m * k / (n * k) = m / n";

   val thm = real_mult_div_cancel2;

   val t1 = (#prop o rep_thm) (num_str thm);

   val t2 = ((Thm.term_of o the o (parse thy)) str);

   t1 = t2;

 val it = false : bool     ... Var .. Free

   val th1 = (num_str thm);

   val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;

   th1 = th2;

 ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!

 *)

 (*prints subgoal etc. 

 ((goal thy);(topthm()) o ) str;                      *)

 (*assume rejects scheme variables 

   assume ((Thm.global_cterm_of thy) (Trueprop $ 

 		(Thm.term_of o the o (parse thy)) str)); *)

 (* outcommented 18.11.xx, xx < 02 -------

 fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)

   | rul2rul' (Calc op_)         = Calc' op_;

 fun rul'2rul thy (Thm'(thmid, ct')) = 

        Thm (thmid, mk_thm thy ct')

   | rul'2rul thy' (Calc' op_)        = Calc op_;

 fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =

   Rls'{preconds'= map string_of_cterm preconds,

        rew_ord' = fst rew_ord,

        rules'   = map rul2rul' rules}:rlsdat';

 fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,

 		   rules'=rules}:rlsdat') =

   let val thy = assoc_thy thy';

   in Rls{preconds = map (the o (parse thy)) preconds,

 	 rew_ord  = (rew_ord, the (assoc'(rew_ord',rew_ord))),

 	 rules    = map (rul'2rul thy) rules}:rls end;

 ------- *)

 (* "metaview" as seen from programs and from user input (both are parsed like terms presently) *)

 fun convert_metaview_to_thmid thy thmid =

   let val thmid' = case thmid of

       "add_commute" => "add.commute"

     | "mult_commute" => "mult.commute"

     | "add_left_commute" => "add.left_commute"

     | "mult_left_commute" => "mult.left_commute"

     | "add_assoc" => "add.assoc"

     | "mult_assoc" => "mult.assoc"

     | _ => thmid

   in (Global_Theory.get_thm thy) thmid' end;

 (* FIXME: the other direction below is probably concerned with this fun:

 thmID_of_derivation_name' @{thm add.assoc} = "assoc"    TODO: repair this fun *);

 fun convert thmid_to_metaview thmid =

   case thmid of

       "add.commute" => "add_commute"

     | "mult.commute" => "mult_commute"

     | "add.left_commute" => "add_left_commute"

     | "mult.left_commute" => "mult_left_commute"

     | "add.assoc" => "add_assoc"

     | "mult.assoc" => "mult_assoc"

     | _ => thmid;

 (*.get the theorem associated with the xstring-identifier;

    if the identifier starts with "sym_" then swap lhs = rhs around =

    (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);

    identifiers starting with "#" come from Calc and

    get a hand-made theorem (containing numerals only).*)

 fun assoc_thm'' (thy : theory) (thmid : thmID) =

   case Symbol.explode thmid of

     "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)

   | "s"::"y"::"m"::"_"::id => ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym

   | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)

   | _ => thmid |> convert_metaview_to_thmid thy |> num_str

 fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =

   (case Symbol.explode thmid of

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

       if hd id = "#" 

       then mk_thm thy ct'

       else ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym

   | id =>

     if hd id = "#" 

     then mk_thm thy ct'

     else thmid |> convert_metaview_to_thmid thy |> num_str

   ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) => 

     error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")

 fun parse' (thy:theory') (ct:cterm') =

     case parse (assoc_thy thy) ct of

 	NONE => NONE

       | SOME ct => SOME ((term2str (Thm.term_of ct)):cterm');

 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

   thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

 fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') (put_asm:bool) (thm:thm') (ct:cterm') =

   let val thy = assoc_thy thy';

   in

     case rewrite_ thy ((the o assoc')(!rew_ord',rew_ord))(assoc_rls rls)

       put_asm ((assoc_thm' thy) thm) ((Thm.term_of o the o (parse thy)) ct) of

       NONE => NONE

     | SOME (t, ts) => SOME (term2str t, terms2str ts)

   end;

 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

   thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

 fun rewrite_set (thy':theory') (put_asm:bool) (rls:rls') (ct:cterm') =

   let val thy = (assoc_thy thy');

   in

     case rewrite_set_ thy put_asm (assoc_rls rls) ((Thm.term_of o the o (parse thy)) ct) of

       NONE => NONE

     | SOME (t, ts) => SOME (term2str t, terms2str ts)

   end;

 fun eval_listexpr_ thy srls t =

   let val rew = rewrite_set_ thy false srls t;

   in case rew of SOME (res,_) => res | NONE => t end;

 fun adhoc_thm' (thy:theory') op_ (ct:cterm') =

    case adhoc_thm (assoc_thy thy) op_

     ((uminus_to_string o Thm.term_of o the o 

       (parse (assoc_thy thy))) ct) of

 	NONE => NONE

       | SOME (thmid, thm) => 

 	    SOME ((thmid, string_of_thmI thm):thm');

 fun calculate (thy':theory') op_ (ct:cterm') =

     let val thy = (assoc_thy thy');

     in

 	case calculate_ thy op_

 			((Thm.term_of o the o (parse thy)) ct) of

 	    NONE => NONE

 	  | SOME (ct,(thmID,thm)) => 

 	    SOME (term2str ct, 

 		  (thmID, string_of_thmI thm):thm')

     end;

 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

   thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

 fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls') 

   (put_asm:bool) subs (thm:thm') (ct:cterm') =

   let

     val thy = assoc_thy thy';

     val thm = assoc_thm' thy thm; (*28.10.02*)

     (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)

   in

     case rewrite_ thy

       ((the o assoc')(!rew_ord',rew_ord)) (assoc_rls rls)

       put_asm (*sub*)thm ((Thm.term_of o the o (parse thy)) ct) of

       NONE => NONE

     | SOME (ctm, ctms) => 

       SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)

   end;

 (*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

   thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

 fun rewrite_set_inst (thy':theory') (put_asm:bool)

   subs' (rls:rls') (ct:cterm') =

   let

     val thy = assoc_thy thy';

     val rls = assoc_rls rls

     val subst = subs'2subst thy subs'

   in case rewrite_set_inst_ thy put_asm subst (*sub*)rls

 			    ((Thm.term_of o the o (parse thy)) ct) of

 	 NONE => NONE

        | SOME (t, ts) => SOME (term2str t, terms2str ts)

   end;

 (*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)

 fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true

   | eval_true' (thy':theory') (rls':rls') (t:term) =

 (* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';

    *)

     let val ct' = term2str t;

     in case rewrite_set thy' false rls' ct' of

 	   SOME ("HOL.True",_) => true

 	 | _ => false 

     end;

 fun eval_true_ _ _ (Const ("HOL.True",_)) = true

   | eval_true_ (thy':theory') rls t =

     case rewrite_set_ (assoc_thy thy') false rls t of

 	   SOME (Const ("HOL.True",_),_) => true

 	 | _ => false;

 (*

 val test_rls = 

   Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right), 

       rules = [Calc ("matches",eval_matches "")

 	       ],

       scr = Prog ((Thm.term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

   rewrite_set_ (Thy_Info_get_theory "Isac") eval_rls false test_rls 

         ((the o (parse thy)) "matches (?a = ?b) (x = #0)");

   val xxx = (Thm.term_of o the o (parse thy)) 

 	       "matches (?a = ?b) (x = #0)";

   eval_matches """" xxx thy;

 SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",

      Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

   rewrite_set_ (Thy_Info_get_theory "Isac") eval_rls false eval_rls 

         ((the o (parse thy)) "contains_root (sqrt #0)");

 val it = SOME ("HOL.True",[]) : (cterm * cterm list) option

 *)

 (*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise

 datatype det = TRUE  | FALSE | INDET;(*FIXXME.WN:16.5.03

 				     introduced with quick-and-dirty code*)

 fun determine dts =

     let val false_indet = 

 	    filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts

         val ts = map (#2: det * term -> term) dts

     in if nil = false_indet then (TRUE, ts)

        else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))

 			    false_indet

        then (INDET, ts)

        else (FALSE, ts) end;

 (* val dts = [(INDET,e_term), (FALSE,@{term False}), 

 	      (INDET,e_term), (TRUE,@{term True})];

   determine dts;

 val it =

   (FALSE,

    [Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),

     Const ("HOL.True","bool")]) : det * term list*)

 fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*)

 if cs = [@{term True}] orelse cs = [] then (TRUE, [])

     else if cs = [@{term False}] then (FALSE, cs)

     else

 	let fun eval t = 

 		let val taopt = rewrite__set_ thy 1 false [] rls t

 		in case taopt of

 		       SOME (t,_) =>

 		       if t = @{term True} then (TRUE, t)

 		       else if t = @{term False} then (FALSE, t)

 		       else (INDET, t)

 		     | NONE => (INDET, t) end

 	in (determine o (map eval)) cs end;

 WN.16.5.0-------------------------------------------------------------*)

 end