1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Wed Mar 14 17:12:43 2012 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Sat Mar 17 11:06:46 2012 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4  "----------- compare all prepat's existing 2010 ---------";
     1.5  "----------- fun app_rev, Rrls, -------------------------";
     1.6  "----------- 2011 thms with axclasses -------------------";
     1.7 +"----------- repair NO asms from rls RatEq_eliminate ----";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -505,3 +506,38 @@
    1.12      (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
    1.13  val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
    1.14  
    1.15 +"----------- repair NO asms from rls RatEq_eliminate ----";
    1.16 +"----------- repair NO asms from rls RatEq_eliminate ----";
    1.17 +"----------- repair NO asms from rls RatEq_eliminate ----";
    1.18 +val t = str2term "1 / x = 5";
    1.19 +trace_rewrite := true;
    1.20 +val SOME (t', asm) = rewrite_ thy e_rew_ord e_rls true @{thm rat_mult_denominator_right} t;
    1.21 +term2str t' = "1 = 5 * x";
    1.22 +terms2str asm = "[\"x ~= 0\"]";
    1.23 +(*
    1.24 + ##  eval asms: x ~= 0 ==> (1 / x = 5) = (1 = 5 * x) 
    1.25 + ###  rls: e_rls on: x ~= 0 
    1.26 + ##  asms accepted: ["x ~= 0"]   stored: ["x ~= 0"] 
    1.27 +*)
    1.28 +trace_rewrite := false;
    1.29 +
    1.30 +trace_rewrite := true;
    1.31 +val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)
    1.32 +term2str t' = "1 = 5 * x";
    1.33 +(*
    1.34 + :
    1.35 + ####  rls: rateq_erls on: x ~= 0 
    1.36 + :
    1.37 + #####  try calc: HOL.eq'    <<<------------------------------- here the error comes from
    1.38 + =====  calc. to: ~ False 
    1.39 + #####  try calc: HOL.eq' 
    1.40 + #####  try thm: not_true 
    1.41 + #####  try thm: not_false 
    1.42 + =====  rewrites to: True 
    1.43 + :
    1.44 + ###  asms accepted: ["x ~= 0"]   stored: []
    1.45 + :
    1.46 +*)
    1.47 +trace_rewrite := false;
    1.48 +(* WN120317.TODO dropped rateq: the above error is the same in 2002 *)
    1.49 +