(* calculate values for function constants

   (c) Walther Neuper 000106

use"ProgLang/calculate.sml";

*)

(* dirty type-conversion 30.1.00 for "fixed_values [R=R]" *)

val aT = Type ("'a", []);

(* isas types for Free, parseold: (1) "R=R" or (2) "R=(R::real)": 

(1)

> val (TFree(ss2,TT2)) = T2;

val ss2 = "'a" : string

val TT2 = ["term"] : sort

(2)

> val (Type(ss2',TT2')) = T2';

val ss2' = "RealDef.real" : string

val TT2' = [] : typ list

(3)

val realType = TFree ("RealDef.real", HOLogic.termS);

is different internally, too;

(1) .. (3) are displayed equally !!!

*)

(* 30.1.00: generating special terms for ME:

   (1) binary numerals reconverted to Free ("#num",...) 

       by libarary_G.num_str: called from parse (below) and 

       interface_ME_ISA for all thms used

       (compare HOLogic.dest_binum)

   (2) 'a types converted to RealDef.real by typ_a2real

       in parse below

   (3) binary operators fixed to type real in RatArith.thy

       (trick by Markus Wenzel)

*)

(** calculate numerals **)

(*27.3.00: problems with patterns below:

"Vars (a // #2 = r * xxxxx b)" doesn't work, but 

"Vars (a // #2 = r * sqrt b)" works

*)

fun popt2str (SOME (str, term)) = "SOME "^term2str term

  | popt2str NONE = "NONE";

(* scan a term for applying eval_fn ef 

args

  thy:

  op_: operator (as string) selecting the root of the pair

  ef : fn : (string -> term -> theory -> (string * term) option)

             ^^^^^^... for creating the string for the resulting theorem

  t  : term to be scanned

result:

  (string * term) option: found by the eval_* -function of type

       fn : string -> string -> term -> theory -> (string * term) option

            ^^^^^^... the selecting operator op_ (variable for eval_binop)

*)

fun get_pair thy op_ (ef:string -> term -> theory -> (string * term) option) 

    (t as (Const(op0,t0) $ arg)) =                      (* unary fns *)

(* val (thy, op_, (ef),    (t as (Const(op0,t0) $ arg))) = 

       (thy, op_, eval_fn, ct);

   *)

    if op_ = op0 then 

	let val popt = ef op_ t thy

	in case popt of

	       SOME _ => popt

	     | NONE => get_pair thy op_ ef arg end

    else get_pair thy op_ ef arg

  | get_pair thy "Atools.ident" ef (t as (Const("Atools.ident",t0) $ _ $ _ )) =

(* val (thy, "Atools.ident", ef,      t as (Const(op0,_) $ t1 $ t2)) =

       (thy, op_,            eval_fn, ct);

   *)

    ef "Atools.ident" t thy                                 (* not nested *)

  | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2)) =  (* binary funs*)

