2 (c) Walther Neuper 2000
7 val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
8 val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
9 val eval_prog_expr: theory -> Rule_Set.T -> term -> term
10 val eval_true_: theory -> Rule_Set.T -> term -> bool
11 val eval_true: theory -> term list -> Rule_Set.T -> bool
12 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
13 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
14 val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
15 term -> (term * term list) option
16 val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
17 -> (term * term) list -> thm -> term -> (term * term list) option
18 val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
19 val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
20 val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
21 -> term -> (term * term list) option
22 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
25 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
26 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
27 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
28 val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
29 val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
30 val trace1: int -> string -> unit
31 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
35 structure Rewrite(**): REWRITE(**) =
40 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
43 if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
45 if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
47 fun rewrite__ thy i bdv tless rls put_asm thm ct =
49 val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
50 (((TermC.inst_bdv bdv) o Eval.norm o #prop o Thm.rep_thm) thm) ct
51 in if rew then SOME (t', distinct asms) else NONE end
52 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
53 and rew_sub thy i bdv tless rls put_asm lrd r t =
55 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
56 (*?alternative Unify.matchers:
57 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
58 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
59 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
60 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
61 val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
62 then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
63 val (t'', p'') = (*conditional rewriting*)
65 val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
69 (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
70 then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
71 " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
73 (t',simpl_p')) (* uncond.rew. from above*)
75 (if ! Celem.trace_rewrite andalso i < ! Celem.depth
76 then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
78 raise STOP_REW_SUB (* don't go into subterms of cond *))
81 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
82 then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
83 then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
86 else (t'', p'', [], true)
88 ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
90 Const(s,T) => (Const(s,T),[],lrd,false)
91 | Free(s,T) => (Free(s,T),[],lrd,false)
92 | Var(n,T) => (Var(n,T),[],lrd,false)
93 | Bound i => (Bound i,[],lrd,false)
95 let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
96 in (Abs(s, T, t'), asms, [], rew) end
98 let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
100 if rew2 then (t1 $ t2', asm2, lrd, true)
102 let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
103 in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
105 and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
106 if asms = [@{term True}] orelse asms = [] then ([], true)
107 else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
108 if asms = [@{term False}] then ([], false)
111 fun chk indets [] = (indets, true) (*return asms<>True until false*)
112 | chk indets (a :: asms) =
113 (case rewrite__set_ thy (i + 1) false bdv rls a of
114 NONE => (chk (indets @ [a]) asms)
116 if t = @{term True} then (chk (indets @ a') asms)
117 else if t = @{term False} then ([], false)
118 (*asm false .. thm not applied ^^^; continue until False vvv*)
119 else chk (indets @ [t] @ a') asms);
121 and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
122 error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
123 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
125 val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
126 val (t', asm, rew) = app_rev thy (i + 1) rrls t
127 in if rew then SOME (t', distinct asm) else NONE end
128 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Eval, Cal1 *)
130 (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
131 datatype switch = Appl | Noap;
132 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
133 | rew_once ruls asm ct Appl [] =
134 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
135 | Rule_Set.Sequence _ => (ct, asm)
136 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
137 | rew_once ruls asm ct apno (rul :: thms) =
139 Rule.Thm (thmid, thm) =>
140 (trace1 i (" try thm: \"" ^ thmid ^ "\"");
141 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
142 ((#erls o Rule_Set.rep) rls) put_asm thm ct of
143 NONE => rew_once ruls asm ct apno thms
144 | SOME (ct', asm') =>
145 (trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
146 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
147 (* once again try the same rule, e.g. associativity against "()"*)
148 | Rule.Eval (cc as (op_, _)) =>
149 let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
150 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
151 in case Eval.adhoc_thm thy cc ct of
152 NONE => rew_once ruls asm ct apno thms
155 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
156 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
157 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
158 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
159 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
160 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
162 | Rule.Cal1 (cc as (op_, _)) =>
163 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
164 val ct = TermC.uminus_to_string ct
165 in case Eval.adhoc_thm1_ thy cc ct of
169 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
170 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
171 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
172 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
173 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
177 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
178 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
179 | NONE => rew_once ruls asm ct apno thms)
180 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
181 val ruls = (#rules o Rule_Set.rep) rls;
182 val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)
183 val (ct', asm') = rew_once ruls [] ct Noap ruls;
184 in if ct = ct' then NONE else SOME (ct', distinct asm') end
185 (*-------------------------------------------------------------*)
186 and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
187 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
188 fun chk_prepat _ _ [] _ = true
189 | chk_prepat thy erls prepat t =
191 fun chk (pres, pat) =
193 val subst: Type.tyenv * Envir.tenv =
194 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
196 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
197 end) handle _ (*TODO Pattern.MATCH*) => false
198 fun scan_ _ [] = false
199 | scan_ f (pp :: pps) =
200 if f pp then true else scan_ f pps;
201 in scan_ chk prepat end;
202 (* apply the normal_form of a rev-set *)
203 fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
204 if chk_prepat thy erls prepat t then normal_form t else NONE
205 | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
206 val opt = app_rev' thy rrls t
209 SOME (t', asm) => (t', asm, true)
210 | NONE => app_sub thy i rrls t
212 and app_sub thy i rrls t = (* apply an Rrls to subterms *)
214 Const (s, T) => (Const(s, T), [], false)
215 | Free (s, T) => (Free(s, T), [], false)
216 | Var (n, T) => (Var(n, T), [], false)
217 | Bound i => (Bound i, [], false)
218 | Abs (s, T, body) =>
219 let val (t', asm, rew) = app_rev thy i rrls body
220 in (Abs(s, T, t'), asm, rew) end
222 let val (t2', asm2, rew2) = app_rev thy i rrls t2
224 if rew2 then (t1 $ t2', asm2, true)
226 let val (t1', asm1, rew1) = app_rev thy i rrls t1
227 in if rew1 then (t1' $ t2, asm1, true)
228 else (t1 $ t2, [], false)
232 (* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
233 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
235 (* rewriting without internal argument [] *)
236 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
237 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
239 (* variants of rewrite; TODO del. put_asm *)
240 fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
241 rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
242 fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
244 (* given a list of equalities (lhs = rhs) and a term,
245 replace all occurrences of lhs in the term with rhs;
246 thus the order or equalities matters: put variables in lhs first. *)
247 fun rewrite_terms_ thy ord erls equs t =
249 fun rew_ (t', asm') [] _ = (t', asm')
250 | rew_ (t', asm') (rules as r::rs) t =
252 val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
255 then rew_ (t'', asm' @ asm'') rules t''
256 else rew_ (t', asm') rs t'
258 val (t'', asm'') = rew_ (TermC.empty, []) equs t
259 in if t'' = TermC.empty then NONE else SOME (t'', asm'')
262 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
263 fun calculate_ thy isa_fn ct =
264 let val ct = TermC.uminus_to_string ct
265 in case Eval.adhoc_thm thy isa_fn ct of
267 | SOME (thmID, thm) =>
268 (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
270 | NONE => raise ERROR ""
271 in SOME (rew, (thmID, thm)) end)
272 handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
275 fun eval_prog_expr thy srls t =
276 let val rew = rewrite_set_ thy false srls t;
277 in case rew of SOME (res,_) => res | NONE => t end;
279 fun eval_true_ _ _ (Const ("HOL.True",_)) = true
280 | eval_true_ thy rls t =
281 case rewrite_set_ thy false rls t of
282 SOME (Const ("HOL.True",_),_) => true