1.1 --- a/src/Tools/isac/IsacKnowledge/Rational-WN.sml Wed Aug 25 15:15:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,257 +0,0 @@
1.4 -(*Stefan K.*)
1.5 -
1.6 -(*protokoll 14.3.02 --------------------------------------------------
1.7 -val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)";
1.8 -val t = (term_of o the) ct;
1.9 -atomt t;
1.10 -val ct = parse thy "not (#1+a)"; (*HOL.thy ?*)
1.11 -val t = (term_of o the) ct;
1.12 -atomt t;
1.13 -val ct = parse thy "x"; (*momentan ist alles 'real'*)
1.14 -val t = (term_of o the) ct;
1.15 -atomty t;
1.16 -val ct = parse thy "(x::int)"; (* !!! *)
1.17 -val t = (term_of o the) ct;
1.18 -atomty t;
1.19 -
1.20 -val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*)
1.21 -
1.22 -val Const ("RatArith.cancel",_) $ zaehler $ nenner = t;
1.23 ----------------------------------------------------------------------*)
1.24 -
1.25 -
1.26 -(*diese vvv funktionen kommen nach src/Isa99/term_G.sml -------------*)
1.27 -fun term2str t =
1.28 - let fun ato (Const(a,T)) n =
1.29 - "\n"^indent n^"Const ( "^a^")"
1.30 - | ato (Free (a,T)) n =
1.31 - "\n"^indent n^"Free ( "^a^", "^")"
1.32 - | ato (Var ((a,ix),T)) n =
1.33 - "\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")"
1.34 - | ato (Bound ix) n =
1.35 - "\n"^indent n^"Bound "^string_of_int ix
1.36 - | ato (Abs(a,T,body)) n =
1.37 - "\n"^indent n^"Abs( "^a^",.."^ato body (n+1)
1.38 - | ato (f$t') n = ato f n^ato t' (n+1)
1.39 - in "\n-------------"^ato t 0^"\n" end;
1.40 -fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
1.41 - handle _ => raise error ("free2int: "^term2str t))
1.42 - | free2int t = raise error ("free2int: "^term2str t);
1.43 -(*diese ^^^ funktionen kommen nach src/Isa99/term_G.sml -------------*)
1.44 -
1.45 -
1.46 -(* remark on exceptions: 'error' is implemented by Isabelle
1.47 - as the typical system error *)
1.48 -
1.49 -
1.50 -type poly = int list;
1.51 -
1.52 -(* transform a Isabelle-term t into internal polynomial format
1.53 - preconditions for t:
1.54 - a-b -> a+(-b)
1.55 - x^1 -> x
1.56 - term ordered ascending
1.57 - parentheses right side (caused by 'ordered rewriting')
1.58 - variable as power (not as product) *)
1.59 -
1.60 -fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
1.61 - if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly
1.62 - else raise error ("term2poly.1 "^term2str t1)
1.63 - | mono (t as Const ("op *",_) $ t1 $
1.64 - (Const ("RatArith.pow",_) $ t2 $ t3)) v g =
1.65 - if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1]
1.66 - else raise error ("term2poly.2 "^term2str t)
1.67 - | mono t _ _ = raise error ("term2poly.3 "^term2str t);
1.68 -
1.69 -fun poly (Const ("op +",_) $ t1 $ t2) v g =
1.70 - let val l = mono t1 v g
1.71 - in (l @ (poly t2 v ((length l) + g))) end
1.72 - | poly t v g = mono t v g;
1.73 -
1.74 -fun term2poly (t as Free (s, _)) v =
1.75 - if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]
1.76 - handle _ => NONE)
1.77 - | term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
1.78 - if t = v then SOME [0, (the o int_of_str) s1] else NONE
1.79 - | term2poly (Const ("op +",_) $ (Free (s1,_)) $ t) v =
1.80 - SOME ([(the o int_of_str) s1] @ (poly t v 1))
1.81 - | term2poly t v =
1.82 - SOME (poly t v 0) handle _ => NONE;
1.83 -
1.84 -(*tests*)
1.85 -val v = (term_of o the o (parse thy)) "x::real";
1.86 -val t = (term_of o the o (parse thy)) "#-1::real";
1.87 -term2poly t v;
1.88 -val t = (term_of o the o (parse thy)) "x::real";
1.89 -term2poly t v;
1.90 -val t = (term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
1.91 -term2poly t v;
1.92 -val t = (term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*)
1.93 -term2poly t v;
1.94 -val t = (term_of o the o (parse thy)) "x^^^#3";
1.95 -term2poly t v;
1.96 -val t = (term_of o the o (parse thy)) "#3 * x^^^#3";
1.97 -term2poly t v;
1.98 -val t = (term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";
1.99 -term2poly t v;
1.100 -val t = (term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";
1.101 -term2poly t v;
1.102 -val t = (term_of o the o (parse thy))
1.103 - "#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))";
1.104 -term2poly t v;
1.105 -val t = (term_of o the o (parse thy))
1.106 - "#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)";
1.107 -term2poly t v;
1.108 -
1.109 -
1.110 -fun is_polynomial_in t v =
1.111 - case term2poly t v of SOME _ => true | NONE => false;
1.112 -
1.113 -(* transform the internal polynomial p into an Isabelle term t
1.114 - where t meets the preconditions of term2poly
1.115 -val mk_mono =
1.116 - fn : typ -> of the coefficients
1.117 - typ -> of the unknown
1.118 - typ -> of the monomial and polynomial
1.119 - typ -> of the exponent of the unknown
1.120 - int -> the coefficient <> 0
1.121 - string -> the unknown
1.122 - int -> the degree, i.e. the value of the exponent
1.123 - term
1.124 -remark: all the typs above are "RealDef.real" due to the typs of * + ^
1.125 -which may change in the future
1.126 -*)
1.127 -fun mk_mono cT vT pT eT c v g =
1.128 - case g of
1.129 - 0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)
1.130 - | 1 => if c = 1 then Free (v, vT)
1.131 - else Const ("op *", [cT, vT]--->pT) $
1.132 - Free (str_of_int c, cT) $ Free (v, vT)
1.133 - | n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $
1.134 - Free (v, vT) $ Free (str_of_int g, eT))
1.135 - else Const ("op *", [cT, vT]--->pT) $
1.136 - Free (str_of_int c, cT) $
1.137 - (Const ("RatArith.pow", [vT, eT]--->pT) $
1.138 - Free (v, vT) $ Free (str_of_int g, eT));
1.139 -(*tests*)
1.140 -val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
1.141 -val eT = HOLogic.realT;
1.142 -val t = mk_mono cT vT pT eT ~5 "x" 5;
1.143 -(cterm_of thy) t;
1.144 -val t = mk_mono cT vT pT eT ~1 "x" 0;
1.145 -(cterm_of thy) t;
1.146 -val t = mk_mono cT vT pT eT 1 "x" 1;
1.147 -(cterm_of thy) t;
1.148 -
1.149 -
1.150 -fun mk_sum pT t1 t2 = Const ("op +", [pT, pT]--->pT) $ t1 $ t2;
1.151 -
1.152 -
1.153 -fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0
1.154 - | poly2term cT vT pT eT (p:poly) v =
1.155 - let
1.156 - fun mk_poly cT vT pT eT [] t v g = t
1.157 - | mk_poly cT vT pT eT [p] t v g =
1.158 - if p = 0 then t
1.159 - else mk_sum pT (mk_mono cT vT pT eT p v g) t
1.160 - | mk_poly cT vT pT eT (p::ps) t v g =
1.161 - if p = 0 then mk_poly cT vT pT eT ps t v (g-1)
1.162 - else mk_poly cT vT pT eT ps
1.163 - (mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1)
1.164 - val (p'::ps') = rev p
1.165 - val g = (length p) - 1
1.166 - in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end;
1.167 -
1.168 -(*tests*)
1.169 -val t = poly2term cT vT pT eT [~1] "x";
1.170 -(cterm_of thy) t;
1.171 -val t = poly2term cT vT pT eT [0,1] "x";
1.172 -(cterm_of thy) t;
1.173 -val t = poly2term cT vT pT eT [0,0,0,1] "x";
1.174 -(cterm_of thy) t;
1.175 -val t = poly2term cT vT pT eT [0,0,0,3] "x";
1.176 -(cterm_of thy) t;
1.177 -val t = poly2term cT vT pT eT [~1,0,0,3] "x";
1.178 -(cterm_of thy) t;
1.179 -val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
1.180 -(cterm_of thy) t;
1.181 -val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
1.182 -(cterm_of thy) t;
1.183 -val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
1.184 -(cterm_of thy) t;
1.185 -
1.186 -"***************************************************************************";
1.187 -"* reverse-rewriting 12.8.02 *";
1.188 -"***************************************************************************";
1.189 -fun rewrite_set_' thy rls put_asm ruless ct =
1.190 - case ruless of
1.191 - Rrls _ => raise error "rewrite_set_' not for Rrls"
1.192 - | Rls _ =>
1.193 - let
1.194 - datatype switch = Appl | Noap;
1.195 - fun rew_once ruls asm ct Noap [] = (ct,asm)
1.196 - | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
1.197 - | rew_once ruls asm ct apno (rul::thms) =
1.198 - case rul of
1.199 - Thm (thmid, thm) =>
1.200 - (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.201 - rls put_asm (thm_of_thm rul) ct of
1.202 - NONE => rew_once ruls asm ct apno thms
1.203 - | SOME (ct',asm') =>
1.204 - rew_once ruls (asm union asm') ct' Appl (rul::thms))
1.205 - | Calc (cc as (op_,_)) =>
1.206 - (case get_calculation_ thy cc ct of
1.207 - NONE => rew_once ruls asm ct apno thms
1.208 - | SOME (thmid, thm') =>
1.209 - let
1.210 - val pairopt =
1.211 - rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.212 - rls put_asm thm' ct;
1.213 - val _ = if pairopt <> NONE then ()
1.214 - else raise error("rewrite_set_, rewrite_ \""^
1.215 - (string_of_thmI thm')^"\" \""^
1.216 - (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
1.217 - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
1.218 - val ruls = (#rules o rep_rls) ruless;
1.219 - val (ct',asm') = rew_once ruls [] ct Noap ruls;
1.220 - in if ct = ct' then NONE else SOME (ct',asm') end;
1.221 -
1.222 -(*
1.223 -fun reverse_rewrite t1 t2 rls =
1.224 -*)
1.225 -fun rewrite_set_' thy rls put_asm ruless ct =
1.226 - case ruless of
1.227 - Rrls _ => raise error "rewrite_set_' not for Rrls"
1.228 - | Rls _ =>
1.229 - let
1.230 - datatype switch = Appl | Noap;
1.231 - fun rew_once ruls asm ct Noap [] = (ct,asm)
1.232 - | rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
1.233 - | rew_once ruls asm ct apno (rul::thms) =
1.234 - case rul of
1.235 - Thm (thmid, thm) =>
1.236 - (case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.237 - rls put_asm (thm_of_thm rul) ct of
1.238 - NONE => rew_once ruls asm ct apno thms
1.239 - | SOME (ct',asm') =>
1.240 - rew_once ruls (asm union asm') ct' Appl (rul::thms))
1.241 - | Calc (cc as (op_,_)) =>
1.242 - (case get_calculation_ thy cc ct of
1.243 - NONE => rew_once ruls asm ct apno thms
1.244 - | SOME (thmid, thm') =>
1.245 - let
1.246 - val pairopt =
1.247 - rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
1.248 - rls put_asm thm' ct;
1.249 - val _ = if pairopt <> NONE then ()
1.250 - else raise error("rewrite_set_, rewrite_ \""^
1.251 - (string_of_thmI thm')^"\" \""^
1.252 - (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
1.253 - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
1.254 - val ruls = (#rules o rep_rls) ruless;
1.255 - val (ct',asm') = rew_once ruls [] ct Noap ruls;
1.256 - in if ct = ct' then NONE else SOME (ct',asm') end;
1.257 -
1.258 - realpow_two;
1.259 - real_mult_div_cancel1;
1.260 -