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

     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 (*default_print_depth 5;*)

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

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

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

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

    15 "----------- fun occurs_in ---------------------------------------------------------------------";

    16 "----------- argument_of --------------------------------";

    17 "----------- sameFunId ----------------------------------";

    18 "----------- filter_sameFunId ---------------------------";

    19 "----------- boollist2sum -------------------------------";

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

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

    22 "----------- fun eval_binop -----------------------------";

    23 "--------------------------------------------------------";

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

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

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

    30 "----------- occurs_in -------------------------------------------";

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

    32 fun str2t str = (Thm.term_of o the o (parse thy)) str;

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

    34 (*=========================================================================*)

    36 val t = str2t "x";

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

    39 val t = str2term "x occurs_in x";

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

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

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

    44 "------- some_occur_in";

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

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

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

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

    49 if term2str t' =

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

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

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

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

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

    56 if term2str t' =

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

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

    60 "----------- fun occurs_in ---------------------------------------------------------------------";

    61 "----------- fun occurs_in ---------------------------------------------------------------------";

    62 "----------- fun occurs_in ---------------------------------------------------------------------";

    63 val v = (Thm.term_of o the o (parse thy)) "x";

    64 val t = (Thm.term_of o the o (parse thy)) "1";

    65 if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();

    67 val v = (Thm.term_of o the o (parse thy)) "AA";

    68 val t = (Thm.term_of o the o (parse thy)) "1";

    69 if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();

    71 (*----------*)

    72 val v = (Thm.term_of o the o (parse thy)) "x";

    73 val t = (Thm.term_of o the o (parse thy)) "a*b+c";

    74 if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();

    76 val v = (Thm.term_of o the o (parse thy)) "AA";

    77 val t = (Thm.term_of o the o (parse thy)) "a*b+c";

    78 if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();

    80 (*----------*)

    81 val v = (Thm.term_of o the o (parse thy)) "x";

    82 val t = (Thm.term_of o the o (parse thy)) "a*x+c";

    83 if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";

    85 val v = (Thm.term_of o the o (parse thy)) "AA";

    86 val t = (Thm.term_of o the o (parse thy)) "a*AA+c";

    87 if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";

    89 (*----------*)

    90 val v = (Thm.term_of o the o (parse thy)) "x";

    91 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";

    92 if occurs_in v t then () else error "factor_right_deg (a*b+c)*x^^^7) x ..changed";

    94 val v = (Thm.term_of o the o (parse thy)) "AA";

    95 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";

    96 if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA^^^7) AA ..changed";

    98 (*----------*)

    99 val v = (Thm.term_of o the o (parse thy)) "x";

   100 val t = (Thm.term_of o the o (parse thy)) "x^^^7";

   101 if occurs_in v t then () else error "factor_right_deg (x^^^7) x ..changed";

   103 val v = (Thm.term_of o the o (parse thy)) "AA";

   104 val t = (Thm.term_of o the o (parse thy)) "AA^^^7";

   105 if occurs_in v t then () else error "factor_right_deg (AA^^^7) AA ..changed";

   107 (*----------*)

   108 val v = (Thm.term_of o the o (parse thy)) "x";

   109 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";

   110 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";

   112 val v = (Thm.term_of o the o (parse thy)) "AA";

   113 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";

   114 if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";

   116 (*----------*)

   117 val v = (Thm.term_of o the o (parse thy)) "x";

   118 val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";

   119 if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";

   121 val v = (Thm.term_of o the o (parse thy)) "AA";

   122 val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";

   123 if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";

   125 (*----------*)

   126 val v = (Thm.term_of o the o (parse thy)) "x";

   127 val t = (Thm.term_of o the o (parse thy)) "x";

   128 if occurs_in v t then () else error "factor_right_deg (x) x ..changed";

   130 val v = (Thm.term_of o the o (parse thy)) "AA";

   131 val t = (Thm.term_of o the o (parse thy)) "AA";

   132 if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";

   134 (*----------*)

   135 val v = (Thm.term_of o the o (parse thy)) "x";

   136 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";

   137 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";

   139 val v = (Thm.term_of o the o (parse thy)) "AA";

   140 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";

   141 if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";

   143 "----------- argument_of -----------------------------------------";

   144 "----------- argument_of -----------------------------------------";

   145 "----------- argument_of -----------------------------------------";

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

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

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

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

   151 "----------- sameFunId -------------------------------------------";

   152 "----------- sameFunId -------------------------------------------";

   153 "----------- sameFunId -------------------------------------------";

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

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

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

   157 f1 = f2 (*true*);

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

   159 			(f1 $ _) $

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

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

   162 f1 = f2 (*true*);

   163 eval_sameFunId "" "Atools.sameFunId"

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

   165 eval_sameFunId "" "Atools.sameFunId"

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

   167 eval_sameFunId "" "Atools.sameFunId"

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

   169 eval_sameFunId "" "Atools.sameFunId"

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

   171 eval_sameFunId "" "Atools.sameFunId"

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

   174 "----------- filter_sameFunId ------------------------------------";

   175 "----------- filter_sameFunId ------------------------------------";

   176 "----------- filter_sameFunId ------------------------------------";

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

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

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

   180     str2t "filter_sameFunId (y' L) \

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

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

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

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

   187 "----------- boollist2sum ----------------------------------------";

   188 "----------- boollist2sum ----------------------------------------";

   189 "----------- boollist2sum ----------------------------------------";

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

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

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

   193 val u_ = str2t "[]";

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

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

   196 val ut_ = isalist2list u_;

   197 val sum_ = map lhs ut_;

   198 val t = list2sum sum_;

   199 term2str t;

   201 val t = str2t

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

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

   205 						   _ $ _) = t;

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

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

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

   212 trace_rewrite := false;

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

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

   215 val t = str2t

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

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

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

   219 trace_rewrite:=false;

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

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

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

   225 (* MK die ersten Tests *)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   245   val bb = (Thm.term_of o the o (parse thy)) "x^^^3";

   246   ord_make_polynomial_in true thy substx (aa, bb);

   247   true; (* => LESS *)

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

   250   val bb = (Thm.term_of o the o (parse thy)) "x^^^3";

   251   ord_make_polynomial_in true thy substa (aa, bb);

   252   false; (* => GREATER *)

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

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

   256   val bdv= (Thm.term_of o the o (parse thy)) "''bdv''";

   257   val x  = (Thm.term_of o the o (parse thy)) "x";

   258   val a  = (Thm.term_of o the o (parse thy)) "a";

   259   val b  = (Thm.term_of o the o (parse thy)) "b";

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

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

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

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

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

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

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

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

   271   val ppp  = (Thm.term_of o the o (parse thy)) ppp';

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

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

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

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

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

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

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

   281   val ttt = (Thm.term_of o the o (parse thy)) ttt';

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

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

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

   286 (*============ inhibit exn WN120316 ==============================================

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

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

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

   290 ============ inhibit exn WN120316 ==============================================*)

   293 "----------- introduction by MG 2003 --------------------";

   294 "----------- introduction by MG 2003 --------------------";

   295 "----------- introduction by MG 2003 --------------------";

   296 (*##################################################################################

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

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

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

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

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

   303   term2str t;

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

   305   val SOME (t,_) =

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

   307   term2str t;

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

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

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

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

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

   314   term2str t;

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

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

   318   val SOME (t,_) =

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

   320   term2str t;

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

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

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

   325   (*das rewriting l"asst sich beobachten mit

   326 trace_rewrite := false;

   327   *)

   329 "------15.11.02 --------------------------";

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

   331   val bdv = (Thm.term_of o the o (parse thy)) "bdv";

   332   val a = (Thm.term_of o the o (parse thy)) "a";

   334 trace_rewrite := false;

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

   336  val SOME (t,_) =

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

   338  term2str t;

   339  val SOME (t,_) =

   340      rewrite_set_ thy false discard_parentheses t;

   341  term2str t;

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

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

   345  val SOME (t,_) =

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

   347  term2str t;

   348  val SOME (t,_) =

   349      rewrite_set_ thy false discard_parentheses t;

   350  term2str t;

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

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

   354  val SOME (t,_) =

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

   356  term2str t;

   357  val SOME (t,_) =

   358      rewrite_set_ thy false discard_parentheses t;

   359  term2str t;

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

   362 (* MG2003

   363  Atools.thy       grundlegende Algebra

   364  Poly.thy         Polynome

   365  Rational.thy     Br"uche

   366  Root.thy         Wurzeln

   367  RootRat.thy      Wurzen + Br"uche

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

   370  get_thm Termorder.thy "bdv_n_collect";

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

   372 *)

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

   374  val SOME (t,_) =

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

   376  term2str t;

   377  val SOME (t,_) =

   378      rewrite_set_ thy false discard_parentheses t;

   379  term2str t;

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

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

   384  val t = (Thm.term_of o the o (parseold thy)) "7";

   385 ##################################################################################*)

   387 "----------- fun eval_binop -----------------------------";

   388 "----------- fun eval_binop -----------------------------";

   389 "----------- fun eval_binop -----------------------------";

   390 val (op_, ef) = the (assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));

   391 val t = (Thm.term_of o the o (parse thy)) "2 * 3";

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

   393 ;

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

   395   (thy, op_, ef, t);

   396 op_ = op0 = true;

   397 ef op_ t thy

   398 ;

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

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

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

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

   403           val res = calcul op0 n1 n2;

   404           val rhs = term_of_float Trange res;

   405           val prop = HOLogic.Trueprop $ (mk_equality (t, rhs));

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

   407 ;

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

   409 else error "eval_binop changed"

   410 ;

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

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

   413 else error "eval_binop changed 2"

author	Walther Neuper <wneuper@ist.tugraz.at>
	Wed, 03 Jul 2019 15:09:16 +0200
changeset 59562	d50fe358f04a
parent 59528	8c7dcea539c4
child 59592	99c8d2ff63eb
permissions	-rw-r--r--