(*Stefan K.*)

(*protokoll 14.3.02 --------------------------------------------------

val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)";

val t = (term_of o the) ct;

atomt t;

val ct = parse thy "not (#1+a)"; (*HOL.thy ?*)

val t = (term_of o the) ct;

atomt t;

val ct = parse thy "x"; (*momentan ist alles 'real'*)

val t = (term_of o the) ct;

atomty t;

val ct = parse thy "(x::int)"; (* !!! *)

val t = (term_of o the) ct;

atomty t;

val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*)

val Const ("RatArith.cancel",_) $ zaehler $ nenner = t;

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

(*diese vvv funktionen kommen nach src/Isa99/termC.sml -------------*)

fun term2str t =

    let fun ato (Const(a,T))     n = 

	    "\n"^indent n^"Const ( "^a^")"

	  | ato (Free (a,T))     n =  

	    "\n"^indent n^"Free ( "^a^", "^")"

	  | ato (Var ((a,ix),T)) n =

	    "\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")"

	  | ato (Bound ix)       n = 

	    "\n"^indent n^"Bound "^string_of_int ix

	  | ato (Abs(a,T,body))  n = 

	    "\n"^indent n^"Abs( "^a^",.."^ato body (n+1)

	  | ato (f$t')           n = ato f n^ato t' (n+1)

    in "\n-------------"^ato t 0^"\n" end;

fun free2int (t as Free (s, _)) = (((the o int_of_str) s)

    handle _ => error ("free2int: "^term2str t))

  | free2int t = error ("free2int: "^term2str t);

(*diese ^^^ funktionen kommen nach src/Isa99/termC.sml -------------*)

(* remark on exceptions: 'error' is implemented by Isabelle 

   as the typical system error                             *)

type poly = int list;

(* transform a Isabelle-term t into internal polynomial format

   preconditions for t: 

     a-b  -> a+(-b)

     x^1 -> x

     term ordered ascending

     parentheses right side (caused by 'ordered rewriting')

     variable as power (not as product) *)

fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =

    if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly 

    else error ("term2poly.1 "^term2str t1)

  | mono (t as Const ("op *",_) $ t1 $ 

	    (Const ("RatArith.pow",_) $ t2 $ t3)) v g =

    if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1] 

    else error ("term2poly.2 "^term2str t)

  | mono t _ _ = error ("term2poly.3 "^term2str t);

fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g = 

    let val l = mono t1 v g

    in (l @ (poly t2 v ((length l) + g))) end

  | poly t v g = mono t v g;

fun term2poly (t as Free (s, _)) v =

    if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]

				  handle _ => NONE)

  | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =

    if t = v then SOME [0, (the o int_of_str) s1] else NONE

  | term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v = 

    SOME ([(the o int_of_str) s1] @ (poly t v 1))

  | term2poly t v = 

    SOME (poly t v 0) handle _ => NONE;

(*tests*)

val v = (term_of o the o (parse thy)) "x::real";

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

term2poly t v;

val t = (term_of o the o (parse thy)) "x::real";

term2poly t v;

val t = (term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)

term2poly t v;

val t = (term_of o the o (parse thy)) "x^^^#1";       (*FIXME: drop it*)

term2poly t v;

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

term2poly t v;

val t = (term_of o the o (parse thy)) "#3 * x^^^#3";

term2poly t v;

val t = (term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";

term2poly t v;

val t = (term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";

term2poly t v;

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

	    "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))";

term2poly t v;

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

	    "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)";

term2poly t v;

fun is_polynomial_in t v =

    case term2poly t v of SOME _ => true | NONE => false;

(* transform the internal polynomial p into an Isabelle term t

   where t meets the preconditions of term2poly

val mk_mono = 

    fn : typ ->     of the coefficients

	 typ ->     of the unknown

	 typ ->     of the monomial and polynomial

	 typ ->     of the exponent of the unknown

	 int ->     the coefficient <> 0

	 string ->  the unknown

	 int ->     the degree, i.e. the value of the exponent

	 term 

remark: all the typs above are "RealDef.real" due to the typs of * + ^

which may change in the future

*)

fun mk_mono cT vT pT eT c v g = 

    case g of

	0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)

      | 1 => if c = 1 then Free (v, vT)

	     else Const ("op *", [cT, vT]--->pT) $

			Free (str_of_int c, cT) $ Free (v, vT)

      | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $ 

			  Free (v, vT) $ Free (str_of_int g, eT))

	     else Const ("op *", [cT, vT]--->pT) $ 

			Free (str_of_int c, cT) $ 

			(Const ("RatArith.pow", [vT, eT]--->pT) $ 

			       Free (v, vT) $ Free (str_of_int g, eT));

