1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sat Jul 03 16:21:07 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jul 12 17:21:37 2021 +0200
1.3 @@ -123,14 +123,18 @@
1.4 ML \<open>
1.5 fun monom_of_term vs (c, es) (t as Const _) =
1.6 (c, list_update es (find_index (curry op = t) vs) 1)
1.7 - | monom_of_term vs (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
1.8 - (t |> HOLogic.dest_number |> snd |> string_of_int
1.9 - |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
1.10 + | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
1.11 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
1.12 + | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
1.13 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
1.14 | monom_of_term vs (c, es) (t as Free _) =
1.15 (c, list_update es (find_index (curry op = t) vs) 1)
1.16 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $
1.17 - (Const ("Num.numeral_class.numeral", _) $ num)) =
1.18 - (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
1.19 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
1.20 + (e as Const ("Num.numeral_class.numeral", _) $ _)) =
1.21 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
1.22 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
1.23 + (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
1.24 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
1.25 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
1.26 let val (c', es') = monom_of_term vs (c, es) m1
1.27 in monom_of_term vs (c', es') m2 end
1.28 @@ -139,6 +143,10 @@
1.29 (*-------v------*)
1.30 fun monoms_of_term vs (t as Const _) =
1.31 [monom_of_term vs (1, replicate (length vs) 0) t]
1.32 + | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
1.33 + [monom_of_term vs (1, replicate (length vs) 0) t]
1.34 + | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
1.35 + [monom_of_term vs (1, replicate (length vs) 0) t]
1.36 | monoms_of_term vs (t as Free _) =
1.37 [monom_of_term vs (1, replicate (length vs) 0) t]
1.38 | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
2.1 --- a/test/Tools/isac/Test_Some.thy Sat Jul 03 16:21:07 2021 +0200
2.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jul 12 17:21:37 2021 +0200
2.3 @@ -93,9 +93,6 @@
2.4 declare [[ML_exception_trace]]
2.5 \<close>
2.6
2.7 -ML_file \<open>MathEngBasic/rewrite.sml\<close>
2.8 -ML_file \<open>Knowledge/poly.sml\<close>
2.9 -
2.10 section \<open>===================================================================================\<close>
2.11 ML \<open>
2.12 \<close> ML \<open>
2.13 @@ -103,356 +100,6 @@
2.14 \<close> ML \<open>
2.15 \<close>
2.16
2.17 -section \<open>2============== NEW src/../"Knowledge/Rational.thy" PART --> Poly.thy ==============\<close>
2.18 -section \<open>Cancellation and addition of fractions\<close>
2.19 -subsection \<open>Conversion term <--> poly\<close>
2.20 -subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
2.21 -ML \<open>
2.22 -fun monom_of_term vs (c, es) (t as Const _) =
2.23 - (c, list_update es (find_index (curry op = t) vs) 1)
2.24 - | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
2.25 - (t |> HOLogic.dest_number |> snd |> string_of_int
2.26 - |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
2.27 - | monom_of_term vs (c, es) (t as Free _) =
2.28 - (c, list_update es (find_index (curry op = t) vs) 1)
2.29 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (t as Free _) $
2.30 - (Const ("Num.numeral_class.numeral", _) $ num)) =
2.31 - (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
2.32 - | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
2.33 - let val (c', es') = monom_of_term vs (c, es) m1
2.34 - in monom_of_term vs (c', es') m2 end
2.35 - | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
2.36 -
2.37 -(*-------v------*)
2.38 -fun monoms_of_term vs (t as Const _) =
2.39 - [monom_of_term vs (1, replicate (length vs) 0) t]
2.40 - | monoms_of_term vs (t as Free _) =
2.41 - [monom_of_term vs (1, replicate (length vs) 0) t]
2.42 - | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
2.43 - [monom_of_term vs (1, replicate (length vs) 0) t]
2.44 - | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
2.45 - [monom_of_term vs (1, replicate (length vs) 0) t]
2.46 - | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
2.47 - (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
2.48 - | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
2.49 -
2.50 -(* convert a term to the internal representation of a multivariate polynomial;
2.51 - the conversion is quite liberal, see test --- fun poly_of_term ---:
2.52 -* the order of variables and the parentheses within a monomial are arbitrary
2.53 -* the coefficient may be somewhere
2.54 -* he order and the parentheses within monomials are arbitrary
2.55 -But the term must be completely expand + over * (laws of distributivity are not applicable).
2.56 -
2.57 -The function requires the free variables as strings already given,
2.58 -because the gcd involves 2 polynomials (with the same length for their list of exponents).
2.59 -*)
2.60 -fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =
2.61 - (SOME (t |> monoms_of_term vs |> order)
2.62 - handle ERROR _ => NONE)
2.63 - | poly_of_term vs t =
2.64 - (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
2.65 - handle ERROR _ => NONE)
2.66 -
2.67 -fun is_poly t =
2.68 - let
2.69 - val vs = TermC.vars_of t
2.70 - in
2.71 - case poly_of_term vs t of SOME _ => true | NONE => false
2.72 - end
2.73 -val is_expanded = is_poly (* TODO: check names *)
2.74 -val is_polynomial = is_poly (* TODO: check names *)
2.75 -\<close>
2.76 -
2.77 -subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
2.78 -ML \<open>
2.79 -fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
2.80 - | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
2.81 - | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
2.82 - | term_of_es baseT expT (v :: vs) (e :: es) =
2.83 - Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
2.84 - :: term_of_es baseT expT vs es
2.85 - | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
2.86 -
2.87 -fun term_of_monom baseT expT vs ((c, es): monom) =
2.88 - let val es' = term_of_es baseT expT vs es
2.89 - in
2.90 - if c = 1
2.91 - then
2.92 - if es' = [] (*if es = [0,0,0,...]*)
2.93 - then HOLogic.mk_number baseT c
2.94 - else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
2.95 - else foldl (HOLogic.mk_binop "Groups.times_class.times")
2.96 - (HOLogic.mk_number baseT c, es')
2.97 - end
2.98 -
2.99 -fun term_of_poly baseT expT vs p =
2.100 - let val monos = map (term_of_monom baseT expT vs) p
2.101 - in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end
2.102 -\<close>
2.103 -
2.104 -subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
2.105 -ML \<open>
2.106 -fun mk_noteq_0 baseT t =
2.107 - Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
2.108 - (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
2.109 -
2.110 -fun mk_asms baseT ts =
2.111 - let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
2.112 - in map (mk_noteq_0 baseT) as' end
2.113 -\<close>
2.114 -
2.115 -subsubsection \<open>Factor out gcd for cancellation\<close>
2.116 -ML \<open>
2.117 -fun check_fraction t =
2.118 - case t of
2.119 - Const ("Rings.divide_class.divide", _) $ numerator $ denominator
2.120 - => SOME (numerator, denominator)
2.121 - | _ => NONE
2.122 -
2.123 -(* prepare a term for cancellation by factoring out the gcd
2.124 - assumes: is a fraction with outmost "/"*)
2.125 -fun factout_p_ (thy: theory) t =
2.126 - let val opt = check_fraction t
2.127 - in
2.128 - case opt of
2.129 - NONE => NONE
2.130 - | SOME (numerator, denominator) =>
2.131 - let
2.132 - val vs = TermC.vars_of t
2.133 - val baseT = type_of numerator
2.134 - val expT = HOLogic.realT
2.135 - in
2.136 - case (poly_of_term vs numerator, poly_of_term vs denominator) of
2.137 - (SOME a, SOME b) =>
2.138 - let
2.139 - val ((a', b'), c) = gcd_poly a b
2.140 - val es = replicate (length vs) 0
2.141 - in
2.142 - if c = [(1, es)] orelse c = [(~1, es)]
2.143 - then NONE
2.144 - else
2.145 - let
2.146 - val b't = term_of_poly baseT expT vs b'
2.147 - val ct = term_of_poly baseT expT vs c
2.148 - val t' =
2.149 - HOLogic.mk_binop "Rings.divide_class.divide"
2.150 - (HOLogic.mk_binop "Groups.times_class.times"
2.151 - (term_of_poly baseT expT vs a', ct),
2.152 - HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
2.153 - in SOME (t', mk_asms baseT [b't, ct]) end
2.154 - end
2.155 - | _ => NONE : (term * term list) option
2.156 - end
2.157 - end
2.158 -\<close>
2.159 -
2.160 -subsubsection \<open>Cancel a fraction\<close>
2.161 -ML \<open>
2.162 -(* cancel a term by the gcd ("" denote terms with internal algebraic structure)
2.163 - cancel_p_ :: theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
2.164 - cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
2.165 - assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
2.166 - yields
2.167 - SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
2.168 - a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
2.169 - \<or> NONE *)
2.170 -fun cancel_p_ (_: theory) t =
2.171 - let val opt = check_fraction t
2.172 - in
2.173 - case opt of
2.174 - NONE => NONE
2.175 - | SOME (numerator, denominator) =>
2.176 - let
2.177 - val vs = TermC.vars_of t
2.178 - val baseT = type_of numerator
2.179 - val expT = HOLogic.realT
2.180 - in
2.181 - case (poly_of_term vs numerator, poly_of_term vs denominator) of
2.182 - (SOME a, SOME b) =>
2.183 - let
2.184 - val ((a', b'), c) = gcd_poly a b
2.185 - val es = replicate (length vs) 0
2.186 - in
2.187 - if c = [(1, es)] orelse c = [(~1, es)]
2.188 - then NONE
2.189 - else
2.190 - let
2.191 - val bt' = term_of_poly baseT expT vs b'
2.192 - val ct = term_of_poly baseT expT vs c
2.193 - val t' =
2.194 - HOLogic.mk_binop "Rings.divide_class.divide"
2.195 - (term_of_poly baseT expT vs a', bt')
2.196 - val asm = mk_asms baseT [bt']
2.197 - in SOME (t', asm) end
2.198 - end
2.199 - | _ => NONE : (term * term list) option
2.200 - end
2.201 - end
2.202 -\<close>
2.203 -
2.204 -subsubsection \<open>Factor out to a common denominator for addition\<close>
2.205 -ML \<open>
2.206 -(* addition of fractions allows (at most) one non-fraction (a monomial) *)
2.207 -fun check_frac_sum
2.208 - (Const ("Groups.plus_class.plus", _) $
2.209 - (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
2.210 - (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
2.211 - = SOME ((n1, d1), (n2, d2))
2.212 - | check_frac_sum
2.213 - (Const ("Groups.plus_class.plus", _) $
2.214 - nofrac $
2.215 - (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
2.216 - = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
2.217 - | check_frac_sum
2.218 - (Const ("Groups.plus_class.plus", _) $
2.219 - (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
2.220 - nofrac)
2.221 - = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
2.222 - | check_frac_sum _ = NONE
2.223 -
2.224 -(* prepare a term for addition by providing the least common denominator as a product
2.225 - assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
2.226 -fun common_nominator_p_ (_: theory) t =
2.227 - let val opt = check_frac_sum t
2.228 - in
2.229 - case opt of
2.230 - NONE => NONE
2.231 - | SOME ((n1, d1), (n2, d2)) =>
2.232 - let
2.233 - val vs = TermC.vars_of t
2.234 - in
2.235 - case (poly_of_term vs d1, poly_of_term vs d2) of
2.236 - (SOME a, SOME b) =>
2.237 - let
2.238 - val ((a', b'), c) = gcd_poly a b
2.239 - val (baseT, expT) = (type_of n1, HOLogic.realT)
2.240 - val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
2.241 - (*----- minimum of parentheses & nice result, but breaks tests: -------------
2.242 - val denom = HOLogic.mk_binop "Groups.times_class.times"
2.243 - (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)
2.244 - val denom =
2.245 - if c = [(1, replicate (length vs) 0)]
2.246 - then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')
2.247 - else
2.248 - HOLogic.mk_binop "Groups.times_class.times" (c',
2.249 - HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)
2.250 - val t' =
2.251 - HOLogic.mk_binop "Groups.plus_class.plus"
2.252 - (HOLogic.mk_binop "Rings.divide_class.divide"
2.253 - (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),
2.254 - HOLogic.mk_binop "Rings.divide_class.divide"
2.255 - (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))
2.256 - val asm = mk_asms baseT [d1', d2', c']
2.257 - in SOME (t', asm) end
2.258 - | _ => NONE : (term * term list) option
2.259 - end
2.260 - end
2.261 -\<close>
2.262 -
2.263 -subsubsection \<open>Addition of at least one fraction within a sum\<close>
2.264 -ML \<open>
2.265 -(* add fractions
2.266 - assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
2.267 - NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
2.268 -fun add_fraction_p_ (_: theory) t =
2.269 - case check_frac_sum t of
2.270 - NONE => NONE
2.271 - | SOME ((n1, d1), (n2, d2)) =>
2.272 - let
2.273 - val vs = TermC.vars_of t
2.274 - in
2.275 - case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
2.276 - (SOME _, SOME a, SOME _, SOME b) =>
2.277 - let
2.278 - val ((a', b'), c) = gcd_poly a b
2.279 - val (baseT, expT) = (type_of n1, HOLogic.realT)
2.280 - val nomin = term_of_poly baseT expT vs
2.281 - (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
2.282 - val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
2.283 - val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)
2.284 - in SOME (t', mk_asms baseT [denom]) end
2.285 - | _ => NONE : (term * term list) option
2.286 - end
2.287 -\<close>
2.288 -
2.289 -section \<open>Embed cancellation and addition into rewriting\<close>
2.290 -ML \<open>val thy = @{theory}\<close>
2.291 -subsection \<open>Rulesets and predicate for embedding\<close>
2.292 -ML \<open>
2.293 -(* evaluates conditions in calculate_Rational *)
2.294 -val calc_rat_erls =
2.295 - prep_rls'
2.296 - (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
2.297 - erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
2.298 - rules =
2.299 - [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
2.300 - Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
2.301 - Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
2.302 - Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
2.303 - scr = Rule.Empty_Prog});
2.304 -
2.305 -(* simplifies expressions with numerals;
2.306 - does NOT rearrange the term by AC-rewriting; thus terms with variables
2.307 - need to have constants to be commuted together respectively *)
2.308 -val calculate_Rational =
2.309 - prep_rls' (Rule_Set.merge "calculate_Rational"
2.310 - (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
2.311 - erls = calc_rat_erls, srls = Rule_Set.Empty,
2.312 - calc = [], errpatts = [],
2.313 - rules =
2.314 - [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
2.315 -
2.316 - Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
2.317 - (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
2.318 - Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),
2.319 - (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
2.320 - \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
2.321 - Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),
2.322 - (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
2.323 - Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),
2.324 - (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
2.325 - Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),
2.326 - (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
2.327 - .... is_const to be omitted here FIXME*)
2.328 -
2.329 - Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
2.330 - (*a / b * (c / d) = a * c / (b * d)*)
2.331 - Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),
2.332 - (*?x * (?y / ?z) = ?x * ?y / ?z*)
2.333 - Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),
2.334 - (*?y / ?z * ?x = ?y * ?x / ?z*)
2.335 -
2.336 - Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),
2.337 - (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
2.338 - Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
2.339 - (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
2.340 -
2.341 - Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
2.342 - (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
2.343 -
2.344 - Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
2.345 - (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
2.346 - Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),
2.347 - (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
2.348 - Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
2.349 - (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
2.350 - scr = Rule.Empty_Prog})
2.351 - calculate_Poly);
2.352 -
2.353 -(*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
2.354 -fun eval_is_expanded (thmid:string) _
2.355 - (t as (Const("Rational.is_expanded", _) $ arg)) thy =
2.356 - if is_expanded arg
2.357 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
2.358 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
2.359 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
2.360 - HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
2.361 - | eval_is_expanded _ _ _ _ = NONE;
2.362 -\<close> ML \<open>
2.363 -\<close> ML \<open>
2.364 -\<close>
2.365 -
2.366 -
2.367 section \<open>3============== NEW src/../ "Knowledge/Poly.thy" ================================\<close>
2.368 subsection \<open>auxiliary functions\<close>
2.369 ML \<open>
2.370 @@ -554,15 +201,14 @@
2.371 (monom2list t1) @ (monom2list t2)
2.372 | monom2list t = [t];
2.373
2.374 +\<close> ML \<open> (* \<longrightarrow> libraryC.sml *)
2.375 +(* accomodate string-representation for int to term-orders in Poly.thy and Rational.thy*)
2.376 +fun string_of_int' i =
2.377 + if i >= 0 then i |> string_of_int
2.378 + else (i * ~1) |> string_of_int |> curry op ^ "-"
2.379 \<close> ML \<open>
2.380 (* use this fun ONLY locally: makes negative numbers with "-" instead of "~" for poly-orders*)
2.381 -fun dest_number' t =
2.382 - let
2.383 - val i = TermC.num_of_term t
2.384 - in
2.385 - if i >= 0 then HOLogic.dest_number t |> snd |> string_of_int
2.386 - else (i * ~1) |> string_of_int |> curry op ^ "-"
2.387 - end
2.388 +fun dest_number' t = t |> TermC.num_of_term |> string_of_int'
2.389 \<close> ML \<open>
2.390 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
2.391 \<close> ML \<open> (* orig.code *)
2.392 @@ -1067,15 +713,411 @@
2.393 \<close>
2.394
2.395
2.396 -section \<open>===================================================================================\<close>
2.397 +section \<open>2============== NEW src/../"Knowledge/Rational.thy" ================= ==============\<close>
2.398 +section \<open>Cancellation and addition of fractions\<close>
2.399 +subsection \<open>Conversion term <--> poly\<close>
2.400 +subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
2.401 ML \<open>
2.402 +val mon1 = (1, [1,2,3]): monom;
2.403 +val mon2 = (~4, [5,6,7]): monom;
2.404 +val poly = [mon1, mon2]: poly
2.405 \<close> ML \<open>
2.406 +fun monom_uminus ((c, ps): monom) = (~1 * c, ps): monom;
2.407 +fun poly_uminus (ms: poly) = map monom_uminus ms: poly;
2.408 +\<close> ML \<open>
2.409 +poly_uminus poly = [(~1, [1, 2, 3]), (4, [5, 6, 7])]
2.410 +\<close> ML \<open>
2.411 +fun monom_of_term vs (c, es) (t as Const _) =
2.412 + (c, list_update es (find_index (curry op = t) vs) 1)
2.413 + | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
2.414 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
2.415 + | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
2.416 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
2.417 + | monom_of_term vs (c, es) (t as Free _) =
2.418 + (c, list_update es (find_index (curry op = t) vs) 1)
2.419 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
2.420 + (e as Const ("Num.numeral_class.numeral", _) $ _)) =
2.421 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
2.422 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
2.423 + (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
2.424 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
2.425 + | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
2.426 + let val (c', es') = monom_of_term vs (c, es) m1
2.427 + in monom_of_term vs (c', es') m2 end
2.428 + | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
2.429 +
2.430 +fun monom_of_term vs (c, es) (t as Const _) =
2.431 + (c, list_update es (find_index (curry op = t) vs) 1)
2.432 + | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
2.433 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
2.434 + | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
2.435 + (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
2.436 + | monom_of_term vs (c, es) (t as Free _) =
2.437 + (c, list_update es (find_index (curry op = t) vs) 1)
2.438 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
2.439 + (e as Const ("Num.numeral_class.numeral", _) $ _)) =
2.440 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
2.441 + | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
2.442 + (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
2.443 + (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
2.444 + | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
2.445 + let val (c', es') = monom_of_term vs (c, es) m1
2.446 + in monom_of_term vs (c', es') m2 end
2.447 + | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
2.448 +
2.449 +(*-------v------*)
2.450 +fun monoms_of_term vs (t as Const _) =
2.451 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.452 + | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
2.453 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.454 + | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
2.455 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.456 + | monoms_of_term vs (t as Free _) =
2.457 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.458 + | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
2.459 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.460 + | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
2.461 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.462 + | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
2.463 + (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
2.464 + | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
2.465 +
2.466 +fun monoms_of_term vs (t as Const _) =
2.467 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.468 + | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
2.469 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.470 + | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
2.471 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.472 + | monoms_of_term vs (t as Free _) =
2.473 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.474 + | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
2.475 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.476 + | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
2.477 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.478 + | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
2.479 + (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
2.480 + | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
2.481 +
2.482 +(* convert a term to the internal representation of a multivariate polynomial;
2.483 + the conversion is quite liberal, see test --- fun poly_of_term ---:
2.484 +* the order of variables and the parentheses within a monomial are arbitrary
2.485 +* the coefficient may be somewhere
2.486 +* he order and the parentheses within monomials are arbitrary
2.487 +But the term must be completely expand + over * (laws of distributivity are not applicable).
2.488 +
2.489 +The function requires the free variables as strings already given,
2.490 +because the gcd involves 2 polynomials (with the same length for their list of exponents).
2.491 +*)
2.492 +fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =
2.493 + (SOME (t |> monoms_of_term vs |> order)
2.494 + handle ERROR _ => NONE)
2.495 +(*| poly_of_term vs (t as Const ("Groups.minus_class.minus", _) $ _ $ _) =
2.496 + (SOME (t |> monoms_of_term vs |> order)
2.497 + handle ERROR _ => NONE)
2.498 +------------------------------------------------------ this is handled ahead by rewriting *)
2.499 + | poly_of_term vs t =
2.500 + (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
2.501 + handle ERROR _ => NONE)
2.502 +
2.503 +fun is_poly t =
2.504 + let
2.505 + val vs = TermC.vars_of t
2.506 + in
2.507 + case poly_of_term vs t of SOME _ => true | NONE => false
2.508 + end
2.509 +val is_expanded = is_poly (* TODO: check names *)
2.510 +val is_polynomial = is_poly (* TODO: check names *)
2.511 +\<close>
2.512 +
2.513 +subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
2.514 +ML \<open>
2.515 +fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
2.516 + | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
2.517 + | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
2.518 + | term_of_es baseT expT (v :: vs) (e :: es) =
2.519 + Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
2.520 + :: term_of_es baseT expT vs es
2.521 + | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
2.522 +
2.523 +fun term_of_monom baseT expT vs ((c, es): monom) =
2.524 + let val es' = term_of_es baseT expT vs es
2.525 + in
2.526 + if c = 1
2.527 + then
2.528 + if es' = [] (*if es = [0,0,0,...]*)
2.529 + then HOLogic.mk_number baseT c
2.530 + else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
2.531 + else foldl (HOLogic.mk_binop "Groups.times_class.times")
2.532 + (HOLogic.mk_number baseT c, es')
2.533 + end
2.534 +
2.535 +fun term_of_poly baseT expT vs p =
2.536 + let val monos = map (term_of_monom baseT expT vs) p
2.537 + in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end
2.538 +\<close>
2.539 +
2.540 +subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
2.541 +ML \<open>
2.542 +fun mk_noteq_0 baseT t =
2.543 + Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
2.544 + (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
2.545 +
2.546 +fun mk_asms baseT ts =
2.547 + let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
2.548 + in map (mk_noteq_0 baseT) as' end
2.549 +\<close>
2.550 +
2.551 +subsubsection \<open>Factor out gcd for cancellation\<close>
2.552 +ML \<open>
2.553 +fun check_fraction t =
2.554 + case t of
2.555 + Const ("Rings.divide_class.divide", _) $ numerator $ denominator
2.556 + => SOME (numerator, denominator)
2.557 + | _ => NONE
2.558 +
2.559 +(* prepare a term for cancellation by factoring out the gcd
2.560 + assumes: is a fraction with outmost "/"*)
2.561 +fun factout_p_ (thy: theory) t =
2.562 + let val opt = check_fraction t
2.563 + in
2.564 + case opt of
2.565 + NONE => NONE
2.566 + | SOME (numerator, denominator) =>
2.567 + let
2.568 + val vs = TermC.vars_of t
2.569 + val baseT = type_of numerator
2.570 + val expT = HOLogic.realT
2.571 + in
2.572 + case (poly_of_term vs numerator, poly_of_term vs denominator) of
2.573 + (SOME a, SOME b) =>
2.574 + let
2.575 + val ((a', b'), c) = gcd_poly a b
2.576 + val es = replicate (length vs) 0
2.577 + in
2.578 + if c = [(1, es)] orelse c = [(~1, es)]
2.579 + then NONE
2.580 + else
2.581 + let
2.582 + val b't = term_of_poly baseT expT vs b'
2.583 + val ct = term_of_poly baseT expT vs c
2.584 + val t' =
2.585 + HOLogic.mk_binop "Rings.divide_class.divide"
2.586 + (HOLogic.mk_binop "Groups.times_class.times"
2.587 + (term_of_poly baseT expT vs a', ct),
2.588 + HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
2.589 + in SOME (t', mk_asms baseT [b't, ct]) end
2.590 + end
2.591 + | _ => NONE : (term * term list) option
2.592 + end
2.593 + end
2.594 +\<close>
2.595 +
2.596 +subsubsection \<open>Cancel a fraction\<close>
2.597 +ML \<open>
2.598 +(* cancel a term by the gcd ("" denote terms with internal algebraic structure)
2.599 + cancel_p_ :: theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
2.600 + cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
2.601 + assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
2.602 + yields
2.603 + SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
2.604 + a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
2.605 + \<or> NONE *)
2.606 +fun cancel_p_ (_: theory) t =
2.607 + let val opt = check_fraction t
2.608 + in
2.609 + case opt of
2.610 + NONE => NONE
2.611 + | SOME (numerator, denominator) =>
2.612 + let
2.613 + val vs = TermC.vars_of t
2.614 + val baseT = type_of numerator
2.615 + val expT = HOLogic.realT
2.616 + in
2.617 + case (poly_of_term vs numerator, poly_of_term vs denominator) of
2.618 + (SOME a, SOME b) =>
2.619 + let
2.620 + val ((a', b'), c) = gcd_poly a b
2.621 + val es = replicate (length vs) 0
2.622 + in
2.623 + if c = [(1, es)] orelse c = [(~1, es)]
2.624 + then NONE
2.625 + else
2.626 + let
2.627 + val bt' = term_of_poly baseT expT vs b'
2.628 + val ct = term_of_poly baseT expT vs c
2.629 + val t' =
2.630 + HOLogic.mk_binop "Rings.divide_class.divide"
2.631 + (term_of_poly baseT expT vs a', bt')
2.632 + val asm = mk_asms baseT [bt']
2.633 + in SOME (t', asm) end
2.634 + end
2.635 + | _ => NONE : (term * term list) option
2.636 + end
2.637 + end
2.638 +\<close>
2.639 +
2.640 +subsubsection \<open>Factor out to a common denominator for addition\<close>
2.641 +ML \<open>
2.642 +(* addition of fractions allows (at most) one non-fraction (a monomial) *)
2.643 +fun check_frac_sum
2.644 + (Const ("Groups.plus_class.plus", _) $
2.645 + (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
2.646 + (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
2.647 + = SOME ((n1, d1), (n2, d2))
2.648 + | check_frac_sum
2.649 + (Const ("Groups.plus_class.plus", _) $
2.650 + nofrac $
2.651 + (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
2.652 + = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
2.653 + | check_frac_sum
2.654 + (Const ("Groups.plus_class.plus", _) $
2.655 + (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
2.656 + nofrac)
2.657 + = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
2.658 + | check_frac_sum _ = NONE
2.659 +
2.660 +(* prepare a term for addition by providing the least common denominator as a product
2.661 + assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
2.662 +fun common_nominator_p_ (_: theory) t =
2.663 + let val opt = check_frac_sum t
2.664 + in
2.665 + case opt of
2.666 + NONE => NONE
2.667 + | SOME ((n1, d1), (n2, d2)) =>
2.668 + let
2.669 + val vs = TermC.vars_of t
2.670 + in
2.671 + case (poly_of_term vs d1, poly_of_term vs d2) of
2.672 + (SOME a, SOME b) =>
2.673 + let
2.674 + val ((a', b'), c) = gcd_poly a b
2.675 + val (baseT, expT) = (type_of n1, HOLogic.realT)
2.676 + val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
2.677 + (*----- minimum of parentheses & nice result, but breaks tests: -------------
2.678 + val denom = HOLogic.mk_binop "Groups.times_class.times"
2.679 + (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)
2.680 + val denom =
2.681 + if c = [(1, replicate (length vs) 0)]
2.682 + then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')
2.683 + else
2.684 + HOLogic.mk_binop "Groups.times_class.times" (c',
2.685 + HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)
2.686 + val t' =
2.687 + HOLogic.mk_binop "Groups.plus_class.plus"
2.688 + (HOLogic.mk_binop "Rings.divide_class.divide"
2.689 + (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),
2.690 + HOLogic.mk_binop "Rings.divide_class.divide"
2.691 + (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))
2.692 + val asm = mk_asms baseT [d1', d2', c']
2.693 + in SOME (t', asm) end
2.694 + | _ => NONE : (term * term list) option
2.695 + end
2.696 + end
2.697 +\<close>
2.698 +
2.699 +subsubsection \<open>Addition of at least one fraction within a sum\<close>
2.700 +ML \<open>
2.701 +(* add fractions
2.702 + assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
2.703 + NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
2.704 +fun add_fraction_p_ (_: theory) t =
2.705 + case check_frac_sum t of
2.706 + NONE => NONE
2.707 + | SOME ((n1, d1), (n2, d2)) =>
2.708 + let
2.709 + val vs = TermC.vars_of t
2.710 + in
2.711 + case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
2.712 + (SOME _, SOME a, SOME _, SOME b) =>
2.713 + let
2.714 + val ((a', b'), c) = gcd_poly a b
2.715 + val (baseT, expT) = (type_of n1, HOLogic.realT)
2.716 + val nomin = term_of_poly baseT expT vs
2.717 + (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
2.718 + val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
2.719 + val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)
2.720 + in SOME (t', mk_asms baseT [denom]) end
2.721 + | _ => NONE : (term * term list) option
2.722 + end
2.723 +\<close>
2.724 +
2.725 +section \<open>Embed cancellation and addition into rewriting\<close>
2.726 +ML \<open>val thy = @{theory}\<close>
2.727 +subsection \<open>Rulesets and predicate for embedding\<close>
2.728 +ML \<open>
2.729 +(* evaluates conditions in calculate_Rational *)
2.730 +val calc_rat_erls =
2.731 + prep_rls'
2.732 + (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
2.733 + erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
2.734 + rules =
2.735 + [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
2.736 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
2.737 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
2.738 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
2.739 + scr = Rule.Empty_Prog});
2.740 +
2.741 +(* simplifies expressions with numerals;
2.742 + does NOT rearrange the term by AC-rewriting; thus terms with variables
2.743 + need to have constants to be commuted together respectively *)
2.744 +val calculate_Rational =
2.745 + prep_rls' (Rule_Set.merge "calculate_Rational"
2.746 + (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
2.747 + erls = calc_rat_erls, srls = Rule_Set.Empty,
2.748 + calc = [], errpatts = [],
2.749 + rules =
2.750 + [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
2.751 +
2.752 + Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
2.753 + (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
2.754 + Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),
2.755 + (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
2.756 + \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
2.757 + Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),
2.758 + (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
2.759 + Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),
2.760 + (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
2.761 + Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),
2.762 + (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
2.763 + .... is_const to be omitted here FIXME*)
2.764 +
2.765 + Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
2.766 + (*a / b * (c / d) = a * c / (b * d)*)
2.767 + Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),
2.768 + (*?x * (?y / ?z) = ?x * ?y / ?z*)
2.769 + Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),
2.770 + (*?y / ?z * ?x = ?y * ?x / ?z*)
2.771 +
2.772 + Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),
2.773 + (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
2.774 + Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
2.775 + (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
2.776 +
2.777 + Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
2.778 + (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
2.779 +
2.780 + Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
2.781 + (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
2.782 + Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),
2.783 + (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
2.784 + Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
2.785 + (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
2.786 + scr = Rule.Empty_Prog})
2.787 + calculate_Poly);
2.788 +
2.789 +(*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
2.790 +fun eval_is_expanded (thmid:string) _
2.791 + (t as (Const("Rational.is_expanded", _) $ arg)) thy =
2.792 + if is_expanded arg
2.793 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
2.794 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
2.795 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
2.796 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
2.797 + | eval_is_expanded _ _ _ _ = NONE;
2.798 \<close> ML \<open>
2.799 \<close> ML \<open>
2.800 \<close>
2.801
2.802 -
2.803 -section \<open>===================================================================================\<close>
2.804 section \<open>===================================================================================\<close>
2.805 ML \<open>
2.806 \<close> ML \<open>
2.807 @@ -1139,8 +1181,26 @@
2.808 "-------- fun poly_of_term ---------------------------------------------------";
2.809 "-------- fun poly_of_term ---------------------------------------------------";
2.810 val thy = @{theory Partial_Fractions};
2.811 -val ctxt = Proof_Context.init_global @{theory}
2.812 -val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"));
2.813 +val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
2.814 +
2.815 +val t = TermC.str2term "-3 + -2 * x ::real";
2.816 +if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
2.817 +then () else error "poly_of_term uminus changed";
2.818 +
2.819 +\<close> ML \<open> (*//---------------- adhoc inserted ------------------------------------------------\\*)
2.820 +\<close> ML \<open>
2.821 +val t = TermC.str2term "x/2 - -(3*x - 2)/9";
2.822 +\<close> ML \<open>
2.823 +val NONE = poly_of_term vs t; (*COMPARE norm_Rational: exception TERM dest_number - 3 + 13 * x
2.824 + BUT: this raises no exn ! ! !*)
2.825 +\<close> ML \<open>
2.826 +Rewrite.trace_on := false;
2.827 +Rewrite.trace_on := true;
2.828 +\<close> text \<open> (*exception TERM raised dest_number - 2 + 3 * x*)
2.829 +val SOME (t', _) = rewrite_set_ thy false norm_Rational t;
2.830 +\<close> ML \<open>
2.831 +@{thm real_mult_minus1}
2.832 +\<close> ML \<open> (*\\---------------- adhoc inserted ------------------------------------------------//*)
2.833
2.834 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
2.835 then () else error "poly_of_term 1 changed";
2.836 @@ -1189,7 +1249,6 @@
2.837 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
2.838 then () else error "poly_of_term 8 changed";
2.839
2.840 -\<close> ML \<open> (*//---------------- inserted for --- fun monoms_of_term --- -----------------------\\*)
2.841 (*from --- rls norm_Rational downto fun gcd_poly ---*)
2.842 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
2.843 ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
2.844 @@ -1210,55 +1269,7 @@
2.845 val baseT = type_of numerator
2.846 val expT = HOLogic.realT;
2.847 \<close> ML \<open>
2.848 -val (NONE, NONE) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
2.849 -\<close> ML \<open> (*------------------ inserted for --- fun poly_of_term --- ---------------------------*)
2.850 -\<close> ML \<open>
2.851 -val vs = [@{term "x::real"}, @{term "y::real"}]
2.852 -\<close> ML \<open>
2.853 -val p1 = TermC.str2term "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)";
2.854 -val p2 = TermC.str2term "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2";
2.855 -\<close> ML \<open>
2.856 - poly_of_term vs p1;
2.857 -"~~~~~ fun poly_of_term , args:"; val (vs, (t as Const ("Groups.plus_class.plus", _) $ _ $ _)) =
2.858 - (vs, p1);
2.859 -\<close> ML \<open>
2.860 -(*+*)UnparseC.term p1 = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)";
2.861 -\<close> ML \<open>
2.862 - t |> monoms_of_term vs; (*ERROR poly malformed 2 with - 12*)
2.863 -\<close> ML \<open>
2.864 -"~~~~~ fun monoms_of_term , args:"; val (vs, (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2)) =
2.865 - (vs, t);
2.866 -\<close> ML \<open>
2.867 -(*+*)UnparseC.term ms1 = "- 12 + 4 * y + 3 * x \<up> 2";
2.868 -\<close> ML \<open>
2.869 - (monoms_of_term vs ms1) (*ERROR poly malformed 2 with - 12*)
2.870 -\<close> ML \<open>
2.871 -"~~~~~ fun monoms_of_term , args:"; val (vs, (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2)) =
2.872 - (vs, ms1);
2.873 -\<close> ML \<open>
2.874 -(*+*)UnparseC.term ms1 = "- 12 + 4 * y";
2.875 -\<close> ML \<open>
2.876 - (monoms_of_term vs ms1) (*ERROR poly malformed 2 with - 12*)
2.877 -\<close> ML \<open>
2.878 -"~~~~~ fun monoms_of_term , args:"; val (vs, (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2)) =
2.879 - (vs, ms1);
2.880 -\<close> ML \<open>
2.881 -(*+*)UnparseC.term ms1 = "- 12";
2.882 -\<close> ML \<open>
2.883 - (monoms_of_term vs ms1) (*ERROR poly malformed 2 with - 12*)
2.884 -\<close> ML \<open>
2.885 -"~~~~~ fun monoms_of_term , args:"; val (vs, (t as Const _)) =
2.886 - (vs, ms1);
2.887 -\<close> ML \<open>
2.888 -ms1
2.889 -\<close> ML \<open>
2.890 -UnparseC.term ms1 = "- 12"
2.891 -\<close> ML \<open>
2.892 -\<close> ML \<open>
2.893 -\<close> ML \<open>
2.894 -\<close> ML \<open>
2.895 -\<close> ML \<open>
2.896 -\<close> ML \<open> (*\\---------------- inserted for --- fun monoms_of_term --- -----------------------//*)
2.897 +val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
2.898
2.899 \<close> ML \<open>
2.900 "-------- fun is_poly --------------------------------------------------------";
2.901 @@ -1282,16 +1293,16 @@
2.902 if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"
2.903 then () else error "term_of_poly 1 changed";
2.904
2.905 -\<close> text \<open> (* factout_p_ \<longrightarrow> NONE *)
2.906 +\<close> ML \<open>
2.907 "-------- integration lev.1 fun factout_p_ -----------------------------------";
2.908 "-------- integration lev.1 fun factout_p_ -----------------------------------";
2.909 "-------- integration lev.1 fun factout_p_ -----------------------------------";
2.910 val t = TermC.str2term "(x \<up> 2 + -1*y \<up> 2) / (x \<up> 2 + -1*x*y)"
2.911 val SOME (t', asm) = factout_p_ thy t;
2.912 -if UnparseC.term t' = "(x + y) * (x + -1 * y) / (x * (x + -1 * y))"
2.913 +if UnparseC.term t' = "(x + y) * (x + - 1 * y) / (x * (x + - 1 * y))"
2.914 then () else error ("factout_p_ term 1 changed: " ^ UnparseC.term t')
2.915 ;
2.916 -if UnparseC.terms asm = "[\"x \<noteq> 0\",\"x + -1 * y \<noteq> 0\"]"
2.917 +if UnparseC.terms asm = "[\"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]"
2.918 then () else error "factout_p_ asm 1 changed"
2.919 ;
2.920 val t = TermC.str2term "nothing + to_cancel ::real";
2.921 @@ -1304,8 +1315,6 @@
2.922 then () else error "factout_p_ 1 changed";
2.923
2.924 \<close> ML \<open>
2.925 -cancel_p_
2.926 -\<close> text \<open> (*cancel_p_ \<longrightarrow> NONE*)
2.927 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
2.928 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
2.929 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
2.930 @@ -1340,18 +1349,14 @@
2.931 if UnparseC.terms asm = "[\"a + b + c \<noteq> 0\", \"y \<noteq> 0\", \"x \<noteq> 0\"]"
2.932 then () else error "common_nominator_p_ asm 1 changed"
2.933
2.934 -\<close> text \<open> (*common_nominator_p_ \<longrightarrow> NONE*)
2.935 "-------- example in mail Nipkow";
2.936 val t = TermC.str2term "x/(x \<up> 2 + -1*y \<up> 2) + y/(x \<up> 2 + -1*x*y)";
2.937 val SOME (t', asm) = common_nominator_p_ thy t;
2.938 -if UnparseC.term t' = "x * x / " ^
2.939 - "((x + -1 * y) * ((x + y) * x))" ^
2.940 - " +\n" ^
2.941 - "y * (x + y) / " ^
2.942 - "((x + -1 * y) * ((x + y) * x))"
2.943 +if UnparseC.term t' =
2.944 + "x * x / ((x + - 1 * y) * ((x + y) * x)) +\ny * (x + y) / ((x + - 1 * y) * ((x + y) * x))"
2.945 then () else error "common_nominator_p_ term 2 changed"
2.946 ;
2.947 -if UnparseC.terms asm = "[\"x + y \<noteq> 0\",\"x \<noteq> 0\",\"x + -1 * y \<noteq> 0\"]"
2.948 +if UnparseC.terms asm = "[\"x + y \<noteq> 0\", \"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]"
2.949 then () else error "common_nominator_p_ asm 2 changed"
2.950
2.951 "-------- example: applicable tested by SML code";
2.952 @@ -1361,20 +1366,20 @@
2.953 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
2.954 val SOME (t', asm) = common_nominator_p_ thy t;
2.955 if UnparseC.term t' =
2.956 - "(x + -1) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (-1 + x))"
2.957 - andalso UnparseC.terms asm = "[\"1 + x \<noteq> 0\",\"-1 + x \<noteq> 0\"]"
2.958 + "(x + - 1) * (- 1 + x) / ((1 + x) * (- 1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (- 1 + x))"
2.959 + andalso UnparseC.terms asm = "[\"1 + x \<noteq> 0\", \"- 1 + x \<noteq> 0\"]"
2.960 then () else error "common_nominator_p_ 3 changed";
2.961
2.962 -\<close> text \<open> (*add_fraction_p_ \<longrightarrow> NONE*)
2.963 +\<close> ML \<open>
2.964 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
2.965 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
2.966 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
2.967 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
2.968 val SOME (t', asm) = add_fraction_p_ thy t;
2.969 -if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (-1 + x \<up> 2)"
2.970 +if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)"
2.971 then () else error "add_fraction_p_ 3 changed";
2.972 ;
2.973 -if UnparseC.terms asm = "[\"-1 + x \<up> 2 \<noteq> 0\"]"
2.974 +if UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"
2.975 then () else error "add_fraction_p_ 3 changed";
2.976 ;
2.977 val t = TermC.str2term "nothing / to_add";
2.978 @@ -1382,8 +1387,8 @@
2.979 ;
2.980 val t = TermC.str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
2.981 val SOME (t', asm) = add_fraction_p_ thy t;
2.982 -if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (-1 + x \<up> 2)" andalso
2.983 - UnparseC.terms asm = "[\"-1 + x \<up> 2 \<noteq> 0\"]"
2.984 +if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" andalso
2.985 + UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]"
2.986 then () else error "add_fraction_p_ 3 changed";
2.987
2.988 \<close> ML \<open>
2.989 @@ -1549,10 +1554,7 @@
2.990 val baseT = type_of numerator
2.991 val expT = HOLogic.realT;
2.992 (*default_print_depth 3; 999*)
2.993 -\<close> ML \<open>
2.994 -val (NONE, NONE) = (poly_of_term vs numerator, poly_of_term vs denominator)
2.995 -\<close> ML \<open>
2.996 -\<close> text \<open> (*poly_of_term --> NONE*)
2.997 +\<close> ML \<open> (*poly_of_term --> NONE*)
2.998 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
2.999 (*default_print_depth 3; 999*)
2.1000 (* does not terminate instead of returning ?:
2.1001 @@ -1616,7 +1618,7 @@
2.1002 UnparseC.term n1; UnparseC.term d1; UnparseC.term n2; UnparseC.term d2;
2.1003 val vs = TermC.vars_of t;
2.1004 (*default_print_depth 3; 999*)
2.1005 -\<close> text \<open> (*poly_of_term \<longrightarrow> (SOME, NONE, NONE, SOME*)
2.1006 +\<close> ML \<open>
2.1007 val (SOME _, SOME a, SOME _, SOME b) =
2.1008 (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2);
2.1009 (*default_print_depth 3; 999*)
2.1010 @@ -1803,7 +1805,7 @@
2.1011 then () else error "rational.sml cancel Schalk 187c";
2.1012 *)
2.1013
2.1014 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1015 +\<close> ML \<open>
2.1016 "-------- example 188a";
2.1017 val t = TermC.str2term "(-8 + 8 * x) / (-9 + 9 * x)";
2.1018 is_expanded (TermC.str2term "8 * x + -8");
2.1019 @@ -1816,24 +1818,24 @@
2.1020 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]")
2.1021 then () else error "rational.sml cancel Schalk make_polynomial 1";
2.1022
2.1023 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1024 +\<close> ML \<open>
2.1025 "-------- example 188b";
2.1026 val t = TermC.str2term "(-15 + 5 * x) / (-18 + 6 * x)";
2.1027 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1028 if (UnparseC.term t', UnparseC.terms asm) = ("5 / 6", "[]")
2.1029 then () else error "rational.sml cancel Schalk 188b";
2.1030
2.1031 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1032 "-------- example 188c";
2.1033 val t = TermC.str2term "(a + -1 * b) / (b + -1 * a)";
2.1034 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1035 -if (UnparseC.term t', UnparseC.terms asm) = ("-1 / 1", "[]")
2.1036 +if (UnparseC.term t', UnparseC.terms asm) = ("- 1 / 1", "[]")
2.1037 then () else error "rational.sml cancel Schalk 188c";
2.1038
2.1039 +\<close> ML \<open>
2.1040 is_expanded (TermC.str2term "a + -1 * b") = true;
2.1041 -val t = TermC.str2term "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
2.1042 +val t = TermC.str2term "((- 1)*(b + (-1) * a))/(1*(b + (- 1) * a))";
2.1043 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
2.1044 -if (UnparseC.term t', UnparseC.terms asm) = ("(a + -1 * b) / (-1 * a + b)", "[]")
2.1045 +if (UnparseC.term t', UnparseC.terms asm) = ("(a + - 1 * b) / (- 1 * a + b)", "[]")
2.1046 then () else error "rational.sml cancel Schalk make_polynomial 2";
2.1047
2.1048 \<close> ML \<open>
2.1049 @@ -1851,20 +1853,18 @@
2.1050 ("(1 + 3 * a + 9 * a \<up> 2 + 27 * a \<up> 3) /\n(3 * a + 18 * a \<up> 2 + 27 * a \<up> 3)", "[]")
2.1051 then () else error "rational.sml make_polynomial Schalk 190c";
2.1052
2.1053 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1054 "-------- example 191a";
2.1055 val t = TermC.str2term "( x \<up> 2 + -1 * y \<up> 2 ) / ( x + y )";
2.1056 - is_expanded (TermC.str2term "x \<up> 2 + -1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
2.1057 + is_expanded (TermC.str2term "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
2.1058 is_expanded (TermC.str2term "x + y") = true;
2.1059 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1060 -if (UnparseC.term t', UnparseC.terms asm) = ("(x + -1 * y) / 1", "[]")
2.1061 +if (UnparseC.term t', UnparseC.terms asm) = ("(x + - 1 * y) / 1", "[]")
2.1062 then () else error "rational.sml make_polynomial Schalk 191a";
2.1063
2.1064 -\<close> text \<open> (*rewrite_set_ make_polynomial \<longrightarrow> NONE*)
2.1065 "-------- example 191b";
2.1066 -val t = TermC.str2term "((x + (-1) * y)*(x + y))/((1)*(x + y))";
2.1067 +val t = TermC.str2term "((x + (- 1) * y)*(x + y))/((1)*(x + y))";
2.1068 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
2.1069 -if (UnparseC.term t', UnparseC.terms asm) = ("(x \<up> 2 + -1 * y \<up> 2) / (x + y)", "[]")
2.1070 +if (UnparseC.term t', UnparseC.terms asm) = ("(x \<up> 2 + - 1 * y \<up> 2) / (x + y)", "[]")
2.1071 then () else error "rational.sml make_polynomial Schalk 191b";
2.1072
2.1073 \<close> ML \<open>
2.1074 @@ -1879,54 +1879,46 @@
2.1075 if (UnparseC.term t', UnparseC.terms asm) = ("(25 + - 30 * x + 9 * x \<up> 2) / (- 25 + 9 * x \<up> 2)", "[]")
2.1076 then () else error "rational.sml make_polynomial Schalk 191c";
2.1077
2.1078 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1079 "-------- example 192b";
2.1080 -val t = TermC.str2term "( 7 * x \<up> 3 + -1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + -1 * y \<up> 3 )";
2.1081 +val t = TermC.str2term "( 7 * x \<up> 3 + - 1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + - 1 * y \<up> 3 )";
2.1082 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1083 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]")
2.1084 then () else error "rational.sml cancel_p Schalk 192b";
2.1085
2.1086 -\<close> text \<open> (*rewrite_set_ make_polynomial \<longrightarrow> NONE*)
2.1087 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
2.1088 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
2.1089 if (UnparseC.term t', UnparseC.terms asm) =
2.1090 - ("(7 * x \<up> 3 + -1 * x \<up> 2 * y) / (7 * x * y \<up> 2 + -1 * y \<up> 3)", "[]")
2.1091 + ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
2.1092 then () else error "rational.sml make_polynomial Schalk 192b";
2.1093
2.1094 -\<close> text \<open> (*rewrite_set_ make_polynomial \<longrightarrow> NONE*)
2.1095 val t = TermC.str2term "((x \<up> 2)*(7 * x + (-1) * y))/((y \<up> 2)*(7 * x + (-1) * y))";
2.1096 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
2.1097 if (UnparseC.term t', UnparseC.terms asm) =
2.1098 - ("(7 * x \<up> 3 + -1 * x \<up> 2 * y) / (7 * x * y \<up> 2 + -1 * y \<up> 3)", "[]")
2.1099 + ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]")
2.1100 then () else error "rational.sml make_polynomial Schalk WN050929 not working";
2.1101
2.1102 -\<close> ML \<open>
2.1103 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1104 val t = TermC.str2term "( x \<up> 2 + -6 * x + 9 ) / ( x \<up> 2 + -9 )";
2.1105 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1106 -if (UnparseC.term t', UnparseC.terms asm) = ("(-3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]")
2.1107 +if (UnparseC.term t', UnparseC.terms asm) = ("(- 3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]")
2.1108 then () else error "rational.sml cancel_p Schalk 193a";
2.1109
2.1110 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1111 "-------- example 193b";
2.1112 val t = TermC.str2term "( x \<up> 2 + -8 * x + 16 ) / ( 2 * x \<up> 2 + -32 )";
2.1113 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1114 -if (UnparseC.term t', UnparseC.terms asm) = ("(-4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]")
2.1115 +if (UnparseC.term t', UnparseC.terms asm) = ("(- 4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]")
2.1116 then () else error "rational.sml cancel_p Schalk 193b";
2.1117
2.1118 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1119 "-------- example 193c";
2.1120 val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + -10 * x + 1 )";
2.1121 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1122 if (UnparseC.term t', UnparseC.terms asm) =
2.1123 - ("(2 * x + 10 * x \<up> 2) / (1 + -5 * x)", "[\"1 + -5 * x \<noteq> 0\"]")
2.1124 + ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]")
2.1125 then () else error "rational.sml cancel_p Schalk 193c";
2.1126
2.1127 -\<close> text \<open> (*rewrite_set_ cancel_p \<longrightarrow> NONE*)
2.1128 -(*WN:*)
2.1129 +(*WN: improved with new numerals*)
2.1130 val t = TermC.str2term "(-25 + 9*x \<up> 2)/(5 + 3*x)";
2.1131 -val SOME (t, asm) = rewrite_set_ thy false cancel_p t;
2.1132 -if (UnparseC.term t', UnparseC.terms asm) = ("(2 * x + 10 * x \<up> 2) / (1 + -5 * x)", "[]")
2.1133 +val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
2.1134 +if (UnparseC.term t', UnparseC.terms asm) = ("(- 5 + 3 * x) / 1", "[]")
2.1135 then () else error "rational.sml cancel WN 1";
2.1136
2.1137 \<close> ML \<open>
2.1138 @@ -2017,18 +2009,20 @@
2.1139 val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc,
2.1140 next_rule = nex, normal_form = nor, ...},...} = cancel_p;
2.1141
2.1142 -\<close> text \<open> (*Rfuns normal_form \<longrightarrow> NONE*)
2.1143 +\<close> ML \<open>
2.1144 (** normal_form produces the result in ONE step **)
2.1145 val SOME (t', _) = nor t;
2.1146 -if UnparseC.term t' = "(3 + -1 * x) / (3 + x)" then ()
2.1147 +\<close> ML \<open>
2.1148 +if UnparseC.term t' = "(3 + - 1 * x) / (3 + x)" then ()
2.1149 else error "rational.sml normal_form (9 - x \<up> 2) / (9 - 6 * x + x \<up> 2)";
2.1150
2.1151 (** initialize the interpreter state used by the 'me' **)
2.1152 val (t, _, revsets, _) = ini t;
2.1153
2.1154 if length (hd revsets) = 11 then () else error "length of revset changed";
2.1155 +\<close> text \<open> (*Rfuns revsets \<longrightarrow> broken*)
2.1156 if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
2.1157 - (@ {thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
2.1158 + (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
2.1159 then () else error "first element of revset changed";
2.1160 if
2.1161 (revsets |> nth 1 |> nth 1 |> Rule.to_string) = "Thm (\"realpow_twoI\",?r1 \<up> 2 = ?r1 * ?r1)" andalso
2.1162 @@ -2127,14 +2121,16 @@
2.1163 next_rule=nex,normal_form=nor,...},...} = cancel_p;
2.1164
2.1165 (*normal_form produces the result in ONE step*)
2.1166 -\<close> text \<open> (*Rfuns normal_form \<longrightarrow> NONE*)
2.1167 -val SOME (t',_) = nor t;
2.1168 -UnparseC.term t' = "(3 + 1 * x) / (3 + -1 * x)";
2.1169 -
2.1170 +val SOME (t', _) = nor t;
2.1171 +if UnparseC.term t' = "(3 + x) / (3 + - 1 * x)"
2.1172 +then () else error "cancel_p normal_form CHANGED";;
2.1173 +
2.1174 +\<close> ML \<open>
2.1175 (*initialize the interpreter state used by the 'me'*)
2.1176 val SOME (t', asm) = cancel_p_ thy t;
2.1177 -UnparseC.term t' = "(3 + x) / (3 + -1 * x)" (*true*);
2.1178 -UnparseC.terms asm = "[\"3 + -1 * x ~= 0\"]" (*true*);
2.1179 +if (UnparseC.term t', UnparseC.terms asm) = ("(3 + x) / (3 + - 1 * x)", "[\"3 + - 1 * x \<noteq> 0\"]")
2.1180 +then () else error "cancel_p CHANGED";;
2.1181 +
2.1182 val (t,_,revsets,_) = ini t;
2.1183
2.1184 (* WN.10.10.02: dieser Fall terminiert nicht
2.1185 @@ -2145,43 +2141,34 @@
2.1186 as was with make_polynomial before ?!?*)
2.1187
2.1188 val SOME r = nex revsets t;
2.1189 +(*
2.1190 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",
2.1191 mk_thm thy "9 = 3 \<up> 2"));
2.1192 -(*WN060831 *** id_of_thm
2.1193 - Exception- ERROR raised ...
2.1194 -val (r,(t,asm))::_ = loc revsets t r;
2.1195 -UnparseC.term t;
2.1196 -
2.1197 - val SOME r = nex revsets t;
2.1198 - val (r,(t,asm))::_ = loc revsets t r;
2.1199 - UnparseC.term t;
2.1200 *)
2.1201
2.1202 \<close> ML \<open>
2.1203 +\<close> ML \<open>
2.1204 +@{thm real_mult_minus1}
2.1205 +\<close> ML \<open>
2.1206 "-------- examples: rls norm_Rational ----------------------------------------";
2.1207 "-------- examples: rls norm_Rational ----------------------------------------";
2.1208 "-------- examples: rls norm_Rational ----------------------------------------";
2.1209 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
2.1210 -val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1211 -\<close> ML \<open>
2.1212 -UnparseC.term t'
2.1213 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1214 +\<close> text \<open> (*norm_Rational: exception TERM dest_number - 2 + 3 * x*)
2.1215 +val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1216 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
2.1217
2.1218 \<close> ML \<open>
2.1219 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
2.1220 +\<close> text \<open> (*norm_Rational: exception TERM dest_number - 3 + 13 * x*)
2.1221 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1222 -\<close> ML \<open>
2.1223 -UnparseC.term t'
2.1224 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1225 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
2.1226 else error "rational.sml 2";
2.1227
2.1228 \<close> ML \<open>
2.1229 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
2.1230 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1231 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1232 -if UnparseC.term t' = "23 + 35 * x + -72 * x \<up> 2" then ()
2.1233 +if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
2.1234 else error "rational.sml 3";
2.1235
2.1236 \<close> ML \<open>
2.1237 @@ -2207,7 +2194,6 @@
2.1238
2.1239 \<close> ML \<open>
2.1240 val t = TermC.str2term "1 - ((13*x)/2 - 5/2) \<up> 2";
2.1241 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1242 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1243 if UnparseC.term t' = "(- 21 + 130 * x + - 169 * x \<up> 2) / 4" then ()
2.1244 else error "rational.sml 5";
2.1245 @@ -2216,32 +2202,29 @@
2.1246 (*SRAM Schalk I, p.92 Nr. 609a*)
2.1247 val t = TermC.str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
2.1248 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1249 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1250 -if UnparseC.term t' = "(-255 + 112 * x) / 135" then ()
2.1251 +if UnparseC.term t' = "(- 255 + 112 * x) / 135" then ()
2.1252 else error "rational.sml 6";
2.1253
2.1254 \<close> ML \<open>
2.1255 (*SRAM Schalk I, p.92 Nr. 610c*)
2.1256 val t = TermC.str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
2.1257 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1258 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1259 -if UnparseC.term t' = "(3 + x) / -2" then () else error "rational.sml 7";
2.1260 +if UnparseC.term t' = "(3 + x) / - 2" then () else error "rational.sml 7";
2.1261
2.1262 \<close> ML \<open>
2.1263 (*SRAM Schalk I, p.92 Nr. 476a*)
2.1264 val t = TermC.str2term "(x \<up> 2/(1 - x \<up> 2) + 1)/(x/(1 - x) + 1) * (1 + x)";
2.1265 (*. a/b : c/d translated to a/b * d/c .*)
2.1266 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1267 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1268 if UnparseC.term t' = "1" then () else error "rational.sml 8";
2.1269
2.1270 \<close> ML \<open>
2.1271 (*Schalk I, p.92 Nr. 472a*)
2.1272 val t = TermC.str2term "((8*x \<up> 2 - 32*y \<up> 2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
2.1273 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1274 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation*)
2.1275 if UnparseC.term t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
2.1276
2.1277 +\<close> ML \<open>
2.1278 (*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*)
2.1279
2.1280 (*WN130910 add_fractions_p exception Div raised + history:
2.1281 @@ -2262,7 +2245,6 @@
2.1282 "-------- rational numerals --------------------------------------------------";
2.1283 (*SRA Schalk I, p.40 Nr. 164b *)
2.1284 val t = TermC.str2term "(47/6 - 76/9 + 13/4)/(35/12)";
2.1285 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation WITH NUMERALS*)
2.1286 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1287 if UnparseC.term t = "19 / 21" then ()
2.1288 else error "rational.sml: diff.behav. in norm_Rational_mg 1";
2.1289 @@ -2270,7 +2252,6 @@
2.1290 \<close> ML \<open>
2.1291 (*SRA Schalk I, p.40 Nr. 166a *)
2.1292 val t = TermC.str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
2.1293 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation WITH NUMERALS*)
2.1294 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1295 if UnparseC.term t = "45 / 2" then ()
2.1296 else error "rational.sml: diff.behav. in norm_Rational_mg 2";
2.1297 @@ -2282,72 +2263,90 @@
2.1298 (* e190c Stefan K.*)
2.1299 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3*a))";
2.1300 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1301 -\<close> text \<open> (*rewrite_set_ norm_Rational NO cancellation MANY EXAMPLES*)
2.1302 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"
2.1303 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
2.1304
2.1305 +\<close> ML \<open>
2.1306 (* e192b Stefan K.*)
2.1307 val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y)) / (y \<up> 2 * (7*x + (-1)*y))";
2.1308 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1309 if UnparseC.term t = "x \<up> 2 / y \<up> 2"
2.1310 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
2.1311
2.1312 +\<close> ML \<open>
2.1313 (*SRC Schalk I, p.66 Nr. 379c *)
2.1314 val t = TermC.str2term "(a - b)/(b - a)";
2.1315 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1316 -UnparseC.term t;
2.1317 -if UnparseC.term t = "-1"
2.1318 +if UnparseC.term t = "- 1"
2.1319 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
2.1320
2.1321 +\<close> ML \<open>
2.1322 (*SRC Schalk I, p.66 Nr. 380b *)
2.1323 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))";
2.1324 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1325 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)"
2.1326 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
2.1327
2.1328 +\<close> ML \<open>
2.1329 (*Schalk I, p.60 Nr. 215c: was not cancelled with Isabelle2002 *)
2.1330 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
2.1331 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1332 -if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + -2 * x * y + y \<up> 2)"
2.1333 +\<close> ML \<open>
2.1334 +UnparseC.term t = "(a \<up> 2 * x + - 1 * a \<up> 2 * y + 2 * a * b * x + - 2 * a * b * y +\n b \<up> 2 * x +\n - 1 * b \<up> 2 * y) /\n(x \<up> 3 + - 3 * x \<up> 2 * y + 3 * x * y \<up> 2 + y \<up> 3)"
2.1335 +\<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)
2.1336 +if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
2.1337 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
2.1338
2.1339 +\<close> ML \<open>
2.1340 (*SRC Schalk I, p.66 Nr. 381b *)
2.1341 val t = TermC.str2term
2.1342 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
2.1343 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1344 -if UnparseC.term t = "1 / (-5 + 2 * x)"
2.1345 +\<close> ML \<open>
2.1346 +UnparseC.term t = "(25 + - 20 * x + 4 * x \<up> 2) /\n(125 + 150 * x + - 60 * x \<up> 2 + 8 * x \<up> 3)"
2.1347 +\<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)
2.1348 +if UnparseC.term t = "1 / (- 5 + 2 * x)"
2.1349 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
2.1350
2.1351 +\<close> ML \<open>
2.1352 (* e190c Stefan K.*)
2.1353 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3 * a))";
2.1354 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1355 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"
2.1356 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3";
2.1357
2.1358 +\<close> ML \<open>
2.1359 (* e192b Stefan K.*)
2.1360 val t = TermC.str2term "(x \<up> 2 * (7*x + (-1)*y)) / (y \<up> 2 * (7*x + (-1)*y))";
2.1361 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1362 if UnparseC.term t = "x \<up> 2 / y \<up> 2"
2.1363 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4";
2.1364
2.1365 +\<close> ML \<open>
2.1366 (*SRC Schalk I, p.66 Nr. 379c *)
2.1367 val t = TermC.str2term "(a - b) / (b - a)";
2.1368 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1369 -if UnparseC.term t = "-1"
2.1370 +if UnparseC.term t = "- 1"
2.1371 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5";
2.1372
2.1373 +\<close> ML \<open>
2.1374 (*SRC Schalk I, p.66 Nr. 380b *)
2.1375 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))";
2.1376 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1377 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)"
2.1378 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6";
2.1379
2.1380 +\<close> ML \<open>
2.1381 (*Schalk I, p.60 Nr. 215c *)
2.1382 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
2.1383 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1384 -if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + -2 * x * y + y \<up> 2)"
2.1385 +\<close> ML \<open>
2.1386 +UnparseC.term t = "(a \<up> 2 * x + - 1 * a \<up> 2 * y + 2 * a * b * x + - 2 * a * b * y +\n b \<up> 2 * x +\n - 1 * b \<up> 2 * y) /\n(x \<up> 3 + - 3 * x \<up> 2 * y + 3 * x * y \<up> 2 + y \<up> 3)"
2.1387 +\<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)
2.1388 +if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
2.1389 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";
2.1390
2.1391 +\<close> ML \<open>
2.1392 (* extreme example from somewhere *)
2.1393 val t = TermC.str2term
2.1394 ("(a \<up> 4 * x + -1*a \<up> 4 * y + 4*a \<up> 3 * b * x + -4*a \<up> 3 * b * y + " ^
2.1395 @@ -2357,34 +2356,45 @@
2.1396 "2*a * b * x \<up> 3 + -6*a * b * x \<up> 2 * y + 6*a * b * x * y \<up> 2 + -2*a * b * y \<up> 3 + " ^
2.1397 "b \<up> 2 * x \<up> 3 + -3*b \<up> 2 * x \<up> 2 * y + 3*b \<up> 2 * x * y \<up> 2 + -1*b \<up> 2 * y \<up> 3)")
2.1398 val SOME (t, _) = rewrite_set_ thy false cancel_p t;
2.1399 -if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + -2 * x * y + y \<up> 2)"
2.1400 +if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
2.1401 then () else error "with Isabelle2002: NONE -- now SOME changed";
2.1402
2.1403 +\<close> ML \<open>
2.1404 (*Schalk I, p.66 Nr. 381a *)
2.1405 (* ATTENTION: here the rls is very slow. In Isabelle2002 this required 2 min *)
2.1406 val t = TermC.str2term "18*(a + b) \<up> 3 * (a - b) \<up> 2 / (72*(a - b) \<up> 3 * (a + b) \<up> 2)";
2.1407 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1408 -if UnparseC.term t = "(a + b) / (4 * a + -4 * b)"
2.1409 +\<close> ML \<open>
2.1410 +UnparseC.term t = "(a \<up> 3 + - 1 * a \<up> 2 * b + - 1 * a * b \<up> 2 + b \<up> 3) /\n(4 * a \<up> 3 + - 12 * a \<up> 2 * b + 12 * a * b \<up> 2 + 4 * b \<up> 3)"
2.1411 +\<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)
2.1412 +if UnparseC.term t = "(a + b) / (4 * a + - 4 * b)"
2.1413 then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
2.1414
2.1415 +\<close> ML \<open>
2.1416 (*SRC Schalk I, p.66 Nr. 381b *)
2.1417 val t = TermC.str2term "(4*x \<up> 2 - 20*x + 25) / (2*x - 5) \<up> 3";
2.1418 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1419 -if UnparseC.term t = "1 / (-5 + 2 * x)"
2.1420 +\<close> ML \<open>
2.1421 +UnparseC.term t = "(25 + - 20 * x + 4 * x \<up> 2) /\n(125 + 150 * x + - 60 * x \<up> 2 + 8 * x \<up> 3)"
2.1422 +\<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)
2.1423 +if UnparseC.term t = "1 / (- 5 + 2 * x)"
2.1424 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
2.1425
2.1426 +\<close> ML \<open>
2.1427 (*SRC Schalk I, p.66 Nr. 381c *)
2.1428 val t = TermC.str2term "(27*a \<up> 3 + 9*a \<up> 2+3*a+1) / (27*a \<up> 3 + 18*a \<up> 2+3*a)";
2.1429 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1430 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)"
2.1431 then () else error "rational.sml: diff.behav. in norm_Rational_mg 10";
2.1432
2.1433 +\<close> ML \<open>
2.1434 (*SRC Schalk I, p.66 Nr. 383a *)
2.1435 val t = TermC.str2term "(5*a \<up> 2 - 5*a*b) / (a - b) \<up> 2";
2.1436 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1437 -if UnparseC.term t = "-5 * a / (-1 * a + b)"
2.1438 +if UnparseC.term t = "- 5 * a / (- 1 * a + b)"
2.1439 then () else error "rational.sml: diff.behav. in norm_Rational_mg 11";
2.1440
2.1441 +\<close> ML \<open>
2.1442 "----- NOT TERMINATING ?: worked before 0707xx";
2.1443 val t = TermC.str2term "(a \<up> 2 - 1)*(b + 1) / ((b \<up> 2 - 1)*(a+1))";
2.1444 (* WN130911 "exception Div raised" by
2.1445 @@ -2403,18 +2413,16 @@
2.1446 (*SRA Schalk I, p.67 Nr. 403a *)
2.1447 val t = TermC.str2term "4/x - 3/y - 1";
2.1448 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1449 -\<close> text \<open> (*rewrite_set_ norm_Rational NO +*)
2.1450 -if UnparseC.term t = "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
2.1451 +if UnparseC.term t = "(- 3 * x + 4 * y + - 1 * x * y) / (x * y)"
2.1452 then () else error "rational.sml: diff.behav. in norm_Rational_mg 12";
2.1453
2.1454 \<close> ML \<open>
2.1455 val t = TermC.str2term "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a \<up> 2+3*b*c)/(a*b*c)";
2.1456 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1457 -\<close> text \<open> (*rewrite_set_ norm_Rational NO +*)
2.1458 if UnparseC.term t = "4 / c"
2.1459 then () else error "rational.sml: diff.behav. in norm_Rational_mg 13";
2.1460
2.1461 -\<close> text \<open>
2.1462 +\<close> ML \<open>
2.1463 (*SRA Schalk I, p.67 Nr. 410b *)
2.1464 val t = TermC.str2term "1/(x+1) + 1/(x+2) - 2/(x+3)";
2.1465 (* WN130911 non-termination due to non-termination of
2.1466 @@ -2425,18 +2433,21 @@
2.1467 then () else error "rational.sml: diff.behav. in norm_Rational_mg 14";
2.1468 *)
2.1469
2.1470 +\<close> ML \<open>
2.1471 (*SRA Schalk I, p.67 Nr. 413b *)
2.1472 val t = TermC.str2term "(1 + x)/(1 - x) - (1 - x)/(1 + x) + 2*x/(1 - x \<up> 2)";
2.1473 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1474 -if UnparseC.term t = "6 * x / (1 + -1 * x \<up> 2)"
2.1475 +if UnparseC.term t = "6 * x / (1 + - 1 * x \<up> 2)"
2.1476 then () else error "rational.sml: diff.behav. in norm_Rational_mg 15";
2.1477
2.1478 +\<close> ML \<open>
2.1479 (*SRA Schalk I, p.68 Nr. 414a *)
2.1480 val t = TermC.str2term "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
2.1481 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1482 -if UnparseC.term t ="(-2 + -5 * x + 2 * x \<up> 2) / (2 + -3 * x + x \<up> 2)"
2.1483 +if UnparseC.term t ="(- 2 + - 5 * x + 2 * x \<up> 2) / (2 + - 3 * x + x \<up> 2)"
2.1484 then () else error "rational.sml: diff.behav. in norm_Rational_mg 16";
2.1485
2.1486 +\<close> ML \<open>
2.1487 (*SRA Schalk I, p.68 Nr. 428b *)
2.1488 val t = TermC.str2term
2.1489 "1/(a - b) \<up> 2 + 1/(a + b) \<up> 2 - 2/(a \<up> 2 - b \<up> 2) - 4*(b \<up> 2 - 1)/(a \<up> 2 - b \<up> 2) \<up> 2";
2.1490 @@ -2448,6 +2459,7 @@
2.1491 then () else error "rational.sml: diff.behav. in norm_Rational_mg 18";
2.1492 *)
2.1493
2.1494 +\<close> ML \<open>
2.1495 (*SRA Schalk I, p.68 Nr. 430b *)
2.1496 val t = TermC.str2term
2.1497 "a \<up> 2/(a - 3*b) - 108*a*b \<up> 3/((a+3*b)*(a \<up> 2 - 9*b \<up> 2)) - 9*b \<up> 2*(a - 3*b)/(a+3*b) \<up> 2";
2.1498 @@ -2455,13 +2467,14 @@
2.1499 if UnparseC.term t = "a + 3 * b"
2.1500 then () else error "rational.sml: diff.behav. in norm_Rational_mg 19";
2.1501
2.1502 +\<close> ML \<open>
2.1503 (*SRA Schalk I, p.68 Nr. 432 *)
2.1504 val t = TermC.str2term
2.1505 ("(a \<up> 2 + a*b) / (a \<up> 2 - b \<up> 2) - (b \<up> 2 - a*b) / (b \<up> 2 - a \<up> 2) + " ^
2.1506 "a \<up> 2*(a - b) / (a \<up> 3 - a \<up> 2*b) - 2*a*(a \<up> 2 - b \<up> 2) / (a \<up> 3 - a*b \<up> 2) - " ^
2.1507 "2*b \<up> 2 / (a \<up> 2 - b \<up> 2)");
2.1508 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1509 -if UnparseC.term t = (*"0" ..isabisac15 | Isabelle2017..*) "0 / (a \<up> 2 + -1 * b \<up> 2)"
2.1510 +if UnparseC.term t = (*"0" ..isabisac15 | Isabelle2017..*) "0 / (a \<up> 2 + - 1 * b \<up> 2)"
2.1511 then () else error "rational.sml: diff.behav. in norm_Rational_mg 20";
2.1512
2.1513 \<close> ML \<open>
2.1514 @@ -2471,22 +2484,27 @@
2.1515 if UnparseC.term t = "(3 * y + b * x) / (b * y)"
2.1516 then () else error "rational.sml: diff.behav. in norm_Rational_mg 21";
2.1517
2.1518 -\<close> text \<open> (*multiply and cancel MANY EXAMPLES*)
2.1519 +
2.1520 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
2.1521 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
2.1522 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------";
2.1523 (*------- SRM Schalk I, p.68 Nr. 436a *)
2.1524 val t = TermC.str2term "3*(x+y) / (15*(x - y)) * 25*(x - y) \<up> 2 / (18*(x + y) \<up> 2)";
2.1525 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1526 -if UnparseC.term t = "(-5 * x + 5 * y) / (-18 * x + -18 * y)"
2.1527 +if UnparseC.term t = "(- 5 * x + 5 * y) / (- 18 * x + - 18 * y)"
2.1528 then () else error "rational.sml: diff.behav. in norm_Rational_mg 22";
2.1529
2.1530 +\<close> ML \<open>
2.1531 (*------- SRM.test Schalk I, p.68 Nr. 436b *)
2.1532 val t = TermC.str2term "5*a*(a - b) \<up> 2*(a + b) \<up> 3/(7*b*(a - b) \<up> 3) * 7*b/(a + b) \<up> 3";
2.1533 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1534 -if UnparseC.term t = "5 * a / (a + -1 * b)"
2.1535 +\<close> ML \<open>
2.1536 + UnparseC.term t = "(5 * a \<up> 3 + - 10 * a \<up> 2 * b + 5 * a * b \<up> 2) /\n(a \<up> 3 + - 3 * a \<up> 2 * b + 3 * a * b \<up> 2 + b \<up> 3)"
2.1537 +\<close> text \<open> (*norm_Rational: INCOMPLETE cancellation*)
2.1538 +if UnparseC.term t = "5 * a / (a + - 1 * b)"
2.1539 then () else error "rational.sml: diff.behav. in norm_Rational_mg 23";
2.1540
2.1541 +\<close> ML \<open>
2.1542 (*------- Schalk I, p.68 Nr. 437a *)
2.1543 val t = TermC.str2term "(3*a - 4*b) / (4*c+3*e) * (3*a+4*b)/(9*a \<up> 2 - 16*b \<up> 2)";
2.1544 (* raises an exception for unclear reasons:
2.1545 @@ -2506,14 +2524,15 @@
2.1546 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
2.1547 *)
2.1548
2.1549 +\<close> ML \<open>
2.1550 "----- S.K. corrected non-termination 060904";
2.1551 val t = TermC.str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a \<up> 2 - 16*b \<up> 2))";
2.1552 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
2.1553 if UnparseC.term t =
2.1554 - "(9 * a \<up> 2 + -16 * b \<up> 2) /\n(36 * a \<up> 2 * c + 27 * a \<up> 2 * e + -64 * b \<up> 2 * c +\n -48 * b \<up> 2 * e)"
2.1555 -(*"(9 * a \<up> 2 + -16 * b \<up> 2) / (36 * a \<up> 2 * c + 27 * a \<up> 2 * e + -64 * b \<up> 2 * c + -48 * b \<up> 2 * e)"*)
2.1556 + "(9 * a \<up> 2 + - 16 * b \<up> 2) /\n(36 * a \<up> 2 * c + 27 * a \<up> 2 * e + - 64 * b \<up> 2 * c +\n - 48 * b \<up> 2 * e)"
2.1557 then () else error "rational.sml: S.K.8..corrected 060904-6";
2.1558
2.1559 +\<close> ML \<open>
2.1560 "----- S.K. corrected non-termination of cancel_p_";
2.1561 val t'' = TermC.str2term ("(9 * a \<up> 2 + -16 * b \<up> 2) /" ^
2.1562 "(36 * a \<up> 2 * c + (27 * a \<up> 2 * e + (-64 * b \<up> 2 * c + -48 * b \<up> 2 * e)))");
2.1563 @@ -2523,6 +2542,7 @@
2.1564 then () else error "rational.sml: diff.behav. in cancel_p S.K.8";
2.1565 \--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------/*)
2.1566
2.1567 +\<close> ML \<open>
2.1568 (*------- Schalk I, p.68 Nr. 437b*)
2.1569 val t = TermC.str2term "(a + b)/(x \<up> 2 - y \<up> 2) * ((x - y) \<up> 2/(a \<up> 2 - b \<up> 2))";
2.1570 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1571 @@ -2535,24 +2555,28 @@
2.1572 exception Div raised
2.1573 *)
2.1574
2.1575 +\<close> ML \<open>
2.1576 (*------- SRM Schalk I, p.68 Nr. 438a *)
2.1577 val t = TermC.str2term "x*y / (x*y - y \<up> 2) * (x \<up> 2 - x*y)";
2.1578 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1579 if UnparseC.term t = "x \<up> 2"
2.1580 then () else error "rational.sml: diff.behav. in norm_Rational_mg 24";
2.1581
2.1582 +\<close> ML \<open>
2.1583 (*------- SRM Schalk I, p.68 Nr. 439b *)
2.1584 val t = TermC.str2term "(4*x \<up> 2 + 4*x + 1) * ((x \<up> 2 - 2*x \<up> 3) / (4*x \<up> 2 + 2*x))";
2.1585 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1586 -if UnparseC.term t = "(x + -4 * x \<up> 3) / 2"
2.1587 +if UnparseC.term t = "(x + - 4 * x \<up> 3) / 2"
2.1588 then () else error "rational.sml: diff.behav. in norm_Rational_mg 25";
2.1589
2.1590 +\<close> ML \<open>
2.1591 (*------- SRM Schalk I, p.68 Nr. 440a *)
2.1592 val t = TermC.str2term "(x \<up> 2 - 2*x) / (x \<up> 2 - 3*x) * (x - 3) \<up> 2 / (x \<up> 2 - 4)";
2.1593 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1594 -if UnparseC.term t = "(-3 + x) / (2 + x)"
2.1595 +if UnparseC.term t = "(- 3 + x) / (2 + x)"
2.1596 then () else error "rational.sml: diff.behav. in norm_Rational_mg 26";
2.1597
2.1598 +\<close> ML \<open>
2.1599 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
2.1600 val t = TermC.str2term "(a \<up> 3 - 9*a) / (a \<up> 3*b - a*b \<up> 3) * (a \<up> 2*b + a*b \<up> 2) / (a+3)";
2.1601 (* WN130911 non-termination for unclear reasons:
2.1602 @@ -2575,6 +2599,7 @@
2.1603 else error "rational.sml: diff.behav. in norm_Rational 27";
2.1604 *)
2.1605
2.1606 +\<close> ML \<open>
2.1607 "----- SK12 works since 0707xx";
2.1608 val t = TermC.str2term "(a \<up> 3 - 9*a) * (a \<up> 2*b+a*b \<up> 2) / ((a \<up> 3*b - a*b \<up> 3) * (a+3))";
2.1609 (* WN130911 non-termination due to non-termination of
2.1610 @@ -2585,16 +2610,17 @@
2.1611 else error "rational.sml: diff.behav. in norm_Rational 28";
2.1612 *)
2.1613
2.1614 -\<close> text \<open> (*common denominator and multiplication MANY EXAMPLES*)
2.1615 +\<close> ML \<open> (*common denominator and multiplication MANY EXAMPLES*)
2.1616 "-------- examples common denominator and multiplication from: Schalk --------";
2.1617 "-------- examples common denominator and multiplication from: Schalk --------";
2.1618 "-------- examples common denominator and multiplication from: Schalk --------";
2.1619 (*------- SRAM Schalk I, p.69 Nr. 441b *)
2.1620 val t = TermC.str2term "(4*a/3 + 3*b \<up> 2/a \<up> 3 + b/(4*a))*(4*b/(3*a))";
2.1621 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1622 -if UnparseC.term t = "(36 * b \<up> 3 + 3 * a \<up> 2 * b \<up> 2 + 16 * a \<up> 4 * b) / (9 * a \<up> 4)"
2.1623 +if UnparseC.term t = "(36 * b \<up> 3 + 3 * a \<up> 2 * b \<up> 2 + 16 * a \<up> 4 * b) /\n(9 * a \<up> 4)"
2.1624 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
2.1625
2.1626 +\<close> ML \<open>
2.1627 (*------- SRAM Schalk I, p.69 Nr. 442b *)
2.1628 val t = TermC.str2term ("(15*a \<up> 2/x \<up> 3 - 5*b \<up> 4/x \<up> 2 + 25*c \<up> 2/x) * " ^
2.1629 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + 1/c \<up> 3 * (b*x/a - 3*a/b \<up> 3)");
2.1630 @@ -2602,32 +2628,37 @@
2.1631 if UnparseC.term t = "5 * x \<up> 2 / (a * b \<up> 3 * c)"
2.1632 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";
2.1633
2.1634 +\<close> ML \<open>
2.1635 (*------- SRAM Schalk I, p.69 Nr. 443b *)
2.1636 val t = TermC.str2term "(a/2 + b/3) * (b/3 - a/2)";
2.1637 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1638 -if UnparseC.term t = "(-9 * a \<up> 2 + 4 * b \<up> 2) / 36"
2.1639 +if UnparseC.term t = "(- 9 * a \<up> 2 + 4 * b \<up> 2) / 36"
2.1640 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";
2.1641
2.1642 +\<close> ML \<open>
2.1643 (*------- SRAM Schalk I, p.69 Nr. 445b *)
2.1644 val t = TermC.str2term "(a \<up> 2/9 + 2*a/(3*b) + 4/b \<up> 2)*(a/3 - 2/b) + 8/b \<up> 3";
2.1645 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1646 if UnparseC.term t = "a \<up> 3 / 27"
2.1647 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";
2.1648
2.1649 +\<close> ML \<open>
2.1650 (*------- SRAM Schalk I, p.69 Nr. 446b *)
2.1651 val t = TermC.str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x \<up> 2 - 16*y \<up> 2)";
2.1652 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1653 if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + -20 * y \<up> 2" ..isabisac15 | Isabelle2017..*)
2.1654 - "(-30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / -1"
2.1655 + "(- 30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / - 1"
2.1656 then () else error "rational.sml: diff.behav. in norm_Rational_mg 32";
2.1657
2.1658 +\<close> ML \<open>
2.1659 (*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
2.1660 val t = TermC.str2term
2.1661 "(2*x \<up> 2/(3*y)+x/y \<up> 2)*(4*x \<up> 4/(9*y \<up> 2)+x \<up> 2/y \<up> 4)*(2*x \<up> 2/(3*y) - x/y \<up> 2)";
2.1662 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1663 -if UnparseC.term t = "(-81 * x \<up> 4 + 16 * x \<up> 8 * y \<up> 4) / (81 * y \<up> 8)"
2.1664 +if UnparseC.term t = "(- 81 * x \<up> 4 + 16 * x \<up> 8 * y \<up> 4) / (81 * y \<up> 8)"
2.1665 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";
2.1666
2.1667 +\<close> ML \<open>
2.1668 (*------- SRAM Schalk I, p.69 Nr. 450a *)
2.1669 val t = TermC.str2term
2.1670 "(4*x/(3*y)+2*y/(3*x)) \<up> 2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
2.1671 @@ -2635,6 +2666,7 @@
2.1672 if UnparseC.term t = "(52 * x \<up> 2 + 16 * y \<up> 2) / (9 * y \<up> 2)"
2.1673 then () else error "rational.sml: diff.behav. in norm_Rational_mg 34";
2.1674
2.1675 +\<close> ML \<open>
2.1676 (*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
2.1677 val t = TermC.str2term
2.1678 ("(15*a \<up> 4/(a*x \<up> 3) - 5*a*((b \<up> 4 - 5*c \<up> 2*x) / x \<up> 2)) * " ^
2.1679 @@ -2644,22 +2676,24 @@
2.1680 then () else error "rational.sml: diff.behav. in norm_Rational_mg 53";
2.1681
2.1682
2.1683 -\<close> text \<open> (*double fractions MANY EXAMPLES*)
2.1684 +\<close> ML \<open> (*double fractions MANY EXAMPLES*)
2.1685 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
2.1686 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
2.1687 "-------- examples double fractions from: Mathematik 1 Schalk ----------------";
2.1688 "----- SRD Schalk I, p.69 Nr. 454b";
2.1689 val t = TermC.str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";
2.1690 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1691 -if UnparseC.term t = "(-4 + 4 * x + -1 * x \<up> 2) / (4 * a \<up> 2)"
2.1692 +if UnparseC.term t = "(- 4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)"
2.1693 then () else error "rational.sml: diff.behav. in norm_Rational_mg 35";
2.1694
2.1695 +\<close> ML \<open>
2.1696 "----- SRD Schalk I, p.69 Nr. 455a";
2.1697 val t = TermC.str2term "(a \<up> 2 + 1)/(a \<up> 2 - 1) / ((a+1)/(a - 1))";
2.1698 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1699 if UnparseC.term t = "(1 + a \<up> 2) / (1 + 2 * a + a \<up> 2)" then ()
2.1700 else error "rational.sml: diff.behav. in norm_Rational_mg 36";
2.1701
2.1702 +\<close> ML \<open>
2.1703 "----- Schalk I, p.69 Nr. 455b";
2.1704 val t = TermC.str2term "(x \<up> 2 - 4)/(y \<up> 2 - 9)/((2+x)/(3 - y))";
2.1705 (* WN130911 non-termination due to non-termination of
2.1706 @@ -2671,6 +2705,7 @@
2.1707 else error "rational.sml: diff.behav. in norm_Rational_mg 37";
2.1708 *)
2.1709
2.1710 +\<close> ML \<open>
2.1711 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
2.1712 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))";
2.1713 (* WN130911 non-termination due to non-termination of
2.1714 @@ -2682,24 +2717,28 @@
2.1715 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
2.1716 *)
2.1717
2.1718 +\<close> ML \<open>
2.1719 "----- ?: worked before 0707xx";
2.1720 val t = TermC.str2term "(3 + -1 * y) / (-9 + y \<up> 2)";
2.1721 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1722 -if UnparseC.term t = "-1 / (3 + y)"
2.1723 +if UnparseC.term t = "- 1 / (3 + y)"
2.1724 then () else error "rational.sml: -1 / (3 + y) norm_Rational";
2.1725
2.1726 +\<close> ML \<open>
2.1727 "----- SRD Schalk I, p.69 Nr. 456b";
2.1728 val t = TermC.str2term "(b \<up> 3 - b \<up> 2) / (b \<up> 2+b) / (b \<up> 2 - 1)";
2.1729 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1730 if UnparseC.term t = "b / (1 + 2 * b + b \<up> 2)"
2.1731 then () else error "rational.sml: diff.behav. in norm_Rational_mg 38";
2.1732
2.1733 +\<close> ML \<open>
2.1734 "----- SRD Schalk I, p.69 Nr. 457b";
2.1735 val t = TermC.str2term "(16*a \<up> 2 - 9*b \<up> 2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a \<up> 2 - 9*a \<up> 2*b \<up> 2))";
2.1736 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1737 -if UnparseC.term t = "8 * a \<up> 2 + -6 * a * b + -12 * a \<up> 2 * b + 9 * a * b \<up> 2"
2.1738 +if UnparseC.term t = "8 * a \<up> 2 + - 6 * a * b + - 12 * a \<up> 2 * b + 9 * a * b \<up> 2"
2.1739 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
2.1740
2.1741 +\<close> ML \<open>
2.1742 "----- Schalk I, p.69 Nr. 458b works since 0707";
2.1743 val t = TermC.str2term "(2*a \<up> 2*x - a \<up> 2) / (a*x - b*x) / (b \<up> 2*(2*x - 1) / (x*(a - b)))";
2.1744 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1745 @@ -2718,12 +2757,14 @@
2.1746 else error "rational.sml: diff.behav. in norm_Rational_mg 39b";
2.1747 *)
2.1748
2.1749 +\<close> ML \<open>
2.1750 "----- SRD Schalk I, p.69 Nr. 459b";
2.1751 val t = TermC.str2term "(a \<up> 2 - b \<up> 2)/(a*b) / (4*(a+b) \<up> 2/a)";
2.1752 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1753 -if UnparseC.term t = "(a + -1 * b) / (4 * a * b + 4 * b \<up> 2)" then ()
2.1754 +if UnparseC.term t = "(a + - 1 * b) / (4 * a * b + 4 * b \<up> 2)" then ()
2.1755 else error "rational.sml: diff.behav. in norm_Rational_mg 41";
2.1756
2.1757 +\<close> ML \<open>
2.1758 "----- Schalk I, p.69 Nr. 460b nonterm.SK";
2.1759 val t = TermC.str2term "(9*(x \<up> 2 - 8*x + 16) / (4*(y \<up> 2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))";
2.1760 (*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1761 @@ -2739,18 +2780,21 @@
2.1762 then () else error "rational.sml: diff.behav. in norm_Rational_mg 42";
2.1763 *)
2.1764
2.1765 +\<close> ML \<open>
2.1766 "----- some variant of the above; was non-terminating before";
2.1767 val t = TermC.str2term "9*(x \<up> 2 - 8*x+16)*(16*y - 16)/(4*(y \<up> 2 - 2*y+1)*(3*x - 12))";
2.1768 val SOME (t , _) = rewrite_set_ thy false norm_Rational t;
2.1769 -if UnparseC.term t = "(48 + -12 * x) / (1 + -1 * y)"
2.1770 +if UnparseC.term t = "(48 + - 12 * x) / (1 + - 1 * y)"
2.1771 then () else error "some variant of the above; was non-terminating before";
2.1772
2.1773 +\<close> ML \<open>
2.1774 "----- SRD Schalk I, p.70 Nr. 472a";
2.1775 val t = TermC.str2term ("((8*x \<up> 2 - 32*y \<up> 2) / (2*x + 4*y)) / ((4*x - 8*y) / (x + y))");
2.1776 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1777 if UnparseC.term t = "x + y"
2.1778 then () else error "rational.sml: diff.behav. in norm_Rational_mg 43";
2.1779
2.1780 +\<close> ML \<open>
2.1781 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
2.1782 val t = TermC.str2term ("(a - (a*b + b \<up> 2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
2.1783 "((a - a \<up> 2/(a+b))/(a+(a*b)/(a - b)))");
2.1784 @@ -2758,18 +2802,21 @@
2.1785 if UnparseC.term t = "(2 * a \<up> 3 + 2 * a \<up> 2 * b) / (a \<up> 2 * b + b \<up> 3)"
2.1786 then () else error "rational.sml: diff.behav. in norm_Rational_mg 51";
2.1787
2.1788 +\<close> ML \<open>
2.1789 (*SRD Schalk I, p.69 Nr. 461a *)
2.1790 val t = TermC.str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x \<up> 2 - 9))";
2.1791 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1792 if UnparseC.term t = "1 / 2"
2.1793 then () else error "rational.sml: diff.behav. in norm_Rational_mg 44";
2.1794
2.1795 +\<close> ML \<open>
2.1796 (*SRD Schalk I, p.69 Nr. 464b *)
2.1797 val t = TermC.str2term "(a - a/(a - 2)) / (a + a/(a - 2))";
2.1798 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1799 -if UnparseC.term t = "(-3 + a) / (-1 + a)"
2.1800 +if UnparseC.term t = "(- 3 + a) / (- 1 + a)"
2.1801 then () else error "rational.sml: diff.behav. in norm_Rational_mg 45";
2.1802
2.1803 +\<close> ML \<open>
2.1804 (*SRD Schalk I, p.69 Nr. 465b *)
2.1805 val t = TermC.str2term "((x+3*y)/9 + (4*y \<up> 2 - 9*z \<up> 2)/(16*x)) / (x/9 + y/6 + z/4)";
2.1806 (* WN130911 non-termination due to non-termination of
2.1807 @@ -2782,17 +2829,19 @@
2.1808 then () else error "rational.sml: diff.behav. in norm_Rational_mg 46";
2.1809 *)
2.1810
2.1811 +\<close> ML \<open>
2.1812 (*SRD Schalk I, p.69 Nr. 466b *)
2.1813 val t = TermC.str2term "((1 - 7*(x - 2)/(x \<up> 2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x \<up> 2 - 25))";
2.1814 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1815 -if UnparseC.term t = "(25 + -10 * x + x \<up> 2) / 18"
2.1816 +if UnparseC.term t = "(25 + - 10 * x + x \<up> 2) / 18"
2.1817 then () else error "rational.sml: diff.behav. in norm_Rational_mg 47";
2.1818
2.1819 +\<close> ML \<open>
2.1820 (*SRD Schalk I, p.70 Nr. 469 *)
2.1821 val t = TermC.str2term ("3*b \<up> 2 / (4*a \<up> 2 - 8*a*b + 4*b \<up> 2) / " ^
2.1822 "(a / (a \<up> 2*b - b \<up> 3) + (a - b) / (4*a*b \<up> 2 + 4*b \<up> 3) - 1 / (4*b \<up> 2))");
2.1823 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
2.1824 -if UnparseC.term t = "-3 * b \<up> 3 / (-2 * a + 2 * b)"
2.1825 +if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)"
2.1826 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48";
2.1827
2.1828 \<close> text \<open> (*me nxt (14 * x * y) / ( x * y )*)
2.1829 @@ -2957,22 +3006,19 @@
2.1830 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
2.1831 if UnparseC.term tt' = "a \<up> 2 + - 2 * a * b + b \<up> 2" then () else error "rls chancel_p 2";
2.1832
2.1833 -\<close> text \<open> (*factout_p_ \<longrightarrow> NONE*)
2.1834 +\<close> ML \<open> (*factout_p_ \<longrightarrow> NONE*)
2.1835 "----- with .make_deriv; WN1130912 not investigated further, will be discontinued";
2.1836 val SOME (tt, _) = factout_p_ thy t;
2.1837 -if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + -1 * b) * (a + - 1 * b))"
2.1838 +if UnparseC.term tt = "(a + b) * (a + - 1 * b) / ((a + - 1 * b) * (a + - 1 * b))"
2.1839 then () else error "rls chancel_p 3";
2.1840 -UnparseC.term tt = "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
2.1841
2.1842 \<close> ML \<open>
2.1843 "--- with simpler ruleset";
2.1844 val {rules, rew_ord= (_, ro), ...} = Rule_Set.rep (assoc_rls "rev_rew_p");
2.1845 val der = Derive.do_one thy Atools_erls rules ro NONE tt;
2.1846 -\<close> ML \<open>
2.1847 -length der = 9
2.1848 -\<close> text \<open> (*Derive.do_one --> length - *)
2.1849 +
2.1850 if length der = 12 then () else error "WN1130912 rls chancel_p 4";
2.1851 -(*default_print_depth 99;*) writeln (deriv2str der); (*default_print_depth 3;*)
2.1852 +(*default_print_depth 99;*) writeln (Derive.deriv2str der); (*default_print_depth 3;*)
2.1853 \<close> ML \<open>
2.1854
2.1855 (*default_print_depth 99;*) map (UnparseC.term o #1) der; (*default_print_depth 3;*)
2.1856 @@ -3044,12 +3090,11 @@
2.1857 (*1st factor separately simplified *)
2.1858 val t = TermC.str2term "((12*x*y / (9*x \<up> 2 - y \<up> 2)) / (1 / (3*x - y) \<up> 2 - 1 / (3*x + y) \<up> 2))";
2.1859 val SOME (t', _) = rewrite_set_ thy false norm_Rational t;
2.1860 -\<close> text \<open> (*rewrite_set_ norm_Rational NOT CANCELLED*)
2.1861 -if UnparseC.term t' = "(-9 * x \<up> 2 + y \<up> 2) / -1" then () else error "Nr. 480b lhs changed";
2.1862 +if UnparseC.term t' = "(- 9 * x \<up> 2 + y \<up> 2) / - 1" then () else error "Nr. 480b lhs changed";
2.1863 (*2nd factor separately simplified *)
2.1864 val t = TermC.str2term "((1/(x - 5*y) \<up> 2 - 1/(x + 5*y) \<up> 2) / (20*x*y / (x \<up> 2 - 25*y \<up> 2)))";
2.1865 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
2.1866 -if UnparseC.term t' = "-1 / (-1 * x \<up> 2 + 25 * y \<up> 2)" then () else error "Nr. 480b rhs changed";
2.1867 +if UnparseC.term t' = "- 1 / (- 1 * x \<up> 2 + 25 * y \<up> 2)" then () else error "Nr. 480b rhs changed";
2.1868
2.1869 \<close> ML \<open>
2.1870 "-------- Schalk I, p.70 Nr. 477a: terms are exploding ?!?";
2.1871 @@ -3183,4 +3228,7 @@
2.1872 "xx"
2.1873 ^ "xxx" (*+*)
2.1874 \<close>
2.1875 +
2.1876 +ML_file \<open>MathEngBasic/rewrite.sml\<close>
2.1877 +ML_file \<open>Knowledge/poly.sml\<close>
2.1878 end