# HG changeset patch # User Walther Neuper # Date 1378131368 -7200 # Node ID c3f399ce32af17c516a14858d7360b7165fd3a10 # Parent 0831a4a6ec8a1664c5d622347eb9d5137e02ea87 Test_Isac works again, almost .. 4 files raise errors: # Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2" # Interpret/inform.sml: "inform.sml: [rational,simplification] 2" # Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result" # Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed" The chunk of changes is due to the fact, that Isac's code still is unstable. The changes are accumulated since e8f46493af82. diff -r 0831a4a6ec8a -r c3f399ce32af src/Tools/isac/Knowledge/GCD_Poly_ML.thy --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 16:16:08 2013 +0200 @@ -374,15 +374,15 @@ in try_new_prime_up a b d M P g p end end - (* HENSEL_lifting_up :: unipoly \ unipoly \ int \ int \ int \ unipoly - HENSEL_lifting_up p1 p2 d M p = gcd + (* iterate_CHINESE_up :: unipoly \ unipoly \ int \ int \ int \ unipoly + iterate_CHINESE_up p1 p2 d M p = gcd assumes d = gcd (lcoeff_up p1, lcoeff_up p2) \ M = LANDAU_MIGNOTTE_bound \ p = prime \ p ~| d \ p1 is primitive \ p2 is primitive yields gcd | p1 \ gcd | p2 \ gcd is primitive argumentns "a b d M p" named according to [1] p.93 *) - fun HENSEL_lifting_up a b d M p = + fun iterate_CHINESE_up a b d M p = let val p = p next_prime_not_dvd d val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p @@ -392,7 +392,7 @@ let val g = primitive_up (try_new_prime_up a b d M p g_p p) in - if (g %|% a) andalso (g %|% b) then g:unipoly else HENSEL_lifting_up a b d M p + if (g %|% a) andalso (g %|% b) then g:unipoly else iterate_CHINESE_up a b d M p end end @@ -405,7 +405,7 @@ let val d = abs (Integer.gcd (lcoeff_up a) (lcoeff_up b)) in if a = b then a else - HENSEL_lifting_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1 + iterate_CHINESE_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1 end; *} @@ -679,10 +679,10 @@ (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b')))) end - (* fn: poly -> poly -> int -> - int -> int -> int list -> poly list -> poly + (* try_new_r :: poly -> poly -> int -> int -> int -> int list -> poly list -> poly + try_new_r a b n M r r_list steps = assumes length a > 1 \ length b > 1 - yields TODO + yields TODO *) and try_new_r a b n M r r_list steps = let @@ -691,16 +691,18 @@ val g_r = gcd_poly' (order (eval a (n - 2) r)) (order (eval b (n - 2) r)) (n - 1) 0 val steps = steps @ [g_r]; - in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end - (* fn: poly -> poly -> int -> - int -> int -> int -> int list -> poly list -> - | poly -> poly -> int list -> poly + in iterate_CHINESE a b n M 1 r r_list steps g_r (zero_poly n) [1] end + + (* iterate_CHINESE :: poly -> poly -> int -> int -> int -> int -> int list -> + | poly list -> poly -> poly -> int list -> poly + iterate_CHINESE a | b n M m r r_list + steps g g_n mult = assumes length a > 1 \ length b > 1 - yields TODO + yields TODO *) - and HENSEL_lifting a b n M m r r_list steps g g_n mult = + and iterate_CHINESE a b n M m r r_list steps g g_n mult = if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else - try_new_r a b n M r r_list steps + try_new_r a b n M r r_list steps else let val r = find_new_r a b r; @@ -709,20 +711,20 @@ (order (eval b (n - 2) r)) (n - 1) 0 in if lex_ord (lmonom g) (lmonom g_r) - then HENSEL_lifting a b n M 1 r r_list steps g g_n mult - else if (lexp g) = (lexp g_r) + then iterate_CHINESE a b n M 1 r r_list steps g g_n mult + else if lexp g = lexp g_r then let val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2) in - if (nth steps (length steps - 1)) = (zero_poly (n - 1)) - then HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new - else HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new + if nth steps (length steps - 1) = zero_poly (n - 1) + then iterate_CHINESE a b n M (M + 1) r r_list steps g_r g_n new + else iterate_CHINESE a b n M (m + 1) r r_list steps g_r g_n new end else (* \ lex_ord (lmonom g) (lmonom g_r) *) - HENSEL_lifting a b n M (m + 1) r r_list steps g g_n mult + iterate_CHINESE a b n M (m + 1) r r_list steps g g_n mult end - fun majority_of_coefficients_is_negative a b c = + fun majority_of_coefficients_is_negative_in a b c = let val cs = (coeffs a) @ (coeffs b) @ (coeffs c) in length (filter (curry op < 0) cs) < length cs div 2 end @@ -736,7 +738,7 @@ val (a': poly, _) = a %%/%% c val (b': poly, _) = b %%/%% c in - if majority_of_coefficients_is_negative a' b' c + if majority_of_coefficients_is_negative_in a' b' c then ((a' %%* ~1, b' %%* ~1), c %%* ~1) (*makes results look nicer*) else ((a', b'), c) end diff -r 0831a4a6ec8a -r c3f399ce32af src/Tools/isac/Knowledge/Rational.thy --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 16:16:08 2013 +0200 @@ -105,10 +105,10 @@ because the gcd involves 2 polynomials (with the same length for their list of exponents). *) fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) = - (SOME (t |> monoms_of_term vs |> order) + (SOME (t |> monoms_of_term vs |> order) handle ERROR _ => NONE) | poly_of_term vs t = - (SOME [monom_of_term vs (1, replicate (length vs) 0) t] + (SOME [monom_of_term vs (1, replicate (length vs) 0) t] handle ERROR _ => NONE) fun is_poly t = @@ -180,6 +180,8 @@ val calc_rat_erls:rls val cancel_p : rls val cancel_p_ : theory -> term -> (term * term list) option + val check_fraction : term -> (term * term) option + val check_frac_sum : term -> ((term * term) * (term * term)) option val common_nominator_p : rls val common_nominator_p_ : theory -> term -> (term * term list) option val eval_is_expanded : string -> 'a -> term -> theory -> @@ -344,7 +346,7 @@ SOME ("a' / b'", ["b' \ 0"]). gcd_poly a b \ 1 \ gcd_poly a b \ -1 \ a' * gcd_poly a b = a \ b' * gcd_poly a b = b \ NONE *) -fun cancel_p_ (thy: theory) t = +fun cancel_p_ (_: theory) t = let val opt = check_fraction t in case opt of @@ -377,51 +379,49 @@ end end -(* addition of fractions allows (at most) one non-fraction ---postponed after 1st integration*) -fun norm_frac_sum +(* addition of fractions allows (at most) one non-fraction (a monomial) *) +fun check_frac_sum (Const ("Groups.plus_class.plus", _) $ (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $ (Const ("Fields.inverse_class.divide", _) $ n2 $ d2)) = SOME ((n1, d1), (n2, d2)) - | norm_frac_sum + | check_frac_sum (Const ("Groups.plus_class.plus", _) $ nofrac $ (Const ("Fields.inverse_class.divide", _) $ n2 $ d2)) = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2)) - | norm_frac_sum + | check_frac_sum (Const ("Groups.plus_class.plus", _) $ (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $ nofrac) = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT))) - | norm_frac_sum _ = NONE + | check_frac_sum _ = NONE (* prepare a term for addition by providing the least common denominator as a product assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*) -fun common_nominator_p_ (thy: theory) t = - let val opt = norm_frac_sum t +fun common_nominator_p_ (_: theory) t = + let val opt = check_frac_sum t in case opt of NONE => NONE | SOME ((n1, d1), (n2, d2)) => - let - val vs = t |> vars |> map free2str |> sort string_ord - val baseT = type_of n1 - val expT = HOLogic.realT + let val vs = t |> vars |> map free2str |> sort string_ord in case (poly_of_term vs d1, poly_of_term vs d2) of (SOME a, SOME b) => let val ((a', b'), c) = gcd_poly a b - val d1' = term_of_poly baseT expT vs a' - val d2' = term_of_poly baseT expT vs b' - val c' = term_of_poly baseT expT vs c + val (baseT, expT) = (type_of n1, HOLogic.realT) + val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c] (*----- minimum of parentheses & nice result, but breaks tests: ------------- val denom = HOLogic.mk_binop "Groups.times_class.times" - (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') - --------------------------------------------------------------------------*) - val denom = HOLogic.mk_binop "Groups.times_class.times" (c', - HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) - (*--------------------------------------------------------------------------*) + (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*) + val denom = + if c = [(1, replicate (length vs) 0)] + then HOLogic.mk_binop "Groups.times_class.times" (d1', d2') + else + HOLogic.mk_binop "Groups.times_class.times" (c', + HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*) val t' = HOLogic.mk_binop "Groups.plus_class.plus" (HOLogic.mk_binop "Fields.inverse_class.divide" @@ -438,29 +438,24 @@ assumes: is a term with outmost "+" and at least one outmost "/" in respective summands NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*) fun add_fraction_p_ (thy: theory) t = - let val opt = norm_frac_sum t - in - case opt of - NONE => NONE - | SOME ((n1, d1), (n2, d2)) => - let - val vs = t |> vars |> map free2str |> sort string_ord - val baseT = type_of n1 - val expT = HOLogic.realT - in - (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of - (SOME _, SOME a, SOME _, SOME b) => - let - val ((a', b'), c) = gcd_poly a b - val nomin = term_of_poly baseT expT vs - (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a')) - val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b') - val t' = HOLogic.mk_binop "Fields.inverse_class.divide" (nomin, denom) - val asm = mk_asms baseT [denom] - in SOME (t', asm) end - | _ => NONE : (term * term list) option - end - end + case check_frac_sum t of + NONE => NONE + | SOME ((n1, d1), (n2, d2)) => + let + val vs = t |> vars |> map free2str |> sort string_ord + in + case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of + (SOME _, SOME a, SOME _, SOME b) => + let + val ((a', b'), c) = gcd_poly a b + val (baseT, expT) = (type_of n1, HOLogic.realT) + val nomin = term_of_poly baseT expT vs + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a')) + val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b') + val t' = HOLogic.mk_binop "Fields.inverse_class.divide" (nomin, denom) + in SOME (t', mk_asms baseT [denom]) end + | _ => NONE : (term * term list) option + end fun (x ins xs) = if x mem xs then xs else x :: xs; fun xs union [] = xs @@ -1708,9 +1703,6 @@ if count_neg(tl(the(term2coef' t (get_vars(t)))))=0 then true else false; -(*. checks for expanded term [3] .*) -fun is_expanded t = test_exp t " " andalso check_coeff(t); - (*WN.7.3.03 Hilfsfunktion f"ur term2poly'*) fun mk_monom v' p vs = let fun conv p (v: string) = if v'= v then p else 0 @@ -3306,7 +3298,7 @@ ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], errpatts = [], scr=Rfuns {init_state = init_state thy Atools_erls ro, - normal_form = add_fraction_p_ thy,(*FIXME.WN0211*) + normal_form = add_fraction_p_ thy, (*FIXME.WN0211*) locate_rule = locate_rule thy Atools_erls ro, next_rule = next_rule thy Atools_erls ro, attach_form = attach_form}} diff -r 0831a4a6ec8a -r c3f399ce32af src/Tools/isac/ProgLang/rewrite.sml --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 16:16:08 2013 +0200 @@ -9,6 +9,11 @@ exception NO_REWRITE; exception STOP_REW_SUB; (*WN050820 quick and dirty*) +fun trace i str = + if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else () +fun trace1 i str = + if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else () + (* Synopsis rewriting (prep for reference manual): ---------------------------------------------- @@ -114,12 +119,11 @@ and eval__true thy i asms bdv rls = if asms = [@{term True}] orelse asms = [] then ([], true) (* this allows to check Rrls with prepat = ([@{term True}], pat) *) - else if asms = [@{term False}] then ([], false) - else + else if asms = [@{term False}] then ([], false) else let fun chk indets [] = (indets, true)(*return asms<>True until false*) | chk indets (a::asms) = - (case rewrite__set_ thy (i+1) false bdv rls a of + (case rewrite__set_ thy (i + 1) false bdv rls a of NONE => (chk (indets @ [a]) asms) | SOME (t, a') => if t = @{term True} then (chk (indets @ a') asms) @@ -129,91 +133,67 @@ in chk [] asms end (* rewrite with a rule set, which must not be the empty Erls *) and rewrite__set_ _ _ __ Erls t = - error("rewrite__set_ called with 'Erls' for '"^term2str t^"'") + error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'") (* rewrite with a 'reverse rule set' implemented by ML code *) | rewrite__set_ thy i _ _ (rrls as Rrls _) t = - let val _= if ! trace_rewrite andalso i < ! depth - then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^ - (term2str t)) else () - val (t', asm, rew) = app_rev thy (i+1) rrls t - in if rew then SOME (t', distinct asm) - else NONE end + let + val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t) + val (t', asm, rew) = app_rev thy (i + 1) rrls t + in if rew then SOME (t', distinct asm) else NONE end (* rewrite with a rule set containing Thms or Calculations *) | rewrite__set_ thy i put_asm bdv rls ct = -(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term); - *) - let - datatype switch = Appl | Noap; - fun rew_once ruls asm ct Noap [] = (ct,asm) - | rew_once ruls asm ct Appl [] = - (case rls of Rls _ => rew_once ruls asm ct Noap ruls - | Seq _ => (ct,asm)) - | rew_once ruls asm ct apno (rul::thms) = -(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls); - val Thm (thmid, thm) = rul; - *) - case rul of - Thm (thmid, thm) => - (if !trace_rewrite andalso i < ! depth - then tracing((idt"#"(i+1))^" try thm: "^thmid) else (); - case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) - ((#erls o rep_rls) rls) put_asm thm ct of - NONE => rew_once ruls asm ct apno thms - | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth - then tracing((idt"="(i+1))^" rewrites to: "^ - (term2str ct')) else (); - rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms))) - | Calc (cc as (op_,_)) => - (let val _= if !trace_rewrite andalso i < ! depth then - tracing((idt"#"(i+1))^" try calc: "^op_^"'") else (); - val ct = uminus_to_string ct - in case get_calculation_ thy cc ct of - NONE => rew_once ruls asm ct apno thms - | SOME (thmid, thm') => - let - val pairopt = - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) - ((#erls o rep_rls) rls) put_asm thm' ct; - val _ = if pairopt <> NONE then () - else error("rewrite_set_, rewrite_ \""^ - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") - val _ = if ! trace_rewrite andalso i < ! depth - then tracing((idt"="(i+1))^" calc. to: "^ - (term2str ((fst o the) pairopt))) - else() - in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end - end) - | Cal1 (cc as (op_,_)) => - (let val _= if !trace_rewrite andalso i < ! depth then - tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else (); - val ct = uminus_to_string ct - in case get_calculation1_ thy cc ct of - NONE => (ct, asm) - | SOME (thmid, thm') => - let - val pairopt = - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls) - ((#erls o rep_rls) rls) put_asm thm' ct; - val _ = if pairopt <> NONE then () - else error("rewrite_set_, rewrite_ \""^ - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE") - val _ = if ! trace_rewrite andalso i < ! depth - then tracing((idt"="(i+1))^" cal1. to: "^ - (term2str ((fst o the) pairopt))) - else() - in the pairopt end - end) - | Rls_ rls' => - (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of - SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms - | NONE => rew_once ruls asm ct apno thms); - - val ruls = (#rules o rep_rls) rls; - val _= if ! trace_rewrite andalso i < ! depth - then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^ - (term2str ct)) else () - val (ct',asm') = rew_once ruls [] ct Noap ruls; - in if ct = ct' then NONE else SOME (ct', distinct asm') end + let + datatype switch = Appl | Noap; + fun rew_once ruls asm ct Noap [] = (ct, asm) + | rew_once ruls asm ct Appl [] = + (case rls of Rls _ => rew_once ruls asm ct Noap ruls + | Seq _ => (ct, asm)) + | rew_once ruls asm ct apno (rul::thms) = + case rul of + Thm (thmid, thm) => + (trace1 i (" try thm: " ^ thmid); + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls) + ((#erls o rep_rls) rls) put_asm thm ct of + NONE => rew_once ruls asm ct apno thms + | SOME (ct',asm') => + (trace1 i (" rewrites to: " ^ term2str ct'); + rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms))) + | Calc (cc as (op_, _)) => + let val _= trace1 i (" try calc: " ^ op_ ^ "'") + val ct = uminus_to_string ct + in case get_calculation_ thy cc ct of + NONE => rew_once ruls asm ct apno thms + | SOME (thmid, thm') => + let + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls) + ((#erls o rep_rls) rls) put_asm thm' ct; + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ + string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE") + val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt)) + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end + end + | Cal1 (cc as (op_, _)) => + let val _= trace1 i (" try cal1: " ^ op_ ^ "'"); + val ct = uminus_to_string ct + in case get_calculation1_ thy cc ct of + NONE => (ct, asm) + | SOME (thmid, thm') => + let + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls) + ((#erls o rep_rls) rls) put_asm thm' ct; + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^ + string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE") + val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt)) + in the pairopt end + end + | Rls_ rls' => + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms + | NONE => rew_once ruls asm ct apno thms); + val ruls = (#rules o rep_rls) rls; + val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct) + val (ct', asm') = rew_once ruls [] ct Noap ruls; + in if ct = ct' then NONE else SOME (ct', distinct asm') end (* apply an Rrls; if not applicable proceed with subterms *) and app_rev thy i rrls t = @@ -233,7 +213,7 @@ if f pp then true else scan_ f pps; in scan_ chk prepat end; (* apply the normal_form of a rev-set *) - fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t = + fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t = if chk_prepat thy erls prepat t then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t) else NONE; @@ -272,20 +252,9 @@ (*WN.11.6.03: shouldnt asm<>[] lead to false ????*) fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls; - -(*.rewriting without internal argument [] for rew_ord.*) -(* val (thy, rew_ord, erls, bool, thm, term) = - (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f); - val (thy, rew_ord, erls, bool, thm, term) = - (thy, rew_ord, erls, false, thm, t''); - *) -fun rewrite_ thy rew_ord erls bool thm term = - rewrite__ thy 1 [] rew_ord erls bool thm term; -fun rewrite_set_ thy bool rls term = -(* val (thy, bool, rls, term) = (thy, false, srls, t); - *) - rewrite__set_ thy 1 bool [] rls term; - +(* rewriting without internal argument [] *) +fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term; +fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term; fun subs'2subst thy (s:subs') = (((map (apfst (term_of o the o (parse thy)))) diff -r 0831a4a6ec8a -r c3f399ce32af src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/src/Tools/isac/calcelems.sml Mon Sep 02 16:16:08 2013 +0200 @@ -97,7 +97,7 @@ and scr = EmptyScr | Prog of term (* for met *) - | Rfuns of (* for Rrls*) + | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *) {init_state : (* initialise for reverse rewriting by the Interpreter *) term -> (* for this the rrlsstate is initialised: *) term * (* the current formula: goes locate_gen -> next_tac via istate *) @@ -194,9 +194,9 @@ val e_rule = Thm ("refl", @{thm refl}); fun id_of_thm (Thm (id, _)) = id - | id_of_thm _ = error "id_of_thm"; + | id_of_thm _ = error "error id_of_thm"; fun thm_of_thm (Thm (_, thm)) = thm - | thm_of_thm _ = error "thm_of_thm"; + | thm_of_thm _ = error "error thm_of_thm"; fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Sep 02 16:16:08 2013 +0200 @@ -1273,8 +1273,8 @@ tree and check if every node implements that what we have wanted.*} ML {* - trace_rewrite := false; - trace_script := false; + trace_rewrite := false; (*true*) + trace_script := false; (*true*) print_depth 9; val fmz = @@ -1309,6 +1309,7 @@ " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"; val (p,_,f,nxt,_,pt) = me nxt p [] pt; "SubProblem"; + print_depth 3; *} text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had @@ -1382,7 +1383,7 @@ \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok \item What is the returned formula: \begin{verbatim} -print_depth 999; f; print_depth 999; +print_depth 999; f; print_depth 3; { Find = [ Correct "solutions z_i"], With = [], Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)", diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Sep 02 16:16:08 2013 +0200 @@ -2465,7 +2465,7 @@ \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok \item What is the returned formula: \begin{verbatim} -print_depth 999; f; print_depth 999; +print_depth 999; f; print_depth 3; { Find = [ Correct "solutions z_i"], With = [], Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)", diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Sep 02 16:16:08 2013 +0200 @@ -71,8 +71,7 @@ the internal representation of "a + b * 3". The '...' indicate that some details are still hidden; further details are received this way: *} -ML {* print_depth 99; - @{term "a + b * 9"} +ML {* print_depth 99; @{term "a + b * 9"}; print_depth 5; *} text {* The internal representation is too comprehensive for several kinds of inspection. Thus ISAC provides additional features, as we see below. First diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Sep 02 16:16:08 2013 +0200 @@ -120,6 +120,7 @@ ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *} ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *} ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *} +ML {* print_depth 3; *} text{* And, please, note that the result of applying the 'nxt' ruleset is to be found in the output of the next step ! *} diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Interpret/calchead.sml --- a/test/Tools/isac/Interpret/calchead.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Sep 02 16:16:08 2013 +0200 @@ -46,8 +46,7 @@ ([3, 2], Res)] then () else error "calchead.sml: diff.behav. get_interval after replace} other 2 a"; -print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); -print_depth 3; +print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); print_depth 3; if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else error "modspec.sml: diff.behav. get_interval after replace} other 2 b"; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Interpret/rewtools.sml --- a/test/Tools/isac/Interpret/rewtools.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Interpret/rewtools.sml Mon Sep 02 16:16:08 2013 +0200 @@ -402,7 +402,7 @@ "----------- fun guh2theID ------------------------------"; val guh = "thy_scri_ListG-thm-zip_Nil"; -print_depth 999; +print_depth 3; (*999*) take_fromto 1 4 (Symbol.explode guh); take_fromto 5 9 (Symbol.explode guh); val rest = takerest (9,(Symbol.explode guh)); diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Interpret/script.sml --- a/test/Tools/isac/Interpret/script.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Interpret/script.sml Mon Sep 02 16:16:08 2013 +0200 @@ -139,7 +139,7 @@ case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => () | _ => error "script.sml, doesnt find Substitute #2"; (* ERROR: caused by f2str f *) -trace_rewrite:=true; +trace_rewrite := false; val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*); trace_rewrite:=false; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/atools.sml --- a/test/Tools/isac/Knowledge/atools.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Sep 02 16:16:08 2013 +0200 @@ -124,7 +124,7 @@ if term2str pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () else error "atools.sml diff.behav. in eval_boollist2sum"; -trace_rewrite:=true; +trace_rewrite := false; val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls [Calc ("Atools.boollist2sum", eval_boollist2sum "")]; val t = str2t @@ -238,7 +238,7 @@ "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*) (*das rewriting l"asst sich beobachten mit - trace_rewrite:=true; +trace_rewrite := false; *) "------15.11.02 --------------------------"; @@ -246,7 +246,7 @@ val bdv = (term_of o the o (parse thy)) "bdv"; val a = (term_of o the o (parse thy)) "a"; - trace_rewrite:=true; +trace_rewrite := false; (* Anwenden einer Regelmenge aus Termorder.ML: *) val SOME (t,_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Mon Sep 02 16:16:08 2013 +0200 @@ -99,7 +99,7 @@ val SOME (ctt,_) = (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct); "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----"; -trace_rewrite := true; +trace_rewrite := false; val ct = "d_d s a"; (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct); (*got: NONE instead SOME*) diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/diffapp.sml Mon Sep 02 16:16:08 2013 +0200 @@ -671,7 +671,7 @@ term2str s; val t = str2term "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]"; -trace_rewrite:=true; +trace_rewrite := false; val SOME (t',_) = rewrite_set_ thy false list_rls t; trace_rewrite:=false; val s' = term2str t'; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/eqsystem.sml --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Sep 02 16:16:08 2013 +0200 @@ -360,7 +360,7 @@ [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*) val t = str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^ "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"); -trace_rewrite:=true; +trace_rewrite := false; val SOME (t',_) = rewrite_set_ thy false prls_triangular t; (*found:... ## try thm: NTH_CONS @@ -421,7 +421,7 @@ val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\ \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]", "solveForVars [c, c_2]", "solution LL"]; -trace_rewrite:=true; +trace_rewrite := false; val matches = refine fmz ["2x2", "linear","system"]; trace_rewrite:=false; print_depth 11; matches; print_depth 3; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/gcd_poly_winkler.sml --- a/test/Tools/isac/Knowledge/gcd_poly_winkler.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/gcd_poly_winkler.sml Mon Sep 02 16:16:08 2013 +0200 @@ -86,7 +86,7 @@ doe not conform with the Isabelle coding standards) *}*) - print_depth 20; + print_depth 3; (*20*) type unipoly = int list; "----------- auxiliary functions univariate -------------"; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/poly.sml --- a/test/Tools/isac/Knowledge/poly.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/poly.sml Mon Sep 02 16:16:08 2013 +0200 @@ -381,11 +381,11 @@ ... then trace_rewrite:*) "-----2 ---"; -trace_rewrite := true; +trace_rewrite := false; match_pbl fmz pbt; trace_rewrite := false; (*... if there is no rewrite, then there is something wrong with prls*) - + "-----3 ---"; print_depth 7; val prls = (#prls o get_pbt) ["polynomial","simplification"]; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 16:16:08 2013 +0200 @@ -1,17 +1,6 @@ (* Title: tests for rationals - Author: Stefan Karnel - Copyright (c) Stefan Karnel 2002 + Author: Walther Neuper Use is subject to license terms. - -12345678901234567890123456789012345678901234567890123456789012345678901234567890 - 10 20 30 40 50 60 70 80 -LEGEND -WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind -WN070906 - nonterm.SK marks non-terminating examples - ord.SK PARTIALLY marks crucial ordering examples - *SK* of some (secondary) interest (on 070906) -WN060104 transfer examples marked with (*SR..*) to the exp-collection *) "-----------------------------------------------------------------------------"; @@ -21,19 +10,19 @@ "-------- fun poly_of_term ---------------------------------------------------"; "-------- fun is_poly --------------------------------------------------------"; "-------- fun term_of_poly ---------------------------------------------------"; -"-------- fun factout_p_ -----------------------------------------------------"; -"-------- fun cancel_p_ ------------------------------------------------------"; -"-------- fun common_nominator_p_ --------------------------------------------"; -"-------- fun add_fraction_p_ ------------------------------------------------"; -"-------- TODO ---------------------------------------------------------------"; -"-------- and app_rev --------------------------------------------------------"; -"-------- external calculating functions test -----------"; -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; -"-------- common_nominator_p ----------------------------"; +"-------- integration lev.1 fun factout_p_ -----------------------------------"; +"-------- integration lev.1 fun cancel_p_ ------------------------------------"; +"-------- integration lev.1 fun common_nominator_p_ --------------------------"; +"-------- integration lev.1 fun add_fraction_p_ ------------------------------"; +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------"; +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; -"-------- reverse rewrite -------------------------------"; -"-------- 'reverse-ruleset' cancel_p --------------------"; -"-------- norm_Rational ---------------------------------"; +"-------- reverse rewrite ----------------------------------------------------"; +"-------- 'reverse-ruleset' cancel_p -----------------------------------------"; +"-------- investigate rls norm_Rational --------------------------------------"; +"-------- examples: rls norm_Rational ----------------------------------------"; "-------- numeral rationals -----------------------------"; "-------- cancellation ----------------------------------"; "-------- common denominator ----------------------------"; @@ -108,9 +97,9 @@ if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5" then () else error "term_of_poly 1 changed"; -"-------- fun factout_p_ -----------------------------------------------------"; -"-------- fun factout_p_ -----------------------------------------------------"; -"-------- fun factout_p_ -----------------------------------------------------"; +"-------- integration lev.1 fun factout_p_ -----------------------------------"; +"-------- integration lev.1 fun factout_p_ -----------------------------------"; +"-------- integration lev.1 fun factout_p_ -----------------------------------"; val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)" val SOME (t', asm) = factout_p_ thy t; if term2str t' = "(x + y) * (x + -1 * y) / (x * (x + -1 * y))" @@ -128,9 +117,9 @@ terms2str asm = "[\"1 + x ~= 0\"]" then () else error "factout_p_ 1 changed"; -"-------- fun cancel_p_ ------------------------------------------------------"; -"-------- fun cancel_p_ ------------------------------------------------------"; -"-------- fun cancel_p_ ------------------------------------------------------"; +"-------- integration lev.1 fun cancel_p_ ------------------------------------"; +"-------- integration lev.1 fun cancel_p_ ------------------------------------"; +"-------- integration lev.1 fun cancel_p_ ------------------------------------"; val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)" val SOME (t', asm) = cancel_p_ thy t; if (term2str t', terms2str asm) = ("(x + y) / x", "[\"x ~= 0\"]") @@ -144,9 +133,9 @@ if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[]" then () else error "cancel_p_ 1 changed"; -"-------- fun common_nominator_p_ --------------------------------------------"; -"-------- fun common_nominator_p_ --------------------------------------------"; -"-------- fun common_nominator_p_ --------------------------------------------"; +"-------- integration lev.1 fun common_nominator_p_ --------------------------"; +"-------- integration lev.1 fun common_nominator_p_ --------------------------"; +"-------- integration lev.1 fun common_nominator_p_ --------------------------"; val t = str2term ("y / (a*x + b*x + c*x) " ^ (* n1 d1 *) "+ a / (x*y)"); @@ -181,13 +170,13 @@ val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; val SOME (t', asm) = common_nominator_p_ thy t; if term2str t' = - "(x + -1) * (-1 + x) / (1 * ((1 + x) * (-1 + x))) +\n(x + 1) * (1 + x) / (1 * ((1 + x) * (-1 + x)))" + "(x + -1) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (-1 + x))" andalso terms2str asm = "[\"1 + x ~= 0\",\"-1 + x ~= 0\"]" then () else error "common_nominator_p_ 3 changed"; -"-------- fun add_fraction_p_ ------------------------------------------------"; -"-------- fun add_fraction_p_ ------------------------------------------------"; -"-------- fun add_fraction_p_ ------------------------------------------------"; +"-------- integration lev.1 fun add_fraction_p_ ------------------------------"; +"-------- integration lev.1 fun add_fraction_p_ ------------------------------"; +"-------- integration lev.1 fun add_fraction_p_ ------------------------------"; val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; val SOME (t', asm) = add_fraction_p_ thy t; if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" @@ -205,15 +194,9 @@ terms2str asm = "[\"-1 + x ^^^ 2 ~= 0\"]" then () else error "add_fraction_p_ 3 changed"; -"-------- TODO ---------------------------------------------------------------"; -"-------- TODO ---------------------------------------------------------------"; -"-------- TODO ---------------------------------------------------------------"; - - - -"-------- and app_rev --------------------------------------------------------"; -"-------- and app_rev --------------------------------------------------------"; -"-------- and app_rev --------------------------------------------------------"; +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------"; +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------"; +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------"; (* trace down until prepats are evaluated (which does not to work, because substitution is not done -- compare rew_sub!); keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p @@ -292,60 +275,64 @@ val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a ============ inhibit exn WN130823: prepat is empty ===================================*) -(*========== inhibit exn WN130824 TODO ======================================================= -"-------- external calculating functions test -----------"; -"-------- external calculating functions test -----------"; -"-------- external calculating functions test -----------"; -val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; -val SOME (t', asm) = factout_p_ thy t; -if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]" -then () else error "factout_p_ 1 changed"; -val SOME (t', asm) = cancel_p_ thy t; -if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]" -then () else error "cancel_p_ 1 changed"; +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; +val t = str2term "(12 * x * y) / (8 * y^^^2 )"; +(* "-------- example 187a": exception Div raised... +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*) +val t = str2term "(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )"; +(* "-------- example 187b": doesn't terminate... +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*) +val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )"; +(* "-------- example 187c": doesn't terminate... +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*) +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac}, false, cancel_p, t); +(* WN130827: exception Div raised... +rewrite__set_ thy 1 bool [] rls term +*) +"~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) = + (thy, 1, bool, [], rls, term); +(* WN130827: exception Div raised... + val (t', asm, rew) = app_rev thy (i+1) rrls t +*) +"~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t); +(* WN130827: exception Div raised... + val opt = app_rev' thy rrls t +*) +"~~~~~ fun app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) = + (thy, rrls, t); +chk_prepat thy erls prepat t = true; +(* WN130827: exception Div raised... +normal_form t +*) +(* lookup Rational.thy, cancel_p: normal_form = cancel_p_ thy*) +"~~~~~ fun cancel_p_, args:"; val (t) = (t); +val opt = check_fraction t; +val SOME (numerator, denominator) = opt + val vs = t |> vars |> map free2str |> sort string_ord + val baseT = type_of numerator + val expT = HOLogic.realT +val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator); +(*"-------- example 187a": exception Div raised... +val a = [(12, [1, 1])]: poly +val b = [(8, [0, 2])]: poly + val ((a', b'), c) = gcd_poly a b +*) +(* "-------- example 187b": doesn't terminate... +val a = [(8, [2, 1, 1])]: poly +val b = [(18, [1, 2, 1])]: poly + val ((a', b'), c) = gcd_poly a b +*) +(* "-------- example 187c": doesn't terminate... +val a = [(9, [5, 2, 4])]: poly +val b = [(15, [6, 3, 1])]: poly + val ((a', b'), c) = gcd_poly a b +*) -val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; -val SOME (t', asm) = factout_(*p_*) thy t; -if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]" -then () else error "factout_ 2 changed"; -val SOME (t', asm) = cancel_(*p_*) thy t; -if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]" -then () else error "cancel_ 2 changed"; - -val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; -val SOME (t', asm) = add_fraction_p_ thy t; -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" -then () else error "add_fraction_p_ 3 changed"; -val SOME (t', asm) = common_nominator_p_ thy t; -if term2str t' = - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" - andalso terms2str asm = "[]" -then () else error "common_nominator_p_ 3 changed"; - -val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; -val SOME (t', asm) = add_fraction_ thy t; -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" -then () else error "factout_ 4 changed"; -val SOME (t', asm) = common_nominator_ thy t; -if term2str t' = - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" - andalso terms2str asm = "[]" -then () else error "cancel_ 4 changed"; - -val t = str2term - "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))"; -val SOME (t', asm) = add_fraction_p_ thy t; -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" -then () else error "add_fraction_p_ 5 changed"; -val SOME (t', asm) = norm_rational_ thy t; -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" -then () else error "norm_rational_ 5 changed"; -============ inhibit exn WN130826 TODO ========================================================*) - - -"-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------"; -"-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------"; -"-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------"; +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; val thy = @{theory "Rational"}; "-------- WN"; val t = str2term "(2 + -3 * x) / 9"; @@ -512,554 +499,19 @@ if (term2str t', terms2str asm) = ("(2 * x + 10 * x ^^^ 2) / (1 + -5 * x)", "[]") then () else error "rational.sml cancel WN 1"; -(*========== inhibit exn WN130826 TODO ========================================================= -"-------- some old tests REVISE ! --------------------------------------------"; -"-------- some old tests REVISE ! --------------------------------------------"; -"-------- some old tests REVISE ! --------------------------------------------"; -(*WAS --- external calculating functions test ---*) -val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; -val SOME (t', asm) = factout_p_ thy t; -if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]" -then () else error "factout_p_ 1 changed"; -val SOME (t', asm) = cancel_p_ thy t; -if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]" -then () else error "cancel_p_ 1 changed"; +"-------- example heuberger"; +val t = str2term ("(x^^^4 + x * y + x^^^3 * y + y^^^2) / " ^ + "(x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)"); +val SOME (t', asm) = rewrite_set_ thy false cancel_p t; +if (term2str t', terms2str asm) = + ("(x ^^^ 3 + y) / (1 + 5 * x + x * y ^^^ 3)", "[\"1 + 5 * x + x * y ^^^ 3 ~= 0\"]") +then () else error "rational.sml cancel_p heuberger"; -val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; -val SOME (t', asm) = factout_(*p_*) thy t; -if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]" -then () else error "factout_ 2 changed"; -val SOME (t', asm) = cancel_(*p_*) thy t; -if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]" -then () else error "cancel_ 2 changed"; +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; +(*deleted example 204 ... 236b at update Isabelle2012-->2013*) -val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; -val SOME (t', asm) = add_fraction_p_ thy t; -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" -then () else error "add_fraction_p_ 3 changed"; -val SOME (t', asm) = common_nominator_p_ thy t; -if term2str t' = - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" - andalso terms2str asm = "[]" -then () else error "common_nominator_p_ 3 changed"; - -val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; -val SOME (t', asm) = add_fraction_ thy t; -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" -then () else error "factout_ 4 changed"; -val SOME (t', asm) = common_nominator_ thy t; -if term2str t' = - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" - andalso terms2str asm = "[]" -then () else error "cancel_ 4 changed"; - -val t = str2term - "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))"; -val SOME (t', asm) = add_fraction_p_ thy t; -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" -then () else error "add_fraction_p_ 5 changed"; -val SOME (t', asm) = norm_rational_ thy t; -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" -then () else error "norm_rational_ 5 changed"; - - -val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))"; -val SOME (t3',_) = common_nominator_ thy t3; -val SOME (t3'',_) = add_fraction_ thy t3; -(term2str t3'); -(term2str t3''); - -val SOME(t4,t5) = norm_expanded_rat_ thy t3; -term2str t4; -term2str (hd(t5)); - - - - val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)"; - val SOME (t',_) = factout_ thy t; - val SOME (t'',_) = cancel_ thy t; - term2str t'; - term2str t''; - "(3 + x) * (3 - x) / ((3 - x) * (3 - x))"; - "(3 + x) / (3 - x)"; - - val t=(term_of o the o (parse thy)) - "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)"; - val SOME (t',_) = common_nominator_ thy t; - val SOME (t'',_) = add_fraction_ thy t; - term2str t'; - term2str t''; - "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))"; - "(4 + x) / (3 - x)"; - -(*WN021016 added -----vv---*) -val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1"; -val SOME (t',_) = common_nominator_ thy t; -val SOME (t'',_) = add_fraction_ thy t; -term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1" ^ - " * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); -term2str t'' = "6 / (3 - x)" (*true*); - -val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)"; -val SOME (t',_) = common_nominator_ thy t; -val SOME (t'',_) = add_fraction_ thy t; -term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n" ^ - "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); -term2str t'' = "6 / (3 - x)" (*true*); -(*WN021016 added -----^^---*) -(*WN030602 added -----vv--- no rewrite -> NONE !*) -val t = str2term "1 / a"; -val NONE = cancel_p_ thy t; -val NONE = rewrite_set_ thy false cancel_p t; -(*WN.2.6.03 added -------^^---*) - -val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)"; -val SOME (t',_) = factout_ thy t; -val SOME (t'',_) = cancel_ thy t; -term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*); -term2str t'' = "(y + x) / (y - x)"; - -val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)"; -val SOME (t',_) = common_nominator_ thy t; -val SOME (t'',_) = add_fraction_ thy t; -term2str t' = -"(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1" ^ -" * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*); -term2str t'' = "(-1 - x - y) / (x - y)" (*true*); - -val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)"; -val SOME (t',_) = common_nominator_ thy t; -val SOME (t'',_) = add_fraction_ thy t; -if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))" ^ -" +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then () -else error "rational.sml lex-ord 1"; -if term2str t'' = "(-1 - y - x) / (y - x)" then () -else error "rational.sml lex-ord 2"; -(*WN.16.10.02 WN070905 lexicographische Ordnung erhalten *) - - -val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)"; -val SOME (t',_) = norm_expanded_rat_ thy t; -if term2str t' = "(x + y) / (x - y)" then () -else error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 No.1"; -(*val SOME (t'',_) = norm_rational_ thy t; - *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial -WN.16.10.02 ?! + WN060831???SK4 -WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*) - - -val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)"; -val SOME (t',_) = norm_expanded_rat_ thy t; -if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then () -else error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +..."; -(*val SOME (t'',_) = norm_rational_ thy t; - *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?! -WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*) - - val t=(term_of o the o (parse thy)) - "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)"; - val SOME (t',_) = norm_expanded_rat_ thy t; - val SOME (t'',_) = norm_rational_ thy t; - term2str t'; - term2str t''; - "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)"; - "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)"; - - -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; -val thy = @{theory "Rational"}; -val thy' = "Rational"; -val rls' = "cancel"; -val mp = "make_polynomial"; - -writeln ("example 186:"); -writeln("a)"); -val e186a'="(14 * x * y) / ( x * y )";(*SRC*) -rewrite_set_ thy false cancel (str2term e186a'); -"@@@@@@@@@@@@@@"; -val e186a = the (rewrite_set thy' false "cancel" e186a'); - is_expanded (parse_rat "14 * x * y"); - is_expanded (parse_rat "x * y"); -if e186a = ("14 / 1", "[\"y * x ~= 0\"]") then () -else error "rational.sml cancel Schalk e186a"; - -writeln("b)"); -val e186b'="(60 * a * b) / ( 15 * a * b )"; -val e186b = the (rewrite_set thy' false "cancel" e186b'); -writeln("c)"); -val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )"; -val e186c = (the (rewrite_set thy' false "cancel" e186c')) - handle e => print_exn_G e; -val t = (term_of o the o (parse thy)) e186c'; -if e186c = ("12 * a / 1", "[\"12 * (c * (b * a)) ~= 0\"]") then () -else error "rational.sml cancel Schalk e186c"; - -writeln ("example 187:"); -writeln("a)"); -val e187a'="(12 * x * y) / (8 * y^^^2 )";(*SRC*) -val e187a = the (rewrite_set thy' false "cancel" e187a'); -writeln("b)"); -val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )"; -val e187b = the (rewrite_set thy' false "cancel" e187b'); -writeln("c)"); -val e187d'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*) -val e187d = the (rewrite_set thy' false "cancel" e187d'); -if e187d = ("3 * z ^^^ 3 / (5 * (y * x))", - "[\"3 * (z * (y ^^^ 2 * x ^^^ 5)) ~= 0\"]") then () -else error "rational.sml cancel Schalk e186d"; - -writeln "example 188:"; -val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*) -val e188a = the (rewrite_set thy' false "cancel" e188a'); - is_expanded (parse_rat "8 * x + -8"); -(* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*) -if e188a = ("8 / 9", "[\"-1 + x ~= 0\"]") then () -else error "rational.sml: e188a new behaviour"; - -val SOME (t,_) = rewrite_set thy' false mp "(8*((-1) + x))/(9*((-1) + x))"; -writeln("b)"); -val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*) -val SOME (t, asm) = rewrite_set thy' false "cancel" e188b'; -t = "5 / 6" (*true*); -writeln("c)"); - -val e188c'="( a + -1 * b ) / ( b + -1 * a )"; -val e188c = the (rewrite_set thy' false "cancel_p" e188c'); -(*is_expanded (parse_rat "a + -1 * b");*) -val SOME (t,_) = - rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))"; -if t= "(a + -1 * b) / (-1 * a + b)" then() -else error "rational.sml: e188c new behaviour"; - -writeln ("example 190:"); -writeln("c)"); -val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )"; -val e190c = the (rewrite_set thy' false "cancel" e190c'); -val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))"; -if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then () -else error "rational.sml: e190c new behaviour"; - -writeln ("example 191:"); -writeln("a)"); -val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )"; -(*WN.23.10.02------- -val e191a = the (rewrite_set thy' false "cancel" e191a'); - is_expanded (parse_rat "x^^^2 + -1 * y^^^2"); - false; - is_expanded (parse_rat "x + y"); - true; -----------*) -val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))"; -(* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*) -if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() -else error "rational.sml: e191a new behaviour"; - -writeln("c)"); -val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )"; -(*WN.23.10.02------- -val e191c = the (rewrite_set thy' false "cancel" e191c'); - is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25"); - false; - is_expanded (parse_rat "25 + -30*x + 9*x^^^2"); - false; - is_expanded (parse_rat "-25 + 9*x^^^2"); - true;------------*) -val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))"; -(* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*) -if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then() -else error "rational.sml: 'e191c' new behaviour"; - - -writeln ("example 192:"); -writeln("b)"); -val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )"; -(*WN.23.10.02------- -val e192b = the (rewrite_set thy' false "cancel" e192b'); --------------------*) -val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))"; -(*========== inhibit exn 110317 ================================================ -if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" -(*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*) -then () else error "rational.sml: 'e192b' new behaviour"; -(*^^^ works with MG's simplifier vvv*) -val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))"; -val SOME (t',_) = rewrite_set_ thy false make_polynomial t; -if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else error "rational.sml: 'e192b'MG new behaviour"; -============ inhibit exn 110317 ==============================================*) - -writeln ("example 193:"); -writeln("a)"); -val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )"; -(*WN.23.10.02------- -val e193a = the (rewrite_set thy' false "cancel" e193a'); --------------------*) -writeln("b)"); -val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )"; -(*WN.23.10.02------- -val e193b = the (rewrite_set thy' false "cancel" e193b'); -writeln("c)"); -val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )"; -val SOME(t,_) = rewrite_set thy' false "cancel" e193c'; --------------------*) - -val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)"; -val SOME (t, asm) = rewrite_set thy' false "cancel" wn01; -(* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*) -if t = "(-5 + 3 * x) / 1" andalso asm = "[\"5 + 3 * x ~= 0\"]" then () -else error "rational.sml: new behav. in cancel wn01"; - -"-------- common_nominator_p ----------------------------"; -"-------- common_nominator_p ----------------------------"; -"-------- common_nominator_p ----------------------------"; -val rls' = "common_nominator_p"; - -writeln ("example 204:"); -writeln("a)"); -val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)"; -val e204a = the (rewrite_set thy' false "common_nominator_p" e204a'); -writeln("b)"); -val e204b'="5 / x + -3 / x + -1 / x"; -val e204b = the (rewrite_set thy' false "common_nominator_p" e204b'); -if e204b = ("1 / x", "[]") then () -else error "rational.sml common_nominator_p example e204b"; - -writeln ("example 205:"); -writeln("a)"); -val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)"; -val e205a = the (rewrite_set thy' false "common_nominator_p" e205a'); -writeln("b)"); -val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)"; -val e205b = the (rewrite_set thy' false "common_nominator_p" e205b'); -if e205b = ("(1 + x) / 1", "[]") then () -else error "rational.sml common_nominator_p example e204b"; - -writeln ("example 206:"); -writeln("a)"); -val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))"; -val e206a = the (rewrite_set thy' false "common_nominator_p" e206a'); -writeln("b)"); -val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))"; -val e206b = the (rewrite_set thy' false "common_nominator_p" e206b'); - -writeln ("example 207:"); -val e207'="((3 * x * y + 3 * y) / (x * y)) + ((5 * x * y + 7 * y) / (x * y)) + ((9 * x * y + -2 * y) / (x * y)) + ((x * y + 4 * y) / (x * y)) "; -val e207 = the (rewrite_set thy' false "common_nominator_p" e207'); - -writeln ("example 208:"); -val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) "; -val e208 = the (rewrite_set thy' false "common_nominator_p" e208'); - -writeln ("example 209:"); -val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) "; -val e209 = the (rewrite_set thy' false "common_nominator_p" e209'); - -writeln ("example 210:"); -val e210'="((2 * x + 3 + -1 * x^^^2) / (5 * x)) + ((5 * x^^^2 + -2 * x + 1) / (5 * x)) + ((-3 * x^^^2 + -2 * x + 1) / (5 * x)) + ((-1 * x^^^2 + -3 * x + -5) / (5 * x)) "; -val e210 = the (rewrite_set thy' false "common_nominator_p" e210'); - -writeln ("example 211:"); -writeln("a)"); -val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))"; -val e211a = the (rewrite_set thy' false "common_nominator_p" e211a'); -writeln("b)"); -val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))"; -val e211b = the (rewrite_set thy' false "common_nominator_p" e211b'); - -writeln ("example 212:"); -writeln("a)"); -val e212a'="((4) / (x)) + ((-3) / (y)) + -1"; -val e212a = the (rewrite_set thy' false "common_nominator_p" e212a'); -writeln("b)"); -val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))"; -val e212b = the (rewrite_set thy' false "common_nominator_p" e212b'); - -writeln ("example 213:"); -writeln("a)"); -val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) "; -val e213a = the (rewrite_set thy' false "common_nominator_p" e213a'); -writeln("b)"); -val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))"; -val e213b = the (rewrite_set thy' false "common_nominator_p" e213b'); - -writeln ("example 214:"); -writeln("a)"); -val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))"; -val e214a = the (rewrite_set thy' false "common_nominator_p" e214a'); -writeln("b)"); -val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))"; -val e214b = the (rewrite_set thy' false "common_nominator_p" e214b'); - -writeln ("example 216:"); -writeln("a)"); -val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))"; -val e216a = the (rewrite_set thy' false "common_nominator_p" e216a'); -writeln("b)"); -val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))"; -val e216b = the (rewrite_set thy' false "common_nominator_p" e216b'); - -writeln ("example 217:"); -val e217'="((z + -1) / (z)) + ((3 * z ^^^2 + -6 * z + 5) / (z^^^2)) + ((-4 * z^^^3 + 7 * z^^^2 + -5 * z + 5) / (z^^^3))"; -val e217 = the (rewrite_set thy' false "common_nominator_p" e217'); - - -val rls' = "common_nominator"; -writeln ("example 218:"); -val e218'="((9 * a^^^3 - 5 * a^^^2 + 2 * a + 8) / (108 * a^^^4)) + ((-5 * a + 3 * a^^^2 + 4) / (8 * a^^^3)) + ((-261 * a^^^3 + 19 * a^^^2 + -112 * a + 16) / (216 * a^^^4))"; -val e218 = the (rewrite_set thy' false "common_nominator" e218'); -if e218 = ("(16 - 63 * a ^^^ 2 - 81 * a ^^^ 3) / (108 * a ^^^ 4)", "[]") then () -else error "rationa.sml common_nominator example e218"; - -writeln ("example 219:"); -writeln("a)"); -val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))"; -val e219a = the (rewrite_set thy' false "common_nominator" e219a'); -writeln("b)"); -val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))"; -val e219b = the (rewrite_set thy' false "common_nominator" e219b'); -if e219b = ("(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)", "[]") then () -else error "rationa.sml common_nominator example e219b"; - -writeln ("example 220:"); -writeln("a)"); -val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))"; -val e220a = the (rewrite_set thy' false "common_nominator" e220a'); -writeln("b)"); -val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))"; -val e220b = the (rewrite_set thy' false "common_nominator" e220b'); - -writeln ("example 221:"); -writeln("a)"); -val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))"; -val e221a = the (rewrite_set thy' false "common_nominator" e221a'); -writeln("b)"); -val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) "; -val e221b = the (rewrite_set thy' false "common_nominator" e221b'); - -writeln ("example 222:"); -writeln("a)"); -val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))"; -val e222a = the (rewrite_set thy' false "common_nominator" e222a'); -writeln("b)"); -val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))"; -val e222b = the (rewrite_set thy' false "common_nominator" e222b'); - -writeln ("example 225:"); -writeln("a)"); -val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))"; -val e225a = the (rewrite_set thy' false "common_nominator" e225a'); -writeln("b)"); -val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))"; -val e225b = the (rewrite_set thy' false "common_nominator" e225b'); - -writeln ("example 226:"); -writeln("a)"); -val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) "; -val e226a = the (rewrite_set thy' false "common_nominator" e226a'); -writeln("b)"); -val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2"; -val e226b = the (rewrite_set thy' false "common_nominator" e226b'); - -writeln ("example 227:"); -writeln("a)"); -val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 "; -val e227a = the (rewrite_set thy' false "common_nominator" e227a'); -writeln("b)"); -val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 "; -val e227b = the (rewrite_set thy' false "common_nominator" e227b'); - -writeln ("example 228:"); -writeln("a)"); -val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))"; -val e228a = the (rewrite_set thy' false "common_nominator" e228a'); -writeln("b)"); -val e228b'="((11 * z + 2 * b) / (4 * b * z + -8 * b^^^2)) + ((-8 * z) / (z^^^2 + -4 * b^^^2)) + ((-9 * z + -2 * b) / (4 * b * z + 8 * b^^^2))"; -val e228b = the (rewrite_set thy' false "common_nominator" e228b'); - - -writeln ("example 229:"); -writeln("a)"); -val e229a'="((5 * x^^^2 + y) / (x + 2 * y)) + ((-8 * x^^^3 + 4 * x^^^2 * y + 3 * x * y) / (x^^^2 + -4 * y^^^2)) + ((3 * x^^^2 + -4 * y) / (x + -2 * y))"; -val e229a = the (rewrite_set thy' false "common_nominator" e229a'); -writeln("b)"); -val e229b'="((7 * x^^^2 + y) / (x + 3 * y)) + ((-24 * x^^^2 * y + 5 * x * y + 21 * y^^^2) / (x^^^2 + -9 * y^^^2)) + ((4 * x^^^2 + -6 * y) / (x + -3 * y))"; -val e229b = the (rewrite_set thy' false "common_nominator" e229b'); - -writeln ("example 230:"); -writeln("a)"); -val e230a'="((5 * x^^^2 + y) / (2 * x + y)) + ((-16 * x^^^3 + 2 * x^^^2 * y + 6 * x * y) / (4 * x^^^2 + -1 * y^^^2)) + ((3 * x^^^2 + -4 * y) / (2 * x + -1 * y))"; -val e230a = the (rewrite_set thy' false "common_nominator" e230a'); -writeln("b)"); -val e230b'="((7 * x^^^2 + y) / (3 * x + y)) + ((-3 * x^^^3 + 15 * x * y + -7 * x^^^2 * y + 7 * y^^^2) / (9 * x^^^2 + -1 * y^^^2)) + ((4 * x^^^2 + -6 * y) / (3 * x + -1 * y))"; -val e230b = the (rewrite_set thy' false "common_nominator" e230b'); - -writeln ("example 231:"); -writeln("a)"); -val e231a'="((2 * x + 5 * y) / (x)) + ((2 * x^^^3 + -5 * y^^^3 + 3 * x * y^^^2) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-3 * x + -6 * y) / (x + -1 * y))"; -val e231a = the (rewrite_set thy' false "common_nominator" e231a'); -writeln("b)"); -val e231b'="((6 * x + 2 * y) / (x)) + ((6 * x^^^2 * y + -4 * x * y^^^2 + -2 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-5 * x + -3 * y) / (x + -1 * y))"; -val e231b = the (rewrite_set thy' false "common_nominator" e231b'); - -writeln ("example 232:"); -writeln("a)"); -val e232a'="((2 * x + 3 * y) / (x)) + ((4 * x^^^3 + -1 * x * y^^^2 + -3 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-5 * x + -6 * y) / (x + -1 * y))"; -val e232a = the (rewrite_set thy' false "common_nominator" e232a'); -writeln("b)"); -val e232b'="((5 * x + 2 * y) / (x)) + ((2 * x^^^3 + -3 * x * y^^^2 + 3 * x^^^2 * y + -2 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-6 * x + -3 * y) / (x + -1 * y))"; -val e232b = the (rewrite_set thy' false "common_nominator" e232b'); - -writeln ("example 233:"); -writeln("a)"); -val e233a'="((5 * x + 6 * y) / (x)) + ((5 * x * y^^^2 + -6 * y^^^3 + -2 * x^^^3 + 3 * x^^^2 * y) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-2 * x + -3 * y) / (x + -1 * y))"; -val e233a = the (rewrite_set thy' false "common_nominator" e233a'); -writeln("b)"); -val e233b'="((6 * x + 5 * y) / (x)) + ((4 * x^^^2 * y + 3 * x * y^^^2 + -5 * y^^^3 + -2 * x^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-3 * x + -2 * y) / (x + -1 * y))"; -val e233b = the (rewrite_set thy' false "common_nominator" e233b'); - -writeln ("example 234:"); -writeln("a)"); -val e234a'="((5 * a + b) / (2 * a * b + -2 * b^^^2)) + ((-3 * a + -1 * b) / (2 * a * b + 2 * b^^^2)) + ((-2 * a) / (a^^^2 + -1 * b^^^2))"; -val e234a = the (rewrite_set thy' false "common_nominator" e234a'); -writeln("b)"); -val e234b'="((5 * a + 3 * b) / (6 * a * b + -18 * b^^^2)) + ((-3 * a + -3 * b) / (6 * a * b + 18 * b^^^2)) + ((-2 * a) / (a^^^2 + -9 * b^^^2)) "; -val e234b = the (rewrite_set thy' false "common_nominator" e234b'); - -writeln ("example 235:"); -writeln("a)"); -val e235a'="((10 * x + 3 * y) / (12 * x * y + -18 * y^^^2)) + ((-6 * x + -3 * y) / (12 * x * y + 18 * y^^^2)) + ((-4 * x) / (4 * x^^^2 + -9 * y^^^2))"; -val e235a = the (rewrite_set thy' false "common_nominator" e235a'); -writeln("b)"); -val e235b'="((8 * a + b) / (4 * a * b + -2 * b^^^2)) + ((-4 * a + -1 * b) / (4 * a * b + 2 * b^^^2)) + ((-2 * a) / (4 * a^^^2 + -1 * b^^^2)) "; -val e235b = the (rewrite_set thy' false "common_nominator" e235b'); - -writeln ("example 236:"); -writeln("a)"); -val e236a'="((8 * a + 5 * b) / (20 * a * b + -50 * b^^^2)) + ((-4 * a + -5 * b) / (20 * a * b + 50 * b^^^2)) + ((-2 * a) / (4 * a^^^2 + -25 * b^^^2))"; -val e236a = the (rewrite_set thy' false "common_nominator" e236a'); -writeln("b)"); -val e236b'="((24 * x + y) / (6 * x * y + -2 * y^^^2)) + ((-18 * x + -1 * y) / (6 * x * y + 2 * y^^^2)) + ((-15 * x) / (9 * x^^^2 + -1 * y^^^2)) "; -val e236b = the (rewrite_set thy' false "common_nominator" e236b'); - - -val rls' = "cancel"; -writeln ("example heuberger:"); -val eheu'="(x^^^4 + x * y + x^^^3 * y + y^^^2) / (x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)"; -val eheu = the (rewrite_set thy' false "cancel" eheu'); - -val rls' = "common_nominator_p"; -writeln ("example stiefel:"); -val est1'="(7) / (-14) + (-2) / (4)"; -val est1 = the (rewrite_set thy' false "common_nominator_p" est1'); -if est1 = ("-1 / 1", "[]") then () -else error "new behaviour in rational.sml: est1'"; - -val t = (term_of o the o (parse thy)) -"(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; -val SOME (t',_) = factout_ thy t; -if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then () -else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; - "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; @@ -1124,46 +576,75 @@ if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)" then () else error "level 5, rewrite_set_ norm_Rational: changed" -"-------- reverse rewrite -------------------------------"; -"-------- reverse rewrite -------------------------------"; -"-------- reverse rewrite -------------------------------"; -(*WN.28.8.02: tests for the 'reverse-rewrite' functions: - these are defined in Rationals.ML and stored in - the 'reverse-ruleset' cancel*) +"-------- reverse rewrite ----------------------------------------------------"; +"-------- reverse rewrite ----------------------------------------------------"; +"-------- reverse rewrite ----------------------------------------------------"; +(** the term for which reverse rewriting is demonstrated **) +val t = str2term "(9 + -1 * x ^^^ 2) / (9 + 6 * x + x ^^^ 2)"; +val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc, + next_rule = nex, normal_form = nor, ...},...} = cancel_p; -(*the term for which reverse rewriting is demonstrated*) - val t = (term_of o the o (parse thy)) - "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)"; - val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc, - next_rule=nex,normal_form=nor,...},...} = cancel; - -(*normal_form produces the result in ONE step*) +(** normal_form produces the result in ONE step **) val SOME (t',_) = nor t; -if term2str t' = "(3 - x) / (3 + x)" then () +if term2str t' = "(3 + -1 * x) / (3 + x)" then () else error "rational.sml normal_form (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; -(*initialize the interpreter state used by the 'me'*) - val (t,_,revsets,_) = ini t; +(** initialize the interpreter state used by the 'me' **) + val (t, _, revsets, _) = ini t; -(*find the rule 'r' to apply to term 't'*) +if length (hd revsets) = 11 then () else error "length of revset changed"; +if (revsets |> nth 1 |> nth 1 |> id_of_thm) = + (@{thm realpow_twoI} |> string_of_thm |> thmID_of_derivation_name) +then () else error "first element of revset changed"; +if +(revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",??.unknown)" andalso +(revsets |> nth 1 |> nth 2 |> rule2str) = + "Thm (\"sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))\",??.unknown)" andalso +(revsets |> nth 1 |> nth 3 |> rule2str) = + "Thm (\"sym_#mult_Float ((2,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso +(revsets |> nth 1 |> nth 4 |> rule2str) = + "Thm (\"sym_#mult_Float ((~1,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso +(revsets |> nth 1 |> nth 5 |> rule2str) = + "Thm (\"sym_#mult_Float ((3,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso +(revsets |> nth 1 |> nth 6 |> rule2str) = "Rls_ (\"sym_order_mult_rls_\")" andalso +(revsets |> nth 1 |> nth 7 |> rule2str) = + "Thm (\"sym_mult_assoc\",Groups.semigroup_mult_class.mult_assoc)" +then () else error "first 7 elements in revset changed" + +(** find the rule 'r' to apply to term 't' **) +(*/------- since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_ + for Isabelle2013, we don't get a working revset, but non-termination: + val SOME (r as (Thm (str, thm))) = nex revsets t; + : +((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), + Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," +((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), + Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))"," +((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), + Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))"," +((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," + : +### Isabelle2002: + Thm ("sym_#mult_2_3", "6 = 2 * 3") +### Isabelle2009-2 for cancel_ (not cancel_p_): if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso string_of_thm thm = (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; -(* before Isa02->09-2 was not checked automatically, ?was different?: -val SOME r = nex revsets t; -val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*) +\---------------------------------------------------------------------------------------/*) -(* check, if the rule 'r' applied by the user to 't' belongs to the ruleset; +(** check, if the rule 'r' applied by the user to 't' belongs to the ruleset; if the rule is OK, the term resulting from applying the rule is returned,too; there might be several rule applications inbetween, - which are listed after the head in reverse order *) + which are listed after the head in reverse order **) +(*/-------------------------------------------- Isabelle2013: this gives "error id_of_thm"; + we don't repair this, because interaction within "reverse rewriting" never worked properly: + val (r, (t, asm))::_ = loc revsets t r; if term2str t = "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" andalso asm = [] -then () -else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; +then () else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; (* find the next rule to apply *) val SOME (r as (Thm (str, thm))) = nex revsets t; @@ -1198,11 +679,13 @@ val ss = term2str t; if ss = "(3 - x) / (3 + x)" andalso terms2str asm = "[\"3 + x ~= 0\"]" then () else error "rational.sml: new behav. in rev-set cancel"; +\--------------------------------------------------------------------------------------/*) -"-------- 'reverse-ruleset' cancel_p --------------------"; -"-------- 'reverse-ruleset' cancel_p --------------------"; -"-------- 'reverse-ruleset' cancel_p --------------------"; -(*WN.11.9.02: the 'reverse-ruleset' cancel_p*) +"-------- 'reverse-ruleset' cancel_p -----------------------------------------"; +"-------- 'reverse-ruleset' cancel_p -----------------------------------------"; +"-------- 'reverse-ruleset' cancel_p -----------------------------------------"; +(*Isabelle2013: the example below shows, why "reverse rewriting" only worked for + special cases.*) (*the term for which reverse rewriting is demonstrated*) val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))"; @@ -1237,16 +720,12 @@ val SOME r = nex revsets t; val (r,(t,asm))::_ = loc revsets t r; term2str t; -*) +*) -writeln "****************** all tests successfull *************************"; - - - -(*WN.17.3.03 =========================================================vvv---*) -"-------- norm_Rational ---------------------------------"; -"-------- norm_Rational ---------------------------------"; -"-------- norm_Rational ---------------------------------"; +(*========== inhibit exn WN130824 TODO ======================================================= +"-------- examples: rls norm_Rational ----------------------------------------"; +"-------- examples: rls norm_Rational ----------------------------------------"; +"-------- examples: rls norm_Rational ----------------------------------------"; val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0"; val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; if term2str t' = "1 / 18 = 0" then () else error "rational.sml 1"; @@ -2415,7 +1894,7 @@ SK060904-2a non-termination of add_fraction_p_"; val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^ " (-1 * a + b * x) / (a + b * x) "); -(* nonterm.SK +(* nonterm.SK = WN130830 val SOME (t',_) = rewrite_set_ thy false common_nominator_p t; "--- 11 ---"; common_nominator_p_ thy t; @@ -2432,11 +1911,11 @@ " errors in cancel_p: --- 4,5,6,7."; " error in common_nominator_p, common_nominator_p_: --- 10; 1,2?."; " errors caused by ruleset norm_Rational: --- 8,9."; -trace_rewrite := true; +trace_rewrite := false; -"--- 1 ---: non-terminating with ### add_fract: done t22 "; +"--- 1 ---: non-terminating with ### add_fract: done t22 "; = WN130830 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)"; -trace_rewrite:= true; +trace_rewrite := false; rewrite_set_ thy false common_nominator_p t; "--- 2 ---: non-terminating with ### add_fract: done t22 "; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/rlang.sml --- a/test/Tools/isac/Knowledge/rlang.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/rlang.sml Mon Sep 02 16:16:08 2013 +0200 @@ -1457,7 +1457,7 @@ val t = str2term"(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)"; -trace_rewrite:=true; +trace_rewrite := false; val SOME (t',asm) = rewrite_set_ thy false norm_Rational t; term2str t'; trace_rewrite:=false; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Knowledge/rooteq.sml --- a/test/Tools/isac/Knowledge/rooteq.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Knowledge/rooteq.sml Mon Sep 02 16:16:08 2013 +0200 @@ -5,7 +5,7 @@ Compiler.Control.Print.printDepth:=10; (*4 default*) Compiler.Control.Print.printDepth:=5; (*4 default*) - trace_rewrite:=true; +trace_rewrite := false; *) "----------- rooteq.sml begin--------"; "--------------(1/sqrt(x)=5)---------------------------------------"; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/OLDTESTS/modspec.sml --- a/test/Tools/isac/OLDTESTS/modspec.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/OLDTESTS/modspec.sml Mon Sep 02 16:16:08 2013 +0200 @@ -31,8 +31,7 @@ ([3, 2], Res)] then () else error "modspec.sml: diff.behav. get_interval after replace} other 2 a"; -print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); -print_depth 3; +print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); print_depth 3; if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) = [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else error "modspec.sml: diff.behav. get_interval after replace} other 2 b"; diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/ProgLang/rewrite.sml --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 16:16:08 2013 +0200 @@ -521,7 +521,7 @@ *) trace_rewrite := false; -trace_rewrite := true; +trace_rewrite := false; val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*) term2str t' = "1 = 5 * x"; (* diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/ProgLang/termC.sml --- a/test/Tools/isac/ProgLang/termC.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/ProgLang/termC.sml Mon Sep 02 16:16:08 2013 +0200 @@ -222,7 +222,7 @@ val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)"; (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*) val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty); -print_depth 999; insts; +print_depth 3; (*999*) insts; (*val insts = ({}, {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))), diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Test_Isac.thy Mon Sep 02 16:16:08 2013 +0200 @@ -2,19 +2,19 @@ Author: Walther Neuper 101001 (c) copyright due to lincense terms. - isac tests - in ~~/test/Tools/isac are structured according - to ~~/src/Tools/isac - Additional tests are in + Isac's tests are organised parallel to sources: + "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac" + plus ~~/test/Tools/isac/ADDTESTS - ~~/test/Tools/isac/Minisubpbl + ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality $ cd /usr/local/isabisac/ $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy & *) -(*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION: - Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?*) +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) +(* !!!!! wait a minute until Isac and the theories below are loaded !!!!! *) +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) theory Test_Isac imports Isac "ADDTESTS/Ctxt" @@ -24,7 +24,7 @@ "ADDTESTS/course/phst11/T2_Rewriting" "ADDTESTS/course/phst11/T3_MathEngine" "ADDTESTS/file-depend/BuildC_Test" - "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform" +(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*) "~~/test/Pure/Isar/Test_Parsers" (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*) "~~/test/Pure/Isar/Test_Parse_Term" @@ -33,12 +33,6 @@ "~~/src/Tools/isac/Knowledge/GCD_Poly" (*not imported by Isac.thy*) "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) -(* !!!!! wait a minute until Isac and the above theories are loaded !!!!! *) -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) -(* !!!!! with this changeset evaluation doen't start < 7min; UG is busy ! *) -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *) - begin section {* test ML Code of isac *} ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} @@ -123,7 +117,7 @@ ML_file "Knowledge/rootrat.sml" ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) ML_file "Knowledge/partial_fractions.sml" -(*ML_file "Knowledge/polyeq.sml" -----------------works if cut into parts !!!!!!!!!!!*) + ML_file "Knowledge/polyeq.sml" (*-----------------works if cut into parts !!!!!!!!!!!*) (*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *) ML_file "Knowledge/calculus.sml" ML_file "Knowledge/trig.sml" diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/Test_Some.thy Mon Sep 02 16:16:08 2013 +0200 @@ -1,45 +1,73 @@ - theory Test_Some imports Isac -begin ML_file "Knowledge/gcd_poly_ml.sml" -(* -declare [[show_types]] -declare [[show_sorts]] -find_theorems "?a <= ?a" +begin +ML_file "Knowledge/rational.sml" -print_facts -print_statement "" -print_theory -*) +section {* code for copy & paste ===============================================================*} ML {* -*} -ML {* (*==================*) -*} -ML {* -*} -ML {* -*} -ML {* (*==================*) -*} -ML {* -*} -ML {* -*} -ML {* (*==================*) "~~~~~ fun , args:"; val () = (); +"~~~~~ and , args:"; val () = (); "~~~~~ to return val:"; val () = (); *} +text {* + declare [[show_types]] + declare [[show_sorts]] + find_theorems "?a <= ?a" + + print_facts + print_statement "" + print_theory +*} +ML {* +(*========== inhibit exn WN130822 only runs with Rational2.thy ================================= +============ inhibit exn WN130822 only runs with Rational2.thy ================================*) + +(*========== inhibit exn WN130826 TODO ========================================================= +============ inhibit exn WN130826 TODO ========================================================*) + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) + +(*=========================^^^ correct until here ^^^==========================================*) +*} + + +section {* ====================================================================================*} +ML {* +*} ML {* +*} ML {* +*} ML {* +*} ML {* +*} + +section {* GREAT CONFUSION -> final hg ci =====================================================*} +ML {* +(*in isabisac12/test/../rational.sml*) +"-------- investigate rls common_nominator_p from OLD gcd --------------------"; +(*ATTENTION: +val common_nominator_p = + Rrls {id = "common_nominator_p", ... + scr = Rfuns {init_state = init_state thy Atools_erls ro, + normal_form = add_fraction_p_ thy, <<<=================================== +: +val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*) +(*but ^^^ not exported, just ^^^*) + +i.e. GREAT CONFUSION: +# normal_form of add_fractions_p is add_fraction_p_, +# and id of add_fractions_p is common_nominator_p +*) + +section {* ===================================================================================*} +ML {* +*} ML {* +*} ML {* +*} + +section {* ===================================================================================*} +ML {* +*} ML {* +*} ML {* +*} end - -(*========== inhibit exn WN1130701 broken already in 2009-2 ======================= -============ inhibit exn WN1130701 broken already in 2009-2 =====================*) -(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=== -============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*) - -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) - -(*=========================^^^ correct until here ^^^===========================*) - - diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/calcelems.sml --- a/test/Tools/isac/calcelems.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/calcelems.sml Mon Sep 02 16:16:08 2013 +0200 @@ -72,7 +72,7 @@ pretty types: PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); - print_depth 99; + print_depth 3; *) "===== extend parse to string with markup==="; (* diff -r 0831a4a6ec8a -r c3f399ce32af test/Tools/isac/xmlsrc/datatypes.sml --- a/test/Tools/isac/xmlsrc/datatypes.sml Mon Sep 02 15:17:34 2013 +0200 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Mon Sep 02 16:16:08 2013 +0200 @@ -32,7 +32,7 @@ "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]); (*get_py (Thy_Info.get_theory "Pure") theID theID (! thehier); (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*) -print_depth 999; +print_depth 3; (*999*) (!thehier); (*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (! thehier));*)