wneuper/isa: test/Tools/isac/Knowledge/atools.sml@06883b595617

     1 (* tests on Atools.thy and Atools.ML

     2    author: Walther Neuper

     3    050814, 08:51

     4    (c) due to copyright terms

     6 use"../smltest/IsacKnowledge/atools.sml";

     7 use"atools.sml";

     8 *)

    10 print_depth 5;

    11 "--------------------------------------------------------";

    12 "table of contents --------------------------------------";

    13 "--------------------------------------------------------";

    14 "----------- occurs_in ----------------------------------";

    15 "----------- argument_of --------------------------------";

    16 "----------- sameFunId ----------------------------------";

    17 "----------- filter_sameFunId ---------------------------";

    18 "----------- boollist2sum -------------------------------";

    19 "----------- Matthias Goldgruber 2003 rewrite orders ----";

    20 (*"----------- introduction by MG 2003 --------------------";*)

    21 "----------- fun eval_binop -----------------------------";

    22 "--------------------------------------------------------";

    25 val thy = @{theory "Atools"};

    27 "----------- occurs_in -------------------------------------------";

    28 "----------- occurs_in -------------------------------------------";

    29 "----------- occurs_in -------------------------------------------";

    30 (*=========================================================================*)

    31 fun str2t str = (term_of o the o (parse thy)) str;

    32 fun term2s t = term_to_string''' thy t;

    33 (*=========================================================================*)

    35 val t = str2t "x";

    36 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";

    38 val t = str2term "x occurs_in x";

    39 val SOME (str, t') = eval_occurs_in 0 "Atools.occurs'_in" t 0;

    40 if term2str t' = "x occurs_in x = True" then ()

    41 else error "x occurs_in x = True ..changed";

    43 "------- some_occur_in";

    44 some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");

    45 val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \

    46 		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

    47 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;

    48 if term2str t' =

    49    "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()

    50 else error "atools.sml: some_occur_in true";

    52 val t = str2t "some_of [c_3, c_4] occur_in \

    53 		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

    54 val SOME (str,t') = eval_some_occur_in 0 "Atools.some'_occur'_in" t 0;

    55 if term2str t' =

    56    "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()

    57 else error "atools.sml: some_occur_in false";

    59 "----------- argument_of -----------------------------------------";

    60 "----------- argument_of -----------------------------------------";

    61 "----------- argument_of -----------------------------------------";

    62 val t = str2term "argument_in (M_b x)";

    63 val SOME (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;

    64 if term2str t' = "(argument_in M_b x) = x" then ()

    65 else error "atools.sml:(argument_in M_b x) = x  ???";

    67 "----------- sameFunId -------------------------------------------";

    68 "----------- sameFunId -------------------------------------------";

    69 "----------- sameFunId -------------------------------------------";

    70 val t = str2t "M_b L"; atomty t;

    71 val t as f1 $ _ = str2t "M_b L";

    72 val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2t "M_b x = c + L*x";

    73 f1 = f2 (*true*);

    74 val (p as Const ("Atools.sameFunId",_) $

    75 			(f1 $ _) $

    76 			(Const ("HOL.eq", _) $ (f2 $ _) $ _)) =

    77     str2t "sameFunId (M_b L) (M_b x = c + L*x)";

    78 f1 = f2 (*true*);

    79 eval_sameFunId "" "Atools.sameFunId"

    80 		 (str2t "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);

    81 eval_sameFunId "" "Atools.sameFunId"

    82 		 (str2t "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);

    83 eval_sameFunId "" "Atools.sameFunId"

    84 		 (str2t "sameFunId (M_b L) (  y x = c + L*x)")""(*false*);

    85 eval_sameFunId "" "Atools.sameFunId"

    86 		 (str2t "sameFunId (  y L) (M_b x = c + L*x)")""(*false*);

    87 eval_sameFunId "" "Atools.sameFunId"

    88 		 (str2t "sameFunId (  y L) (  y x = c + L*x)")""(*true*);

    90 "----------- filter_sameFunId ------------------------------------";

    91 "----------- filter_sameFunId ------------------------------------";

    92 "----------- filter_sameFunId ------------------------------------";

    93 val flhs as (fid $ _) = str2t "y' L";

    94 val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";

    95 val (p as Const ("Atools.filter'_sameFunId",_) $ (fid $ _) $ fs) =

    96     str2t "filter_sameFunId (y' L) \

    97 	     \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";

    98 val SOME (str, es) = eval_filter_sameFunId "" "Atools.filter'_sameFunId" p "";

    99 if term2str es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n                        y x = c + L * x]) =\n[y' x = c + L * x]" then ()

   100 else error "atools.slm diff.behav. in filter_sameFunId";

   103 "----------- boollist2sum ----------------------------------------";

   104 "----------- boollist2sum ----------------------------------------";

   105 "----------- boollist2sum ----------------------------------------";

   106 fun lhs (Const ("HOL.eq",_) $ l $ _) = l

   107   | lhs t = error("lhs called with (" ^ term2str t ^ ")");

   108 "-----------^^^redefined due to overwritten identifier -----------";

   109 val u_ = str2t "[]";

   110 val u_ = str2t "[b1 = k - 2*q]";

   111 val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

   112 val ut_ = isalist2list u_;

   113 val sum_ = map lhs ut_;

   114 val t = list2sum sum_;

   115 term2str t;

   117 val t = str2t

   118        "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

   120 val p as Const ("Atools.boollist2sum", _) $ (Const ("List.list.Cons", _) $

   121 						   _ $ _) = t;

   124 val SOME (str, pred) = eval_boollist2sum "" "Atools.boollist2sum" t "";

   125 if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then ()

   126 else error "atools.sml diff.behav. in eval_boollist2sum";

   128 trace_rewrite := false;

   129 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls

   130 		      [Calc ("Atools.boollist2sum", eval_boollist2sum "")];

   131 val t = str2t

   132        "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

   133 case rewrite_set_ thy false srls_ t of SOME _ => ()

   134 | _ => error "atools.sml diff.rewrite boollist2sum";

   135 trace_rewrite:=false;

   138 "----------- Matthias Goldgruber 2003 rewrite orders ----";

   139 "----------- Matthias Goldgruber 2003 rewrite orders ----";

   140 "----------- Matthias Goldgruber 2003 rewrite orders ----";

   141 (* MK die ersten Tests *)

   142   val substa = [(e_term, (term_of o the o (parse thy)) "a")];

   143   val substb = [(e_term, (term_of o the o (parse thy)) "b")];

   144   val substx = [(e_term, (term_of o the o (parse thy)) "x")];

   146   val x1 = (term_of o the o (parse thy)) "a + b + x";

   147   val x2 = (term_of o the o (parse thy)) "a + x + b";

   148   val x3 = (term_of o the o (parse thy)) "a + x + b";

   149   val x4 = (term_of o the o (parse thy)) "x + a + b";

   151 if ord_make_polynomial_in true thy substx (x1,x2) = true(*LESS *) then ()

   152 else error "termorder.sml diff.behav ord_make_polynomial_in #1";

   154 if ord_make_polynomial_in true thy substa (x1,x2) = true(*LESS *) then ()

   155 else error "termorder.sml diff.behav ord_make_polynomial_in #2";

   157 if ord_make_polynomial_in true thy substb (x1,x2) = false(*GREATER*) then ()

   158 else error "termorder.sml diff.behav ord_make_polynomial_in #3";

   160   val aa = (term_of o the o (parse thy)) "-1 * a * x";

   161   val bb = (term_of o the o (parse thy)) "x^^^3";

   162   ord_make_polynomial_in true thy substx (aa, bb);

   163   true; (* => LESS *)

   165   val aa = (term_of o the o (parse thy)) "-1 * a * x";

   166   val bb = (term_of o the o (parse thy)) "x^^^3";

   167   ord_make_polynomial_in true thy substa (aa, bb);

   168   false; (* => GREATER *)

   170 (* und nach dem Re-engineering der Termorders in den 'rulesets'

   171    kannst Du die 'gr"osste' Variable frei w"ahlen: *)

   172   val bdv= (term_of o the o (parse thy)) "bdv";

   173   val x  = (term_of o the o (parse thy)) "x";

   174   val a  = (term_of o the o (parse thy)) "a";

   175   val b  = (term_of o the o (parse thy)) "b";

   176 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;

   177 if term2str t' = "b + x + a" then ()

   178 else error "termorder.sml diff.behav ord_make_polynomial_in #11";

   180 val NONE = rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;

   182 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;

   183 if term2str t' = "a + b + x" then ()

   184 else error "termorder.sml diff.behav ord_make_polynomial_in #13";

   186   val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";

   187   val ppp  = (term_of o the o (parse thy)) ppp';

   188 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;

   189 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()

   190 else error "termorder.sml diff.behav ord_make_polynomial_in #14";

   192 val SOME (t',_) = rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp';

   193 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then ()

   194 else error "termorder.sml diff.behav ord_make_polynomial_in #15";

   196   val ttt' = "(3*x + 5)/18";

   197   val ttt = (term_of o the o (parse thy)) ttt';

   198 val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;

   199 if term2str uuu = "(5 + 3 * x) / 18" then ()

   200 else error "termorder.sml diff.behav ord_make_polynomial_in #16a";

   202 (*============ inhibit exn WN120316 ==============================================

   203 val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;

   204 if term2str uuu = "(5 + 3 * x) / 18" then ()

   205 else error "termorder.sml diff.behav ord_make_polynomial_in #16b";

   206 ============ inhibit exn WN120316 ==============================================*)

   209 "----------- introduction by MG 2003 --------------------";

   210 "----------- introduction by MG 2003 --------------------";

   211 "----------- introduction by MG 2003 --------------------";

   212 (*##################################################################################

   213 -----------28.2.03: war nicht upgedatet und ausgeklammert in ROOT.ML-->Test_Isac.thy

   215   (*Aufgabe zum Einstieg in die Arbeit...*)

   216   val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";

   217   (*ein 'ruleset' aus Poly.ML wird angewandt...*)

   218   val SOME (t,_) = rewrite_set_ thy Poly_erls false make_polynomial t;

   219   term2str t;

   220   "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";

   221   val SOME (t,_) =

   222       rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;

   223   term2str t;

   224   "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";

   225 (* bei Verwendung von "size_of-term" nach MG :*)

   226 (*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0"  !!! *)

   228   (*wir holen 'a' wieder aus der Klammerung heraus...*)

   229   val SOME (t,_) = rewrite_set_ thy Poly_erls false discard_parentheses t;

   230   term2str t;

   231    "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";

   232 (* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)

   234   val SOME (t,_) =

   235       rewrite_set_inst_ thy Poly_erls false [("bdv","a")] make_polynomial_in t;

   236   term2str t;

   237   "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";

   238   (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben

   239   "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)

   241   (*das rewriting l"asst sich beobachten mit

   242 trace_rewrite := false;

   243   *)

   245 "------15.11.02 --------------------------";

   246   val t = (term_of o the o (parse thy)) "1 + a * x + b * x";

   247   val bdv = (term_of o the o (parse thy)) "bdv";

   248   val a = (term_of o the o (parse thy)) "a";

   250 trace_rewrite := false;

   251  (* Anwenden einer Regelmenge aus Termorder.ML: *)

   252  val SOME (t,_) =

   253      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

   254  term2str t;

   255  val SOME (t,_) =

   256      rewrite_set_ thy false discard_parentheses t;

   257  term2str t;

   258 "1 + b * x + x * a";

   260  val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";

   261  val SOME (t,_) =

   262      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

   263  term2str t;

   264  val SOME (t,_) =

   265      rewrite_set_ thy false discard_parentheses t;

   266  term2str t;

   267 "1 + (x + b * x) * a + a ^^^ 2";

   269  val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";

   270  val SOME (t,_) =

   271      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

   272  term2str t;

   273  val SOME (t,_) =

   274      rewrite_set_ thy false discard_parentheses t;

   275  term2str t;

   276 "1 + b * a + (7 + x) * a ^^^ 2";

   278 (* MG2003

   279  Atools.thy       grundlegende Algebra

   280  Poly.thy         Polynome

   281  Rational.thy     Br"uche

   282  Root.thy         Wurzeln

   283  RootRat.thy      Wurzen + Br"uche

   284  Termorder.thy    BITTE NUR HIERHER SCHREIBEN (...WN03)

   286  get_thm Termorder.thy "bdv_n_collect";

   287  get_thm (theory "Isac") "bdv_n_collect";

   288 *)

   289  val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";

   290  val SOME (t,_) =

   291      rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

   292  term2str t;

   293  val SOME (t,_) =

   294      rewrite_set_ thy false discard_parentheses t;

   295  term2str t;

   296 "(7 + x) * a ^^^ 2";

   298  val t = (term_of o the o (parse Termorder.thy)) "Pi";

   300  val t = (term_of o the o (parseold thy)) "7";

   301 ##################################################################################*)

   303 "----------- fun eval_binop -----------------------------";

   304 "----------- fun eval_binop -----------------------------";

   305 "----------- fun eval_binop -----------------------------";

   306 val (op_, ef) = the (assoc (calclist, "TIMES"));

   307 val t = (term_of o the o (parse thy)) "2 * 3";

   308 (*val SOME (thmid,t') = *)get_pair thy op_ ef t;

   309 ;

   310 "~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =

   311   (thy, op_, ef, t);

   312 op_ = op0 = true;

   313 ef op_ t thy

   314 ;

   315 "~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string),

   316       (t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)

   317 val (SOME n1, SOME n2) = (numeral t1, numeral t2)

   318           val (_, _, Trange) = dest_binop_typ t0;

   319           val res = calc op0 n1 n2;

   320           val rhs = term_of_float Trange res;

   321           val prop = Trueprop $ (mk_equality (t, rhs));

   322 val SOME (thmid, tm) = SOME ("#: " ^ term2str prop, prop)

   323 ;

   324 if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()

   325 else error "eval_binop changed"

   326 ;

   327 val SOME (thmid, tm) = eval_binop "#mult_"  op_ t thy;

   328 if thmid = "#: 2 * 3 = 6" andalso term2str prop = "2 * 3 = 6" then ()

   329 else error "eval_binop changed 2"

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 31 Jul 2014 14:32:05 +0200
changeset 55487	06883b595617
parent 52101	c3f399ce32af
child 55490	a8f80537db69
permissions	-rw-r--r--