1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Jul 13 15:28:43 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Jul 15 14:10:18 2021 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  "--------------------------------------------------------";
     1.5  "table of contents --------------------------------------";
     1.6  "--------------------------------------------------------";
     1.7 +"----------- fun contains_mult_pot_only --------------------------------------------------------";
     1.8 +"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
     1.9 +"----------- fun ist_monom ---------------------------------------------------------------------";
    1.10  "----------- fun eval_ist_monom -------------------------";
    1.11  "----------- watch order_add_mult  ----------------------";
    1.12  "----------- build predicate for +- ordering ------------";
    1.13 @@ -29,6 +32,55 @@
    1.14  
    1.15  val thy = @{theory "PolyMinus"};
    1.16  
    1.17 +"----------- fun contains_mult_pot_only --------------------------------------------------------";
    1.18 +"----------- fun contains_mult_pot_only --------------------------------------------------------";
    1.19 +"----------- fun contains_mult_pot_only --------------------------------------------------------";
    1.20 +val t = @{term 0};
    1.21 + if contains_mult_pot_only t then () else error "contains_mult_pot_only 1";
    1.22 +
    1.23 +val t = @{term "a"};
    1.24 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 2";
    1.25 +
    1.26 +val t = @{term "2 * a"};
    1.27 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 3";
    1.28 +
    1.29 +val t = @{term "2 * a * b"};
    1.30 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 4";
    1.31 +
    1.32 +val t = @{term "a * b"};
    1.33 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 5";
    1.34 +
    1.35 +val t = @{term "2 * a \<up> 2 * b"};
    1.36 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 6";
    1.37 +
    1.38 +val t = @{term "a \<up> 2 * b \<up> 3"};
    1.39 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 7";
    1.40 +
    1.41 +(* but also ..*)
    1.42 +val t = @{term "a \<up> 2 * 4 * b \<up> 3 * 5"};
    1.43 +if contains_mult_pot_only t then () else error "contains_mult_pot_only 8";
    1.44 +
    1.45 +
    1.46 +"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
    1.47 +"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
    1.48 +"----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
    1.49 +val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
    1.50 +
    1.51 +val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
    1.52 +           eval_kleiner "aaa" "bbb" t "ccc";
    1.53 +"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const ("PolyMinus.kleiner",_) $ a $ b)), _) =
    1.54 +  ("aaa", "bbb", t, "ccc");
    1.55 +    (*if*) TermC.is_num b (*else*);
    1.56 +
    1.57 +   	(*if*) identifier a < identifier b  (*else*);
    1.58 +"~~~~~ fun identifier , args:"; val (t) = (a);
    1.59 +
    1.60 +(*+*)case a of
    1.61 +  Const ("Num.numeral_class.numeral", _) $ (Const ("Num.num.Bit0", _) $
    1.62 +    (Const ("Num.num.Bit0", _) $ (Const ("Num.num.Bit1", _) $ Const ("Num.num.One", _)))) => ()
    1.63 +| _ => error "eval_kleiner CHANGED";
    1.64 +
    1.65 +
    1.66  "----------- fun eval_ist_monom ----------------------------------";
    1.67  "----------- fun eval_ist_monom ----------------------------------";
    1.68  "----------- fun eval_ist_monom ----------------------------------";