wneuper/isa: src/Tools/isac/Knowledge/Test.thy@4022d670753c

     1 (* some tests are based on specficially simple scripts etc.

     2    Author: Walther Neuper 2003

     3    (c) due to copyright terms

     4 *)

     6 theory Test imports Atools + Rational + Root + Poly +

     8 consts

    10 (*"cancel":: [real, real] => real    (infixl "'/'/'/" 70) ...divide 2002*)

    12   Expand'_binomtest

    13              :: "['y,

    14 		    'y] => 'y"

    15                ("((Script Expand'_binomtest (_ =))//

    16                    (_))" 9)

    18   Solve'_univar'_err

    19              :: "[bool,real,bool,

    20 		    bool list] => bool list"

    21                ("((Script Solve'_univar'_err (_ _ _ =))//

    22                    (_))" 9)

    24   Solve'_linear

    25              :: "[bool,real,

    26 		    bool list] => bool list"

    27                ("((Script Solve'_linear (_ _ =))//

    28                    (_))" 9)

    30 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)

    32   "is'_root'_free" :: 'a => bool           ("is'_root'_free _" 10)

    33   "contains'_root" :: 'a => bool           ("contains'_root _" 10)

    35   Solve'_root'_equation

    36              :: "[bool,real,

    37 		    bool list] => bool list"

    38                ("((Script Solve'_root'_equation (_ _ =))//

    39                    (_))" 9)

    41   Solve'_plain'_square

    42              :: "[bool,real,

    43 		    bool list] => bool list"

    44                ("((Script Solve'_plain'_square (_ _ =))//

    45                    (_))" 9)

    47   Norm'_univar'_equation

    48              :: "[bool,real,

    49 		    bool] => bool"

    50                ("((Script Norm'_univar'_equation (_ _ =))//

    51                    (_))" 9)

    53   STest'_simplify

    54              :: "['z,

    55 		    'z] => 'z"

    56                ("((Script STest'_simplify (_ =))//

    57                    (_))" 9)

    59 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)

    61 axioms (*TODO: prove as theorems*)

    63   radd_mult_distrib2      "(k::real) * (m + n) = k * m + k * n"

    64   rdistr_right_assoc      "(k::real) + l * n + m * n = k + (l + m) * n"

    65   rdistr_right_assoc_p    "l * n + (m * n + (k::real)) = (l + m) * n + k"

    66   rdistr_div_right        "((k::real) + l) / n = k / n + l / n"

    67   rcollect_right

    68           "[| l is_const; m is_const |] ==> (l::real)*n + m*n = (l + m) * n"

    69   rcollect_one_left

    70           "m is_const ==> (n::real) + m * n = (1 + m) * n"

    71   rcollect_one_left_assoc

    72           "m is_const ==> (k::real) + n + m * n = k + (1 + m) * n"

    73   rcollect_one_left_assoc_p

    74           "m is_const ==> n + (m * n + (k::real)) = (1 + m) * n + k"

    76   rtwo_of_the_same        "a + a = 2 * a"

    77   rtwo_of_the_same_assoc  "(x + a) + a = x + 2 * a"

    78   rtwo_of_the_same_assoc_p"a + (a + x) = 2 * a + x"

    80   rcancel_den             "not(a=0) ==> a * (b / a) = b"

    81   rcancel_const           "[| a is_const; b is_const |] ==> a*(x/b) = a/b*x"

    82   rshift_nominator        "(a::real) * b / c = a / c * b"

    84   exp_pow                 "(a ^^^ b) ^^^ c = a ^^^ (b * c)"

    85   rsqare                  "(a::real) * a = a ^^^ 2"

    86   power_1                 "(a::real) ^^^ 1 = a"

    87   rbinom_power_2          "((a::real) + b)^^^ 2 = a^^^ 2 + 2*a*b + b^^^ 2"

    89   rmult_1                 "1 * k = (k::real)"

    90   rmult_1_right           "k * 1 = (k::real)"

    91   rmult_0                 "0 * k = (0::real)"

    92   rmult_0_right           "k * 0 = (0::real)"

    93   radd_0                  "0 + k = (k::real)"

    94   radd_0_right            "k + 0 = (k::real)"

    96   radd_real_const_eq

    97           "[| a is_const; c is_const; d is_const |] ==> a/d + c/d = (a+c)/(d::real)"

    98   radd_real_const

    99           "[| a is_const; b is_const; c is_const; d is_const |] ==> a/b + c/d = (a*d + b*c)/(b*(d::real))"

   101 (*for AC-operators*)

   102   radd_commute            "(m::real) + (n::real) = n + m"

   103   radd_left_commute       "(x::real) + (y + z) = y + (x + z)"

   104   radd_assoc              "(m::real) + n + k = m + (n + k)"

   105   rmult_commute           "(m::real) * n = n * m"

   106   rmult_left_commute      "(x::real) * (y * z) = y * (x * z)"

   107   rmult_assoc             "(m::real) * n * k = m * (n * k)"

   109 (*for equations: 'bdv' is a meta-constant*)

   110   risolate_bdv_add       "((k::real) + bdv = m) = (bdv = m + (-1)*k)"

   111   risolate_bdv_mult_add  "((k::real) + n*bdv = m) = (n*bdv = m + (-1)*k)"

   112   risolate_bdv_mult      "((n::real) * bdv = m) = (bdv = m / n)"

   114   rnorm_equation_add

   115       "~(b =!= 0) ==> (a = b) = (a + (-1)*b = 0)"

   117 (*17.9.02 aus SqRoot.thy------------------------------vvv---*)

   118   root_ge0            "0 <= a ==> 0 <= sqrt a"

   119   (*should be dropped with better simplification in eval_rls ...*)

   120   root_add_ge0

   121 	"[| 0 <= a; 0 <= b |] ==> (0 <= sqrt a + sqrt b) = True"

   122   root_ge0_1

   123 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= a * sqrt b + sqrt c) = True"

   124   root_ge0_2

   125 	"[| 0<=a; 0<=b; 0<=c |] ==> (0 <= sqrt a + b * sqrt c) = True"

   128   rroot_square_inv         "(sqrt a)^^^ 2 = a"

   129   rroot_times_root         "sqrt a * sqrt b = sqrt(a*b)"

   130   rroot_times_root_assoc   "(a * sqrt b) * sqrt c = a * sqrt(b*c)"

   131   rroot_times_root_assoc_p "sqrt b * (sqrt c * a)= sqrt(b*c) * a"

   134 (*for root-equations*)

   135   square_equation_left

   136           "[| 0 <= a; 0 <= b |] ==> (((sqrt a)=b)=(a=(b^^^ 2)))"

   137   square_equation_right

   138           "[| 0 <= a; 0 <= b |] ==> ((a=(sqrt b))=((a^^^ 2)=b))"

   139   (*causes frequently non-termination:*)

   140   square_equation

   141           "[| 0 <= a; 0 <= b |] ==> ((a=b)=((a^^^ 2)=b^^^ 2))"

   143   risolate_root_add        "(a+  sqrt c = d) = (  sqrt c = d + (-1)*a)"

   144   risolate_root_mult       "(a+b*sqrt c = d) = (b*sqrt c = d + (-1)*a)"

   145   risolate_root_div        "(a * sqrt c = d) = (  sqrt c = d / a)"

   147 (*for polynomial equations of degree 2; linear case in RatArith*)

   148   mult_square		"(a*bdv^^^2 = b) = (bdv^^^2 = b / a)"

   149   constant_square       "(a + bdv^^^2 = b) = (bdv^^^2 = b + -1*a)"

   150   constant_mult_square  "(a + b*bdv^^^2 = c) = (b*bdv^^^2 = c + -1*a)"

   152   square_equality

   153 	     "0 <= a ==> (x^^^2 = a) = ((x=sqrt a) | (x=-1*sqrt a))"

   154   square_equality_0

   155 	     "(x^^^2 = 0) = (x = 0)"

   157 (*isolate root on the LEFT hand side of the equation

   158   otherwise shuffling from left to right would not terminate*)

   160   rroot_to_lhs

   161           "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)"

   162   rroot_to_lhs_mult

   163           "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)"

   164   rroot_to_lhs_add_mult

   165           "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"

   166 (*17.9.02 aus SqRoot.thy------------------------------^^^---*)

   168 ML {*

   169 (** evaluation of numerals and predicates **)

   171 (*does a term contain a root ?*)

   172 fun eval_root_free (thmid:string) _ (t as (Const(op0,t0) $ arg)) thy =

   173   if strip_thy op0 <> "is'_root'_free"

   174     then raise error ("eval_root_free: wrong "^op0)

   175   else if const_in (strip_thy op0) arg

   176 	 then SOME (mk_thmid thmid ""

   177 		    ((Syntax.string_of_term (thy2ctxt thy)) arg) "",

   178 		    Trueprop $ (mk_equality (t, false_as_term)))

   179        else SOME (mk_thmid thmid ""

   180 		  ((Syntax.string_of_term (thy2ctxt thy)) arg) "",

   181 		  Trueprop $ (mk_equality (t, true_as_term)))

   182   | eval_root_free _ _ _ _ = NONE;

   184 (*does a term contain a root ?*)

   185 fun eval_contains_root (thmid:string) _

   186 		       (t as (Const("Test.contains'_root",t0) $ arg)) thy =

   187     if member op = (ids_of arg) "sqrt"

   188     then SOME (mk_thmid thmid ""

   189 			((Syntax.string_of_term (thy2ctxt thy)) arg) "",

   190 	       Trueprop $ (mk_equality (t, true_as_term)))

   191     else SOME (mk_thmid thmid ""

   192 			((Syntax.string_of_term (thy2ctxt thy)) arg) "",

   193 	       Trueprop $ (mk_equality (t, false_as_term)))

   194   | eval_contains_root _ _ _ _ = NONE;

   196 calclist':= overwritel (!calclist',

   197    [("is_root_free", ("Test.is'_root'_free",

   198 		      eval_root_free"#is_root_free_")),

   199     ("contains_root", ("Test.contains'_root",

   200 		       eval_contains_root"#contains_root_"))

   201     ]);

   203 (** term order **)

   204 fun term_order (_:subst) tu = (term_ordI [] tu = LESS);

   206 (** rule sets **)

   208 val testerls =

   209   Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),

   210       erls = e_rls, srls = Erls,

   211       calc = [],

   212       rules = [Thm ("refl",num_str refl),

   213 	       Thm ("le_refl",num_str le_refl),

   214 	       Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

   215 	       Thm ("not_true",num_str not_true),

   216 	       Thm ("not_false",num_str not_false),

   217 	       Thm ("and_true",and_true),

   218 	       Thm ("and_false",and_false),

   219 	       Thm ("or_true",or_true),

   220 	       Thm ("or_false",or_false),

   221 	       Thm ("and_commute",num_str and_commute),

   222 	       Thm ("or_commute",num_str or_commute),

   224 	       Calc ("Atools.is'_const",eval_const "#is_const_"),

   225 	       Calc ("Tools.matches",eval_matches ""),

   227 	       Calc ("op +",eval_binop "#add_"),

   228 	       Calc ("op *",eval_binop "#mult_"),

   229 	       Calc ("Atools.pow" ,eval_binop "#power_"),

   231 	       Calc ("op <",eval_equ "#less_"),

   232 	       Calc ("op <=",eval_equ "#less_equal_"),

   234 	       Calc ("Atools.ident",eval_ident "#ident_")],

   235       scr = Script ((term_of o the o (parse thy))

   236       "empty_script")

   237       }:rls;

   239 (*.for evaluation of conditions in rewrite rules.*)

   240 (*FIXXXXXXME 10.8.02: handle like _simplify*)

   241 val tval_rls =

   242   Rls{id = "tval_rls", preconds = [],

   243       rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),

   244       erls=testerls,srls = e_rls,

   245       calc=[],

   246       rules = [Thm ("refl",num_str refl),

   247 	       Thm ("le_refl",num_str le_refl),

   248 	       Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),

   249 	       Thm ("not_true",num_str not_true),

   250 	       Thm ("not_false",num_str not_false),

   251 	       Thm ("and_true",and_true),

   252 	       Thm ("and_false",and_false),

   253 	       Thm ("or_true",or_true),

   254 	       Thm ("or_false",or_false),

   255 	       Thm ("and_commute",num_str and_commute),

   256 	       Thm ("or_commute",num_str or_commute),

   258 	       Thm ("real_diff_minus",num_str real_diff_minus),

   260 	       Thm ("root_ge0",num_str root_ge0),

   261 	       Thm ("root_add_ge0",num_str root_add_ge0),

   262 	       Thm ("root_ge0_1",num_str root_ge0_1),

   263 	       Thm ("root_ge0_2",num_str root_ge0_2),

   265 	       Calc ("Atools.is'_const",eval_const "#is_const_"),

   266 	       Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),

   267 	       Calc ("Tools.matches",eval_matches ""),

   268 	       Calc ("Test.contains'_root",

   269 		     eval_contains_root"#contains_root_"),

   271 	       Calc ("op +",eval_binop "#add_"),

   272 	       Calc ("op *",eval_binop "#mult_"),

   273 	       Calc ("Root.sqrt",eval_sqrt "#sqrt_"),

   274 	       Calc ("Atools.pow" ,eval_binop "#power_"),

   276 	       Calc ("op <",eval_equ "#less_"),

   277 	       Calc ("op <=",eval_equ "#less_equal_"),

   279 	       Calc ("Atools.ident",eval_ident "#ident_")],

   280       scr = Script ((term_of o the o (parse thy))

   281       "empty_script")

   282       }:rls;

   285 ruleset' := overwritelthy thy (!ruleset',

   286   [("testerls", prep_rls testerls)

   287    ]);

   290 (*make () dissappear*)

   291 val rearrange_assoc =

   292   Rls{id = "rearrange_assoc", preconds = [],

   293       rew_ord = ("e_rew_ord",e_rew_ord),

   294       erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

   295       rules =

   296       [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),

   297        Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],

   298       scr = Script ((term_of o the o (parse thy))

   299       "empty_script")

   300       }:rls;

   302 val ac_plus_times =

   303   Rls{id = "ac_plus_times", preconds = [], rew_ord = ("term_order",term_order),

   304       erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

   305       rules =

   306       [Thm ("radd_commute",radd_commute),

   307        Thm ("radd_left_commute",radd_left_commute),

   308        Thm ("radd_assoc",radd_assoc),

   309        Thm ("rmult_commute",rmult_commute),

   310        Thm ("rmult_left_commute",rmult_left_commute),

   311        Thm ("rmult_assoc",rmult_assoc)],

   312       scr = Script ((term_of o the o (parse thy))

   313       "empty_script")

   314       }:rls;

   316 (*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)

   317 val norm_equation =

   318   Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),

   319       erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)

   320       rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)

   321 	       ],

   322       scr = Script ((term_of o the o (parse thy))

   323       "empty_script")

   324       }:rls;

   326 (** rule sets **)

   328 val STest_simplify =     (*   vv--- not changed to real by parse*)

   329   "Script STest_simplify (t_::'z) =                           " ^

   330   "(Repeat" ^

   331   "    ((Try (Repeat (Rewrite real_diff_minus False))) @@        " ^

   332   "     (Try (Repeat (Rewrite radd_mult_distrib2 False))) @@  " ^

   333   "     (Try (Repeat (Rewrite rdistr_right_assoc False))) @@  " ^

   334   "     (Try (Repeat (Rewrite rdistr_right_assoc_p False))) @@" ^

   335   "     (Try (Repeat (Rewrite rdistr_div_right False))) @@    " ^

   336   "     (Try (Repeat (Rewrite rbinom_power_2 False))) @@      " ^

   338   "     (Try (Repeat (Rewrite radd_commute False))) @@        " ^

   339   "     (Try (Repeat (Rewrite radd_left_commute False))) @@   " ^

   340   "     (Try (Repeat (Rewrite radd_assoc False))) @@          " ^

   341   "     (Try (Repeat (Rewrite rmult_commute False))) @@       " ^

   342   "     (Try (Repeat (Rewrite rmult_left_commute False))) @@  " ^

   343   "     (Try (Repeat (Rewrite rmult_assoc False))) @@         " ^

   345   "     (Try (Repeat (Rewrite radd_real_const_eq False))) @@   " ^

   346   "     (Try (Repeat (Rewrite radd_real_const False))) @@   " ^

   347   "     (Try (Repeat (Calculate plus))) @@   " ^

   348   "     (Try (Repeat (Calculate times))) @@   " ^

   349   "     (Try (Repeat (Calculate divide_))) @@" ^

   350   "     (Try (Repeat (Calculate power_))) @@  " ^

   352   "     (Try (Repeat (Rewrite rcollect_right False))) @@   " ^

   353   "     (Try (Repeat (Rewrite rcollect_one_left False))) @@   " ^

   354   "     (Try (Repeat (Rewrite rcollect_one_left_assoc False))) @@   " ^

   355   "     (Try (Repeat (Rewrite rcollect_one_left_assoc_p False))) @@   " ^

   357   "     (Try (Repeat (Rewrite rshift_nominator False))) @@   " ^

   358   "     (Try (Repeat (Rewrite rcancel_den False))) @@   " ^

   359   "     (Try (Repeat (Rewrite rroot_square_inv False))) @@   " ^

   360   "     (Try (Repeat (Rewrite rroot_times_root False))) @@   " ^

   361   "     (Try (Repeat (Rewrite rroot_times_root_assoc_p False))) @@   " ^

   362   "     (Try (Repeat (Rewrite rsqare False))) @@   " ^

   363   "     (Try (Repeat (Rewrite power_1 False))) @@   " ^

   364   "     (Try (Repeat (Rewrite rtwo_of_the_same False))) @@   " ^

   365   "     (Try (Repeat (Rewrite rtwo_of_the_same_assoc_p False))) @@   " ^

   367   "     (Try (Repeat (Rewrite rmult_1 False))) @@   " ^

   368   "     (Try (Repeat (Rewrite rmult_1_right False))) @@   " ^

   369   "     (Try (Repeat (Rewrite rmult_0 False))) @@   " ^

   370   "     (Try (Repeat (Rewrite rmult_0_right False))) @@   " ^

   371   "     (Try (Repeat (Rewrite radd_0 False))) @@   " ^

   372   "     (Try (Repeat (Rewrite radd_0_right False)))) " ^

   373   " t_)";

   376 (* expects * distributed over + *)

   377 val Test_simplify =

   378   Rls{id = "Test_simplify", preconds = [],

   379       rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),

   380       erls = tval_rls, srls = e_rls,

   381       calc=[(*since 040209 filled by prep_rls*)],

   382       (*asm_thm = [],*)

   383       rules = [

   384 	       Thm ("real_diff_minus",num_str real_diff_minus),

   385 	       Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),

   386 	       Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),

   387 	       Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),

   388 	       Thm ("rdistr_div_right",num_str rdistr_div_right),

   389 	       Thm ("rbinom_power_2",num_str rbinom_power_2),

   391                Thm ("radd_commute",num_str radd_commute),

   392 	       Thm ("radd_left_commute",num_str radd_left_commute),

   393 	       Thm ("radd_assoc",num_str radd_assoc),

   394 	       Thm ("rmult_commute",num_str rmult_commute),

   395 	       Thm ("rmult_left_commute",num_str rmult_left_commute),

   396 	       Thm ("rmult_assoc",num_str rmult_assoc),

   398 	       Thm ("radd_real_const_eq",num_str radd_real_const_eq),

   399 	       Thm ("radd_real_const",num_str radd_real_const),

   400 	       (* these 2 rules are invers to distr_div_right wrt. termination.

   401 		  thus they MUST be done IMMEDIATELY before calc *)

   402 	       Calc ("op +", eval_binop "#add_"),

   403 	       Calc ("op *", eval_binop "#mult_"),

   404 	       Calc ("HOL.divide", eval_cancel "#divide_"),

   405 	       Calc ("Atools.pow", eval_binop "#power_"),

   407 	       Thm ("rcollect_right",num_str rcollect_right),

   408 	       Thm ("rcollect_one_left",num_str rcollect_one_left),

   409 	       Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),

   410 	       Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),

   412 	       Thm ("rshift_nominator",num_str rshift_nominator),

   413 	       Thm ("rcancel_den",num_str rcancel_den),

   414 	       Thm ("rroot_square_inv",num_str rroot_square_inv),

   415 	       Thm ("rroot_times_root",num_str rroot_times_root),

   416 	       Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),

   417 	       Thm ("rsqare",num_str rsqare),

   418 	       Thm ("power_1",num_str power_1),

   419 	       Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),

   420 	       Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),

   422 	       Thm ("rmult_1",num_str rmult_1),

   423 	       Thm ("rmult_1_right",num_str rmult_1_right),

   424 	       Thm ("rmult_0",num_str rmult_0),

   425 	       Thm ("rmult_0_right",num_str rmult_0_right),

   426 	       Thm ("radd_0",num_str radd_0),

   427 	       Thm ("radd_0_right",num_str radd_0_right)

   428 	       ],

   429       scr = Script ((term_of o the o (parse thy)) "empty_script")

   430 		    (*since 040209 filled by prep_rls: STest_simplify*)

   431       }:rls;

   437 (** rule sets **)

   441 (*isolate the root in a root-equation*)

   442 val isolate_root =

   443   Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),

   444       erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)

   445       rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),

   446 	       Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),

   447 	       Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),

   448 	       Thm ("risolate_root_add",num_str risolate_root_add),

   449 	       Thm ("risolate_root_mult",num_str risolate_root_mult),

   450 	       Thm ("risolate_root_div",num_str risolate_root_div)       ],

   451       scr = Script ((term_of o the o (parse thy))

   452       "empty_script")

   453       }:rls;

   455 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)

   456 val isolate_bdv =

   457     Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),

   458 	erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)

   459 	rules =

   460 	[Thm ("risolate_bdv_add",num_str risolate_bdv_add),

   461 	 Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),

   462 	 Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),

   463 	 Thm ("mult_square",num_str mult_square),

   464 	 Thm ("constant_square",num_str constant_square),

   465 	 Thm ("constant_mult_square",num_str constant_mult_square)

   466 	 ],

   467 	scr = Script ((term_of o the o (parse thy))

   468 			  "empty_script")

   469 	}:rls;

   474 (* association list for calculate_, calculate

   475    "op +" etc. not usable in scripts *)

   476 val calclist =

   477     [

   478      (*as Tools.ML*)

   479      ("Vars"    ,("Tools.Vars"    ,eval_var "#Vars_")),

   480      ("matches",("Tools.matches",eval_matches "#matches_")),

   481      ("lhs"    ,("Tools.lhs"    ,eval_lhs "")),

   482      (*aus Atools.ML*)

   483      ("PLUS"    ,("op +"        ,eval_binop "#add_")),

   484      ("TIMES"   ,("op *"        ,eval_binop "#mult_")),

   485      ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_")),

   486      ("POWER"  ,("Atools.pow"  ,eval_binop "#power_")),

   487      ("is_const",("Atools.is'_const",eval_const "#is_const_")),

   488      ("le"      ,("op <"        ,eval_equ "#less_")),

   489      ("leq"     ,("op <="       ,eval_equ "#less_equal_")),

   490      ("ident"   ,("Atools.ident",eval_ident "#ident_")),

   491      (*von hier (ehem.SqRoot*)

   492      ("sqrt"    ,("Root.sqrt"   ,eval_sqrt "#sqrt_")),

   493      ("Test.is_root_free",("is'_root'_free", eval_root_free"#is_root_free_")),

   494      ("Test.contains_root",("contains'_root",

   495 			    eval_contains_root"#contains_root_"))

   496      ];

   498 ruleset' := overwritelthy thy (!ruleset',

   499   [("Test_simplify", prep_rls Test_simplify),

   500    ("tval_rls", prep_rls tval_rls),

   501    ("isolate_root", prep_rls isolate_root),

   502    ("isolate_bdv", prep_rls isolate_bdv),

   503    ("matches",

   504     prep_rls (append_rls "matches" testerls

   505 			 [Calc ("Tools.matches",eval_matches "#matches_")]))

   506    ]);

   508 (** problem types **)

   509 store_pbt

   510  (prep_pbt (theory "Test") "pbl_test" [] e_pblID

   511  (["test"],

   512   [],

   513   e_rls, NONE, []));

   514 store_pbt

   515  (prep_pbt (theory "Test") "pbl_test_equ" [] e_pblID

   516  (["equation","test"],

   517   [("#Given" ,["equality e_","solveFor v_"]),

   518    ("#Where" ,["matches (?a = ?b) e_"]),

   519    ("#Find"  ,["solutions v_i_"])

   520   ],

   521   assoc_rls "matches",

   522   SOME "solve (e_::bool, v_)", []));

   524 store_pbt

   525  (prep_pbt (theory "Test") "pbl_test_uni" [] e_pblID

   526  (["univariate","equation","test"],

   527   [("#Given" ,["equality e_","solveFor v_"]),

   528    ("#Where" ,["matches (?a = ?b) e_"]),

   529    ("#Find"  ,["solutions v_i_"])

   530   ],

   531   assoc_rls "matches",

   532   SOME "solve (e_::bool, v_)", []));

   534 store_pbt

   535  (prep_pbt (theory "Test") "pbl_test_uni_lin" [] e_pblID

   536  (["linear","univariate","equation","test"],

   537   [("#Given" ,["equality e_","solveFor v_"]),

   538    ("#Where" ,["(matches (   v_ = 0) e_) | (matches (   ?b*v_ = 0) e_) |" ^

   539 	       "(matches (?a+v_ = 0) e_) | (matches (?a+?b*v_ = 0) e_)  "]),

   540    ("#Find"  ,["solutions v_i_"])

   541   ],

   542   assoc_rls "matches",

   543   SOME "solve (e_::bool, v_)", [["Test","solve_linear"]]));

   545 (*25.8.01 ------

   546 store_pbt

   547  (prep_pbt (theory "Test")

   548  (["(theory "Test")"],

   549   [("#Given" ,"boolTestGiven g_"),

   550    ("#Find"  ,"boolTestFind f_")

   551   ],

   552   []));

   554 store_pbt

   555  (prep_pbt (theory "Test")

   556  (["testeq","(theory "Test")"],

   557   [("#Given" ,"boolTestGiven g_"),

   558    ("#Find"  ,"boolTestFind f_")

   559   ],

   560   []));

   563 val ttt = (term_of o the o (parse (theory "Isac"))) "(matches (   v_ = 0) e_)";

   565  ------ 25.8.01*)

   568 (** methods **)

   569 store_met

   570  (prep_met (theory "Diff") "met_test" [] e_metID

   571  (["Test"],

   572    [],

   573    {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,

   574     crls=Atools_erls, nrls=e_rls(*,

   575     asm_rls=[],asm_thm=[]*)}, "empty_script"));

   576 (*

   577 store_met

   578  (prep_met (theory "Script")

   579  (e_metID,(*empty method*)

   580    [],

   581    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

   582     asm_rls=[],asm_thm=[]},

   583    "Undef"));*)

   584 store_met

   585  (prep_met (theory "Test") "met_test_solvelin" [] e_metID

   586  (["Test","solve_linear"]:metID,

   587   [("#Given" ,["equality e_","solveFor v_"]),

   588     ("#Where" ,["matches (?a = ?b) e_"]),

   589     ("#Find"  ,["solutions v_i_"])

   590     ],

   591    {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,

   592     prls=assoc_rls "matches",

   593     calc=[],

   594     crls=tval_rls, nrls=Test_simplify},

   595  "Script Solve_linear (e_::bool) (v_::real)=             " ^

   596  "(let e_ =" ^

   597  "  Repeat" ^

   598  "    (((Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^

   599  "      (Rewrite_Set Test_simplify False))) e_" ^

   600  " in [e_::bool])"

   601  )

   602 (*, prep_met (theory "Test") (*test for equations*)

   603  (["Test","testeq"]:metID,

   604   [("#Given" ,["boolTestGiven g_"]),

   605    ("#Find"  ,["boolTestFind f_"])

   606     ],

   607   {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[],

   608    asm_thm=[("square_equation_left","")]},

   609  "Script Testeq (eq_::bool) =                                         " ^

   610    "Repeat                                                            " ^

   611    " (let e_ = Try (Repeat (Rewrite rroot_square_inv False eq_));      " ^

   612    "      e_ = Try (Repeat (Rewrite square_equation_left True e_)); " ^

   613    "      e_ = Try (Repeat (Rewrite rmult_0 False e_))                " ^

   614    "   in e_) Until (is_root_free e_)" (*deleted*)

   615  )

   616 , ---------27.4.02*)

   617 );

   622 ruleset' := overwritelthy thy (!ruleset',

   623   [("norm_equation", prep_rls norm_equation),

   624    ("ac_plus_times", prep_rls ac_plus_times),

   625    ("rearrange_assoc", prep_rls rearrange_assoc)

   626    ]);

   629 fun bin_o (Const (op_,(Type ("fun",

   630 	   [Type (s2,[]),Type ("fun",

   631 	    [Type (s4,tl4),Type (s5,tl5)])])))) =

   632     if (s2=s4)andalso(s4=s5)then[op_]else[]

   633     | bin_o _                                   = [];

   635 fun bin_op (t1 $ t2) = union op = (bin_op t1) (bin_op t2)

   636   | bin_op t         =  bin_o t;

   637 fun is_bin_op t = ((bin_op t)<>[]);

   639 fun bin_op_arg1 ((Const (op_,(Type ("fun",

   640 	   [Type (s2,[]),Type ("fun",

   641 	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =

   642     arg1;

   643 fun bin_op_arg2 ((Const (op_,(Type ("fun",

   644 	   [Type (s2,[]),Type ("fun",

   645 	    [Type (s4,tl4),Type (s5,tl5)])]))))$ arg1 $ arg2) =

   646     arg2;

   649 exception NO_EQUATION_TERM;

   650 fun is_equation ((Const ("op =",(Type ("fun",

   651 		 [Type (_,[]),Type ("fun",

   652 		  [Type (_,[]),Type ("bool",[])])])))) $ _ $ _)

   653                   = true

   654   | is_equation _ = false;

   655 fun equ_lhs ((Const ("op =",(Type ("fun",

   656 		 [Type (_,[]),Type ("fun",

   657 		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r)

   658               = l

   659   | equ_lhs _ = raise NO_EQUATION_TERM;

   660 fun equ_rhs ((Const ("op =",(Type ("fun",

   661 		 [Type (_,[]),Type ("fun",

   662 		  [Type (_,[]),Type ("bool",[])])])))) $ l $ r)

   663               = r

   664   | equ_rhs _ = raise NO_EQUATION_TERM;

   667 fun atom (Const (_,Type (_,[])))           = true

   668   | atom (Free  (_,Type (_,[])))           = true

   669   | atom (Var   (_,Type (_,[])))           = true

   670 (*| atom (_     (_,"?DUMMY"   ))           = true ..ML-error *)

   671   | atom((Const ("Bin.integ_of_bin",_)) $ _) = true

   672   | atom _                                 = false;

   674 fun varids (Const  (s,Type (_,[])))         = [strip_thy s]

   675   | varids (Free   (s,Type (_,[])))         = if is_no s then []

   676 					      else [strip_thy s]

   677   | varids (Var((s,_),Type (_,[])))         = [strip_thy s]

   678 (*| varids (_      (s,"?DUMMY"   ))         =   ..ML-error *)

   679   | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)

   680   | varids (Abs(a,T,t)) = union op = [a] (varids t)

   681   | varids (t1 $ t2) = union op = (varids t1) (varids t2)

   682   | varids _         = [];

   683 (*> val t = term_of (hd (parse Diophant.thy "x"));

   684 val t = Free ("x","?DUMMY") : term

   685 > varids t;

   686 val it = [] : string list          [] !!! *)

   689 fun bin_ops_only ((Const op_) $ t1 $ t2) =

   690     if(is_bin_op (Const op_))

   691     then(bin_ops_only t1)andalso(bin_ops_only t2)

   692     else false

   693   | bin_ops_only t =

   694     if atom t then true else bin_ops_only t;

   696 fun polynomial opl t bdVar = (* bdVar TODO *)

   697     subset op = (bin_op t, opl) andalso (bin_ops_only t);

   699 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *)

   700     andalso polynomial opl (equ_lhs t) bdVar

   701     andalso polynomial opl (equ_rhs t) bdVar

   702     andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse

   703              subset op = (varids bdVar, varids (equ_lhs t)));

   705 (*fun max is =

   706     let fun max_ m [] = m

   707 	  | max_ m (i::is) = if m<i then max_ i is else max_ m is;

   708     in max_ (hd is) is end;

   709 > max [1,5,3,7,4,2];

   710 val it = 7 : int  *)

   712 fun max (a,b) = if a < b then b else a;

   714 fun degree addl mul bdVar t =

   715 let

   716 fun deg _ _ v (Const  (s,Type (_,[])))         = if v=strip_thy s then 1 else 0

   717   | deg _ _ v (Free   (s,Type (_,[])))         = if v=strip_thy s then 1 else 0

   718   | deg _ _ v (Var((s,_),Type (_,[])))         = if v=strip_thy s then 1 else 0

   719 (*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *)

   720   | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0

   721   | deg addl mul v (h $ t1 $ t2) =

   722     if subset op = (bin_op h, addl)

   723     then max (deg addl mul v t1  ,deg addl mul v t2)

   724     else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)

   725 in if polynomial (addl @ [mul]) t bdVar

   726    then SOME (deg addl mul (id_of bdVar) t) else (NONE:int option)

   727 end;

   728 fun degree_ addl mul bdVar t = (* do not export *)

   729     let fun opt (SOME i)= i

   730 	  | opt  NONE   = 0

   731 in opt (degree addl mul bdVar t) end;

   734 fun linear addl mul t bdVar = (degree_ addl mul bdVar t)<2;

   736 fun linear_equ addl mul bdVar t =

   737     if is_equation t

   738     then let val degl = degree_ addl mul bdVar (equ_lhs t);

   739 	     val degr = degree_ addl mul bdVar (equ_rhs t)

   740 	 in if (degl>0 orelse degr>0)andalso max(degl,degr)<2

   741 		then true else false

   742 	 end

   743     else false;

   744 (* strip_thy op_  before *)

   745 fun is_div_op (dv,(Const (op_,(Type ("fun",

   746 	   [Type (s2,[]),Type ("fun",

   747 	    [Type (s4,tl4),Type (s5,tl5)])])))) )= (dv = strip_thy op_)

   748   | is_div_op _ = false;

   750 fun is_denom bdVar div_op t =

   751     let fun is bool[v]dv (Const  (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

   752 	  | is bool[v]dv (Free   (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

   753 	  | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)

   754 	  | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false

   755 	  | is bool[v]dv (h$n$d) =

   756 	      if is_div_op(dv,h)

   757 	      then (is false[v]dv n)orelse(is true[v]dv d)

   758 	      else (is bool [v]dv n)orelse(is bool[v]dv d)

   759 in is false (varids bdVar) (strip_thy div_op) t end;

   762 fun rational t div_op bdVar =

   763     is_denom bdVar div_op t andalso bin_ops_only t;

   767 (** problem types **)

   769 store_pbt

   770  (prep_pbt (theory "Test") "pbl_test_uni_plain2" [] e_pblID

   771  (["plain_square","univariate","equation","test"],

   772   [("#Given" ,["equality e_","solveFor v_"]),

   773    ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |" ^

   774 	       "(matches (     ?b*v_ ^^^2 = 0) e_) |" ^

   775 	       "(matches (?a +    v_ ^^^2 = 0) e_) |" ^

   776 	       "(matches (        v_ ^^^2 = 0) e_)"]),

   777    ("#Find"  ,["solutions v_i_"])

   778   ],

   779   assoc_rls "matches",

   780   SOME "solve (e_::bool, v_)", [["Test","solve_plain_square"]]));

   781 (*

   782  val e_ = (term_of o the o (parse thy)) "e_::bool";

   783  val ve = (term_of o the o (parse thy)) "4 + 3*x^^^2 = 0";

   784  val env = [(e_,ve)];

   786  val pre = (term_of o the o (parse thy))

   787 	      "(matches (a + b*v_ ^^^2 = 0, e_::bool)) |" ^

   788 	      "(matches (    b*v_ ^^^2 = 0, e_::bool)) |" ^

   789 	      "(matches (a +   v_ ^^^2 = 0, e_::bool)) |" ^

   790 	      "(matches (      v_ ^^^2 = 0, e_::bool))";

   791  val prei = subst_atomic env pre;

   792  val cpre = (cterm_of thy) prei;

   794  val SOME (ct,_) = rewrite_set_ thy false tval_rls cpre;

   795 val ct = "True | False | False | False" : cterm

   797 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

   798 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

   799 > val SOME (ct,_) = rewrite_ thy sqrt_right tval_rls false or_false ct;

   800 val ct = "True" : cterm

   802 *)

   804 store_pbt

   805  (prep_pbt (theory "Test") "pbl_test_uni_poly" [] e_pblID

   806  (["polynomial","univariate","equation","test"],

   807   [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),

   808    ("#Where" ,["False"]),

   809    ("#Find"  ,["solutions v_i_"])

   810   ],

   811   e_rls, SOME "solve (e_::bool, v_)", []));

   813 store_pbt

   814  (prep_pbt (theory "Test") "pbl_test_uni_poly_deg2" [] e_pblID

   815  (["degree_two","polynomial","univariate","equation","test"],

   816   [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),

   817    ("#Find"  ,["solutions v_i_"])

   818   ],

   819   e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));

   821 store_pbt

   822  (prep_pbt (theory "Test") "pbl_test_uni_poly_deg2_pq" [] e_pblID

   823  (["pq_formula","degree_two","polynomial","univariate","equation","test"],

   824   [("#Given" ,["equality (v_ ^^^2 + p_ * v_ + q__ = 0)","solveFor v_"]),

   825    ("#Find"  ,["solutions v_i_"])

   826   ],

   827   e_rls, SOME "solve (v_ ^^^2 + p_ * v_ + q__ = 0, v_)", []));

   829 store_pbt

   830  (prep_pbt (theory "Test") "pbl_test_uni_poly_deg2_abc" [] e_pblID

   831  (["abc_formula","degree_two","polynomial","univariate","equation","test"],

   832   [("#Given" ,["equality (a_ * x ^^^2 + b_ * x + c_ = 0)","solveFor v_"]),

   833    ("#Find"  ,["solutions v_i_"])

   834   ],

   835   e_rls, SOME "solve (a_ * x ^^^2 + b_ * x + c_ = 0, v_)", []));

   837 store_pbt

   838  (prep_pbt (theory "Test") "pbl_test_uni_root" [] e_pblID

   839  (["squareroot","univariate","equation","test"],

   840   [("#Given" ,["equality e_","solveFor v_"]),

   841    ("#Where" ,["contains_root (e_::bool)"]),

   842    ("#Find"  ,["solutions v_i_"])

   843   ],

   844   append_rls "contains_root" e_rls [Calc ("Test.contains'_root",

   845 			  eval_contains_root "#contains_root_")],

   846   SOME "solve (e_::bool, v_)", [["Test","square_equation"]]));

   848 store_pbt

   849  (prep_pbt (theory "Test") "pbl_test_uni_norm" [] e_pblID

   850  (["normalize","univariate","equation","test"],

   851   [("#Given" ,["equality e_","solveFor v_"]),

   852    ("#Where" ,[]),

   853    ("#Find"  ,["solutions v_i_"])

   854   ],

   855   e_rls, SOME "solve (e_::bool, v_)", [["Test","norm_univar_equation"]]));

   857 store_pbt

   858  (prep_pbt (theory "Test") "pbl_test_uni_roottest" [] e_pblID

   859  (["sqroot-test","univariate","equation","test"],

   860   [("#Given" ,["equality e_","solveFor v_"]),

   861    (*("#Where" ,["contains_root (e_::bool)"]),*)

   862    ("#Find"  ,["solutions v_i_"])

   863   ],

   864   e_rls, SOME "solve (e_::bool, v_)", []));

   866 (*

   867 (#ppc o get_pbt) ["sqroot-test","univariate","equation"];

   868   *)

   871 store_met

   872  (prep_met (theory "Test")  "met_test_sqrt" [] e_metID

   873 (*root-equation, version for tests before 8.01.01*)

   874  (["Test","sqrt-equ-test"]:metID,

   875   [("#Given" ,["equality e_","solveFor v_"]),

   876    ("#Where" ,["contains_root (e_::bool)"]),

   877    ("#Find"  ,["solutions v_i_"])

   878    ],

   879   {rew_ord'="e_rew_ord",rls'=tval_rls,

   880    srls =append_rls "srls_contains_root" e_rls

   881 		    [Calc ("Test.contains'_root",eval_contains_root "")],

   882    prls =append_rls "prls_contains_root" e_rls

   883 		    [Calc ("Test.contains'_root",eval_contains_root "")],

   884    calc=[],

   885    crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   886    asm_thm=[("square_equation_left",""),

   887 	    ("square_equation_right","")]*)},

   888  "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

   889  "(let e_ = " ^

   890  "   ((While (contains_root e_) Do" ^

   891  "      ((Rewrite square_equation_left True) @@" ^

   892  "       (Try (Rewrite_Set Test_simplify False)) @@" ^

   893  "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^

   894  "       (Try (Rewrite_Set isolate_root False)) @@" ^

   895  "       (Try (Rewrite_Set Test_simplify False)))) @@" ^

   896  "    (Try (Rewrite_Set norm_equation False)) @@" ^

   897  "    (Try (Rewrite_Set Test_simplify False)) @@" ^

   898  "    (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^

   899  "    (Try (Rewrite_Set Test_simplify False)))" ^

   900  "   e_" ^

   901  " in [e_::bool])"

   902   ));

   904 store_met

   905  (prep_met (theory "Test")  "met_test_sqrt2" [] e_metID

   906 (*root-equation ... for test-*.sml until 8.01*)

   907  (["Test","squ-equ-test2"]:metID,

   908   [("#Given" ,["equality e_","solveFor v_"]),

   909    ("#Find"  ,["solutions v_i_"])

   910    ],

   911   {rew_ord'="e_rew_ord",rls'=tval_rls,

   912    srls = append_rls "srls_contains_root" e_rls

   913 		     [Calc ("Test.contains'_root",eval_contains_root"")],

   914    prls=e_rls,calc=[],

   915    crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   916    asm_thm=[("square_equation_left",""),

   917 	    ("square_equation_right","")]*)},

   918  "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

   919  "(let e_ = " ^

   920  "   ((While (contains_root e_) Do" ^

   921  "      ((Rewrite square_equation_left True) @@" ^

   922  "       (Try (Rewrite_Set Test_simplify False)) @@" ^

   923  "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^

   924  "       (Try (Rewrite_Set isolate_root False)) @@" ^

   925  "       (Try (Rewrite_Set Test_simplify False)))) @@" ^

   926  "    (Try (Rewrite_Set norm_equation False)) @@" ^

   927  "    (Try (Rewrite_Set Test_simplify False)) @@" ^

   928  "    (Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False) @@" ^

   929  "    (Try (Rewrite_Set Test_simplify False)))" ^

   930  "   e_;" ^

   931  "  (L_::bool list) = Tac subproblem_equation_dummy;          " ^

   932  "  L_ = Tac solve_equation_dummy                             " ^

   933  "  in Check_elementwise L_ {(v_::real). Assumptions})"

   934   ));

   936 store_met

   937  (prep_met (theory "Test") "met_test_squ_sub" [] e_metID

   938 (*tests subproblem fixed linear*)

   939  (["Test","squ-equ-test-subpbl1"]:metID,

   940   [("#Given" ,["equality e_","solveFor v_"]),

   941    ("#Find"  ,["solutions v_i_"])

   942    ],

   943   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

   944     crls=tval_rls, nrls=Test_simplify},

   945   "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

   946    " (let e_ = ((Try (Rewrite_Set norm_equation False)) @@              " ^

   947    "            (Try (Rewrite_Set Test_simplify False))) e_;              " ^

   948    "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^

   949    "                    [Test,solve_linear]) [bool_ e_, real_ v_])" ^

   950    "in Check_elementwise L_ {(v_::real). Assumptions})"

   951   ));

   953 store_met

   954  (prep_met (theory "Test") "met_test_squ_sub2" [] e_metID

   955  (*tests subproblem fixed degree 2*)

   956  (["Test","squ-equ-test-subpbl2"]:metID,

   957   [("#Given" ,["equality e_","solveFor v_"]),

   958    ("#Find"  ,["solutions v_i_"])

   959    ],

   960   {rew_ord'="e_rew_ord",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],

   961     crls=tval_rls, nrls=e_rls(*,

   962    asm_rls=[],asm_thm=[("square_equation_left",""),

   963 	    ("square_equation_right","")]*)},

   964    "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

   965    " (let e_ = Try (Rewrite_Set norm_equation False) e_;              " ^

   966    "(L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^

   967    "                    [Test,solve_by_pq_formula]) [bool_ e_, real_ v_])" ^

   968    "in Check_elementwise L_ {(v_::real). Assumptions})"

   969    ));

   971 store_met

   972  (prep_met (theory "Test") "met_test_squ_nonterm" [] e_metID

   973  (*root-equation: see foils..., but notTerminating*)

   974  (["Test","square_equation...notTerminating"]:metID,

   975   [("#Given" ,["equality e_","solveFor v_"]),

   976    ("#Find"  ,["solutions v_i_"])

   977    ],

   978   {rew_ord'="e_rew_ord",rls'=tval_rls,

   979    srls = append_rls "srls_contains_root" e_rls

   980 		     [Calc ("Test.contains'_root",eval_contains_root"")],

   981    prls=e_rls,calc=[],

   982     crls=tval_rls, nrls=e_rls(*,asm_rls=[],

   983    asm_thm=[("square_equation_left",""),

   984 	    ("square_equation_right","")]*)},

   985  "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

   986  "(let e_ = " ^

   987  "   ((While (contains_root e_) Do" ^

   988  "      ((Rewrite square_equation_left True) @@" ^

   989  "       (Try (Rewrite_Set Test_simplify False)) @@" ^

   990  "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^

   991  "       (Try (Rewrite_Set isolate_root False)) @@" ^

   992  "       (Try (Rewrite_Set Test_simplify False)))) @@" ^

   993  "    (Try (Rewrite_Set norm_equation False)) @@" ^

   994  "    (Try (Rewrite_Set Test_simplify False)))" ^

   995  "   e_;" ^

   996  "  (L_::bool list) =                                        " ^

   997  "    (SubProblem (Test_,[linear,univariate,equation,test]," ^

   998  "                 [Test,solve_linear]) [bool_ e_, real_ v_])" ^

   999  "in Check_elementwise L_ {(v_::real). Assumptions})"

  1000   ));

  1002 store_met

  1003  (prep_met (theory "Test")  "met_test_eq1" [] e_metID

  1004 (*root-equation1:*)

  1005  (["Test","square_equation1"]:metID,

  1006    [("#Given" ,["equality e_","solveFor v_"]),

  1007     ("#Find"  ,["solutions v_i_"])

  1008     ],

  1009    {rew_ord'="e_rew_ord",rls'=tval_rls,

  1010    srls = append_rls "srls_contains_root" e_rls

  1011 		     [Calc ("Test.contains'_root",eval_contains_root"")],

  1012    prls=e_rls,calc=[],

  1013     crls=tval_rls, nrls=e_rls(*,asm_rls=[],

  1014    asm_thm=[("square_equation_left",""),

  1015 	    ("square_equation_right","")]*)},

  1016  "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

  1017  "(let e_ = " ^

  1018  "   ((While (contains_root e_) Do" ^

  1019  "      ((Rewrite square_equation_left True) @@" ^

  1020  "       (Try (Rewrite_Set Test_simplify False)) @@" ^

  1021  "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^

  1022  "       (Try (Rewrite_Set isolate_root False)) @@" ^

  1023  "       (Try (Rewrite_Set Test_simplify False)))) @@" ^

  1024  "    (Try (Rewrite_Set norm_equation False)) @@" ^

  1025  "    (Try (Rewrite_Set Test_simplify False)))" ^

  1026  "   e_;" ^

  1027  "  (L_::bool list) = (SubProblem (Test_,[linear,univariate,equation,test]," ^

  1028  "                    [Test,solve_linear]) [bool_ e_, real_ v_])" ^

  1029  "  in Check_elementwise L_ {(v_::real). Assumptions})"

  1030   ));

  1032 store_met

  1033  (prep_met (theory "Test") "met_test_squ2" [] e_metID

  1034  (*root-equation2*)

  1035  (["Test","square_equation2"]:metID,

  1036    [("#Given" ,["equality e_","solveFor v_"]),

  1037     ("#Find"  ,["solutions v_i_"])

  1038     ],

  1039    {rew_ord'="e_rew_ord",rls'=tval_rls,

  1040    srls = append_rls "srls_contains_root" e_rls

  1041 		     [Calc ("Test.contains'_root",eval_contains_root"")],

  1042    prls=e_rls,calc=[],

  1043     crls=tval_rls, nrls=e_rls(*,asm_rls=[],

  1044    asm_thm=[("square_equation_left",""),

  1045 	    ("square_equation_right","")]*)},

  1046  "Script Solve_root_equation (e_::bool) (v_::real)  =  " ^

  1047  "(let e_ = " ^

  1048  "   ((While (contains_root e_) Do" ^

  1049  "      (((Rewrite square_equation_left True) Or " ^

  1050  "        (Rewrite square_equation_right True)) @@" ^

  1051  "       (Try (Rewrite_Set Test_simplify False)) @@" ^

  1052  "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^

  1053  "       (Try (Rewrite_Set isolate_root False)) @@" ^

  1054  "       (Try (Rewrite_Set Test_simplify False)))) @@" ^

  1055  "    (Try (Rewrite_Set norm_equation False)) @@" ^

  1056  "    (Try (Rewrite_Set Test_simplify False)))" ^

  1057  "   e_;" ^

  1058  "  (L_::bool list) = (SubProblem (Test_,[plain_square,univariate,equation,test]," ^

  1059  "                    [Test,solve_plain_square]) [bool_ e_, real_ v_])" ^

  1060  "  in Check_elementwise L_ {(v_::real). Assumptions})"

  1061   ));

  1063 store_met

  1064  (prep_met (theory "Test") "met_test_squeq" [] e_metID

  1065  (*root-equation*)

  1066  (["Test","square_equation"]:metID,

  1067    [("#Given" ,["equality e_","solveFor v_"]),

  1068     ("#Find"  ,["solutions v_i_"])

  1069     ],

  1070    {rew_ord'="e_rew_ord",rls'=tval_rls,

  1071    srls = append_rls "srls_contains_root" e_rls

  1072 		     [Calc ("Test.contains'_root",eval_contains_root"")],

  1073    prls=e_rls,calc=[],

  1074     crls=tval_rls, nrls=e_rls(*,asm_rls=[],

  1075    asm_thm=[("square_equation_left",""),

  1076 	    ("square_equation_right","")]*)},

  1077  "Script Solve_root_equation (e_::bool) (v_::real) =  " ^

  1078  "(let e_ = " ^

  1079  "   ((While (contains_root e_) Do" ^

  1080  "      (((Rewrite square_equation_left True) Or" ^

  1081  "        (Rewrite square_equation_right True)) @@" ^

  1082  "       (Try (Rewrite_Set Test_simplify False)) @@" ^

  1083  "       (Try (Rewrite_Set rearrange_assoc False)) @@" ^

  1084  "       (Try (Rewrite_Set isolate_root False)) @@" ^

  1085  "       (Try (Rewrite_Set Test_simplify False)))) @@" ^

  1086  "    (Try (Rewrite_Set norm_equation False)) @@" ^

  1087  "    (Try (Rewrite_Set Test_simplify False)))" ^

  1088  "   e_;" ^

  1089  "  (L_::bool list) = (SubProblem (Test_,[univariate,equation,test]," ^

  1090  "                    [no_met]) [bool_ e_, real_ v_])" ^

  1091  "  in Check_elementwise L_ {(v_::real). Assumptions})"

  1092   ) ); (*#######*)

  1094 store_met

  1095  (prep_met (theory "Test") "met_test_eq_plain" [] e_metID

  1096  (*solve_plain_square*)

  1097  (["Test","solve_plain_square"]:metID,

  1098    [("#Given",["equality e_","solveFor v_"]),

  1099    ("#Where" ,["(matches (?a + ?b*v_ ^^^2 = 0) e_) |" ^

  1100 	       "(matches (     ?b*v_ ^^^2 = 0) e_) |" ^

  1101 	       "(matches (?a +    v_ ^^^2 = 0) e_) |" ^

  1102 	       "(matches (        v_ ^^^2 = 0) e_)"]),

  1103    ("#Find"  ,["solutions v_i_"])

  1104    ],

  1105    {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=e_rls,

  1106     prls = assoc_rls "matches",

  1107     crls=tval_rls, nrls=e_rls(*,

  1108     asm_rls=[],asm_thm=[]*)},

  1109   "Script Solve_plain_square (e_::bool) (v_::real) =           " ^

  1110    " (let e_ = ((Try (Rewrite_Set isolate_bdv False)) @@         " ^

  1111    "            (Try (Rewrite_Set Test_simplify False)) @@     " ^

  1112    "            ((Rewrite square_equality_0 False) Or        " ^

  1113    "             (Rewrite square_equality True)) @@            " ^

  1114    "            (Try (Rewrite_Set tval_rls False))) e_             " ^

  1115    "  in ((Or_to_List e_)::bool list))"

  1116  ));

  1118 store_met

  1119  (prep_met (theory "Test") "met_test_norm_univ" [] e_metID

  1120  (["Test","norm_univar_equation"]:metID,

  1121    [("#Given",["equality e_","solveFor v_"]),

  1122    ("#Where" ,[]),

  1123    ("#Find"  ,["solutions v_i_"])

  1124    ],

  1125    {rew_ord'="e_rew_ord",rls'=tval_rls,srls = e_rls,prls=e_rls,

  1126    calc=[],

  1127     crls=tval_rls, nrls=e_rls(*,asm_rls=[],asm_thm=[]*)},

  1128   "Script Norm_univar_equation (e_::bool) (v_::real) =      " ^

  1129    " (let e_ = ((Try (Rewrite rnorm_equation_add False)) @@   " ^

  1130    "            (Try (Rewrite_Set Test_simplify False))) e_   " ^

  1131    "  in (SubProblem (Test_,[univariate,equation,test],         " ^

  1132    "                    [no_met]) [bool_ e_, real_ v_]))"

  1133  ));

  1137 (*17.9.02 aus SqRoot.ML------------------------------^^^---*)

  1139 (*8.4.03  aus Poly.ML--------------------------------vvv---

  1140   make_polynomial  ---> make_poly

  1141   ^-- for user          ^-- for systest _ONLY_*)

  1143 local (*. for make_polytest .*)

  1145 open Term;  (* for type order = EQUAL | LESS | GREATER *)

  1147 fun pr_ord EQUAL = "EQUAL"

  1148   | pr_ord LESS  = "LESS"

  1149   | pr_ord GREATER = "GREATER";

  1151 fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)

  1152   (case a of

  1153      "Atools.pow" => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)

  1154    | _ => (((a, 0), T), 0))

  1155   | dest_hd' (Free (a, T)) = (((a, 0), T), 1)

  1156   | dest_hd' (Var v) = (v, 2)

  1157   | dest_hd' (Bound i) = ((("", i), dummyT), 3)

  1158   | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);

  1159 (* RL *)

  1160 fun get_order_pow (t $ (Free(order,_))) =

  1161     	(case int_of_str (order) of

  1162 	             SOME d => d

  1163 		   | NONE   => 0)

  1164   | get_order_pow _ = 0;

  1166 fun size_of_term' (Const(str,_) $ t) =

  1167   if "Atools.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)

  1168   | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body

  1169   | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t

  1170   | size_of_term' _ = 1;

  1172 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)

  1173       (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)

  1174   | term_ord' pr thy (t, u) =

  1175       (if pr then

  1176 	 let

  1177 	   val (f, ts) = strip_comb t and (g, us) = strip_comb u;

  1178 	   val _=writeln("t= f@ts= " ^ "" ^

  1179 	      ((Syntax.string_of_term (thy2ctxt thy)) f)^ "\" @ " ^ "[" ^

  1180 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) ts)) ^ "]""");

  1181 	   val _=writeln("u= g@us= " ^ "" ^

  1182 	      ((Syntax.string_of_term (thy2ctxt thy)) g) ^ "\" @ " ^ "[" ^

  1183 	      (commas(map(Syntax.string_of_term (thy2ctxt thy)) us))^"]""");

  1184 	   val _=writeln("size_of_term(t,u)= ("^

  1185 	      (string_of_int(size_of_term' t)) ^ ", " ^

  1186 	      (string_of_int(size_of_term' u)) ^ ")");

  1187 	   val _=writeln("hd_ord(f,g)      = " ^ ((pr_ord o hd_ord)(f,g)));

  1188 	   val _=writeln("terms_ord(ts,us) = " ^

  1189 			   ((pr_ord o terms_ord str false)(ts,us)));

  1190 	   val _=writeln("-------");

  1191 	 in () end

  1192        else ();

  1193 	 case int_ord (size_of_term' t, size_of_term' u) of

  1194 	   EQUAL =>

  1195 	     let val (f, ts) = strip_comb t and (g, us) = strip_comb u in

  1196 	       (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)

  1197 	     | ord => ord)

  1198 	     end

  1199 	 | ord => ord)

  1200 and hd_ord (f, g) =                                        (* ~ term.ML *)

  1201   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)

  1202 and terms_ord str pr (ts, us) =

  1203     list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);

  1204 in

  1206 fun ord_make_polytest (pr:bool) thy (_:subst) tu =

  1207     (term_ord' pr thy(***) tu = LESS );

  1209 end;(*local*)

  1211 rew_ord' := overwritel (!rew_ord',

  1212 [("termlessI", termlessI),

  1213  ("ord_make_polytest", ord_make_polytest false thy)

  1214  ]);

  1216 (*WN060510 this was a preparation for prep_rls ...

  1217 val scr_make_polytest =

  1218 "Script Expand_binomtest t_ =" ^

  1219 "(Repeat                       " ^

  1220 "((Try (Repeat (Rewrite real_diff_minus         False))) @@ " ^

  1222 " (Try (Repeat (Rewrite real_add_mult_distrib   False))) @@ " ^

  1223 " (Try (Repeat (Rewrite real_add_mult_distrib2  False))) @@ " ^

  1224 " (Try (Repeat (Rewrite real_diff_mult_distrib  False))) @@ " ^

  1225 " (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ " ^

  1227 " (Try (Repeat (Rewrite real_mult_1             False))) @@ " ^

  1228 " (Try (Repeat (Rewrite real_mult_0             False))) @@ " ^

  1229 " (Try (Repeat (Rewrite real_add_zero_left      False))) @@ " ^

  1231 " (Try (Repeat (Rewrite real_mult_commute       False))) @@ " ^

  1232 " (Try (Repeat (Rewrite real_mult_left_commute  False))) @@ " ^

  1233 " (Try (Repeat (Rewrite real_mult_assoc         False))) @@ " ^

  1234 " (Try (Repeat (Rewrite real_add_commute        False))) @@ " ^

  1235 " (Try (Repeat (Rewrite real_add_left_commute   False))) @@ " ^

  1236 " (Try (Repeat (Rewrite real_add_assoc          False))) @@ " ^

  1238 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^

  1239 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^

  1240 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^

  1241 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^

  1243 " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^

  1244 " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^

  1246 " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^

  1247 " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^

  1249 " (Try (Repeat (Calculate plus  ))) @@ " ^

  1250 " (Try (Repeat (Calculate times ))) @@ " ^

  1251 " (Try (Repeat (Calculate power_)))) " ^

  1252 " t_)";

  1253 -----------------------------------------------------*)

  1255 val make_polytest =

  1256   Rls{id = "make_polytest", preconds = []:term list,

  1257       rew_ord = ("ord_make_polytest", ord_make_polytest false (theory "Poly")),

  1258       erls = testerls, srls = Erls,

  1259       calc = [("PLUS"  , ("op +", eval_binop "#add_")),

  1260 	      ("TIMES" , ("op *", eval_binop "#mult_")),

  1261 	      ("POWER", ("Atools.pow", eval_binop "#power_"))

  1262 	      ],

  1263       (*asm_thm = [],*)

  1264       rules = [Thm ("real_diff_minus",num_str real_diff_minus),

  1265 	       (*"a - b = a + (-1) * b"*)

  1266 	       Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),

  1267 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

  1268 	       Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),

  1269 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

  1270 	       Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),

  1271 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

  1272 	       Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),

  1273 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

  1274 	       Thm ("real_mult_1",num_str real_mult_1),

  1275 	       (*"1 * z = z"*)

  1276 	       Thm ("real_mult_0",num_str real_mult_0),

  1277 	       (*"0 * z = 0"*)

  1278 	       Thm ("real_add_zero_left",num_str real_add_zero_left),

  1279 	       (*"0 + z = z"*)

  1281 	       (*AC-rewriting*)

  1282 	       Thm ("real_mult_commute",num_str real_mult_commute),

  1283 	       (* z * w = w * z *)

  1284 	       Thm ("real_mult_left_commute",num_str real_mult_left_commute),

  1285 	       (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)

  1286 	       Thm ("real_mult_assoc",num_str real_mult_assoc),

  1287 	       (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)

  1288 	       Thm ("real_add_commute",num_str real_add_commute),

  1289 	       (*z + w = w + z*)

  1290 	       Thm ("real_add_left_commute",num_str real_add_left_commute),

  1291 	       (*x + (y + z) = y + (x + z)*)

  1292 	       Thm ("real_add_assoc",num_str real_add_assoc),

  1293 	       (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)

  1295 	       Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),

  1296 	       (*"r1 * r1 = r1 ^^^ 2"*)

  1297 	       Thm ("realpow_plus_1",num_str realpow_plus_1),

  1298 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

  1299 	       Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),

  1300 	       (*"z1 + z1 = 2 * z1"*)

  1301 	       Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),

  1302 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

  1304 	       Thm ("real_num_collect",num_str real_num_collect),

  1305 	       (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)

  1306 	       Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),

  1307 	       (*"[| l is_const; m is_const |] ==>

  1308 				l * n + (m * n + k) =  (l + m) * n + k"*)

  1309 	       Thm ("real_one_collect",num_str real_one_collect),

  1310 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)

  1311 	       Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),

  1312 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

  1314 	       Calc ("op +", eval_binop "#add_"),

  1315 	       Calc ("op *", eval_binop "#mult_"),

  1316 	       Calc ("Atools.pow", eval_binop "#power_")

  1317 	       ],

  1318       scr = EmptyScr(*Script ((term_of o the o (parse thy))

  1319       scr_make_polytest)*)

  1320       }:rls;

  1321 (*WN060510 this was done before 'fun prep_rls' ...

  1322 val scr_expand_binomtest =

  1323 "Script Expand_binomtest t_ =" ^

  1324 "(Repeat                       " ^

  1325 "((Try (Repeat (Rewrite real_plus_binom_pow2    False))) @@ " ^

  1326 " (Try (Repeat (Rewrite real_plus_binom_times   False))) @@ " ^

  1327 " (Try (Repeat (Rewrite real_minus_binom_pow2   False))) @@ " ^

  1328 " (Try (Repeat (Rewrite real_minus_binom_times  False))) @@ " ^

  1329 " (Try (Repeat (Rewrite real_plus_minus_binom1  False))) @@ " ^

  1330 " (Try (Repeat (Rewrite real_plus_minus_binom2  False))) @@ " ^

  1332 " (Try (Repeat (Rewrite real_mult_1             False))) @@ " ^

  1333 " (Try (Repeat (Rewrite real_mult_0             False))) @@ " ^

  1334 " (Try (Repeat (Rewrite real_add_zero_left      False))) @@ " ^

  1336 " (Try (Repeat (Calculate plus  ))) @@ " ^

  1337 " (Try (Repeat (Calculate times ))) @@ " ^

  1338 " (Try (Repeat (Calculate power_))) @@ " ^

  1340 " (Try (Repeat (Rewrite sym_realpow_twoI        False))) @@ " ^

  1341 " (Try (Repeat (Rewrite realpow_plus_1          False))) @@ " ^

  1342 " (Try (Repeat (Rewrite sym_real_mult_2         False))) @@ " ^

  1343 " (Try (Repeat (Rewrite real_mult_2_assoc       False))) @@ " ^

  1345 " (Try (Repeat (Rewrite real_num_collect        False))) @@ " ^

  1346 " (Try (Repeat (Rewrite real_num_collect_assoc  False))) @@ " ^

  1348 " (Try (Repeat (Rewrite real_one_collect        False))) @@ " ^

  1349 " (Try (Repeat (Rewrite real_one_collect_assoc  False))) @@ " ^

  1351 " (Try (Repeat (Calculate plus  ))) @@ " ^

  1352 " (Try (Repeat (Calculate times ))) @@ " ^

  1353 " (Try (Repeat (Calculate power_)))) " ^

  1354 " t_)";

  1355 ------------------------------------------------------*)

  1357 val expand_binomtest =

  1358   Rls{id = "expand_binomtest", preconds = [],

  1359       rew_ord = ("termlessI",termlessI),

  1360       erls = testerls, srls = Erls,

  1361       calc = [("PLUS"  , ("op +", eval_binop "#add_")),

  1362 	      ("TIMES" , ("op *", eval_binop "#mult_")),

  1363 	      ("POWER", ("Atools.pow", eval_binop "#power_"))

  1364 	      ],

  1365       (*asm_thm = [],*)

  1366       rules = [Thm ("real_plus_binom_pow2"  ,num_str real_plus_binom_pow2),

  1367 	       (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)

  1368 	       Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),

  1369 	      (*"(a + b)*(a + b) = ...*)

  1370 	       Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),

  1371 	       (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)

  1372 	       Thm ("real_minus_binom_times",num_str real_minus_binom_times),

  1373 	       (*"(a - b)*(a - b) = ...*)

  1374 	       Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),

  1375 		(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)

  1376 	       Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),

  1377 		(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)

  1378 	       (*RL 020915*)

  1379 	       Thm ("real_pp_binom_times",num_str real_pp_binom_times),

  1380 		(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)

  1381                Thm ("real_pm_binom_times",num_str real_pm_binom_times),

  1382 		(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)

  1383                Thm ("real_mp_binom_times",num_str real_mp_binom_times),

  1384 		(*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)

  1385                Thm ("real_mm_binom_times",num_str real_mm_binom_times),

  1386 		(*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)

  1387 	       Thm ("realpow_multI",num_str realpow_multI),

  1388 		(*(a*b)^^^n = a^^^n * b^^^n*)

  1389 	       Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),

  1390 	        (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)

  1391 	       Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),

  1392 	        (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)

  1395              (*  Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),

  1396 		(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

  1397 	       Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),

  1398 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

  1399 	       Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),

  1400 	       (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)

  1401 	       Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),

  1402 	       (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)

  1403 	       *)

  1405 	       Thm ("real_mult_1",num_str real_mult_1),              (*"1 * z = z"*)

  1406 	       Thm ("real_mult_0",num_str real_mult_0),              (*"0 * z = 0"*)

  1407 	       Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)

  1409 	       Calc ("op +", eval_binop "#add_"),

  1410 	       Calc ("op *", eval_binop "#mult_"),

  1411 	       Calc ("Atools.pow", eval_binop "#power_"),

  1412                (*

  1413 	        Thm ("real_mult_commute",num_str real_mult_commute),		(*AC-rewriting*)

  1414 	       Thm ("real_mult_left_commute",num_str real_mult_left_commute),	(**)

  1415 	       Thm ("real_mult_assoc",num_str real_mult_assoc),			(**)

  1416 	       Thm ("real_add_commute",num_str real_add_commute),		(**)

  1417 	       Thm ("real_add_left_commute",num_str real_add_left_commute),	(**)

  1418 	       Thm ("real_add_assoc",num_str real_add_assoc),	                (**)

  1419 	       *)

  1421 	       Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),

  1422 	       (*"r1 * r1 = r1 ^^^ 2"*)

  1423 	       Thm ("realpow_plus_1",num_str realpow_plus_1),

  1424 	       (*"r * r ^^^ n = r ^^^ (n + 1)"*)

  1425 	       (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),

  1426 	       (*"z1 + z1 = 2 * z1"*)*)

  1427 	       Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),

  1428 	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

  1430 	       Thm ("real_num_collect",num_str real_num_collect),

  1431 	       (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)

  1432 	       Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),

  1433 	       (*"[| l is_const; m is_const |] ==>  l * n + (m * n + k) =  (l + m) * n + k"*)

  1434 	       Thm ("real_one_collect",num_str real_one_collect),

  1435 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)

  1436 	       Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),

  1437 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)

  1439 	       Calc ("op +", eval_binop "#add_"),

  1440 	       Calc ("op *", eval_binop "#mult_"),

  1441 	       Calc ("Atools.pow", eval_binop "#power_")

  1442 	       ],

  1443       scr = EmptyScr

  1444 (*Script ((term_of o the o (parse thy)) scr_expand_binomtest)*)

  1445       }:rls;

  1448 ruleset' := overwritelthy thy (!ruleset',

  1449    [("make_polytest", prep_rls make_polytest),

  1450     ("expand_binomtest", prep_rls expand_binomtest)

  1451     ]);

  1452 *}

  1454 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Fri, 27 Aug 2010 14:56:54 +0200
branch	isac-update-Isa09-2
changeset 37954	4022d670753c
parent 37947	22235e4dbe5f
child 37965	9c11005c33b8
permissions	-rw-r--r--