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

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

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

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

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

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

    29 (*=========================================================================*)

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

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

    32 (*=========================================================================*)

    34 val t = str2t "x";

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

    37 val t = str2term "x occurs_in x";

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

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

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

    42 "------- some_occur_in";

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

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

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

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

    47 if term2str t' =

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

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

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

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

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

    54 if term2str t' =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    72 f1 = f2 (*true*);

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

    74 			(f1 $ _) $

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

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

    77 f1 = f2 (*true*);

    78 eval_sameFunId "" "Atools.sameFunId"

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

    80 eval_sameFunId "" "Atools.sameFunId"

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

    82 eval_sameFunId "" "Atools.sameFunId"

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

    84 eval_sameFunId "" "Atools.sameFunId"

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

    86 eval_sameFunId "" "Atools.sameFunId"

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

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

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

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

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

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

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

    95     str2t "filter_sameFunId (y' L) \

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

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

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

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

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

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

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

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

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

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

   108 val u_ = str2t "[]";

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

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

   111 val ut_ = isalist2list u_;

   112 val sum_ = map lhs ut_;

   113 val t = list2sum sum_;

   114 term2str t;

   116 val t = str2t

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

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

   120 						   _ $ _) = t;

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

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

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

   127 trace_rewrite := false;

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

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

   130 val t = str2t

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

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

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

   134 trace_rewrite:=false;

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

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

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

   140 (* MK die ersten Tests *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   161   ord_make_polynomial_in true thy substx (aa, bb);

   162   true; (* => LESS *)

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

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

   166   ord_make_polynomial_in true thy substa (aa, bb);

   167   false; (* => GREATER *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   201 (*============ inhibit exn WN120316 ==============================================

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

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

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

   205 ============ inhibit exn WN120316 ==============================================*)

   208 "----------- introduction by MG 2003 --------------------";

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

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

   211 (*##################################################################################

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

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

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

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

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

   218   term2str t;

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

   220   val SOME (t,_) =

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

   222   term2str t;

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

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

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

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

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

   229   term2str t;

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

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

   233   val SOME (t,_) =

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

   235   term2str t;

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

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

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

   240   (*das rewriting l"asst sich beobachten mit

   241 trace_rewrite := false;

   242   *)

   244 "------15.11.02 --------------------------";

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

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

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

   249 trace_rewrite := false;

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

   251  val SOME (t,_) =

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

   253  term2str t;

   254  val SOME (t,_) =

   255      rewrite_set_ thy false discard_parentheses t;

   256  term2str t;

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

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

   260  val SOME (t,_) =

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

   262  term2str t;

   263  val SOME (t,_) =

   264      rewrite_set_ thy false discard_parentheses t;

   265  term2str t;

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

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

   269  val SOME (t,_) =

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

   271  term2str t;

   272  val SOME (t,_) =

   273      rewrite_set_ thy false discard_parentheses t;

   274  term2str t;

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

   277 (* MG2003

   278  Atools.thy       grundlegende Algebra

   279  Poly.thy         Polynome

   280  Rational.thy     Br"uche

   281  Root.thy         Wurzeln

   282  RootRat.thy      Wurzen + Br"uche

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

   285  get_thm Termorder.thy "bdv_n_collect";

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

   287 *)

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

   289  val SOME (t,_) =

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

   291  term2str t;

   292  val SOME (t,_) =

   293      rewrite_set_ thy false discard_parentheses t;

   294  term2str t;

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

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

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

   300 ##################################################################################*)

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 02 Sep 2013 16:16:08 +0200
changeset 52101	c3f399ce32af
parent 52070	77138c64f4f6
child 55487	06883b595617
permissions	-rw-r--r--