1.1 --- a/src/sml/IsacKnowledge/PolyMinus.ML Mon Dec 10 09:01:54 2007 +0100
1.2 +++ b/src/sml/IsacKnowledge/PolyMinus.ML Mon Dec 10 11:09:26 2007 +0100
1.3 @@ -49,13 +49,16 @@
1.4
1.5 (** rulesets **)
1.6
1.7 +val erls_ordne_alphabetisch =
1.8 + append_rls "erls_ordne_alphabetisch" e_rls
1.9 + [Calc ("PolyMinus.kleiner", eval_kleiner ""),
1.10 + Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
1.11 + ];
1.12 +
1.13 val ordne_alphabetisch =
1.14 Rls{id = "ordne_alphabetisch", preconds = [],
1.15 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
1.16 - erls = append_rls "erls-ordne_alphabetisch" e_rls
1.17 - [Calc ("PolyMinus.kleiner", eval_kleiner ""),
1.18 - Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
1.19 - ],
1.20 + erls = erls_ordne_alphabetisch,
1.21 rules = [Thm ("tausche_plus",num_str tausche_plus),
1.22 (*"b kleiner a ==> (b + a) = (a + b)"*)
1.23 Thm ("tausche_plus_plus",num_str tausche_plus_plus),
2.1 --- a/src/sml/ROOT.ML Mon Dec 10 09:01:54 2007 +0100
2.2 +++ b/src/sml/ROOT.ML Mon Dec 10 11:09:26 2007 +0100
2.3 @@ -119,7 +119,9 @@
2.4 use"calculate-float.sml";
2.5 use"calculate.sml";
2.6 use"listg.sml";
2.7 + use"rewrite.sml";
2.8 use"scrtools.sml";
2.9 + use"term_G.sml";
2.10 cd "../..";
2.11 cd"smltest/ME";
2.12 use"ctree.sml";
3.1 --- a/src/sml/RTEST-root.sml Mon Dec 10 09:01:54 2007 +0100
3.2 +++ b/src/sml/RTEST-root.sml Mon Dec 10 11:09:26 2007 +0100
3.3 @@ -29,7 +29,9 @@
3.4 use"calculate-float.sml";
3.5 use"calculate.sml";
3.6 use"listg.sml";
3.7 + use"rewrite.sml";
3.8 use"scrtools.sml";
3.9 + use"term_G.sml";
3.10 cd "../..";
3.11 cd"smltest/ME";
3.12 use"ctree.sml";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/Scripts/rewrite.sml Mon Dec 10 11:09:26 2007 +0100
4.3 @@ -0,0 +1,704 @@
4.4 +(* isac's rewriter
4.5 + (c) Walther Neuper 2000
4.6 +
4.7 +use"Scripts/rewrite.sml";
4.8 +use"rewrite.sml";
4.9 +*)
4.10 +
4.11 +
4.12 +exception NO_REWRITE;
4.13 +exception STOP_REW_SUB; (*WN050820 quick and dirty*)
4.14 +
4.15 +(*17.6.00: rewrite by going down the term with rew_sub*)
4.16 +(* val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
4.17 + (thy, 1, [], rew_ord, erls, bool, thm, term);
4.18 + *)
4.19 +fun rewrite__ thy i bdv tless rls put_asm thm ct =
4.20 + ((*writeln ("@@@ r..te__ begin: t = "^(term2str ct));*)
4.21 + let
4.22 + val (t',asms,lrd,rew) =
4.23 + rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
4.24 + (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
4.25 + in if rew then Some (t', distinct asms)
4.26 + else None end)
4.27 +(* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct);
4.28 + val t1 = (#prop o rep_thm) thm;
4.29 + val t2 = norm t1;
4.30 + val t3 = inst_bdv bdv t2;
4.31 +
4.32 + val thm4 = read_instantiate [("bdv","x")] thm;
4.33 + val t4 = (norm o #prop o rep_thm) thm4;
4.34 + *)
4.35 +(* val (thy, i, bdv, tless, rls, put_asm, r, t) =
4.36 + (thy, i, bdv, tless, rls, put_asm,
4.37 + (((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
4.38 + *)
4.39 +and rew_sub thy i bdv tless rls put_asm lrd r t =
4.40 + (((*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
4.41 + let (* copy from Pure/thm.ML: fun rewritec *)
4.42 + val (lhs,rhs) = (dest_equals' o strip_trueprop
4.43 + o Logic.strip_imp_concl) r;
4.44 + val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (lhs,t);
4.45 + (*TODOtest: (-"-) handle _ => raise NO_REWRITE; 12.8.02 ???*)
4.46 + (*val _=writeln("@@@ rew_sub: Pattern.match (lhs,t) ");*)
4.47 + val r' = ren_inst (insts, r, lhs, t);
4.48 + val p' = map strip_trueprop (Logic.strip_imp_prems r');
4.49 + val t' = (snd o dest_equals' o strip_trueprop
4.50 + o Logic.strip_imp_concl) r';
4.51 + (*val _= writeln("@@@ rew_sub match: t'= "^(term2str t'));*)
4.52 + val _= if ! trace_rewrite andalso i < ! depth andalso p' <> []
4.53 + then writeln((idt"#"(i+1))^" eval asms: "^(term2str r')) else();
4.54 + val (t'',p'') =
4.55 + let val (simpl_p', nofalse) = eval__true thy (i+1) p' bdv rls
4.56 + in if nofalse
4.57 + then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
4.58 + then writeln((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
4.59 + " stored: "^(terms2str simpl_p'))
4.60 + else(); (t',simpl_p')) (* + uncond.rew. *)
4.61 + else
4.62 + (if ! trace_rewrite andalso i < ! depth
4.63 + then writeln((idt"#"(i+1))^" asms false: "^(terms2str p'))
4.64 + else(); raise STOP_REW_SUB)
4.65 + end
4.66 + in if perm lhs rhs andalso not (tless bdv (t',t))
4.67 + then (if ! trace_rewrite andalso i < ! depth
4.68 + then writeln((idt"#"i)^" not: \""^
4.69 + (Sign.string_of_term (sign_of thy) t)^"\" > \""^
4.70 + (Sign.string_of_term (sign_of thy) t')^"\"") else ();
4.71 + raise NO_REWRITE )
4.72 + else ((*writeln("##@ rew_sub: (t''= "^(term2str t'')^
4.73 + ", p'' ="^(terms2str p'')^", true)");*)
4.74 + (t'',p'',[],true))
4.75 + end) handle STOP_REW_SUB => (t,[],[],false)
4.76 + ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests*) =>
4.77 + ((*writeln ("@@@ rew_sub gosub: t = "^(term2str t));*)
4.78 + case t of
4.79 + Const(s,T) => (Const(s,T),[],lrd,false)
4.80 + | Free(s,T) => (Free(s,T),[],lrd,false)
4.81 + | Var(n,T) => (Var(n,T),[],lrd,false)
4.82 + | Bound i => (Bound i,[],lrd,false)
4.83 + | Abs(s,T,body) =>
4.84 + let val (t', asms, lrd, rew) =
4.85 + rew_sub thy i bdv tless rls put_asm (lrd@[D]) r body
4.86 + in (Abs(s,T,t'), asms, [], rew) end
4.87 + | t1 $ t2 =>
4.88 + let val (t2', asm2, lrd, rew2) =
4.89 + rew_sub thy i bdv tless rls put_asm (lrd@[R]) r t2
4.90 + in if rew2 then (t1 $ t2', asm2, lrd, true)
4.91 + else let val (t1', asm1, lrd, rew1) =
4.92 + rew_sub thy i bdv tless rls put_asm (lrd@[L]) r t1
4.93 + in if rew1 then (t1' $ t2, asm1, lrd, true)
4.94 + else (t1 $ t2,[], lrd, false) end
4.95 + end)
4.96 +(* val (cprems',rls)=([pre],prls);
4.97 + rewrite__set_ thy i false rls pre;
4.98 + *)
4.99 +and eval__true thy i asms bdv rls =
4.100 +(* val (thy, i, asms, bdv, rls) = (thy, (i+1), p', bdv, rls);
4.101 + *)
4.102 + if asms = [HOLogic.true_const] orelse asms = []
4.103 + then ([], true) else if asms = [HOLogic.false_const] then ([], false)
4.104 + else let
4.105 + fun chk indets [] = (indets, true)(*return asms<>True until false*)
4.106 + | chk indets (a::asms) =
4.107 +(* val (indets, (a::asms)) = ([], asms);
4.108 + *)
4.109 + (case rewrite__set_ thy (i+1) false bdv rls a of
4.110 + None => (chk (indets @ [a]) asms)
4.111 + | Some (t, a') =>
4.112 + if t = HOLogic.true_const
4.113 + then (chk (indets @ a') asms)
4.114 + else if t = HOLogic.false_const then ([], false)
4.115 + (*asm false .. thm not applied ^^^; continue until False vvv*)
4.116 + else (chk (indets @ [t] @ a') asms));
4.117 + in chk [] asms end
4.118 +
4.119 +and rewrite__set_ _ _ __ Erls t =
4.120 + raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
4.121 + | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
4.122 + let val _= if ! trace_rewrite andalso i < ! depth
4.123 + then writeln ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
4.124 + (term2str t)) else ()
4.125 + val (t', asm, rew) = app_rev thy (i+1) rrls t
4.126 + in if rew then Some (t', distinct asm)
4.127 + else None end
4.128 + | rewrite__set_ thy i put_asm bdv rls ct =
4.129 +(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
4.130 + *)
4.131 + let
4.132 + datatype switch = Appl | Noap;
4.133 + fun rew_once ruls asm ct Noap [] = (ct,asm)
4.134 + | rew_once ruls asm ct Appl [] =
4.135 + (case rls of Rls _ => rew_once ruls asm ct Noap ruls
4.136 + | Seq _ => (ct,asm))
4.137 + | rew_once ruls asm ct apno (rul::thms) =
4.138 +(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
4.139 + val Thm (thmid, thm) = rul;
4.140 + *)
4.141 + case rul of
4.142 + Thm (thmid, thm) =>
4.143 + (if !trace_rewrite andalso i < ! depth
4.144 + then writeln((idt"#"(i+1))^" try thm: "^thmid) else ();
4.145 + case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
4.146 + ((#erls o rep_rls) rls) put_asm thm ct of
4.147 + None => rew_once ruls asm ct apno thms
4.148 + | Some (ct',asm') => (if ! trace_rewrite andalso i < ! depth
4.149 + then writeln((idt"="(i+1))^" rewrites to: "^
4.150 + (Sign.string_of_term (sign_of thy) ct')) else ();
4.151 + rew_once ruls (asm union asm') ct' Appl (rul::thms)))
4.152 + | Calc (cc as (op_,_)) =>
4.153 + (let val _= if !trace_rewrite andalso i < ! depth then
4.154 + writeln((idt"#"(i+1))^" try calc: "^op_^"'") else ();
4.155 + val ct = app_num_tr'2 ct
4.156 + in case get_calculation_ thy cc ct of
4.157 + None => rew_once ruls asm ct apno thms
4.158 + | Some (thmid, thm') =>
4.159 + let
4.160 + val pairopt =
4.161 + rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
4.162 + ((#erls o rep_rls) rls) put_asm thm' ct;
4.163 + val _ = if pairopt <> None then ()
4.164 + else raise error("rewrite_set_, rewrite_ \""^
4.165 + (string_of_thmI thm')^"\" "^(term2str ct)^" = None")
4.166 + val _ = if ! trace_rewrite andalso i < ! depth
4.167 + then writeln((idt"="(i+1))^" calc. to: "^
4.168 + (term2str ((fst o the) pairopt)))
4.169 + else()
4.170 + in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
4.171 + end)
4.172 + | Rls_ rls' =>
4.173 + (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
4.174 + Some (t',asm') => rew_once ruls (asm union asm') t' Appl thms
4.175 + | None => rew_once ruls asm ct apno thms);
4.176 +
4.177 + val ruls = (#rules o rep_rls) rls;
4.178 + val _= if ! trace_rewrite andalso i < ! depth
4.179 + then writeln ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
4.180 + (term2str ct)) else ()
4.181 + val (ct',asm') = rew_once ruls [] ct Noap ruls;
4.182 + in if ct = ct' then None else Some (ct', distinct asm') end
4.183 +
4.184 +and app_rev thy i rrls t =
4.185 + let (*.check a (precond, pattern) of a rev-set; stops with 1st true.*)
4.186 + fun chk_prepat thy erls [] t = true
4.187 + | chk_prepat thy erls prepat t =
4.188 + let fun chk (pres, pat) =
4.189 + let val (_, sbst) =
4.190 + (Pattern.match
4.191 + (Sign.tsig_of (sign_of(assoc_thy "Isac.thy")))
4.192 + (pat, t))
4.193 + handle _ => ([], [])
4.194 + val subst = map mk_subs sbst;
4.195 + (*val _=writeln("### chk_prepat: subst = "^(subst2str subst));*)
4.196 + in if subst = nil then false
4.197 + else ((*writeln("### chk_prepat: (pre,pat) ("^
4.198 + (term2str pre)^", "^(term2str pat)^" = "^(bool2str (
4.199 + eval_true thy [subst_atomic subst pre] (assoc_rls erls))));*)
4.200 + snd (eval__true thy (i+1)
4.201 + (map (subst_atomic subst) pres)
4.202 + [] erls))
4.203 + end
4.204 + fun scan_ f [] = false (*scan_ NEVER called by []*)
4.205 + | scan_ f (pp::pps) = if f pp then true
4.206 + else scan_ f pps;
4.207 + in scan_ chk prepat end;
4.208 +
4.209 + (*.apply the normal_form of a rev-set.*)
4.210 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
4.211 + if chk_prepat thy erls prepat t
4.212 + then ((*writeln("### app_rev': t = "^(term2str t));*)
4.213 + normal_form t)
4.214 + else None;
4.215 +
4.216 + val opt = app_rev' thy rrls t
4.217 + in case opt of
4.218 + Some (t', asm) => (t', asm, true)
4.219 + | None => app_sub thy i rrls t
4.220 + end
4.221 +and app_sub thy i rrls t =
4.222 + ((*writeln("### app_sub: subterm = "^(term2str t));*)
4.223 + case t of
4.224 + Const (s, T) => (Const(s, T), [], false)
4.225 + | Free (s, T) => (Free(s, T), [], false)
4.226 + | Var (n, T) => (Var(n, T), [], false)
4.227 + | Bound i => (Bound i, [], false)
4.228 + | Abs (s, T, body) =>
4.229 + let val (t', asm, rew) = app_rev thy i rrls body
4.230 + in (Abs(s, T, t'), asm, rew) end
4.231 + | t1 $ t2 =>
4.232 + let val (t2', asm2, rew2) = app_rev thy i rrls t2
4.233 + in if rew2 then (t1 $ t2', asm2, true)
4.234 + else let val (t1', asm1, rew1) = app_rev thy i rrls t1
4.235 + in if rew1 then (t1' $ t2, asm1, true)
4.236 + else (t1 $ t2, [], false) end
4.237 + end);
4.238 +
4.239 +
4.240 +
4.241 +(*.rewriting without argument [] for rew_ord.*)
4.242 +(*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
4.243 +fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
4.244 +
4.245 +
4.246 +(*.rewriting without internal argument [] for rew_ord.*)
4.247 +(* val (thy, rew_ord, erls, bool, thm, term) =
4.248 + (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
4.249 + *)
4.250 +fun rewrite_ thy rew_ord erls bool thm term =
4.251 + rewrite__ thy 1 [] rew_ord erls bool thm term;
4.252 +fun rewrite_set_ thy bool rls term =
4.253 +(* val (thy, bool, rls, term) = (thy, false, srls, t);
4.254 + *)
4.255 + rewrite__set_ thy 1 bool [] rls term;
4.256 +
4.257 +
4.258 +fun subs'2subst thy (s:subs') =
4.259 + (((map (apfst (term_of o the o (parse thy))))
4.260 + o (map (apsnd (term_of o the o (parse thy))))) s):subst;
4.261 +
4.262 +(*.variants of rewrite.*)
4.263 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,
4.264 + thus the argument put_asm IS NOT NECESSARY -- FIXME*)
4.265 +(* val (rew_ord,rls,put_asm,thm,ct)=
4.266 + (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);
4.267 + *)
4.268 +fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool)
4.269 + (subst:(term * term) list) (thm:thm) (ct:term) =
4.270 + rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
4.271 +
4.272 +fun rewrite_set_inst_ (thy:theory)
4.273 + (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =
4.274 + (*let
4.275 + val subst = subs'2subst thy subs';
4.276 + val subrls = instantiate_rls subs' rls
4.277 + in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
4.278 + (*end*);
4.279 +
4.280 +
4.281 +(*.rewrite using a list of terms.*)
4.282 +fun rewrite_terms_ thy ord erls subte t =
4.283 + let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
4.284 + term_detail2str (hd subte)^
4.285 + "### rewrite_terms_ t= '"^term2str t^"' ..."^
4.286 + term_detail2str t);*)
4.287 + fun rew_ (t', asm') [] _ = (t', asm')
4.288 + | rew_ (t', asm') (rules as r::rs) t =
4.289 + let val (t'', asm'', lrd, rew) =
4.290 + rew_sub thy 1 [] ord erls false [] r t
4.291 + in if rew
4.292 + then rew_ (t'', asm' @ asm'') rules t''
4.293 + else rew_ (t', asm') rs t'
4.294 + end
4.295 + val (t'', asm'') = rew_ (e_term, []) subte t
4.296 + in if t'' = e_term
4.297 + then None else Some (t'', asm'')
4.298 + end;
4.299 +
4.300 +
4.301 +(*. search ct for adjacent numerals and calculate them by operator isa_fn .*)
4.302 +fun calculate_ thy isa_fn ct =
4.303 + let val ct = app_num_tr'2 ct
4.304 + in case get_calculation_ thy isa_fn ct of
4.305 + None => None
4.306 + | Some (thmID, thm) =>
4.307 + (let val Some (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct
4.308 + in Some (rew,(thmID, thm)) end)
4.309 + handle _ => error ("calculate_: "^thmID^" does not rewrite")
4.310 + end;
4.311 +(*
4.312 +> val thy = InsSort.thy;
4.313 +> val op_ = "le"; (* < *)
4.314 +> val ct = (the o (parse thy))
4.315 + "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";
4.316 +> calculate_ thy op_ ct;
4.317 + Some
4.318 + ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",
4.319 + "(#1 < #3) = True") : (cterm * thm) option *)
4.320 +
4.321 +
4.322 +(* for test-printouts:
4.323 +val _ = writeln("in rew_sub : "^( Sign.string_of_term (sign_of thy) t))
4.324 +val _ = writeln("in eval_true: prems= "^(commas (map (Sign.string_of_term (sign_of thy)) prems')))
4.325 +*)
4.326 +
4.327 +
4.328 +
4.329 +
4.330 +
4.331 +
4.332 +fun get_rls_scr rs' = ((#scr o rep_rls o #2 o the o assoc') (!ruleset',rs'))
4.333 + handle _ => raise error ("get_rls_scr: no script for "^rs');
4.334 +
4.335 +
4.336 +(*make_thm added to Pure/thm.ML*)
4.337 +fun mk_thm thy str =
4.338 + let val t = (term_of o the o (parse thy)) str
4.339 + val t' = case t of
4.340 + Const ("==>",_) $ _ $ _ => t
4.341 + | _ => Trueprop $ t
4.342 + in make_thm (cterm_of (sign_of thy) t') end;
4.343 +(*
4.344 + val str = "?r ^^^ 2 = ?r * ?r";
4.345 + val thm = realpow_twoI;
4.346 +
4.347 + val t1 = (#prop o rep_thm) (num_str thm);
4.348 + val t2 = Trueprop $ ((term_of o the o (parse thy)) str);
4.349 + t1 = t2;
4.350 +val it = true : bool ... !!!
4.351 + val th1 = (num_str thm);
4.352 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
4.353 + th1 = th2;
4.354 +ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
4.355 +
4.356 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
4.357 + val str = "k ~= 0 ==> m * k / (n * k) = m / n";
4.358 + val thm = real_mult_div_cancel2;
4.359 +
4.360 + val t1 = (#prop o rep_thm) (num_str thm);
4.361 + val t2 = ((term_of o the o (parse thy)) str);
4.362 + t1 = t2;
4.363 +val it = false : bool ... Var .. Free
4.364 + val th1 = (num_str thm);
4.365 + val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;
4.366 + th1 = th2;
4.367 +ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!
4.368 +*)
4.369 +
4.370 +
4.371 +(*prints subgoal etc.
4.372 +((goal thy);(topthm()) o ) str; *)
4.373 +(*assume rejects scheme variables
4.374 + assume (cterm_of (sign_of thy) (Trueprop $
4.375 + (term_of o the o (parse thy)) str)); *)
4.376 +
4.377 +
4.378 +(* outcommented 18.11.xx, xx < 02 -------
4.379 +fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)
4.380 + | rul2rul' (Calc op_) = Calc' op_;
4.381 +fun rul'2rul thy (Thm'(thmid, ct')) =
4.382 + Thm (thmid, mk_thm thy ct')
4.383 + | rul'2rul thy' (Calc' op_) = Calc op_;
4.384 +
4.385 +
4.386 +fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =
4.387 + Rls'{preconds'= map string_of_cterm preconds,
4.388 + rew_ord' = fst rew_ord,
4.389 + rules' = map rul2rul' rules}:rlsdat';
4.390 +
4.391 +fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,
4.392 + rules'=rules}:rlsdat') =
4.393 + let val thy = the (assoc' (theory',thy'))
4.394 + in Rls{preconds = map (the o (parse thy)) preconds,
4.395 + rew_ord = (rew_ord, the (assoc'(rew_ord',rew_ord))),
4.396 + rules = map (rul'2rul thy) rules}:rls end;
4.397 +------- *)
4.398 +
4.399 +(*.get the theorem associated with the xstring-identifier;
4.400 + if the identifier starts with "sym_" then swap lhs = rhs around =
4.401 + (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);
4.402 + identifiers starting with "#" come from Calc and
4.403 + get a hand-made theorem (containing numerals only).*)
4.404 +fun assoc_thm' (thy:theory) ((thmid, ct'):thm') =
4.405 + (case explode thmid of
4.406 + "s"::"y"::"m"::"_"::id =>
4.407 + if hd id = "#"
4.408 + then mk_thm thy ct'
4.409 + else ((num_str o (get_thm thy)) (implode id)) RS sym
4.410 + | id =>
4.411 + if hd id = "#"
4.412 + then mk_thm thy ct'
4.413 + else (num_str o (get_thm thy)) thmid
4.414 + ) handle _ =>
4.415 + raise error ("assoc_thm': '"^thmid^"' not in '"^
4.416 + (theory2domID thy)^"' (and parents)");
4.417 +(*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
4.418 +val it = "6 = 2 * 3" : thm
4.419 +
4.420 +> assoc_thm' Isac.thy ("real_add_zero_left","");
4.421 +val it = "0 + ?z = ?z" : thm
4.422 +
4.423 +> assoc_thm' Isac.thy ("sym_real_add_zero_left","");
4.424 +val it = "?t = 0 + ?t" [.] : thm
4.425 +
4.426 +> assoc_thm' HOL.thy ("sym_real_add_zero_left","");
4.427 +*** Unknown theorem(s) "real_add_zero_left"
4.428 +*** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
4.429 + uncaught exception ERROR*)
4.430 +
4.431 +
4.432 +fun parse' (thy:theory') (ct:cterm') =
4.433 + case parse ((the o assoc')(!theory',thy)) ct of
4.434 + None => None
4.435 + | Some ct => Some ((string_of_cterm ct):cterm');
4.436 +
4.437 +
4.438 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
4.439 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
4.440 +fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls')
4.441 + (put_asm:bool) (thm:thm') (ct:cterm') =
4.442 +(* val (rew_ord, rls, thm, ct) = (rew_ord', id_rls rls', thm', f);
4.443 + *)
4.444 + let val thy = (the o assoc')(!theory',thy');
4.445 + in
4.446 + case rewrite_ thy
4.447 + ((the o assoc')(!rew_ord',rew_ord))((#2 o the o assoc')(!ruleset',rls))
4.448 + put_asm ((assoc_thm' thy) thm)
4.449 + ((term_of o the o (parse thy)) ct) of
4.450 + None => None
4.451 + | Some (t, ts) => Some (Sign.string_of_term (sign_of thy) t,
4.452 + map (Sign.string_of_term (sign_of thy)) ts)
4.453 + end;
4.454 +
4.455 +(*
4.456 +val thy = "RatArith.thy";
4.457 +val rew_ord = "dummy_ord";
4.458 +> val rls = "eval_rls";
4.459 +val put_asm = true;
4.460 +val thm = ("square_equation_left","");
4.461 +val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#-3+x)";
4.462 +
4.463 +val Zthy = ((the o assoc')(!theory',thy));
4.464 +val Zrew_ord = ((the o assoc')(!rew_ord',rew_ord));
4.465 +val Zrls = ((the o assoc')(!ruleset',rls));
4.466 +val Zput_asm = put_asm;
4.467 +val Zthm = ((the o (assoc'_thm' thy)) thm);
4.468 +val Zct = ((the o (parse ((the o assoc')(!theory',thy)))) ct);
4.469 +
4.470 +rewrite_ Zthy Zrew_ord Zrls Zput_asm Zthm Zct;
4.471 +
4.472 + use"Isa99/interface_ME_ISA.sml";
4.473 +*)
4.474 +
4.475 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
4.476 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
4.477 +fun rewrite_set (thy':theory') (put_asm:bool)
4.478 + (rls:rls') (ct:cterm') =
4.479 + let val thy = (the o assoc')(!theory',thy');
4.480 + in
4.481 + case rewrite_set_ thy put_asm ((#2 o the o assoc')(!ruleset',rls))
4.482 + ((term_of o the o (parse thy)) ct) of
4.483 + None => None
4.484 + | Some (t, ts) => Some (Sign.string_of_term (sign_of thy) t,
4.485 + map (Sign.string_of_term (sign_of thy)) ts)
4.486 + end;
4.487 +
4.488 +(*evaluate list-expressions
4.489 + should work on term, and stand in Isa99/rewrite-parse.sml,
4.490 + but there list_rls <- eval_binop is not yet defined*)
4.491 +(*fun eval_listexpr' ct =
4.492 + let val rew = rewrite_set "ListG.thy" false "list_rls" ct;
4.493 + in case rew of
4.494 + Some (res,_) => res
4.495 + | None => ct end;-----------------30.9.02---*)
4.496 +fun eval_listexpr_ thy srls t =
4.497 +(* val (thy, srls, t) =
4.498 + ((assoc_thy th), sr, (subst_atomic (upd_env_opt E (a,v)) t));
4.499 + *)
4.500 + let val rew = rewrite_set_ thy false srls t;
4.501 + in case rew of
4.502 + Some (res,_) => res
4.503 + | None => t end;
4.504 +
4.505 +
4.506 +fun get_calculation' (thy:theory') op_ (ct:cterm') =
4.507 + case get_calculation_ ((the o assoc')(!theory',thy)) op_
4.508 + ((app_num_tr'2 o term_of o the o
4.509 + (parse ((the o assoc')(!theory',thy)))) ct) of
4.510 + None => None
4.511 + | Some (thmid, thm) =>
4.512 + Some ((thmid, string_of_thmI thm):thm');
4.513 +
4.514 +fun calculate (thy':theory') op_ (ct:cterm') =
4.515 + let val thy = (the o assoc')(!theory',thy');
4.516 + in
4.517 + case calculate_ thy op_
4.518 + ((term_of o the o (parse thy)) ct) of
4.519 + None => None
4.520 + | Some (ct,(thmID,thm)) =>
4.521 + Some (Sign.string_of_term (sign_of thy) ct,
4.522 + (thmID, string_of_thmI thm):thm')
4.523 + end;
4.524 +(*
4.525 +fun instantiate'' thy' subs ((thmid,ct'):thm') =
4.526 + let val thmid_ = implode ("#"::(explode thmid)) (*see type thm'*)
4.527 + in (thmid_, (string_of_thmI o (read_instantiate subs))
4.528 + ((the o (assoc_thm' thy')) (thmid_,ct'))):thm' end;
4.529 +
4.530 +fun instantiate_rls' thy' subs (rls:rls') =
4.531 + rls2rls' (instantiate_rls subs ((the o (assoc_rls thy')) rls)):rlsdat';
4.532 +
4.533 +... problem with these functions:
4.534 +> val thm = mk_thm thy "(bdv + a = b) = (bdv = b - a)";
4.535 +val thm = "(bdv + a = b) = (bdv = b - a)" : thm
4.536 +> show_types:=true; thm;
4.537 +val it = "((bdv::'a) + (a::'a) = (b::'a)) = (bdv = b - a)" : thm
4.538 +... and this doesn't match because of too general typing (?!)
4.539 + and read_insitantiate doesn't instantiate the types (?!)
4.540 +=== solutions:
4.541 +(1) hard-coded type-instantiation ("'a", "RatArith.rat")
4.542 +(2) instantiate', instantiate ... no help by isabelle-users@ !!!
4.543 +=== conclusion:
4.544 + rewrite_inst, rewrite_set_inst circumvent the problem,
4.545 + according functions out-commented with 'instantiate''
4.546 +*)
4.547 +
4.548 +(* instantiate''
4.549 +fun instantiate'' thy' subs ((thmid,ct'):thm') =
4.550 + let
4.551 + val thmid_ = implode ("#"::(explode thmid)); (*see type thm'*)
4.552 + val thy = (the o assoc')(!theory',thy');
4.553 + val typs = map (#T o rep_cterm o the o (parse thy))
4.554 + ((snd o split_list) subs);
4.555 + val ctyps = map
4.556 + ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o (parse thy))
4.557 + ((snd o split_list) subs);
4.558 +
4.559 +> val thy' = "RatArith.thy";
4.560 +> val subs = [("bdv","x::rat"),("zzz","z::nat")];
4.561 +> (the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
4.562 +> (#T o rep_cterm o the o (parse ((the o assoc')(!theory',thy'))));
4.563 +
4.564 +> val ctyp = ((ctyp_of (sign_of thy)) o #T o rep_cterm o the o
4.565 + (parse ((the o assoc')(!theory',thy')))) "x::rat";
4.566 +> val bdv = (the o (parse thy)) "bdv";
4.567 +> val x = (the o (parse thy)) "x";
4.568 +> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
4.569 + handle e => print_exn e;
4.570 +uncaught exception THM
4.571 + raised at: thm.ML:1085.18-1085.69
4.572 + thm.ML:1092.34
4.573 + goals.ML:536.61
4.574 +
4.575 +> val bdv = (the o (parse thy)) "bdv::nat";
4.576 +> val x = (the o (parse thy)) "x::nat";
4.577 +> (instantiate ([(("'a",0),ctyp)],[(bdv,x)]) isolate_bdv_add)
4.578 + handle e => print_exn e;
4.579 +uncaught exception THM
4.580 + raised at: thm.ML:1085.18-1085.69
4.581 + thm.ML:1092.34
4.582 + goals.ML:536.61
4.583 +
4.584 +> (instantiate' [Some ctyp] [] isolate_bdv_add)
4.585 + handle e => print_exn e;
4.586 +uncaught exception TYPE
4.587 + raised at: drule.ML:613.13-615.44
4.588 + goals.ML:536.61
4.589 +
4.590 +> val repct = (rep_cterm o the o (parse ((the o assoc')(!theory',thy')))) "x::rat";
4.591 +*)
4.592 +
4.593 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
4.594 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
4.595 +fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls')
4.596 + (put_asm:bool) subs (thm:thm') (ct:cterm') =
4.597 + let
4.598 + val thy = (the o assoc')(!theory',thy');
4.599 + val thm = assoc_thm' thy thm; (*28.10.02*)
4.600 + (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)
4.601 + in
4.602 + case rewrite_ thy
4.603 + ((the o assoc')(!rew_ord',rew_ord)) ((#2 o the o assoc')(!ruleset',rls))
4.604 + put_asm (*sub*)thm ((term_of o the o (parse thy)) ct) of
4.605 + None => None
4.606 + | Some (ctm, ctms) =>
4.607 + Some ((Sign.string_of_term (sign_of thy) ctm):cterm',
4.608 + (map (Sign.string_of_term (sign_of thy)) ctms):cterm' list)
4.609 + end;
4.610 +
4.611 +(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst
4.612 + thus the argument put_asm IS NOT NECESSARY -- FIXME ~~~~~*)
4.613 +fun rewrite_set_inst (thy':theory') (put_asm:bool)
4.614 + subs' (rls:rls') (ct:cterm') =
4.615 + let
4.616 + val thy = (the o assoc')(!theory',thy');
4.617 + val rls = assoc_rls rls
4.618 + val subst = subs'2subst thy subs'
4.619 + (*val subrls = instantiate_rls subs ((the o assoc')(!ruleset',rls))*)
4.620 + in
4.621 + case rewrite_set_inst_ thy put_asm subst (*sub*)rls
4.622 + ((term_of o the o (parse thy)) ct) of
4.623 + None => None
4.624 + | Some (t, ts) => Some (Sign.string_of_term (sign_of thy) t,
4.625 + map (Sign.string_of_term (sign_of thy)) ts)
4.626 + end;
4.627 +
4.628 +
4.629 +(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)
4.630 +fun eval_true' (thy':theory') (rls':rls') (Const ("True",_)) = true
4.631 +
4.632 + | eval_true' (thy':theory') (rls':rls') (t:term) =
4.633 +(* val thy'="Isac.thy"; val rls'="eval_rls"; val t=hd pres';
4.634 + *)
4.635 + let val ct' = Sign.string_of_term (sign_of (assoc_thy thy')) t;
4.636 + in case rewrite_set thy' false rls' ct' of
4.637 + Some ("True",_) => true
4.638 + | _ => false
4.639 + end;
4.640 +fun eval_true_ _ _ (Const ("True",_)) = true
4.641 + | eval_true_ (thy':theory') rls t =
4.642 + case rewrite_set_ (assoc_thy thy') false rls t of
4.643 + Some (Const ("True",_),_) => true
4.644 + | _ => false;
4.645 +
4.646 +(*
4.647 +val test_rls =
4.648 + Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right),
4.649 + rules = [Calc ("matches",eval_matches "")
4.650 + ],
4.651 + scr = Script ((term_of o the o (parse thy))
4.652 + "empty_script")
4.653 + }:rls;
4.654 +
4.655 +
4.656 +
4.657 + rewrite_set_ Isac.thy eval_rls false test_rls
4.658 + ((the o (parse thy)) "matches (?a = ?b) (x = #0)");
4.659 + val xxx = (term_of o the o (parse thy))
4.660 + "matches (?a = ?b) (x = #0)";
4.661 + eval_matches """" xxx thy;
4.662 +Some ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",
4.663 + Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))
4.664 +
4.665 +
4.666 +
4.667 + rewrite_set_ Isac.thy eval_rls false eval_rls
4.668 + ((the o (parse thy)) "contains_root (sqrt #0)");
4.669 +val it = Some ("True",[]) : (cterm * cterm list) option
4.670 +
4.671 +*)
4.672 +
4.673 +
4.674 +(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise
4.675 +datatype det = TRUE | FALSE | INDET;(*FIXXME.WN:16.5.03
4.676 + introduced with quick-and-dirty code*)
4.677 +fun determine dts =
4.678 + let val false_indet =
4.679 + filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts
4.680 + val ts = map (#2: det * term -> term) dts
4.681 + in if nil = false_indet then (TRUE, ts)
4.682 + else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))
4.683 + false_indet
4.684 + then (INDET, ts)
4.685 + else (FALSE, ts) end;
4.686 +(* val dts = [(INDET,e_term), (FALSE,HOLogic.false_const),
4.687 + (INDET,e_term), (TRUE,HOLogic.true_const)];
4.688 + determine dts;
4.689 +val it =
4.690 + (FALSE,
4.691 + [Const ("empty","'a"),Const ("False","bool"),Const ("empty","'a"),
4.692 + Const ("True","bool")]) : det * term list*)
4.693 +
4.694 +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*)
4.695 +if cs = [HOLogic.true_const] orelse cs = [] then (TRUE, [])
4.696 + else if cs = [HOLogic.false_const] then (FALSE, cs)
4.697 + else
4.698 + let fun eval t =
4.699 + let val taopt = rewrite__set_ thy 1 false [] rls t
4.700 + in case taopt of
4.701 + Some (t,_) =>
4.702 + if t = HOLogic.true_const then (TRUE, t)
4.703 + else if t = HOLogic.false_const then (FALSE, t)
4.704 + else (INDET, t)
4.705 + | None => (INDET, t) end
4.706 + in (determine o (map eval)) cs end;
4.707 +WN.16.5.0-------------------------------------------------------------*)
4.708 \ No newline at end of file
5.1 --- a/src/smltest/IsacKnowledge/polyminus.sml Mon Dec 10 09:01:54 2007 +0100
5.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml Mon Dec 10 11:09:26 2007 +0100
5.3 @@ -87,6 +87,25 @@
5.4
5.5 val t = str2term "a + c + d + b";
5.6 val Some (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
5.7 +"a + c + b + d";(*?!?...*)
5.8 +
5.9 +"----- rewrite seems not to go into subterms";
5.10 +val od = ord_make_polynomial true Poly.thy;(*/////////not necessary*)
5.11 +val erls = erls_ordne_alphabetisch;
5.12 +val t = str2term "a + c + b + d";
5.13 +val Some (t,_) = rewrite_ thy od erls false tausche_plus_plus t; term2str t;
5.14 +
5.15 +"----- here we see rew_sub going into subterm with cond.rew....";
5.16 +val t = str2term "b + a + c + d";
5.17 +val Some (t,_) = rewrite_ thy od erls false tausche_plus t; term2str t;
5.18 +
5.19 +"----- here we see rew_sub going into subterm with ord.rew....";
5.20 +val od = ord_make_polynomial false Poly.thy;
5.21 +val t = str2term "b + a + c + d";
5.22 +val Some (t,_) = rewrite_ thy od erls false real_add_commute t; term2str t;
5.23 +val Some (t,_) = rewrite_ thy od erls false real_add_commute t; term2str t;
5.24 +(*@@@ rew_sub gosub: t = d + (b + a + c)
5.25 + @@@ rew_sub begin: t = b + a + c*)
5.26
5.27
5.28
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/smltest/Scripts/rewrite.sml Mon Dec 10 11:09:26 2007 +0100
6.3 @@ -0,0 +1,64 @@
6.4 +(* tests for ME/rewrite.sml
6.5 + TODO.WN0509 collect typical tests from systest here !!!!!
6.6 + author: Walther Neuper 050908
6.7 + (c) copyright due to lincense terms.
6.8 +
6.9 +use"../smltest/Scripts/rewrite.sml";
6.10 +use"rewrite.sml";
6.11 +*)
6.12 +"-----------------------------------------------------------------";
6.13 +"table of contents -----------------------------------------------";
6.14 +"-----------------------------------------------------------------";
6.15 +"----------- rewrite_terms_ -------------------------------------";
6.16 +"----------- rewrite_inst_ bdvs ----------------------------------";
6.17 +"-----------------------------------------------------------------";
6.18 +"-----------------------------------------------------------------";
6.19 +"-----------------------------------------------------------------";
6.20 +
6.21 +
6.22 +"----------- rewrite_terms_ -------------------------------------";
6.23 +"----------- rewrite_terms_ -------------------------------------";
6.24 +"----------- rewrite_terms_ -------------------------------------";
6.25 +val subte = [str2term"x = 0"];
6.26 +val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
6.27 +val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
6.28 +if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
6.29 +else raise error "rewrite.sml rewrite_terms_ [x = 0]";
6.30 +
6.31 +val subte = [str2term"M_b 0 = 0"];
6.32 +val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
6.33 +val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
6.34 +if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
6.35 +else raise error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
6.36 +
6.37 +val subte = [str2term"x = 0", str2term"M_b 0 = 0"];
6.38 +val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
6.39 +val Some (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
6.40 +if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
6.41 +else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
6.42 +
6.43 +
6.44 +"----------- rewrite_inst_ bdvs ----------------------------------";
6.45 +"----------- rewrite_inst_ bdvs ----------------------------------";
6.46 +"----------- rewrite_inst_ bdvs ----------------------------------";
6.47 +(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
6.48 +val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
6.49 +val bdvs = [(str2term"bdv_1",str2term"c"),
6.50 + (str2term"bdv_2",str2term"c_2"),
6.51 + (str2term"bdv_3",str2term"c_3"),
6.52 + (str2term"bdv_4",str2term"c_4")];
6.53 +(*------------ outcommented WN071210, after inclusion into ROOT.ML
6.54 +val Some (t,_) =
6.55 + rewrite_inst_ thy e_rew_ord
6.56 + (append_rls "erls_isolate_bdvs" e_rls
6.57 + [(Calc ("EqSystem.occur'_exactly'_in",
6.58 + eval_occur_exactly_in
6.59 + "#eval_occur_exactly_in_"))
6.60 + ])
6.61 + false bdvs (num_str separate_bdvs_add) t;
6.62 +(writeln o term2str) t;
6.63 +if term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
6.64 +then () else raise error "rewrite.sml rewrite_inst_ bdvs";
6.65 +trace_rewrite:=true;
6.66 +trace_rewrite:=false;--------------------------------------------*)
6.67 +
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/smltest/Scripts/term_G.sml Mon Dec 10 11:09:26 2007 +0100
7.3 @@ -0,0 +1,82 @@
7.4 +(* tests on Scripts/term_G.sml
7.5 + author: Walther Neuper
7.6 + 051006,
7.7 + (c) due to copyright terms
7.8 +
7.9 +use"../smltest/Scripts/term_G.sml";
7.10 +use"term_G.sml";
7.11 +*)
7.12 +"-----------------------------------------------------------------";
7.13 +"table of contents -----------------------------------------------";
7.14 +"-----------------------------------------------------------------";
7.15 +"----------- inst_bdv --------------------------------------------";
7.16 +"----------- subst_atomic_all ------------------------------------";
7.17 +"----------- Pattern.match ---------------------------------------";
7.18 +"-----------------------------------------------------------------";
7.19 +"-----------------------------------------------------------------";
7.20 +"-----------------------------------------------------------------";
7.21 +
7.22 +
7.23 +"----------- inst_bdv --------------------------------------------";
7.24 +"----------- inst_bdv --------------------------------------------";
7.25 +"----------- inst_bdv --------------------------------------------";
7.26 +if string_of_thm (num_str d1_isolate_add2) =
7.27 + "\"~ ?bdv occurs_in ?a ==> (?a + ?bdv = 0) = (?bdv = -1 * ?a)\"" then ()
7.28 +else raise error "term_G.sml d1_isolate_add2";
7.29 +val subst = [(str2term "bdv", str2term "x")];
7.30 +val t = (norm o #prop o rep_thm) (num_str d1_isolate_add2);
7.31 +val t' = inst_bdv subst t;
7.32 +if term2str t' = "~ x occurs_in ?a ==> (?a + x = 0) = (x = -1 * ?a)" then ()
7.33 +else raise error "term_G.sml inst_bdv 1";
7.34 +
7.35 +if string_of_thm (num_str separate_bdvs_add) =
7.36 + "\"[] from_ [?bdv_1.0, ?bdv_2.0, ?bdv_3.0, ?bdv_4.0] occur_exactly_in ?a\n\
7.37 + \ ==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)\"" then ()
7.38 +else raise error "term_G.sml separate_bdvs_add";
7.39 +val subst = [(str2term"bdv_1",str2term"c"),
7.40 + (str2term"bdv_2",str2term"c_2"),
7.41 + (str2term"bdv_3",str2term"c_3"),
7.42 + (str2term"bdv_4",str2term"c_4")];
7.43 +val t = (norm o #prop o rep_thm) (num_str separate_bdvs_add);
7.44 +val t' = inst_bdv subst t;
7.45 +if term2str t' = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in ?a\n\
7.46 + \==> (?a + ?b = ?c) = (?b = ?c + -1 * ?a)" then ()
7.47 +else raise error "term_G.sml inst_bdv 2";
7.48 +
7.49 +
7.50 +"----------- subst_atomic_all ------------------------------------";
7.51 +"----------- subst_atomic_all ------------------------------------";
7.52 +"----------- subst_atomic_all ------------------------------------";
7.53 +val t = str2term"(tl vs_) from_ vs_ occur_exactly_in (nth_ 1(es_::bool list))";
7.54 +val env = [(str2term"vs_::real list",str2term"[c, c_2]"),
7.55 + (str2term"es_::bool list",str2term"[c_2=0, c+c_2=1]")];
7.56 +val (all_Free_subst, t') = subst_atomic_all env t;
7.57 +if all_Free_subst andalso
7.58 + term2str t' = "tl [c, c_2] from_ [c, c_2] occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
7.59 +else raise error "term_G.sml subst_atomic_all should be 'true'";
7.60 +
7.61 +
7.62 +val (all_Free_subst, t') = subst_atomic_all (tl env) t;
7.63 +if not all_Free_subst andalso
7.64 + term2str t' = "tl vs_ from_ vs_ occur_exactly_in nth_ 1 [c_2 = 0, c + c_2 = 1]" then ()
7.65 +else raise error "term_G.sml subst_atomic_all should be 'false'";
7.66 +
7.67 +
7.68 +"----------- Pattern.match ---------------------------------------";
7.69 +"----------- Pattern.match ---------------------------------------";
7.70 +"----------- Pattern.match ---------------------------------------";
7.71 +val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
7.72 +val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = c";
7.73 +(* !^^^^^^^^!... necessary for Pattern.match*)
7.74 +val insts = Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t);
7.75 +(*val insts =
7.76 + ([],
7.77 + [(("c",0),Free ("1","RealDef.real")),(("b",0),Free ("x","RealDef.real")),
7.78 + (("a",0),Free ("3","RealDef.real"))])
7.79 + : (indexname * typ) list * (indexname * term) list*)
7.80 +
7.81 +"----- throws exn MATCH...";
7.82 +val t = str2term "x";
7.83 +(Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))
7.84 +handle MATCH => ([(* (Term.indexname * Term.typ) *)],
7.85 + [(* (Term.indexname * Term.term) *)]);