(* 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*)

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 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 = "^(PolyML.makestring 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;

     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)

        | 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 get_calculation_ 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 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 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 ((*tracing("### 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

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

(* 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 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  *)

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

  handle _ => 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 = 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;

------- *)

(*.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 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 (num_str o (Global_Theory.get_thm thy)) thmid

	     ) handle _ => 

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

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

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

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

> assoc_thm' (Thy_Info.get_theory "Isac") ("add_0_left","");

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

> assoc_thm' (Thy_Info.get_theory "Isac") ("sym_real_add_zero_left","");

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

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

*** Unknown theorem(s) "add_0_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 (assoc_thy 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 = assoc_thy 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";

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     = assoc_thy 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 (assoc_thy 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 = (assoc_thy 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" 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_ (assoc_thy thy) op_

    ((uminus_to_string o 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_

			((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 ("#"::(Symbol.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 ("#"::(Symbol.explode thmid));  (*see type thm'*)

    val thy = assoc_thy 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";

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

> (the o (parse (assoc_thy thy'))) "x::rat";

> (#T o rep_cterm o the o (parse (assoc_thy thy')));

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

	      (parse (assoc_thy 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 = 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)) ((#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 = assoc_thy 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 ("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 ((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 = (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-------------------------------------------------------------*)