1.1 --- a/src/Tools/isac/ProgLang/calculate.sml Thu Sep 23 16:38:25 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Sat Sep 25 16:49:33 2010 +0200
1.3 @@ -229,9 +229,7 @@
1.4 tracing("@@@ get_calculation: ct= ");atomty ct;*)
1.5 NONE)
1.6 | SOME (thmid,t) =>
1.7 - ((*tracing("@@@ get_calculation: NONE, op_="^op_);
1.8 - tracing("@@@ get_calculation: ct= ");atomty ct;*)
1.9 - SOME (thmid, (make_thm o (cterm_of thy)) t));
1.10 + SOME (thmid, (make_thm o (cterm_of thy)) t);
1.11 (*
1.12 > val ct = (the o (parse thy)) "#9 is_const";
1.13 > get_calculation_ thy ("is'_const",the (assoc(!eval_list,"is'_const"))) ct;
2.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Sep 23 16:38:25 2010 +0200
2.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Sat Sep 25 16:49:33 2010 +0200
2.3 @@ -14,30 +14,13 @@
2.4 (thy, 1, []:(Term.term * Term.term) list, rew_ord, erls, bool,thm,term);
2.5 *)
2.6 fun rewrite__ thy i bdv tless rls put_asm thm ct =
2.7 - ((*tracing ("@@@ r..te__ begin: t = "^(term2str ct));*)
2.8 - let
2.9 + (let
2.10 val (t',asms,lrd,rew) =
2.11 rew_sub thy i bdv tless rls put_asm [(*root of the term*)]
2.12 (((inst_bdv bdv) o norm o #prop o rep_thm) thm) ct;
2.13 in if rew then SOME (t', distinct asms)
2.14 else NONE end)
2.15 -(* val(r,t)=(((inst_bdv bdv) o norm o #prop o rep_thm) thm,ct);
2.16 - val t1 = (#prop o rep_thm) thm;
2.17 - val t2 = norm t1;
2.18 - val t3 = inst_bdv bdv t2;
2.19 -
2.20 - val thm4 = read_instantiate [("bdv","x")] thm;
2.21 - val t4 = (norm o #prop o rep_thm) thm4;
2.22 - *)
2.23 -(* val (thy, i, bdv, tless, rls, put_asm, r, t) =
2.24 - (thy, i,bdv, tless, rls, put_asm,
2.25 - (((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
2.26 - val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
2.27 - (thy, 1, [], ord, erls,false, [], r, t);
2.28 - val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
2.29 - (thy, i, bdv, tless, rls, put_asm, [],
2.30 - ((inst_bdv bdv) o norm o #prop o rep_thm) thm, ct);
2.31 - *)
2.32 +(* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
2.33 and rew_sub thy i bdv tless rls put_asm lrd r t =
2.34 ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));*)
2.35 let (* copy from Pure/thm.ML: fun rewritec *)
2.36 @@ -45,7 +28,8 @@
2.37 o Logic.strip_imp_concl) r;
2.38 val r' = Envir.subst_term (Pattern.match thy (lhs, t)
2.39 (Vartab.empty, Vartab.empty)) r;
2.40 - val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
2.41 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
2.42 + (Logic.count_prems r', [], r'));
2.43 val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
2.44 o Logic.strip_imp_concl) r';
2.45 (*val _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)
2.46 @@ -57,7 +41,7 @@
2.47 then (if ! trace_rewrite andalso i < ! depth andalso p' <> []
2.48 then tracing((idt"#"(i+1))^" asms accepted: "^(terms2str p')^
2.49 " stored: "^(terms2str simpl_p'))
2.50 - else(); (t',simpl_p')) (* + unconditional rew.*)
2.51 + else(); (t',simpl_p')) (* uncond.rew. from above*)
2.52 else
2.53 (if ! trace_rewrite andalso i < ! depth
2.54 then tracing((idt"#"(i+1))^" asms false: "^(terms2str p'))
2.55 @@ -93,19 +77,13 @@
2.56 in if rew1 then (t1' $ t2, asm1, lrd, true)
2.57 else (t1 $ t2,[], lrd, false) end
2.58 end)
2.59 -(* val (cprems',rls)=([pre],prls);
2.60 - rewrite__set_ thy i false rls pre;
2.61 - *)
2.62 +(* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)
2.63 and eval__true thy i asms bdv rls =
2.64 -(* val (thy, i, asms, bdv, rls) = (thy, (i+1), p', bdv, rls);
2.65 - *)
2.66 - if asms = [HOLogic.true_const] orelse asms = []
2.67 - then ([], true) else if asms = [HOLogic.false_const] then ([], false)
2.68 + if asms = [HOLogic.true_const] orelse asms = [] then ([], true)
2.69 + else if asms = [HOLogic.false_const] then ([], false)
2.70 else let
2.71 fun chk indets [] = (indets, true)(*return asms<>True until false*)
2.72 | chk indets (a::asms) =
2.73 -(* val (indets, (a::asms)) = ([], asms);
2.74 - *)
2.75 (case rewrite__set_ thy (i+1) false bdv rls a of
2.76 NONE => (chk (indets @ [a]) asms)
2.77 | SOME (t, a') =>
2.78 @@ -113,11 +91,12 @@
2.79 then (chk (indets @ a') asms)
2.80 else if t = HOLogic.false_const then ([], false)
2.81 (*asm false .. thm not applied ^^^; continue until False vvv*)
2.82 - else (chk (indets @ [t] @ a') asms));
2.83 + else chk (indets @ [t] @ a') asms);
2.84 in chk [] asms end
2.85 -
2.86 +(* rewrite with a rule set, which must not be the empty Erls *)
2.87 and rewrite__set_ _ _ __ Erls t =
2.88 raise error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
2.89 + (* rewrite with a 'reverse rule set' based on ML code *)
2.90 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
2.91 let val _= if ! trace_rewrite andalso i < ! depth
2.92 then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
2.93 @@ -125,6 +104,7 @@
2.94 val (t', asm, rew) = app_rev thy (i+1) rrls t
2.95 in if rew then SOME (t', distinct asm)
2.96 else NONE end
2.97 + (* rewrite with a rule set containing Thms or Calculations *)
2.98 | rewrite__set_ thy i put_asm bdv rls ct =
2.99 (* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
2.100 *)
2.101 @@ -154,8 +134,7 @@
2.102 tracing((idt"#"(i+1))^" try calc: "^op_^"'") else ();
2.103 val ct = uminus_to_string ct
2.104 in case get_calculation_ thy cc ct of
2.105 - NONE => ((*tracing "@@@ rewrite__set_: get_calculation_-> NONE";*)
2.106 - rew_once ruls asm ct apno thms)
2.107 + NONE => rew_once ruls asm ct apno thms
2.108 | SOME (thmid, thm') =>
2.109 let
2.110 val pairopt =
2.111 @@ -168,10 +147,8 @@
2.112 then tracing((idt"="(i+1))^" calc. to: "^
2.113 (term2str ((fst o the) pairopt)))
2.114 else()
2.115 - in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end
2.116 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end
2.117 end)
2.118 -(* use"ProgLang/rewrite.sml";
2.119 - @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
2.120 | Cal1 (cc as (op_,_)) =>
2.121 (let val _= if !trace_rewrite andalso i < ! depth then
2.122 tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
2.123 @@ -192,7 +169,6 @@
2.124 else()
2.125 in the pairopt end
2.126 end)
2.127 -(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
2.128 | Rls_ rls' =>
2.129 (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
2.130 SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
3.1 --- a/src/Tools/isac/calcelems.sml Thu Sep 23 16:38:25 2010 +0200
3.2 +++ b/src/Tools/isac/calcelems.sml Sat Sep 25 16:49:33 2010 +0200
3.3 @@ -606,10 +606,14 @@
3.4 however, dynamic lookup is required, since "Isac" is not yet built here.*)
3.5 fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term
3.6 (ProofContext.init_global (Thy_Info.get_theory "Isac"))) t;
3.7 +fun terms2str ts = (strs2str o (map term2str )) ts;
3.8 +(*terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";*)
3.9 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
3.10 +(*terms2str' [t1,t2] = "[1 + 2,abc]";*)
3.11 +fun terms2strs ts = (map term2str) ts;
3.12 +(*terms2strs [t1,t2] = ["1 + 2", "abc"];*)
3.13
3.14 -fun terms2str ts= (strs2str o (map (Syntax.string_of_term
3.15 - (thy2ctxt' "Isac")))) ts;
3.16 -fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
3.17 +un type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
3.18 val string_of_typ = type2str;
3.19
3.20 fun subst2str (s:subst) =
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/coding-standard.txt Sat Sep 25 16:49:33 2010 +0200
4.3 @@ -0,0 +1,2 @@
4.4 +these string patterns serve 'grep -R "SEE BELOW" *':
4.5 +# " thmid: "
5.1 --- a/src/Tools/isac/library.sml Thu Sep 23 16:38:25 2010 +0200
5.2 +++ b/src/Tools/isac/library.sml Sat Sep 25 16:49:33 2010 +0200
5.3 @@ -324,3 +324,20 @@
5.4 if key = keyi then SOME xi else assoc_string (pairs, key);
5.5 fun if_none NONE y = y (*cp from 2002 Pure/library.ML FIXXXME replace*)
5.6 | if_none (SOME x) _ = x;
5.7 +
5.8 +(* redirect tracing, following The Isabelle Cookbook *)
5.9 +(* TODO: how redirect tracing to emacs buffer again ? *)
5.10 +val strip_specials =
5.11 + let
5.12 + fun strip ("\^A" :: _ :: cs) = strip cs
5.13 + | strip (c :: cs) = c :: strip cs
5.14 + | strip [] = [];
5.15 + in
5.16 + implode o strip o explode
5.17 + end
5.18 +fun redir stream =
5.19 + Output.tracing_fn := (fn s =>
5.20 + (TextIO.output (stream, (strip_specials s));
5.21 + TextIO.output (stream, "\n");
5.22 + TextIO.flushOut stream));
5.23 +fun redirect_tracing path = redir (TextIO.openOut path);
6.1 --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 16:38:25 2010 +0200
6.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sat Sep 25 16:49:33 2010 +0200
6.3 @@ -182,11 +182,33 @@
6.4 "----- stepwise from the rulesets in simplify_Integral and below-----";
6.5 (*###*)val rls = norm_Rational_noadd_fractions;
6.6 "###-1-##################################################";
6.7 +(*--------------------------------------------------------------------
6.8 +val strip_specials =
6.9 +let
6.10 + fun strip ("\^A" :: _ :: cs) = strip cs
6.11 + | strip (c :: cs) = c :: strip cs
6.12 + | strip [] = [];
6.13 +in
6.14 + implode o strip o explode
6.15 +end;
6.16 +
6.17 +fun redirect_tracing stream =
6.18 + Output.tracing_fn := (fn s =>
6.19 + (TextIO.output (stream, (strip_specials s));
6.20 + TextIO.output (stream, "\n");
6.21 + TextIO.flushOut stream));
6.22 +
6.23 +redirect_tracing (TextIO.openOut "/home/neuper/tmp/trace_rewrite.sml");
6.24 +--------------------------------------------------------------------*)
6.25 trace_rewrite := true;
6.26 -val SOME (ttt, _) = rewrite_set_inst_ thy true subs rls t;
6.27 +
6.28 +tracing "###-1-##################################################";
6.29 +(*val SOME (ttt, _) =*) rewrite_set_inst_ thy true subs rls t;
6.30 +tracing "###-2-##################################################";
6.31 term2str ttt;
6.32 "###-2-##################################################";
6.33
6.34 +(*===== inhibit exn ====================================================
6.35 case rewrite_set_inst_ thy true subs rls t of
6.36 SOME _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
6.37 | NONE => ();
6.38 @@ -594,3 +616,6 @@
6.39 if p = ([], Res) andalso term2str res = "5 * a" then ()
6.40 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
6.41 *)
6.42 +
6.43 +
6.44 +===== inhibit exn ====================================================*)
7.1 --- a/test/Tools/isac/Knowledge/poly.sml Thu Sep 23 16:38:25 2010 +0200
7.2 +++ b/test/Tools/isac/Knowledge/poly.sml Sat Sep 25 16:49:33 2010 +0200
7.3 @@ -2,30 +2,40 @@
7.4 author: Matthias Goldgruber 2003
7.5 (c) due to copyright terms
7.6
7.7 -use"../smltest/IsacKnowledge/poly.sml";
7.8 -use"poly.sml";
7.9 -****************************************************************.*)
7.10 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
7.11 + 10 20 30 40 50 60 70 80
7.12 +*)
7.13
7.14 -(******************************************************************
7.15 +(*******************************************************************************
7.16 WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
7.17 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
7.18 -*******************************************************************)
7.19 -"-----------------------------------------------------------------";
7.20 -"table of contents -----------------------------------------------";
7.21 -"-----------------------------------------------------------------";
7.22 -"-------- build Script Expand_binoms -----------------------------";
7.23 -"-------- investigate new uniary minus ---------------------------";
7.24 -"-------- Bsple aus Schalk I -------------------------------------";
7.25 -"-------- Script 'simplification for_polynomials' ----------------";
7.26 -"-------- check pbl 'polynomial simplification' -----------------";
7.27 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
7.28 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
7.29 -"-------- ord_make_polynomial ------------------------------------";
7.30 -"-----------------------------------------------------------------";
7.31 -"-----------------------------------------------------------------";
7.32 -"-----------------------------------------------------------------";
7.33 +*******************************************************************************)
7.34 +"--------------------------------------------------------";
7.35 +"--------------------------------------------------------";
7.36 +"table of contents --------------------------------------";
7.37 +"--------------------------------------------------------";
7.38 +"-------- check is'_polyexp is_polyexp ------------------";
7.39 +"-------- build Script Expand_binoms --------------------";
7.40 +"-------- investigate new uniary minus ------------------";
7.41 +"-------- Bsple aus Schalk I ----------------------------";
7.42 +"-------- Script 'simplification for_polynomials' -------";
7.43 +"-------- check pbl 'polynomial simplification' --------";
7.44 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
7.45 +"-------- norm_Poly NOT COMPLETE ------------------------";
7.46 +"-------- ord_make_polynomial ---------------------------";
7.47 +"--------------------------------------------------------";
7.48 +"--------------------------------------------------------";
7.49 +"--------------------------------------------------------";
7.50
7.51
7.52 +"-------- check is'_polyexp is_polyexp ------------------";
7.53 +"-------- check is'_polyexp is_polyexp ------------------";
7.54 +"-------- check is'_polyexp is_polyexp ------------------";
7.55 +if is_polyexp @{term "x / x"}
7.56 +then raise error "poly.sml: check is'_polyexp is_polyexp" else ();
7.57 +
7.58 +
7.59 +(*===== inhibit exn ?===========================================================
7.60 "-------- build Script Expand_binoms -----------------------------";
7.61 "-------- build Script Expand_binoms -----------------------------";
7.62 "-------- build Script Expand_binoms -----------------------------";
7.63 @@ -466,3 +476,4 @@
7.64
7.65
7.66 ----------------------------------------------*)
7.67 +===== inhibit exn ?===========================================================*)
8.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Sep 23 16:38:25 2010 +0200
8.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Sat Sep 25 16:49:33 2010 +0200
8.3 @@ -1,10 +1,15 @@
8.4 -(* test calculation of values for function constants
8.5 - (c) Walther Neuper 2000
8.6 +(* Title: test calculation of values for function constants
8.7 + Author: Walther Neuper 2000
8.8 + (c) copyright due to lincense terms.
8.9
8.10 -use"../smltest/Scripts/calculate.sml";
8.11 -use"calculate.sml";
8.12 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
8.13 + 10 20 30 40 50 60 70 80
8.14 *)
8.15
8.16 +"--------------------------------------------------------";
8.17 +"table of contents --------------------------------------";
8.18 +"--------------------------------------------------------";
8.19 +"----------- check return value of get_calculation_ ----";
8.20 " ================= calculate.sml: calculate_ ======================== ";
8.21 " ================= calculate.sml: aus script ======================== ";
8.22 " ================= calculate.sml: 2.8.02 check test-root-equ ======== ";
8.23 @@ -14,14 +19,25 @@
8.24 "----------- get_pair with 3 args --------------------------------";
8.25 " ================= eval_binop Float =================== ";
8.26 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
8.27 +"--------------------------------------------------------";
8.28 +"--------------------------------------------------------";
8.29 +"--------------------------------------------------------";
8.30
8.31 -(* [("Vars",("Tools.Vars",fn)),("Length",("Tools.Length",fn)),
8.32 - ("Nth",("Tools.Nth",fn)),
8.33 - ("power_",("Atools.pow",fn)),("plus",("Groups.plus_class.plus",fn)),("times",("op *",fn)),
8.34 - ("is_const",("Atools.is'_const",fn)),
8.35 - ("le",("op <",fn)),("leq",("op <=",fn)),
8.36 - ("ident",("Atools.ident",fn))] *)
8.37
8.38 +"----------- check return value of get_calculation_ ----";
8.39 +"----------- check return value of get_calculation_ ----";
8.40 +"----------- check return value of get_calculation_ ----";
8.41 +val thy = theory "Poly";
8.42 +val cal = snd (assoc1 (! calclist', "is_polyexp"));
8.43 +val t = @{term "(x / x) is_polyexp"};
8.44 +val SOME (thmID, thm) = get_calculation_ thy cal t;
8.45 +(HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")
8.46 +handle TERM _ =>
8.47 + raise error "calculate.sml: get_calculation_ must return Trueprop";
8.48 +
8.49 +
8.50 +
8.51 +(*===== inhibit exn ?===========================================================
8.52 val thy' = "Isac.thy";
8.53
8.54 " ================= calculate.sml: calculate_ ======================== ";
8.55 @@ -31,24 +47,24 @@
8.56
8.57 val thy = Test.thy;
8.58 val t = (term_of o the o (parse thy)) "1+2";
8.59 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
8.60 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
8.61
8.62 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
8.63 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
8.64 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.65 -Syntax.string_of_term (thy2ctxt thy) t;
8.66 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
8.67 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.68 +Sign.string_of_term (sign_of thy) t;
8.69 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
8.70 -val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
8.71 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.72 -Syntax.string_of_term (thy2ctxt thy) t;
8.73 +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
8.74 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.75 +Sign.string_of_term (sign_of thy) t;
8.76 (*val it = "(#12 // #3) ^^^ #2" : string*)
8.77 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
8.78 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.79 -Syntax.string_of_term (thy2ctxt thy) t;
8.80 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
8.81 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.82 +Sign.string_of_term (sign_of thy) t;
8.83 (*it = "#4 ^^^ #2" : string*)
8.84 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
8.85 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.86 -Syntax.string_of_term (thy2ctxt thy) t;
8.87 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
8.88 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.89 +Sign.string_of_term (sign_of thy) t;
8.90 (*val it = "#16" : string*)
8.91 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
8.92 else ();
8.93 @@ -61,14 +77,14 @@
8.94 (prep_pbt Test.thy "pbl_ttest" [] e_pblID
8.95 (["test"],
8.96 [],
8.97 - e_rls, NONE, []));
8.98 + e_rls, None, []));
8.99 store_pbt
8.100 (prep_pbt Test.thy "pbl_ttest_calc" [] e_pblID
8.101 (["calculate","test"],
8.102 [("#Given" ,["realTestGiven t_"]),
8.103 ("#Find" ,["realTestFind s_"])
8.104 ],
8.105 - e_rls, NONE, [["Test","test_calculate"]]));
8.106 + e_rls, None, [["Test","test_calculate"]]));
8.107
8.108 store_met
8.109 (prep_met Test.thy "met_testcal" [] e_metID
8.110 @@ -77,9 +93,9 @@
8.111 ("#Find" ,["realTestFind s_"])
8.112 ],
8.113 {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
8.114 - calc=[("plus" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
8.115 + calc=[("plus" ,("op +" ,eval_binop "#add_")),
8.116 ("times" ,("op *" ,eval_binop "#mult_")),
8.117 - ("divide_" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_")),
8.118 + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")),
8.119 ("power_" ,("Atools.pow" ,eval_binop "#power_"))],
8.120 crls=tval_rls, nrls=e_rls(*,
8.121 asm_rls=[],asm_thm=[]*)},
8.122 @@ -145,7 +161,7 @@
8.123 val op_ = "divide_";
8.124 val ct = "sqrt (x ^^^ 2 + -3 * x) =\
8.125 \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
8.126 - val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
8.127 + val Some (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
8.128 writeln ct;
8.129 (*
8.130 sqrt (x ^^^ 2 + -3 * x) =\
8.131 @@ -171,10 +187,10 @@
8.132 val t = (term_of o the o (parse Test.thy)) "2 is_const";
8.133 atomty t;
8.134 rewrite_set_ Test.thy false tval_rls t;
8.135 -(*val it = SOME (Const ("True","bool"),[]) ... works*)
8.136 +(*val it = Some (Const ("True","bool"),[]) ... works*)
8.137
8.138 val t = str2term "2 * x is_const";
8.139 - val SOME (str,t') = eval_const "" "" t Isac.thy;
8.140 + val Some (str,t') = eval_const "" "" t Isac.thy;
8.141 term2str t';
8.142
8.143
8.144 @@ -185,7 +201,7 @@
8.145 trace_rewrite:=true;
8.146 val thy = Test.thy;
8.147 val t = (term_of o the o (parse thy)) "(-4) / 2";
8.148 - val SOME (_,t) = eval_cancel "xxx" "Rings.inverse_class.divide" t thy;
8.149 + val Some (_,t) = eval_cancel "xxx" "HOL.divide" t thy;
8.150 term2str t;
8.151 "-4 / 2 = (-2)";
8.152 (*-------------- but ... *)
8.153 @@ -219,7 +235,7 @@
8.154 val thy = Test.thy;
8.155 val rls = Test_simplify;
8.156 val t = str2term "(3+(1+2*x))/2";
8.157 - val SOME (t',asm) = rewrite_set_ thy false rls t;
8.158 + val Some (t',asm) = rewrite_set_ thy false rls t;
8.159 term2str t';
8.160 (*val t = "2 + x" ... works: give up----------------------------------------*)
8.161 trace_rewrite:=false;
8.162 @@ -267,12 +283,12 @@
8.163 ### trying calc. 'cancel'
8.164 @@@ get_pair: binop, t = x + (-4) / 2
8.165 @@@ get_pair: t else
8.166 -@@@ get_pair: t else -> NONE
8.167 +@@@ get_pair: t else -> None
8.168 @@@ get_pair: binop, t = (-4) / 2
8.169 @@@ get_pair: then 1
8.170 -@@@ get_pair: t -> NONE
8.171 -@@@ get_pair: t1 -> NONE
8.172 -@@@ get_calculation: NONE
8.173 +@@@ get_pair: t -> None
8.174 +@@@ get_pair: t1 -> None
8.175 +@@@ get_calculation: None
8.176 ### trying calc. 'pow'
8.177 *)
8.178
8.179 @@ -286,10 +302,10 @@
8.180 ### trying calc. 'cancel'
8.181 @@@ get_pair: binop, t = x + -4 / 2
8.182 @@@ get_pair: t else
8.183 -@@@ get_pair: t else -> NONE
8.184 +@@@ get_pair: t else -> None
8.185 @@@ get_pair: binop, t = -4 / 2
8.186 @@@ get_pair: then 1
8.187 -@@@ get_calculation: SOME #cancel_-4_2
8.188 +@@@ get_calculation: Some #cancel_-4_2
8.189 ### calc. to: x + (-2)
8.190 ### trying calc. 'cancel'
8.191 *)
8.192 @@ -330,8 +346,8 @@
8.193 *** Const ( HOL.divide, [real, real] => real)
8.194 *** . Free ( aaa, real)
8.195 *** . Free ( 1, real) *)
8.196 - val thm = num_str @{thm divide_1};
8.197 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.198 + val thm = num_str real_divide_1;
8.199 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.200 (*val t = Free ("aaa","RealDef.real") : term*)
8.201
8.202
8.203 @@ -365,8 +381,8 @@
8.204 *** Const ( Nat.power, [real, nat] => real)
8.205 *** . Free ( 1, real)
8.206 *** . Free ( aaa, nat) .......................... nat !!! *)
8.207 - val thm = num_str @{thm realpow_eq_one;
8.208 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.209 + val thm = num_str realpow_eq_one;
8.210 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.211 (*val t = Free ("1","RealDef.real") : term*)
8.212
8.213 " ================= calculate.sml: calculate_ 2002 =================== ";
8.214 @@ -375,42 +391,42 @@
8.215
8.216 val thy = Test.thy;
8.217 val t = (term_of o the o (parse thy)) "12 / 3";
8.218 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
8.219 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.220 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
8.221 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.222 "12 / 3 = 4";
8.223 val thy = Test.thy;
8.224 val t = (term_of o the o (parse thy)) "4 ^^^ 2";
8.225 -val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
8.226 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.227 +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t;
8.228 +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.229 "4 ^ 2 = 16";
8.230
8.231 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
8.232 - val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
8.233 + val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
8.234 "1 + 2 = 3";
8.235 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.236 - Syntax.string_of_term (thy2ctxt thy) t;
8.237 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.238 + Sign.string_of_term (sign_of thy) t;
8.239 "(3 * 4 / 3) ^^^ 2";
8.240 - val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
8.241 + val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
8.242 "3 * 4 = 12";
8.243 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.244 - Syntax.string_of_term (thy2ctxt thy) t;
8.245 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.246 + Sign.string_of_term (sign_of thy) t;
8.247 "(12 / 3) ^^^ 2";
8.248 - val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
8.249 + val Some (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
8.250 "12 / 3 = 4";
8.251 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.252 - Syntax.string_of_term (thy2ctxt thy) t;
8.253 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.254 + Sign.string_of_term (sign_of thy) t;
8.255 "4 ^^^ 2";
8.256 - val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
8.257 + val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
8.258 "4 ^^^ 2 = 16";
8.259 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.260 - Syntax.string_of_term (thy2ctxt thy) t;
8.261 + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t;
8.262 + Sign.string_of_term (sign_of thy) t;
8.263 "16";
8.264 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
8.265 else ();
8.266
8.267 (*13.9.02 *** calc: operator = pow not defined*)
8.268 val t = (term_of o the o (parse thy)) "3^^^2";
8.269 - val SOME (thmID,thm) =
8.270 + val Some (thmID,thm) =
8.271 get_calculation_ thy (the(assoc(calclist,"power_"))) t;
8.272 (*** calc: operator = pow not defined*)
8.273
8.274 @@ -419,14 +435,14 @@
8.275 val op_ = "Atools.pow" : string
8.276 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
8.277
8.278 - val SOME (thmid,t') = get_pair thy op_ eval_fn t;
8.279 + val Some (thmid,t') = get_pair thy op_ eval_fn t;
8.280 (*** calc: operator = pow not defined*)
8.281
8.282 - val SOME (id,t') = eval_fn op_ t thy;
8.283 + val Some (id,t') = eval_fn op_ t thy;
8.284 (*** calc: operator = pow not defined*)
8.285
8.286 val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
8.287 - val SOME (id,t') = eval_binop thmid op_ t thy;
8.288 + val Some (id,t') = eval_binop thmid op_ t thy;
8.289 (*** calc: operator = pow not defined*)
8.290
8.291
8.292 @@ -439,7 +455,7 @@
8.293 str2term
8.294 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
8.295 );
8.296 -val SOME (str, simpl) = get_pair thy op_ ef arg;
8.297 +val Some (str, simpl) = get_pair thy op_ ef arg;
8.298 if str =
8.299 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
8.300 then () else raise error "calculate.sml get_pair with 3 args:occur_exactly_in";
8.301 @@ -462,10 +478,11 @@
8.302 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
8.303 "------------------ 3.6.03 (2 * x is_const) ---------------------------";
8.304 val t = str2term "2 * x is_const";
8.305 -val SOME (str, t') = eval_const "" "" t Test.thy;
8.306 +val Some (str, t') = eval_const "" "" t Test.thy;
8.307 term2str t';
8.308 "(2 * x is_const) = False";
8.309
8.310 -val SOME (t',_) = rewrite_set_ Test.thy false tval_rls t;
8.311 +val Some (t',_) = rewrite_set_ Test.thy false tval_rls t;
8.312 term2str t';
8.313 "False";
8.314 +===== inhibit exn ?===========================================================*)
9.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Thu Sep 23 16:38:25 2010 +0200
9.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Sat Sep 25 16:49:33 2010 +0200
9.3 @@ -3,26 +3,27 @@
9.4 author: Walther Neuper 050908
9.5 (c) copyright due to lincense terms.
9.6
9.7 -use"../smltest/Scripts/rewrite.sml";
9.8 -use"rewrite.sml";
9.9 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
9.10 + 10 20 30 40 50 60 70 80
9.11 *)
9.12
9.13 -"-----------------------------------------------------------------";
9.14 -"table of contents -----------------------------------------------";
9.15 -"-----------------------------------------------------------------";
9.16 -"----------- assemble rewrite ------------------------------------";
9.17 -"----------- test rewriting without Isac's thys ------------------";
9.18 -"----------- conditional rewriting without Isac's thys -----------";
9.19 -"----------- rewrite_terms_ -------------------------------------";
9.20 -"----------- rewrite_inst_ bdvs ----------------------------------";
9.21 -"-----------------------------------------------------------------";
9.22 -"-----------------------------------------------------------------";
9.23 -"-----------------------------------------------------------------";
9.24 +"--------------------------------------------------------";
9.25 +"table of contents --------------------------------------";
9.26 +"--------------------------------------------------------";
9.27 +"----------- assemble rewrite ---------------------------";
9.28 +"----------- test rewriting without Isac's thys ---------";
9.29 +"----------- conditional rewriting without Isac's thys --";
9.30 +"----------- step through 'and rew_sub': ----------------";
9.31 +"----------- rewrite_terms_ ----------------------------";
9.32 +"----------- rewrite_inst_ bdvs -------------------------";
9.33 +"----------- check diff 2002--2009-3 --------------------";
9.34 +"--------------------------------------------------------";
9.35 +"--------------------------------------------------------";
9.36 +"--------------------------------------------------------";
9.37
9.38 -"----------- assemble rewrite ------------------------------------";
9.39 -"----------- assemble rewrite ------------------------------------";
9.40 -"----------- assemble rewrite ------------------------------------";
9.41 -(*ML {**)
9.42 +"----------- assemble rewrite ---------------------------";
9.43 +"----------- assemble rewrite ---------------------------";
9.44 +"----------- assemble rewrite ---------------------------";
9.45 "===== rewriting by thm with 'a";
9.46 show_types := true;
9.47 val thy = @{theory Complex_Main};
9.48 @@ -40,9 +41,9 @@
9.49 "----- fun match_rew in Pure/pattern.ML";
9.50 val rtm = the_default rhs (Term.rename_abs lhs t rhs);
9.51
9.52 -tracing(Syntax.string_of_term ctxt rtm);
9.53 -tracing(Syntax.string_of_term ctxt lhs);
9.54 -tracing(Syntax.string_of_term ctxt t);
9.55 +writeln(Syntax.string_of_term ctxt rtm);
9.56 +writeln(Syntax.string_of_term ctxt lhs);
9.57 +writeln(Syntax.string_of_term ctxt t);
9.58
9.59 (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty));
9.60 val (rew, rhs) = (Envir.subst_term
9.61 @@ -50,8 +51,7 @@
9.62 (*lookup in isabelle?trace?response...*)
9.63 writeln(Syntax.string_of_term ctxt rew);
9.64 writeln(Syntax.string_of_term ctxt rhs);
9.65 -(*}
9.66 -ML {*)
9.67 +
9.68 "===== rewriting: prep insertion into rew_sub";
9.69 val thy = @{theory Complex_Main};
9.70 val ctxt = @{context};
9.71 @@ -72,10 +72,10 @@
9.72 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} t');
9.73 (*}*)
9.74
9.75 -"----------- test rewriting without Isac's thys ------------------";
9.76 -"----------- test rewriting without Isac's thys ------------------";
9.77 -"----------- test rewriting without Isac's thys ------------------";
9.78 -(*ML {*)
9.79 +"----------- test rewriting without Isac's thys ---------";
9.80 +"----------- test rewriting without Isac's thys ---------";
9.81 +"----------- test rewriting without Isac's thys ---------";
9.82 +
9.83 "===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
9.84 val thy = @{theory Complex_Main};
9.85 val ctxt = @{context};
9.86 @@ -83,36 +83,36 @@
9.87 val tm = @{term "x + y*z::real"};
9.88
9.89 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
9.90 - handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
9.91 + handle _ => error "rewrite.sml diff.behav. in rewriting";
9.92 (*is displayed on _TOP_ of <response> buffer...*)
9.93 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
9.94 +if r = @{term "y*z + x::real"}
9.95 +then () else error "rewrite.sml diff.result in rewriting";
9.96
9.97 "----- rewriting a subterm";
9.98 val tm = @{term "w*(x + y*z)::real"};
9.99
9.100 val SOME (r,_) = (rewrite_ thy dummy_ord e_rls false thm tm)
9.101 - handle _ => error "rewrite.sml diff.behav. in rew_sub with Isabelle2009-1 only";
9.102 + handle _ => error "rewrite.sml diff.behav. in rew_sub";
9.103
9.104 "----- ordered rewriting";
9.105 -fun tord (_:subst) pp = TermOrd.termless pp;
9.106 +fun tord (_:subst) pp = Term_Ord.termless pp;
9.107 if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
9.108 -else error "rewrite.sml diff.behav. in ord.rewr. with Isabelle2009-1 only";
9.109 +else error "rewrite.sml diff.behav. in ord.rewr.";
9.110
9.111 val NONE = (rewrite_ thy tord e_rls false thm tm)
9.112 - handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
9.113 + handle _ => error "rewrite.sml diff.behav. in rewriting";
9.114 (*is displayed on _TOP_ of <response> buffer...*)
9.115 Pretty.writeln (ProofContext.pretty_term_abbrev @{context} r);
9.116
9.117 val tm = @{term "x*y + z::real"};
9.118 val SOME (r,_) = (rewrite_ thy tord e_rls false thm tm)
9.119 - handle _ => error "rewrite.sml diff.behav. in rewriting with Isabelle2009-1 only";
9.120 + handle _ => error "rewrite.sml diff.behav. in rewriting";
9.121
9.122
9.123 -(*}*)
9.124 -
9.125 -"----------- conditional rewriting without Isac's thys -----------";
9.126 -"----------- conditional rewriting without Isac's thys -----------";
9.127 -"----------- conditional rewriting without Isac's thys -----------";
9.128 +"----------- conditional rewriting without Isac's thys --";
9.129 +"----------- conditional rewriting without Isac's thys --";
9.130 +"----------- conditional rewriting without Isac's thys --";
9.131 (*ML {*)
9.132 "===== prepr cond.rew. with Pattern.match";
9.133 val thy = @{theory Complex_Main};
9.134 @@ -139,30 +139,63 @@
9.135 "----- conditional rewriting creating an assumption";
9.136 "----- conditional rewriting creating an assumption";
9.137 val tm = @{term "x*y / y::real"};
9.138 -val SOME (rew,asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
9.139 - handle _ => error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only a";
9.140 +val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
9.141 + handle _ => error "rewrite.sml diff.behav. in cond.rew.";
9.142
9.143 -if rew = @{term "x::real"} then ()
9.144 -else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only b";
9.145 +if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
9.146 +else error "rewrite.sml diff.result in cond.rew.";
9.147
9.148 -if HOLogic.dest_Trueprop (hd asm) = @{term "~ y = (0::real)"} then ()
9.149 -else error "rewrite.sml diff.behav. in cond.rew. with Isabelle2009-1 only c";
9.150 +if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
9.151 +then () else error "rewrite.sml diff.asm in cond.rew.";
9.152 +"----- conditional rewriting immediately: can only be done with ";
9.153 +"------Isabelle numerals, because erls cannot handle them yet.";
9.154
9.155 -"----- conditional rewriting immediately: can only be done with Isabelle numerals\
9.156 -\because erls cannot handle them yet.";
9.157 -(*}*)
9.158
9.159 +"----------- step through 'and rew_sub': ----------------";
9.160 +"----------- step through 'and rew_sub': ----------------";
9.161 +"----------- step through 'and rew_sub': ----------------";
9.162 +(*and make asms without Trueprop, beginning with the result:*)
9.163 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (prop_of thm) tm;
9.164 +show_types := false;
9.165 +"----- evaluate arguments";
9.166 +val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
9.167 + (thy, 0, [], dummy_ord, e_rls, true, [], (prop_of thm), tm);
9.168 +"----- step 1: lhs, rhs of rule";
9.169 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
9.170 + o Logic.strip_imp_concl) r;
9.171 +term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
9.172 +term2str lhs = "?a * ?b / ?b"; term2str rhs = "?a";
9.173 +"----- step 2: the rule instantiated";
9.174 + val r' = Envir.subst_term (Pattern.match thy (lhs, t)
9.175 + (Vartab.empty, Vartab.empty)) r;
9.176 +term2str r' = "y ~= 0 ==> x * y / y = x";
9.177 +"----- step 3: get the (instantiated) assumption(s)";
9.178 + val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
9.179 +term2str (hd p') = "y ~= 0";
9.180 +"=====vvv make asms without Trueprop ---vvv";
9.181 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
9.182 + (Logic.count_prems r', [], r'));
9.183 +case p' of
9.184 + [Const ("Not", _) $ (Const ("op =", _) $ Free ("y", _) $
9.185 + Const ("Groups.zero_class.zero", _))] => ()
9.186 + | _ => error "rewrite.sml assumption changed";
9.187 +"=====^^^ make asms without Trueprop ---^^^";
9.188 +"----- step 4: get the (instantiated) rhs";
9.189 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
9.190 + o Logic.strip_imp_concl) r';
9.191 +term2str t' = "x";
9.192
9.193 -"----------- rewrite_terms_ -------------------------------------";
9.194 -"----------- rewrite_terms_ -------------------------------------";
9.195 -"----------- rewrite_terms_ -------------------------------------";
9.196 -val subte = [str2term"x = 0"];
9.197 -val t = str2term"M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
9.198 -val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
9.199 +(*===== inhibit exn ============================================================
9.200 +"----------- rewrite_terms_ ----------------------------";
9.201 +"----------- rewrite_terms_ ----------------------------";
9.202 +"----------- rewrite_terms_ ----------------------------";
9.203 +val subte = [str2term "x = 0"];
9.204 +val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
9.205 +val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t; (*NONE..TODO*)
9.206 if term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
9.207 else raise error "rewrite.sml rewrite_terms_ [x = 0]";
9.208
9.209 -val subte = [str2term"M_b 0 = 0"];
9.210 +val subte = [str2term "M_b 0 = 0"];
9.211 val t = str2term"M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
9.212 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
9.213 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
9.214 @@ -173,11 +206,12 @@
9.215 val SOME (t',_) = rewrite_terms_ thy dummy_ord Erls subte t;
9.216 if term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
9.217 else raise error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
9.218 +===== inhibit exn ============================================================*)
9.219
9.220
9.221 -"----------- rewrite_inst_ bdvs ----------------------------------";
9.222 -"----------- rewrite_inst_ bdvs ----------------------------------";
9.223 -"----------- rewrite_inst_ bdvs ----------------------------------";
9.224 +"----------- rewrite_inst_ bdvs -------------------------";
9.225 +"----------- rewrite_inst_ bdvs -------------------------";
9.226 +"----------- rewrite_inst_ bdvs -------------------------";
9.227 (*see smltest/Scripts/term_G.sml: inst_bdv 2*)
9.228 val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
9.229 val bdvs = [(str2term"bdv_1",str2term"c"),
9.230 @@ -199,3 +233,93 @@
9.231 trace_rewrite:=true;
9.232 trace_rewrite:=false;--------------------------------------------*)
9.233
9.234 +"----------- check diff 2002--2009-3 --------------------";
9.235 +"----------- check diff 2002--2009-3 --------------------";
9.236 +"----------- check diff 2002--2009-3 --------------------";
9.237 +(*----- 2002 -------------------------------------------------------------------
9.238 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
9.239 +q_0 * x ^^^ 2 / 2)
9.240 +## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
9.241 +/ 2)
9.242 +### try thm: real_diff_minus
9.243 +### try thm: sym_real_mult_minus1
9.244 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
9.245 +/ 2)
9.246 +### try thm: rat_mult_poly_l
9.247 +### try thm: rat_mult_poly_r
9.248 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
9.249 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
9.250 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
9.251 +##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
9.252 +is_polyexp
9.253 +###### try calc: Poly.is'_polyexp'
9.254 +====== calc. to: False
9.255 +###### try calc: Poly.is'_polyexp'
9.256 +###### try calc: Poly.is'_polyexp'
9.257 +#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
9.258 +----- 2002 NONE rewrite --------------------------------------------------------
9.259 +----- 2009 should maintain this behaviour, but: --------------------------------
9.260 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
9.261 +## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
9.262 +### try thm: real_diff_minus
9.263 +### try thm: sym_real_mult_minus1
9.264 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
9.265 +### try thm: rat_mult_poly_l
9.266 +### try thm: rat_mult_poly_r
9.267 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
9.268 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
9.269 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
9.270 +##### rls: e_rls-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
9.271 +###### try calc: Poly.is'_polyexp'
9.272 +====== calc. to: False
9.273 +###### try calc: Poly.is'_polyexp'
9.274 +###### try calc: Poly.is'_polyexp'
9.275 +#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
9.276 +=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
9.277 +----- 2009 -------------------------------------------------------------------*)
9.278 +
9.279 +(*the situation as was before repair (asm without Trueprop) is outcommented*)
9.280 +val thy = theory "Isac";
9.281 +"===== example which raised the problem =================";
9.282 +val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
9.283 +"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
9.284 +val subs = [(str2term "bdv", str2term "x")];
9.285 +val rls = norm_Rational_noadd_fractions;
9.286 +val NONE (*SOME (t', _)*) = rewrite_set_inst_ thy true subs rls t;
9.287 +"----- rewrite_ rat_mult_poly_r--------------------------";
9.288 +val thm = @{thm rat_mult_poly_r};
9.289 + "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
9.290 +val erls = append_rls "e_rls-is_polyexp" e_rls
9.291 + [Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
9.292 +val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
9.293 +(*t' = t''; (*false because of further rewrites in t'*)*)
9.294 +"----- rew_sub --------------------------------";
9.295 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
9.296 +(*t'' = t'''; (*true*)*)
9.297 +"----- rewrite_set_ erls --------------------------------";
9.298 +val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
9.299 +val NONE = rewrite_set_ thy true erls cond;
9.300 +(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
9.301 +
9.302 +writeln "===== maximally simplified example =====================";
9.303 +val t = @{term "a / b * (x / x ^^^ 2)"};
9.304 + "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
9.305 +writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
9.306 +val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
9.307 +term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
9.308 +(*checked visually: trace_rewrite looks like above for 2009*)
9.309 +
9.310 +trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
9.311 +show_types := false;
9.312 +writeln "----- rewrite_ rat_mult_poly_r--------------------------";
9.313 +val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
9.314 +(*t' = t''; (*false because of further rewrites in t'*)*)
9.315 +writeln "----- rew_sub --------------------------------";
9.316 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (prop_of thm) t;
9.317 +(*t'' = t'''; (*true*)*)
9.318 +writeln "----- rewrite_set_ erls --------------------------------";
9.319 +val cond = @{term "(x / x ^^^ 2)"};
9.320 +val NONE = rewrite_set_ thy true erls cond;
9.321 +(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
9.322 +trace_rewrite := false; (*<<<<<<<<<<<<<<<<<<<<<###############################*)
9.323 +"--------------------------------------------------------";
10.1 --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 16:38:25 2010 +0200
10.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Sep 25 16:49:33 2010 +0200
10.3 @@ -10,7 +10,7 @@
10.4 *)
10.5
10.6 theory Test_Isac imports Isac begin
10.7 -
10.8 +
10.9 ML{* writeln "**** run the tests **************************************" *};
10.10 ML {* Toplevel.debug := true; *}
10.11 (*
10.12 @@ -27,12 +27,29 @@
10.13 cd "../..";
10.14 *)
10.15 ML{* writeln "**** run systests complete ******************************" *};
10.16 +
10.17 +ML {*
10.18 +val t1 = @{term "1+2::real"};
10.19 +val t2 = @{term "abc"};
10.20 +term2str t2 = "abc";
10.21 +fun terms2str ts = (strs2str o (map term2str )) ts;
10.22 +terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]";
10.23 +fun terms2str' ts = (strs2str' o (map term2str )) ts;
10.24 +terms2str' [t1,t2] = "[1 + 2,abc]";
10.25 +fun terms2strs ts = (map term2str) ts;
10.26 +terms2strs [t1,t2] = ["1 + 2", "abc"];
10.27 +*}
10.28 +
10.29 (*
10.30 cd"smltest/Scripts";
10.31 use"calculate-float.sml";
10.32 - use"calculate.sml";
10.33 +*)
10.34 +use"ProgLang/calculate.sml"; (*part.*)
10.35 +(*
10.36 use"listg.sml";
10.37 - use"rewrite.sml";
10.38 +*)
10.39 +use"ProgLang/rewrite.sml"; (*part.*)
10.40 +(*
10.41 use"scrtools.sml";
10.42 use"term.sml";
10.43 use"tools.sml";
10.44 @@ -65,26 +82,15 @@
10.45 use"complex.sml";
10.46 use"diff.sml";
10.47 use"diffapp.sml";
10.48 -*)
10.49 -ML {*print_depth 3*}
10.50 +(**)
10.51 +use "Knowledge/integrate.sml"; (*part.*)
10.52
10.53 -ML {*
10.54 -trace_rewrite := true;
10.55 -fun ((i: int) upto j) =
10.56 - if i > j
10.57 - then (if !trace_rewrite then tracing (string_of_int i) else ();
10.58 - [])
10.59 - else (if !trace_rewrite then tracing (string_of_int i) else ();
10.60 - i :: (i + 1 upto j));
10.61 -1 upto 5;
10.62 -*}
10.63 -
10.64 -use "Knowledge/integrate.sml";
10.65 -(*
10.66 use"equation.sml";
10.67 (*use"inssort.sml"; problems with recdef in Isabelle2002*)
10.68 use"logexp.sml";
10.69 - use"poly.sml";
10.70 +*)
10.71 +use"Knowledge/poly.sml"; (*part.*)
10.72 +(*
10.73 use"polyminus.sml";
10.74 use"polyeq.sml"; (*TODO 31.b, n1., 44.a, 1.a~, 1.b (all'expanded')WN
10.75 ? also check others without check 'diff.behav.'*);
10.76 @@ -105,6 +111,14 @@
10.77 use"algein.sml";
10.78 cd "../..";
10.79 *)
10.80 +(* TODO
10.81 +use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
10.82 +
10.83 +*** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
10.84 +*** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
10.85 +
10.86 +use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
10.87 +*)
10.88 use_thy "../../Pure/Isar/Test_Parse_Term"
10.89 use_thy "../../Pure/Isar/Test_Parsers"
10.90