1.1 --- a/src/Tools/isac/Build_Isac.thy Fri Feb 23 07:29:36 2018 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sat Feb 24 11:14:56 2018 +0100
1.3 @@ -73,6 +73,7 @@
1.4 ML {*
1.5 *} ML {*
1.6 *}
1.7 +ML {* Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *) *}
1.8 ML {* LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
1.9 ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *}
1.10 ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Fri Feb 23 07:29:36 2018 +0100
2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sat Feb 24 11:14:56 2018 +0100
2.3 @@ -61,150 +61,102 @@
2.4 fun trace1 i str =
2.5 if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
2.6
2.7 -(*
2.8 -Synopsis rewriting (prep for reference manual):
2.9 -----------------------------------------------
2.10 -Rewriting uses theorems for transforming terms. However, not all kinds
2.11 -of such transformations can be done by rewriting. Examples are
2.12 -calculation with numerals or cancellation of fractions.
2.13 -
2.14 -Isac tries to present transformations like calculations or cancellation
2.15 -as simple rewrite steps for the naive user. However, some of such
2.16 -transformations should be transparent to the user by single-stepping.
2.17 -For instance, cancellation involves interesting CA algorithms like
2.18 -GCD of multivariate polynomials.
2.19 -
2.20 -Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",
2.21 -the former for steps which are not meant to be inspected by single-stepping
2.22 -the latter meant for single-stepping and providing respective mechanisms.
2.23 -
2.24 -(1) Inclusion by "thm Calc" for 1-step execution
2.25 -TODO
2.26 -
2.27 -(2) Inclusion by "Rrls" for multi-step execution
2.28 -TODO
2.29 -In multi-step execution "reverse rewriting" worked only as passive presentation
2.30 -without any interaction. So the functions init_state, locate_rule etc are just dummies.
2.31 -TODO
2.32 -? multi-step execution did never work.
2.33 -what worked is "reverse rewriting",
2.34 -i.e. presentation of intermediate steps *without* interaction
2.35 -TODO
2.36 -# type rule and scr | Rfuns
2.37 -# type rrlsstate = (*state for reverse rewriting*)
2.38 -# type and rls | Rrls
2.39 -all in calcelems.sml
2.40 -TODO
2.41 -*)
2.42 fun rewrite__ thy i bdv tless rls put_asm thm ct =
2.43 + let
2.44 + val(t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
2.45 + (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm) ct
2.46 + in if rew then SOME (t', distinct asms) else NONE end
2.47 +and rew_sub thy i bdv tless rls put_asm lrd r t =
2.48 (let
2.49 - val (t',asms,lrd,rew) =
2.50 - rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
2.51 - (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm) ct;
2.52 - in if rew then SOME (t', distinct asms)
2.53 - else NONE end)
2.54 -(* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
2.55 -and rew_sub thy i bdv tless rls put_asm lrd r t =
2.56 - ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));
2.57 - tracing ("@@@ rew_sub begin: bdv = "^(@{make_string} bdv));
2.58 - tracing ("@@@ rew_sub begin: r = "^(term2str r));*)
2.59 - let (* copy from Pure/thm.ML: fun rewritec *)
2.60 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
2.61 - o Logic.strip_imp_concl) r;
2.62 - (*?alternative Unify.matchers:
2.63 - http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
2.64 - val r' = Envir.subst_term (Pattern.match thy (lhs, t)
2.65 - (Vartab.empty, Vartab.empty)) r;
2.66 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
2.67 - (Logic.count_prems r', [], r'));
2.68 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
2.69 - o Logic.strip_imp_concl) r';
2.70 - (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)
2.71 - val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.72 - then tracing((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
2.73 - val (t'',p'') = (*conditional rewriting*)
2.74 - let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
2.75 - in if nofalse
2.76 - then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.77 - then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
2.78 - " stored: "^(terms2str simpl_p'))
2.79 - else(); (t',simpl_p')) (* uncond.rew. from above*)
2.80 - else
2.81 - (if ! trace_rewrite andalso i < ! depth
2.82 - then tracing((idt"#"(i+1))^" asms false: "^(terms2str p'))
2.83 - else(); raise STOP_REW_SUB (*dont go into subterms of cond*))
2.84 - end
2.85 - in if perm lhs rhs andalso not (tless bdv (t',t)) (*ordered rewriting*)
2.86 - then (if ! trace_rewrite andalso i < ! depth
2.87 - then tracing((idt"#"i)^" not: \""^
2.88 - (term2str t)^"\" > \""^
2.89 - (term2str t')^"\"") else ();
2.90 - raise NO_REWRITE )
2.91 - else ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^
2.92 - ", p'' ="^(terms2str p'')^", true)");*)
2.93 - (t'',p'',[],true))
2.94 - end
2.95 - ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) =>
2.96 - ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)
2.97 - case t of
2.98 - Const(s,T) => (Const(s,T),[],lrd,false)
2.99 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
2.100 + (*?alternative Unify.matchers:
2.101 + http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
2.102 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
2.103 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
2.104 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
2.105 + val _ = if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.106 + then tracing (idt "#" (i + 1) ^ " eval asms: " ^ term2str r') else ()
2.107 + val (t'', p'') = (*conditional rewriting*)
2.108 + let
2.109 + val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
2.110 + in
2.111 + if nofalse
2.112 + then
2.113 + (if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.114 + then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ terms2str p' ^
2.115 + " stored: " ^ terms2str simpl_p')
2.116 + else();
2.117 + (t',simpl_p')) (* uncond.rew. from above*)
2.118 + else
2.119 + (if ! trace_rewrite andalso i < ! depth
2.120 + then tracing (idt "#" (i + 1) ^ " asms false: " ^ terms2str p')
2.121 + else();
2.122 + raise STOP_REW_SUB (* don't go into subterms of cond *))
2.123 + end
2.124 + in
2.125 + if perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
2.126 + then (if ! trace_rewrite andalso i < ! depth
2.127 + then tracing (idt"#"i ^ " not: \"" ^ term2str t ^ "\" > \"" ^ term2str t' ^ "\"")
2.128 + else ();
2.129 + raise NO_REWRITE)
2.130 + else (t'', p'', [], true)
2.131 + end
2.132 + ) handle Pattern.MATCH (*TODO Pattern.MATCH when tests are ready *) =>
2.133 + (case t of
2.134 + Const(s,T) => (Const(s,T),[],lrd,false)
2.135 | Free(s,T) => (Free(s,T),[],lrd,false)
2.136 | Var(n,T) => (Var(n,T),[],lrd,false)
2.137 | Bound i => (Bound i,[],lrd,false)
2.138 | Abs(s,T,body) =>
2.139 - let val (t', asms, lrd, rew) =
2.140 - rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
2.141 - in (Abs(s,T,t'), asms, [], rew) end
2.142 + let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [D]) r body
2.143 + in (Abs(s, T, t'), asms, [], rew) end
2.144 | t1 $ t2 =>
2.145 - let val (t2', asm2, lrd, rew2) =
2.146 - rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
2.147 - in if rew2 then (t1 $ t2', asm2, lrd, true)
2.148 - else let val (t1', asm1, lrd, rew1) =
2.149 - rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
2.150 - in if rew1 then (t1' $ t2, asm1, lrd, true)
2.151 - else (t1 $ t2,[], lrd, false) end
2.152 - end)
2.153 -(* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
2.154 -and eval__true thy i asms bdv rls =
2.155 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
2.156 + in
2.157 + if rew2 then (t1 $ t2', asm2, lrd, true)
2.158 + else
2.159 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
2.160 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
2.161 + end)
2.162 +and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
2.163 if asms = [@{term True}] orelse asms = [] then ([], true)
2.164 - (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
2.165 - else if asms = [@{term False}] then ([], false) else
2.166 - let
2.167 - fun chk indets [] = (indets, true)(*return asms<>True until false*)
2.168 - | chk indets (a::asms) =
2.169 - (case rewrite__set_ thy (i + 1) false bdv rls a of
2.170 - NONE => (chk (indets @ [a]) asms)
2.171 - | SOME (t, a') =>
2.172 - if t = @{term True} then (chk (indets @ a') asms)
2.173 - else if t = @{term False} then ([], false)
2.174 - (*asm false .. thm not applied ^^^; continue until False vvv*)
2.175 - else chk (indets @ [t] @ a') asms);
2.176 - in chk [] asms end
2.177 -(* rewrite with a rule set, which must not be the empty Erls *)
2.178 -and rewrite__set_ _ _ __ Erls t =
2.179 + else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
2.180 + if asms = [@{term False}] then ([], false)
2.181 + else
2.182 + let
2.183 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
2.184 + | chk indets (a :: asms) =
2.185 + (case rewrite__set_ thy (i + 1) false bdv rls a of
2.186 + NONE => (chk (indets @ [a]) asms)
2.187 + | SOME (t, a') =>
2.188 + if t = @{term True} then (chk (indets @ a') asms)
2.189 + else if t = @{term False} then ([], false)
2.190 + (*asm false .. thm not applied ^^^; continue until False vvv*)
2.191 + else chk (indets @ [t] @ a') asms);
2.192 + in chk [] asms end
2.193 +and rewrite__set_ _ _ __ Erls t = (* rewrite with a rule set *)
2.194 error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
2.195 - (* rewrite with a 'reverse rule set' implemented by ML code *)
2.196 - | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
2.197 + | rewrite__set_ thy i _ _ (rrls as Rrls _) t = (* rewrite with a 'reverse rule set' *)
2.198 let
2.199 val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
2.200 val (t', asm, rew) = app_rev thy (i + 1) rrls t
2.201 in if rew then SOME (t', distinct asm) else NONE end
2.202 - (* rewrite with a rule set containing Thms or Calculations *)
2.203 - | rewrite__set_ thy i put_asm bdv rls ct =
2.204 + | rewrite__set_ thy i put_asm bdv rls ct = (* rule set containing Thms or Calculations *)
2.205 let
2.206 datatype switch = Appl | Noap;
2.207 - fun rew_once ruls asm ct Noap [] = (ct, asm) (* unify with version in rewtools.sml *)
2.208 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with rewtools.sml *)
2.209 | rew_once ruls asm ct Appl [] =
2.210 (case rls of Rls _ => rew_once ruls asm ct Noap ruls
2.211 - | Seq _ => (ct, asm))
2.212 - | rew_once ruls asm ct apno (rul::thms) =
2.213 + | Seq _ => (ct, asm)
2.214 + | rls => raise ERROR ("rew_once not appl. to \"" ^ rls2str rls ^ "\""))
2.215 + | rew_once ruls asm ct apno (rul :: thms) =
2.216 case rul of
2.217 Thm (thmid, thm) =>
2.218 (trace1 i (" try thm: " ^ thmid);
2.219 case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
2.220 ((#erls o rep_rls) rls) put_asm thm ct of
2.221 NONE => rew_once ruls asm ct apno thms
2.222 - | SOME (ct',asm') =>
2.223 + | SOME (ct', asm') =>
2.224 (trace1 i (" rewrites to: " ^ term2str ct');
2.225 rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
2.226 | Calc (cc as (op_, _)) =>
2.227 @@ -212,7 +164,7 @@
2.228 val ct = uminus_to_string ct
2.229 in case adhoc_thm thy cc ct of
2.230 NONE => rew_once ruls asm ct apno thms
2.231 - | SOME (thmid, thm') =>
2.232 + | SOME (_, thm') =>
2.233 let
2.234 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
2.235 ((#erls o rep_rls) rls) put_asm thm' ct;
2.236 @@ -226,7 +178,7 @@
2.237 val ct = uminus_to_string ct
2.238 in case adhoc_thm1_ thy cc ct of
2.239 NONE => (ct, asm)
2.240 - | SOME (thmid, thm') =>
2.241 + | SOME (_, thm') =>
2.242 let
2.243 val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
2.244 ((#erls o rep_rls) rls) put_asm thm' ct;
2.245 @@ -238,16 +190,15 @@
2.246 | Rls_ rls' =>
2.247 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
2.248 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
2.249 - | NONE => rew_once ruls asm ct apno thms);
2.250 + | NONE => rew_once ruls asm ct apno thms)
2.251 + | r => raise ERROR ("rew_once not appl. to \"" ^ rule2str r ^ "\"");
2.252 val ruls = (#rules o rep_rls) rls;
2.253 - val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
2.254 + val _ = trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
2.255 val (ct', asm') = rew_once ruls [] ct Noap ruls;
2.256 in if ct = ct' then NONE else SOME (ct', distinct asm') end
2.257 -
2.258 -(* apply an Rrls; if not applicable proceed with subterms *)
2.259 -and app_rev thy i rrls t =
2.260 +and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
2.261 let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
2.262 - fun chk_prepat thy erls [] t = true
2.263 + fun chk_prepat _ _ [] _ = true
2.264 | chk_prepat thy erls prepat t =
2.265 let
2.266 fun chk (pres, pat) =
2.267 @@ -256,24 +207,22 @@
2.268 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
2.269 in
2.270 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
2.271 - end) handle _ => false
2.272 - fun scan_ f [] = false (*scan_ NEVER called by []*)
2.273 + end) handle _ (*TODO Pattern.MATCH*) => false
2.274 + fun scan_ _ [] = false
2.275 | scan_ f (pp::pps) =
2.276 if f pp then true else scan_ f pps;
2.277 in scan_ chk prepat end;
2.278 (* apply the normal_form of a rev-set *)
2.279 fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
2.280 - if chk_prepat thy erls prepat t then normal_form t else NONE;
2.281 + if chk_prepat thy erls prepat t then normal_form t else NONE
2.282 + | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ rls2str r ^ "\"");
2.283 val opt = app_rev' thy rrls t
2.284 in
2.285 case opt of
2.286 SOME (t', asm) => (t', asm, true)
2.287 | NONE => app_sub thy i rrls t
2.288 end
2.289 -
2.290 -(* apply an Rrls to subterms *)
2.291 -and app_sub thy i rrls t =
2.292 - ((*tracing("### app_sub: subterm = "^(term2str t));*)
2.293 +and app_sub thy i rrls t = (* apply an Rrls to subterms *)
2.294 case t of
2.295 Const (s, T) => (Const(s, T), [], false)
2.296 | Free (s, T) => (Free(s, T), [], false)
2.297 @@ -291,39 +240,19 @@
2.298 in if rew1 then (t1' $ t2, asm1, true)
2.299 else (t1 $ t2, [], false)
2.300 end
2.301 - end);
2.302 + end;
2.303
2.304 -
2.305 -
2.306 -(*.rewriting without argument [] for rew_ord.*)
2.307 -(*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
2.308 +(* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
2.309 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
2.310
2.311 (* rewriting without internal argument [] *)
2.312 fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
2.313 fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
2.314
2.315 -fun subs'2subst thy (s:subs') =
2.316 - (((map (apfst (Thm.term_of o the o (parse thy))))
2.317 - o (map (apsnd (Thm.term_of o the o (parse thy))))) s):subst;
2.318 -
2.319 -(*.variants of rewrite.*)
2.320 -(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
2.321 - thus the argument put_asm IS NOT NECESSARY -- FIXME*)
2.322 -(* val (rew_ord,rls,put_asm,thm,ct)=
2.323 - (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
2.324 - *)
2.325 -fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
2.326 - (subst:(term * term) list) (thm:thm) (ct:term) =
2.327 - rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
2.328 -
2.329 -fun rewrite_set_inst_ (thy:theory)
2.330 - (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
2.331 - (*let
2.332 - val subst = subs'2subst thy subs';
2.333 - val subrls = instantiate_rls subs' rls
2.334 - in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
2.335 - (*end*);
2.336 +(* variants of rewrite; TODO del. put_asm *)
2.337 +fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
2.338 + rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
2.339 +fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
2.340
2.341 (* given a list of equalities (lhs = rhs) and a term,
2.342 replace all occurrences of lhs in the term with rhs;
2.343 @@ -333,7 +262,7 @@
2.344 fun rew_ (t', asm') [] _ = (t', asm')
2.345 | rew_ (t', asm') (rules as r::rs) t =
2.346 let
2.347 - val (t'', asm'', lrd, rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
2.348 + val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (Trueprop $ r) t
2.349 in
2.350 if rew
2.351 then rew_ (t'', asm' @ asm'') rules t''
2.352 @@ -343,96 +272,26 @@
2.353 in if t'' = e_term then NONE else SOME (t'', asm'')
2.354 end;
2.355
2.356 -(*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
2.357 +(* search ct for adjacent numerals and calculate them by operator isa_fn *)
2.358 fun calculate_ thy isa_fn ct =
2.359 let val ct = uminus_to_string ct
2.360 in case adhoc_thm thy isa_fn ct of
2.361 NONE => NONE
2.362 - | SOME (thmID, thm) =>
2.363 - (let val SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
2.364 - in SOME (rew,(thmID, thm)) end)
2.365 - handle _ => error ("calculate_: "^thmID^" does not rewrite")
2.366 + | SOME (thmID, thm) =>
2.367 + (let val rew = case rewrite_ thy dummy_ord e_rls false thm ct of
2.368 + SOME (rew, _) => rew
2.369 + | NONE => raise ERROR ""
2.370 + in SOME (rew, (thmID, thm)) end)
2.371 + handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
2.372 end;
2.373 -(*
2.374 -> val thy = InsSort.thy;
2.375 -> val op_ = "le"; (* < *)
2.376 -> val ct = (the o (parse thy))
2.377 - "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
2.378 -> calculate_ thy op_ ct;
2.379 - SOME
2.380 - ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
2.381 - "(#1 < #3) = True") : (cterm * thm) option *)
2.382
2.383 -fun get_rls_scr rls' = ((#scr o rep_rls o assoc_rls) rls')
2.384 - handle _ => error ("get_rls_scr: no script for " ^ rls');
2.385 -
2.386 -(*Thm.make_thm added to Pure/thm.ML*)
2.387 -fun mk_thm'' thy t =
2.388 - let val t' = case t of
2.389 - Const ("==>",_) $ _ $ _ => t
2.390 - | _ => Trueprop $ t
2.391 - in Thm.make_thm (Thm.global_cterm_of thy t') end;
2.392 +(* Thm.make_thm added to Pure/thm.ML *)
2.393 fun mk_thm thy str =
2.394 let val t = (Thm.term_of o the o (parse thy)) str
2.395 val t' = case t of
2.396 Const ("==>",_) $ _ $ _ => t
2.397 | _ => Trueprop $ t
2.398 in Thm.make_thm (Thm.global_cterm_of thy t') end;
2.399 -(*
2.400 - val str = "?r ^^^ 2 = ?r * ?r";
2.401 - val thm = realpow_twoI;
2.402 -
2.403 - val t1 = (#prop o rep_thm) (num_str thm);
2.404 - val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);
2.405 - t1 = t2;
2.406 -val it = true : bool ... !!!
2.407 - val th1 = (num_str thm);
2.408 - val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
2.409 - th1 = th2;
2.410 -ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
2.411 -
2.412 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2.413 - val str = "k ~= 0 ==> m * k / (n * k) = m / n";
2.414 - val thm = real_mult_div_cancel2;
2.415 -
2.416 - val t1 = (#prop o rep_thm) (num_str thm);
2.417 - val t2 = ((Thm.term_of o the o (parse thy)) str);
2.418 - t1 = t2;
2.419 -val it = false : bool ... Var .. Free
2.420 - val th1 = (num_str thm);
2.421 - val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
2.422 - th1 = th2;
2.423 -ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
2.424 -*)
2.425 -
2.426 -
2.427 -(*prints subgoal etc.
2.428 -((goal thy);(topthm()) o ) str; *)
2.429 -(*assume rejects scheme variables
2.430 - assume ((Thm.global_cterm_of thy) (Trueprop $
2.431 - (Thm.term_of o the o (parse thy)) str)); *)
2.432 -
2.433 -
2.434 -(* outcommented 18.11.xx, xx < 02 -------
2.435 -fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
2.436 - | rul2rul' (Calc op_) = Calc' op_;
2.437 -fun rul'2rul thy (Thm'(thmid, ct')) =
2.438 - Thm (thmid, mk_thm thy ct')
2.439 - | rul'2rul thy' (Calc' op_) = Calc op_;
2.440 -
2.441 -
2.442 -fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
2.443 - Rls'{preconds'= map string_of_cterm preconds,
2.444 - rew_ord' = fst rew_ord,
2.445 - rules' = map rul2rul' rules}:rlsdat';
2.446 -
2.447 -fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
2.448 - rules'=rules}:rlsdat') =
2.449 - let val thy = assoc_thy thy';
2.450 - in Rls{preconds = map (the o (parse thy)) preconds,
2.451 - rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
2.452 - rules = map (rul'2rul thy) rules}:rls end;
2.453 -------- *)
2.454
2.455 (* "metaview" as seen from programs and from user input (both are parsed like terms presently) *)
2.456 fun convert_metaview_to_thmid thy thmid =
2.457 @@ -446,31 +305,18 @@
2.458 | _ => thmid
2.459 in (Global_Theory.get_thm thy) thmid' end;
2.460
2.461 -(* FIXME: the other direction below is probably concerned with this fun:
2.462 -thmID_of_derivation_name' @{thm add.assoc} = "assoc" TODO: repair this fun *);
2.463 -
2.464 -fun convert thmid_to_metaview thmid =
2.465 - case thmid of
2.466 - "add.commute" => "add_commute"
2.467 - | "mult.commute" => "mult_commute"
2.468 - | "add.left_commute" => "add_left_commute"
2.469 - | "mult.left_commute" => "mult_left_commute"
2.470 - | "add.assoc" => "add_assoc"
2.471 - | "mult.assoc" => "mult_assoc"
2.472 - | _ => thmid;
2.473 -
2.474 -(*.get the theorem associated with the xstring-identifier;
2.475 +(* get the theorem associated with the xstring-identifier;
2.476 if the identifier starts with "sym_" then swap lhs = rhs around =
2.477 (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
2.478 identifiers starting with "#" come from Calc and
2.479 - get a hand-made theorem (containing numerals only).*)
2.480 -fun assoc_thm'' (thy : theory) (thmid : thmID) =
2.481 + get a hand-made theorem (containing numerals only) *)
2.482 +fun assoc_thm'' thy thmid =
2.483 case Symbol.explode thmid of
2.484 "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
2.485 | "s"::"y"::"m"::"_"::id => ((num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
2.486 | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
2.487 | _ => thmid |> convert_metaview_to_thmid thy |> num_str
2.488 -fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
2.489 +fun assoc_thm' thy (thmid, ct') =
2.490 (case Symbol.explode thmid of
2.491 "s"::"y"::"m"::"_"::id =>
2.492 if hd id = "#"
2.493 @@ -480,169 +326,17 @@
2.494 if hd id = "#"
2.495 then mk_thm thy ct'
2.496 else thmid |> convert_metaview_to_thmid thy |> num_str
2.497 - ) handle _ (*TODO: fin exn behind ERROR: Undefined fact: "add_commute"*) =>
2.498 + ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
2.499 error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")
2.500
2.501 -fun parse' (thy:theory') (ct:cterm') =
2.502 - case parse (assoc_thy thy) ct of
2.503 - NONE => NONE
2.504 - | SOME ct => SOME ((term2str (Thm.term_of ct)):cterm');
2.505 -
2.506 -
2.507 -(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
2.508 - thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
2.509 -fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') (put_asm:bool) (thm:thm') (ct:cterm') =
2.510 - let val thy = assoc_thy thy';
2.511 - in
2.512 - case rewrite_ thy ((the o assoc')(!rew_ord',rew_ord))(assoc_rls rls)
2.513 - put_asm ((assoc_thm' thy) thm) ((Thm.term_of o the o (parse thy)) ct) of
2.514 - NONE => NONE
2.515 - | SOME (t, ts) => SOME (term2str t, terms2str ts)
2.516 - end;
2.517 -
2.518 -(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
2.519 - thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
2.520 -fun rewrite_set (thy':theory') (put_asm:bool) (rls:rls') (ct:cterm') =
2.521 - let val thy = (assoc_thy thy');
2.522 - in
2.523 - case rewrite_set_ thy put_asm (assoc_rls rls) ((Thm.term_of o the o (parse thy)) ct) of
2.524 - NONE => NONE
2.525 - | SOME (t, ts) => SOME (term2str t, terms2str ts)
2.526 - end;
2.527 -
2.528 fun eval_listexpr_ thy srls t =
2.529 let val rew = rewrite_set_ thy false srls t;
2.530 in case rew of SOME (res,_) => res | NONE => t end;
2.531
2.532 -fun adhoc_thm' (thy:theory') op_ (ct:cterm') =
2.533 - case adhoc_thm (assoc_thy thy) op_
2.534 - ((uminus_to_string o Thm.term_of o the o
2.535 - (parse (assoc_thy thy))) ct) of
2.536 - NONE => NONE
2.537 - | SOME (thmid, thm) =>
2.538 - SOME ((thmid, string_of_thmI thm):thm');
2.539 -
2.540 -fun calculate (thy':theory') op_ (ct:cterm') =
2.541 - let val thy = (assoc_thy thy');
2.542 - in
2.543 - case calculate_ thy op_
2.544 - ((Thm.term_of o the o (parse thy)) ct) of
2.545 - NONE => NONE
2.546 - | SOME (ct,(thmID,thm)) =>
2.547 - SOME (term2str ct,
2.548 - (thmID, string_of_thmI thm):thm')
2.549 - end;
2.550 -
2.551 -(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
2.552 - thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
2.553 -fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
2.554 - (put_asm:bool) subs (thm:thm') (ct:cterm') =
2.555 - let
2.556 - val thy = assoc_thy thy';
2.557 - val thm = assoc_thm' thy thm; (*28.10.02*)
2.558 - (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
2.559 - in
2.560 - case rewrite_ thy
2.561 - ((the o assoc')(!rew_ord',rew_ord)) (assoc_rls rls)
2.562 - put_asm (*sub*)thm ((Thm.term_of o the o (parse thy)) ct) of
2.563 - NONE => NONE
2.564 - | SOME (ctm, ctms) =>
2.565 - SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)
2.566 - end;
2.567 -
2.568 -(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
2.569 - thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
2.570 -fun rewrite_set_inst (thy':theory') (put_asm:bool)
2.571 - subs' (rls:rls') (ct:cterm') =
2.572 - let
2.573 - val thy = assoc_thy thy';
2.574 - val rls = assoc_rls rls
2.575 - val subst = subs'2subst thy subs'
2.576 - in case rewrite_set_inst_ thy put_asm subst (*sub*)rls
2.577 - ((Thm.term_of o the o (parse thy)) ct) of
2.578 - NONE => NONE
2.579 - | SOME (t, ts) => SOME (term2str t, terms2str ts)
2.580 - end;
2.581 -
2.582 -
2.583 -(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
2.584 -fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true
2.585 -
2.586 - | eval_true' (thy':theory') (rls':rls') (t:term) =
2.587 -(* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';
2.588 - *)
2.589 - let val ct' = term2str t;
2.590 - in case rewrite_set thy' false rls' ct' of
2.591 - SOME ("HOL.True",_) => true
2.592 - | _ => false
2.593 - end;
2.594 fun eval_true_ _ _ (Const ("HOL.True",_)) = true
2.595 | eval_true_ (thy':theory') rls t =
2.596 case rewrite_set_ (assoc_thy thy') false rls t of
2.597 SOME (Const ("HOL.True",_),_) => true
2.598 | _ => false;
2.599
2.600 -(*
2.601 -val test_rls =
2.602 - Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
2.603 - rules = [Calc ("matches",eval_matches "")
2.604 - ],
2.605 - scr = Prog ((Thm.term_of o the o (parse thy))
2.606 - "empty_script")
2.607 - }:rls;
2.608 -
2.609 -
2.610 -
2.611 - rewrite_set_ (Thy_Info_get_theory "Isac") eval_rls false test_rls
2.612 - ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
2.613 - val xxx = (Thm.term_of o the o (parse thy))
2.614 - "matches (?a = ?b) (x = #0)";
2.615 - eval_matches """" xxx thy;
2.616 -SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
2.617 - Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
2.618 -
2.619 -
2.620 -
2.621 - rewrite_set_ (Thy_Info_get_theory "Isac") eval_rls false eval_rls
2.622 - ((the o (parse thy)) "contains_root (sqrt #0)");
2.623 -val it = SOME ("HOL.True",[]) : (cterm * cterm list) option
2.624 -
2.625 -*)
2.626 -
2.627 -
2.628 -(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
2.629 -datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
2.630 - introduced with quick-and-dirty code*)
2.631 -fun determine dts =
2.632 - let val false_indet =
2.633 - filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
2.634 - val ts = map (#2: det * term -> term) dts
2.635 - in if nil = false_indet then (TRUE, ts)
2.636 - else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
2.637 - false_indet
2.638 - then (INDET, ts)
2.639 - else (FALSE, ts) end;
2.640 -(* val dts = [(INDET,e_term), (FALSE,@{term False}),
2.641 - (INDET,e_term), (TRUE,@{term True})];
2.642 - determine dts;
2.643 -val it =
2.644 - (FALSE,
2.645 - [Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),
2.646 - Const ("HOL.True","bool")]) : det * term list*)
2.647 -
2.648 -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*)
2.649 -if cs = [@{term True}] orelse cs = [] then (TRUE, [])
2.650 - else if cs = [@{term False}] then (FALSE, cs)
2.651 - else
2.652 - let fun eval t =
2.653 - let val taopt = rewrite__set_ thy 1 false [] rls t
2.654 - in case taopt of
2.655 - SOME (t,_) =>
2.656 - if t = @{term True} then (TRUE, t)
2.657 - else if t = @{term False} then (FALSE, t)
2.658 - else (INDET, t)
2.659 - | NONE => (INDET, t) end
2.660 - in (determine o (map eval)) cs end;
2.661 -WN.16.5.0-------------------------------------------------------------*)
2.662 -
2.663 end
2.664 \ No newline at end of file
3.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Fri Feb 23 07:29:36 2018 +0100
3.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Sat Feb 24 11:14:56 2018 +0100
3.3 @@ -23,6 +23,7 @@
3.4 "----------- repair NO asms from rls RatEq_eliminate ----";
3.5 "----------- fun assoc_thm' -----------------------------";
3.6 "----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
3.7 +"----------- fun mk_thm ------------------------------------------------------------------------";
3.8 "--------------------------------------------------------";
3.9 "--------------------------------------------------------";
3.10 "--------------------------------------------------------";
3.11 @@ -587,3 +588,33 @@
3.12 val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
3.13 if (Envir.subst_term match r |> term2str) = "x * (y + z) = x * y + x * z" then ()
3.14 else error "Pattern.match CHANGED";
3.15 +
3.16 +"----------- fun mk_thm ------------------------------------------------------------------------";
3.17 +"----------- fun mk_thm ------------------------------------------------------------------------";
3.18 +"----------- fun mk_thm ------------------------------------------------------------------------";
3.19 +(*
3.20 + val str = "?r ^^^ 2 = ?r * ?r";
3.21 + val thm = realpow_twoI;
3.22 +
3.23 + val t1 = (#prop o rep_thm) (num_str thm);
3.24 + val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);
3.25 + t1 = t2;
3.26 +val it = true : bool ... !!!
3.27 + val th1 = (num_str thm);
3.28 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
3.29 + th1 = th2;
3.30 +ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
3.31 +
3.32 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3.33 + val str = "k ~= 0 ==> m * k / (n * k) = m / n";
3.34 + val thm = real_mult_div_cancel2;
3.35 +
3.36 + val t1 = (#prop o rep_thm) (num_str thm);
3.37 + val t2 = ((Thm.term_of o the o (parse thy)) str);
3.38 + t1 = t2;
3.39 +val it = false : bool ... Var .. Free
3.40 + val th1 = (num_str thm);
3.41 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
3.42 + th1 = th2;
3.43 +ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
3.44 +*)