wneuper/isac: src/sml/IsacKnowledge/Rational-WN.sml@0bf7c1333a35

     1 (*Stefan K.*)

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

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

     5 val t = (term_of o the) ct;

     6 atomt t;

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

     8 val t = (term_of o the) ct;

     9 atomt t;

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

    11 val t = (term_of o the) ct;

    12 atomty t;

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

    14 val t = (term_of o the) ct;

    15 atomty t;

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

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

    20 ---------------------------------------------------------------------*)

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

    24 fun term2str t =

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

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

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

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

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

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

    31 	  | ato (Bound ix)       n =

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

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

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

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

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

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

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

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

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

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

    44    as the typical system error                             *)

    47 type poly = int list;

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

    50    preconditions for t:

    51      a-b  -> a+(-b)

    52      x^1 -> x

    53      term ordered ascending

    54      parentheses right side (caused by 'ordered rewriting')

    55      variable as power (not as product) *)

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

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

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

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

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

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

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

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

    66 fun poly (Const ("op +",_) $ t1 $ t2) v g =

    67     let val l = mono t1 v g

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

    69   | poly t v g = mono t v g;

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

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

    73 				  handle _ => None)

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

    75     if t = v then Some [0, (the o int_of_str) s1] else None

    76   | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v =

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

    78   | term2poly t v =

    79     Some (poly t v 0) handle _ => None;

    81 (*tests*)

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

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

    84 term2poly t v;

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

    86 term2poly t v;

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

    88 term2poly t v;

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

    90 term2poly t v;

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

    92 term2poly t v;

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

    94 term2poly t v;

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

    96 term2poly t v;

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

    98 term2poly t v;

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

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

   101 term2poly t v;

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

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

   104 term2poly t v;

   107 fun is_polynomial_in t v =

   108     case term2poly t v of Some _ => true | None => false;

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

   111    where t meets the preconditions of term2poly

   112 val mk_mono =

   113     fn : typ ->     of the coefficients

   114 	 typ ->     of the unknown

   115 	 typ ->     of the monomial and polynomial

   116 	 typ ->     of the exponent of the unknown

   117 	 int ->     the coefficient <> 0

   118 	 string ->  the unknown

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

   120 	 term

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

   122 which may change in the future

   123 *)

   124 fun mk_mono cT vT pT eT c v g =

   125     case g of

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

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

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

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

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

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

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

   133 			Free (str_of_int c, cT) $

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

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

   136 (*tests*)

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

   138 val eT = HOLogic.realT;

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

   140 cterm_of (sign_of thy) t;

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

   142 cterm_of (sign_of thy) t;

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

   144 cterm_of (sign_of thy) t;

   147 fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;

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

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

   152   let

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

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

   155 	if p = 0 then t

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

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

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

   159 	else mk_poly cT vT pT eT ps

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

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

   162     val g = (length p) - 1

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

   165 (*tests*)

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

   167 cterm_of (sign_of thy) t;

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

   169 cterm_of (sign_of thy) t;

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

   171 cterm_of (sign_of thy) t;

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

   173 cterm_of (sign_of thy) t;

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

   175 cterm_of (sign_of thy) t;

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

   177 cterm_of (sign_of thy) t;

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

   179 cterm_of (sign_of thy) t;

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

   181 cterm_of (sign_of thy) t;

   183 "***************************************************************************";

   184 "*                            reverse-rewriting 12.8.02                    *";

   185 "***************************************************************************";

   186 fun rewrite_set_' thy rls put_asm ruless ct =

   187     case ruless of

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

   189       | Rls _ =>

   190   let

   191     datatype switch = Appl | Noap;

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

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

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

   195       case rul of

   196 	Thm (thmid, thm) =>

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

   198 	     rls put_asm (thm_of_thm rul) ct of

   199 	     None => rew_once ruls asm ct apno thms

   200 	   | Some (ct',asm') =>

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

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

   203 	  (case get_calculation_ thy cc ct of

   204 	       None => rew_once ruls asm ct apno thms

   205 	   | Some (thmid, thm') =>

   206 	       let

   207 		 val pairopt =

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

   209 		   rls put_asm thm' ct;

   210 		 val _ = if pairopt <> None then ()

   211 			 else raise error("rewrite_set_, rewrite_ \""^

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

   213 			 (Sign.string_of_term (sign_of thy) ct)^"\" = None")

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

   215     val ruls = (#rules o rep_rls) ruless;

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

   217   in if ct = ct' then None else Some (ct',asm') end;

   219 (*

   220 fun reverse_rewrite t1 t2 rls =

   221 *)

   222 fun rewrite_set_' thy rls put_asm ruless ct =

   223     case ruless of

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

   225       | Rls _ =>

   226   let

   227     datatype switch = Appl | Noap;

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

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

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

   231       case rul of

   232 	Thm (thmid, thm) =>

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

   234 	     rls put_asm (thm_of_thm rul) ct of

   235 	     None => rew_once ruls asm ct apno thms

   236 	   | Some (ct',asm') =>

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

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

   239 	  (case get_calculation_ thy cc ct of

   240 	       None => rew_once ruls asm ct apno thms

   241 	   | Some (thmid, thm') =>

   242 	       let

   243 		 val pairopt =

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

   245 		   rls put_asm thm' ct;

   246 		 val _ = if pairopt <> None then ()

   247 			 else raise error("rewrite_set_, rewrite_ \""^

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

   249 			 (Sign.string_of_term (sign_of thy) ct)^"\" = None")

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

   251     val ruls = (#rules o rep_rls) ruless;

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

   253   in if ct = ct' then None else Some (ct',asm') end;

   255  realpow_two;

   256  real_mult_div_cancel1;

author	wneuper
	Fri, 03 Nov 2006 10:51:51 +0100
branch	start_Take
changeset 680	0bf7c1333a35
parent 365	022b8b845fbe
permissions	-rw-r--r--