reorganise struct. ThmC, part 1
2 (c) Walther Neuper 2000
7 (*/------- to ThmC_Def -------\*)
8 val assoc_thm': theory -> ThmC_Def.thm' -> thm
9 val assoc_thm'': theory -> ThmC_Def.thmID -> thm
10 (*\------- to ThmC_Def -------/*)
11 val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
12 val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
13 val eval_prog_expr: theory -> Rule_Set.T -> term -> term
14 val eval_true_: theory -> Rule_Set.T -> term -> bool
15 val eval_true: theory -> term list -> Rule_Set.T -> bool
16 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
17 -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
18 val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
19 term -> (term * term list) option
20 val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
21 -> (term * term) list -> thm -> term -> (term * term list) option
22 val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
23 val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
24 val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
25 -> term -> (term * term list) option
26 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
28 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
29 val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
30 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
31 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
32 val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
33 val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
34 val mk_thm: theory -> string -> thm
35 val trace1: int -> string -> unit
36 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40 structure Rewrite(**): REWRITE(**) =
45 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
48 if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
50 if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
52 fun rewrite__ thy i bdv tless rls put_asm thm ct =
54 val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
55 (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct
56 in if rew then SOME (t', distinct asms) else NONE end
57 (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
58 and rew_sub thy i bdv tless rls put_asm lrd r t =
60 val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
61 (*?alternative Unify.matchers:
62 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
63 val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
64 val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
65 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
66 val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
67 then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.term_in_thy thy r') else ()
68 val (t'', p'') = (*conditional rewriting*)
70 val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
74 (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
75 then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.terms_in_thy thy p' ^
76 " stored: " ^ UnparseC.terms_in_thy thy simpl_p')
78 (t',simpl_p')) (* uncond.rew. from above*)
80 (if ! Celem.trace_rewrite andalso i < ! Celem.depth
81 then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.terms_in_thy thy p')
83 raise STOP_REW_SUB (* don't go into subterms of cond *))
86 if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
87 then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
88 then tracing (idt"#"i ^ " not: \"" ^ UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"")
91 else (t'', p'', [], true)
93 ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
95 Const(s,T) => (Const(s,T),[],lrd,false)
96 | Free(s,T) => (Free(s,T),[],lrd,false)
97 | Var(n,T) => (Var(n,T),[],lrd,false)
98 | Bound i => (Bound i,[],lrd,false)
100 let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
101 in (Abs(s, T, t'), asms, [], rew) end
103 let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
105 if rew2 then (t1 $ t2', asm2, lrd, true)
107 let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
108 in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
110 and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
111 if asms = [@{term True}] orelse asms = [] then ([], true)
112 else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
113 if asms = [@{term False}] then ([], false)
116 fun chk indets [] = (indets, true) (*return asms<>True until false*)
117 | chk indets (a :: asms) =
118 (case rewrite__set_ thy (i + 1) false bdv rls a of
119 NONE => (chk (indets @ [a]) asms)
121 if t = @{term True} then (chk (indets @ a') asms)
122 else if t = @{term False} then ([], false)
123 (*asm false .. thm not applied ^^^; continue until False vvv*)
124 else chk (indets @ [t] @ a') asms);
126 and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
127 error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_thy thy t ^ "'")
128 | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
130 val _= trace i (" rls: " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_thy thy t)
131 val (t', asm, rew) = app_rev thy (i + 1) rrls t
132 in if rew then SOME (t', distinct asm) else NONE end
133 | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
135 (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
136 datatype switch = Appl | Noap;
137 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
138 | rew_once ruls asm ct Appl [] =
139 (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
140 | Rule_Set.Seqence _ => (ct, asm)
141 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
142 | rew_once ruls asm ct apno (rul :: thms) =
144 Rule.Thm (thmid, thm) =>
145 (trace1 i (" try thm: \"" ^ thmid ^ "\"");
146 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
147 ((#erls o Rule_Set.rep) rls) put_asm thm ct of
148 NONE => rew_once ruls asm ct apno thms
149 | SOME (ct', asm') =>
150 (trace1 i (" rewrites to: \"" ^ UnparseC.term_in_thy thy ct' ^ "\"");
151 rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
152 (* once again try the same rule, e.g. associativity against "()"*)
153 | Rule.Num_Calc (cc as (op_, _)) =>
154 let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
155 val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
156 in case Num_Calc.adhoc_thm thy cc ct of
157 NONE => rew_once ruls asm ct apno thms
160 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
161 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
162 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
163 ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
164 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
165 in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
167 | Rule.Cal1 (cc as (op_, _)) =>
168 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
169 val ct = TermC.uminus_to_string ct
170 in case Num_Calc.adhoc_thm1_ thy cc ct of
174 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
175 ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
176 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
177 ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
178 val _ = trace1 i (" cal1. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
182 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
183 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
184 | NONE => rew_once ruls asm ct apno thms)
185 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");
186 val ruls = (#rules o Rule_Set.rep) rls;
187 val _ = trace i (" rls: " ^ Rule_Set.id rls ^ " on: " ^ UnparseC.term_in_thy thy ct)
188 val (ct', asm') = rew_once ruls [] ct Noap ruls;
189 in if ct = ct' then NONE else SOME (ct', distinct asm') end
190 (*-------------------------------------------------------------*)
191 and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
192 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
193 fun chk_prepat _ _ [] _ = true
194 | chk_prepat thy erls prepat t =
196 fun chk (pres, pat) =
198 val subst: Type.tyenv * Envir.tenv =
199 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
201 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
202 end) handle _ (*TODO Pattern.MATCH*) => false
203 fun scan_ _ [] = false
204 | scan_ f (pp :: pps) =
205 if f pp then true else scan_ f pps;
206 in scan_ chk prepat end;
207 (* apply the normal_form of a rev-set *)
208 fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
209 if chk_prepat thy erls prepat t then normal_form t else NONE
210 | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");
211 val opt = app_rev' thy rrls t
214 SOME (t', asm) => (t', asm, true)
215 | NONE => app_sub thy i rrls t
217 and app_sub thy i rrls t = (* apply an Rrls to subterms *)
219 Const (s, T) => (Const(s, T), [], false)
220 | Free (s, T) => (Free(s, T), [], false)
221 | Var (n, T) => (Var(n, T), [], false)
222 | Bound i => (Bound i, [], false)
223 | Abs (s, T, body) =>
224 let val (t', asm, rew) = app_rev thy i rrls body
225 in (Abs(s, T, t'), asm, rew) end
227 let val (t2', asm2, rew2) = app_rev thy i rrls t2
229 if rew2 then (t1 $ t2', asm2, true)
231 let val (t1', asm1, rew1) = app_rev thy i rrls t1
232 in if rew1 then (t1' $ t2, asm1, true)
233 else (t1 $ t2, [], false)
237 (* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
238 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
240 (* rewriting without internal argument [] *)
241 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
242 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
244 (* variants of rewrite; TODO del. put_asm *)
245 fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
246 rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
247 fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
249 (* given a list of equalities (lhs = rhs) and a term,
250 replace all occurrences of lhs in the term with rhs;
251 thus the order or equalities matters: put variables in lhs first. *)
252 fun rewrite_terms_ thy ord erls equs t =
254 fun rew_ (t', asm') [] _ = (t', asm')
255 | rew_ (t', asm') (rules as r::rs) t =
257 val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
260 then rew_ (t'', asm' @ asm'') rules t''
261 else rew_ (t', asm') rs t'
263 val (t'', asm'') = rew_ (TermC.empty, []) equs t
264 in if t'' = TermC.empty then NONE else SOME (t'', asm'')
267 (* search ct for adjacent numerals and calculate them by operator isa_fn *)
268 fun calculate_ thy isa_fn ct =
269 let val ct = TermC.uminus_to_string ct
270 in case Num_Calc.adhoc_thm thy isa_fn ct of
272 | SOME (thmID, thm) =>
273 (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
275 | NONE => raise ERROR ""
276 in SOME (rew, (thmID, thm)) end)
277 handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
280 (* Thm.make_thm added to Pure/thm.ML *)
283 val t = (Thm.term_of o the o (TermC.parse thy)) str
285 Const ("Pure.imp", _) $ _ $ _ => t
286 | _ => HOLogic.Trueprop $ t
287 in Thm.make_thm (Thm.global_cterm_of thy t') end;
289 (*/------- to ThmC_Def -------\*)
291 "metaview" as seen from programs and from user input;
292 both are parsed as terms by the function package.
294 fun convert_metaview_to_thmid thy thmid =
295 let val thmid' = case thmid of
296 "add_commute" => "add.commute"
297 | "mult_commute" => "mult.commute"
298 | "add_left_commute" => "add.left_commute"
299 | "mult_left_commute" => "mult.left_commute"
300 | "add_assoc" => "add.assoc"
301 | "mult_assoc" => "mult.assoc"
303 in (Global_Theory.get_thm thy) thmid' end;
305 (* get the theorem associated with the xstring-identifier;
306 if the identifier starts with "sym_" then swap lhs = rhs around =
307 (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
308 identifiers starting with "#" come from Num_Calc and
309 get a hand-made theorem (containing numerals only) *)
310 fun assoc_thm'' thy thmid =
311 case Symbol.explode thmid of
312 "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
313 | "s"::"y"::"m"::"_"::id => ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
314 | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
315 | _ => thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
316 fun assoc_thm' thy (thmid, ct') =
317 (case Symbol.explode thmid of
318 "s"::"y"::"m"::"_"::id =>
321 else ((ThmC.numerals_to_Free o (Global_Theory.get_thm thy)) (implode id)) RS sym
325 else thmid |> convert_metaview_to_thmid thy |> ThmC.numerals_to_Free
326 ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
328 ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
329 (*\------- to ThmC_Def -------/*)
332 fun eval_prog_expr thy srls t =
333 let val rew = rewrite_set_ thy false srls t;
334 in case rew of SOME (res,_) => res | NONE => t end;
336 fun eval_true_ _ _ (Const ("HOL.True",_)) = true
337 | eval_true_ thy rls t =
338 case rewrite_set_ thy false rls t of
339 SOME (Const ("HOL.True",_),_) => true