(*tests*)

val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;

val eT = HOLogic.realT;

val t = mk_mono cT vT pT eT ~5 "x" 5;

(cterm_of thy) t;

val t = mk_mono cT vT pT eT ~1 "x" 0;

(cterm_of thy) t;

val t = mk_mono cT vT pT eT 1 "x" 1;

(cterm_of thy) t;

fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;

fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0

  | poly2term cT vT pT eT (p:poly) v = 

  let 

    fun mk_poly cT vT pT eT [] t v g = t

      | mk_poly cT vT pT eT [p] t v g = 

	if p = 0 then t

	else mk_sum pT (mk_mono cT vT pT eT p v g) t

      | mk_poly cT vT pT eT (p::ps) t v g =

	if p = 0 then mk_poly cT vT pT eT ps t v (g-1)

	else mk_poly cT vT pT eT ps 

		     (mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1)

    val (p'::ps') = rev p

    val g = (length p) - 1

    in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end;

(*tests*)    

val t = poly2term cT vT pT eT [~1] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [0,1] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [0,0,0,1] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [0,0,0,3] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [~1,0,0,3] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";

(cterm_of thy) t;

val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";

(cterm_of thy) t;

"***************************************************************************";

"*                            reverse-rewriting 12.8.02                    *";

"***************************************************************************";

fun rewrite_set_' thy rls put_asm ruless ct =

    case ruless of

	Rrls _ => error "rewrite_set_' not for Rrls"

      | Rls _ =>

  let

    datatype switch = Appl | Noap;

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

      | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls

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

      case rul of

	Thm (thmid, thm) =>

	  (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) 

	     rls put_asm (thm_of_thm rul) ct of

	     NONE => rew_once ruls asm ct apno thms

	   | SOME (ct',asm') => 

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

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

	  (case get_calculation_ thy cc ct of

	       NONE => rew_once ruls asm ct apno thms

	   | SOME (thmid, thm') => 

	       let 

		 val pairopt = 

		   rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) 

		   rls put_asm thm' ct;

		 val _ = if pairopt <> NONE then () 

			 else error("rewrite_set_, rewrite_ \""^

			 (string_of_thmI thm')^"\" \""^

			 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")

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

    val ruls = (#rules o rep_rls) ruless;

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

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

(*

fun reverse_rewrite t1 t2 rls =

*)

fun rewrite_set_' thy rls put_asm ruless ct =

    case ruless of

	Rrls _ => error "rewrite_set_' not for Rrls"

      | Rls _ =>

  let

    datatype switch = Appl | Noap;

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

      | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls

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

      case rul of

	Thm (thmid, thm) =>

	  (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) 

	     rls put_asm (thm_of_thm rul) ct of

	     NONE => rew_once ruls asm ct apno thms

	   | SOME (ct',asm') => 

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

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

	  (case get_calculation_ thy cc ct of

	       NONE => rew_once ruls asm ct apno thms

	   | SOME (thmid, thm') => 

	       let 

		 val pairopt = 

		   rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) 

		   rls put_asm thm' ct;

		 val _ = if pairopt <> NONE then () 

			 else error("rewrite_set_, rewrite_ \""^

			 (string_of_thmI thm')^"\" \""^

			 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")

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

    val ruls = (#rules o rep_rls) ruless;

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

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

 realpow_two;

 real_mult_div_cancel1;