1.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml	Tue Jul 13 15:28:43 2021 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml	Thu Jul 15 14:10:18 2021 +0200
     1.3 @@ -62,7 +62,6 @@
     1.4  fun trace_eq2 i str thy t t' =
     1.5    trace i (" " ^ str ^ ": \"" ^
     1.6      UnparseC.term_in_thy thy t ^ "\" > \"" ^ UnparseC.term_in_thy thy t' ^ "\"");
     1.7 -
     1.8  fun trace1 i str =
     1.9    if ! trace_on andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
    1.10  fun trace_in1 i str thmid =
    1.11 @@ -89,24 +88,19 @@
    1.12    (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
    1.13  and rew_sub thy i bdv tless rls put_asm lrd r t = 
    1.14    (let
    1.15 -(** )val _ = @{print}{a = "@ rew_sub: 1 < ?n \<Longrightarrow> NTH ?n..", r = UnparseC.term r};( *TODOO*)
    1.16      val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
    1.17 -(** )val _ = @{print}{a = "@ rew_sub NO: patterns..", lhs = UnparseC.term lhs, rhs = UnparseC.term rhs};( *TODOO*)
    1.18      val r' = (Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r)
    1.19        handle Pattern.MATCH => raise NO_REWRITE
    1.20 -(** )val _ = @{print}{a = "@ Envir.subst_term: OK gives (3 + - 1)", r' = UnparseC.term r'};( *TODOO*)
    1.21      val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
    1.22      val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
    1.23      val _ = trace_in2 i "eval asms" thy r';
    1.24 -(** )val _ = @{print}{a = "@ eval asms", r' = UnparseC.term r'};( *TODOO*)
    1.25      val (t'', p'') =                                                      (*conditional rewriting*)
    1.26        let val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls 	     
    1.27 -(** )val _ = @{print}{a = "@ eval__true asms", simpl_p' = UnparseC.terms simpl_p', nofalse = nofalse};( *TODOO*)
    1.28  	    in
    1.29  	      if nofalse
    1.30 -        then (trace_in4 i "asms accepted" thy p' simpl_p'; (t',simpl_p'))(* uncond.rew.from above*)
    1.31 +        then (trace_in4 i "asms accepted" thy p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)
    1.32          else (trace_in5 i "asms false" thy p'; raise NO_REWRITE)   (* don't go into subtm.of cond*)
    1.33 -	    end
    1.34 +	    end                                    
    1.35    in
    1.36      if TermC.perm lhs rhs andalso not (tless bdv (t', t))                     (*ordered rewriting*)
    1.37      then (trace_eq2 i "not >" thy t t'; raise NO_REWRITE)
    1.38 @@ -129,7 +123,7 @@
    1.39            let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
    1.40            in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
    1.41      end)
    1.42 -and eval__true thy i asms bdv rls =           (* simplify asumptions until one evaluates to false*)
    1.43 +and eval__true thy i asms bdv rls =            (* rewrite asumptions until one evaluates to false*)
    1.44    if asms = [@{term True}] orelse asms = [] then ([], true)
    1.45    else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
    1.46      if asms = [@{term False}] then ([], false)
    1.47 @@ -256,10 +250,10 @@
    1.48          end
    1.49      end;
    1.50  
    1.51 -(* rewriting without argument [] for rew_ord;  WN110603: shouldnt asm<>[] lead to false? *)
    1.52 +(* rewriting without argument [] for rew_ord *)
    1.53  fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
    1.54  
    1.55 -(* rewriting without internal argument [] *)
    1.56 +(* rewriting without internal arguments 1, [] *)
    1.57  fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
    1.58  fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
    1.59