Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/polyminus.sml
changeset 60565 f92963a33fe3
parent 60556 486223010ea8
child 60571 19a172de0bb5
equal deleted inserted replaced
60564:90ea835c07b3 60565:f92963a33fe3 
    34 val ctxt = Proof_Context.init_global thy;
 
    34 val ctxt = Proof_Context.init_global thy;
 
    35 
    35 
    36 "----------- fun identifier --------------------------------------------------------------------";
 
    36 "----------- fun identifier --------------------------------------------------------------------";
 
    37 "----------- fun identifier --------------------------------------------------------------------";
 
    37 "----------- fun identifier --------------------------------------------------------------------";
 
    38 "----------- fun identifier --------------------------------------------------------------------";
 
    38 "----------- fun identifier --------------------------------------------------------------------";
 
    39 if identifier (TermC.str2term "12 ::real") = "12"     then () else error "identifier 1";
 
    39 if identifier (TermC.parse_test @{context} "12 ::real") = "12"     then () else error "identifier 1";
 
    40 if identifier (TermC.str2term
 
    40 if identifier (TermC.parse_test @{context}
 
    41   "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g ::real") = "|||||||||||||"
 
    41   "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g ::real") = "|||||||||||||"
 
    42                                                       then () else error "identifier 1a";
 
    42                                                       then () else error "identifier 1a";
 
    43 
    43 
    44 if identifier (TermC.str2term "a ::real") = "a"       then () else error "identifier 2";
 
    44 if identifier (TermC.parse_test @{context} "a ::real") = "a"       then () else error "identifier 2";
 
    45 if identifier (TermC.str2term "3 * a ::real") = "a"   then () else error "identifier 3";
 
    45 if identifier (TermC.parse_test @{context} "3 * a ::real") = "a"   then () else error "identifier 3";
 
    46 
    46 
    47 if identifier (TermC.str2term "a \<up> 2 ::real") = "a"   then () else error "identifier 4";
 
    47 if identifier (TermC.parse_test @{context} "a \<up> 2 ::real") = "a"   then () else error "identifier 4";
 
    48 if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
 
    48 if identifier (TermC.parse_test @{context} "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
 
    49 if identifier (TermC.str2term "a * b ::real") = "b"   then () else error "identifier 5b";
 
    49 if identifier (TermC.parse_test @{context} "a * b ::real") = "b"   then () else error "identifier 5b";
 
    50 
    50 
    51 (*these are strange (see "specific monomials" in comment to fun.def.)..*)
 
    51 (*these are strange (see "specific monomials" in comment to fun.def.)..*)
 
    52 if identifier (TermC.str2term "a*b ::real") = "b"     then () else error "identifier 6";
 
    52 if identifier (TermC.parse_test @{context} "a*b ::real") = "b"     then () else error "identifier 6";
 
    53 if identifier (TermC.str2term "(3*a*b) ::real") = "b" then () else error "identifier 7";
 
    53 if identifier (TermC.parse_test @{context} "(3*a*b) ::real") = "b" then () else error "identifier 7";
 
    54 
    54 
    55 
    55 
    56 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
 
    56 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
 
    57 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
 
    57 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
 
    58 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
 
    58 "----------- fun eval_kleiner, fun kleiner -----------------------------------------------------";
 
    60 "ba" < "ab";
 
    60 "ba" < "ab";
 
    61 "123" < "a"; (*unused due to ---vvv*)
 
    61 "123" < "a"; (*unused due to ---vvv*)
 
    62 "12" < "3"; (*true !!!*)
 
    62 "12" < "3"; (*true !!!*)
 
    63 
    63 
    64 " a kleiner b ==> (b + a) = (a + b)";
 
    64 " a kleiner b ==> (b + a) = (a + b)";
 
    65 TermC.str2term "aaa";
 
    65 TermC.parse_test @{context} "aaa";
 
    66 TermC.str2term "222 * aaa";
 
    66 TermC.parse_test @{context} "222 * aaa";
 
    67 
    67 
    68 case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
 
    68 case eval_kleiner 0 0 (TermC.parse_test @{context} "123 kleiner 32") 0 of
 
    69     SOME ("123 kleiner 32 = False", _) => ()
 
    69     SOME ("123 kleiner 32 = False", _) => ()
 
    70   | _ => error "polyminus.sml: 12 kleiner 9 = False";
 
    70   | _ => error "polyminus.sml: 12 kleiner 9 = False";
 
    71 case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
 
    71 case eval_kleiner 0 0 (TermC.parse_test @{context} "a kleiner b") 0 of
 
    72     SOME ("a kleiner b = True", _) => ()
 
    72     SOME ("a kleiner b = True", _) => ()
 
    73   | _ => error "polyminus.sml: a kleiner b = True";
 
    73   | _ => error "polyminus.sml: a kleiner b = True";
 
    74 case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
 
    74 case eval_kleiner 0 0 (TermC.parse_test @{context} "(10*g) kleiner f") 0 of
 
    75     SOME ("10 * g kleiner f = False", _) => ()
 
    75     SOME ("10 * g kleiner f = False", _) => ()
 
    76   | _ => error "polyminus.sml: 10 * g kleiner f = False";
 
    76   | _ => error "polyminus.sml: 10 * g kleiner f = False";
 
    77 case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
 
    77 case eval_kleiner 0 0 (TermC.parse_test @{context} "(a \<up> 2) kleiner b") 0 of
 
    78     SOME ("a \<up> 2 kleiner b = True", _) => ()
 
    78     SOME ("a \<up> 2 kleiner b = True", _) => ()
 
    79   | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
 
    79   | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
 
    80 case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
 
    80 case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a \<up> 2) kleiner b") 0 of
 
    81     SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
 
    81     SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
 
    82   | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
 
    82   | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
 
    83 case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
 
    83 case eval_kleiner 0 0 (TermC.parse_test @{context} "(a*b) kleiner c") 0 of
 
    84     SOME ("a * b kleiner c = True", _) => ()
 
    84     SOME ("a * b kleiner c = True", _) => ()
 
    85   | _ => error "polyminus.sml: a * b kleiner b = True";
 
    85   | _ => error "polyminus.sml: a * b kleiner b = True";
 
    86 case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
 
    86 case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a*b) kleiner c") 0 of
 
    87     SOME ("3 * a * b kleiner c = True", _) => ()
 
    87     SOME ("3 * a * b kleiner c = True", _) => ()
 
    88   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
 
    88   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
 
    89 
    89 
    90 
    90 
    91 val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
 
    91 val t = TermC.parse_test @{context} "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
 
    92 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
 
    92 val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
 
    93            eval_kleiner "aaa" "bbb" t "ccc";
 
    93            eval_kleiner "aaa" "bbb" t "ccc";
 
    94 "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>,_) $ a $ b)), _) =
 
    94 "~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>,_) $ a $ b)), _) =
 
    95   ("aaa", "bbb", t, "ccc");
 
    95   ("aaa", "bbb", t, "ccc");
 
    96     (*if*) TermC.is_num b (*else*);
 
    96     (*if*) TermC.is_num b (*else*);
 
   104 
   104 
   105 
   105 
   106 "----------- fun ist_monom ---------------------------------------------------------------------";
 
   106 "----------- fun ist_monom ---------------------------------------------------------------------";
 
   107 "----------- fun ist_monom ---------------------------------------------------------------------";
 
   107 "----------- fun ist_monom ---------------------------------------------------------------------";
 
   108 "----------- fun ist_monom ---------------------------------------------------------------------";
 
   108 "----------- fun ist_monom ---------------------------------------------------------------------";
 
   109 val t = TermC.str2term "0 ::real";
 
   109 val t = TermC.parse_test @{context} "0 ::real";
 
   110  if ist_monom t then () else error "ist_monom 1";
 
   110  if ist_monom t then () else error "ist_monom 1";
 
   111 
   111 
   112 val t = TermC.str2term "a";
 
   112 val t = TermC.parse_test @{context} "a";
 
   113 if ist_monom t then () else error "ist_monom 2";
 
   113 if ist_monom t then () else error "ist_monom 2";
 
   114 
   114 
   115 val t = TermC.str2term "2 * a";
 
   115 val t = TermC.parse_test @{context} "2 * a";
 
   116 if ist_monom t then () else error "ist_monom 3";
 
   116 if ist_monom t then () else error "ist_monom 3";
 
   117 
   117 
   118 val t = TermC.str2term "2 * a * b";
 
   118 val t = TermC.parse_test @{context} "2 * a * b";
 
   119 if ist_monom t then () else error "ist_monom 4";
 
   119 if ist_monom t then () else error "ist_monom 4";
 
   120 
   120 
   121 val t = TermC.str2term "a * b";
 
   121 val t = TermC.parse_test @{context} "a * b";
 
   122 if ist_monom t then () else error "ist_monom 5";
 
   122 if ist_monom t then () else error "ist_monom 5";
 
   123 
   123 
   124 (*not covered before NEW numerals*)
 
   124 (*not covered before NEW numerals*)
 
   125 val t = TermC.str2term "2 * a \<up> 2 * b";
 
   125 val t = TermC.parse_test @{context} "2 * a \<up> 2 * b";
 
   126 if ist_monom t then () else error "ist_monom 6";
 
   126 if ist_monom t then () else error "ist_monom 6";
 
   127 
   127 
   128 (*not covered before NEW numerals*)
 
   128 (*not covered before NEW numerals*)
 
   129 val t = TermC.str2term "a \<up> 2 * b \<up> 3";
 
   129 val t = TermC.parse_test @{context} "a \<up> 2 * b \<up> 3";
 
   130 if ist_monom t then () else error "ist_monom 7";
 
   130 if ist_monom t then () else error "ist_monom 7";
 
   131 
   131 
   132 val t = TermC.str2term "a \<up> 2 * 4 * b \<up> 3 * 5";
 
   132 val t = TermC.parse_test @{context} "a \<up> 2 * 4 * b \<up> 3 * 5";
 
   133 if ist_monom t then () else error "ist_monom 8";
 
   133 if ist_monom t then () else error "ist_monom 8";
 
   134 
   134 
   135 
   135 
   136 "----------- fun eval_ist_monom ----------------------------------";
 
   136 "----------- fun eval_ist_monom ----------------------------------";
 
   137 "----------- fun eval_ist_monom ----------------------------------";
 
   137 "----------- fun eval_ist_monom ----------------------------------";
 
   138 "----------- fun eval_ist_monom ----------------------------------";
 
   138 "----------- fun eval_ist_monom ----------------------------------";
 
   139 case eval_ist_monom 0 0 (TermC.str2term "12 ist_monom") 0 of
 
   139 case eval_ist_monom 0 0 (TermC.parse_test @{context} "12 ist_monom") 0 of
 
   140     SOME ("12 ist_monom = True", _) => ()
 
   140     SOME ("12 ist_monom = True", _) => ()
 
   141   | _ => error "polyminus.sml: 12 ist_monom = True";
 
   141   | _ => error "polyminus.sml: 12 ist_monom = True";
 
   142 
   142 
   143 case eval_ist_monom 0 0 (TermC.str2term "a ist_monom") 0 of
 
   143 case eval_ist_monom 0 0 (TermC.parse_test @{context} "a ist_monom") 0 of
 
   144     SOME ("a ist_monom = True", _) => ()
 
   144     SOME ("a ist_monom = True", _) => ()
 
   145   | _ => error "polyminus.sml: a ist_monom = True";
 
   145   | _ => error "polyminus.sml: a ist_monom = True";
 
   146 
   146 
   147 case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of
 
   147 case eval_ist_monom 0 0 (TermC.parse_test @{context} "(3*a) ist_monom") 0 of
 
   148     SOME ("3 * a ist_monom = True", _) => ()
 
   148     SOME ("3 * a ist_monom = True", _) => ()
 
   149   | _ => error "polyminus.sml: 3 * a ist_monom = True";
 
   149   | _ => error "polyminus.sml: 3 * a ist_monom = True";
 
   150 
   150 
   151 case eval_ist_monom 0 0 (TermC.str2term "(a \<up> 2) ist_monom") 0 of 
   151 case eval_ist_monom 0 0 (TermC.parse_test @{context} "(a \<up> 2) ist_monom") 0 of 
   152    SOME ("a \<up> 2 ist_monom = True", _) => ()
 
   152    SOME ("a \<up> 2 ist_monom = True", _) => ()
 
   153   | _ => error "polyminus.sml: a \<up> 2 ist_monom = True";
 
   153   | _ => error "polyminus.sml: a \<up> 2 ist_monom = True";
 
   154 
   154 
   155 case eval_ist_monom 0 0 (TermC.str2term "(3*a \<up> 2) ist_monom") 0 of
 
   155 case eval_ist_monom 0 0 (TermC.parse_test @{context} "(3*a \<up> 2) ist_monom") 0 of
 
   156     SOME ("3 * a \<up> 2 ist_monom = True", _) => ()
 
   156     SOME ("3 * a \<up> 2 ist_monom = True", _) => ()
 
   157   | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True";
 
   157   | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True";
 
   158 
   158 
   159 case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of
 
   159 case eval_ist_monom 0 0 (TermC.parse_test @{context} "(a*b) ist_monom") 0 of
 
   160     SOME ("a * b ist_monom = True", _) => ()
 
   160     SOME ("a * b ist_monom = True", _) => ()
 
   161   | _ => error "polyminus.sml: a*b ist_monom = True";
 
   161   | _ => error "polyminus.sml: a*b ist_monom = True";
 
   162 
   162 
   163 case eval_ist_monom 0 0 (TermC.str2term "(3*a*b) ist_monom") 0 of
 
   163 case eval_ist_monom 0 0 (TermC.parse_test @{context} "(3*a*b) ist_monom") 0 of
 
   164     SOME ("3 * a * b ist_monom = True", _) => ()
 
   164     SOME ("3 * a * b ist_monom = True", _) => ()
 
   165   | _ => error "polyminus.sml: 3*a*b ist_monom = True";
 
   165   | _ => error "polyminus.sml: 3*a*b ist_monom = True";
 
   166 
   166 
   167 
   167 
   168 "----------- watch order_add_mult  -------------------------------";
 
   168 "----------- watch order_add_mult  -------------------------------";
 
   169 "----------- watch order_add_mult  -------------------------------";
 
   169 "----------- watch order_add_mult  -------------------------------";
 
   170 "----------- watch order_add_mult  -------------------------------";
 
   170 "----------- watch order_add_mult  -------------------------------";
 
   171 "----- with these simple variables it works...";
 
   171 "----- with these simple variables it works...";
 
   172 val ctxt = @{context};
 
   172 val ctxt = @{context};
 
   173 val t = TermC.str2term "((a + d) + c) + b";
 
   173 val t = TermC.parse_test @{context} "((a + d) + c) + b";
 
   174 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
 
   174 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
 
   175 if UnparseC.term t = "a + (b + (c + d))" then ()
 
   175 if UnparseC.term t = "a + (b + (c + d))" then ()
 
   176 else error "polyminus.sml 1 watch order_add_mult";
 
   176 else error "polyminus.sml 1 watch order_add_mult";
 
   177 
   177 
   178 "----- the same stepwise...";
 
   178 "----- the same stepwise...";
 
   179 val od = ord_make_polynomial true (@{theory "Poly"});
 
   179 val od = ord_make_polynomial true (@{theory "Poly"});
 
   180 val t = TermC.str2term "((a + d) + c) + b";
 
   180 val t = TermC.parse_test @{context} "((a + d) + c) + b";
 
   181 "((a + d) + c) + b"; 
   181 "((a + d) + c) + b"; 
   182 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
 
   182 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
 
   183 "b + ((a + d) + c)";
 
   183 "b + ((a + d) + c)";
 
   184 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
 
   184 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t; UnparseC.term t;
 
   185 "b + (c + (a + d))";
 
   185 "b + (c + (a + d))";
 
   189 "a + (b + (c + d))";
 
   189 "a + (b + (c + d))";
 
   190 if UnparseC.term t = "a + (b + (c + d))" then ()
 
   190 if UnparseC.term t = "a + (b + (c + d))" then ()
 
   191 else error "polyminus.sml 2 watch order_add_mult";
 
   191 else error "polyminus.sml 2 watch order_add_mult";
 
   192 
   192 
   193 "----- if parentheses are right, left_commute is (almost) sufficient...";
 
   193 "----- if parentheses are right, left_commute is (almost) sufficient...";
 
   194 val t = TermC.str2term "a + (d + (c + b))";
 
   194 val t = TermC.parse_test @{context} "a + (d + (c + b))";
 
   195 "a + (d + (c + b))";
 
   195 "a + (d + (c + b))";
 
   196 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
 
   196 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
 
   197 "a + (c + (d + b))";
 
   197 "a + (c + (d + b))";
 
   198 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
 
   198 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.commute} t;UnparseC.term t;
 
   199 "a + (c + (b + d))";
 
   199 "a + (c + (b + d))";
 
   200 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
 
   200 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty true @{thm add.left_commute} t;UnparseC.term t;
 
   201 "a + (b + (c + d))";
 
   201 "a + (b + (c + d))";
 
   202 
   202 
   203 "----- but we do not want the parentheses at right; thus: cond.rew.";
 
   203 "----- but we do not want the parentheses at right; thus: cond.rew.";
 
   204 "WN0712707 complicated monomials do not yet work ...";
 
   204 "WN0712707 complicated monomials do not yet work ...";
 
   205 val t = TermC.str2term "((5*a + 4*d) + 3*c) + 2*b";
 
   205 val t = TermC.parse_test @{context} "((5*a + 4*d) + 3*c) + 2*b";
 
   206 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
 
   206 val SOME (t,_) = rewrite_set_ ctxt false order_add_mult t; UnparseC.term t;
 
   207 if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
 
   207 if UnparseC.term t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()
 
   208 else error "polyminus.sml: order_add_mult changed";
 
   208 else error "polyminus.sml: order_add_mult changed";
 
   209 
   209 
   210 "----- here we see rew_sub going into subterm with ord.rew....";
 
   210 "----- here we see rew_sub going into subterm with ord.rew....";
 
   211 val od = ord_make_polynomial false (@{theory "Poly"});
 
   211 val od = ord_make_polynomial false (@{theory "Poly"});
 
   212 val t = TermC.str2term "b + a + c + d";
 
   212 val t = TermC.parse_test @{context} "b + a + c + d";
 
   213 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
 
   213 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
 
   214 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
 
   214 val SOME (t,_) = rewrite_ ctxt od Rule_Set.empty false @{thm add.commute} t; UnparseC.term t;
 
   215 (*@@@ rew_sub gosub: t = d + (b + a + c)
 
   215 (*@@@ rew_sub gosub: t = d + (b + a + c)
 
   216   @@@ rew_sub begin: t = b + a + c*)
 
   216   @@@ rew_sub begin: t = b + a + c*)
 
   217 
   217 
   223 "ba" < "ab";
 
   223 "ba" < "ab";
 
   224 "123" < "a"; (*unused due to ---vvv*)
 
   224 "123" < "a"; (*unused due to ---vvv*)
 
   225 "12" < "3"; (*true !!!*)
 
   225 "12" < "3"; (*true !!!*)
 
   226 
   226 
   227 " a kleiner b ==> (b + a) = (a + b)";
 
   227 " a kleiner b ==> (b + a) = (a + b)";
 
   228 TermC.str2term "aaa";
 
   228 TermC.parse_test @{context} "aaa";
 
   229 TermC.str2term "222 * aaa";
 
   229 TermC.parse_test @{context} "222 * aaa";
 
   230 
   230 
   231 case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
 
   231 case eval_kleiner 0 0 (TermC.parse_test @{context} "123 kleiner 32") 0 of
 
   232     SOME ("123 kleiner 32 = False", _) => ()
 
   232     SOME ("123 kleiner 32 = False", _) => ()
 
   233   | _ => error "polyminus.sml: 12 kleiner 9 = False";
 
   233   | _ => error "polyminus.sml: 12 kleiner 9 = False";
 
   234 
   234 
   235 case eval_kleiner 0 0 (TermC.str2term "a kleiner b") 0 of
 
   235 case eval_kleiner 0 0 (TermC.parse_test @{context} "a kleiner b") 0 of
 
   236     SOME ("a kleiner b = True", _) => ()
 
   236     SOME ("a kleiner b = True", _) => ()
 
   237   | _ => error "polyminus.sml: a kleiner b = True";
 
   237   | _ => error "polyminus.sml: a kleiner b = True";
 
   238 
   238 
   239 case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of
 
   239 case eval_kleiner 0 0 (TermC.parse_test @{context} "(10*g) kleiner f") 0 of
 
   240     SOME ("10 * g kleiner f = False", _) => ()
 
   240     SOME ("10 * g kleiner f = False", _) => ()
 
   241   | _ => error "polyminus.sml: 10 * g kleiner f = False";
 
   241   | _ => error "polyminus.sml: 10 * g kleiner f = False";
 
   242 
   242 
   243 case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
 
   243 case eval_kleiner 0 0 (TermC.parse_test @{context} "(a \<up> 2) kleiner b") 0 of
 
   244     SOME ("a \<up> 2 kleiner b = True", _) => ()
 
   244     SOME ("a \<up> 2 kleiner b = True", _) => ()
 
   245   | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
 
   245   | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
 
   246 
   246 
   247 case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
 
   247 case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a \<up> 2) kleiner b") 0 of
 
   248     SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
 
   248     SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
 
   249   | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
 
   249   | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
 
   250 
   250 
   251 case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
 
   251 case eval_kleiner 0 0 (TermC.parse_test @{context} "(a*b) kleiner c") 0 of
 
   252     SOME ("a * b kleiner c = True", _) => ()
 
   252     SOME ("a * b kleiner c = True", _) => ()
 
   253   | _ => error "polyminus.sml: a * b kleiner b = True";
 
   253   | _ => error "polyminus.sml: a * b kleiner b = True";
 
   254 
   254 
   255 case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of
 
   255 case eval_kleiner 0 0 (TermC.parse_test @{context} "(3*a*b) kleiner c") 0 of
 
   256     SOME ("3 * a * b kleiner c = True", _) => ()
 
   256     SOME ("3 * a * b kleiner c = True", _) => ()
 
   257   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
 
   257   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";
 
   258 
   258 
   259 "======= compare tausche_plus with real_num_collect";
 
   259 "======= compare tausche_plus with real_num_collect";
 
   260 val od = Rewrite_Ord.function_empty;
 
   260 val od = Rewrite_Ord.function_empty;
 
   261 
   261 
   262 val erls = erls_ordne_alphabetisch;
 
   262 val erls = erls_ordne_alphabetisch;
 
   263 val t = TermC.str2term "b + a";
 
   263 val t = TermC.parse_test @{context} "b + a";
 
   264 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
 
   264 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
 
   265 if UnparseC.term t = "a + b" then ()
 
   265 if UnparseC.term t = "a + b" then ()
 
   266 else error "polyminus.sml: ordne_alphabetisch1 b + a";
 
   266 else error "polyminus.sml: ordne_alphabetisch1 b + a";
 
   267 
   267 
   268 val erls = Atools_erls;
 
   268 val erls = Atools_erls;
 
   269 val t = TermC.str2term "2*a + 3*a";
 
   269 val t = TermC.parse_test @{context} "2*a + 3*a";
 
   270 val SOME (t,_) = rewrite_ ctxt od erls false @{thm real_num_collect} t; UnparseC.term t;
 
   270 val SOME (t,_) = rewrite_ ctxt od erls false @{thm real_num_collect} t; UnparseC.term t;
 
   271 
   271 
   272 "======= test rewrite_, rewrite_set_";
 
   272 "======= test rewrite_, rewrite_set_";
 
   273 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   273 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   274 val erls = erls_ordne_alphabetisch;
 
   274 val erls = erls_ordne_alphabetisch;
 
   275 val t = TermC.str2term "b + a";
 
   275 val t = TermC.parse_test @{context} "b + a";
 
   276 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   276 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   277 if UnparseC.term t = "a + b" then ()
 
   277 if UnparseC.term t = "a + b" then ()
 
   278 else error "polyminus.sml: ordne_alphabetisch a + b";
 
   278 else error "polyminus.sml: ordne_alphabetisch a + b";
 
   279 
   279 
   280 val t = TermC.str2term "2*b + a";
 
   280 val t = TermC.parse_test @{context} "2*b + a";
 
   281 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   281 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   282 if UnparseC.term t = "a + 2 * b" then ()
 
   282 if UnparseC.term t = "a + 2 * b" then ()
 
   283 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
 
   283 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";
 
   284 
   284 
   285 val t = TermC.str2term "a + c + b";
 
   285 val t = TermC.parse_test @{context} "a + c + b";
 
   286 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   286 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   287 if UnparseC.term t = "a + b + c" then ()
 
   287 if UnparseC.term t = "a + b + c" then ()
 
   288 else error "polyminus.sml: ordne_alphabetisch a + b + c";
 
   288 else error "polyminus.sml: ordne_alphabetisch a + b + c";
 
   289 
   289 
   290 "======= rewrite goes into subterms";
 
   290 "======= rewrite goes into subterms";
 
   291 val t = TermC.str2term "a + c + b + d ::real";
 
   291 val t = TermC.parse_test @{context} "a + c + b + d ::real";
 
   292 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
 
   292 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus_plus} t; UnparseC.term t;
 
   293 if UnparseC.term t = "a + b + c + d" then ()
 
   293 if UnparseC.term t = "a + b + c + d" then ()
 
   294 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
 
   294 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";
 
   295 
   295 
   296 val t = TermC.str2term "a + c + d + b";
 
   296 val t = TermC.parse_test @{context} "a + c + d + b";
 
   297 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   297 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; UnparseC.term t;
 
   298 if UnparseC.term t = "a + b + c + d" then ()
 
   298 if UnparseC.term t = "a + b + c + d" then ()
 
   299 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
 
   299 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";
 
   300 
   300 
   301 "======= here we see rew_sub going into subterm with cond.rew....";
 
   301 "======= here we see rew_sub going into subterm with cond.rew....";
 
   302 val t = TermC.str2term "b + a + c + d";
 
   302 val t = TermC.parse_test @{context} "b + a + c + d";
 
   303 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
 
   303 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t;
 
   304 if UnparseC.term t = "a + b + c + d" then ()
 
   304 if UnparseC.term t = "a + b + c + d" then ()
 
   305 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
 
   305 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
 
   306 
   306 
   307 "======= compile rls for the most complicated terms";
 
   307 "======= compile rls for the most complicated terms";
 
   308 val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
 
   308 val t = TermC.parse_test @{context} "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
 
   309 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
 
   309 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
 
   310 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; 
   310 val SOME (t,_) = rewrite_set_ ctxt false ordne_alphabetisch t; 
   311 if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
 
   311 if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
 
   312 then () else error "polyminus.sml: ordne_alphabetisch finished";
 
   312 then () else error "polyminus.sml: ordne_alphabetisch finished";
 
   313 
   313 
   314 
   314 
   315 
   315 
   316 "----------- build fasse_zusammen --------------------------------";
 
   316 "----------- build fasse_zusammen --------------------------------";
 
   317 "----------- build fasse_zusammen --------------------------------";
 
   317 "----------- build fasse_zusammen --------------------------------";
 
   318 "----------- build fasse_zusammen --------------------------------";
 
   318 "----------- build fasse_zusammen --------------------------------";
 
   319 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
 
   319 val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";
 
   320 val SOME (t,_) = rewrite_set_ ctxt false fasse_zusammen t;
 
   320 val SOME (t,_) = rewrite_set_ ctxt false fasse_zusammen t;
 
   321 if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
 
   321 if UnparseC.term t = "3 + - 2 * e + 2 * f + 2 * g" then ()
 
   322 else error "polyminus.sml: fasse_zusammen finished";
 
   322 else error "polyminus.sml: fasse_zusammen finished";
 
   323 
   323 
   324 "----------- build verschoenere ----------------------------------";
 
   324 "----------- build verschoenere ----------------------------------";
 
   325 "----------- build verschoenere ----------------------------------";
 
   325 "----------- build verschoenere ----------------------------------";
 
   326 "----------- build verschoenere ----------------------------------";
 
   326 "----------- build verschoenere ----------------------------------";
 
   327 val t = TermC.str2term "3 + - 2 * e + 2 * f + 2 * g";
 
   327 val t = TermC.parse_test @{context} "3 + - 2 * e + 2 * f + 2 * g";
 
   328 val SOME (t,_) = rewrite_set_ ctxt false verschoenere t;
 
   328 val SOME (t,_) = rewrite_set_ ctxt false verschoenere t;
 
   329 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
 
   329 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
 
   330 else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
 
   330 else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
 
   331 
   331 
   332 
   332 
   522 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
 
   522 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
 
   523 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
 
   523 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
 
   524 "----- 2  \<up> ";
 
   524 "----- 2  \<up> ";
 
   525 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   525 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   526 val erls = erls_ordne_alphabetisch;
 
   526 val erls = erls_ordne_alphabetisch;
 
   527 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 
   527 val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 
   528 val SOME (t',_) = 
   528 val SOME (t',_) = 
   529     rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t;
 
   529     rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t;
 
   530 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
 
   530 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
 
   531 
   531 
   532 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 
   532 val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 
   533 val NONE = 
   533 val NONE = 
   534     rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t;
 
   534     rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t;
 
   535 
   535 
   536 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 
   536 val t = TermC.parse_test @{context} "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
 
   537 val SOME (t',_) = 
   537 val SOME (t',_) = 
   538     rewrite_set_ ctxt false ordne_alphabetisch t;
 
   538     rewrite_set_ ctxt false ordne_alphabetisch t;
 
   539 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
 
   539 UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
 
   540 
   540 
   541 
   541 
   596 "----------- pbl binom polynom vereinfachen p.39 -----------------";
 
   596 "----------- pbl binom polynom vereinfachen p.39 -----------------";
 
   597 "----------- pbl binom polynom vereinfachen p.39 -----------------";
 
   597 "----------- pbl binom polynom vereinfachen p.39 -----------------";
 
   598 "----------- pbl binom polynom vereinfachen p.39 -----------------";
 
   598 "----------- pbl binom polynom vereinfachen p.39 -----------------";
 
   599 val thy = @{theory};
 
   599 val thy = @{theory};
 
   600 val rls = klammern_ausmultiplizieren;
 
   600 val rls = klammern_ausmultiplizieren;
 
   601 val t = TermC.str2term "(3 * a + 2) * (4 * a - 1::real)";
 
   601 val t = TermC.parse_test @{context} "(3 * a + 2) * (4 * a - 1::real)";
 
   602 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   602 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   603 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
 
   603 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";
 
   604 val rls = discard_parentheses;
 
   604 val rls = discard_parentheses;
 
   605 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   605 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   606 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
 
   606 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";
 
   607 val rls = ordne_monome;
 
   607 val rls = ordne_monome;
 
   608 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   608 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   609 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
 
   609 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";
 
   610 (*
 
   610 (*
 
   611 val t = TermC.str2term "3 * a * 4 * a";
 
   611 val t = TermC.parse_test @{context} "3 * a * 4 * a";
 
   612 val rls = ordne_monome;
 
   612 val rls = ordne_monome;
 
   613 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   613 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   614 *)
 
   614 *)
 
   615 val rls = klammern_aufloesen;
 
   615 val rls = klammern_aufloesen;
 
   616 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   616 val SOME (t,_) = rewrite_set_ ctxt false rls t; UnparseC.term t;
 
   662 val matches = Refine.refine_PIDE @{context} fmz ["vereinfachen"];
 
   662 val matches = Refine.refine_PIDE @{context} fmz ["vereinfachen"];
 
   663 (*default_print_depth 3;*)
 
   663 (*default_print_depth 3;*)
 
   664 
   664 
   665 "----- go into details, if it seems not to work -----";
 
   665 "----- go into details, if it seems not to work -----";
 
   666 "--- does the predicate evaluate correctly ?";
 
   666 "--- does the predicate evaluate correctly ?";
 
   667 val t = TermC.str2term 
   667 val t = TermC.parse_patt_test @{theory} 
   668 	    "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
 
   668 	    "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
 
   669 val ma = eval_matchsub "" "Prog_Expr.matchsub" t ctxt;
 
   669 val ma = eval_matchsub "" "Prog_Expr.matchsub" t ctxt;
 
   670 case ma of
 
   670 case ma of
 
   671     SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
 
   671     SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
 
   672 	  \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
 
   672 	  \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
 
   686 	      (*"(~ False) = True"*)];
 
   686 	      (*"(~ False) = True"*)];
 
   687 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   687 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   688 val SOME (t', _) = rewrite_set_ ctxt false prls t;
 
   688 val SOME (t', _) = rewrite_set_ ctxt false prls t;
 
   689 
   689 
   690 "--- does the respective prls rewrite the whole predicate ?";
 
   690 "--- does the respective prls rewrite the whole predicate ?";
 
   691 val t = TermC.str2term 
   691 val t = TermC.parse_patt_test @{theory}
 
   692 	    "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
 
   692 	    "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \
 
   693 	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
 
   693 	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
 
   694 	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
 
   694 	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
 
   695 	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
 
   695 	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
 
   696 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
 
   696 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
wneuper/isa