1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Fri Aug 23 09:32:05 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Sat Aug 24 11:18:43 2013 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  "-------- ... missing WN060103 --------------------------";
     1.5  "-------- fun monom2term,  fun poly2term' ---------------";
     1.6  "~~~~~END: decomment structure RationalI : RATIONALI ~~~~";
     1.7 +"-------- and app_rev --------------------------------------------------------";
     1.8  "-------- external calculating functions test -----------";
     1.9  "-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
    1.10  "-------- common_nominator_p ----------------------------";
    1.11 @@ -305,6 +306,86 @@
    1.12   val SOME t' = polynomial2expanded t; term2str t';
    1.13  "1 - x ^^^ 2 - 5 * x ^^^ 5";
    1.14  
    1.15 +"-------- and app_rev --------------------------------------------------------";
    1.16 +"-------- and app_rev --------------------------------------------------------";
    1.17 +"-------- and app_rev --------------------------------------------------------";
    1.18 +(* trace down until prepats are evaluated 
    1.19 +  (which does not to work, because substitution is not done -- compare rew_sub!);
    1.20 +  keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p
    1.21 +  (again) get prepat = [] changed to <>[]. *)
    1.22 +val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)";
    1.23 +
    1.24 +(*rewrite_set_ @{theory Isac} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.25 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, cancel_p, t);
    1.26 +"~~~~~ fun rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
    1.27 +  (thy, 1, bool, [], rls, term);
    1.28 +(*val (t', asm, rew) = app_rev thy (i+1) rrls t; rew = false!!!!!!!!!!!!!!!!!!!!!*)
    1.29 +"~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
    1.30 +    fun chk_prepat thy erls [] t = true
    1.31 +      | chk_prepat thy erls prepat t =
    1.32 +        let
    1.33 +          fun chk (pres, pat) =
    1.34 +            (let 
    1.35 +              val subst: Type.tyenv * Envir.tenv =
    1.36 +                Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
    1.37 +             in
    1.38 +              snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
    1.39 +             end) handle _ => false
    1.40 +           fun scan_ f [] = false (*scan_ NEVER called by []*)
    1.41 +             | scan_ f (pp::pps) =
    1.42 +               if f pp then true else scan_ f pps;
    1.43 +        in scan_ chk prepat end;
    1.44 +    (* apply the normal_form of a rev-set *)
    1.45 +    fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
    1.46 +      if chk_prepat thy erls prepat t
    1.47 +      then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
    1.48 +      else NONE;
    1.49 +(*  val opt = app_rev' thy rrls t  ..NONE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.50 +"~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
    1.51 +  (thy, rrls, t);
    1.52 +(* chk_prepat thy erls prepat t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.53 +(* app_sub thy i rrls t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.54 +"~~~~~ fun chk_prepat, args:"; val (thy, erls, prepat, t) = (thy, erls, prepat, t);
    1.55 +          fun chk (pres, pat) =
    1.56 +            (let 
    1.57 +              val subst: Type.tyenv * Envir.tenv =
    1.58 +                Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
    1.59 +             in
    1.60 +              snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
    1.61 +             end) handle _ => false
    1.62 +           fun scan_ f [] = false (*scan_ NEVER called by []*)
    1.63 +             | scan_ f (pp::pps) =
    1.64 +               if f pp then true else scan_ f pps;
    1.65 +
    1.66 +(*========== inhibit exn WN130823: (pp::pps) = [(*prepat*)] ====================================
    1.67 +(* scan_ chk prepat = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.68 +"~~~~~ fun , args:"; val (f, (pp::pps)) = (chk, prepat);
    1.69 +f;
    1.70 +val ([t1, t2], t) = pp;
    1.71 +term2str t1 = "?r is_expanded";
    1.72 +term2str t2 = "?s is_expanded";
    1.73 +term2str t = "?r / ?s";
    1.74 +(* f pp = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.75 +"~~~~~ fun chk, args:"; val (pres, pat) = (pp);
    1.76 +              val subst: Type.tyenv * Envir.tenv =
    1.77 +                Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
    1.78 +(*subst = 
    1.79 +  ({}, {(("r", 0), ("real", Var (("r", 0), "real"))), 
    1.80 +        (("s", 0), ("real", Var (("s", 0), "real")))}*)
    1.81 +;
    1.82 +              snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
    1.83 +"~~~~~ fun eval__true, args:"; val (thy, i, asms, bdv, rls) =
    1.84 +  (thy, (i + 1), (map (Envir.subst_term subst) pres), [], erls);
    1.85 +terms2str asms;                         (* = "[\"?r is_expanded\",\"?s is_expanded\"]"*)
    1.86 +asms = [@{term True}] orelse asms = []; (* = false*)
    1.87 +asms = [@{term False}]                ; (* = false*)
    1.88 +"~~~~~ fun chk, args:"; val (indets, (a::asms)) = ([], asms);
    1.89 +bdv (*= []: _a list*);
    1.90 +val bdv : (term * term) list = [];
    1.91 +rewrite__set_ thy (i+1) false;
    1.92 +term2str a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*)
    1.93 +val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a
    1.94 +============ inhibit exn WN130823: (pp::pps) = [(*prepat*)] ===================================*)
    1.95  
    1.96  "-------- external calculating functions test -----------";
    1.97  "-------- external calculating functions test -----------";