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.
1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 15:17:34 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 16:16:08 2013 +0200
1.3 @@ -374,15 +374,15 @@
1.4 in try_new_prime_up a b d M P g p end
1.5 end
1.6
1.7 - (* HENSEL_lifting_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
1.8 - HENSEL_lifting_up p1 p2 d M p = gcd
1.9 + (* iterate_CHINESE_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
1.10 + iterate_CHINESE_up p1 p2 d M p = gcd
1.11 assumes d = gcd (lcoeff_up p1, lcoeff_up p2) \<and>
1.12 M = LANDAU_MIGNOTTE_bound \<and> p = prime \<and> p ~| d \<and>
1.13 p1 is primitive \<and> p2 is primitive
1.14 yields gcd | p1 \<and> gcd | p2 \<and> gcd is primitive
1.15
1.16 argumentns "a b d M p" named according to [1] p.93 *)
1.17 - fun HENSEL_lifting_up a b d M p =
1.18 + fun iterate_CHINESE_up a b d M p =
1.19 let
1.20 val p = p next_prime_not_dvd d
1.21 val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p
1.22 @@ -392,7 +392,7 @@
1.23 let
1.24 val g = primitive_up (try_new_prime_up a b d M p g_p p)
1.25 in
1.26 - if (g %|% a) andalso (g %|% b) then g:unipoly else HENSEL_lifting_up a b d M p
1.27 + if (g %|% a) andalso (g %|% b) then g:unipoly else iterate_CHINESE_up a b d M p
1.28 end
1.29 end
1.30
1.31 @@ -405,7 +405,7 @@
1.32 let val d = abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))
1.33 in
1.34 if a = b then a else
1.35 - HENSEL_lifting_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1
1.36 + iterate_CHINESE_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1
1.37 end;
1.38 *}
1.39
1.40 @@ -679,10 +679,10 @@
1.41 (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))
1.42 end
1.43
1.44 - (* fn: poly -> poly -> int ->
1.45 - int -> int -> int list -> poly list -> poly
1.46 + (* try_new_r :: poly -> poly -> int -> int -> int -> int list -> poly list -> poly
1.47 + try_new_r a b n M r r_list steps =
1.48 assumes length a > 1 \<and> length b > 1
1.49 - yields TODO
1.50 + yields TODO
1.51 *)
1.52 and try_new_r a b n M r r_list steps =
1.53 let
1.54 @@ -691,16 +691,18 @@
1.55 val g_r = gcd_poly' (order (eval a (n - 2) r))
1.56 (order (eval b (n - 2) r)) (n - 1) 0
1.57 val steps = steps @ [g_r];
1.58 - in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end
1.59 - (* fn: poly -> poly -> int ->
1.60 - int -> int -> int -> int list -> poly list ->
1.61 - | poly -> poly -> int list -> poly
1.62 + in iterate_CHINESE a b n M 1 r r_list steps g_r (zero_poly n) [1] end
1.63 +
1.64 + (* iterate_CHINESE :: poly -> poly -> int -> int -> int -> int -> int list ->
1.65 + | poly list -> poly -> poly -> int list -> poly
1.66 + iterate_CHINESE a | b n M m r r_list
1.67 + steps g g_n mult =
1.68 assumes length a > 1 \<and> length b > 1
1.69 - yields TODO
1.70 + yields TODO
1.71 *)
1.72 - and HENSEL_lifting a b n M m r r_list steps g g_n mult =
1.73 + and iterate_CHINESE a b n M m r r_list steps g g_n mult =
1.74 if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else
1.75 - try_new_r a b n M r r_list steps
1.76 + try_new_r a b n M r r_list steps
1.77 else
1.78 let
1.79 val r = find_new_r a b r;
1.80 @@ -709,20 +711,20 @@
1.81 (order (eval b (n - 2) r)) (n - 1) 0
1.82 in
1.83 if lex_ord (lmonom g) (lmonom g_r)
1.84 - then HENSEL_lifting a b n M 1 r r_list steps g g_n mult
1.85 - else if (lexp g) = (lexp g_r)
1.86 + then iterate_CHINESE a b n M 1 r r_list steps g g_n mult
1.87 + else if lexp g = lexp g_r
1.88 then
1.89 let val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2)
1.90 in
1.91 - if (nth steps (length steps - 1)) = (zero_poly (n - 1))
1.92 - then HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new
1.93 - else HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
1.94 + if nth steps (length steps - 1) = zero_poly (n - 1)
1.95 + then iterate_CHINESE a b n M (M + 1) r r_list steps g_r g_n new
1.96 + else iterate_CHINESE a b n M (m + 1) r r_list steps g_r g_n new
1.97 end
1.98 else (* \<not> lex_ord (lmonom g) (lmonom g_r) *)
1.99 - HENSEL_lifting a b n M (m + 1) r r_list steps g g_n mult
1.100 + iterate_CHINESE a b n M (m + 1) r r_list steps g g_n mult
1.101 end
1.102
1.103 - fun majority_of_coefficients_is_negative a b c =
1.104 + fun majority_of_coefficients_is_negative_in a b c =
1.105 let val cs = (coeffs a) @ (coeffs b) @ (coeffs c)
1.106 in length (filter (curry op < 0) cs) < length cs div 2 end
1.107
1.108 @@ -736,7 +738,7 @@
1.109 val (a': poly, _) = a %%/%% c
1.110 val (b': poly, _) = b %%/%% c
1.111 in
1.112 - if majority_of_coefficients_is_negative a' b' c
1.113 + if majority_of_coefficients_is_negative_in a' b' c
1.114 then ((a' %%* ~1, b' %%* ~1), c %%* ~1) (*makes results look nicer*)
1.115 else ((a', b'), c)
1.116 end
2.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 15:17:34 2013 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Sep 02 16:16:08 2013 +0200
2.3 @@ -105,10 +105,10 @@
2.4 because the gcd involves 2 polynomials (with the same length for their list of exponents).
2.5 *)
2.6 fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =
2.7 - (SOME (t |> monoms_of_term vs |> order)
2.8 + (SOME (t |> monoms_of_term vs |> order)
2.9 handle ERROR _ => NONE)
2.10 | poly_of_term vs t =
2.11 - (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
2.12 + (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
2.13 handle ERROR _ => NONE)
2.14
2.15 fun is_poly t =
2.16 @@ -180,6 +180,8 @@
2.17 val calc_rat_erls:rls
2.18 val cancel_p : rls
2.19 val cancel_p_ : theory -> term -> (term * term list) option
2.20 + val check_fraction : term -> (term * term) option
2.21 + val check_frac_sum : term -> ((term * term) * (term * term)) option
2.22 val common_nominator_p : rls
2.23 val common_nominator_p_ : theory -> term -> (term * term list) option
2.24 val eval_is_expanded : string -> 'a -> term -> theory ->
2.25 @@ -344,7 +346,7 @@
2.26 SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
2.27 a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
2.28 \<or> NONE *)
2.29 -fun cancel_p_ (thy: theory) t =
2.30 +fun cancel_p_ (_: theory) t =
2.31 let val opt = check_fraction t
2.32 in
2.33 case opt of
2.34 @@ -377,51 +379,49 @@
2.35 end
2.36 end
2.37
2.38 -(* addition of fractions allows (at most) one non-fraction ---postponed after 1st integration*)
2.39 -fun norm_frac_sum
2.40 +(* addition of fractions allows (at most) one non-fraction (a monomial) *)
2.41 +fun check_frac_sum
2.42 (Const ("Groups.plus_class.plus", _) $
2.43 (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $
2.44 (Const ("Fields.inverse_class.divide", _) $ n2 $ d2))
2.45 = SOME ((n1, d1), (n2, d2))
2.46 - | norm_frac_sum
2.47 + | check_frac_sum
2.48 (Const ("Groups.plus_class.plus", _) $
2.49 nofrac $
2.50 (Const ("Fields.inverse_class.divide", _) $ n2 $ d2))
2.51 = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
2.52 - | norm_frac_sum
2.53 + | check_frac_sum
2.54 (Const ("Groups.plus_class.plus", _) $
2.55 (Const ("Fields.inverse_class.divide", _) $ n1 $ d1) $
2.56 nofrac)
2.57 = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
2.58 - | norm_frac_sum _ = NONE
2.59 + | check_frac_sum _ = NONE
2.60
2.61 (* prepare a term for addition by providing the least common denominator as a product
2.62 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
2.63 -fun common_nominator_p_ (thy: theory) t =
2.64 - let val opt = norm_frac_sum t
2.65 +fun common_nominator_p_ (_: theory) t =
2.66 + let val opt = check_frac_sum t
2.67 in
2.68 case opt of
2.69 NONE => NONE
2.70 | SOME ((n1, d1), (n2, d2)) =>
2.71 - let
2.72 - val vs = t |> vars |> map free2str |> sort string_ord
2.73 - val baseT = type_of n1
2.74 - val expT = HOLogic.realT
2.75 + let val vs = t |> vars |> map free2str |> sort string_ord
2.76 in
2.77 case (poly_of_term vs d1, poly_of_term vs d2) of
2.78 (SOME a, SOME b) =>
2.79 let
2.80 val ((a', b'), c) = gcd_poly a b
2.81 - val d1' = term_of_poly baseT expT vs a'
2.82 - val d2' = term_of_poly baseT expT vs b'
2.83 - val c' = term_of_poly baseT expT vs c
2.84 + val (baseT, expT) = (type_of n1, HOLogic.realT)
2.85 + val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
2.86 (*----- minimum of parentheses & nice result, but breaks tests: -------------
2.87 val denom = HOLogic.mk_binop "Groups.times_class.times"
2.88 - (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c')
2.89 - --------------------------------------------------------------------------*)
2.90 - val denom = HOLogic.mk_binop "Groups.times_class.times" (c',
2.91 - HOLogic.mk_binop "Groups.times_class.times" (d1', d2'))
2.92 - (*--------------------------------------------------------------------------*)
2.93 + (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)
2.94 + val denom =
2.95 + if c = [(1, replicate (length vs) 0)]
2.96 + then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')
2.97 + else
2.98 + HOLogic.mk_binop "Groups.times_class.times" (c',
2.99 + HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)
2.100 val t' =
2.101 HOLogic.mk_binop "Groups.plus_class.plus"
2.102 (HOLogic.mk_binop "Fields.inverse_class.divide"
2.103 @@ -438,29 +438,24 @@
2.104 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
2.105 NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
2.106 fun add_fraction_p_ (thy: theory) t =
2.107 - let val opt = norm_frac_sum t
2.108 - in
2.109 - case opt of
2.110 - NONE => NONE
2.111 - | SOME ((n1, d1), (n2, d2)) =>
2.112 - let
2.113 - val vs = t |> vars |> map free2str |> sort string_ord
2.114 - val baseT = type_of n1
2.115 - val expT = HOLogic.realT
2.116 - in
2.117 - (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
2.118 - (SOME _, SOME a, SOME _, SOME b) =>
2.119 - let
2.120 - val ((a', b'), c) = gcd_poly a b
2.121 - val nomin = term_of_poly baseT expT vs
2.122 - (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
2.123 - val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
2.124 - val t' = HOLogic.mk_binop "Fields.inverse_class.divide" (nomin, denom)
2.125 - val asm = mk_asms baseT [denom]
2.126 - in SOME (t', asm) end
2.127 - | _ => NONE : (term * term list) option
2.128 - end
2.129 - end
2.130 + case check_frac_sum t of
2.131 + NONE => NONE
2.132 + | SOME ((n1, d1), (n2, d2)) =>
2.133 + let
2.134 + val vs = t |> vars |> map free2str |> sort string_ord
2.135 + in
2.136 + case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
2.137 + (SOME _, SOME a, SOME _, SOME b) =>
2.138 + let
2.139 + val ((a', b'), c) = gcd_poly a b
2.140 + val (baseT, expT) = (type_of n1, HOLogic.realT)
2.141 + val nomin = term_of_poly baseT expT vs
2.142 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
2.143 + val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
2.144 + val t' = HOLogic.mk_binop "Fields.inverse_class.divide" (nomin, denom)
2.145 + in SOME (t', mk_asms baseT [denom]) end
2.146 + | _ => NONE : (term * term list) option
2.147 + end
2.148
2.149 fun (x ins xs) = if x mem xs then xs else x :: xs;
2.150 fun xs union [] = xs
2.151 @@ -1708,9 +1703,6 @@
2.152 if count_neg(tl(the(term2coef' t (get_vars(t)))))=0 then true
2.153 else false;
2.154
2.155 -(*. checks for expanded term [3] .*)
2.156 -fun is_expanded t = test_exp t " " andalso check_coeff(t);
2.157 -
2.158 (*WN.7.3.03 Hilfsfunktion f"ur term2poly'*)
2.159 fun mk_monom v' p vs =
2.160 let fun conv p (v: string) = if v'= v then p else 0
2.161 @@ -3306,7 +3298,7 @@
2.162 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
2.163 errpatts = [],
2.164 scr=Rfuns {init_state = init_state thy Atools_erls ro,
2.165 - normal_form = add_fraction_p_ thy,(*FIXME.WN0211*)
2.166 + normal_form = add_fraction_p_ thy, (*FIXME.WN0211*)
2.167 locate_rule = locate_rule thy Atools_erls ro,
2.168 next_rule = next_rule thy Atools_erls ro,
2.169 attach_form = attach_form}}
3.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 15:17:34 2013 +0200
3.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 16:16:08 2013 +0200
3.3 @@ -9,6 +9,11 @@
3.4 exception NO_REWRITE;
3.5 exception STOP_REW_SUB; (*WN050820 quick and dirty*)
3.6
3.7 +fun trace i str =
3.8 + if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()
3.9 +fun trace1 i str =
3.10 + if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()
3.11 +
3.12 (*
3.13 Synopsis rewriting (prep for reference manual):
3.14 ----------------------------------------------
3.15 @@ -114,12 +119,11 @@
3.16 and eval__true thy i asms bdv rls =
3.17 if asms = [@{term True}] orelse asms = [] then ([], true)
3.18 (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
3.19 - else if asms = [@{term False}] then ([], false)
3.20 - else
3.21 + else if asms = [@{term False}] then ([], false) else
3.22 let
3.23 fun chk indets [] = (indets, true)(*return asms<>True until false*)
3.24 | chk indets (a::asms) =
3.25 - (case rewrite__set_ thy (i+1) false bdv rls a of
3.26 + (case rewrite__set_ thy (i + 1) false bdv rls a of
3.27 NONE => (chk (indets @ [a]) asms)
3.28 | SOME (t, a') =>
3.29 if t = @{term True} then (chk (indets @ a') asms)
3.30 @@ -129,91 +133,67 @@
3.31 in chk [] asms end
3.32 (* rewrite with a rule set, which must not be the empty Erls *)
3.33 and rewrite__set_ _ _ __ Erls t =
3.34 - error("rewrite__set_ called with 'Erls' for '"^term2str t^"'")
3.35 + error ("rewrite__set_ called with 'Erls' for '" ^ term2str t ^ "'")
3.36 (* rewrite with a 'reverse rule set' implemented by ML code *)
3.37 | rewrite__set_ thy i _ _ (rrls as Rrls _) t =
3.38 - let val _= if ! trace_rewrite andalso i < ! depth
3.39 - then tracing ((idt"#"i)^" rls: "^(id_rls rrls)^" on: "^
3.40 - (term2str t)) else ()
3.41 - val (t', asm, rew) = app_rev thy (i+1) rrls t
3.42 - in if rew then SOME (t', distinct asm)
3.43 - else NONE end
3.44 + let
3.45 + val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str t)
3.46 + val (t', asm, rew) = app_rev thy (i + 1) rrls t
3.47 + in if rew then SOME (t', distinct asm) else NONE end
3.48 (* rewrite with a rule set containing Thms or Calculations *)
3.49 | rewrite__set_ thy i put_asm bdv rls ct =
3.50 -(* val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
3.51 - *)
3.52 - let
3.53 - datatype switch = Appl | Noap;
3.54 - fun rew_once ruls asm ct Noap [] = (ct,asm)
3.55 - | rew_once ruls asm ct Appl [] =
3.56 - (case rls of Rls _ => rew_once ruls asm ct Noap ruls
3.57 - | Seq _ => (ct,asm))
3.58 - | rew_once ruls asm ct apno (rul::thms) =
3.59 -(* val (ruls, asm, ct, apno, (rul::thms)) = (ruls, [], ct, Noap, ruls);
3.60 - val Thm (thmid, thm) = rul;
3.61 - *)
3.62 - case rul of
3.63 - Thm (thmid, thm) =>
3.64 - (if !trace_rewrite andalso i < ! depth
3.65 - then tracing((idt"#"(i+1))^" try thm: "^thmid) else ();
3.66 - case rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
3.67 - ((#erls o rep_rls) rls) put_asm thm ct of
3.68 - NONE => rew_once ruls asm ct apno thms
3.69 - | SOME (ct',asm') => (if ! trace_rewrite andalso i < ! depth
3.70 - then tracing((idt"="(i+1))^" rewrites to: "^
3.71 - (term2str ct')) else ();
3.72 - rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
3.73 - | Calc (cc as (op_,_)) =>
3.74 - (let val _= if !trace_rewrite andalso i < ! depth then
3.75 - tracing((idt"#"(i+1))^" try calc: "^op_^"'") else ();
3.76 - val ct = uminus_to_string ct
3.77 - in case get_calculation_ thy cc ct of
3.78 - NONE => rew_once ruls asm ct apno thms
3.79 - | SOME (thmid, thm') =>
3.80 - let
3.81 - val pairopt =
3.82 - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
3.83 - ((#erls o rep_rls) rls) put_asm thm' ct;
3.84 - val _ = if pairopt <> NONE then ()
3.85 - else error("rewrite_set_, rewrite_ \""^
3.86 - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
3.87 - val _ = if ! trace_rewrite andalso i < ! depth
3.88 - then tracing((idt"="(i+1))^" calc. to: "^
3.89 - (term2str ((fst o the) pairopt)))
3.90 - else()
3.91 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul::thms) end
3.92 - end)
3.93 - | Cal1 (cc as (op_,_)) =>
3.94 - (let val _= if !trace_rewrite andalso i < ! depth then
3.95 - tracing((idt"#"(i+1))^" try cal1: "^op_^"'") else ();
3.96 - val ct = uminus_to_string ct
3.97 - in case get_calculation1_ thy cc ct of
3.98 - NONE => (ct, asm)
3.99 - | SOME (thmid, thm') =>
3.100 - let
3.101 - val pairopt =
3.102 - rewrite__ thy (i+1) bdv ((snd o #rew_ord o rep_rls) rls)
3.103 - ((#erls o rep_rls) rls) put_asm thm' ct;
3.104 - val _ = if pairopt <> NONE then ()
3.105 - else error("rewrite_set_, rewrite_ \""^
3.106 - (string_of_thmI thm')^"\" "^(term2str ct)^" = NONE")
3.107 - val _ = if ! trace_rewrite andalso i < ! depth
3.108 - then tracing((idt"="(i+1))^" cal1. to: "^
3.109 - (term2str ((fst o the) pairopt)))
3.110 - else()
3.111 - in the pairopt end
3.112 - end)
3.113 - | Rls_ rls' =>
3.114 - (case rewrite__set_ thy (i+1) put_asm bdv rls' ct of
3.115 - SOME (t',asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
3.116 - | NONE => rew_once ruls asm ct apno thms);
3.117 -
3.118 - val ruls = (#rules o rep_rls) rls;
3.119 - val _= if ! trace_rewrite andalso i < ! depth
3.120 - then tracing ((idt"#"i)^" rls: "^(id_rls rls)^" on: "^
3.121 - (term2str ct)) else ()
3.122 - val (ct',asm') = rew_once ruls [] ct Noap ruls;
3.123 - in if ct = ct' then NONE else SOME (ct', distinct asm') end
3.124 + let
3.125 + datatype switch = Appl | Noap;
3.126 + fun rew_once ruls asm ct Noap [] = (ct, asm)
3.127 + | rew_once ruls asm ct Appl [] =
3.128 + (case rls of Rls _ => rew_once ruls asm ct Noap ruls
3.129 + | Seq _ => (ct, asm))
3.130 + | rew_once ruls asm ct apno (rul::thms) =
3.131 + case rul of
3.132 + Thm (thmid, thm) =>
3.133 + (trace1 i (" try thm: " ^ thmid);
3.134 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
3.135 + ((#erls o rep_rls) rls) put_asm thm ct of
3.136 + NONE => rew_once ruls asm ct apno thms
3.137 + | SOME (ct',asm') =>
3.138 + (trace1 i (" rewrites to: " ^ term2str ct');
3.139 + rew_once ruls (union (op =) asm asm') ct' Appl (rul::thms)))
3.140 + | Calc (cc as (op_, _)) =>
3.141 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
3.142 + val ct = uminus_to_string ct
3.143 + in case get_calculation_ thy cc ct of
3.144 + NONE => rew_once ruls asm ct apno thms
3.145 + | SOME (thmid, thm') =>
3.146 + let
3.147 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
3.148 + ((#erls o rep_rls) rls) put_asm thm' ct;
3.149 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
3.150 + string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
3.151 + val _ = trace1 i (" calc. to: " ^ term2str ((fst o the) pairopt))
3.152 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
3.153 + end
3.154 + | Cal1 (cc as (op_, _)) =>
3.155 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
3.156 + val ct = uminus_to_string ct
3.157 + in case get_calculation1_ thy cc ct of
3.158 + NONE => (ct, asm)
3.159 + | SOME (thmid, thm') =>
3.160 + let
3.161 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)
3.162 + ((#erls o rep_rls) rls) put_asm thm' ct;
3.163 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
3.164 + string_of_thmI thm' ^ "\" " ^ term2str ct ^ " = NONE")
3.165 + val _ = trace1 i (" cal1. to: " ^ term2str ((fst o the) pairopt))
3.166 + in the pairopt end
3.167 + end
3.168 + | Rls_ rls' =>
3.169 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
3.170 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
3.171 + | NONE => rew_once ruls asm ct apno thms);
3.172 + val ruls = (#rules o rep_rls) rls;
3.173 + val _= trace i (" rls: " ^ id_rls rls ^ " on: " ^ term2str ct)
3.174 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
3.175 + in if ct = ct' then NONE else SOME (ct', distinct asm') end
3.176
3.177 (* apply an Rrls; if not applicable proceed with subterms *)
3.178 and app_rev thy i rrls t =
3.179 @@ -233,7 +213,7 @@
3.180 if f pp then true else scan_ f pps;
3.181 in scan_ chk prepat end;
3.182 (* apply the normal_form of a rev-set *)
3.183 - fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
3.184 + fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =
3.185 if chk_prepat thy erls prepat t
3.186 then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
3.187 else NONE;
3.188 @@ -272,20 +252,9 @@
3.189 (*WN.11.6.03: shouldnt asm<>[] lead to false ????*)
3.190 fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
3.191
3.192 -
3.193 -(*.rewriting without internal argument [] for rew_ord.*)
3.194 -(* val (thy, rew_ord, erls, bool, thm, term) =
3.195 - (thy, (assoc_rew_ord ro), rls', false, (assoc_thm' thy thm'), f);
3.196 - val (thy, rew_ord, erls, bool, thm, term) =
3.197 - (thy, rew_ord, erls, false, thm, t'');
3.198 - *)
3.199 -fun rewrite_ thy rew_ord erls bool thm term =
3.200 - rewrite__ thy 1 [] rew_ord erls bool thm term;
3.201 -fun rewrite_set_ thy bool rls term =
3.202 -(* val (thy, bool, rls, term) = (thy, false, srls, t);
3.203 - *)
3.204 - rewrite__set_ thy 1 bool [] rls term;
3.205 -
3.206 +(* rewriting without internal argument [] *)
3.207 +fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
3.208 +fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
3.209
3.210 fun subs'2subst thy (s:subs') =
3.211 (((map (apfst (term_of o the o (parse thy))))
4.1 --- a/src/Tools/isac/calcelems.sml Mon Sep 02 15:17:34 2013 +0200
4.2 +++ b/src/Tools/isac/calcelems.sml Mon Sep 02 16:16:08 2013 +0200
4.3 @@ -97,7 +97,7 @@
4.4 and scr =
4.5 EmptyScr
4.6 | Prog of term (* for met *)
4.7 - | Rfuns of (* for Rrls*)
4.8 + | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
4.9 {init_state : (* initialise for reverse rewriting by the Interpreter *)
4.10 term -> (* for this the rrlsstate is initialised: *)
4.11 term * (* the current formula: goes locate_gen -> next_tac via istate *)
4.12 @@ -194,9 +194,9 @@
4.13
4.14 val e_rule = Thm ("refl", @{thm refl});
4.15 fun id_of_thm (Thm (id, _)) = id
4.16 - | id_of_thm _ = error "id_of_thm";
4.17 + | id_of_thm _ = error "error id_of_thm";
4.18 fun thm_of_thm (Thm (_, thm)) = thm
4.19 - | thm_of_thm _ = error "thm_of_thm";
4.20 + | thm_of_thm _ = error "error thm_of_thm";
4.21 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
4.22
4.23 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
5.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Sep 02 15:17:34 2013 +0200
5.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Sep 02 16:16:08 2013 +0200
5.3 @@ -1273,8 +1273,8 @@
5.4 tree and check if every node implements that what we have wanted.*}
5.5
5.6 ML {*
5.7 - trace_rewrite := false;
5.8 - trace_script := false;
5.9 + trace_rewrite := false; (*true*)
5.10 + trace_script := false; (*true*)
5.11 print_depth 9;
5.12
5.13 val fmz =
5.14 @@ -1309,6 +1309,7 @@
5.15 " --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
5.16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
5.17 "SubProblem";
5.18 + print_depth 3;
5.19 *}
5.20
5.21 text {*\noindent Instead of \ttfamily nxt = Subproblem \normalfont above we had
5.22 @@ -1382,7 +1383,7 @@
5.23 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
5.24 \item What is the returned formula:
5.25 \begin{verbatim}
5.26 -print_depth 999; f; print_depth 999;
5.27 +print_depth 999; f; print_depth 3;
5.28 { Find = [ Correct "solutions z_i"],
5.29 With = [],
5.30 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
6.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Sep 02 15:17:34 2013 +0200
6.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Sep 02 16:16:08 2013 +0200
6.3 @@ -2465,7 +2465,7 @@
6.4 \ttfamily get\_obj g\_pbl pt (fst p);\normalfont? YES -- ok
6.5 \item What is the returned formula:
6.6 \begin{verbatim}
6.7 -print_depth 999; f; print_depth 999;
6.8 +print_depth 999; f; print_depth 3;
6.9 { Find = [ Correct "solutions z_i"],
6.10 With = [],
6.11 Given = [Correct "equality (-1 + -2*z + 8*z ^^^ 2 = 0)",
7.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Sep 02 15:17:34 2013 +0200
7.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Sep 02 16:16:08 2013 +0200
7.3 @@ -71,8 +71,7 @@
7.4 the internal representation of "a + b * 3". The '...' indicate that some
7.5 details are still hidden; further details are received this way:
7.6 *}
7.7 -ML {* print_depth 99;
7.8 - @{term "a + b * 9"}
7.9 +ML {* print_depth 99; @{term "a + b * 9"}; print_depth 5;
7.10 *}
7.11 text {* The internal representation is too comprehensive for several kinds of
7.12 inspection. Thus ISAC provides additional features, as we see below. First
8.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Sep 02 15:17:34 2013 +0200
8.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Sep 02 16:16:08 2013 +0200
8.3 @@ -120,6 +120,7 @@
8.4 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
8.5 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
8.6 ML {* val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; *}
8.7 +ML {* print_depth 3; *}
8.8 text{* And, please, note that the result of applying the 'nxt' ruleset is to be
8.9 found in the output of the next step !
8.10 *}
9.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Sep 02 15:17:34 2013 +0200
9.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Sep 02 16:16:08 2013 +0200
9.3 @@ -46,8 +46,7 @@
9.4 ([3, 2], Res)] then () else
9.5 error "calchead.sml: diff.behav. get_interval after replace} other 2 a";
9.6
9.7 -print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
9.8 -print_depth 3;
9.9 +print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); print_depth 3;
9.10 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
9.11 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
9.12 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
10.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Sep 02 15:17:34 2013 +0200
10.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Mon Sep 02 16:16:08 2013 +0200
10.3 @@ -402,7 +402,7 @@
10.4 "----------- fun guh2theID ------------------------------";
10.5
10.6 val guh = "thy_scri_ListG-thm-zip_Nil";
10.7 -print_depth 999;
10.8 +print_depth 3; (*999*)
10.9 take_fromto 1 4 (Symbol.explode guh);
10.10 take_fromto 5 9 (Symbol.explode guh);
10.11 val rest = takerest (9,(Symbol.explode guh));
11.1 --- a/test/Tools/isac/Interpret/script.sml Mon Sep 02 15:17:34 2013 +0200
11.2 +++ b/test/Tools/isac/Interpret/script.sml Mon Sep 02 16:16:08 2013 +0200
11.3 @@ -139,7 +139,7 @@
11.4 case nxt of (_, Apply_Method ["IntegrierenUndKonstanteBestimmen"]) => ()
11.5 | _ => error "script.sml, doesnt find Substitute #2";
11.6 (* ERROR: caused by f2str f *)
11.7 -trace_rewrite:=true;
11.8 +trace_rewrite := false;
11.9
11.10 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f(*------------------------*);
11.11 trace_rewrite:=false;
12.1 --- a/test/Tools/isac/Knowledge/atools.sml Mon Sep 02 15:17:34 2013 +0200
12.2 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Sep 02 16:16:08 2013 +0200
12.3 @@ -124,7 +124,7 @@
12.4 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 ()
12.5 else error "atools.sml diff.behav. in eval_boollist2sum";
12.6
12.7 -trace_rewrite:=true;
12.8 +trace_rewrite := false;
12.9 val srls_ = append_rls "srls_..Berechnung-erstSymbolisch" e_rls
12.10 [Calc ("Atools.boollist2sum", eval_boollist2sum "")];
12.11 val t = str2t
12.12 @@ -238,7 +238,7 @@
12.13 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
12.14
12.15 (*das rewriting l"asst sich beobachten mit
12.16 - trace_rewrite:=true;
12.17 +trace_rewrite := false;
12.18 *)
12.19
12.20 "------15.11.02 --------------------------";
12.21 @@ -246,7 +246,7 @@
12.22 val bdv = (term_of o the o (parse thy)) "bdv";
12.23 val a = (term_of o the o (parse thy)) "a";
12.24
12.25 - trace_rewrite:=true;
12.26 +trace_rewrite := false;
12.27 (* Anwenden einer Regelmenge aus Termorder.ML: *)
12.28 val SOME (t,_) =
12.29 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
13.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon Sep 02 15:17:34 2013 +0200
13.2 +++ b/test/Tools/isac/Knowledge/diff.sml Mon Sep 02 16:16:08 2013 +0200
13.3 @@ -99,7 +99,7 @@
13.4 val SOME (ctt,_) =
13.5 (rewrite_inst thy' "tless_true" "erls" false [("bdv","x")] thm ct);
13.6 "----- for 'd_d s a' we got 'a is_const' --> False --------vvv-----";
13.7 -trace_rewrite := true;
13.8 +trace_rewrite := false;
13.9 val ct = "d_d s a";
13.10 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
13.11 (*got: NONE instead SOME*)
14.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Mon Sep 02 15:17:34 2013 +0200
14.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Mon Sep 02 16:16:08 2013 +0200
14.3 @@ -671,7 +671,7 @@
14.4 term2str s;
14.5 val t = str2term
14.6 "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
14.7 -trace_rewrite:=true;
14.8 +trace_rewrite := false;
14.9 val SOME (t',_) = rewrite_set_ thy false list_rls t;
14.10 trace_rewrite:=false;
14.11 val s' = term2str t';
15.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Sep 02 15:17:34 2013 +0200
15.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Sep 02 16:16:08 2013 +0200
15.3 @@ -360,7 +360,7 @@
15.4 [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
15.5 val t = str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^
15.6 "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]");
15.7 -trace_rewrite:=true;
15.8 +trace_rewrite := false;
15.9 val SOME (t',_) = rewrite_set_ thy false prls_triangular t;
15.10 (*found:...
15.11 ## try thm: NTH_CONS
15.12 @@ -421,7 +421,7 @@
15.13 val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
15.14 \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]",
15.15 "solveForVars [c, c_2]", "solution LL"];
15.16 -trace_rewrite:=true;
15.17 +trace_rewrite := false;
15.18 val matches = refine fmz ["2x2", "linear","system"];
15.19 trace_rewrite:=false;
15.20 print_depth 11; matches; print_depth 3;
16.1 --- a/test/Tools/isac/Knowledge/gcd_poly_winkler.sml Mon Sep 02 15:17:34 2013 +0200
16.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_winkler.sml Mon Sep 02 16:16:08 2013 +0200
16.3 @@ -86,7 +86,7 @@
16.4 doe not conform with the Isabelle coding standards)
16.5 *}*)
16.6
16.7 - print_depth 20;
16.8 + print_depth 3; (*20*)
16.9 type unipoly = int list;
16.10
16.11 "----------- auxiliary functions univariate -------------";
17.1 --- a/test/Tools/isac/Knowledge/poly.sml Mon Sep 02 15:17:34 2013 +0200
17.2 +++ b/test/Tools/isac/Knowledge/poly.sml Mon Sep 02 16:16:08 2013 +0200
17.3 @@ -381,11 +381,11 @@
17.4 ... then trace_rewrite:*)
17.5
17.6 "-----2 ---";
17.7 -trace_rewrite := true;
17.8 +trace_rewrite := false;
17.9 match_pbl fmz pbt;
17.10 trace_rewrite := false;
17.11 (*... if there is no rewrite, then there is something wrong with prls*)
17.12 -
17.13 +
17.14 "-----3 ---";
17.15 print_depth 7;
17.16 val prls = (#prls o get_pbt) ["polynomial","simplification"];
18.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 15:17:34 2013 +0200
18.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 02 16:16:08 2013 +0200
18.3 @@ -1,17 +1,6 @@
18.4 (* Title: tests for rationals
18.5 - Author: Stefan Karnel
18.6 - Copyright (c) Stefan Karnel 2002
18.7 + Author: Walther Neuper
18.8 Use is subject to license terms.
18.9 -
18.10 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
18.11 - 10 20 30 40 50 60 70 80
18.12 -LEGEND
18.13 -WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind
18.14 -WN070906
18.15 - nonterm.SK marks non-terminating examples
18.16 - ord.SK PARTIALLY marks crucial ordering examples
18.17 - *SK* of some (secondary) interest (on 070906)
18.18 -WN060104 transfer examples marked with (*SR..*) to the exp-collection
18.19 *)
18.20
18.21 "-----------------------------------------------------------------------------";
18.22 @@ -21,19 +10,19 @@
18.23 "-------- fun poly_of_term ---------------------------------------------------";
18.24 "-------- fun is_poly --------------------------------------------------------";
18.25 "-------- fun term_of_poly ---------------------------------------------------";
18.26 -"-------- fun factout_p_ -----------------------------------------------------";
18.27 -"-------- fun cancel_p_ ------------------------------------------------------";
18.28 -"-------- fun common_nominator_p_ --------------------------------------------";
18.29 -"-------- fun add_fraction_p_ ------------------------------------------------";
18.30 -"-------- TODO ---------------------------------------------------------------";
18.31 -"-------- and app_rev --------------------------------------------------------";
18.32 -"-------- external calculating functions test -----------";
18.33 -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
18.34 -"-------- common_nominator_p ----------------------------";
18.35 +"-------- integration lev.1 fun factout_p_ -----------------------------------";
18.36 +"-------- integration lev.1 fun cancel_p_ ------------------------------------";
18.37 +"-------- integration lev.1 fun common_nominator_p_ --------------------------";
18.38 +"-------- integration lev.1 fun add_fraction_p_ ------------------------------";
18.39 +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
18.40 +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
18.41 +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
18.42 +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
18.43 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
18.44 -"-------- reverse rewrite -------------------------------";
18.45 -"-------- 'reverse-ruleset' cancel_p --------------------";
18.46 -"-------- norm_Rational ---------------------------------";
18.47 +"-------- reverse rewrite ----------------------------------------------------";
18.48 +"-------- 'reverse-ruleset' cancel_p -----------------------------------------";
18.49 +"-------- investigate rls norm_Rational --------------------------------------";
18.50 +"-------- examples: rls norm_Rational ----------------------------------------";
18.51 "-------- numeral rationals -----------------------------";
18.52 "-------- cancellation ----------------------------------";
18.53 "-------- common denominator ----------------------------";
18.54 @@ -108,9 +97,9 @@
18.55 if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
18.56 then () else error "term_of_poly 1 changed";
18.57
18.58 -"-------- fun factout_p_ -----------------------------------------------------";
18.59 -"-------- fun factout_p_ -----------------------------------------------------";
18.60 -"-------- fun factout_p_ -----------------------------------------------------";
18.61 +"-------- integration lev.1 fun factout_p_ -----------------------------------";
18.62 +"-------- integration lev.1 fun factout_p_ -----------------------------------";
18.63 +"-------- integration lev.1 fun factout_p_ -----------------------------------";
18.64 val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
18.65 val SOME (t', asm) = factout_p_ thy t;
18.66 if term2str t' = "(x + y) * (x + -1 * y) / (x * (x + -1 * y))"
18.67 @@ -128,9 +117,9 @@
18.68 terms2str asm = "[\"1 + x ~= 0\"]"
18.69 then () else error "factout_p_ 1 changed";
18.70
18.71 -"-------- fun cancel_p_ ------------------------------------------------------";
18.72 -"-------- fun cancel_p_ ------------------------------------------------------";
18.73 -"-------- fun cancel_p_ ------------------------------------------------------";
18.74 +"-------- integration lev.1 fun cancel_p_ ------------------------------------";
18.75 +"-------- integration lev.1 fun cancel_p_ ------------------------------------";
18.76 +"-------- integration lev.1 fun cancel_p_ ------------------------------------";
18.77 val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
18.78 val SOME (t', asm) = cancel_p_ thy t;
18.79 if (term2str t', terms2str asm) = ("(x + y) / x", "[\"x ~= 0\"]")
18.80 @@ -144,9 +133,9 @@
18.81 if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[]"
18.82 then () else error "cancel_p_ 1 changed";
18.83
18.84 -"-------- fun common_nominator_p_ --------------------------------------------";
18.85 -"-------- fun common_nominator_p_ --------------------------------------------";
18.86 -"-------- fun common_nominator_p_ --------------------------------------------";
18.87 +"-------- integration lev.1 fun common_nominator_p_ --------------------------";
18.88 +"-------- integration lev.1 fun common_nominator_p_ --------------------------";
18.89 +"-------- integration lev.1 fun common_nominator_p_ --------------------------";
18.90 val t = str2term ("y / (a*x + b*x + c*x) " ^
18.91 (* n1 d1 *)
18.92 "+ a / (x*y)");
18.93 @@ -181,13 +170,13 @@
18.94 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
18.95 val SOME (t', asm) = common_nominator_p_ thy t;
18.96 if term2str t' =
18.97 - "(x + -1) * (-1 + x) / (1 * ((1 + x) * (-1 + x))) +\n(x + 1) * (1 + x) / (1 * ((1 + x) * (-1 + x)))"
18.98 + "(x + -1) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (-1 + x))"
18.99 andalso terms2str asm = "[\"1 + x ~= 0\",\"-1 + x ~= 0\"]"
18.100 then () else error "common_nominator_p_ 3 changed";
18.101
18.102 -"-------- fun add_fraction_p_ ------------------------------------------------";
18.103 -"-------- fun add_fraction_p_ ------------------------------------------------";
18.104 -"-------- fun add_fraction_p_ ------------------------------------------------";
18.105 +"-------- integration lev.1 fun add_fraction_p_ ------------------------------";
18.106 +"-------- integration lev.1 fun add_fraction_p_ ------------------------------";
18.107 +"-------- integration lev.1 fun add_fraction_p_ ------------------------------";
18.108 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
18.109 val SOME (t', asm) = add_fraction_p_ thy t;
18.110 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)"
18.111 @@ -205,15 +194,9 @@
18.112 terms2str asm = "[\"-1 + x ^^^ 2 ~= 0\"]"
18.113 then () else error "add_fraction_p_ 3 changed";
18.114
18.115 -"-------- TODO ---------------------------------------------------------------";
18.116 -"-------- TODO ---------------------------------------------------------------";
18.117 -"-------- TODO ---------------------------------------------------------------";
18.118 -
18.119 -
18.120 -
18.121 -"-------- and app_rev --------------------------------------------------------";
18.122 -"-------- and app_rev --------------------------------------------------------";
18.123 -"-------- and app_rev --------------------------------------------------------";
18.124 +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
18.125 +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
18.126 +"-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
18.127 (* trace down until prepats are evaluated
18.128 (which does not to work, because substitution is not done -- compare rew_sub!);
18.129 keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p
18.130 @@ -292,60 +275,64 @@
18.131 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a
18.132 ============ inhibit exn WN130823: prepat is empty ===================================*)
18.133
18.134 -(*========== inhibit exn WN130824 TODO =======================================================
18.135 -"-------- external calculating functions test -----------";
18.136 -"-------- external calculating functions test -----------";
18.137 -"-------- external calculating functions test -----------";
18.138 -val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
18.139 -val SOME (t', asm) = factout_p_ thy t;
18.140 -if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]"
18.141 -then () else error "factout_p_ 1 changed";
18.142 -val SOME (t', asm) = cancel_p_ thy t;
18.143 -if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]"
18.144 -then () else error "cancel_p_ 1 changed";
18.145 +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
18.146 +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
18.147 +"-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
18.148 +val t = str2term "(12 * x * y) / (8 * y^^^2 )";
18.149 +(* "-------- example 187a": exception Div raised...
18.150 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
18.151 +val t = str2term "(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
18.152 +(* "-------- example 187b": doesn't terminate...
18.153 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
18.154 +val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";
18.155 +(* "-------- example 187c": doesn't terminate...
18.156 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
18.157 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac}, false, cancel_p, t);
18.158 +(* WN130827: exception Div raised...
18.159 +rewrite__set_ thy 1 bool [] rls term
18.160 +*)
18.161 +"~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
18.162 + (thy, 1, bool, [], rls, term);
18.163 +(* WN130827: exception Div raised...
18.164 + val (t', asm, rew) = app_rev thy (i+1) rrls t
18.165 +*)
18.166 +"~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
18.167 +(* WN130827: exception Div raised...
18.168 + val opt = app_rev' thy rrls t
18.169 +*)
18.170 +"~~~~~ fun app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
18.171 + (thy, rrls, t);
18.172 +chk_prepat thy erls prepat t = true;
18.173 +(* WN130827: exception Div raised...
18.174 +normal_form t
18.175 +*)
18.176 +(* lookup Rational.thy, cancel_p: normal_form = cancel_p_ thy*)
18.177 +"~~~~~ fun cancel_p_, args:"; val (t) = (t);
18.178 +val opt = check_fraction t;
18.179 +val SOME (numerator, denominator) = opt
18.180 + val vs = t |> vars |> map free2str |> sort string_ord
18.181 + val baseT = type_of numerator
18.182 + val expT = HOLogic.realT
18.183 +val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
18.184 +(*"-------- example 187a": exception Div raised...
18.185 +val a = [(12, [1, 1])]: poly
18.186 +val b = [(8, [0, 2])]: poly
18.187 + val ((a', b'), c) = gcd_poly a b
18.188 +*)
18.189 +(* "-------- example 187b": doesn't terminate...
18.190 +val a = [(8, [2, 1, 1])]: poly
18.191 +val b = [(18, [1, 2, 1])]: poly
18.192 + val ((a', b'), c) = gcd_poly a b
18.193 +*)
18.194 +(* "-------- example 187c": doesn't terminate...
18.195 +val a = [(9, [5, 2, 4])]: poly
18.196 +val b = [(15, [6, 3, 1])]: poly
18.197 + val ((a', b'), c) = gcd_poly a b
18.198 +*)
18.199
18.200 -val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
18.201 -val SOME (t', asm) = factout_(*p_*) thy t;
18.202 -if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]"
18.203 -then () else error "factout_ 2 changed";
18.204 -val SOME (t', asm) = cancel_(*p_*) thy t;
18.205 -if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]"
18.206 -then () else error "cancel_ 2 changed";
18.207 -
18.208 -val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
18.209 -val SOME (t', asm) = add_fraction_p_ thy t;
18.210 -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
18.211 -then () else error "add_fraction_p_ 3 changed";
18.212 -val SOME (t', asm) = common_nominator_p_ thy t;
18.213 -if term2str t' =
18.214 - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
18.215 - andalso terms2str asm = "[]"
18.216 -then () else error "common_nominator_p_ 3 changed";
18.217 -
18.218 -val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
18.219 -val SOME (t', asm) = add_fraction_ thy t;
18.220 -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
18.221 -then () else error "factout_ 4 changed";
18.222 -val SOME (t', asm) = common_nominator_ thy t;
18.223 -if term2str t' =
18.224 - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
18.225 - andalso terms2str asm = "[]"
18.226 -then () else error "cancel_ 4 changed";
18.227 -
18.228 -val t = str2term
18.229 - "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
18.230 -val SOME (t', asm) = add_fraction_p_ thy t;
18.231 -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
18.232 -then () else error "add_fraction_p_ 5 changed";
18.233 -val SOME (t', asm) = norm_rational_ thy t;
18.234 -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
18.235 -then () else error "norm_rational_ 5 changed";
18.236 -============ inhibit exn WN130826 TODO ========================================================*)
18.237 -
18.238 -
18.239 -"-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
18.240 -"-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
18.241 -"-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
18.242 +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
18.243 +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
18.244 +"-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
18.245 val thy = @{theory "Rational"};
18.246 "-------- WN";
18.247 val t = str2term "(2 + -3 * x) / 9";
18.248 @@ -512,554 +499,19 @@
18.249 if (term2str t', terms2str asm) = ("(2 * x + 10 * x ^^^ 2) / (1 + -5 * x)", "[]")
18.250 then () else error "rational.sml cancel WN 1";
18.251
18.252 -(*========== inhibit exn WN130826 TODO =========================================================
18.253 -"-------- some old tests REVISE ! --------------------------------------------";
18.254 -"-------- some old tests REVISE ! --------------------------------------------";
18.255 -"-------- some old tests REVISE ! --------------------------------------------";
18.256 -(*WAS --- external calculating functions test ---*)
18.257 -val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
18.258 -val SOME (t', asm) = factout_p_ thy t;
18.259 -if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]"
18.260 -then () else error "factout_p_ 1 changed";
18.261 -val SOME (t', asm) = cancel_p_ thy t;
18.262 -if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]"
18.263 -then () else error "cancel_p_ 1 changed";
18.264 +"-------- example heuberger";
18.265 +val t = str2term ("(x^^^4 + x * y + x^^^3 * y + y^^^2) / " ^
18.266 + "(x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)");
18.267 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
18.268 +if (term2str t', terms2str asm) =
18.269 + ("(x ^^^ 3 + y) / (1 + 5 * x + x * y ^^^ 3)", "[\"1 + 5 * x + x * y ^^^ 3 ~= 0\"]")
18.270 +then () else error "rational.sml cancel_p heuberger";
18.271
18.272 -val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
18.273 -val SOME (t', asm) = factout_(*p_*) thy t;
18.274 -if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]"
18.275 -then () else error "factout_ 2 changed";
18.276 -val SOME (t', asm) = cancel_(*p_*) thy t;
18.277 -if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]"
18.278 -then () else error "cancel_ 2 changed";
18.279 +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
18.280 +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
18.281 +"-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
18.282 +(*deleted example 204 ... 236b at update Isabelle2012-->2013*)
18.283
18.284 -val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
18.285 -val SOME (t', asm) = add_fraction_p_ thy t;
18.286 -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
18.287 -then () else error "add_fraction_p_ 3 changed";
18.288 -val SOME (t', asm) = common_nominator_p_ thy t;
18.289 -if term2str t' =
18.290 - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
18.291 - andalso terms2str asm = "[]"
18.292 -then () else error "common_nominator_p_ 3 changed";
18.293 -
18.294 -val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
18.295 -val SOME (t', asm) = add_fraction_ thy t;
18.296 -if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
18.297 -then () else error "factout_ 4 changed";
18.298 -val SOME (t', asm) = common_nominator_ thy t;
18.299 -if term2str t' =
18.300 - "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
18.301 - andalso terms2str asm = "[]"
18.302 -then () else error "cancel_ 4 changed";
18.303 -
18.304 -val t = str2term
18.305 - "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
18.306 -val SOME (t', asm) = add_fraction_p_ thy t;
18.307 -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
18.308 -then () else error "add_fraction_p_ 5 changed";
18.309 -val SOME (t', asm) = norm_rational_ thy t;
18.310 -if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
18.311 -then () else error "norm_rational_ 5 changed";
18.312 -
18.313 -
18.314 -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))";
18.315 -val SOME (t3',_) = common_nominator_ thy t3;
18.316 -val SOME (t3'',_) = add_fraction_ thy t3;
18.317 -(term2str t3');
18.318 -(term2str t3'');
18.319 -
18.320 -val SOME(t4,t5) = norm_expanded_rat_ thy t3;
18.321 -term2str t4;
18.322 -term2str (hd(t5));
18.323 -
18.324 -
18.325 -
18.326 - val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
18.327 - val SOME (t',_) = factout_ thy t;
18.328 - val SOME (t'',_) = cancel_ thy t;
18.329 - term2str t';
18.330 - term2str t'';
18.331 - "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
18.332 - "(3 + x) / (3 - x)";
18.333 -
18.334 - val t=(term_of o the o (parse thy))
18.335 - "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)";
18.336 - val SOME (t',_) = common_nominator_ thy t;
18.337 - val SOME (t'',_) = add_fraction_ thy t;
18.338 - term2str t';
18.339 - term2str t'';
18.340 - "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))";
18.341 - "(4 + x) / (3 - x)";
18.342 -
18.343 -(*WN021016 added -----vv---*)
18.344 -val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
18.345 -val SOME (t',_) = common_nominator_ thy t;
18.346 -val SOME (t'',_) = add_fraction_ thy t;
18.347 -term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1" ^
18.348 - " * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
18.349 -term2str t'' = "6 / (3 - x)" (*true*);
18.350 -
18.351 -val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
18.352 -val SOME (t',_) = common_nominator_ thy t;
18.353 -val SOME (t'',_) = add_fraction_ thy t;
18.354 -term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n" ^
18.355 - "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
18.356 -term2str t'' = "6 / (3 - x)" (*true*);
18.357 -(*WN021016 added -----^^---*)
18.358 -(*WN030602 added -----vv--- no rewrite -> NONE !*)
18.359 -val t = str2term "1 / a";
18.360 -val NONE = cancel_p_ thy t;
18.361 -val NONE = rewrite_set_ thy false cancel_p t;
18.362 -(*WN.2.6.03 added -------^^---*)
18.363 -
18.364 -val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
18.365 -val SOME (t',_) = factout_ thy t;
18.366 -val SOME (t'',_) = cancel_ thy t;
18.367 -term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*);
18.368 -term2str t'' = "(y + x) / (y - x)";
18.369 -
18.370 -val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
18.371 -val SOME (t',_) = common_nominator_ thy t;
18.372 -val SOME (t'',_) = add_fraction_ thy t;
18.373 -term2str t' =
18.374 -"(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1" ^
18.375 -" * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*);
18.376 -term2str t'' = "(-1 - x - y) / (x - y)" (*true*);
18.377 -
18.378 -val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
18.379 -val SOME (t',_) = common_nominator_ thy t;
18.380 -val SOME (t'',_) = add_fraction_ thy t;
18.381 -if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))" ^
18.382 -" +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then ()
18.383 -else error "rational.sml lex-ord 1";
18.384 -if term2str t'' = "(-1 - y - x) / (y - x)" then ()
18.385 -else error "rational.sml lex-ord 2";
18.386 -(*WN.16.10.02 WN070905 lexicographische Ordnung erhalten *)
18.387 -
18.388 -
18.389 -val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
18.390 -val SOME (t',_) = norm_expanded_rat_ thy t;
18.391 -if term2str t' = "(x + y) / (x - y)" then ()
18.392 -else error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 No.1";
18.393 -(*val SOME (t'',_) = norm_rational_ thy t;
18.394 - *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
18.395 -WN.16.10.02 ?! + WN060831???SK4
18.396 -WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*)
18.397 -
18.398 -
18.399 -val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
18.400 -val SOME (t',_) = norm_expanded_rat_ thy t;
18.401 -if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then ()
18.402 -else error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
18.403 -(*val SOME (t'',_) = norm_rational_ thy t;
18.404 - *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!
18.405 -WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*)
18.406 -
18.407 - val t=(term_of o the o (parse thy))
18.408 - "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
18.409 - val SOME (t',_) = norm_expanded_rat_ thy t;
18.410 - val SOME (t'',_) = norm_rational_ thy t;
18.411 - term2str t';
18.412 - term2str t'';
18.413 - "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
18.414 - "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)";
18.415 -
18.416 -
18.417 -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
18.418 -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
18.419 -"-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
18.420 -val thy = @{theory "Rational"};
18.421 -val thy' = "Rational";
18.422 -val rls' = "cancel";
18.423 -val mp = "make_polynomial";
18.424 -
18.425 -writeln ("example 186:");
18.426 -writeln("a)");
18.427 -val e186a'="(14 * x * y) / ( x * y )";(*SRC*)
18.428 -rewrite_set_ thy false cancel (str2term e186a');
18.429 -"@@@@@@@@@@@@@@";
18.430 -val e186a = the (rewrite_set thy' false "cancel" e186a');
18.431 - is_expanded (parse_rat "14 * x * y");
18.432 - is_expanded (parse_rat "x * y");
18.433 -if e186a = ("14 / 1", "[\"y * x ~= 0\"]") then ()
18.434 -else error "rational.sml cancel Schalk e186a";
18.435 -
18.436 -writeln("b)");
18.437 -val e186b'="(60 * a * b) / ( 15 * a * b )";
18.438 -val e186b = the (rewrite_set thy' false "cancel" e186b');
18.439 -writeln("c)");
18.440 -val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
18.441 -val e186c = (the (rewrite_set thy' false "cancel" e186c'))
18.442 - handle e => print_exn_G e;
18.443 -val t = (term_of o the o (parse thy)) e186c';
18.444 -if e186c = ("12 * a / 1", "[\"12 * (c * (b * a)) ~= 0\"]") then ()
18.445 -else error "rational.sml cancel Schalk e186c";
18.446 -
18.447 -writeln ("example 187:");
18.448 -writeln("a)");
18.449 -val e187a'="(12 * x * y) / (8 * y^^^2 )";(*SRC*)
18.450 -val e187a = the (rewrite_set thy' false "cancel" e187a');
18.451 -writeln("b)");
18.452 -val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
18.453 -val e187b = the (rewrite_set thy' false "cancel" e187b');
18.454 -writeln("c)");
18.455 -val e187d'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*)
18.456 -val e187d = the (rewrite_set thy' false "cancel" e187d');
18.457 -if e187d = ("3 * z ^^^ 3 / (5 * (y * x))",
18.458 - "[\"3 * (z * (y ^^^ 2 * x ^^^ 5)) ~= 0\"]") then ()
18.459 -else error "rational.sml cancel Schalk e186d";
18.460 -
18.461 -writeln "example 188:";
18.462 -val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*)
18.463 -val e188a = the (rewrite_set thy' false "cancel" e188a');
18.464 - is_expanded (parse_rat "8 * x + -8");
18.465 -(* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
18.466 -if e188a = ("8 / 9", "[\"-1 + x ~= 0\"]") then ()
18.467 -else error "rational.sml: e188a new behaviour";
18.468 -
18.469 -val SOME (t,_) = rewrite_set thy' false mp "(8*((-1) + x))/(9*((-1) + x))";
18.470 -writeln("b)");
18.471 -val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
18.472 -val SOME (t, asm) = rewrite_set thy' false "cancel" e188b';
18.473 -t = "5 / 6" (*true*);
18.474 -writeln("c)");
18.475 -
18.476 -val e188c'="( a + -1 * b ) / ( b + -1 * a )";
18.477 -val e188c = the (rewrite_set thy' false "cancel_p" e188c');
18.478 -(*is_expanded (parse_rat "a + -1 * b");*)
18.479 -val SOME (t,_) =
18.480 - rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
18.481 -if t= "(a + -1 * b) / (-1 * a + b)" then()
18.482 -else error "rational.sml: e188c new behaviour";
18.483 -
18.484 -writeln ("example 190:");
18.485 -writeln("c)");
18.486 -val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
18.487 -val e190c = the (rewrite_set thy' false "cancel" e190c');
18.488 -val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
18.489 -if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
18.490 -else error "rational.sml: e190c new behaviour";
18.491 -
18.492 -writeln ("example 191:");
18.493 -writeln("a)");
18.494 -val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )";
18.495 -(*WN.23.10.02-------
18.496 -val e191a = the (rewrite_set thy' false "cancel" e191a');
18.497 - is_expanded (parse_rat "x^^^2 + -1 * y^^^2");
18.498 - false;
18.499 - is_expanded (parse_rat "x + y");
18.500 - true; -----------*)
18.501 -val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
18.502 -(* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
18.503 -if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
18.504 -else error "rational.sml: e191a new behaviour";
18.505 -
18.506 -writeln("c)");
18.507 -val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
18.508 -(*WN.23.10.02-------
18.509 -val e191c = the (rewrite_set thy' false "cancel" e191c');
18.510 - is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25");
18.511 - false;
18.512 - is_expanded (parse_rat "25 + -30*x + 9*x^^^2");
18.513 - false;
18.514 - is_expanded (parse_rat "-25 + 9*x^^^2");
18.515 - true;------------*)
18.516 -val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
18.517 -(* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
18.518 -if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
18.519 -else error "rational.sml: 'e191c' new behaviour";
18.520 -
18.521 -
18.522 -writeln ("example 192:");
18.523 -writeln("b)");
18.524 -val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
18.525 -(*WN.23.10.02-------
18.526 -val e192b = the (rewrite_set thy' false "cancel" e192b');
18.527 --------------------*)
18.528 -val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
18.529 -(*========== inhibit exn 110317 ================================================
18.530 -if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)"
18.531 -(*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*)
18.532 -then () else error "rational.sml: 'e192b' new behaviour";
18.533 -(*^^^ works with MG's simplifier vvv*)
18.534 -val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
18.535 -val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
18.536 -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";
18.537 -============ inhibit exn 110317 ==============================================*)
18.538 -
18.539 -writeln ("example 193:");
18.540 -writeln("a)");
18.541 -val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
18.542 -(*WN.23.10.02-------
18.543 -val e193a = the (rewrite_set thy' false "cancel" e193a');
18.544 --------------------*)
18.545 -writeln("b)");
18.546 -val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
18.547 -(*WN.23.10.02-------
18.548 -val e193b = the (rewrite_set thy' false "cancel" e193b');
18.549 -writeln("c)");
18.550 -val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
18.551 -val SOME(t,_) = rewrite_set thy' false "cancel" e193c';
18.552 --------------------*)
18.553 -
18.554 -val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
18.555 -val SOME (t, asm) = rewrite_set thy' false "cancel" wn01;
18.556 -(* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
18.557 -if t = "(-5 + 3 * x) / 1" andalso asm = "[\"5 + 3 * x ~= 0\"]" then ()
18.558 -else error "rational.sml: new behav. in cancel wn01";
18.559 -
18.560 -"-------- common_nominator_p ----------------------------";
18.561 -"-------- common_nominator_p ----------------------------";
18.562 -"-------- common_nominator_p ----------------------------";
18.563 -val rls' = "common_nominator_p";
18.564 -
18.565 -writeln ("example 204:");
18.566 -writeln("a)");
18.567 -val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)";
18.568 -val e204a = the (rewrite_set thy' false "common_nominator_p" e204a');
18.569 -writeln("b)");
18.570 -val e204b'="5 / x + -3 / x + -1 / x";
18.571 -val e204b = the (rewrite_set thy' false "common_nominator_p" e204b');
18.572 -if e204b = ("1 / x", "[]") then ()
18.573 -else error "rational.sml common_nominator_p example e204b";
18.574 -
18.575 -writeln ("example 205:");
18.576 -writeln("a)");
18.577 -val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)";
18.578 -val e205a = the (rewrite_set thy' false "common_nominator_p" e205a');
18.579 -writeln("b)");
18.580 -val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)";
18.581 -val e205b = the (rewrite_set thy' false "common_nominator_p" e205b');
18.582 -if e205b = ("(1 + x) / 1", "[]") then ()
18.583 -else error "rational.sml common_nominator_p example e204b";
18.584 -
18.585 -writeln ("example 206:");
18.586 -writeln("a)");
18.587 -val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))";
18.588 -val e206a = the (rewrite_set thy' false "common_nominator_p" e206a');
18.589 -writeln("b)");
18.590 -val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))";
18.591 -val e206b = the (rewrite_set thy' false "common_nominator_p" e206b');
18.592 -
18.593 -writeln ("example 207:");
18.594 -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)) ";
18.595 -val e207 = the (rewrite_set thy' false "common_nominator_p" e207');
18.596 -
18.597 -writeln ("example 208:");
18.598 -val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) ";
18.599 -val e208 = the (rewrite_set thy' false "common_nominator_p" e208');
18.600 -
18.601 -writeln ("example 209:");
18.602 -val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) ";
18.603 -val e209 = the (rewrite_set thy' false "common_nominator_p" e209');
18.604 -
18.605 -writeln ("example 210:");
18.606 -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)) ";
18.607 -val e210 = the (rewrite_set thy' false "common_nominator_p" e210');
18.608 -
18.609 -writeln ("example 211:");
18.610 -writeln("a)");
18.611 -val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))";
18.612 -val e211a = the (rewrite_set thy' false "common_nominator_p" e211a');
18.613 -writeln("b)");
18.614 -val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))";
18.615 -val e211b = the (rewrite_set thy' false "common_nominator_p" e211b');
18.616 -
18.617 -writeln ("example 212:");
18.618 -writeln("a)");
18.619 -val e212a'="((4) / (x)) + ((-3) / (y)) + -1";
18.620 -val e212a = the (rewrite_set thy' false "common_nominator_p" e212a');
18.621 -writeln("b)");
18.622 -val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))";
18.623 -val e212b = the (rewrite_set thy' false "common_nominator_p" e212b');
18.624 -
18.625 -writeln ("example 213:");
18.626 -writeln("a)");
18.627 -val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) ";
18.628 -val e213a = the (rewrite_set thy' false "common_nominator_p" e213a');
18.629 -writeln("b)");
18.630 -val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))";
18.631 -val e213b = the (rewrite_set thy' false "common_nominator_p" e213b');
18.632 -
18.633 -writeln ("example 214:");
18.634 -writeln("a)");
18.635 -val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))";
18.636 -val e214a = the (rewrite_set thy' false "common_nominator_p" e214a');
18.637 -writeln("b)");
18.638 -val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))";
18.639 -val e214b = the (rewrite_set thy' false "common_nominator_p" e214b');
18.640 -
18.641 -writeln ("example 216:");
18.642 -writeln("a)");
18.643 -val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))";
18.644 -val e216a = the (rewrite_set thy' false "common_nominator_p" e216a');
18.645 -writeln("b)");
18.646 -val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))";
18.647 -val e216b = the (rewrite_set thy' false "common_nominator_p" e216b');
18.648 -
18.649 -writeln ("example 217:");
18.650 -val e217'="((z + -1) / (z)) + ((3 * z ^^^2 + -6 * z + 5) / (z^^^2)) + ((-4 * z^^^3 + 7 * z^^^2 + -5 * z + 5) / (z^^^3))";
18.651 -val e217 = the (rewrite_set thy' false "common_nominator_p" e217');
18.652 -
18.653 -
18.654 -val rls' = "common_nominator";
18.655 -writeln ("example 218:");
18.656 -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))";
18.657 -val e218 = the (rewrite_set thy' false "common_nominator" e218');
18.658 -if e218 = ("(16 - 63 * a ^^^ 2 - 81 * a ^^^ 3) / (108 * a ^^^ 4)", "[]") then ()
18.659 -else error "rationa.sml common_nominator example e218";
18.660 -
18.661 -writeln ("example 219:");
18.662 -writeln("a)");
18.663 -val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))";
18.664 -val e219a = the (rewrite_set thy' false "common_nominator" e219a');
18.665 -writeln("b)");
18.666 -val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))";
18.667 -val e219b = the (rewrite_set thy' false "common_nominator" e219b');
18.668 -if e219b = ("(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)", "[]") then ()
18.669 -else error "rationa.sml common_nominator example e219b";
18.670 -
18.671 -writeln ("example 220:");
18.672 -writeln("a)");
18.673 -val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))";
18.674 -val e220a = the (rewrite_set thy' false "common_nominator" e220a');
18.675 -writeln("b)");
18.676 -val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))";
18.677 -val e220b = the (rewrite_set thy' false "common_nominator" e220b');
18.678 -
18.679 -writeln ("example 221:");
18.680 -writeln("a)");
18.681 -val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))";
18.682 -val e221a = the (rewrite_set thy' false "common_nominator" e221a');
18.683 -writeln("b)");
18.684 -val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) ";
18.685 -val e221b = the (rewrite_set thy' false "common_nominator" e221b');
18.686 -
18.687 -writeln ("example 222:");
18.688 -writeln("a)");
18.689 -val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))";
18.690 -val e222a = the (rewrite_set thy' false "common_nominator" e222a');
18.691 -writeln("b)");
18.692 -val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))";
18.693 -val e222b = the (rewrite_set thy' false "common_nominator" e222b');
18.694 -
18.695 -writeln ("example 225:");
18.696 -writeln("a)");
18.697 -val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))";
18.698 -val e225a = the (rewrite_set thy' false "common_nominator" e225a');
18.699 -writeln("b)");
18.700 -val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))";
18.701 -val e225b = the (rewrite_set thy' false "common_nominator" e225b');
18.702 -
18.703 -writeln ("example 226:");
18.704 -writeln("a)");
18.705 -val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) ";
18.706 -val e226a = the (rewrite_set thy' false "common_nominator" e226a');
18.707 -writeln("b)");
18.708 -val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2";
18.709 -val e226b = the (rewrite_set thy' false "common_nominator" e226b');
18.710 -
18.711 -writeln ("example 227:");
18.712 -writeln("a)");
18.713 -val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 ";
18.714 -val e227a = the (rewrite_set thy' false "common_nominator" e227a');
18.715 -writeln("b)");
18.716 -val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 ";
18.717 -val e227b = the (rewrite_set thy' false "common_nominator" e227b');
18.718 -
18.719 -writeln ("example 228:");
18.720 -writeln("a)");
18.721 -val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))";
18.722 -val e228a = the (rewrite_set thy' false "common_nominator" e228a');
18.723 -writeln("b)");
18.724 -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))";
18.725 -val e228b = the (rewrite_set thy' false "common_nominator" e228b');
18.726 -
18.727 -
18.728 -writeln ("example 229:");
18.729 -writeln("a)");
18.730 -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))";
18.731 -val e229a = the (rewrite_set thy' false "common_nominator" e229a');
18.732 -writeln("b)");
18.733 -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))";
18.734 -val e229b = the (rewrite_set thy' false "common_nominator" e229b');
18.735 -
18.736 -writeln ("example 230:");
18.737 -writeln("a)");
18.738 -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))";
18.739 -val e230a = the (rewrite_set thy' false "common_nominator" e230a');
18.740 -writeln("b)");
18.741 -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))";
18.742 -val e230b = the (rewrite_set thy' false "common_nominator" e230b');
18.743 -
18.744 -writeln ("example 231:");
18.745 -writeln("a)");
18.746 -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))";
18.747 -val e231a = the (rewrite_set thy' false "common_nominator" e231a');
18.748 -writeln("b)");
18.749 -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))";
18.750 -val e231b = the (rewrite_set thy' false "common_nominator" e231b');
18.751 -
18.752 -writeln ("example 232:");
18.753 -writeln("a)");
18.754 -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))";
18.755 -val e232a = the (rewrite_set thy' false "common_nominator" e232a');
18.756 -writeln("b)");
18.757 -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))";
18.758 -val e232b = the (rewrite_set thy' false "common_nominator" e232b');
18.759 -
18.760 -writeln ("example 233:");
18.761 -writeln("a)");
18.762 -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))";
18.763 -val e233a = the (rewrite_set thy' false "common_nominator" e233a');
18.764 -writeln("b)");
18.765 -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))";
18.766 -val e233b = the (rewrite_set thy' false "common_nominator" e233b');
18.767 -
18.768 -writeln ("example 234:");
18.769 -writeln("a)");
18.770 -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))";
18.771 -val e234a = the (rewrite_set thy' false "common_nominator" e234a');
18.772 -writeln("b)");
18.773 -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)) ";
18.774 -val e234b = the (rewrite_set thy' false "common_nominator" e234b');
18.775 -
18.776 -writeln ("example 235:");
18.777 -writeln("a)");
18.778 -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))";
18.779 -val e235a = the (rewrite_set thy' false "common_nominator" e235a');
18.780 -writeln("b)");
18.781 -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)) ";
18.782 -val e235b = the (rewrite_set thy' false "common_nominator" e235b');
18.783 -
18.784 -writeln ("example 236:");
18.785 -writeln("a)");
18.786 -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))";
18.787 -val e236a = the (rewrite_set thy' false "common_nominator" e236a');
18.788 -writeln("b)");
18.789 -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)) ";
18.790 -val e236b = the (rewrite_set thy' false "common_nominator" e236b');
18.791 -
18.792 -
18.793 -val rls' = "cancel";
18.794 -writeln ("example heuberger:");
18.795 -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)";
18.796 -val eheu = the (rewrite_set thy' false "cancel" eheu');
18.797 -
18.798 -val rls' = "common_nominator_p";
18.799 -writeln ("example stiefel:");
18.800 -val est1'="(7) / (-14) + (-2) / (4)";
18.801 -val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
18.802 -if est1 = ("-1 / 1", "[]") then ()
18.803 -else error "new behaviour in rational.sml: est1'";
18.804 -
18.805 -val t = (term_of o the o (parse thy))
18.806 -"(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
18.807 -val SOME (t',_) = factout_ thy t;
18.808 -if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then ()
18.809 -else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
18.810 -
18.811 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
18.812 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
18.813 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
18.814 @@ -1124,46 +576,75 @@
18.815 if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)"
18.816 then () else error "level 5, rewrite_set_ norm_Rational: changed"
18.817
18.818 -"-------- reverse rewrite -------------------------------";
18.819 -"-------- reverse rewrite -------------------------------";
18.820 -"-------- reverse rewrite -------------------------------";
18.821 -(*WN.28.8.02: tests for the 'reverse-rewrite' functions:
18.822 - these are defined in Rationals.ML and stored in
18.823 - the 'reverse-ruleset' cancel*)
18.824 +"-------- reverse rewrite ----------------------------------------------------";
18.825 +"-------- reverse rewrite ----------------------------------------------------";
18.826 +"-------- reverse rewrite ----------------------------------------------------";
18.827 +(** the term for which reverse rewriting is demonstrated **)
18.828 +val t = str2term "(9 + -1 * x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
18.829 +val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc,
18.830 + next_rule = nex, normal_form = nor, ...},...} = cancel_p;
18.831
18.832 -(*the term for which reverse rewriting is demonstrated*)
18.833 - val t = (term_of o the o (parse thy))
18.834 - "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
18.835 - val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
18.836 - next_rule=nex,normal_form=nor,...},...} = cancel;
18.837 -
18.838 -(*normal_form produces the result in ONE step*)
18.839 +(** normal_form produces the result in ONE step **)
18.840 val SOME (t',_) = nor t;
18.841 -if term2str t' = "(3 - x) / (3 + x)" then ()
18.842 +if term2str t' = "(3 + -1 * x) / (3 + x)" then ()
18.843 else error "rational.sml normal_form (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
18.844
18.845 -(*initialize the interpreter state used by the 'me'*)
18.846 - val (t,_,revsets,_) = ini t;
18.847 +(** initialize the interpreter state used by the 'me' **)
18.848 + val (t, _, revsets, _) = ini t;
18.849
18.850 -(*find the rule 'r' to apply to term 't'*)
18.851 +if length (hd revsets) = 11 then () else error "length of revset changed";
18.852 +if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
18.853 + (@{thm realpow_twoI} |> string_of_thm |> thmID_of_derivation_name)
18.854 +then () else error "first element of revset changed";
18.855 +if
18.856 +(revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",??.unknown)" andalso
18.857 +(revsets |> nth 1 |> nth 2 |> rule2str) =
18.858 + "Thm (\"sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))\",??.unknown)" andalso
18.859 +(revsets |> nth 1 |> nth 3 |> rule2str) =
18.860 + "Thm (\"sym_#mult_Float ((2,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso
18.861 +(revsets |> nth 1 |> nth 4 |> rule2str) =
18.862 + "Thm (\"sym_#mult_Float ((~1,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso
18.863 +(revsets |> nth 1 |> nth 5 |> rule2str) =
18.864 + "Thm (\"sym_#mult_Float ((3,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso
18.865 +(revsets |> nth 1 |> nth 6 |> rule2str) = "Rls_ (\"sym_order_mult_rls_\")" andalso
18.866 +(revsets |> nth 1 |> nth 7 |> rule2str) =
18.867 + "Thm (\"sym_mult_assoc\",Groups.semigroup_mult_class.mult_assoc)"
18.868 +then () else error "first 7 elements in revset changed"
18.869 +
18.870 +(** find the rule 'r' to apply to term 't' **)
18.871 +(*/------- since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
18.872 + for Isabelle2013, we don't get a working revset, but non-termination:
18.873 +
18.874 val SOME (r as (Thm (str, thm))) = nex revsets t;
18.875 + :
18.876 +((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
18.877 + Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))","
18.878 +((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),
18.879 + Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))","
18.880 +((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),
18.881 + Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))","
18.882 +((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), []))","
18.883 + :
18.884 +### Isabelle2002:
18.885 + Thm ("sym_#mult_2_3", "6 = 2 * 3")
18.886 +### Isabelle2009-2 for cancel_ (not cancel_p_):
18.887 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
18.888 andalso string_of_thm thm =
18.889 (string_of_thm o make_thm o (cterm_of (@{theory "Isac"})))
18.890 (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
18.891 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
18.892 -(* before Isa02->09-2 was not checked automatically, ?was different?:
18.893 -val SOME r = nex revsets t;
18.894 -val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
18.895 +\---------------------------------------------------------------------------------------/*)
18.896
18.897 -(* check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
18.898 +(** check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
18.899 if the rule is OK, the term resulting from applying the rule is returned,too;
18.900 there might be several rule applications inbetween,
18.901 - which are listed after the head in reverse order *)
18.902 + which are listed after the head in reverse order **)
18.903 +(*/-------------------------------------------- Isabelle2013: this gives "error id_of_thm";
18.904 + we don't repair this, because interaction within "reverse rewriting" never worked properly:
18.905 +
18.906 val (r, (t, asm))::_ = loc revsets t r;
18.907 if term2str t = "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" andalso asm = []
18.908 -then ()
18.909 -else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
18.910 +then () else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
18.911
18.912 (* find the next rule to apply *)
18.913 val SOME (r as (Thm (str, thm))) = nex revsets t;
18.914 @@ -1198,11 +679,13 @@
18.915 val ss = term2str t;
18.916 if ss = "(3 - x) / (3 + x)" andalso terms2str asm = "[\"3 + x ~= 0\"]" then ()
18.917 else error "rational.sml: new behav. in rev-set cancel";
18.918 +\--------------------------------------------------------------------------------------/*)
18.919
18.920 -"-------- 'reverse-ruleset' cancel_p --------------------";
18.921 -"-------- 'reverse-ruleset' cancel_p --------------------";
18.922 -"-------- 'reverse-ruleset' cancel_p --------------------";
18.923 -(*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
18.924 +"-------- 'reverse-ruleset' cancel_p -----------------------------------------";
18.925 +"-------- 'reverse-ruleset' cancel_p -----------------------------------------";
18.926 +"-------- 'reverse-ruleset' cancel_p -----------------------------------------";
18.927 +(*Isabelle2013: the example below shows, why "reverse rewriting" only worked for
18.928 + special cases.*)
18.929
18.930 (*the term for which reverse rewriting is demonstrated*)
18.931 val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
18.932 @@ -1237,16 +720,12 @@
18.933 val SOME r = nex revsets t;
18.934 val (r,(t,asm))::_ = loc revsets t r;
18.935 term2str t;
18.936 -*)
18.937 +*)
18.938
18.939 -writeln "****************** all tests successfull *************************";
18.940 -
18.941 -
18.942 -
18.943 -(*WN.17.3.03 =========================================================vvv---*)
18.944 -"-------- norm_Rational ---------------------------------";
18.945 -"-------- norm_Rational ---------------------------------";
18.946 -"-------- norm_Rational ---------------------------------";
18.947 +(*========== inhibit exn WN130824 TODO =======================================================
18.948 +"-------- examples: rls norm_Rational ----------------------------------------";
18.949 +"-------- examples: rls norm_Rational ----------------------------------------";
18.950 +"-------- examples: rls norm_Rational ----------------------------------------";
18.951 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
18.952 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
18.953 if term2str t' = "1 / 18 = 0" then () else error "rational.sml 1";
18.954 @@ -2415,7 +1894,7 @@
18.955 SK060904-2a non-termination of add_fraction_p_";
18.956 val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
18.957 " (-1 * a + b * x) / (a + b * x) ");
18.958 -(* nonterm.SK
18.959 +(* nonterm.SK = WN130830
18.960 val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
18.961 "--- 11 ---";
18.962 common_nominator_p_ thy t;
18.963 @@ -2432,11 +1911,11 @@
18.964 " errors in cancel_p: --- 4,5,6,7.";
18.965 " error in common_nominator_p, common_nominator_p_: --- 10; 1,2?.";
18.966 " errors caused by ruleset norm_Rational: --- 8,9.";
18.967 -trace_rewrite := true;
18.968 +trace_rewrite := false;
18.969
18.970 -"--- 1 ---: non-terminating with ### add_fract: done t22 ";
18.971 +"--- 1 ---: non-terminating with ### add_fract: done t22 "; = WN130830
18.972 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)";
18.973 -trace_rewrite:= true;
18.974 +trace_rewrite := false;
18.975 rewrite_set_ thy false common_nominator_p t;
18.976
18.977 "--- 2 ---: non-terminating with ### add_fract: done t22 ";
19.1 --- a/test/Tools/isac/Knowledge/rlang.sml Mon Sep 02 15:17:34 2013 +0200
19.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Mon Sep 02 16:16:08 2013 +0200
19.3 @@ -1457,7 +1457,7 @@
19.4
19.5
19.6 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)";
19.7 -trace_rewrite:=true;
19.8 +trace_rewrite := false;
19.9 val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
19.10 term2str t';
19.11 trace_rewrite:=false;
20.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Mon Sep 02 15:17:34 2013 +0200
20.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Mon Sep 02 16:16:08 2013 +0200
20.3 @@ -5,7 +5,7 @@
20.4
20.5 Compiler.Control.Print.printDepth:=10; (*4 default*)
20.6 Compiler.Control.Print.printDepth:=5; (*4 default*)
20.7 - trace_rewrite:=true;
20.8 +trace_rewrite := false;
20.9 *)
20.10 "----------- rooteq.sml begin--------";
20.11 "--------------(1/sqrt(x)=5)---------------------------------------";
21.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml Mon Sep 02 15:17:34 2013 +0200
21.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml Mon Sep 02 16:16:08 2013 +0200
21.3 @@ -31,8 +31,7 @@
21.4 ([3, 2], Res)] then () else
21.5 error "modspec.sml: diff.behav. get_interval after replace} other 2 a";
21.6
21.7 -print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt);
21.8 -print_depth 3;
21.9 +print_depth 99;map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt); print_depth 3;
21.10 if map fst (get_interval ([3, 2, 1], Res) ([],Res) 9999 pt) =
21.11 [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res)] then () else
21.12 error "modspec.sml: diff.behav. get_interval after replace} other 2 b";
22.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 15:17:34 2013 +0200
22.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Mon Sep 02 16:16:08 2013 +0200
22.3 @@ -521,7 +521,7 @@
22.4 *)
22.5 trace_rewrite := false;
22.6
22.7 -trace_rewrite := true;
22.8 +trace_rewrite := false;
22.9 val SOME (t', []) = rewrite_set_ thy true RatEq_eliminate t; (*= [] must be = "x ~= 0"*)
22.10 term2str t' = "1 = 5 * x";
22.11 (*
23.1 --- a/test/Tools/isac/ProgLang/termC.sml Mon Sep 02 15:17:34 2013 +0200
23.2 +++ b/test/Tools/isac/ProgLang/termC.sml Mon Sep 02 16:16:08 2013 +0200
23.3 @@ -222,7 +222,7 @@
23.4 val pat = (free2var o term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
23.5 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
23.6 val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
23.7 -print_depth 999; insts;
23.8 +print_depth 3; (*999*) insts;
23.9 (*val insts =
23.10 ({},
23.11 {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))),
24.1 --- a/test/Tools/isac/Test_Isac.thy Mon Sep 02 15:17:34 2013 +0200
24.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Sep 02 16:16:08 2013 +0200
24.3 @@ -2,19 +2,19 @@
24.4 Author: Walther Neuper 101001
24.5 (c) copyright due to lincense terms.
24.6
24.7 - isac tests
24.8 - in ~~/test/Tools/isac are structured according
24.9 - to ~~/src/Tools/isac
24.10 - Additional tests are in
24.11 + Isac's tests are organised parallel to sources:
24.12 + "~~/test/Tools/isac" has same directory structure as "~~/src/Tools/isac"
24.13 + plus
24.14 ~~/test/Tools/isac/ADDTESTS
24.15 - ~~/test/Tools/isac/Minisubpbl
24.16 + ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
24.17
24.18 $ cd /usr/local/isabisac/
24.19 $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
24.20 *)
24.21
24.22 -(*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION:
24.23 - Tracing paused. Stop, or continue with next 100, 1000, 10000 messages?*)
24.24 +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
24.25 +(* !!!!! wait a minute until Isac and the theories below are loaded !!!!! *)
24.26 +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
24.27
24.28 theory Test_Isac imports Isac
24.29 "ADDTESTS/Ctxt"
24.30 @@ -24,7 +24,7 @@
24.31 "ADDTESTS/course/phst11/T2_Rewriting"
24.32 "ADDTESTS/course/phst11/T3_MathEngine"
24.33 "ADDTESTS/file-depend/BuildC_Test"
24.34 - "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
24.35 +(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"*)
24.36 "~~/test/Pure/Isar/Test_Parsers"
24.37 (*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" lost at update 2009-2-->2011*)
24.38 "~~/test/Pure/Isar/Test_Parse_Term"
24.39 @@ -33,12 +33,6 @@
24.40 "~~/src/Tools/isac/Knowledge/GCD_Poly" (*not imported by Isac.thy*)
24.41 "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
24.42
24.43 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
24.44 -(* !!!!! wait a minute until Isac and the above theories are loaded !!!!! *)
24.45 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
24.46 -(* !!!!! with this changeset evaluation doen't start < 7min; UG is busy ! *)
24.47 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
24.48 -
24.49 begin
24.50 section {* test ML Code of isac *}
24.51 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
24.52 @@ -123,7 +117,7 @@
24.53 ML_file "Knowledge/rootrat.sml"
24.54 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
24.55 ML_file "Knowledge/partial_fractions.sml"
24.56 -(*ML_file "Knowledge/polyeq.sml" -----------------works if cut into parts !!!!!!!!!!!*)
24.57 + ML_file "Knowledge/polyeq.sml" (*-----------------works if cut into parts !!!!!!!!!!!*)
24.58 (*ML_file "Knowledge/rlang.sml" much to clean up, not urgent due to similar tests *)
24.59 ML_file "Knowledge/calculus.sml"
24.60 ML_file "Knowledge/trig.sml"
25.1 --- a/test/Tools/isac/Test_Some.thy Mon Sep 02 15:17:34 2013 +0200
25.2 +++ b/test/Tools/isac/Test_Some.thy Mon Sep 02 16:16:08 2013 +0200
25.3 @@ -1,45 +1,73 @@
25.4 -
25.5 theory Test_Some imports Isac
25.6 -begin ML_file "Knowledge/gcd_poly_ml.sml"
25.7 -(*
25.8 -declare [[show_types]]
25.9 -declare [[show_sorts]]
25.10 -find_theorems "?a <= ?a"
25.11 +begin
25.12 +ML_file "Knowledge/rational.sml"
25.13
25.14 -print_facts
25.15 -print_statement ""
25.16 -print_theory
25.17 -*)
25.18 +section {* code for copy & paste ===============================================================*}
25.19 ML {*
25.20 -*}
25.21 -ML {* (*==================*)
25.22 -*}
25.23 -ML {*
25.24 -*}
25.25 -ML {*
25.26 -*}
25.27 -ML {* (*==================*)
25.28 -*}
25.29 -ML {*
25.30 -*}
25.31 -ML {*
25.32 -*}
25.33 -ML {* (*==================*)
25.34 "~~~~~ fun , args:"; val () = ();
25.35 +"~~~~~ and , args:"; val () = ();
25.36
25.37 "~~~~~ to return val:"; val () = ();
25.38
25.39 *}
25.40 +text {*
25.41 + declare [[show_types]]
25.42 + declare [[show_sorts]]
25.43 + find_theorems "?a <= ?a"
25.44 +
25.45 + print_facts
25.46 + print_statement ""
25.47 + print_theory
25.48 +*}
25.49 +ML {*
25.50 +(*========== inhibit exn WN130822 only runs with Rational2.thy =================================
25.51 +============ inhibit exn WN130822 only runs with Rational2.thy ================================*)
25.52 +
25.53 +(*========== inhibit exn WN130826 TODO =========================================================
25.54 +============ inhibit exn WN130826 TODO ========================================================*)
25.55 +
25.56 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
25.57 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
25.58 +
25.59 +(*=========================^^^ correct until here ^^^==========================================*)
25.60 +*}
25.61 +
25.62 +
25.63 +section {* ====================================================================================*}
25.64 +ML {*
25.65 +*} ML {*
25.66 +*} ML {*
25.67 +*} ML {*
25.68 +*} ML {*
25.69 +*}
25.70 +
25.71 +section {* GREAT CONFUSION -> final hg ci =====================================================*}
25.72 +ML {*
25.73 +(*in isabisac12/test/../rational.sml*)
25.74 +"-------- investigate rls common_nominator_p from OLD gcd --------------------";
25.75 +(*ATTENTION:
25.76 +val common_nominator_p =
25.77 + Rrls {id = "common_nominator_p", ...
25.78 + scr = Rfuns {init_state = init_state thy Atools_erls ro,
25.79 + normal_form = add_fraction_p_ thy, <<<===================================
25.80 +:
25.81 +val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
25.82 +(*but ^^^ not exported, just ^^^*)
25.83 +
25.84 +i.e. GREAT CONFUSION:
25.85 +# normal_form of add_fractions_p is add_fraction_p_,
25.86 +# and id of add_fractions_p is common_nominator_p
25.87 +*)
25.88 +
25.89 +section {* ===================================================================================*}
25.90 +ML {*
25.91 +*} ML {*
25.92 +*} ML {*
25.93 +*}
25.94 +
25.95 +section {* ===================================================================================*}
25.96 +ML {*
25.97 +*} ML {*
25.98 +*} ML {*
25.99 +*}
25.100 end
25.101 -
25.102 -(*========== inhibit exn WN1130701 broken already in 2009-2 =======================
25.103 -============ inhibit exn WN1130701 broken already in 2009-2 =====================*)
25.104 -(*========== inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some===
25.105 -============ inhibit exn WN1130722 Isabelle2012-->13 thehier? works in Test_Some=*)
25.106 -
25.107 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
25.108 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
25.109 -
25.110 -(*=========================^^^ correct until here ^^^===========================*)
25.111 -
25.112 -
26.1 --- a/test/Tools/isac/calcelems.sml Mon Sep 02 15:17:34 2013 +0200
26.2 +++ b/test/Tools/isac/calcelems.sml Mon Sep 02 16:16:08 2013 +0200
26.3 @@ -72,7 +72,7 @@
26.4 pretty types:
26.5 PolyML.addPrettyPrinter
26.6 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
26.7 - print_depth 99;
26.8 + print_depth 3;
26.9 *)
26.10 "===== extend parse to string with markup===";
26.11 (*
27.1 --- a/test/Tools/isac/xmlsrc/datatypes.sml Mon Sep 02 15:17:34 2013 +0200
27.2 +++ b/test/Tools/isac/xmlsrc/datatypes.sml Mon Sep 02 16:16:08 2013 +0200
27.3 @@ -32,7 +32,7 @@
27.4 "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
27.5 (*get_py (Thy_Info.get_theory "Pure") theID theID (! thehier);
27.6 (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
27.7 -print_depth 999;
27.8 +print_depth 3; (*999*)
27.9 (!thehier);
27.10
27.11 (*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info.get_theory "Pure"), theID, theID, (! thehier));*)