neuper@37906
|
1 |
(* isac's rewriter
|
neuper@37906
|
2 |
(c) Walther Neuper 2000
|
neuper@37906
|
3 |
|
neuper@37906
|
4 |
use"Scripts/rewrite.sml";
|
neuper@37906
|
5 |
use"rewrite.sml";
|
neuper@37906
|
6 |
*)
|
neuper@37906
|
7 |
|
neuper@37906
|
8 |
|
neuper@37906
|
9 |
exception NO_REWRITE;
|
neuper@37906
|
10 |
exception STOP_REW_SUB; (*WN050820 quick and dirty*)
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
(*17.6.00: rewrite by going down the term with rew_sub*)
|
neuper@37906
|
13 |
(* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
|
neuper@37906
|
14 |
(thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
|
neuper@37906
|
15 |
*)
|
neuper@37906
|
16 |
fun rewrite__ thy i bdv tless rls put_asm thm ct =
|
neuper@37906
|
17 |
((*writeln ("@@@ r..te__ begin: t = "^(term2str ct));*)
|
neuper@37906
|
18 |
let
|
neuper@37906
|
19 |
val (t',asms,lrd,rew) =
|
neuper@37906
|
20 |
rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
|
neuper@37906
|
21 |
(((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
|
neuper@37906
|
22 |
in if rew then SOME (t', distinct asms)
|
neuper@37906
|
23 |
else NONE end)
|
neuper@37906
|
24 |
(* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct);
|
neuper@37906
|
25 |
val t1 = (#prop o rep_thm) thm;
|
neuper@37906
|
26 |
val t2 = norm t1;
|
neuper@37906
|
27 |
val t3 = inst_bdv bdv t2;
|
neuper@37906
|
28 |
|
neuper@37906
|
29 |
val thm4 = read_instantiate [("bdv","x")] thm;
|
neuper@37906
|
30 |
val t4 = (norm o #prop o rep_thm) thm4;
|
neuper@37906
|
31 |
*)
|
neuper@37906
|
32 |
(* val (thy, i, bdv, tless, rls, put_asm, r, t) =
|
neuper@37906
|
33 |
(thy, i,bdv, tless, rls, put_asm,
|
neuper@37906
|
34 |
(((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
|
neuper@37906
|
35 |
val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
neuper@37906
|
36 |
(thy, 1, [], ord, erls,false, [], r, t);
|
neuper@37906
|
37 |
val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
|
neuper@37906
|
38 |
(thy, i, bdv, tless, rls, put_asm, [],
|
neuper@37906
|
39 |
((inst_bdv bdv) o norm o #prop o rep_thm) thm, ct);
|
neuper@37906
|
40 |
*)
|
neuper@37906
|
41 |
and rew_sub thy i bdv tless rls put_asm lrd r t =
|
neuper@37906
|
42 |
((*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
|
neuper@37906
|
43 |
let (* copy from Pure/thm.ML: fun rewritec *)
|
neuper@37906
|
44 |
(*val (lhs,rhs) = (dest_equals' o strip_trueprop
|
neuper@37906
|
45 |
o Logic.strip_imp_concl) r;
|
neuper@37906
|
46 |
val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t);
|
neuper@37906
|
47 |
val r' = ren_inst (insts, r, lhs, t);
|
neuper@37906
|
48 |
val p' = map strip_trueprop (Logic.strip_imp_prems r');
|
neuper@37906
|
49 |
val t' = (snd o dest_equals' o strip_trueprop
|
neuper@37906
|
50 |
o Logic.strip_imp_concl) r';*)
|
neuper@37906
|
51 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
52 |
o Logic.strip_imp_concl) r;
|
neuper@37906
|
53 |
val r' = Envir.subst_term (Pattern.match thy (lhs, t)
|
neuper@37906
|
54 |
(Vartab.empty, Vartab.empty)) r;
|
neuper@37906
|
55 |
val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
|
neuper@37906
|
56 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
|
neuper@37906
|
57 |
o Logic.strip_imp_concl) r';
|
neuper@37906
|
58 |
(*val _= writeln("@@@ rew_sub match: t'= "^(term2str t'));*)
|
neuper@37906
|
59 |
val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
|
neuper@37906
|
60 |
then writeln((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
|
neuper@37906
|
61 |
val (t'',p'') = (*conditional rewriting*)
|
neuper@37906
|
62 |
let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
|
neuper@37906
|
63 |
in if nofalse
|
neuper@37906
|
64 |
then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
|
neuper@37906
|
65 |
then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
|
neuper@37906
|
66 |
" stored: "^(terms2str simpl_p'))
|
neuper@37906
|
67 |
else(); (t',simpl_p')) (* + uncond.rew. *)
|
neuper@37906
|
68 |
else
|
neuper@37906
|
69 |
(if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
70 |
then writeln((idt"#"(i+1))^" asms false: "^(terms2str p'))
|
neuper@37906
|
71 |
else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
|
neuper@37906
|
72 |
end
|
neuper@37906
|
73 |
in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
|
neuper@37906
|
74 |
then (if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
75 |
then writeln((idt"#"i)^" not: \""^
|
neuper@37906
|
76 |
(term2str t)^"\" > \""^
|
neuper@37906
|
77 |
(term2str t')^"\"") else ();
|
neuper@37906
|
78 |
raise NO_REWRITE )
|
neuper@37906
|
79 |
else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
|
neuper@37906
|
80 |
", p'' ="^(terms2str p'')^", true)");*)
|
neuper@37906
|
81 |
(t'',p'',[],true))
|
neuper@37906
|
82 |
end
|
neuper@37906
|
83 |
) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
|
neuper@37906
|
84 |
((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*)
|
neuper@37906
|
85 |
case t of
|
neuper@37906
|
86 |
Const(s,T) => (Const(s,T),[],lrd,false)
|
neuper@37906
|
87 |
| Free(s,T) => (Free(s,T),[],lrd,false)
|
neuper@37906
|
88 |
| Var(n,T) => (Var(n,T),[],lrd,false)
|
neuper@37906
|
89 |
| Bound i => (Bound i,[],lrd,false)
|
neuper@37906
|
90 |
| Abs(s,T,body) =>
|
neuper@37906
|
91 |
let val (t', asms, lrd, rew) =
|
neuper@37906
|
92 |
rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
|
neuper@37906
|
93 |
in (Abs(s,T,t'), asms, [], rew) end
|
neuper@37906
|
94 |
| t1 $ t2 =>
|
neuper@37906
|
95 |
let val (t2', asm2, lrd, rew2) =
|
neuper@37906
|
96 |
rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
|
neuper@37906
|
97 |
in if rew2 then (t1 $ t2', asm2, lrd, true)
|
neuper@37906
|
98 |
else let val (t1', asm1, lrd, rew1) =
|
neuper@37906
|
99 |
rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
|
neuper@37906
|
100 |
in if rew1 then (t1' $ t2, asm1, lrd, true)
|
neuper@37906
|
101 |
else (t1 $ t2,[], lrd, false) end
|
neuper@37906
|
102 |
end)
|
neuper@37906
|
103 |
(* val (cprems',rls)=([pre],prls);
|
neuper@37906
|
104 |
rewrite__set_ thy i false rls pre;
|
neuper@37906
|
105 |
*)
|
neuper@37906
|
106 |
and eval__true thy i asms bdv rls =
|
neuper@37906
|
107 |
(* val (thy, i, asms, bdv, rls) = (thy, (i+1), p', bdv, rls);
|
neuper@37906
|
108 |
*)
|
neuper@37906
|
109 |
if asms = [HOLogic.true_const] orelse asms = []
|
neuper@37906
|
110 |
then ([], true) else if asms = [HOLogic.false_const] then ([], false)
|
neuper@37906
|
111 |
else let
|
neuper@37906
|
112 |
fun chk indets [] = (indets, true)(*return asms<>True until false*)
|
neuper@37906
|
113 |
| chk indets (a::asms) =
|
neuper@37906
|
114 |
(* val (indets, (a::asms)) = ([], asms);
|
neuper@37906
|
115 |
*)
|
neuper@37906
|
116 |
(case rewrite__set_ thy (i+1) false bdv rls a of
|
neuper@37906
|
117 |
NONE => (chk (indets @ [a]) asms)
|
neuper@37906
|
118 |
| SOME (t, a') =>
|
neuper@37906
|
119 |
if t = HOLogic.true_const
|
neuper@37906
|
120 |
then (chk (indets @ a') asms)
|
neuper@37906
|
121 |
else if t = HOLogic.false_const then ([], false)
|
neuper@37906
|
122 |
(*asm false .. thm not applied ^^^; continue until False vvv*)
|
neuper@37906
|
123 |
else (chk (indets @ [t] @ a') asms));
|
neuper@37906
|
124 |
in chk [] asms end
|
neuper@37906
|
125 |
|
neuper@37906
|
126 |
and rewrite__set_ _ _ __ Erls t =
|
neuper@37906
|
127 |
raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
|
neuper@37906
|
128 |
| rewrite__set_ thy i _ _ (rrls as Rrls _) t =
|
neuper@37906
|
129 |
let val _= if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
130 |
then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
|
neuper@37906
|
131 |
(term2str t)) else ()
|
neuper@37906
|
132 |
val (t', asm, rew) = app_rev thy (i+1) rrls t
|
neuper@37906
|
133 |
in if rew then SOME (t', distinct asm)
|
neuper@37906
|
134 |
else NONE end
|
neuper@37906
|
135 |
| rewrite__set_ thy i put_asm bdv rls ct =
|
neuper@37906
|
136 |
(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
|
neuper@37906
|
137 |
*)
|
neuper@37906
|
138 |
let
|
neuper@37906
|
139 |
datatype switch = Appl | Noap;
|
neuper@37906
|
140 |
fun rew_once ruls asm ct Noap [] = (ct,asm)
|
neuper@37906
|
141 |
| rew_once ruls asm ct Appl [] =
|
neuper@37906
|
142 |
(case rls of Rls _ => rew_once ruls asm ct Noap ruls
|
neuper@37906
|
143 |
| Seq _ => (ct,asm))
|
neuper@37906
|
144 |
| rew_once ruls asm ct apno (rul::thms) =
|
neuper@37906
|
145 |
(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
|
neuper@37906
|
146 |
val Thm (thmid, thm) = rul;
|
neuper@37906
|
147 |
*)
|
neuper@37906
|
148 |
case rul of
|
neuper@37906
|
149 |
Thm (thmid, thm) =>
|
neuper@37906
|
150 |
(if !trace_rewrite andalso i < ! depth
|
neuper@37906
|
151 |
then writeln((idt"#"(i+1))^" try thm: "^thmid) else ();
|
neuper@37906
|
152 |
case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
|
neuper@37906
|
153 |
((#erls o rep_rls) rls) put_asm thm ct of
|
neuper@37906
|
154 |
NONE => rew_once ruls asm ct apno thms
|
neuper@37906
|
155 |
| SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
156 |
then writeln((idt"="(i+1))^" rewrites to: "^
|
neuper@37906
|
157 |
(term2str ct')) else ();
|
neuper@37906
|
158 |
rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
|
neuper@37906
|
159 |
| Calc (cc as (op_,_)) =>
|
neuper@37906
|
160 |
(let val _= if !trace_rewrite andalso i < ! depth then
|
neuper@37906
|
161 |
writeln((idt"#"(i+1))^" try calc: "^op_^"'") else ();
|
neuper@37906
|
162 |
val ct = uminus_to_string ct
|
neuper@37906
|
163 |
in case get_calculation_ thy cc ct of
|
neuper@37906
|
164 |
NONE => ((*writeln "@@@ rewrite__set_: get_calculation_-> NONE";*)
|
neuper@37906
|
165 |
rew_once ruls asm ct apno thms)
|
neuper@37906
|
166 |
| SOME (thmid, thm') =>
|
neuper@37906
|
167 |
let
|
neuper@37906
|
168 |
val pairopt =
|
neuper@37906
|
169 |
rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
|
neuper@37906
|
170 |
((#erls o rep_rls) rls) put_asm thm' ct;
|
neuper@37906
|
171 |
val _ = if pairopt <> NONE then ()
|
neuper@37906
|
172 |
else raise error("rewrite_set_, rewrite_ \""^
|
neuper@37906
|
173 |
(string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
|
neuper@37906
|
174 |
val _ = if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
175 |
then writeln((idt"="(i+1))^" calc. to: "^
|
neuper@37906
|
176 |
(term2str ((fst o the) pairopt)))
|
neuper@37906
|
177 |
else()
|
neuper@37906
|
178 |
in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
|
neuper@37906
|
179 |
end)
|
neuper@37906
|
180 |
(* use"Scripts/rewrite.sml";
|
neuper@37906
|
181 |
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
|
neuper@37906
|
182 |
| Cal1 (cc as (op_,_)) =>
|
neuper@37906
|
183 |
(let val _= if !trace_rewrite andalso i < ! depth then
|
neuper@37906
|
184 |
writeln((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
|
neuper@37906
|
185 |
val ct = uminus_to_string ct
|
neuper@37906
|
186 |
in case get_calculation1_ thy cc ct of
|
neuper@37906
|
187 |
NONE => (ct, asm)
|
neuper@37906
|
188 |
| SOME (thmid, thm') =>
|
neuper@37906
|
189 |
let
|
neuper@37906
|
190 |
val pairopt =
|
neuper@37906
|
191 |
rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
|
neuper@37906
|
192 |
((#erls o rep_rls) rls) put_asm thm' ct;
|
neuper@37906
|
193 |
val _ = if pairopt <> NONE then ()
|
neuper@37906
|
194 |
else raise error("rewrite_set_, rewrite_ \""^
|
neuper@37906
|
195 |
(string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
|
neuper@37906
|
196 |
val _ = if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
197 |
then writeln((idt"="(i+1))^" cal1. to: "^
|
neuper@37906
|
198 |
(term2str ((fst o the) pairopt)))
|
neuper@37906
|
199 |
else()
|
neuper@37906
|
200 |
in the pairopt end
|
neuper@37906
|
201 |
end)
|
neuper@37906
|
202 |
(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
|
neuper@37906
|
203 |
| Rls_ rls' =>
|
neuper@37906
|
204 |
(case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
|
neuper@37906
|
205 |
SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
|
neuper@37906
|
206 |
| NONE => rew_once ruls asm ct apno thms);
|
neuper@37906
|
207 |
|
neuper@37906
|
208 |
val ruls = (#rules o rep_rls) rls;
|
neuper@37906
|
209 |
val _= if ! trace_rewrite andalso i < ! depth
|
neuper@37906
|
210 |
then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
|
neuper@37906
|
211 |
(term2str ct)) else ()
|
neuper@37906
|
212 |
val (ct',asm') = rew_once ruls [] ct Noap ruls;
|
neuper@37906
|
213 |
in if ct = ct' then NONE else SOME (ct', distinct asm') end
|
neuper@37906
|
214 |
|
neuper@37906
|
215 |
and app_rev thy i rrls t =
|
neuper@37906
|
216 |
let (*.check a (precond, pattern) of a rev-set; stops with 1st true.*)
|
neuper@37906
|
217 |
fun chk_prepat thy erls [] t = true
|
neuper@37906
|
218 |
| chk_prepat thy erls prepat t =
|
neuper@37906
|
219 |
let fun chk (pres, pat) =
|
neuper@37906
|
220 |
(let val subst: Type.tyenv * Envir.tenv =
|
neuper@37906
|
221 |
Pattern.match thy (pat, t)
|
neuper@37906
|
222 |
(Vartab.empty, Vartab.empty)
|
neuper@37906
|
223 |
in snd (eval__true thy (i+1)
|
neuper@37906
|
224 |
(map (Envir.subst_term subst) pres)
|
neuper@37906
|
225 |
[] erls)
|
neuper@37906
|
226 |
end)
|
neuper@37906
|
227 |
handle _ => false
|
neuper@37906
|
228 |
fun scan_ f [] = false (*scan_ NEVER called by []*)
|
neuper@37906
|
229 |
| scan_ f (pp::pps) = if f pp then true
|
neuper@37906
|
230 |
else scan_ f pps;
|
neuper@37906
|
231 |
in scan_ chk prepat end;
|
neuper@37906
|
232 |
|
neuper@37906
|
233 |
(*.apply the normal_form of a rev-set.*)
|
neuper@37906
|
234 |
fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
|
neuper@37906
|
235 |
if chk_prepat thy erls prepat t
|
neuper@37906
|
236 |
then ((*writeln("### app_rev': t = "^(term2str t));*)
|
neuper@37906
|
237 |
normal_form t)
|
neuper@37906
|
238 |
else NONE;
|
neuper@37906
|
239 |
|
neuper@37906
|
240 |
val opt = app_rev' thy rrls t
|
neuper@37906
|
241 |
in case opt of
|
neuper@37906
|
242 |
SOME (t', asm) => (t', asm, true)
|
neuper@37906
|
243 |
| NONE => app_sub thy i rrls t
|
neuper@37906
|
244 |
end
|
neuper@37906
|
245 |
and app_sub thy i rrls t =
|
neuper@37906
|
246 |
((*writeln("### app_sub: subterm = "^(term2str t));*)
|
neuper@37906
|
247 |
case t of
|
neuper@37906
|
248 |
Const (s, T) => (Const(s, T), [], false)
|
neuper@37906
|
249 |
| Free (s, T) => (Free(s, T), [], false)
|
neuper@37906
|
250 |
| Var (n, T) => (Var(n, T), [], false)
|
neuper@37906
|
251 |
| Bound i => (Bound i, [], false)
|
neuper@37906
|
252 |
| Abs (s, T, body) =>
|
neuper@37906
|
253 |
let val (t', asm, rew) = app_rev thy i rrls body
|
neuper@37906
|
254 |
in (Abs(s, T, t'), asm, rew) end
|
neuper@37906
|
255 |
| t1 $ t2 =>
|
neuper@37906
|
256 |
let val (t2', asm2, rew2) = app_rev thy i rrls t2
|
neuper@37906
|
257 |
in if rew2 then (t1 $ t2', asm2, true)
|
neuper@37906
|
258 |
else let val (t1', asm1, rew1) = app_rev thy i rrls t1
|
neuper@37906
|
259 |
in if rew1 then (t1' $ t2, asm1, true)
|
neuper@37906
|
260 |
else (t1 $ t2, [], false) end
|
neuper@37906
|
261 |
end);
|
neuper@37906
|
262 |
|
neuper@37906
|
263 |
|
neuper@37906
|
264 |
|
neuper@37906
|
265 |
(*.rewriting without argument [] for rew_ord.*)
|
neuper@37906
|
266 |
(*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
|
neuper@37906
|
267 |
fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
|
neuper@37906
|
268 |
|
neuper@37906
|
269 |
|
neuper@37906
|
270 |
(*.rewriting without internal argument [] for rew_ord.*)
|
neuper@37906
|
271 |
(* val (thy, rew_ord, erls, bool, thm, term) =
|
neuper@37906
|
272 |
(thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
|
neuper@37906
|
273 |
val (thy, rew_ord, erls, bool, thm, term) =
|
neuper@37906
|
274 |
(thy, rew_ord, erls, false, thm, t'');
|
neuper@37906
|
275 |
*)
|
neuper@37906
|
276 |
fun rewrite_ thy rew_ord erls bool thm term =
|
neuper@37906
|
277 |
rewrite__ thy 1 [] rew_ord erls bool thm term;
|
neuper@37906
|
278 |
fun rewrite_set_ thy bool rls term =
|
neuper@37906
|
279 |
(* val (thy, bool, rls, term) = (thy, false, srls, t);
|
neuper@37906
|
280 |
*)
|
neuper@37906
|
281 |
rewrite__set_ thy 1 bool [] rls term;
|
neuper@37906
|
282 |
|
neuper@37906
|
283 |
|
neuper@37906
|
284 |
fun subs'2subst thy (s:subs') =
|
neuper@37906
|
285 |
(((map (apfst (term_of o the o (parse thy))))
|
neuper@37906
|
286 |
o (map (apsnd (term_of o the o (parse thy))))) s):subst;
|
neuper@37906
|
287 |
|
neuper@37906
|
288 |
(*.variants of rewrite.*)
|
neuper@37906
|
289 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
|
neuper@37906
|
290 |
thus the argument put_asm IS NOT NECESSARY -- FIXME*)
|
neuper@37906
|
291 |
(* val (rew_ord,rls,put_asm,thm,ct)=
|
neuper@37906
|
292 |
(e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
|
neuper@37906
|
293 |
*)
|
neuper@37906
|
294 |
fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
|
neuper@37906
|
295 |
(subst:(term * term) list) (thm:thm) (ct:term) =
|
neuper@37906
|
296 |
rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
|
neuper@37906
|
297 |
|
neuper@37906
|
298 |
fun rewrite_set_inst_ (thy:theory)
|
neuper@37906
|
299 |
(put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
|
neuper@37906
|
300 |
(*let
|
neuper@37906
|
301 |
val subst = subs'2subst thy subs';
|
neuper@37906
|
302 |
val subrls = instantiate_rls subs' rls
|
neuper@37906
|
303 |
in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
|
neuper@37906
|
304 |
(*end*);
|
neuper@37906
|
305 |
|
neuper@37906
|
306 |
(* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t);
|
neuper@37906
|
307 |
*)
|
neuper@37906
|
308 |
(*.rewrite using a list of terms.*)
|
neuper@37906
|
309 |
fun rewrite_terms_ thy ord erls subte t =
|
neuper@37906
|
310 |
let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
|
neuper@37906
|
311 |
term_detail2str (hd subte)^
|
neuper@37906
|
312 |
"### rewrite_terms_ t= '"^term2str t^"' ..."^
|
neuper@37906
|
313 |
term_detail2str t);*)
|
neuper@37906
|
314 |
fun rew_ (t', asm') [] _ = (t', asm')
|
neuper@37906
|
315 |
(* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t);
|
neuper@37906
|
316 |
2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
|
neuper@37906
|
317 |
rew_ (t', asm') (r::rs) t;
|
neuper@37906
|
318 |
*)
|
neuper@37906
|
319 |
| rew_ (t', asm') (rules as r::rs) t =
|
neuper@37906
|
320 |
let val _ = writeln("rew_ "^term2str t);
|
neuper@37906
|
321 |
val (t'', asm'', lrd, rew) =
|
neuper@37906
|
322 |
rew_sub thy 1 [] ord erls false [] r t
|
neuper@37906
|
323 |
in if rew
|
neuper@37906
|
324 |
then (writeln("true rew_ "^term2str t'');
|
neuper@37906
|
325 |
rew_ (t'', asm' @ asm'') rules t'')
|
neuper@37906
|
326 |
else (writeln("false rew_ "^term2str t'');
|
neuper@37906
|
327 |
rew_ (t', asm') rs t')
|
neuper@37906
|
328 |
end
|
neuper@37906
|
329 |
val (t'', asm'') = rew_ (e_term, []) subte t
|
neuper@37906
|
330 |
in if t'' = e_term
|
neuper@37906
|
331 |
then NONE else SOME (t'', asm'')
|
neuper@37906
|
332 |
end;
|
neuper@37906
|
333 |
|
neuper@37906
|
334 |
|
neuper@37906
|
335 |
(*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
|
neuper@37906
|
336 |
fun calculate_ thy isa_fn ct =
|
neuper@37906
|
337 |
let val ct = uminus_to_string ct
|
neuper@37906
|
338 |
in case get_calculation_ thy isa_fn ct of
|
neuper@37906
|
339 |
NONE => NONE
|
neuper@37906
|
340 |
| SOME (thmID, thm) =>
|
neuper@37906
|
341 |
(let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
|
neuper@37906
|
342 |
in SOME (rew,(thmID, thm)) end)
|
neuper@37906
|
343 |
handle _ => error ("calculate_: "^thmID^" does not rewrite")
|
neuper@37906
|
344 |
end;
|
neuper@37906
|
345 |
(*
|
neuper@37906
|
346 |
> val thy = InsSort.thy;
|
neuper@37906
|
347 |
> val op_ = "le"; (* < *)
|
neuper@37906
|
348 |
> val ct = (the o (parse thy))
|
neuper@37906
|
349 |
"foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
|
neuper@37906
|
350 |
> calculate_ thy op_ ct;
|
neuper@37906
|
351 |
SOME
|
neuper@37906
|
352 |
("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
|
neuper@37906
|
353 |
"(#1 < #3) = True") : (cterm * thm) option *)
|
neuper@37906
|
354 |
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
(* for test-printouts:
|
neuper@37906
|
357 |
val _ = writeln("in rew_sub : "^( Sign.string_of_term (sign_of thy) t))
|
neuper@37906
|
358 |
val _ = writeln("in eval_true: prems= "^(commas (map (Sign.string_of_term (sign_of thy)) prems')))
|
neuper@37906
|
359 |
*)
|
neuper@37906
|
360 |
|
neuper@37906
|
361 |
|
neuper@37906
|
362 |
|
neuper@37906
|
363 |
|
neuper@37906
|
364 |
|
neuper@37906
|
365 |
|
neuper@37906
|
366 |
fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
|
neuper@37906
|
367 |
handle _ => raise error ("get_rls_scr: no script for "^rs');
|
neuper@37906
|
368 |
|
neuper@37906
|
369 |
|
neuper@37906
|
370 |
(*make_thm added to Pure/thm.ML*)
|
neuper@37906
|
371 |
fun mk_thm thy str =
|
neuper@37906
|
372 |
let val t = (term_of o the o (parse thy)) str
|
neuper@37906
|
373 |
val t' = case t of
|
neuper@37906
|
374 |
Const ("==>",_) $ _ $ _ => t
|
neuper@37906
|
375 |
| _ => Trueprop $ t
|
neuper@37906
|
376 |
in make_thm (Thm.cterm_of thy t') end;
|
neuper@37906
|
377 |
(*
|
neuper@37906
|
378 |
val str = "?r ^^^ 2 = ?r * ?r";
|
neuper@37906
|
379 |
val thm = realpow_twoI;
|
neuper@37906
|
380 |
|
neuper@37906
|
381 |
val t1 = (#prop o rep_thm) (num_str thm);
|
neuper@37906
|
382 |
val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
|
neuper@37906
|
383 |
t1 = t2;
|
neuper@37906
|
384 |
val it = true : bool ... !!!
|
neuper@37906
|
385 |
val th1 = (num_str thm);
|
neuper@37906
|
386 |
val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
|
neuper@37906
|
387 |
th1 = th2;
|
neuper@37906
|
388 |
ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
|
neuper@37906
|
389 |
|
neuper@37906
|
390 |
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
neuper@37906
|
391 |
val str = "k ~= 0 ==> m * k / (n * k) = m / n";
|
neuper@37906
|
392 |
val thm = real_mult_div_cancel2;
|
neuper@37906
|
393 |
|
neuper@37906
|
394 |
val t1 = (#prop o rep_thm) (num_str thm);
|
neuper@37906
|
395 |
val t2 = ((term_of o the o (parse thy)) str);
|
neuper@37906
|
396 |
t1 = t2;
|
neuper@37906
|
397 |
val it = false : bool ... Var .. Free
|
neuper@37906
|
398 |
val th1 = (num_str thm);
|
neuper@37906
|
399 |
val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
|
neuper@37906
|
400 |
th1 = th2;
|
neuper@37906
|
401 |
ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
|
neuper@37906
|
402 |
*)
|
neuper@37906
|
403 |
|
neuper@37906
|
404 |
|
neuper@37906
|
405 |
(*prints subgoal etc.
|
neuper@37906
|
406 |
((goal thy);(topthm()) o ) str; *)
|
neuper@37906
|
407 |
(*assume rejects scheme variables
|
neuper@37906
|
408 |
assume (cterm_of (sign_of thy) (Trueprop $
|
neuper@37906
|
409 |
(term_of o the o (parse thy)) str)); *)
|
neuper@37906
|
410 |
|
neuper@37906
|
411 |
|
neuper@37906
|
412 |
(* outcommented 18.11.xx, xx < 02 -------
|
neuper@37906
|
413 |
fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
|
neuper@37906
|
414 |
| rul2rul' (Calc op_) = Calc' op_;
|
neuper@37906
|
415 |
fun rul'2rul thy (Thm'(thmid, ct')) =
|
neuper@37906
|
416 |
Thm (thmid, mk_thm thy ct')
|
neuper@37906
|
417 |
| rul'2rul thy' (Calc' op_) = Calc op_;
|
neuper@37906
|
418 |
|
neuper@37906
|
419 |
|
neuper@37906
|
420 |
fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
|
neuper@37906
|
421 |
Rls'{preconds'= map string_of_cterm preconds,
|
neuper@37906
|
422 |
rew_ord' = fst rew_ord,
|
neuper@37906
|
423 |
rules' = map rul2rul' rules}:rlsdat';
|
neuper@37906
|
424 |
|
neuper@37906
|
425 |
fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
|
neuper@37906
|
426 |
rules'=rules}:rlsdat') =
|
neuper@37906
|
427 |
let val thy = the (assoc' (theory',thy'))
|
neuper@37906
|
428 |
in Rls{preconds = map (the o (parse thy)) preconds,
|
neuper@37906
|
429 |
rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
|
neuper@37906
|
430 |
rules = map (rul'2rul thy) rules}:rls end;
|
neuper@37906
|
431 |
------- *)
|
neuper@37906
|
432 |
|
neuper@37906
|
433 |
(*.get the theorem associated with the xstring-identifier;
|
neuper@37906
|
434 |
if the identifier starts with "sym_" then swap lhs = rhs around =
|
neuper@37906
|
435 |
(ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
|
neuper@37906
|
436 |
identifiers starting with "#" come from Calc and
|
neuper@37906
|
437 |
get a hand-made theorem (containing numerals only).*)
|
neuper@37906
|
438 |
fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
|
neuper@37906
|
439 |
(case explode thmid of
|
neuper@37906
|
440 |
"s"::"y"::"m"::"_"::id =>
|
neuper@37906
|
441 |
if hd id = "#"
|
neuper@37906
|
442 |
then mk_thm thy ct'
|
neuper@37906
|
443 |
else ((num_str o (PureThy.get_thm thy)) (implode id)) RS sym
|
neuper@37906
|
444 |
| id =>
|
neuper@37906
|
445 |
if hd id = "#"
|
neuper@37906
|
446 |
then mk_thm thy ct'
|
neuper@37906
|
447 |
else (num_str o (PureThy.get_thm thy)) thmid
|
neuper@37906
|
448 |
) handle _ =>
|
neuper@37906
|
449 |
raise error ("assoc_thm': '"^thmid^"' not in '"^
|
neuper@37906
|
450 |
(theory2domID thy)^"' (and parents)");
|
neuper@37906
|
451 |
(*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
|
neuper@37906
|
452 |
val it = "6 = 2 * 3" : thm
|
neuper@37906
|
453 |
|
neuper@37906
|
454 |
> assoc_thm' Isac.thy ("real_add_zero_left","");
|
neuper@37906
|
455 |
val it = "0 + ?z = ?z" : thm
|
neuper@37906
|
456 |
|
neuper@37906
|
457 |
> assoc_thm' Isac.thy ("sym_real_add_zero_left","");
|
neuper@37906
|
458 |
val it = "?t = 0 + ?t" [.] : thm
|
neuper@37906
|
459 |
|
neuper@37906
|
460 |
> assoc_thm' HOL.thy ("sym_real_add_zero_left","");
|
neuper@37906
|
461 |
*** Unknown theorem(s) "real_add_zero_left"
|
neuper@37906
|
462 |
*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
|
neuper@37906
|
463 |
uncaught exception ERROR*)
|
neuper@37906
|
464 |
|
neuper@37906
|
465 |
|
neuper@37906
|
466 |
fun parse' (thy:theory') (ct:cterm') =
|
neuper@37906
|
467 |
case parse ((the o assoc')(!theory',thy)) ct of
|
neuper@37906
|
468 |
NONE => NONE
|
neuper@37906
|
469 |
| SOME ct => SOME ((term2str (term_of ct)):cterm');
|
neuper@37906
|
470 |
|
neuper@37906
|
471 |
|
neuper@37906
|
472 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
473 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
474 |
fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
|
neuper@37906
|
475 |
(put_asm:bool) (thm:thm') (ct:cterm') =
|
neuper@37906
|
476 |
(* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);
|
neuper@37906
|
477 |
*)
|
neuper@37906
|
478 |
let val thy = (the o assoc')(!theory',thy');
|
neuper@37906
|
479 |
in
|
neuper@37906
|
480 |
case rewrite_ thy
|
neuper@37906
|
481 |
((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))
|
neuper@37906
|
482 |
put_asm ((assoc_thm' thy) thm)
|
neuper@37906
|
483 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
484 |
NONE => NONE
|
neuper@37906
|
485 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
486 |
end;
|
neuper@37906
|
487 |
|
neuper@37906
|
488 |
(*
|
neuper@37906
|
489 |
val thy = "RatArith.thy";
|
neuper@37906
|
490 |
val rew_ord = "dummy_ord";
|
neuper@37906
|
491 |
> val rls = "eval_rls";
|
neuper@37906
|
492 |
val put_asm = true;
|
neuper@37906
|
493 |
val thm = ("square_equation_left","");
|
neuper@37906
|
494 |
val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
|
neuper@37906
|
495 |
|
neuper@37906
|
496 |
val Zthy = ((the o assoc')(!theory',thy));
|
neuper@37906
|
497 |
val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
|
neuper@37906
|
498 |
val Zrls = ((the o assoc')(!ruleset',rls));
|
neuper@37906
|
499 |
val Zput_asm = put_asm;
|
neuper@37906
|
500 |
val Zthm = ((the o (assoc'_thm' thy)) thm);
|
neuper@37906
|
501 |
val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct);
|
neuper@37906
|
502 |
|
neuper@37906
|
503 |
rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
|
neuper@37906
|
504 |
|
neuper@37906
|
505 |
use"Isa99/interface_ME_ISA.sml";
|
neuper@37906
|
506 |
*)
|
neuper@37906
|
507 |
|
neuper@37906
|
508 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
509 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
510 |
fun rewrite_set (thy':theory') (put_asm:bool)
|
neuper@37906
|
511 |
(rls:rls') (ct:cterm') =
|
neuper@37906
|
512 |
let val thy = (the o assoc')(!theory',thy');
|
neuper@37906
|
513 |
in
|
neuper@37906
|
514 |
case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))
|
neuper@37906
|
515 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
516 |
NONE => NONE
|
neuper@37906
|
517 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
518 |
end;
|
neuper@37906
|
519 |
|
neuper@37906
|
520 |
(*evaluate list-expressions
|
neuper@37906
|
521 |
should work on term, and stand in Isa99/rewrite-parse.sml,
|
neuper@37906
|
522 |
but there list_rls <- eval_binop is not yet defined*)
|
neuper@37906
|
523 |
(*fun eval_listexpr' ct =
|
neuper@37906
|
524 |
let val rew = rewrite_set "ListG.thy" false "list_rls" ct;
|
neuper@37906
|
525 |
in case rew of
|
neuper@37906
|
526 |
SOME (res,_) => res
|
neuper@37906
|
527 |
| NONE => ct end;-----------------30.9.02---*)
|
neuper@37906
|
528 |
fun eval_listexpr_ thy srls t =
|
neuper@37906
|
529 |
(* val (thy, srls, t) =
|
neuper@37906
|
530 |
((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
|
neuper@37906
|
531 |
*)
|
neuper@37906
|
532 |
let val rew = rewrite_set_ thy false srls t;
|
neuper@37906
|
533 |
in case rew of
|
neuper@37906
|
534 |
SOME (res,_) => res
|
neuper@37906
|
535 |
| NONE => t end;
|
neuper@37906
|
536 |
|
neuper@37906
|
537 |
|
neuper@37906
|
538 |
fun get_calculation' (thy:theory') op_ (ct:cterm') =
|
neuper@37906
|
539 |
case get_calculation_ ((the o assoc')(!theory',thy)) op_
|
neuper@37906
|
540 |
((uminus_to_string o term_of o the o
|
neuper@37906
|
541 |
(parse ((the o assoc')(!theory',thy)))) ct) of
|
neuper@37906
|
542 |
NONE => NONE
|
neuper@37906
|
543 |
| SOME (thmid, thm) =>
|
neuper@37906
|
544 |
SOME ((thmid, string_of_thmI thm):thm');
|
neuper@37906
|
545 |
|
neuper@37906
|
546 |
fun calculate (thy':theory') op_ (ct:cterm') =
|
neuper@37906
|
547 |
let val thy = (the o assoc')(!theory',thy');
|
neuper@37906
|
548 |
in
|
neuper@37906
|
549 |
case calculate_ thy op_
|
neuper@37906
|
550 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
551 |
NONE => NONE
|
neuper@37906
|
552 |
| SOME (ct,(thmID,thm)) =>
|
neuper@37906
|
553 |
SOME (term2str ct,
|
neuper@37906
|
554 |
(thmID, string_of_thmI thm):thm')
|
neuper@37906
|
555 |
end;
|
neuper@37906
|
556 |
(*
|
neuper@37906
|
557 |
fun instantiate'' thy' subs ((thmid,ct'):thm') =
|
neuper@37906
|
558 |
let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
|
neuper@37906
|
559 |
in (thmid_, (string_of_thmI o (read_instantiate subs))
|
neuper@37906
|
560 |
((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
|
neuper@37906
|
561 |
|
neuper@37906
|
562 |
fun instantiate_rls' thy' subs (rls:rls') =
|
neuper@37906
|
563 |
rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
|
neuper@37906
|
564 |
|
neuper@37906
|
565 |
... problem with these functions:
|
neuper@37906
|
566 |
> val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
|
neuper@37906
|
567 |
val thm = "(bdv + a = b) = (bdv = b - a)" : thm
|
neuper@37906
|
568 |
> show_types:=true; thm;
|
neuper@37906
|
569 |
val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
|
neuper@37906
|
570 |
... and this doesn't match because of too general typing (?!)
|
neuper@37906
|
571 |
and read_insitantiate doesn't instantiate the types (?!)
|
neuper@37906
|
572 |
=== solutions:
|
neuper@37906
|
573 |
(1) hard-coded type-instantiation ("'a", "RatArith.rat")
|
neuper@37906
|
574 |
(2) instantiate', instantiate ... no help by isabelle-users@ !!!
|
neuper@37906
|
575 |
=== conclusion:
|
neuper@37906
|
576 |
rewrite_inst, rewrite_set_inst circumvent the problem,
|
neuper@37906
|
577 |
according functions out-commented with 'instantiate''
|
neuper@37906
|
578 |
*)
|
neuper@37906
|
579 |
|
neuper@37906
|
580 |
(* instantiate''
|
neuper@37906
|
581 |
fun instantiate'' thy' subs ((thmid,ct'):thm') =
|
neuper@37906
|
582 |
let
|
neuper@37906
|
583 |
val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*)
|
neuper@37906
|
584 |
val thy = (the o assoc')(!theory',thy');
|
neuper@37906
|
585 |
val typs = map (#T o rep_cterm o the o (parse thy))
|
neuper@37906
|
586 |
((snd o split_list) subs);
|
neuper@37906
|
587 |
val ctyps = map
|
neuper@37906
|
588 |
((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
|
neuper@37906
|
589 |
((snd o split_list) subs);
|
neuper@37906
|
590 |
|
neuper@37906
|
591 |
> val thy' = "RatArith.thy";
|
neuper@37906
|
592 |
> val subs = [("bdv","x::rat"),("zzz","z::nat")];
|
neuper@37906
|
593 |
> (the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
|
neuper@37906
|
594 |
> (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy'))));
|
neuper@37906
|
595 |
|
neuper@37906
|
596 |
> val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
|
neuper@37906
|
597 |
(parse ((the o assoc')(!theory',thy')))) "x::rat";
|
neuper@37906
|
598 |
> val bdv = (the o (parse thy)) "bdv";
|
neuper@37906
|
599 |
> val x = (the o (parse thy)) "x";
|
neuper@37906
|
600 |
> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
|
neuper@37906
|
601 |
handle e => print_exn e;
|
neuper@37906
|
602 |
uncaught exception THM
|
neuper@37906
|
603 |
raised at: thm.ML:1085.18-1085.69
|
neuper@37906
|
604 |
thm.ML:1092.34
|
neuper@37906
|
605 |
goals.ML:536.61
|
neuper@37906
|
606 |
|
neuper@37906
|
607 |
> val bdv = (the o (parse thy)) "bdv::nat";
|
neuper@37906
|
608 |
> val x = (the o (parse thy)) "x::nat";
|
neuper@37906
|
609 |
> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
|
neuper@37906
|
610 |
handle e => print_exn e;
|
neuper@37906
|
611 |
uncaught exception THM
|
neuper@37906
|
612 |
raised at: thm.ML:1085.18-1085.69
|
neuper@37906
|
613 |
thm.ML:1092.34
|
neuper@37906
|
614 |
goals.ML:536.61
|
neuper@37906
|
615 |
|
neuper@37906
|
616 |
> (instantiate' [SOME ctyp] [] isolate_bdv_add)
|
neuper@37906
|
617 |
handle e => print_exn e;
|
neuper@37906
|
618 |
uncaught exception TYPE
|
neuper@37906
|
619 |
raised at: drule.ML:613.13-615.44
|
neuper@37906
|
620 |
goals.ML:536.61
|
neuper@37906
|
621 |
|
neuper@37906
|
622 |
> val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
|
neuper@37906
|
623 |
*)
|
neuper@37906
|
624 |
|
neuper@37906
|
625 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
626 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
627 |
fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
|
neuper@37906
|
628 |
(put_asm:bool) subs (thm:thm') (ct:cterm') =
|
neuper@37906
|
629 |
let
|
neuper@37906
|
630 |
val thy = (the o assoc')(!theory',thy');
|
neuper@37906
|
631 |
val thm = assoc_thm' thy thm; (*28.10.02*)
|
neuper@37906
|
632 |
(*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
|
neuper@37906
|
633 |
in
|
neuper@37906
|
634 |
case rewrite_ thy
|
neuper@37906
|
635 |
((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls))
|
neuper@37906
|
636 |
put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
637 |
NONE => NONE
|
neuper@37906
|
638 |
| SOME (ctm, ctms) =>
|
neuper@37906
|
639 |
SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
|
neuper@37906
|
640 |
end;
|
neuper@37906
|
641 |
|
neuper@37906
|
642 |
(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
|
neuper@37906
|
643 |
thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
|
neuper@37906
|
644 |
fun rewrite_set_inst (thy':theory') (put_asm:bool)
|
neuper@37906
|
645 |
subs' (rls:rls') (ct:cterm') =
|
neuper@37906
|
646 |
let
|
neuper@37906
|
647 |
val thy = (the o assoc')(!theory',thy');
|
neuper@37906
|
648 |
val rls = assoc_rls rls
|
neuper@37906
|
649 |
val subst = subs'2subst thy subs'
|
neuper@37906
|
650 |
(*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
|
neuper@37906
|
651 |
in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
|
neuper@37906
|
652 |
((term_of o the o (parse thy)) ct) of
|
neuper@37906
|
653 |
NONE => NONE
|
neuper@37906
|
654 |
| SOME (t, ts) => SOME (term2str t, terms2str ts)
|
neuper@37906
|
655 |
end;
|
neuper@37906
|
656 |
|
neuper@37906
|
657 |
|
neuper@37906
|
658 |
(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
|
neuper@37906
|
659 |
fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
|
neuper@37906
|
660 |
|
neuper@37906
|
661 |
| eval_true' (thy':theory') (rls':rls') (t:term) =
|
neuper@37906
|
662 |
(* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres';
|
neuper@37906
|
663 |
*)
|
neuper@37906
|
664 |
let val ct' = term2str t;
|
neuper@37906
|
665 |
in case rewrite_set thy' false rls' ct' of
|
neuper@37906
|
666 |
SOME ("True",_) => true
|
neuper@37906
|
667 |
| _ => false
|
neuper@37906
|
668 |
end;
|
neuper@37906
|
669 |
fun eval_true_ _ _ (Const ("True",_)) = true
|
neuper@37906
|
670 |
| eval_true_ (thy':theory') rls t =
|
neuper@37906
|
671 |
case rewrite_set_ (assoc_thy thy') false rls t of
|
neuper@37906
|
672 |
SOME (Const ("True",_),_) => true
|
neuper@37906
|
673 |
| _ => false;
|
neuper@37906
|
674 |
|
neuper@37906
|
675 |
(*
|
neuper@37906
|
676 |
val test_rls =
|
neuper@37906
|
677 |
Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
|
neuper@37906
|
678 |
rules = [Calc ("matches",eval_matches "")
|
neuper@37906
|
679 |
],
|
neuper@37906
|
680 |
scr = Script ((term_of o the o (parse thy))
|
neuper@37906
|
681 |
"empty_script")
|
neuper@37906
|
682 |
}:rls;
|
neuper@37906
|
683 |
|
neuper@37906
|
684 |
|
neuper@37906
|
685 |
|
neuper@37906
|
686 |
rewrite_set_ Isac.thy eval_rls false test_rls
|
neuper@37906
|
687 |
((the o (parse thy)) "matches (?a = ?b) (x = #0)");
|
neuper@37906
|
688 |
val xxx = (term_of o the o (parse thy))
|
neuper@37906
|
689 |
"matches (?a = ?b) (x = #0)";
|
neuper@37906
|
690 |
eval_matches """" xxx thy;
|
neuper@37906
|
691 |
SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
|
neuper@37906
|
692 |
Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
|
neuper@37906
|
693 |
|
neuper@37906
|
694 |
|
neuper@37906
|
695 |
|
neuper@37906
|
696 |
rewrite_set_ Isac.thy eval_rls false eval_rls
|
neuper@37906
|
697 |
((the o (parse thy)) "contains_root (sqrt #0)");
|
neuper@37906
|
698 |
val it = SOME ("True",[]) : (cterm * cterm list) option
|
neuper@37906
|
699 |
|
neuper@37906
|
700 |
*)
|
neuper@37906
|
701 |
|
neuper@37906
|
702 |
|
neuper@37906
|
703 |
(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
|
neuper@37906
|
704 |
datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
|
neuper@37906
|
705 |
introduced with quick-and-dirty code*)
|
neuper@37906
|
706 |
fun determine dts =
|
neuper@37906
|
707 |
let val false_indet =
|
neuper@37906
|
708 |
filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
|
neuper@37906
|
709 |
val ts = map (#2: det * term -> term) dts
|
neuper@37906
|
710 |
in if nil = false_indet then (TRUE, ts)
|
neuper@37906
|
711 |
else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
|
neuper@37906
|
712 |
false_indet
|
neuper@37906
|
713 |
then (INDET, ts)
|
neuper@37906
|
714 |
else (FALSE, ts) end;
|
neuper@37906
|
715 |
(* val dts = [(INDET,e_term), (FALSE,HOLogic.false_const),
|
neuper@37906
|
716 |
(INDET,e_term), (TRUE,HOLogic.true_const)];
|
neuper@37906
|
717 |
determine dts;
|
neuper@37906
|
718 |
val it =
|
neuper@37906
|
719 |
(FALSE,
|
neuper@37906
|
720 |
[Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"),
|
neuper@37906
|
721 |
Const ("True","bool")]) : det * term list*)
|
neuper@37906
|
722 |
|
neuper@37906
|
723 |
fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*)
|
neuper@37906
|
724 |
if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, [])
|
neuper@37906
|
725 |
else if cs = [HOLogic.false_const] then (FALSE, cs)
|
neuper@37906
|
726 |
else
|
neuper@37906
|
727 |
let fun eval t =
|
neuper@37906
|
728 |
let val taopt = rewrite__set_ thy 1 false [] rls t
|
neuper@37906
|
729 |
in case taopt of
|
neuper@37906
|
730 |
SOME (t,_) =>
|
neuper@37906
|
731 |
if t = HOLogic.true_const then (TRUE, t)
|
neuper@37906
|
732 |
else if t = HOLogic.false_const then (FALSE, t)
|
neuper@37906
|
733 |
else (INDET, t)
|
neuper@37906
|
734 |
| NONE => (INDET, t) end
|
neuper@37906
|
735 |
in (determine o (map eval)) cs end;
|
neuper@37906
|
736 |
WN.16.5.0-------------------------------------------------------------*)
|