wneuper/isa: test/Tools/isac/Knowledge/atools.sml@04d3f0133827

     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 "--------------------------------------------------------";

    11 "table of contents --------------------------------------";

    12 "--------------------------------------------------------";

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

    14 "----------- argument_of --------------------------------";

    15 "----------- sameFunId ----------------------------------";

    16 "----------- filter_sameFunId ---------------------------";

    17 "----------- boollist2sum -------------------------------";

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

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

    20 "--------------------------------------------------------";

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

    25 "----------- occurs_in -------------------------------------------";

    26 "----------- occurs_in -------------------------------------------";

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

    28 (*=========================================================================*)

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

    30 fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t;

    31 (*=========================================================================*)

    33 val t = str2t "x";

    34 if occurs_in t t then "OK" else error "atools.sml: occurs_in x x -> f";

    36 val t = str2t "x occurs_in x";

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

    38 if (term2s t') = "x occurs_in x = True" then ()

    39 else error "atools.sml: x occurs_in x = True ???";

    41 "------- some_occur_in";

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

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

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

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

    46 if term2str t' =

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

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

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

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

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

    53 if term2str t' =

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

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

    57 "----------- argument_of -----------------------------------------";

    58 "----------- argument_of -----------------------------------------";

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

    60 val t = str2t "argument_in (M_b x)";

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

    62 if term2s t' = "(argument_in M_b x) = x" then ()

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

    65 "----------- sameFunId -------------------------------------------";

    66 "----------- sameFunId -------------------------------------------";

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

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

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

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

    71 f1 = f2 (*true*);

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

    73 			(f1 $ _) $

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

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

    76 f1 = f2 (*true*);

    77 eval_sameFunId "" "Atools.sameFunId"

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

    79 eval_sameFunId "" "Atools.sameFunId"

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

    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 (  y L) (M_b x = c + L*x)")""(*false*);

    85 eval_sameFunId "" "Atools.sameFunId"

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

    88 "----------- filter_sameFunId ------------------------------------";

    89 "----------- filter_sameFunId ------------------------------------";

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

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

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

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

    94     str2t "filter_sameFunId (y' L) \

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

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

    97 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 ()

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

   101 "----------- boollist2sum ----------------------------------------";

   102 "----------- boollist2sum ----------------------------------------";

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

   104 val u_ = str2t "[]";

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

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

   107 val ut_ = isalist2list u_;

   108 val sum_ = map lhs ut_;

   109 val t = list2sum sum_;

   110 term2str t;

   112 val t = str2t

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

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

   116 						   _ $ _) = t;

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

   120 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 ()

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

   123 trace_rewrite:=true;

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

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

   126 val t = str2t

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

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

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

   130 trace_rewrite:=false;

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

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

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

   136 (* MK die ersten Tests *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   157   ord_make_polynomial_in true thy substx (aa, bb);

   158   true; (* => LESS *)

   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 substa (aa, bb);

   163   false; (* => GREATER *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   197 (*============ inhibit exn WN120316 ==============================================

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

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

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

   201 ============ inhibit exn WN120316 ==============================================*)

   204 "----------- introduction by MG 2003 --------------------";

   205 "----------- introduction by MG 2003 --------------------";

   206 "----------- introduction by MG 2003 --------------------";

   207 (*##################################################################################

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

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

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

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

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

   214   term2str t;

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

   216   val SOME (t,_) =

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

   218   term2str t;

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

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

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

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

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

   225   term2str t;

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

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

   229   val SOME (t,_) =

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

   231   term2str t;

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

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

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

   236   (*das rewriting l"asst sich beobachten mit

   237   trace_rewrite:=true;

   238   *)

   240 "------15.11.02 --------------------------";

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

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

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

   245  trace_rewrite:=true;

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

   247  val SOME (t,_) =

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

   249  term2str t;

   250  val SOME (t,_) =

   251      rewrite_set_ thy false discard_parentheses t;

   252  term2str t;

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

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

   256  val SOME (t,_) =

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

   258  term2str t;

   259  val SOME (t,_) =

   260      rewrite_set_ thy false discard_parentheses t;

   261  term2str t;

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

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

   265  val SOME (t,_) =

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

   267  term2str t;

   268  val SOME (t,_) =

   269      rewrite_set_ thy false discard_parentheses t;

   270  term2str t;

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

   273 (* MG2003

   274  Atools.thy       grundlegende Algebra

   275  Poly.thy         Polynome

   276  Rational.thy     Br"uche

   277  Root.thy         Wurzeln

   278  RootRat.thy      Wurzen + Br"uche

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

   281  get_thm Termorder.thy "bdv_n_collect";

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

   283 *)

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

   285  val SOME (t,_) =

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

   287  term2str t;

   288  val SOME (t,_) =

   289      rewrite_set_ thy false discard_parentheses t;

   290  term2str t;

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

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

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

   296 ##################################################################################*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 19 Mar 2012 09:48:03 +0100
changeset 42398	04d3f0133827
parent 42397	4f1cc40522c4
child 48895	35751d90365e
permissions	-rw-r--r--