(* isac's rewriter

    (c) Walther Neuper 2000

 use"ProgLang/rewrite.sml"; 

 use"rewrite.sml";

 *)

 exception NO_REWRITE;

 exception STOP_REW_SUB; (*WN050820 quick and dirty*)

 (*17.6.00: rewrite by going down the term with rew_sub*)

 (* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =

        (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);

    *)

 fun rewrite__ thy i bdv tless rls put_asm thm ct =

   ((*writeln ("@@@ r..te__ begin: t = "^(term2str 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 rep_thm) thm) ct;

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

      else NONE end)

 (* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct);

    val t1 = (#prop o rep_thm) thm;

    val t2 = norm t1;

    val t3 = inst_bdv bdv t2;

    val thm4 = read_instantiate [("bdv","x")] thm;

    val t4 = (norm o #prop o rep_thm) thm4;

    *)

 (* val (thy, i, bdv, tless, rls, put_asm, r,             t) = 

        (thy, i,bdv, tless, rls, put_asm, 

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

    val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 

        (thy, 1, [],  ord,   erls,false,   [],  r, t);

    val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 

        (thy, i, bdv, tless, rls, put_asm, [],  

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

    *)

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

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

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

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

 		      o Logic.strip_imp_concl) r;

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

      val r' = ren_inst (insts, r, lhs, t);

      val p' = map strip_trueprop (Logic.strip_imp_prems r'); 

      val t' = (snd o dest_equals' o strip_trueprop 

 	       o Logic.strip_imp_concl) r';*)

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

                        o Logic.strip_imp_concl) r;

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

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

      val p' = (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 _= writeln("@@@ rew_sub match: t'= "^(term2str t'));*)

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

 	    then writeln((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 writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^

 			       "   stored: "^(terms2str simpl_p'))

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

 	    else 

 		(if ! trace_rewrite andalso i < ! depth 

 		 then writeln((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 writeln((idt"#"i)^" not: \""^

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

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

 	      raise NO_REWRITE )

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

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

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

    end

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

      ((*writeln ("@@@ 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)

 (* val (cprems',rls)=([pre],prls);

    rewrite__set_ thy i false rls pre;

    *)

 and eval__true thy i asms bdv rls =

 (* val (thy, i, asms, bdv, rls) = (thy, (i+1), p', bdv, rls);

    *)

   if asms = [HOLogic.true_const] orelse asms = [] 

   then ([], true) else if asms = [HOLogic.false_const] then ([], false)

   else let                            

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

 	| chk indets (a::asms) =

 (* val (indets, (a::asms)) = ([], asms);

    *) 

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

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

 	    | SOME (t, a') =>

 	      if t = HOLogic.true_const 

 	      then (chk (indets @ a') asms)

 	      else if t = HOLogic.false_const then ([], false)

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

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

   in chk [] asms end

 and rewrite__set_ _ _ __ Erls t = 

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

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

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

 	       then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^

 			     (term2str t)) else ()

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

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

        else NONE end

   | rewrite__set_ thy i put_asm bdv rls ct =

 (* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);

    *)

   let

     datatype switch = Appl | Noap;

     fun rew_once ruls asm ct Noap [] = (ct,asm)

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

 (* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);

    val Thm (thmid, thm) = rul;

    *)

       case rul of

 	Thm (thmid, thm) =>

 	  (if !trace_rewrite andalso i < ! depth 

 	   then writeln((idt"#"(i+1))^" try thm: "^thmid) else ();

 	   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') => (if ! trace_rewrite andalso i < ! depth 

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

 			  (term2str ct')) else ();

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

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

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

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

 	     val ct = uminus_to_string ct

 	   in case get_calculation_ thy cc ct of

 	     NONE => ((*writeln "@@@ rewrite__set_: get_calculation_-> 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 raise error("rewrite_set_, rewrite_ \""^

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

 		 val _ = if ! trace_rewrite andalso i < ! depth 

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

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

 			 else()

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

 	   end)

 (* use"ProgLang/rewrite.sml";

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

       | 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_calculation1_ 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 (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 _= if ! trace_rewrite andalso i < ! depth 

 	   then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^

 			 (term2str ct)) else ()

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

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

 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 ((*writeln("### app_rev': t = "^(term2str t));*)

                   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

 and app_sub thy i rrls t =

      ((*writeln("### 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 [] for rew_ord.*)

 (* val (thy, rew_ord, erls, bool, thm, term) =

        (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);

    val (thy, rew_ord, erls, bool, thm, term) =

        (thy, rew_ord, erls, false, thm, t'');

    *)

 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 =

 (* val (thy, bool, rls, term) = (thy, false, srls, t);

    *)

     rewrite__set_ thy 1 bool [] rls term;

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

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

      o (map (apsnd (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*);

 (* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t);

    *)

 (*.rewrite using a list of terms.*)

 fun rewrite_terms_ thy ord erls subte t =

     let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^

 		      term_detail2str (hd subte)^

 		      "### rewrite_terms_ t= '"^term2str t^"' ..."^

 		      term_detail2str t);*)

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

 	  (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t);

 	     2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');

 	     rew_ (t', asm') (r::rs) t;

 	     *)

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

 	    let val _ = writeln("rew_ "^term2str t);

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

 		    rew_sub thy 1 [] ord erls false [] r t

 	    in if rew 

 	       then (writeln("true  rew_ "^term2str t'');

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

 	       else (writeln("false rew_ "^term2str t'');

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

 	    end

 	val (t'', asm'') = rew_ (e_term, []) subte 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 get_calculation_ 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  *)

 (* for test-printouts:

 val _ = writeln("in rew_sub  : "^( Syntax.string_of_term (thy2ctxt thy) t))

 val _ = writeln("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems')))

 *)

 fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))

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

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

 fun mk_thm thy str = 

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

 	val t' = case t of

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

 		   | _ => Trueprop $ t

     in make_thm (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 $ ((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 = ((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 ((cterm_of thy) (Trueprop $ 

 		(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 = the (assoc' (theory',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;

 ------- *)

 (*.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, ct'):thm') =

     (case explode thmid of

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

 	if hd id = "#" 

 	then mk_thm thy ct'

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

       | id => 

 	if hd id = "#" 

 	then mk_thm thy ct'

 	else (num_str o (PureThy.get_thm thy)) thmid

 	     ) handle _ => 

 		      raise error ("assoc_thm': '"^thmid^"' not in '"^

 				   (theory2domID thy)^"' (and parents)");

 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");

 val it = "6 = 2 * 3" : thm          

 > assoc_thm' Isac.thy ("real_add_zero_left","");

 val it = "0 + ?z = ?z" : thm

 > assoc_thm' Isac.thy ("sym_real_add_zero_left","");

 val it = "?t = 0 + ?t"  [.] : thm

 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");

 *** Unknown theorem(s) "real_add_zero_left"

 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)

  uncaught exception ERROR*)

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

     case parse ((the o assoc')(!theory',thy)) ct of

 	NONE => NONE

       | SOME ct => SOME ((term2str (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') =

 (* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);

    *)

     let val thy = (the o assoc')(!theory',thy');

     in

     case rewrite_ thy

 	((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))

 	put_asm ((assoc_thm' thy) thm)

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

 	NONE => NONE

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

     end;

 (*

 val thy     = "RatArith.thy";

 val rew_ord = "dummy_ord"; 

 > val rls     = "eval_rls";

 val put_asm = true; 

 val thm     = ("square_equation_left","");

 val ct      = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";

 val Zthy     = ((the o assoc')(!theory',thy));

 val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord)); 

 val Zrls     = ((the o assoc')(!ruleset',rls));

 val Zput_asm = put_asm; 

 val Zthm     = ((the o (assoc'_thm' thy)) thm);

 val Zct      = ((the o (parse ((the o assoc')(!theory',thy)))) ct);

 rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;

  use"Isa99/interface_ME_ISA.sml";

 *)

 (*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 = (the o assoc')(!theory',thy');

     in

     case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))

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

 	NONE => NONE

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

     end;

 (*evaluate list-expressions

   should work on term, and stand in Isa99/rewrite-parse.sml, 

   but there list_rls <- eval_binop is not yet defined*)

 (*fun eval_listexpr' ct = 

     let val rew = rewrite_set "ListC.thy" false "list_rls" ct;

     in case rew of 

 	   SOME (res,_) => res

 	 | NONE => ct end;-----------------30.9.02---*)

 fun eval_listexpr_ thy srls t =

 (* val (thy,            srls, t) = 

        ((assoc_thy th), sr,  (subst_atomic (upd_env_opt E (a,v)) t));

    *) 

     let val rew = rewrite_set_ thy false srls t;

     in case rew of 

 	   SOME (res,_) => res

 	 | NONE => t end;

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

    case get_calculation_ ((the o assoc')(!theory',thy)) op_

     ((uminus_to_string o term_of o the o 

       (parse ((the o assoc')(!theory',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 = (the o assoc')(!theory',thy');

     in

 	case calculate_ thy op_

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

 (*

 fun instantiate'' thy' subs ((thmid,ct'):thm') = 

   let val thmid_ = implode ("#"::(explode thmid))  (*see type thm'*)

   in (thmid_, (string_of_thmI o (read_instantiate subs)) 

       ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;

 fun instantiate_rls' thy' subs (rls:rls') = 

     rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';

 ... problem with these functions: 

 > val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";

 val thm = "(bdv + a = b) = (bdv = b - a)" : thm

 > show_types:=true; thm;    

 val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm

 ... and this doesn't match because of too general typing (?!)

     and read_insitantiate doesn't instantiate the types (?!)

 === solutions:

 (1) hard-coded type-instantiation ("'a", "RatArith.rat")

 (2) instantiate', instantiate ... no help by isabelle-users@ !!!

 === conclusion:

     rewrite_inst, rewrite_set_inst circumvent the problem,

     according functions out-commented with 'instantiate''

 *)

 (* instantiate''

 fun instantiate'' thy' subs ((thmid,ct'):thm') = 

   let 

     val thmid_ = implode ("#"::(explode thmid));  (*see type thm'*)

     val thy = (the o assoc')(!theory',thy');

     val typs = map (#T o rep_cterm o the o (parse thy)) 

       ((snd o split_list) subs);

     val ctyps = map 

       ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy)) 

       ((snd o split_list) subs);

 > val thy' = "RatArith.thy";

 > val subs = [("bdv","x::rat"),("zzz","z::nat")];

 > (the o (parse ((the o assoc')(!theory',thy')))) "x::rat";

 > (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy'))));

 > val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o 

 	      (parse ((the o assoc')(!theory',thy')))) "x::rat";

 > val bdv = (the o (parse thy)) "bdv";

 > val x   = (the o (parse thy)) "x";

 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)

       handle e => print_exn e;

 uncaught exception THM

   raised at: thm.ML:1085.18-1085.69

              thm.ML:1092.34

              goals.ML:536.61

 > val bdv = (the o (parse thy)) "bdv::nat";

 > val x   = (the o (parse thy)) "x::nat";

 > (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)

       handle e => print_exn e;

 uncaught exception THM

   raised at: thm.ML:1085.18-1085.69

              thm.ML:1092.34

              goals.ML:536.61

 > (instantiate' [SOME ctyp] [] isolate_bdv_add)

       handle e => print_exn e;      

 uncaught exception TYPE

   raised at: drule.ML:613.13-615.44

              goals.ML:536.61

 > val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";

 *)

 (*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 = (the o assoc')(!theory',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)) ((#2 o the o assoc')(!ruleset',rls))

       put_asm (*sub*)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 = (the o assoc')(!theory',thy');

     val rls = assoc_rls rls

     val subst = subs'2subst thy subs'

     (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)

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

 			    ((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 ("True",_)) = true

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

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

    *)

     let val ct' = term2str t;

     in case rewrite_set thy' false rls' ct' of

 	   SOME ("True",_) => true

 	 | _ => false 

     end;

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

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

     case rewrite_set_ (assoc_thy thy') false rls t of

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

 	 | _ => false;

 (*

 val test_rls = 

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

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

 	       ],

       scr = Script ((term_of o the o (parse thy)) 

       "empty_script")

       }:rls;      

   rewrite_set_ Isac.thy eval_rls false test_rls 

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

   val xxx = (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 ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

   rewrite_set_ Isac.thy eval_rls false eval_rls 

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

 val it = SOME ("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,HOLogic.false_const), 

 	      (INDET,e_term), (TRUE,HOLogic.true_const)];

   determine dts;

 val it =

   (FALSE,

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

     Const ("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 = [HOLogic.true_const] orelse cs = [] then (TRUE, [])

     else if cs = [HOLogic.false_const] 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 = HOLogic.true_const then (TRUE, t)

 		       else if t = HOLogic.false_const then (FALSE, t)

 		       else (INDET, t)

 		     | NONE => (INDET, t) end

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

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