1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/Rational-WN.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,257 @@
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 thy t;
1.16 +val ct = parse thy "(x::int)"; (* !!! *)
1.17 +val t = (term_of o the) ct;
1.18 +atomty thy 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 (sign_of thy) t;
1.144 +val t = mk_mono cT vT pT eT ~1 "x" 0;
1.145 +cterm_of (sign_of thy) t;
1.146 +val t = mk_mono cT vT pT eT 1 "x" 1;
1.147 +cterm_of (sign_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 (sign_of thy) t;
1.171 +val t = poly2term cT vT pT eT [0,1] "x";
1.172 +cterm_of (sign_of thy) t;
1.173 +val t = poly2term cT vT pT eT [0,0,0,1] "x";
1.174 +cterm_of (sign_of thy) t;
1.175 +val t = poly2term cT vT pT eT [0,0,0,3] "x";
1.176 +cterm_of (sign_of thy) t;
1.177 +val t = poly2term cT vT pT eT [~1,0,0,3] "x";
1.178 +cterm_of (sign_of thy) t;
1.179 +val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
1.180 +cterm_of (sign_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 (sign_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 (sign_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_thm thm')^"\" \""^
1.216 + (Sign.string_of_term (sign_of 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_thm thm')^"\" \""^
1.252 + (Sign.string_of_term (sign_of 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 +