neuper@37906
|
1 |
(*Stefan K.*)
|
neuper@37906
|
2 |
|
neuper@37906
|
3 |
(*protokoll 14.3.02 --------------------------------------------------
|
neuper@37906
|
4 |
val ct = parse thy "(a + #1)//(#2*a^^^#2 - #2)";
|
neuper@37906
|
5 |
val t = (term_of o the) ct;
|
neuper@37906
|
6 |
atomt t;
|
neuper@37906
|
7 |
val ct = parse thy "not (#1+a)"; (*HOL.thy ?*)
|
neuper@37906
|
8 |
val t = (term_of o the) ct;
|
neuper@37906
|
9 |
atomt t;
|
neuper@37906
|
10 |
val ct = parse thy "x"; (*momentan ist alles 'real'*)
|
neuper@37906
|
11 |
val t = (term_of o the) ct;
|
neuper@37906
|
12 |
atomty t;
|
neuper@37906
|
13 |
val ct = parse thy "(x::int)"; (* !!! *)
|
neuper@37906
|
14 |
val t = (term_of o the) ct;
|
neuper@37906
|
15 |
atomty t;
|
neuper@37906
|
16 |
|
neuper@37906
|
17 |
val ct = parse thy "(x::int)*(y::real)"; (*momentan ist alles 'real'*)
|
neuper@37906
|
18 |
|
neuper@37906
|
19 |
val Const ("RatArith.cancel",_) $ zaehler $ nenner = t;
|
neuper@37906
|
20 |
---------------------------------------------------------------------*)
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
|
neuper@37947
|
23 |
(*diese vvv funktionen kommen nach src/Isa99/term.sml -------------*)
|
neuper@37906
|
24 |
fun term2str t =
|
neuper@37906
|
25 |
let fun ato (Const(a,T)) n =
|
neuper@37906
|
26 |
"\n"^indent n^"Const ( "^a^")"
|
neuper@37906
|
27 |
| ato (Free (a,T)) n =
|
neuper@37906
|
28 |
"\n"^indent n^"Free ( "^a^", "^")"
|
neuper@37906
|
29 |
| ato (Var ((a,ix),T)) n =
|
neuper@37906
|
30 |
"\n"^indent n^"Var (("^a^", "^string_of_int ix^"), "^")"
|
neuper@37906
|
31 |
| ato (Bound ix) n =
|
neuper@37906
|
32 |
"\n"^indent n^"Bound "^string_of_int ix
|
neuper@37906
|
33 |
| ato (Abs(a,T,body)) n =
|
neuper@37906
|
34 |
"\n"^indent n^"Abs( "^a^",.."^ato body (n+1)
|
neuper@37906
|
35 |
| ato (f$t') n = ato f n^ato t' (n+1)
|
neuper@37906
|
36 |
in "\n-------------"^ato t 0^"\n" end;
|
neuper@37906
|
37 |
fun free2int (t as Free (s, _)) = (((the o int_of_str) s)
|
neuper@37906
|
38 |
handle _ => raise error ("free2int: "^term2str t))
|
neuper@37906
|
39 |
| free2int t = raise error ("free2int: "^term2str t);
|
neuper@37947
|
40 |
(*diese ^^^ funktionen kommen nach src/Isa99/term.sml -------------*)
|
neuper@37906
|
41 |
|
neuper@37906
|
42 |
|
neuper@37906
|
43 |
(* remark on exceptions: 'error' is implemented by Isabelle
|
neuper@37906
|
44 |
as the typical system error *)
|
neuper@37906
|
45 |
|
neuper@37906
|
46 |
|
neuper@37906
|
47 |
type poly = int list;
|
neuper@37906
|
48 |
|
neuper@37906
|
49 |
(* transform a Isabelle-term t into internal polynomial format
|
neuper@37906
|
50 |
preconditions for t:
|
neuper@37906
|
51 |
a-b -> a+(-b)
|
neuper@37906
|
52 |
x^1 -> x
|
neuper@37906
|
53 |
term ordered ascending
|
neuper@37906
|
54 |
parentheses right side (caused by 'ordered rewriting')
|
neuper@37906
|
55 |
variable as power (not as product) *)
|
neuper@37906
|
56 |
|
neuper@37906
|
57 |
fun mono (Const ("RatArith.pow",_) $ t1 $ t2) v g =
|
neuper@37906
|
58 |
if t1 = v then ((replicate ((free2int t2) - g) 0) @ [1]) : poly
|
neuper@37906
|
59 |
else raise error ("term2poly.1 "^term2str t1)
|
neuper@37906
|
60 |
| mono (t as Const ("op *",_) $ t1 $
|
neuper@37906
|
61 |
(Const ("RatArith.pow",_) $ t2 $ t3)) v g =
|
neuper@37906
|
62 |
if t2 = v then (replicate ((free2int t3) - g) 0) @ [free2int t1]
|
neuper@37906
|
63 |
else raise error ("term2poly.2 "^term2str t)
|
neuper@37906
|
64 |
| mono t _ _ = raise error ("term2poly.3 "^term2str t);
|
neuper@37906
|
65 |
|
neuper@38014
|
66 |
fun poly (Const ("Groups.plus_class.plus",_) $ t1 $ t2) v g =
|
neuper@37906
|
67 |
let val l = mono t1 v g
|
neuper@37906
|
68 |
in (l @ (poly t2 v ((length l) + g))) end
|
neuper@37906
|
69 |
| poly t v g = mono t v g;
|
neuper@37906
|
70 |
|
neuper@37906
|
71 |
fun term2poly (t as Free (s, _)) v =
|
neuper@37926
|
72 |
if t = v then SOME ([0,1] : poly) else (SOME [(the o int_of_str) s]
|
neuper@37926
|
73 |
handle _ => NONE)
|
neuper@37906
|
74 |
| term2poly (Const ("op *",_) $ (Free (s1,_)) $ (t as Free (s2,_))) v =
|
neuper@37926
|
75 |
if t = v then SOME [0, (the o int_of_str) s1] else NONE
|
neuper@38014
|
76 |
| term2poly (Const ("Groups.plus_class.plus",_) $ (Free (s1,_)) $ t) v =
|
neuper@37926
|
77 |
SOME ([(the o int_of_str) s1] @ (poly t v 1))
|
neuper@37906
|
78 |
| term2poly t v =
|
neuper@37926
|
79 |
SOME (poly t v 0) handle _ => NONE;
|
neuper@37906
|
80 |
|
neuper@37906
|
81 |
(*tests*)
|
neuper@37906
|
82 |
val v = (term_of o the o (parse thy)) "x::real";
|
neuper@37906
|
83 |
val t = (term_of o the o (parse thy)) "#-1::real";
|
neuper@37906
|
84 |
term2poly t v;
|
neuper@37906
|
85 |
val t = (term_of o the o (parse thy)) "x::real";
|
neuper@37906
|
86 |
term2poly t v;
|
neuper@37906
|
87 |
val t = (term_of o the o (parse thy)) "#1 * x::real"; (*FIXME: drop it*)
|
neuper@37906
|
88 |
term2poly t v;
|
neuper@37906
|
89 |
val t = (term_of o the o (parse thy)) "x^^^#1"; (*FIXME: drop it*)
|
neuper@37906
|
90 |
term2poly t v;
|
neuper@37906
|
91 |
val t = (term_of o the o (parse thy)) "x^^^#3";
|
neuper@37906
|
92 |
term2poly t v;
|
neuper@37906
|
93 |
val t = (term_of o the o (parse thy)) "#3 * x^^^#3";
|
neuper@37906
|
94 |
term2poly t v;
|
neuper@37906
|
95 |
val t = (term_of o the o (parse thy)) "#-1 + #3 * x^^^#3";
|
neuper@37906
|
96 |
term2poly t v;
|
neuper@37906
|
97 |
val t = (term_of o the o (parse thy)) "#-1 + (#3 * x^^^#3 + #5 * x^^^#5)";
|
neuper@37906
|
98 |
term2poly t v;
|
neuper@37906
|
99 |
val t = (term_of o the o (parse thy))
|
neuper@37906
|
100 |
"#-1 + (#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7))";
|
neuper@37906
|
101 |
term2poly t v;
|
neuper@37906
|
102 |
val t = (term_of o the o (parse thy))
|
neuper@37906
|
103 |
"#3 * x^^^#3 + (#5 * x^^^#5 + #7 * x^^^#7)";
|
neuper@37906
|
104 |
term2poly t v;
|
neuper@37906
|
105 |
|
neuper@37906
|
106 |
|
neuper@37906
|
107 |
fun is_polynomial_in t v =
|
neuper@37926
|
108 |
case term2poly t v of SOME _ => true | NONE => false;
|
neuper@37906
|
109 |
|
neuper@37906
|
110 |
(* transform the internal polynomial p into an Isabelle term t
|
neuper@37906
|
111 |
where t meets the preconditions of term2poly
|
neuper@37906
|
112 |
val mk_mono =
|
neuper@37906
|
113 |
fn : typ -> of the coefficients
|
neuper@37906
|
114 |
typ -> of the unknown
|
neuper@37906
|
115 |
typ -> of the monomial and polynomial
|
neuper@37906
|
116 |
typ -> of the exponent of the unknown
|
neuper@37906
|
117 |
int -> the coefficient <> 0
|
neuper@37906
|
118 |
string -> the unknown
|
neuper@37906
|
119 |
int -> the degree, i.e. the value of the exponent
|
neuper@37906
|
120 |
term
|
neuper@37906
|
121 |
remark: all the typs above are "RealDef.real" due to the typs of * + ^
|
neuper@37906
|
122 |
which may change in the future
|
neuper@37906
|
123 |
*)
|
neuper@37906
|
124 |
fun mk_mono cT vT pT eT c v g =
|
neuper@37906
|
125 |
case g of
|
neuper@37906
|
126 |
0 => Free (str_of_int c, cT) (*will cause problems with diff.typs*)
|
neuper@37906
|
127 |
| 1 => if c = 1 then Free (v, vT)
|
neuper@37906
|
128 |
else Const ("op *", [cT, vT]--->pT) $
|
neuper@37906
|
129 |
Free (str_of_int c, cT) $ Free (v, vT)
|
neuper@37906
|
130 |
| n => if c = 1 then (Const ("RatArith.pow", [vT, eT]--->pT) $
|
neuper@37906
|
131 |
Free (v, vT) $ Free (str_of_int g, eT))
|
neuper@37906
|
132 |
else Const ("op *", [cT, vT]--->pT) $
|
neuper@37906
|
133 |
Free (str_of_int c, cT) $
|
neuper@37906
|
134 |
(Const ("RatArith.pow", [vT, eT]--->pT) $
|
neuper@37906
|
135 |
Free (v, vT) $ Free (str_of_int g, eT));
|
neuper@37906
|
136 |
(*tests*)
|
neuper@37906
|
137 |
val cT = HOLogic.realT; val vT = HOLogic.realT; val pT = HOLogic.realT;
|
neuper@37906
|
138 |
val eT = HOLogic.realT;
|
neuper@37906
|
139 |
val t = mk_mono cT vT pT eT ~5 "x" 5;
|
neuper@37938
|
140 |
(cterm_of thy) t;
|
neuper@37906
|
141 |
val t = mk_mono cT vT pT eT ~1 "x" 0;
|
neuper@37938
|
142 |
(cterm_of thy) t;
|
neuper@37906
|
143 |
val t = mk_mono cT vT pT eT 1 "x" 1;
|
neuper@37938
|
144 |
(cterm_of thy) t;
|
neuper@37906
|
145 |
|
neuper@37906
|
146 |
|
neuper@38014
|
147 |
fun mk_sum pT t1 t2 = Const ("Groups.plus_class.plus", [pT, pT]--->pT) $ t1 $ t2;
|
neuper@37906
|
148 |
|
neuper@37906
|
149 |
|
neuper@37906
|
150 |
fun poly2term cT vT pT eT ([p]:poly) v = mk_mono cT vT pT eT p v 0
|
neuper@37906
|
151 |
| poly2term cT vT pT eT (p:poly) v =
|
neuper@37906
|
152 |
let
|
neuper@37906
|
153 |
fun mk_poly cT vT pT eT [] t v g = t
|
neuper@37906
|
154 |
| mk_poly cT vT pT eT [p] t v g =
|
neuper@37906
|
155 |
if p = 0 then t
|
neuper@37906
|
156 |
else mk_sum pT (mk_mono cT vT pT eT p v g) t
|
neuper@37906
|
157 |
| mk_poly cT vT pT eT (p::ps) t v g =
|
neuper@37906
|
158 |
if p = 0 then mk_poly cT vT pT eT ps t v (g-1)
|
neuper@37906
|
159 |
else mk_poly cT vT pT eT ps
|
neuper@37906
|
160 |
(mk_sum pT (mk_mono cT vT pT eT p v g) t) v (g-1)
|
neuper@37906
|
161 |
val (p'::ps') = rev p
|
neuper@37906
|
162 |
val g = (length p) - 1
|
neuper@37906
|
163 |
in mk_poly cT vT pT eT ps' (mk_mono cT vT pT eT p' v g) v (g-1) end;
|
neuper@37906
|
164 |
|
neuper@37906
|
165 |
(*tests*)
|
neuper@37906
|
166 |
val t = poly2term cT vT pT eT [~1] "x";
|
neuper@37938
|
167 |
(cterm_of thy) t;
|
neuper@37906
|
168 |
val t = poly2term cT vT pT eT [0,1] "x";
|
neuper@37938
|
169 |
(cterm_of thy) t;
|
neuper@37906
|
170 |
val t = poly2term cT vT pT eT [0,0,0,1] "x";
|
neuper@37938
|
171 |
(cterm_of thy) t;
|
neuper@37906
|
172 |
val t = poly2term cT vT pT eT [0,0,0,3] "x";
|
neuper@37938
|
173 |
(cterm_of thy) t;
|
neuper@37906
|
174 |
val t = poly2term cT vT pT eT [~1,0,0,3] "x";
|
neuper@37938
|
175 |
(cterm_of thy) t;
|
neuper@37906
|
176 |
val t = poly2term cT vT pT eT [~1,0,0,3,0,5] "x";
|
neuper@37938
|
177 |
(cterm_of thy) t;
|
neuper@37906
|
178 |
val t = poly2term cT vT pT eT [~1,0,0,3,0,5,0,7] "x";
|
neuper@37938
|
179 |
(cterm_of thy) t;
|
neuper@37906
|
180 |
val t = poly2term cT vT pT eT [0,0,0,3,0,5,0,7] "x";
|
neuper@37938
|
181 |
(cterm_of thy) t;
|
neuper@37906
|
182 |
|
neuper@37906
|
183 |
"***************************************************************************";
|
neuper@37906
|
184 |
"* reverse-rewriting 12.8.02 *";
|
neuper@37906
|
185 |
"***************************************************************************";
|
neuper@37906
|
186 |
fun rewrite_set_' thy rls put_asm ruless ct =
|
neuper@37906
|
187 |
case ruless of
|
neuper@37906
|
188 |
Rrls _ => raise error "rewrite_set_' not for Rrls"
|
neuper@37906
|
189 |
| Rls _ =>
|
neuper@37906
|
190 |
let
|
neuper@37906
|
191 |
datatype switch = Appl | Noap;
|
neuper@37906
|
192 |
fun rew_once ruls asm ct Noap [] = (ct,asm)
|
neuper@37906
|
193 |
| rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
|
neuper@37906
|
194 |
| rew_once ruls asm ct apno (rul::thms) =
|
neuper@37906
|
195 |
case rul of
|
neuper@37906
|
196 |
Thm (thmid, thm) =>
|
neuper@37906
|
197 |
(case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
|
neuper@37906
|
198 |
rls put_asm (thm_of_thm rul) ct of
|
neuper@37926
|
199 |
NONE => rew_once ruls asm ct apno thms
|
neuper@37926
|
200 |
| SOME (ct',asm') =>
|
neuper@37906
|
201 |
rew_once ruls (asm union asm') ct' Appl (rul::thms))
|
neuper@37906
|
202 |
| Calc (cc as (op_,_)) =>
|
neuper@37906
|
203 |
(case get_calculation_ thy cc ct of
|
neuper@37926
|
204 |
NONE => rew_once ruls asm ct apno thms
|
neuper@37926
|
205 |
| SOME (thmid, thm') =>
|
neuper@37906
|
206 |
let
|
neuper@37906
|
207 |
val pairopt =
|
neuper@37906
|
208 |
rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
|
neuper@37906
|
209 |
rls put_asm thm' ct;
|
neuper@37926
|
210 |
val _ = if pairopt <> NONE then ()
|
neuper@37906
|
211 |
else raise error("rewrite_set_, rewrite_ \""^
|
neuper@37906
|
212 |
(string_of_thmI thm')^"\" \""^
|
neuper@37933
|
213 |
(Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
|
neuper@37906
|
214 |
in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
|
neuper@37906
|
215 |
val ruls = (#rules o rep_rls) ruless;
|
neuper@37906
|
216 |
val (ct',asm') = rew_once ruls [] ct Noap ruls;
|
neuper@37926
|
217 |
in if ct = ct' then NONE else SOME (ct',asm') end;
|
neuper@37906
|
218 |
|
neuper@37906
|
219 |
(*
|
neuper@37906
|
220 |
fun reverse_rewrite t1 t2 rls =
|
neuper@37906
|
221 |
*)
|
neuper@37906
|
222 |
fun rewrite_set_' thy rls put_asm ruless ct =
|
neuper@37906
|
223 |
case ruless of
|
neuper@37906
|
224 |
Rrls _ => raise error "rewrite_set_' not for Rrls"
|
neuper@37906
|
225 |
| Rls _ =>
|
neuper@37906
|
226 |
let
|
neuper@37906
|
227 |
datatype switch = Appl | Noap;
|
neuper@37906
|
228 |
fun rew_once ruls asm ct Noap [] = (ct,asm)
|
neuper@37906
|
229 |
| rew_once ruls asm ct Appl [] = rew_once ruls asm ct Noap ruls
|
neuper@37906
|
230 |
| rew_once ruls asm ct apno (rul::thms) =
|
neuper@37906
|
231 |
case rul of
|
neuper@37906
|
232 |
Thm (thmid, thm) =>
|
neuper@37906
|
233 |
(case rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
|
neuper@37906
|
234 |
rls put_asm (thm_of_thm rul) ct of
|
neuper@37926
|
235 |
NONE => rew_once ruls asm ct apno thms
|
neuper@37926
|
236 |
| SOME (ct',asm') =>
|
neuper@37906
|
237 |
rew_once ruls (asm union asm') ct' Appl (rul::thms))
|
neuper@37906
|
238 |
| Calc (cc as (op_,_)) =>
|
neuper@37906
|
239 |
(case get_calculation_ thy cc ct of
|
neuper@37926
|
240 |
NONE => rew_once ruls asm ct apno thms
|
neuper@37926
|
241 |
| SOME (thmid, thm') =>
|
neuper@37906
|
242 |
let
|
neuper@37906
|
243 |
val pairopt =
|
neuper@37906
|
244 |
rewrite_ thy ((snd o #rew_ord o rep_rls) ruless)
|
neuper@37906
|
245 |
rls put_asm thm' ct;
|
neuper@37926
|
246 |
val _ = if pairopt <> NONE then ()
|
neuper@37906
|
247 |
else raise error("rewrite_set_, rewrite_ \""^
|
neuper@37906
|
248 |
(string_of_thmI thm')^"\" \""^
|
neuper@37933
|
249 |
(Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
|
neuper@37906
|
250 |
in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
|
neuper@37906
|
251 |
val ruls = (#rules o rep_rls) ruless;
|
neuper@37906
|
252 |
val (ct',asm') = rew_once ruls [] ct Noap ruls;
|
neuper@37926
|
253 |
in if ct = ct' then NONE else SOME (ct',asm') end;
|
neuper@37906
|
254 |
|
neuper@37906
|
255 |
realpow_two;
|
neuper@37906
|
256 |
real_mult_div_cancel1;
|
neuper@37906
|
257 |
|