1.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Wed Feb 07 15:00:37 2018 +0100
     1.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Thu Feb 08 12:49:52 2018 +0100
     1.3 @@ -62,9 +62,9 @@
     1.4  "===== rewriting: prep insertion into rew_sub";
     1.5  val thy = @{theory Complex_Main};
     1.6  val ctxt = @{context};
     1.7 -val thm =  @{thm nonzero_mult_divide_cancel_right};
     1.8 +val thm =  @{thm nonzero_divide_mult_cancel_right};
     1.9  val r = Thm.prop_of thm;
    1.10 -val tm = @{term "x*2 / 2::real"};
    1.11 +val tm = @{term "x / (2 * x)::real"};
    1.12  "----- and rew_sub";
    1.13  val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.14                    o Logic.strip_imp_concl) r;
    1.15 @@ -124,9 +124,9 @@
    1.16  "===== prepr cond.rew. with Pattern.match";
    1.17  val thy = @{theory Complex_Main};
    1.18  val ctxt = @{context};
    1.19 -val thm =  @{thm nonzero_mult_divide_cancel_right};
    1.20 +val thm =  @{thm nonzero_divide_mult_cancel_right};
    1.21  val rule = Thm.prop_of thm;
    1.22 -val tm = @{term "x*2 / 2::real"};
    1.23 +val tm = @{term "x / (2 * x)::real"};
    1.24  
    1.25  val prem = Logic.strip_imp_prems rule;
    1.26  val nps = Logic.count_prems rule;
    1.27 @@ -145,14 +145,15 @@
    1.28  
    1.29  "----- conditional rewriting creating an assumption";
    1.30  "----- conditional rewriting creating an assumption";
    1.31 -val tm = @{term "x*y / y::real"};
    1.32 +val thm =  @{thm nonzero_divide_mult_cancel_right};
    1.33 +val tm = @{term "x / (2 * x)::real"};
    1.34  val SOME (rew, asm) = (rewrite_ thy dummy_ord e_rls false thm tm)
    1.35    handle _ => error "rewrite.sml diff.behav. in cond.rew.";
    1.36  
    1.37 -if rew = @{term "x::real"} then () (* the rewrite is _NO_ Trueprop *)
    1.38 +if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
    1.39  else error "rewrite.sml diff.result in cond.rew.";
    1.40  
    1.41 -if hd asm = @{term "~ y = (0::real)"} (* dropped Trueprop $ ...*)
    1.42 +if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
    1.43  then () else error "rewrite.sml diff.asm in cond.rew.";
    1.44  "----- conditional rewriting immediately: can only be done with ";
    1.45  "------Isabelle numerals, because erls cannot handle them yet.";
    1.46 @@ -162,7 +163,7 @@
    1.47  "----------- step through 'and rew_sub': ----------------";
    1.48  "----------- step through 'and rew_sub': ----------------";
    1.49  (*and make asms without Trueprop, beginning with the result:*)
    1.50 -val tm = @{term "x*y / y::real"};
    1.51 +val tm = @{term "x / (2 * x)::real"};
    1.52  val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord e_rls true [] (Thm.prop_of thm) tm;
    1.53  (*show_types := false;*)
    1.54  "----- evaluate arguments";
    1.55 @@ -171,27 +172,27 @@
    1.56  "----- step 1: LHS, RHS of rule";
    1.57       val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
    1.58                         o Logic.strip_imp_concl) r;
    1.59 -term2str r = "?b ~= (0::?'a) ==> ?a * ?b / ?b = ?a";
    1.60 -term2str LHS = "?a * ?b / ?b"; term2str RHS = "?a";
    1.61 +term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
    1.62 +term2str LHS = "?b / (?a * ?b)"; term2str RHS = "(1::?'a) / ?a";
    1.63  "----- step 2: the rule instantiated";
    1.64       val r' = Envir.subst_term 
    1.65                    (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
    1.66 -term2str r' = "y ~= 0 ==> x * y / y = x";
    1.67 +term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
    1.68  "----- step 3: get the (instantiated) assumption(s)";
    1.69       val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
    1.70 -term2str (hd p') = "y ~= 0";
    1.71 +term2str (hd p') = "x \<noteq> 0";
    1.72  "=====vvv make asms without Trueprop ---vvv";
    1.73       val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) 
    1.74                                               (Logic.count_prems r', [], r'));
    1.75  case p' of
    1.76 -    [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) $ Free ("y", _) $
    1.77 -                               Const ("Groups.zero_class.zero", _))] => ()
    1.78 +    [Const ("HOL.Not", _) $ (Const ("HOL.eq", _) 
    1.79 +      $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
    1.80    | _ => error "rewrite.sml assumption changed";
    1.81  "=====^^^ make asms without Trueprop ---^^^";
    1.82  "----- step 4: get the (instantiated) RHS";
    1.83       val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop 
    1.84                 o Logic.strip_imp_concl) r';
    1.85 -term2str t' = "x";
    1.86 +term2str t' = "1 / 2";
    1.87  
    1.88  "----------- step through 'fun rewrite_terms_'  ---------";
    1.89  "----------- step through 'fun rewrite_terms_'  ---------";