(* val (thy, op_, ef,      (t as (Const(op0,_) $ t1 $ t2))) = 

       (thy, op_, eval_fn, ct);

   *)

    ((*tracing("1.. get_pair: binop = "^op_);*)

     if op_ = op0 then 

	 let val popt = ef op_ t thy

	 (*val _ = tracing("2.. get_pair: "^term2str t^" -> "^popt2str popt)*)

	 in case popt of 

		SOME (id,_) => popt

	      | NONE => 

		let val popt = get_pair thy op_ ef t1

		    (*val _ = tracing("3.. get_pair: "^term2str t1^

				    " -> "^popt2str popt)*)

		in case popt of 

		       SOME (id,_) => popt

		     | NONE => get_pair thy op_ ef t2

		end

	 end

     else (*search subterms*)

	 let val popt = get_pair thy op_ ef t1

	 (*val _ = tracing("4.. get_pair: "^term2str t^" -> "^popt2str popt)*)

	 in case popt of 

		SOME (id,_) => popt

	      | NONE => get_pair thy op_ ef t2

	 end)

  | get_pair thy op_ ef (t as (Const(op0,_) $ t1 $ t2 $ t3)) =(* trinary funs*)

    ((*tracing("### get_pair 4a: t= "^term2str t);

     tracing("### get_pair 4a: op_= "^op_);

     tracing("### get_pair 4a: op0= "^op0);*)

     if op_ = op0 then 

	case ef op_ t thy of

	    SOME tt => SOME tt

	  | NONE => (case get_pair thy op_ ef t2 of

			 SOME tt => SOME tt

		       | NONE => get_pair thy op_ ef t3)

    else (case get_pair thy op_ ef t1 of

	     SOME tt => SOME tt

	   | NONE => (case get_pair thy op_ ef t2 of

			  SOME tt => SOME tt

			| NONE => get_pair thy op_ ef t3)))

  | get_pair thy op_ ef (Const _) = NONE

  | get_pair thy op_ ef (Free _) = NONE

  | get_pair thy op_ ef (Var _) = NONE

  | get_pair thy op_ ef (Bound _) = NONE

  | get_pair thy op_ ef (Abs(a,T,body)) = get_pair thy op_ ef body

  | get_pair thy op_ ef (t1$t2) = 

    let(*val _= tracing("5.. get_pair t1 $ t2: "^term2str t1^" 

						   $ "^term2str t2)*)

	val popt = get_pair thy op_ ef t1

    in case popt of 

	   SOME _ => popt

	 | NONE => ((*tracing"### get_pair: t1 $ t2 -> NONE";*)

		    get_pair thy op_ ef t2) 

    end;

 (*

>  val t = (term_of o the o (parse thy)) "#3 + #4";

>  val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus"));

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>  atomty t';

> 

>  val t = (term_of o the o (parse thy)) "(a + #3) + #4";

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";

>  atomty t;

>  val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>  val it = "#3 + (#4 + a) = #7 + a" : string

>

>

>  val t = (term_of o the o (parse thy)) "#-4//#-2";

>  val eval_fn = the (assoc (!eval_list, "cancel"));

>  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "#2^^^#3";

>  eval_binop "xxx" "pow" t thy;

>  val eval_fn = (eval_binop "xxx")

>		 : string -> term -> theory -> (string * term) option;

>  val SOME (id,t') = get_pair thy "pow" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>  val eval_fn = the (assoc (!eval_list, "pow"));

>  val (SOME (id,t')) = get_pair thy "pow" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";

>  val eval_fn = the (assoc (!eval_list, "Groups.times_class.times"));

>  val (SOME (id,t')) = get_pair thy "Groups.times_class.times" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "#0 < #4";

>  val eval_fn = the (assoc (!eval_list, "op <"));

>  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>  val t = (term_of o the o (parse thy)) "#0 < #-4";

>  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "#3 is_const";

>  val eval_fn = the (assoc (!eval_list, "is'_const"));

>  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>  val t = (term_of o the o (parse thy)) "a is_const";

>  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "#6//(#8::real)";

>  val eval_fn = the (assoc (!eval_list, "cancel"));

>  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

> 

>  val t = (term_of o the o (parse thy)) "sqrt #12";

>  val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));

>  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>  val it = "sqrt #12 = #2 * sqrt #3 " : string

>

>  val t = (term_of o the o (parse thy)) "sqrt #9";

>  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

>

>  val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";

>  val eval_fn = the (assoc (!eval_list, "Tools.Nth"));

>  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;

>  Syntax.string_of_term (thy2ctxt thy) t';

*)

(* val ((op_, eval_fn),ct)=(cc,pre);

   (get_calculation_ Isac.thy (op_, eval_fn) ct) handle e => print_exn e;

   parse thy ""

   *)

(*.get a thm from an op_ somewhere in the term;

   apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711).*)

fun get_calculation_ thy (op_, eval_fn) ct =

(* val (thy, (op_, eval_fn),                           ct) = 

       (thy, (the (assoc(!calclist',"order_system"))), t);

   *)

  case get_pair thy op_ eval_fn ct of

	 NONE => ((*tracing("@@@ get_calculation: NONE, op_="^op_);

		  tracing("@@@ get_calculation: ct= ");atomty ct;*)

		  NONE)

       | SOME (thmid,t) =>

	   SOME (thmid, (make_thm o (cterm_of thy)) t);

(*

> val ct = (the o (parse thy)) "#9 is_const";

> get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;

val it = SOME ("is_const9_","(is_const 9 ) = True  [(is_const 9 ) = True]")

> val ct = (the o (parse thy)) "sqrt #9";

> get_calculation_ thy ("sqrt",the (assoc(!eval_list,"sqrt"))) ct;

val it = SOME ("sqrt_9_","sqrt 9  = 3  [sqrt 9  = 3]") : (string * thm) option

> val ct = (the o (parse thy)) "#4<#4";

> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#";

val it = SOME ("less_5_4","(5 < 4) = False  [(5 < 4) = False]")

> val ct = (the o (parse thy)) "a<#4";

> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;

val it = NONE : (string * thm) option

> val ct = (the o (parse thy)) "#5<=#4";

> get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct;

val it = SOME ("less_equal_5_4","(5 <= 4) = False  [(5 <= 4) = False]")

-------------------------------------------------------------------6.8.02:

 val thy = SqRoot.thy;

 val t = (term_of o the o (parse thy)) "1+2";

 get_calculation_ thy (the(assoc(!calc_list,"PLUS"))) t;

 val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option

-------------------------------------------------------------------6.8.02:

 val t = (term_of o the o (parse thy)) "-1";

 atomty t;

 val t = (term_of o the o (parse thy)) "0";

 atomty t;

 val t = (term_of o the o (parse thy)) "1";

 atomty t;

 val t = (term_of o the o (parse thy)) "2";

 atomty t;

 val t = (term_of o the o (parse thy)) "999999999";

 atomty t;

-------------------------------------------------------------------6.8.02:

> val ct = (the o (parse thy)) "a+#3+#4";

> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

val it = SOME ("add_3_4","a + 3 + 4 = a + 7  [a + 3 + 4 = a + 7]")

> val ct = (the o (parse thy)) "#3+(#4+a)";

> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

val it = SOME ("add_3_4","3 + (4 + a) = 7 + a  [3 + (4 + a) = 7 + a]")

> val ct = (the o (parse thy)) "a+(#3+#4)+#5";

> get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct;

val it = SOME ("add_3_4","3 + 4 = 7  [3 + 4 = 7]") : (string * thm) option

> val ct = (the o (parse thy)) "#3*(#4*a)";

> get_calculation_ thy ("Groups.times_class.times",the (assoc(!eval_list,"Groups.times_class.times"))) ct;

val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a  [3 * (4 * a) = 12 * a]")

> val ct = (the o (parse thy)) "#3 + #4^^^#2 + #5";

> get_calculation_ thy ("pow",the (assoc(!eval_list,"pow"))) ct;

val it = SOME ("4_(+2)","4 ^ 2 = 16  [4 ^ 2 = 16]") : (string * thm) option

> val ct = (the o (parse thy)) "#-4//#-2";

> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;

val it = SOME ("cancel_(-4)_(-2)","(-4) // (-2) = (+2)  [(-4) // (-2) = (+2)]")

> val ct = (the o (parse thy)) "#6//#-8";

> get_calculation_ thy ("cancel",the (assoc(!eval_list,"cancel"))) ct;

val it = SOME ("cancel_6_(-8)","6 // (-8) = (-3) // 4  [6 // (-8) = (-3) // 4]")

*) 

(*

> val ct = (the o (parse thy)) "a + 3*4";

> applicable "calculate" (Calc("Groups.times_class.times", "mult_")) ct;

val it = SOME "3 * 4 = 12  [3 * 4 = 12]" : thm option

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

> val ct = (the o (parse thy)) "3 =!= 3";

> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm

> val ct = (the o (parse thy)) "~ (3 =!= 3)";

> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

val thm = "(3 =!= 3) = True  [(3 =!= 3) = True]" : thm

> val ct = (the o (parse thy)) "3 =!= 4";

> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

val thm = "(3 =!= 4) = False  [(3 =!= 4) = False]" : thm

> val ct = (the o (parse thy)) "( 4 + (4 * x + x ^ 2) =!= (+0))";

> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

  "(4 + (4 * x + x ^ 2) =!= (+0)) = False"

> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";

> val (thmid, thm) = the (get_calculation_ thy "Atools.ident" ct);

  "(4 + (4 * x + x ^ 2) =!= (+0)) = False"

> val ct = (the o (parse thy)) "~ ( 4 + (4 * x + x ^ 2) =!= (+0))";

> val rls = eval_rls;

> val (ct,_) = the (rewrite_set_ thy false rls ct);

val ct = "True" : cterm

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

*)

(*.get a thm applying an op_ to a term;

   apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711).*)

(* val (thy, (op_, eval_fn), ct) = 

       (thy, ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"), term);

   *)

fun get_calculation1_ thy ((op_, eval_fn):cal) ct =

    case eval_fn op_ ct thy of

	NONE => NONE

      | SOME (thmid,t) =>

	SOME (thmid, (make_thm o (cterm_of thy)) t);

(*.substitute bdv in an rls and leave Calc as they are.(*28.10.02*)

fun inst_thm' subs (Thm (id, thm)) = 

    Thm (id, (*read_instantiate throws: *** No such variable in term: ?bdv*)

	 (read_instantiate subs thm) handle _ => thm)

  | inst_thm' _ calc = calc; 

fun inst_thm' (subs as (bdv,_)::_) (Thm (id, thm)) = 

    Thm (id, (tracing("@@@ inst_thm': thm= "^(string_of_thmI thm));

	      if bdv mem (vars_str o #prop o rep_thm) thm

	     then (tracing("@@@ inst_thm': read_instantiate, thm="^((string_of_thmI thm)));

		   read_instantiate subs thm)

	     else (tracing("@@@ inst_thm': not mem.. "^bdv);

		   thm)))

  | inst_thm' _ calc = calc; 

fun instantiate_rls subs 

  (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,

       asm_thm=at,rules=rules,scr=scr}:rls) =

  (Rls{preconds=preconds,rew_ord=rew_ord,erls=ev,srls=sr,calc=ca,

       asm_thm=at,scr=scr,

   rules = map (inst_thm' subs) rules}:rls);---------------------------*)

(** rewriting: ordered, conditional **)

fun mk_rule (prems,l,r) = 

    Trueprop $ (list_implies (prems, mk_equality (l,r)));

(* 'norms' a rule, e.g.

(*1*) a = 1 ==> a*(b+c) = b+c 

                =>  a = 1 ==> a*(b+c) = b+c          no change

(*2*) t = t     =>  (t=t) = True                        !!

(*3*) [| k < l; m + l = k + n |] ==> m < n

	        =>  [| k<l; m+l=k+n |] ==> m < n = True !! *)

(* val it = fn : term -> term *)

fun norm rule =

  let

    val (prems,concl)=(map strip_trueprop(Logic.strip_imp_prems rule),

		       (strip_trueprop o  Logic.strip_imp_concl)rule)

  in if is_equality concl then 

      let val (l,r) = dest_equals' concl

      in if l = r then 

	 (*2*) mk_rule(prems,concl,true_as_term)

	 else (*1*) rule end

     else (*3*) mk_rule(prems,concl,true_as_term)

  end;