1.1 --- a/test/Tools/isac/Knowledge/rational.sml Sat Aug 24 11:54:39 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Sat Aug 24 17:41:40 2013 +0200
1.3 @@ -14,6 +14,7 @@
1.4 WN060104 transfer examples marked with (*SR..*) to the exp-collection
1.5 *)
1.6
1.7 +(*========== inhibit exn WN130824 TODO =======================================================
1.8 "--------------------------------------------------------";
1.9 "--------------------------------------------------------";
1.10 "table of contents --------------------------------------";
1.11 @@ -308,10 +309,10 @@
1.12 val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5";
1.13 val SOME t' = polynomial2expanded t; term2str t';
1.14 "1 - x ^^^ 2 - 5 * x ^^^ 5";
1.15 +============ inhibit exn WN130824 TODO ======================================================*)
1.16
1.17 "-------- fun poly_of_term ---------------------------------------------------";
1.18 "-------- fun poly_of_term ---------------------------------------------------";
1.19 -(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
1.20 "-------- fun poly_of_term ---------------------------------------------------";
1.21 val vs = "12 * x^^^3 * y^^^4 * z^^^6" |> str2term |> vars |> map free2str |> sort string_ord;
1.22
1.23 @@ -341,21 +342,17 @@
1.24 if poly_of_term vs (str2term "2 * x^^^3 * y^^^4 * z^^^6 + (7 * y^^^8 + 1)")
1.25 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
1.26 then () else error "poly_of_term 8 changed";
1.27 -============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
1.28
1.29 "-------- fun is_poly --------------------------------------------------------";
1.30 "-------- fun is_poly --------------------------------------------------------";
1.31 -(*========== inhibit exn WN130822 TODO =========================================================
1.32 "-------- fun is_poly --------------------------------------------------------";
1.33 if is_poly (str2term "2 * x^^^3 * y^^^4 * z^^^6 + 7 * y^^^8 + 1")
1.34 then () else error "is_poly 1 changed";
1.35 if not (is_poly (str2term "2 * (x^^^3 * y^^^4 * z^^^6 + 7) * y^^^8 + 1"))
1.36 then () else error "is_poly 2 changed";
1.37 -============ inhibit exn WN130822 TODO ========================================================*)
1.38
1.39 "-------- fun term_of_poly ---------------------------------------------------";
1.40 "-------- fun term_of_poly ---------------------------------------------------";
1.41 -(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
1.42 "-------- fun term_of_poly ---------------------------------------------------";
1.43 val expT = HOLogic.realT
1.44 val Free (_, baseT) = (hd o vars o str2term) "12 * x^^^3 * y^^^4 * z^^^6";
1.45 @@ -365,7 +362,6 @@
1.46 ;
1.47 if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
1.48 then () else error "term_of_poly 1 changed";
1.49 -============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
1.50
1.51
1.52 "-------- and app_rev --------------------------------------------------------";
1.53 @@ -419,7 +415,7 @@
1.54 | scan_ f (pp::pps) =
1.55 if f pp then true else scan_ f pps;
1.56
1.57 -(*========== inhibit exn WN130823: (pp::pps) = [(*prepat*)] ====================================
1.58 +(*========== inhibit exn WN130823: prepat is empty ====================================
1.59 (* scan_ chk prepat = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
1.60 "~~~~~ fun , args:"; val (f, (pp::pps)) = (chk, prepat);
1.61 f;
1.62 @@ -447,64 +443,58 @@
1.63 rewrite__set_ thy (i+1) false;
1.64 term2str a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*)
1.65 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a
1.66 -============ inhibit exn WN130823: (pp::pps) = [(*prepat*)] ===================================*)
1.67 +============ inhibit exn WN130823: prepat is empty ===================================*)
1.68
1.69 +(*========== inhibit exn WN130824 TODO =======================================================
1.70 "-------- external calculating functions test -----------";
1.71 "-------- external calculating functions test -----------";
1.72 "-------- external calculating functions test -----------";
1.73 -val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.74 -val SOME (t1',asm)= factout_p_ thy t1;
1.75 -term2str t1'; terms2str asm;
1.76 -"(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))";
1.77 -"[]";
1.78 -val SOME (t1',asm)= cancel_p_ thy t1;
1.79 -term2str t1'; terms2str asm;
1.80 -"(3 + 3 * x) / 2";
1.81 -"[\"1 + 1 * x ~= 0\"]";
1.82 +val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.83 +val SOME (t', asm) = factout_p_ thy t;
1.84 +if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]"
1.85 +then () else error "factout_p_ 1 changed";
1.86 +val SOME (t', asm) = cancel_p_ thy t;
1.87 +if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]"
1.88 +then () else error "cancel_p_ 1 changed";
1.89
1.90 -val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
1.91 -val SOME (t',asm)= cancel_ thy t;
1.92 -term2str t'; terms2str asm;
1.93 -"(3 - 3 * x) / 2";
1.94 -"[\"-1 + x ~= 0\"]";
1.95 -val SOME (t',asm)= factout_ thy t;
1.96 -term2str t'; terms2str asm;
1.97 -"(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))";
1.98 -"[]";
1.99 +val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
1.100 +val SOME (t', asm) = factout_(*p_*) thy t;
1.101 +if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]"
1.102 +then () else error "factout_ 2 changed";
1.103 +val SOME (t', asm) = cancel_(*p_*) thy t;
1.104 +if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]"
1.105 +then () else error "cancel_ 2 changed";
1.106
1.107 -val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.108 -val SOME (t',asm) = add_fraction_p_ thy t;
1.109 -term2str t'; terms2str asm;
1.110 -"(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)";
1.111 -"[]";
1.112 -val SOME (t',asm) = common_nominator_p_ thy t;
1.113 -term2str t'; terms2str asm;
1.114 -"(-1 + 1 * x) * (-1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x)) +\n(1 + 1 * x) * (1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x))";
1.115 -"[]";
1.116 +val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.117 +val SOME (t', asm) = add_fraction_p_ thy t;
1.118 +if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
1.119 +then () else error "add_fraction_p_ 3 changed";
1.120 +val SOME (t', asm) = common_nominator_p_ thy t;
1.121 +if term2str t' =
1.122 + "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
1.123 + andalso terms2str asm = "[]"
1.124 +then () else error "common_nominator_p_ 3 changed";
1.125
1.126 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
1.127 -val SOME (t',asm) = add_fraction_ thy t;
1.128 -term2str t'; terms2str asm;
1.129 -"(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)";
1.130 -"[]";
1.131 -val SOME (t',asm) = common_nominator_ thy t;
1.132 -term2str t'; terms2str asm;
1.133 -"(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))";
1.134 -"[]";
1.135 +val SOME (t', asm) = add_fraction_ thy t;
1.136 +if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
1.137 +then () else error "factout_ 4 changed";
1.138 +val SOME (t', asm) = common_nominator_ thy t;
1.139 +if term2str t' =
1.140 + "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
1.141 + andalso terms2str asm = "[]"
1.142 +then () else error "cancel_ 4 changed";
1.143
1.144 -val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
1.145 -val SOME (t',asm) = common_nominator_p_ thy t;
1.146 -term2str t'; terms2str asm;
1.147 -"1 * (1 + -2 * x + 1 * x ^^^ 2) /\n((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n(1 * (-1 + 1 * x ^^^ 2) /\n ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n (1 * (-2 + 2 * x) / ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n 1 * (#";
1.148 -"[]";
1.149 -val SOME (t',asm) = add_fraction_p_ thy t;
1.150 -term2str t'; terms2str asm;
1.151 -"1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
1.152 -"[\"1 + 1 * x ~= 0\"]";
1.153 -val SOME(t',asm) = norm_rational_ thy t;
1.154 -term2str t'; terms2str asm;
1.155 -"1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
1.156 -"[\"1 + 1 * x ~= 0\"]";
1.157 +val t = str2term
1.158 + "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
1.159 +val SOME (t', asm) = add_fraction_p_ thy t;
1.160 +if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
1.161 +then () else error "add_fraction_p_ 5 changed";
1.162 +val SOME (t', asm) = norm_rational_ thy t;
1.163 +if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
1.164 +then () else error "norm_rational_ 5 changed";
1.165 +
1.166 +
1.167
1.168 val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))";
1.169 val SOME (t3',_) = common_nominator_ thy t3;
1.170 @@ -578,7 +568,7 @@
1.171 else error "rational.sml lex-ord 1";
1.172 if term2str t'' = "(-1 - y - x) / (y - x)" then ()
1.173 else error "rational.sml lex-ord 2";
1.174 -(*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*)
1.175 +(*WN.16.10.02 WN070905 lexicographische Ordnung erhalten *)
1.176
1.177
1.178 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
1.179 @@ -2387,4 +2377,5 @@
1.180 "--- 12 ---";
1.181 "...both are to be considered after common_nominator_p_ is improved";
1.182 --------------------------------------------------------------------------------------/*)
1.183 +============ inhibit exn WN130824 TODO ======================================================*)
1.184