neuper@37906
|
1 |
(* isac's rewriter
|
neuper@37906
|
2 |
(c) Walther Neuper 2000
|
neuper@37906
|
3 |
*)
|
neuper@37906
|
4 |
|
wneuper@59380
|
5 |
signature REWRITE =
|
wneuper@59380
|
6 |
sig
|
wneuper@59405
|
7 |
val assoc_thm': theory -> Celem.thm' -> thm
|
wneuper@59405
|
8 |
val assoc_thm'': theory -> Celem.thmID -> thm
|
wneuper@59416
|
9 |
val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option
|
wneuper@59416
|
10 |
val eval__true: theory -> int -> term list -> (term * term) list -> Rule.rls -> term list * bool
|
wneuper@59416
|
11 |
val eval_listexpr_: theory -> Rule.rls -> term -> term
|
wneuper@59416
|
12 |
val eval_true: theory -> term list -> Rule.rls -> bool
|
wneuper@59416
|
13 |
val eval_true_: Rule.theory' -> Rule.rls -> term -> bool
|
wneuper@59405
|
14 |
val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
|
wneuper@59416
|
15 |
-> Rule.rls -> bool -> Celem.lrd list -> term -> term -> term * term list * Celem.lrd list * bool
|
wneuper@59416
|
16 |
val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool -> thm ->
|
wneuper@59405
|
17 |
term -> (term * term list) option
|
wneuper@59416
|
18 |
val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> bool
|
wneuper@59405
|
19 |
-> (term * term) list -> thm -> term -> (term * term list) option
|
wneuper@59416
|
20 |
val rewrite_set_: theory -> bool -> Rule.rls -> term -> (term * term list) option
|
wneuper@59416
|
21 |
val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
|
wneuper@59416
|
22 |
val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule.rls -> term list
|
wneuper@59405
|
23 |
-> term -> (term * term list) option
|
wneuper@59380
|
24 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59380
|
25 |
(* NONE *)
|
wneuper@59380
|
26 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59409
|
27 |
val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
|
wneuper@59416
|
28 |
Rule.rls -> bool -> thm -> term -> (term * term list) option
|
wneuper@59416
|
29 |
val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule.rls -> term -> (term * term list) option
|
wneuper@59416
|
30 |
val app_rev: theory -> int -> Rule.rls -> term -> term * term list * bool
|
wneuper@59416
|
31 |
val app_sub: theory -> int -> Rule.rls -> term -> term * term list * bool
|
wneuper@59380
|
32 |
val mk_thm: theory -> string -> thm
|
wneuper@59398
|
33 |
val trace1: int -> string -> unit
|
wneuper@59380
|
34 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59380
|
35 |
end
|
wneuper@59380
|
36 |
|
wneuper@59380
|
37 |
(**)
|
wneuper@59380
|
38 |
structure Rewrite(**): REWRITE(**) =
|
wneuper@59380
|
39 |
struct
|
wneuper@59380
|
40 |
(**)
|
neuper@37906
|
41 |
|
neuper@37906
|
42 |
exception NO_REWRITE;
|
neuper@37906
|
43 |
exception STOP_REW_SUB; (*WN050820 quick and dirty*)
|
neuper@37906
|
44 |
|
neuper@52101
|
45 |
fun trace i str =
|
wneuper@59405
|
46 |
if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
|
neuper@52101
|
47 |
fun trace1 i str =
|
wneuper@59405
|
48 |
if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
|
neuper@52101
|
49 |
|
neuper@37906
|
50 |
fun rewrite__ thy i bdv tless rls put_asm thm ct =
|
wneuper@59381
|
51 |
let
|
wneuper@59405
|
52 |
val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: Celem.lrd list)
|
wneuper@59389
|
53 |
(((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct
|
wneuper@59381
|
54 |
in if rew then SOME (t', distinct asms) else NONE end
|
wneuper@59383
|
55 |
(* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
|
wneuper@59381
|
56 |
and rew_sub thy i bdv tless rls put_asm lrd r t =
|
neuper@38022
|
57 |
(let
|
wneuper@59381
|
58 |
val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
|
wneuper@59381
|
59 |
(*?alternative Unify.matchers:
|
wneuper@59381
|
60 |
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
|
wneuper@59381
|
61 |
val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
|
wneuper@59381
|
62 |
val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
|
wneuper@59381
|
63 |
val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
|
wneuper@59405
|
64 |
val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
|
wneuper@59416
|
65 |
then tracing (idt "#" (i + 1) ^ " eval asms: " ^ Rule.t2str thy r') else ()
|
wneuper@59381
|
66 |
val (t'', p'') = (*conditional rewriting*)
|
wneuper@59381
|
67 |
let
|
wneuper@59381
|
68 |
val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
|
wneuper@59381
|
69 |
in
|
wneuper@59381
|
70 |
if nofalse
|
wneuper@59381
|
71 |
then
|
wneuper@59405
|
72 |
(if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
|
wneuper@59416
|
73 |
then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ Rule.ts2str thy p' ^
|
wneuper@59416
|
74 |
" stored: " ^ Rule.ts2str thy simpl_p')
|
wneuper@59381
|
75 |
else();
|
wneuper@59381
|
76 |
(t',simpl_p')) (* uncond.rew. from above*)
|
wneuper@59381
|
77 |
else
|
wneuper@59405
|
78 |
(if ! Celem.trace_rewrite andalso i < ! Celem.depth
|
wneuper@59416
|
79 |
then tracing (idt "#" (i + 1) ^ " asms false: " ^ Rule.ts2str thy p')
|
wneuper@59381
|
80 |
else();
|
wneuper@59381
|
81 |
raise STOP_REW_SUB (* don't go into subterms of cond *))
|
wneuper@59381
|
82 |
end
|
wneuper@59381
|
83 |
in
|
wneuper@59389
|
84 |
if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
|
wneuper@59405
|
85 |
then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
|
wneuper@59416
|
86 |
then tracing (idt"#"i ^ " not: \"" ^ Rule.t2str thy t ^ "\" > \"" ^ Rule.t2str thy t' ^ "\"")
|
wneuper@59381
|
87 |
else ();
|
wneuper@59381
|
88 |
raise NO_REWRITE)
|
wneuper@59381
|
89 |
else (t'', p'', [], true)
|
wneuper@59381
|
90 |
end
|
wneuper@59383
|
91 |
) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
|
wneuper@59381
|
92 |
(case t of
|
wneuper@59381
|
93 |
Const(s,T) => (Const(s,T),[],lrd,false)
|
neuper@37906
|
94 |
| Free(s,T) => (Free(s,T),[],lrd,false)
|
neuper@37906
|
95 |
| Var(n,T) => (Var(n,T),[],lrd,false)
|
neuper@37906
|
96 |
| Bound i => (Bound i,[],lrd,false)
|
neuper@37906
|
97 |
| Abs(s,T,body) =>
|
wneuper@59405
|
98 |
let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.D]) r body
|
wneuper@59381
|
99 |
in (Abs(s, T, t'), asms, [], rew) end
|
neuper@37906
|
100 |
| t1 $ t2 =>
|
wneuper@59405
|
101 |
let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.R]) r t2
|
wneuper@59381
|
102 |
in
|
wneuper@59381
|
103 |
if rew2 then (t1 $ t2', asm2, lrd, true)
|
wneuper@59381
|
104 |
else
|
wneuper@59405
|
105 |
let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [Celem.L]) r t1
|
wneuper@59381
|
106 |
in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
|
wneuper@59381
|
107 |
end)
|
wneuper@59381
|
108 |
and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
|
neuper@48760
|
109 |
if asms = [@{term True}] orelse asms = [] then ([], true)
|
wneuper@59381
|
110 |
else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
|
wneuper@59381
|
111 |
if asms = [@{term False}] then ([], false)
|
wneuper@59381
|
112 |
else
|
wneuper@59381
|
113 |
let
|
wneuper@59381
|
114 |
fun chk indets [] = (indets, true) (*return asms<>True until false*)
|
wneuper@59381
|
115 |
| chk indets (a :: asms) =
|
wneuper@59381
|
116 |
(case rewrite__set_ thy (i + 1) false bdv rls a of
|
wneuper@59381
|
117 |
NONE => (chk (indets @ [a]) asms)
|
wneuper@59381
|
118 |
| SOME (t, a') =>
|
wneuper@59381
|
119 |
if t = @{term True} then (chk (indets @ a') asms)
|
wneuper@59381
|
120 |
else if t = @{term False} then ([], false)
|
wneuper@59381
|
121 |
(*asm false .. thm not applied ^^^; continue until False vvv*)
|
wneuper@59381
|
122 |
else chk (indets @ [t] @ a') asms);
|
wneuper@59381
|
123 |
in chk [] asms end
|
wneuper@59416
|
124 |
and rewrite__set_ thy _ __ Rule.Erls t = (* rewrite with a rule set *)
|
wneuper@59416
|
125 |
error ("rewrite__set_ called with 'Erls' for '" ^ Rule.t2str thy t ^ "'")
|
wneuper@59416
|
126 |
| rewrite__set_ thy i _ _ (rrls as Rule.Rrls _) t = (* rewrite with a 'reverse rule set' *)
|
neuper@52101
|
127 |
let
|
wneuper@59416
|
128 |
val _= trace i (" rls: " ^ Rule.id_rls rrls ^ " on: " ^ Rule.t2str thy t)
|
wneuper@59382
|
129 |
val (t', asm, rew) = app_rev thy (i + 1) rrls t
|
neuper@52101
|
130 |
in if rew then SOME (t', distinct asm) else NONE end
|
wneuper@59382
|
131 |
| rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Calc, Cal1 *)
|
neuper@52101
|
132 |
let
|
wneuper@59398
|
133 |
(* attention with cp to test/..: unbound thy, i, bdv, rls TODO1803? pull out to rewrite__*)
|
neuper@52101
|
134 |
datatype switch = Appl | Noap;
|
wneuper@59399
|
135 |
fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Tools.rew_once? *)
|
neuper@52101
|
136 |
| rew_once ruls asm ct Appl [] =
|
wneuper@59416
|
137 |
(case rls of Rule.Rls _ => rew_once ruls asm ct Noap ruls
|
wneuper@59416
|
138 |
| Rule.Seq _ => (ct, asm)
|
wneuper@59416
|
139 |
| rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
|
wneuper@59381
|
140 |
| rew_once ruls asm ct apno (rul :: thms) =
|
neuper@52101
|
141 |
case rul of
|
wneuper@59416
|
142 |
Rule.Thm (thmid, thm) =>
|
neuper@52101
|
143 |
(trace1 i (" try thm: " ^ thmid);
|
wneuper@59416
|
144 |
case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
wneuper@59416
|
145 |
((#erls o Rule.rep_rls) rls) put_asm thm ct of
|
neuper@52101
|
146 |
NONE => rew_once ruls asm ct apno thms
|
wneuper@59381
|
147 |
| SOME (ct', asm') =>
|
wneuper@59416
|
148 |
(trace1 i (" rewrites to: " ^ Rule.t2str thy ct');
|
wneuper@59399
|
149 |
rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
|
wneuper@59399
|
150 |
(* once again try the same rule, e.g. associativity against "()"*)
|
wneuper@59416
|
151 |
| Rule.Calc (cc as (op_, _)) =>
|
neuper@52101
|
152 |
let val _= trace1 i (" try calc: " ^ op_ ^ "'")
|
wneuper@59389
|
153 |
val ct = TermC.uminus_to_string ct
|
wneuper@59386
|
154 |
in case Calc.adhoc_thm thy cc ct of
|
neuper@52101
|
155 |
NONE => rew_once ruls asm ct apno thms
|
wneuper@59381
|
156 |
| SOME (_, thm') =>
|
neuper@52101
|
157 |
let
|
wneuper@59416
|
158 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
wneuper@59416
|
159 |
((#erls o Rule.rep_rls) rls) put_asm thm' ct;
|
neuper@52101
|
160 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
wneuper@59416
|
161 |
Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
|
wneuper@59416
|
162 |
val _ = trace1 i (" calc. to: " ^ Rule.t2str thy ((fst o the) pairopt))
|
neuper@52101
|
163 |
in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
|
neuper@52101
|
164 |
end
|
wneuper@59416
|
165 |
| Rule.Cal1 (cc as (op_, _)) =>
|
neuper@52101
|
166 |
let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
|
wneuper@59389
|
167 |
val ct = TermC.uminus_to_string ct
|
wneuper@59386
|
168 |
in case Calc.adhoc_thm1_ thy cc ct of
|
neuper@52101
|
169 |
NONE => (ct, asm)
|
wneuper@59381
|
170 |
| SOME (_, thm') =>
|
neuper@52101
|
171 |
let
|
wneuper@59416
|
172 |
val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.rep_rls) rls)
|
wneuper@59416
|
173 |
((#erls o Rule.rep_rls) rls) put_asm thm' ct;
|
neuper@52101
|
174 |
val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
|
wneuper@59416
|
175 |
Rule.string_of_thmI thm' ^ "\" " ^ Rule.t2str thy ct ^ " = NONE")
|
wneuper@59416
|
176 |
val _ = trace1 i (" cal1. to: " ^ Rule.t2str thy ((fst o the) pairopt))
|
neuper@52101
|
177 |
in the pairopt end
|
neuper@52101
|
178 |
end
|
wneuper@59416
|
179 |
| Rule.Rls_ rls' =>
|
neuper@52101
|
180 |
(case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
|
neuper@52101
|
181 |
SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
|
wneuper@59381
|
182 |
| NONE => rew_once ruls asm ct apno thms)
|
wneuper@59416
|
183 |
| r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
|
wneuper@59416
|
184 |
val ruls = (#rules o Rule.rep_rls) rls;
|
wneuper@59416
|
185 |
val _ = trace i (" rls: " ^ Rule.id_rls rls ^ " on: " ^ Rule.t2str thy ct)
|
neuper@52101
|
186 |
val (ct', asm') = rew_once ruls [] ct Noap ruls;
|
neuper@52101
|
187 |
in if ct = ct' then NONE else SOME (ct', distinct asm') end
|
wneuper@59405
|
188 |
(*------------------------
|
wneuper@59405
|
189 |
-------------------------------------*)
|
wneuper@59381
|
190 |
and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
|
neuper@52085
|
191 |
let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
|
wneuper@59381
|
192 |
fun chk_prepat _ _ [] _ = true
|
neuper@52085
|
193 |
| chk_prepat thy erls prepat t =
|
neuper@52085
|
194 |
let
|
neuper@52085
|
195 |
fun chk (pres, pat) =
|
neuper@52085
|
196 |
(let
|
neuper@52085
|
197 |
val subst: Type.tyenv * Envir.tenv =
|
neuper@52085
|
198 |
Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
|
neuper@52085
|
199 |
in
|
neuper@52085
|
200 |
snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
|
wneuper@59381
|
201 |
end) handle _ (*TODO Pattern.MATCH*) => false
|
wneuper@59381
|
202 |
fun scan_ _ [] = false
|
wneuper@59398
|
203 |
| scan_ f (pp :: pps) =
|
neuper@52085
|
204 |
if f pp then true else scan_ f pps;
|
neuper@52085
|
205 |
in scan_ chk prepat end;
|
neuper@52085
|
206 |
(* apply the normal_form of a rev-set *)
|
wneuper@59416
|
207 |
fun app_rev' thy (Rule.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
|
wneuper@59381
|
208 |
if chk_prepat thy erls prepat t then normal_form t else NONE
|
wneuper@59416
|
209 |
| app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule.rls2str r ^ "\"");
|
neuper@52085
|
210 |
val opt = app_rev' thy rrls t
|
neuper@52085
|
211 |
in
|
neuper@52085
|
212 |
case opt of
|
neuper@52085
|
213 |
SOME (t', asm) => (t', asm, true)
|
neuper@52085
|
214 |
| NONE => app_sub thy i rrls t
|
neuper@52085
|
215 |
end
|
wneuper@59381
|
216 |
and app_sub thy i rrls t = (* apply an Rrls to subterms *)
|
neuper@52085
|
217 |
case t of
|
neuper@52085
|
218 |
Const (s, T) => (Const(s, T), [], false)
|
neuper@52085
|
219 |
| Free (s, T) => (Free(s, T), [], false)
|
neuper@52085
|
220 |
| Var (n, T) => (Var(n, T), [], false)
|
neuper@52085
|
221 |
| Bound i => (Bound i, [], false)
|
neuper@52085
|
222 |
| Abs (s, T, body) =>
|
neuper@37906
|
223 |
let val (t', asm, rew) = app_rev thy i rrls body
|
neuper@37906
|
224 |
in (Abs(s, T, t'), asm, rew) end
|
neuper@52085
|
225 |
| t1 $ t2 =>
|
neuper@52085
|
226 |
let val (t2', asm2, rew2) = app_rev thy i rrls t2
|
neuper@52085
|
227 |
in
|
neuper@52085
|
228 |
if rew2 then (t1 $ t2', asm2, true)
|
neuper@52085
|
229 |
else
|
neuper@52085
|
230 |
let val (t1', asm1, rew1) = app_rev thy i rrls t1
|
neuper@52085
|
231 |
in if rew1 then (t1' $ t2, asm1, true)
|
neuper@52085
|
232 |
else (t1 $ t2, [], false)
|
neuper@52085
|
233 |
end
|
wneuper@59381
|
234 |
end;
|
neuper@37906
|
235 |
|
wneuper@59381
|
236 |
(* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
|
neuper@37906
|
237 |
fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
|
neuper@37906
|
238 |
|
neuper@52101
|
239 |
(* rewriting without internal argument [] *)
|
neuper@52101
|
240 |
fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
|
neuper@52101
|
241 |
fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
|
neuper@37906
|
242 |
|
wneuper@59381
|
243 |
(* variants of rewrite; TODO del. put_asm *)
|
wneuper@59381
|
244 |
fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
|
wneuper@59381
|
245 |
rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
|
wneuper@59381
|
246 |
fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
|
neuper@37906
|
247 |
|
neuper@38025
|
248 |
(* given a list of equalities (lhs = rhs) and a term,
|
neuper@38025
|
249 |
replace all occurrences of lhs in the term with rhs;
|
neuper@38025
|
250 |
thus the order or equalities matters: put variables in lhs first. *)
|
neuper@38025
|
251 |
fun rewrite_terms_ thy ord erls equs t =
|
neuper@42359
|
252 |
let
|
neuper@42359
|
253 |
fun rew_ (t', asm') [] _ = (t', asm')
|
neuper@42359
|
254 |
| rew_ (t', asm') (rules as r::rs) t =
|
neuper@42359
|
255 |
let
|
wneuper@59390
|
256 |
val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
|
neuper@42359
|
257 |
in
|
neuper@42359
|
258 |
if rew
|
neuper@42359
|
259 |
then rew_ (t'', asm' @ asm'') rules t''
|
neuper@42359
|
260 |
else rew_ (t', asm') rs t'
|
neuper@42359
|
261 |
end
|
wneuper@59416
|
262 |
val (t'', asm'') = rew_ (Rule.e_term, []) equs t
|
wneuper@59416
|
263 |
in if t'' = Rule.e_term then NONE else SOME (t'', asm'')
|
neuper@42359
|
264 |
end;
|
neuper@37906
|
265 |
|
wneuper@59381
|
266 |
(* search ct for adjacent numerals and calculate them by operator isa_fn *)
|
neuper@37906
|
267 |
fun calculate_ thy isa_fn ct =
|
wneuper@59389
|
268 |
let val ct = TermC.uminus_to_string ct
|
wneuper@59386
|
269 |
in case Calc.adhoc_thm thy isa_fn ct of
|
neuper@37906
|
270 |
NONE => NONE
|
wneuper@59381
|
271 |
| SOME (thmID, thm) =>
|
wneuper@59416
|
272 |
(let val rew = case rewrite_ thy Rule.dummy_ord Rule.e_rls false thm ct of
|
wneuper@59381
|
273 |
SOME (rew, _) => rew
|
wneuper@59381
|
274 |
| NONE => raise ERROR ""
|
wneuper@59381
|
275 |
in SOME (rew, (thmID, thm)) end)
|
wneuper@59381
|
276 |
handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
|
neuper@37906
|
277 |
end;
|
neuper@37906
|
278 |
|
wneuper@59381
|
279 |
(* Thm.make_thm added to Pure/thm.ML *)
|
neuper@37906
|
280 |
fun mk_thm thy str =
|
wneuper@59385
|
281 |
let
|
wneuper@59389
|
282 |
val t = (Thm.term_of o the o (TermC.parse thy)) str
|
wneuper@59385
|
283 |
val t' = case t of
|
wneuper@59385
|
284 |
Const ("Pure.imp", _) $ _ $ _ => t
|
wneuper@59390
|
285 |
| _ => HOLogic.Trueprop $ t
|
wneuper@59385
|
286 |
in Thm.make_thm (Thm.global_cterm_of thy t') end;
|
neuper@37906
|
287 |
|
wneuper@59108
|
288 |
(* "metaview" as seen from programs and from user input (both are parsed like terms presently) *)
|
wneuper@59108
|
289 |
fun convert_metaview_to_thmid thy thmid =
|
wneuper@59108
|
290 |
let val thmid' = case thmid of
|
wneuper@59108
|
291 |
"add_commute" => "add.commute"
|
wneuper@59108
|
292 |
| "mult_commute" => "mult.commute"
|
wneuper@59108
|
293 |
| "add_left_commute" => "add.left_commute"
|
wneuper@59108
|
294 |
| "mult_left_commute" => "mult.left_commute"
|
wneuper@59108
|
295 |
| "add_assoc" => "add.assoc"
|
wneuper@59108
|
296 |
| "mult_assoc" => "mult.assoc"
|
wneuper@59108
|
297 |
| _ => thmid
|
wneuper@59108
|
298 |
in (Global_Theory.get_thm thy) thmid' end;
|
wneuper@59108
|
299 |
|
wneuper@59381
|
300 |
(* get the theorem associated with the xstring-identifier;
|
neuper@37906
|
301 |
if the identifier starts with "sym_" then swap lhs = rhs around =
|
neuper@37906
|
302 |
(ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
|
neuper@37906
|
303 |
identifiers starting with "#" come from Calc and
|
wneuper@59381
|
304 |
get a hand-made theorem (containing numerals only) *)
|
wneuper@59381
|
305 |
fun assoc_thm'' thy thmid =
|
wneuper@59253
|
306 |
case Symbol.explode thmid of
|
wneuper@59253
|
307 |
"s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
|
wneuper@59389
|
308 |
| "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
|
wneuper@59253
|
309 |
| "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
|
wneuper@59389
|
310 |
| _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str
|
wneuper@59381
|
311 |
fun assoc_thm' thy (thmid, ct') =
|
neuper@55487
|
312 |
(case Symbol.explode thmid of
|
neuper@55487
|
313 |
"s"::"y"::"m"::"_"::id =>
|
neuper@55487
|
314 |
if hd id = "#"
|
neuper@55487
|
315 |
then mk_thm thy ct'
|
wneuper@59389
|
316 |
else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
|
wneuper@59109
|
317 |
| id =>
|
neuper@55487
|
318 |
if hd id = "#"
|
neuper@55487
|
319 |
then mk_thm thy ct'
|
wneuper@59389
|
320 |
else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
|
wneuper@59381
|
321 |
) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
|
wneuper@59416
|
322 |
error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Rule.theory2domID thy ^ "\" (and parents)")
|
neuper@37906
|
323 |
|
neuper@37906
|
324 |
fun eval_listexpr_ thy srls t =
|
neuper@52139
|
325 |
let val rew = rewrite_set_ thy false srls t;
|
neuper@52139
|
326 |
in case rew of SOME (res,_) => res | NONE => t end;
|
neuper@37906
|
327 |
|
neuper@41928
|
328 |
fun eval_true_ _ _ (Const ("HOL.True",_)) = true
|
wneuper@59405
|
329 |
| eval_true_ thy' rls t =
|
wneuper@59405
|
330 |
case rewrite_set_ (Celem.assoc_thy thy') false rls t of
|
neuper@41928
|
331 |
SOME (Const ("HOL.True",_),_) => true
|
neuper@37906
|
332 |
| _ => false;
|
neuper@37906
|
333 |
|
wneuper@59380
|
334 |
end |