wneuper/isa: src/Tools/isac/Knowledge/Poly.thy@04d3f0133827 (annotated)

neuper@37906	1	(* WN.020812: theorems in the Reals,
neuper@37906	2	necessary for special rule sets, in addition to Isabelle2002.
neuper@37906	3	!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
neuper@37906	4	!!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
neuper@37906	5	!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
neuper@37906	6	xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
neuper@37906	7	changed by: Richard Lang 020912
neuper@37906	8	*)
neuper@37906	9
neuper@37950	10	theory Poly imports Simplify begin
neuper@37906	11
neuper@37906	12	consts
neuper@37906	13
neuper@37906	14	is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
neuper@37950	15	is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (RL DA )
neuper@37950	16	has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(RL DA )
neuper@37950	17	is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(RL030626)
neuper@37906	18
neuper@37950	19	is'_multUnordered:: "real => bool" ("_ is'_multUnordered")
neuper@37950	20	is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (WN030618)
neuper@37950	21	is'_polyexp :: "real => bool" ("_ is'_polyexp")
neuper@37906	22
neuper@37906	23	Expand'_binoms
neuper@37950	24	:: "['y,
neuper@37950	25	'y] => 'y"
neuper@37950	26	("((Script Expand'_binoms (_ =))//
neuper@37950	27	(_))" 9)
neuper@37906	28
neuper@37906	29	(-------------------- rules------------------------------------------------)
t@42211	30	axioms(axiomatization where) (*.not contained in Isabelle2002,
neuper@37906	31	stated as axioms, TODO: prove as theorems;
neuper@37906	32	theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
neuper@37906	33
t@42211	34	realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" (and)
t@42211	35	realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" (and)
t@42211	36	realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" (and)
t@42211	37	realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" (and)
neuper@37906	38
t@42211	39	realpow_oneI: "r ^^^ 1 = r" (and)
t@42211	40	realpow_zeroI: "r ^^^ 0 = 1" (and)
t@42211	41	realpow_eq_oneI: "1 ^^^ n = 1" (and)
t@42211	42	realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" (and)
neuper@37974	43	realpow_multI_poly: "[\| r is_polyexp; s is_polyexp \|] ==>
t@42211	44	(r * s) ^^^ n = r ^^^ n * s ^^^ n" (and)
t@42211	45	realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" (and)
neuper@37906	46
t@42211	47	realpow_twoI: "r ^^^ 2 = r * r" (and)
t@42211	48	realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" (and)
t@42211	49	realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" (and)
t@42211	50	realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" (and)
t@42211	51	realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" (and)
t@42211	52	realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" (and)
t@42211	53	realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" (and)
t@42211	54	realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" (and)
t@42211	55	realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" (and)
neuper@37974	56	realpow_def_atom: "[\| Not (r is_atom); 1 < n \|]
t@42211	57	==> r ^^^ n = r * r ^^^ (n + -1)" (and)
t@42211	58	realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" (and)
neuper@37906	59
neuper@37906	60
t@42211	61	realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" (and)
t@42211	62	realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" (and)
neuper@37906	63
neuper@37906	64
neuper@37906	65	(* RL 020914 *)
t@42211	66	real_pp_binom_times: "(a + b)(c + d) = ac + ad + bc + bd" (and*)
t@42211	67	real_pm_binom_times: "(a + b)(c - d) = ac - ad + bc - bd" (and*)
t@42211	68	real_mp_binom_times: "(a - b)(c + d) = ac + ad - bc - bd" (and*)
t@42211	69	real_mm_binom_times: "(a - b)(c - d) = ac - ad - bc + bd" (and*)
t@42211	70	real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3" (and)
neuper@37974	71	real_plus_binom_pow3_poly: "[\| a is_polyexp; b is_polyexp \|] ==>
t@42211	72	(a + b)^^^3 = a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3" (and)
t@42211	73	real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3a^^^2b + 3ab^^^2 - b^^^3" (and)
neuper@37974	74	real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3a^^^2b + 3ab^^^2 +
t@42211	75	-1b^^^3" (and*)
neuper@37974	76	(* real_plus_binom_pow: "[\| n is_const; 3 < n \|] ==>
neuper@37950	77	(a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
neuper@37974	78	real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3)
t@42211	79	(a + b)" (and*)
neuper@37974	80	real_plus_binom_pow4_poly: "[\| a is_polyexp; b is_polyexp \|] ==>
neuper@37950	81	(a + b)^^^4 = (a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3)
t@42211	82	(a + b)" (and*)
neuper@37974	83	real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3)
t@42211	84	(a^^^2 + 2ab + b^^^2)" (and*)
neuper@37974	85	real_plus_binom_pow5_poly: "[\| a is_polyexp; b is_polyexp \|] ==>
neuper@37950	86	(a + b)^^^5 = (a^^^3 + 3a^^^2b + 3ab^^^2
t@42211	87	+ b^^^3)(a^^^2 + 2ab + b^^^2)" (and*)
t@42211	88	real_diff_plus: "a - b = a + -b" (17.3.03: do_NOT_use) (and)
t@42211	89	real_diff_minus: "a - b = a + -1 * b" (and)
t@42211	90	real_plus_binom_times: "(a + b)(a + b) = a^^^2 + 2ab + b^^^2" (and*)
t@42211	91	real_minus_binom_times: "(a - b)(a - b) = a^^^2 - 2ab + b^^^2" (and*)
neuper@37906	92	(WN071229 changed for Schaerding -----vvv)
neuper@37974	93	(real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2ab + b^^^2")
t@42211	94	real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" (and)
neuper@37906	95	(WN071229 changed for Schaerding -----^^^)
neuper@37974	96	real_plus_binom_pow2_poly: "[\| a is_polyexp; b is_polyexp \|] ==>
t@42211	97	(a + b)^^^2 = a^^^2 + 2ab + b^^^2" (and)
t@42211	98	real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2ab + b^^^2" (and)
t@42211	99	real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2ab + b^^^2" (and)
t@42211	100	real_plus_minus_binom1: "(a + b)(a - b) = a^^^2 - b^^^2" (and*)
t@42211	101	real_plus_minus_binom1_p: "(a + b)(a - b) = a^^^2 + -1b^^^2" (and)
t@42211	102	real_plus_minus_binom1_p_p: "(a + b)(a + -1 b) = a^^^2 + -1b^^^2" (and*)
t@42211	103	real_plus_minus_binom2: "(a - b)(a + b) = a^^^2 - b^^^2" (and*)
t@42211	104	real_plus_minus_binom2_p: "(a - b)(a + b) = a^^^2 + -1b^^^2" (and)
t@42211	105	real_plus_minus_binom2_p_p: "(a + -1 * b)(a + b) = a^^^2 + -1b^^^2" (and)
t@42211	106	real_plus_binom_times1: "(a + 1b)(a + -1b) = a^^^2 + -1b^^^2" (and)
t@42211	107	real_plus_binom_times2: "(a + -1b)(a + 1b) = a^^^2 + -1b^^^2" (and)
neuper@37906	108
neuper@37974	109	real_num_collect: "[\| l is_const; m is_const \|] ==>
t@42211	110	l * n + m * n = (l + m) * n" (and)
neuper@37906	111	(* FIXME.MG.0401: replace 'real_num_collect_assoc'
neuper@37906	112	by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
neuper@37974	113	real_num_collect_assoc: "[\| l is_const; m is_const \|] ==>
t@42211	114	l * n + (m * n + k) = (l + m) * n + k" (and)
neuper@37974	115	real_num_collect_assoc_l: "[\| l is_const; m is_const \|] ==>
neuper@37950	116	l * n + (m * n + k) = (l + m)
t@42211	117	* n + k" (and)
neuper@37974	118	real_num_collect_assoc_r: "[\| l is_const; m is_const \|] ==>
t@42211	119	(k + m * n) + l * n = k + (l + m) * n" (and)
t@42211	120	real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" (and)
neuper@37906	121	(* FIXME.MG.0401: replace 'real_one_collect_assoc'
neuper@37906	122	by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
t@42211	123	real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" (and)
neuper@37906	124
t@42211	125	real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" (and)
t@42211	126	real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" (and)
neuper@37906	127
neuper@37906	128	(* FIXME.MG.0401: replace 'real_mult_2_assoc'
neuper@37906	129	by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
t@42211	130	real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" (and)
t@42211	131	real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" (and)
t@42211	132	real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" (and)
neuper@37906	133
t@42211	134	real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" (and)
neuper@37974	135	real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
neuper@37950	136
neuper@37950	137	text {* remark on 'polynomials'
neuper@37950	138	WN020919
neuper@37950	139	* there are 5 kinds of expanded normalforms *
neuper@37950	140
neuper@37950	141	[1] 'complete polynomial' (Komplettes Polynom), univariate
neuper@37950	142	a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
neuper@37950	143	not (a_n = 0), some a_i may be zero (DON'T disappear),
neuper@37950	144	variables in monomials lexicographically ordered and complete,
neuper@37950	145	x written as 1*x^1, ...
neuper@37950	146	[2] 'polynomial' (Polynom), univariate and multivariate
neuper@37950	147	a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
neuper@37950	148	a_0 + a_1.x_1.x_2^n_12...x_m^n_1m +...+ a_n.x_1^n.x_2^n_n2...x_m^n_nm
neuper@37950	149	not (a_n = 0), some a_i may be zero (ie. monomials disappear),
neuper@37950	150	exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
neuper@37950	151	and variables in monomials are lexicographically ordered
neuper@37950	152	examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
neuper@37950	153	[1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
neuper@37950	154	[2]: "x + (-50) * x ^^^ 3"
neuper@37950	155	[2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
neuper@37950	156
neuper@37950	157	[3] 'expanded_term' (Ausmultiplizierter Term):
neuper@37950	158	pull out unary minus to binary minus,
neuper@37950	159	as frequently exercised in schools; other conditions for [2] hold however
neuper@37950	160	examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
neuper@37950	161	"4 * x ^^^ 2 - 9 * y ^^^ 2"
neuper@37950	162	[4] 'polynomial_in' (Polynom in):
neuper@37950	163	polynomial in 1 variable with arbitrary coefficients
neuper@37950	164	examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
neuper@37950	165	"(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
neuper@37950	166	[5] 'expanded_in' (Ausmultiplizierter Termin in):
neuper@37950	167	analoguous to [3] with binary minus like [3]
neuper@37950	168	examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
neuper@37950	169	"(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
neuper@37950	170	*}
neuper@37950	171
neuper@37950	172	ML {*
neuper@37972	173	val thy = @{theory};
neuper@37972	174
neuper@37950	175	(* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
neuper@37950	176	fun is_polyrat_in t v =
neuper@37950	177	let fun coeff_in c v = member op = (vars c) v;
neuper@38031	178	fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
neuper@37950	179	(* at the moment there is no term like this, but ....*)
neuper@38014	180	\| finddivide (t as (Const ("Rings.inverse_class.divide",_) $ _ $ b)) v =
neuper@37950	181	not(coeff_in b v)
neuper@37950	182	\| finddivide (_ $ t1 $ t2) v =
neuper@37950	183	(finddivide t1 v) orelse (finddivide t2 v)
neuper@37950	184	\| finddivide (_ $ t1) v = (finddivide t1 v)
neuper@37950	185	\| finddivide _ _ = false;
neuper@37950	186	in finddivide t v end;
neuper@37950	187
neuper@37950	188	fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
neuper@37950	189	if is_polyrat_in t v
neuper@37950	190	then SOME ((term2str p) ^ " = True",
neuper@37950	191	Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950	192	else SOME ((term2str p) ^ " = True",
neuper@37950	193	Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@38015	194	\| eval_is_polyrat_in _ _ _ _ = ((tracing"### no matches";) NONE);
neuper@37950	195
neuper@37950	196	local
neuper@37950	197	(.a 'c is coefficient of v' if v does NOT occur in c.)
neuper@37950	198	fun coeff_in c v = not (member op = (vars c) v);
neuper@37950	199	(* FIXME.WN100826 shift this into test--------------
neuper@37950	200	val v = (term_of o the o (parse thy)) "x";
neuper@37950	201	val t = (term_of o the o (parse thy)) "1";
neuper@37950	202	coeff_in t v;
neuper@37950	203	(val it = true : bool)
neuper@37950	204	val t = (term_of o the o (parse thy)) "a*b+c";
neuper@37950	205	coeff_in t v;
neuper@37950	206	(val it = true : bool)
neuper@37950	207	val t = (term_of o the o (parse thy)) "a*x+c";
neuper@37950	208	coeff_in t v;
neuper@37950	209	(val it = false : bool)
neuper@37950	210	----------------------------------------------------*)
neuper@37950	211	(*. a 'monomial t in variable v' is a term t with
neuper@37950	212	either (1) v NOT existent in t, or (2) v contained in t,
neuper@37950	213	if (1) then degree 0
neuper@37950	214	if (2) then v is a factor on the very right, ev. with exponent.*)
neuper@37950	215	fun factor_right_deg (case 2)
neuper@38034	216	(t as Const ("Groups.times_class.times",_) $ t1 $
neuper@37950	217	(Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
neuper@37950	218	if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
neuper@37950	219	\| factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
neuper@37950	220	if (vv = v) then SOME (int_of_str' d) else NONE
neuper@38034	221	\| factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v =
neuper@37950	222	if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
neuper@37950	223	\| factor_right_deg vv v =
neuper@37950	224	if (vv = v) then SOME 1 else NONE;
neuper@37950	225	fun mono_deg_in m v =
neuper@37950	226	if coeff_in m v then (case 1) SOME 0
neuper@37950	227	else factor_right_deg m v;
neuper@37950	228	(* FIXME.WN100826 shift this into test-----------------------------
neuper@37950	229	val v = (term_of o the o (parse thy)) "x";
neuper@37950	230	val t = (term_of o the o (parse thy)) "(ab+c)x^^^7";
neuper@37950	231	mono_deg_in t v;
neuper@37950	232	(val it = SOME 7)
neuper@37950	233	val t = (term_of o the o (parse thy)) "x^^^7";
neuper@37950	234	mono_deg_in t v;
neuper@37950	235	(val it = SOME 7)
neuper@37950	236	val t = (term_of o the o (parse thy)) "(ab+c)x";
neuper@37950	237	mono_deg_in t v;
neuper@37950	238	(val it = SOME 1)
neuper@37950	239	val t = (term_of o the o (parse thy)) "(ab+x)x";
neuper@37950	240	mono_deg_in t v;
neuper@37950	241	(val it = NONE)
neuper@37950	242	val t = (term_of o the o (parse thy)) "x";
neuper@37950	243	mono_deg_in t v;
neuper@37950	244	(val it = SOME 1)
neuper@37950	245	val t = (term_of o the o (parse thy)) "(a*b+c)";
neuper@37950	246	mono_deg_in t v;
neuper@37950	247	(val it = SOME 0)
neuper@37950	248	val t = (term_of o the o (parse thy)) "ab - (ab)x";
neuper@37950	249	mono_deg_in t v;
neuper@37950	250	(val it = NONE)
neuper@37950	251	------------------------------------------------------------------*)
neuper@37950	252	fun expand_deg_in t v =
neuper@38014	253	let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950	254	(case mono_deg_in t2 v of (* $ is left associative*)
neuper@37950	255	SOME d' => edi d' d' t1
neuper@37950	256	\| NONE => NONE)
neuper@38014	257	\| edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
neuper@37950	258	(case mono_deg_in t2 v of
neuper@37950	259	SOME d' => edi d' d' t1
neuper@37950	260	\| NONE => NONE)
neuper@38014	261	\| edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
neuper@37950	262	(case mono_deg_in t2 v of
neuper@37950	263	(RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x)
neuper@37950	264	SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
neuper@37950	265	then edi d' dmax t1 else NONE
neuper@37950	266	\| NONE => NONE)
neuper@38014	267	\| edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950	268	(case mono_deg_in t2 v of
neuper@37950	269	(RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x)
neuper@37950	270	SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
neuper@37950	271	then edi d' dmax t1 else NONE
neuper@37950	272	\| NONE => NONE)
neuper@37950	273	\| edi ~1 ~1 t = (case mono_deg_in t v of
neuper@37950	274	d as SOME _ => d
neuper@37950	275	\| NONE => NONE)
neuper@37950	276	\| edi d dmax t = (basecase last)
neuper@37950	277	(case mono_deg_in t v of
neuper@37950	278	SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
neuper@37950	279	then SOME dmax else NONE
neuper@37950	280	\| NONE => NONE)
neuper@37950	281	in edi ~1 ~1 t end;
neuper@37950	282	(* FIXME.WN100826 shift this into test-----------------------------
neuper@37950	283	val v = (term_of o the o (parse thy)) "x";
neuper@37950	284	val t = (term_of o the o (parse thy)) "a+b";
neuper@37950	285	expand_deg_in t v;
neuper@37950	286	(val it = SOME 0)
neuper@37950	287	val t = (term_of o the o (parse thy)) "(a+b)*x";
neuper@37950	288	expand_deg_in t v;
neuper@37950	289	(SOME 1)
neuper@37950	290	val t = (term_of o the o (parse thy)) "ab - (a+b)x";
neuper@37950	291	expand_deg_in t v;
neuper@37950	292	(SOME 1)
neuper@37950	293	val t = (term_of o the o (parse thy)) "ab + (a-b)x";
neuper@37950	294	expand_deg_in t v;
neuper@37950	295	(SOME 1)
neuper@37950	296	val t = (term_of o the o (parse thy)) "ab + (a+b)x + x^^^2";
neuper@37950	297	expand_deg_in t v;
neuper@37950	298	-------------------------------------------------------------------*)
neuper@37950	299	fun poly_deg_in t v =
neuper@38014	300	let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950	301	(case mono_deg_in t2 v of (* $ is left associative*)
neuper@37950	302	SOME d' => edi d' d' t1
neuper@37950	303	\| NONE => NONE)
neuper@38014	304	\| edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950	305	(case mono_deg_in t2 v of
neuper@37950	306	(RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x)
neuper@37950	307	SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
neuper@37950	308	then edi d' dmax t1 else NONE
neuper@37950	309	\| NONE => NONE)
neuper@37950	310	\| edi ~1 ~1 t = (case mono_deg_in t v of
neuper@37950	311	d as SOME _ => d
neuper@37950	312	\| NONE => NONE)
neuper@37950	313	\| edi d dmax t = (basecase last)
neuper@37950	314	(case mono_deg_in t v of
neuper@37950	315	SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
neuper@37950	316	then SOME dmax else NONE
neuper@37950	317	\| NONE => NONE)
neuper@37950	318	in edi ~1 ~1 t end;
neuper@37950	319	in
neuper@37950	320
neuper@37950	321	fun is_expanded_in t v =
neuper@37950	322	case expand_deg_in t v of SOME _ => true \| NONE => false;
neuper@37950	323	fun is_poly_in t v =
neuper@37950	324	case poly_deg_in t v of SOME _ => true \| NONE => false;
neuper@37950	325	fun has_degree_in t v =
neuper@37950	326	case expand_deg_in t v of SOME d => d \| NONE => ~1;
neuper@37980	327	end;(local)
neuper@37950	328	(* FIXME.WN100826 shift this into test-----------------------------
neuper@37950	329	val v = (term_of o the o (parse thy)) "x";
neuper@37950	330	val t = (term_of o the o (parse thy)) "ab - (a+b)x + x^^^2";
neuper@37950	331	has_degree_in t v;
neuper@37950	332	(val it = 2)
neuper@37950	333	val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
neuper@37950	334	has_degree_in t v;
neuper@37950	335	(val it = 2)
neuper@37950	336	val t = (term_of o the o (parse thy)) "6 + 13x + 6x^^^2";
neuper@37950	337	has_degree_in t v;
neuper@37950	338	(val it = 2)
neuper@37950	339	-------------------------------------------------------------------*)
neuper@37950	340
neuper@37950	341	(("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")))
neuper@37950	342	fun eval_is_expanded_in _ _
neuper@37950	343	(p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
neuper@37950	344	if is_expanded_in t v
neuper@37950	345	then SOME ((term2str p) ^ " = True",
neuper@37950	346	Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950	347	else SOME ((term2str p) ^ " = True",
neuper@37950	348	Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950	349	\| eval_is_expanded_in _ _ _ _ = NONE;
neuper@37950	350	(*
neuper@37950	351	val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
neuper@37950	352	val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
neuper@37950	353	(val id = "Poly.is'_expanded'_in (-8 - 2 x + x ^^^ 2) x = True"*)
neuper@37950	354	term2str t';
neuper@37950	355	(val it = "Poly.is'_expanded'_in (-8 - 2 x + x ^^^ 2) x = True"*)
neuper@37950	356	*)
neuper@37950	357
neuper@37950	358	(("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")))
neuper@37950	359	fun eval_is_poly_in _ _
neuper@37950	360	(p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
neuper@37950	361	if is_poly_in t v
neuper@37950	362	then SOME ((term2str p) ^ " = True",
neuper@37950	363	Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950	364	else SOME ((term2str p) ^ " = True",
neuper@37950	365	Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950	366	\| eval_is_poly_in _ _ _ _ = NONE;
neuper@37950	367	(*
neuper@37950	368	val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
neuper@37950	369	val SOME (id, t') = eval_is_poly_in 0 0 t 0;
neuper@37950	370	(val id = "Poly.is'_poly'_in (8 + 2 x + x ^^^ 2) x = True"*)
neuper@37950	371	term2str t';
neuper@37950	372	(val it = "Poly.is'_poly'_in (8 + 2 x + x ^^^ 2) x = True"*)
neuper@37950	373	*)
neuper@37950	374
neuper@37950	375	(("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")))
neuper@37950	376	fun eval_has_degree_in _ _
neuper@37950	377	(p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
neuper@37950	378	let val d = has_degree_in t v
neuper@37950	379	val d' = term_of_num HOLogic.realT d
neuper@37950	380	in SOME ((term2str p) ^ " = " ^ (string_of_int d),
neuper@37950	381	Trueprop $ (mk_equality (p, d')))
neuper@37950	382	end
neuper@37950	383	\| eval_has_degree_in _ _ _ _ = NONE;
neuper@37950	384	(*
neuper@37950	385	> val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
neuper@37950	386	> val SOME (id, t') = eval_has_degree_in 0 0 t 0;
neuper@37950	387	val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
neuper@37950	388	> term2str t';
neuper@37950	389	val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
neuper@37950	390	*)
neuper@37950	391
neuper@37978	392	(..)
neuper@37978	393	val calculate_Poly =
neuper@37978	394	append_rls "calculate_PolyFIXXXME.not.impl." e_rls
neuper@37978	395	[];
neuper@37978	396
neuper@37950	397	(.for evaluation of conditions in rewrite rules.)
neuper@42319	398	val Poly_erls = append_rls "Poly_erls" Atools_erls
neuper@42319	399	[ Calc ("HOL.eq",eval_equal "#equal_"),
neuper@42319	400	Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
neuper@42319	401	Calc ("Groups.plus_class.plus",eval_binop "#add_"),
neuper@42319	402	Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
neuper@42319	403	Calc ("Groups.times_class.times",eval_binop "#mult_"),
neuper@42319	404	Calc ("Atools.pow" ,eval_binop "#power_")
neuper@42319	405	];
neuper@37950	406
neuper@37950	407	val poly_crls =
neuper@37950	408	append_rls "poly_crls" Atools_crls
neuper@41922	409	[ Calc ("HOL.eq",eval_equal "#equal_"),
neuper@37969	410	Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
neuper@38014	411	Calc ("Groups.plus_class.plus",eval_binop "#add_"),
neuper@38014	412	Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
neuper@38034	413	Calc ("Groups.times_class.times",eval_binop "#mult_"),
neuper@37950	414	Calc ("Atools.pow" ,eval_binop "#power_")
neuper@37950	415	];
neuper@37950	416
neuper@37950	417	local (. for make_polynomial .)
neuper@37950	418
neuper@37950	419	open Term; (* for type order = EQUAL \| LESS \| GREATER *)
neuper@37950	420
neuper@37950	421	fun pr_ord EQUAL = "EQUAL"
neuper@37950	422	\| pr_ord LESS = "LESS"
neuper@37950	423	\| pr_ord GREATER = "GREATER";
neuper@37950	424
neuper@37950	425	fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
neuper@37950	426	(case a of
neuper@37950	427	"Atools.pow" => ((("\|\|\|\|\|\|\|\|\|\|\|\|\|", 0), T), 0) (WN greatest string)
neuper@37950	428	\| _ => (((a, 0), T), 0))
neuper@37950	429	\| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
neuper@37950	430	\| dest_hd' (Var v) = (v, 2)
neuper@37950	431	\| dest_hd' (Bound i) = ((("", i), dummyT), 3)
neuper@37950	432	\| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
neuper@37950	433
neuper@37950	434	fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
neuper@37950	435	(case int_of_str (order) of
neuper@37950	436	SOME d => d
neuper@37950	437	\| NONE => 0)
neuper@37950	438	\| get_order_pow _ = 0;
neuper@37950	439
neuper@37950	440	fun size_of_term' (Const(str,_) $ t) =
neuper@37950	441	if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(WN)
neuper@37950	442	\| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
neuper@37950	443	\| size_of_term' (f$t) = size_of_term' f + size_of_term' t
neuper@37950	444	\| size_of_term' _ = 1;
neuper@37950	445
neuper@37950	446	fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
neuper@37974	447	(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) \| ord => ord)
neuper@37950	448	\| term_ord' pr thy (t, u) =
neuper@37950	449	(if pr then
neuper@37950	450	let
neuper@37950	451	val (f, ts) = strip_comb t and (g, us) = strip_comb u;
neuper@38053	452	val _ = tracing ("t= f@ts= \"" ^
neuper@38053	453	(Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) f) ^
neuper@38053	454	"\" @ \"[" ^
neuper@38053	455	(commas (map (Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	456	(thy2ctxt thy))) ts)) ^
neuper@38053	457	"]\"");
neuper@38053	458	val _ = tracing("u= g@us= \""^
neuper@38053	459	(Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) g) ^
neuper@38053	460	"\" @ \"[" ^
neuper@38053	461	(commas (map (Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	462	(thy2ctxt thy))) us)) ^
neuper@38053	463	"]\"");
neuper@38053	464	val _ = tracing ("size_of_term(t,u)= (" ^
neuper@38053	465	(string_of_int (size_of_term' t)) ^ ", " ^
neuper@38053	466	(string_of_int (size_of_term' u)) ^ ")");
neuper@38053	467	val _ = tracing ("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
neuper@38053	468	val _ = tracing ("terms_ord(ts,us) = " ^
neuper@38053	469	((pr_ord o terms_ord str false) (ts, us)));
neuper@38053	470	val _ = tracing ("-------");
neuper@37950	471	in () end
neuper@37950	472	else ();
neuper@37950	473	case int_ord (size_of_term' t, size_of_term' u) of
neuper@37950	474	EQUAL =>
neuper@37950	475	let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
neuper@37950	476	(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
neuper@37950	477	\| ord => ord)
neuper@37950	478	end
neuper@37950	479	\| ord => ord)
neuper@37950	480	and hd_ord (f, g) = (* ~ term.ML *)
neuper@37974	481	prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
neuper@37950	482	and terms_ord str pr (ts, us) =
neuper@37991	483	list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us);
neuper@37950	484	in
neuper@37950	485
neuper@37950	486	fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
neuper@37950	487	(term_ord' pr thy(***) tu = LESS );
neuper@37950	488
neuper@37950	489	end;(local)
neuper@37950	490
neuper@37950	491
neuper@37950	492	rew_ord' := overwritel (!rew_ord',
neuper@37950	493	[("termlessI", termlessI),
neuper@37950	494	("ord_make_polynomial", ord_make_polynomial false thy)
neuper@37950	495	]);
neuper@37950	496
neuper@37950	497
neuper@37950	498	val expand =
neuper@37974	499	Rls{id = "expand", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
neuper@37974	500	erls = e_rls,srls = Erls, calc = [],
neuper@37965	501	rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950	502	("(z1.0 + z2.0) w = z1.0 * w + z2.0 * w"*)
neuper@37974	503	Thm ("right_distrib",num_str @{thm right_distrib})
neuper@37950	504	("w (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950	505	], scr = EmptyScr}:rls;
neuper@37950	506
neuper@37950	507	(*----------------- Begin: rulesets for make_polynomial_ -----------------
neuper@37950	508	'rlsIDs' redefined by MG as 'rlsIDs_'
neuper@37950	509	^^^*)
neuper@37950	510
neuper@37980	511	val discard_minus =
neuper@37980	512	Rls{id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
neuper@37980	513	erls = e_rls, srls = Erls, calc = [],
neuper@37950	514	(asm_thm = [],)
neuper@37969	515	rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
neuper@37950	516	("a - b = a + -1 b"*)
neuper@37969	517	Thm ("sym_real_mult_minus1",
neuper@37974	518	num_str (@{thm real_mult_minus1} RS @{thm sym}))
neuper@37950	519	(- ?z = "-1 ?z"*)
neuper@37950	520	], scr = EmptyScr}:rls;
neuper@37980	521
neuper@37950	522	val expand_poly_ =
neuper@37950	523	Rls{id = "expand_poly_", preconds = [],
neuper@37950	524	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	525	erls = e_rls,srls = Erls,
neuper@37950	526	calc = [],
neuper@37950	527	(asm_thm = [],)
neuper@37969	528	rules = [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),
neuper@37950	529	("(a + b)^^^4 = ... ")
neuper@37969	530	Thm ("real_plus_binom_pow5",num_str @{thm real_plus_binom_pow5}),
neuper@37950	531	("(a + b)^^^5 = ... ")
neuper@37969	532	Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
neuper@37950	533	("(a + b)^^^3 = a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3" )
neuper@37950	534	(WN071229 changed/removed for Schaerding -----vvv)
neuper@37969	535	(Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),)
neuper@37950	536	("(a + b)^^^2 = a^^^2 + 2ab + b^^^2")
neuper@37969	537	Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
neuper@37950	538	("(a + b)^^^2 = (a + b) (a + b)"*)
neuper@37950	539	(*Thm ("real_plus_minus_binom1_p_p",
neuper@37969	540	num_str @{thm real_plus_minus_binom1_p_p}),*)
neuper@37950	541	("(a + b)(a + -1 * b) = a^^^2 + -1b^^^2")
neuper@37950	542	(*Thm ("real_plus_minus_binom2_p_p",
neuper@37969	543	num_str @{thm real_plus_minus_binom2_p_p}),*)
neuper@37950	544	("(a + -1 b)(a + b) = a^^^2 + -1b^^^2"*)
neuper@37950	545	(WN071229 changed/removed for Schaerding -----^^^)
neuper@37950	546
neuper@37965	547	Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950	548	("(z1.0 + z2.0) w = z1.0 * w + z2.0 * w"*)
neuper@37974	549	Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950	550	("w (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950	551
neuper@37969	552	Thm ("realpow_multI", num_str @{thm realpow_multI}),
neuper@37950	553	("(r s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37969	554	Thm ("realpow_pow",num_str @{thm realpow_pow})
neuper@37950	555	("(a ^^^ b) ^^^ c = a ^^^ (b c)"*)
neuper@37950	556	], scr = EmptyScr}:rls;
neuper@37950	557
neuper@37950	558	(.the expression contains + - ^ only ?
neuper@37950	559	this is weaker than 'is_polynomial' !.*)
neuper@37950	560	fun is_polyexp (Free _) = true
neuper@38014	561	\| is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
neuper@38014	562	\| is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
neuper@38034	563	\| is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
neuper@37950	564	\| is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
neuper@38014	565	\| is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950	566	((is_polyexp t1) andalso (is_polyexp t2))
neuper@38014	567	\| is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
neuper@37950	568	((is_polyexp t1) andalso (is_polyexp t2))
neuper@38034	569	\| is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
neuper@37950	570	((is_polyexp t1) andalso (is_polyexp t2))
neuper@37950	571	\| is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
neuper@37950	572	((is_polyexp t1) andalso (is_polyexp t2))
neuper@37950	573	\| is_polyexp _ = false;
neuper@37950	574
neuper@37950	575	(("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")))
neuper@37950	576	fun eval_is_polyexp (thmid:string) _
neuper@37950	577	(t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
neuper@37950	578	if is_polyexp arg
neuper@37950	579	then SOME (mk_thmid thmid ""
neuper@38053	580	(Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	581	(thy2ctxt thy)) arg) "",
neuper@37950	582	Trueprop $ (mk_equality (t, HOLogic.true_const)))
neuper@37950	583	else SOME (mk_thmid thmid ""
neuper@38053	584	(Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	585	(thy2ctxt thy)) arg) "",
neuper@37950	586	Trueprop $ (mk_equality (t, HOLogic.false_const)))
neuper@37950	587	\| eval_is_polyexp _ _ _ _ = NONE;
neuper@37950	588
neuper@37950	589	val expand_poly_rat_ =
neuper@37950	590	Rls{id = "expand_poly_rat_", preconds = [],
neuper@37950	591	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	592	erls = append_rls "e_rls-is_polyexp" e_rls
neuper@37950	593	[Calc ("Poly.is'_polyexp", eval_is_polyexp "")
neuper@37950	594	],
neuper@37950	595	srls = Erls,
neuper@37950	596	calc = [],
neuper@37950	597	(asm_thm = [],)
neuper@37950	598	rules =
neuper@37969	599	[Thm ("real_plus_binom_pow4_poly", num_str @{thm real_plus_binom_pow4_poly}),
neuper@37950	600	("[\| a is_polyexp; b is_polyexp \|] ==> (a + b)^^^4 = ... ")
neuper@37969	601	Thm ("real_plus_binom_pow5_poly", num_str @{thm real_plus_binom_pow5_poly}),
neuper@37950	602	("[\| a is_polyexp; b is_polyexp \|] ==> (a + b)^^^5 = ... ")
neuper@37969	603	Thm ("real_plus_binom_pow2_poly",num_str @{thm real_plus_binom_pow2_poly}),
neuper@37950	604	(*"[\| a is_polyexp; b is_polyexp \|] ==>
neuper@37950	605	(a + b)^^^2 = a^^^2 + 2ab + b^^^2"*)
neuper@37969	606	Thm ("real_plus_binom_pow3_poly",num_str @{thm real_plus_binom_pow3_poly}),
neuper@37950	607	(*"[\| a is_polyexp; b is_polyexp \|] ==>
neuper@37950	608	(a + b)^^^3 = a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3" *)
neuper@37969	609	Thm ("real_plus_minus_binom1_p_p",num_str @{thm real_plus_minus_binom1_p_p}),
neuper@37950	610	("(a + b)(a + -1 * b) = a^^^2 + -1b^^^2")
neuper@37969	611	Thm ("real_plus_minus_binom2_p_p",num_str @{thm real_plus_minus_binom2_p_p}),
neuper@37950	612	("(a + -1 b)(a + b) = a^^^2 + -1b^^^2"*)
neuper@37950	613
neuper@37974	614	Thm ("real_add_mult_distrib_poly",
neuper@37974	615	num_str @{thm real_add_mult_distrib_poly}),
neuper@37950	616	("w is_polyexp ==> (z1.0 + z2.0) w = z1.0 * w + z2.0 * w"*)
neuper@37974	617	Thm("real_add_mult_distrib2_poly",
neuper@37974	618	num_str @{thm real_add_mult_distrib2_poly}),
neuper@37950	619	("w is_polyexp ==> w (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950	620
neuper@37969	621	Thm ("realpow_multI_poly", num_str @{thm realpow_multI_poly}),
neuper@37950	622	(*"[\| r is_polyexp; s is_polyexp \|] ==>
neuper@37950	623	(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37969	624	Thm ("realpow_pow",num_str @{thm realpow_pow})
neuper@37950	625	("(a ^^^ b) ^^^ c = a ^^^ (b c)"*)
neuper@37950	626	], scr = EmptyScr}:rls;
neuper@37950	627
neuper@37950	628	val simplify_power_ =
neuper@37950	629	Rls{id = "simplify_power_", preconds = [],
neuper@37950	630	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	631	erls = e_rls, srls = Erls,
neuper@37950	632	calc = [],
neuper@37950	633	(asm_thm = [],)
neuper@37950	634	rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
neuper@37950	635	a(aa) --> aa^^^2 und nicht a(aa) --> a^^^2a *)
neuper@37969	636	Thm ("sym_realpow_twoI",
neuper@37969	637	num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@37950	638	("r r = r ^^^ 2"*)
neuper@37969	639	Thm ("realpow_twoI_assoc_l",num_str @{thm realpow_twoI_assoc_l}),
neuper@37950	640	("r (r * s) = r ^^^ 2 * s"*)
neuper@37950	641
neuper@37969	642	Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
neuper@37950	643	("r r ^^^ n = r ^^^ (n + 1)"*)
neuper@37969	644	Thm ("realpow_plus_1_assoc_l",
neuper@37969	645	num_str @{thm realpow_plus_1_assoc_l}),
neuper@37950	646	("r (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
neuper@37950	647	(MG 9.7.03: neues Thm wegen a(a(ab)) --> a^^^2(ab) *)
neuper@37969	648	Thm ("realpow_plus_1_assoc_l2",
neuper@37969	649	num_str @{thm realpow_plus_1_assoc_l2}),
neuper@37950	650	("r ^^^ m (r * s) = r ^^^ (1 + m) * s"*)
neuper@37950	651
neuper@37969	652	Thm ("sym_realpow_addI",
neuper@37969	653	num_str (@{thm realpow_addI} RS @{thm sym})),
neuper@37950	654	("r ^^^ n r ^^^ m = r ^^^ (n + m)"*)
neuper@37969	655	Thm ("realpow_addI_assoc_l",num_str @{thm realpow_addI_assoc_l}),
neuper@37950	656	("r ^^^ n (r ^^^ m * s) = r ^^^ (n + m) * s"*)
neuper@37950	657
neuper@37950	658	(* ist in expand_poly - wird hier aber auch gebraucht, wegen:
neuper@37950	659	"r * r = r ^^^ 2" wenn r=a^^^b*)
neuper@37969	660	Thm ("realpow_pow",num_str @{thm realpow_pow})
neuper@37950	661	("(a ^^^ b) ^^^ c = a ^^^ (b c)"*)
neuper@37950	662	], scr = EmptyScr}:rls;
neuper@37950	663
neuper@37950	664	val calc_add_mult_pow_ =
neuper@37950	665	Rls{id = "calc_add_mult_pow_", preconds = [],
neuper@37950	666	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	667	erls = Atools_erls(erls3.4.03),srls = Erls,
neuper@38014	668	calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38034	669	("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37950	670	("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950	671	],
neuper@37950	672	(asm_thm = [],)
neuper@38014	673	rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@38034	674	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	675	Calc ("Atools.pow", eval_binop "#power_")
neuper@37950	676	], scr = EmptyScr}:rls;
neuper@37950	677
neuper@37950	678	val reduce_012_mult_ =
neuper@37950	679	Rls{id = "reduce_012_mult_", preconds = [],
neuper@37950	680	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	681	erls = e_rls,srls = Erls,
neuper@37950	682	calc = [],
neuper@37950	683	(asm_thm = [],)
neuper@37950	684	rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
neuper@37965	685	Thm ("mult_1_right",num_str @{thm mult_1_right}),
neuper@37950	686	("z 1 = z") (wegen "a * b * b^^^(-1) + a"*)
neuper@37969	687	Thm ("realpow_zeroI",num_str @{thm realpow_zeroI}),
neuper@37950	688	("r ^^^ 0 = 1") (wegen "aa^^^(-1)c + b + c")
neuper@37969	689	Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
neuper@37950	690	("r ^^^ 1 = r")
neuper@37974	691	Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
neuper@37950	692	("1 ^^^ n = 1")
neuper@37950	693	], scr = EmptyScr}:rls;
neuper@37950	694
neuper@37950	695	val collect_numerals_ =
neuper@37950	696	Rls{id = "collect_numerals_", preconds = [],
neuper@37950	697	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	698	erls = Atools_erls, srls = Erls,
neuper@38014	699	calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
neuper@37950	700	],
neuper@37950	701	rules =
neuper@37969	702	[Thm ("real_num_collect",num_str @{thm real_num_collect}),
neuper@37950	703	("[\| l is_const; m is_const \|]==>l n + m * n = (l + m) * n"*)
neuper@37969	704	Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}),
neuper@37950	705	(*"[\| l is_const; m is_const \|] ==> \
neuper@37950	706	\(k + m * n) + l * n = k + (l + m)n")
neuper@37969	707	Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950	708	("m is_const ==> n + m n = (1 + m) * n"*)
neuper@37969	709	Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}),
neuper@37950	710	("m is_const ==> (k + n) + m n = k + (m + 1) * n"*)
neuper@37950	711
neuper@38014	712	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@37950	713
neuper@37950	714	(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
neuper@37950	715	(a+a)+a --> a + 2a --> 3a and not (a+a)+a --> 2a + a )
neuper@37969	716	Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}),
neuper@37950	717	("(k + z1) + z1 = k + 2 z1"*)
neuper@37969	718	Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym}))
neuper@37950	719	("z1 + z1 = 2 z1"*)
neuper@37950	720	], scr = EmptyScr}:rls;
neuper@37950	721
neuper@37950	722	val reduce_012_ =
neuper@37950	723	Rls{id = "reduce_012_", preconds = [],
neuper@37950	724	rew_ord = ("dummy_ord", dummy_ord),
neuper@37974	725	erls = e_rls,srls = Erls, calc = [],
neuper@37965	726	rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
neuper@37950	727	("1 z = z"*)
neuper@37965	728	Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
neuper@37950	729	("0 z = 0"*)
neuper@37974	730	Thm ("mult_zero_right",num_str @{thm mult_zero_right}),
neuper@37950	731	("z 0 = 0"*)
neuper@37965	732	Thm ("add_0_left",num_str @{thm add_0_left}),
neuper@37950	733	("0 + z = z")
neuper@37965	734	Thm ("add_0_right",num_str @{thm add_0_right}),
neuper@37950	735	("z + 0 = z") (wegen a+b-b --> a+(1-1)b --> a+0 --> a*)
neuper@37950	736
neuper@37969	737	(Thm ("realpow_oneI",num_str @{thm realpow_oneI}))
neuper@37950	738	("?r ^^^ 1 = ?r")
neuper@37965	739	Thm ("divide_zero_left",num_str @{thm divide_zero_left})(WN060914)
neuper@37950	740	("0 / ?x = 0")
neuper@37950	741	], scr = EmptyScr}:rls;
neuper@37950	742
neuper@37950	743	(ein Hilfs-'ruleset' (benutzt das leere 'ruleset'))
neuper@37979	744	val discard_parentheses1 =
neuper@37979	745	append_rls "discard_parentheses1" e_rls
neuper@37969	746	[Thm ("sym_real_mult_assoc",
neuper@37969	747	num_str (@{thm real_mult_assoc} RS @{thm sym}))
neuper@37950	748	("?z1.1 (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
neuper@37974	749	(*Thm ("sym_add_assoc",
neuper@37974	750	num_str (@{thm add_assoc} RS @{thm sym}))*)
neuper@37950	751	("?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1")
neuper@37950	752	];
neuper@37950	753
neuper@37950	754	(----------------- End: rulesets for make_polynomial_ -----------------)
neuper@37950	755
neuper@37950	756	(*MG.0401 ev. for use in rls with ordered rewriting ?
neuper@37950	757	val collect_numerals_left =
neuper@37950	758	Rls{id = "collect_numerals", preconds = [],
neuper@37950	759	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	760	erls = Atools_erls(erls3.4.03),srls = Erls,
neuper@38014	761	calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38034	762	("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37950	763	("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950	764	],
neuper@37950	765	(asm_thm = [],)
neuper@37969	766	rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}),
neuper@37950	767	("[\| l is_const; m is_const \|]==>l n + m * n = (l + m) * n"*)
neuper@37969	768	Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
neuper@37950	769	(*"[\| l is_const; m is_const \|] ==>
neuper@37950	770	l * n + (m * n + k) = (l + m) * n + k"*)
neuper@37969	771	Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950	772	("m is_const ==> n + m n = (1 + m) * n"*)
neuper@37969	773	Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
neuper@37950	774	("m is_const ==> n + (m n + k) = (1 + m) * n + k"*)
neuper@37950	775
neuper@38014	776	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@37950	777
neuper@37950	778	(MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben)
neuper@37969	779	Thm ("sym_real_mult_2",
neuper@37969	780	num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@37950	781	("z1 + z1 = 2 z1"*)
neuper@37969	782	Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
neuper@37950	783	("z1 + (z1 + k) = 2 z1 + k"*)
neuper@37950	784	], scr = EmptyScr}:rls;*)
neuper@37950	785
neuper@37950	786	val expand_poly =
neuper@37950	787	Rls{id = "expand_poly", preconds = [],
neuper@37950	788	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	789	erls = e_rls,srls = Erls,
neuper@37950	790	calc = [],
neuper@37950	791	(asm_thm = [],)
neuper@37965	792	rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950	793	("(z1.0 + z2.0) w = z1.0 * w + z2.0 * w"*)
neuper@37974	794	Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950	795	("w (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37965	796	(*Thm ("left_distrib1",num_str @{thm left_distrib}1),
neuper@37950	797	....... 18.3.03 undefined???*)
neuper@37950	798
neuper@37969	799	Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
neuper@37950	800	("(a + b)^^^2 = a^^^2 + 2ab + b^^^2")
neuper@37969	801	Thm ("real_minus_binom_pow2_p",num_str @{thm real_minus_binom_pow2_p}),
neuper@37950	802	("(a - b)^^^2 = a^^^2 + -2ab + b^^^2")
neuper@37950	803	Thm ("real_plus_minus_binom1_p",
neuper@37969	804	num_str @{thm real_plus_minus_binom1_p}),
neuper@37950	805	("(a + b)(a - b) = a^^^2 + -1b^^^2")
neuper@37950	806	Thm ("real_plus_minus_binom2_p",
neuper@37969	807	num_str @{thm real_plus_minus_binom2_p}),
neuper@37950	808	("(a - b)(a + b) = a^^^2 + -1b^^^2")
neuper@37950	809
neuper@37965	810	Thm ("minus_minus",num_str @{thm minus_minus}),
neuper@37950	811	("- (- ?z) = ?z")
neuper@37969	812	Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
neuper@37950	813	("a - b = a + -1 b"*)
neuper@37969	814	Thm ("sym_real_mult_minus1",
neuper@37969	815	num_str (@{thm real_mult_minus1} RS @{thm sym}))
neuper@37950	816	(- ?z = "-1 ?z"*)
neuper@37950	817
neuper@37950	818	(*Thm ("real_minus_add_distrib",
neuper@37969	819	num_str @{thm real_minus_add_distrib}),*)
neuper@37950	820	("- (?x + ?y) = - ?x + - ?y")
neuper@37969	821	(Thm ("real_diff_plus",num_str @{thm real_diff_plus}))
neuper@37950	822	("a - b = a + -b")
neuper@37950	823	], scr = EmptyScr}:rls;
neuper@37950	824
neuper@37950	825	val simplify_power =
neuper@37950	826	Rls{id = "simplify_power", preconds = [],
neuper@37950	827	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	828	erls = e_rls, srls = Erls,
neuper@37950	829	calc = [],
neuper@37950	830	(asm_thm = [],)
neuper@37969	831	rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),
neuper@37950	832	("(r s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37950	833
neuper@37969	834	Thm ("sym_realpow_twoI",
neuper@37969	835	num_str( @{thm realpow_twoI} RS @{thm sym})),
neuper@37950	836	("r1 r1 = r1 ^^^ 2"*)
neuper@37969	837	Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
neuper@37950	838	("r r ^^^ n = r ^^^ (n + 1)"*)
neuper@37969	839	Thm ("realpow_pow",num_str @{thm realpow_pow}),
neuper@37950	840	("(a ^^^ b) ^^^ c = a ^^^ (b c)"*)
neuper@37969	841	Thm ("sym_realpow_addI",
neuper@37969	842	num_str (@{thm realpow_addI} RS @{thm sym})),
neuper@37950	843	("r ^^^ n r ^^^ m = r ^^^ (n + m)"*)
neuper@37969	844	Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
neuper@37950	845	("r ^^^ 1 = r")
neuper@37969	846	Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
neuper@37950	847	("1 ^^^ n = 1")
neuper@37950	848	], scr = EmptyScr}:rls;
neuper@37950	849	(*MG.0401: termorders for multivariate polys dropped due to principal problems:
neuper@37950	850	(total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
neuper@37950	851	val order_add_mult =
neuper@37950	852	Rls{id = "order_add_mult", preconds = [],
neuper@37972	853	rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
neuper@37950	854	erls = e_rls,srls = Erls,
neuper@37950	855	calc = [],
neuper@37950	856	(asm_thm = [],)
neuper@37969	857	rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37950	858	(* z * w = w * z *)
neuper@37969	859	Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
neuper@37950	860	(z1.0 (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37969	861	Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
neuper@37950	862	(z1.0 z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37965	863	Thm ("add_commute",num_str @{thm add_commute}),
neuper@37950	864	(z + w = w + z)
neuper@37965	865	Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37950	866	(x + (y + z) = y + (x + z))
neuper@37965	867	Thm ("add_assoc",num_str @{thm add_assoc})
neuper@37950	868	(z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0))
neuper@37950	869	], scr = EmptyScr}:rls;
neuper@37950	870	(*MG.0401: termorders for multivariate polys dropped due to principal problems:
neuper@37950	871	(total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
neuper@37950	872	val order_mult =
neuper@37950	873	Rls{id = "order_mult", preconds = [],
neuper@37972	874	rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
neuper@37950	875	erls = e_rls,srls = Erls,
neuper@37950	876	calc = [],
neuper@37950	877	(asm_thm = [],)
neuper@37969	878	rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37950	879	(* z * w = w * z *)
neuper@37969	880	Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
neuper@37950	881	(z1.0 (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37969	882	Thm ("real_mult_assoc",num_str @{thm real_mult_assoc})
neuper@37950	883	(z1.0 z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37950	884	], scr = EmptyScr}:rls;
neuper@37950	885	val collect_numerals =
neuper@37950	886	Rls{id = "collect_numerals", preconds = [],
neuper@37950	887	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	888	erls = Atools_erls(erls3.4.03),srls = Erls,
neuper@38014	889	calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38034	890	("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37950	891	("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950	892	],
neuper@37950	893	(asm_thm = [],)
neuper@37969	894	rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}),
neuper@37950	895	("[\| l is_const; m is_const \|]==>l n + m * n = (l + m) * n"*)
neuper@37969	896	Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
neuper@37950	897	(*"[\| l is_const; m is_const \|] ==>
neuper@37950	898	l * n + (m * n + k) = (l + m) * n + k"*)
neuper@37969	899	Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950	900	("m is_const ==> n + m n = (1 + m) * n"*)
neuper@37969	901	Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
neuper@37950	902	("m is_const ==> k + (n + m n) = k + (1 + m) * n"*)
neuper@38014	903	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@38034	904	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	905	Calc ("Atools.pow", eval_binop "#power_")
neuper@37950	906	], scr = EmptyScr}:rls;
neuper@37950	907	val reduce_012 =
neuper@37950	908	Rls{id = "reduce_012", preconds = [],
neuper@37950	909	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	910	erls = e_rls,srls = Erls,
neuper@37950	911	calc = [],
neuper@37950	912	(asm_thm = [],)
neuper@37965	913	rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
neuper@37950	914	("1 z = z"*)
neuper@37969	915	(Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),14.3.03)
neuper@37950	916	("-1 z = - z"*)
neuper@37965	917	Thm ("minus_mult_left",
neuper@37974	918	num_str (@{thm minus_mult_left} RS @{thm sym})),
neuper@37950	919	(- (?x ?y) = "- ?x * ?y"*)
neuper@37969	920	(*Thm ("real_minus_mult_cancel",
neuper@37969	921	num_str @{thm real_minus_mult_cancel}),
neuper@37950	922	("- ?x - ?y = ?x * ?y")---)
neuper@37965	923	Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
neuper@37950	924	("0 z = 0"*)
neuper@37965	925	Thm ("add_0_left",num_str @{thm add_0_left}),
neuper@37950	926	("0 + z = z")
neuper@37965	927	Thm ("right_minus",num_str @{thm right_minus}),
neuper@37950	928	("?z + - ?z = 0")
neuper@37969	929	Thm ("sym_real_mult_2",
neuper@37969	930	num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@37950	931	("z1 + z1 = 2 z1"*)
neuper@37969	932	Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
neuper@37950	933	("z1 + (z1 + k) = 2 z1 + k"*)
neuper@37950	934	], scr = EmptyScr}:rls;
neuper@37950	935	(ein Hilfs-'ruleset' (benutzt das leere 'ruleset'))
neuper@37950	936	val discard_parentheses =
neuper@37950	937	append_rls "discard_parentheses" e_rls
neuper@37969	938	[Thm ("sym_real_mult_assoc",
neuper@37969	939	num_str (@{thm real_mult_assoc} RS @{thm sym})),
neuper@37974	940	Thm ("sym_add_assoc",
neuper@37974	941	num_str (@{thm add_assoc} RS @{thm sym}))];
neuper@37950	942
neuper@37950	943	val scr_make_polynomial =
neuper@37976	944	"Script Expand_binoms t_t = " ^
neuper@37950	945	"(Repeat " ^
neuper@37950	946	"((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
neuper@37950	947
neuper@37971	948	" (Try (Repeat (Rewrite left_distrib False))) @@ " ^
neuper@37971	949	" (Try (Repeat (Rewrite right_distrib False))) @@ " ^
neuper@37971	950	" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
neuper@37971	951	" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
neuper@37950	952
neuper@37971	953	" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
neuper@37971	954	" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
neuper@37971	955	" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
neuper@37950	956
neuper@37950	957	" (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
neuper@37950	958	" (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
neuper@37950	959	" (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
neuper@37971	960	" (Try (Repeat (Rewrite add_commute False))) @@ " ^
neuper@37971	961	" (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
neuper@37971	962	" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
neuper@37950	963
neuper@37950	964	" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
neuper@37950	965	" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
neuper@37950	966	" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
neuper@37950	967	" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
neuper@37950	968
neuper@37950	969	" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
neuper@37950	970	" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
neuper@37950	971
neuper@37950	972	" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
neuper@37950	973	" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
neuper@37950	974
neuper@37975	975	" (Try (Repeat (Calculate PLUS ))) @@ " ^
neuper@37975	976	" (Try (Repeat (Calculate TIMES ))) @@ " ^
neuper@37975	977	" (Try (Repeat (Calculate POWER)))) " ^
neuper@37976	978	" t_t)";
neuper@37950	979
neuper@37950	980	(*version used by MG.02/03, overwritten by version AG in 04 below
neuper@37950	981	val make_polynomial = prep_rls(
neuper@37950	982	Seq{id = "make_polynomial", preconds = []:term list,
neuper@37950	983	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	984	erls = Atools_erls, srls = Erls,
neuper@37950	985	calc = [],(asm_thm = [],)
neuper@37950	986	rules = [Rls_ expand_poly,
neuper@37950	987	Rls_ order_add_mult,
neuper@37950	988	Rls_ simplify_power, (realpow_eq_oneI, eg. x^1 --> x )
neuper@37950	989	Rls_ collect_numerals, (eg. x^(2+ -1) --> x^1 )
neuper@37950	990	Rls_ reduce_012,
neuper@37969	991	Thm ("realpow_oneI",num_str @{thm realpow_oneI}),(in --^)
neuper@37950	992	Rls_ discard_parentheses
neuper@37950	993	],
neuper@37950	994	scr = EmptyScr
neuper@37950	995	}:rls); *)
neuper@37950	996
neuper@37950	997	val scr_expand_binoms =
neuper@37974	998	"Script Expand_binoms t_t =" ^
neuper@37950	999	"(Repeat " ^
neuper@37950	1000	"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
neuper@37950	1001	" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
neuper@37950	1002	" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
neuper@37950	1003	" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
neuper@37950	1004	" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
neuper@37950	1005	" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
neuper@37950	1006
neuper@37971	1007	" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
neuper@37971	1008	" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
neuper@37971	1009	" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
neuper@37950	1010
neuper@37975	1011	" (Try (Repeat (Calculate PLUS ))) @@ " ^
neuper@37975	1012	" (Try (Repeat (Calculate TIMES ))) @@ " ^
neuper@37975	1013	" (Try (Repeat (Calculate POWER))) @@ " ^
neuper@37950	1014
neuper@37950	1015	" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
neuper@37950	1016	" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
neuper@37950	1017	" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
neuper@37950	1018	" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
neuper@37950	1019
neuper@37950	1020	" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
neuper@37950	1021	" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
neuper@37950	1022
neuper@37950	1023	" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
neuper@37950	1024	" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
neuper@37950	1025
neuper@37975	1026	" (Try (Repeat (Calculate PLUS ))) @@ " ^
neuper@37975	1027	" (Try (Repeat (Calculate TIMES ))) @@ " ^
neuper@37975	1028	" (Try (Repeat (Calculate POWER)))) " ^
neuper@37974	1029	" t_t)";
neuper@37974	1030
neuper@37950	1031	val expand_binoms =
neuper@37950	1032	Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
neuper@37950	1033	erls = Atools_erls, srls = Erls,
neuper@38014	1034	calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38034	1035	("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37950	1036	("POWER", ("Atools.pow", eval_binop "#power_"))
neuper@37950	1037	],
neuper@37974	1038	rules = [Thm ("real_plus_binom_pow2",
neuper@37974	1039	num_str @{thm real_plus_binom_pow2}),
neuper@37950	1040	("(a + b) ^^^ 2 = a ^^^ 2 + 2 a * b + b ^^^ 2"*)
neuper@37974	1041	Thm ("real_plus_binom_times",
neuper@37974	1042	num_str @{thm real_plus_binom_times}),
neuper@37950	1043	("(a + b)(a + b) = ...*)
neuper@37974	1044	Thm ("real_minus_binom_pow2",
neuper@37974	1045	num_str @{thm real_minus_binom_pow2}),
neuper@37950	1046	("(a - b) ^^^ 2 = a ^^^ 2 - 2 a * b + b ^^^ 2"*)
neuper@37974	1047	Thm ("real_minus_binom_times",
neuper@37974	1048	num_str @{thm real_minus_binom_times}),
neuper@37950	1049	("(a - b)(a - b) = ...*)
neuper@37974	1050	Thm ("real_plus_minus_binom1",
neuper@37974	1051	num_str @{thm real_plus_minus_binom1}),
neuper@37950	1052	("(a + b) (a - b) = a ^^^ 2 - b ^^^ 2"*)
neuper@37974	1053	Thm ("real_plus_minus_binom2",
neuper@37974	1054	num_str @{thm real_plus_minus_binom2}),
neuper@37950	1055	("(a - b) (a + b) = a ^^^ 2 - b ^^^ 2"*)
neuper@37950	1056	(RL 020915)
neuper@37969	1057	Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
neuper@37950	1058	((a + b)(c + d) = ac + ad + bc + bd*)
neuper@37969	1059	Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
neuper@37950	1060	((a + b)(c - d) = ac - ad + bc - bd*)
neuper@37969	1061	Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
neuper@37950	1062	((a - b)(c + d) = ac + ad - bc - bd*)
neuper@37969	1063	Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
neuper@37950	1064	((a - b)(c - d) = ac - ad - bc + bd*)
neuper@37974	1065	Thm ("realpow_multI",num_str @{thm realpow_multI}),
neuper@37950	1066	((ab)^^^n = a^^^n * b^^^n*)
neuper@37969	1067	Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
neuper@37950	1068	(* (a + b)^^^3 = a^^^3 + 3a^^^2b + 3ab^^^2 + b^^^3 *)
neuper@37974	1069	Thm ("real_minus_binom_pow3",
neuper@37974	1070	num_str @{thm real_minus_binom_pow3}),
neuper@37950	1071	(* (a - b)^^^3 = a^^^3 - 3a^^^2b + 3ab^^^2 - b^^^3 *)
neuper@37950	1072
neuper@37950	1073
neuper@37974	1074	(*Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950	1075	("(z1.0 + z2.0) w = z1.0 * w + z2.0 * w"*)
neuper@37974	1076	Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950	1077	("w (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37965	1078	Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
neuper@37950	1079	("(z1.0 - z2.0) w = z1.0 * w - z2.0 * w"*)
neuper@37982	1080	Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
neuper@37950	1081	("w (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
neuper@37974	1082	*)
neuper@37974	1083	Thm ("mult_1_left",num_str @{thm mult_1_left}),
neuper@37974	1084	("1 z = z"*)
neuper@37974	1085	Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
neuper@37974	1086	("0 z = 0"*)
neuper@37965	1087	Thm ("add_0_left",num_str @{thm add_0_left}),("0 + z = z")
neuper@37950	1088
neuper@38014	1089	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@38034	1090	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1091	Calc ("Atools.pow", eval_binop "#power_"),
neuper@37974	1092	(*Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
neuper@37974	1093	(AC-rewriting)
neuper@37974	1094	Thm ("real_mult_left_commute",
neuper@37974	1095	num_str @{thm real_mult_left_commute}),
neuper@37974	1096	Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
neuper@37974	1097	Thm ("add_commute",num_str @{thm add_commute}),
neuper@37974	1098	Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37974	1099	Thm ("add_assoc",num_str @{thm add_assoc}),
neuper@37974	1100	*)
neuper@37969	1101	Thm ("sym_realpow_twoI",
neuper@37969	1102	num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@37950	1103	("r1 r1 = r1 ^^^ 2"*)
neuper@37969	1104	Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
neuper@37950	1105	("r r ^^^ n = r ^^^ (n + 1)"*)
neuper@37974	1106	(*Thm ("sym_real_mult_2",
neuper@37974	1107	num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@37950	1108	("z1 + z1 = 2 z1"))
neuper@37969	1109	Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
neuper@37950	1110	("z1 + (z1 + k) = 2 z1 + k"*)
neuper@37950	1111
neuper@37969	1112	Thm ("real_num_collect",num_str @{thm real_num_collect}),
neuper@37974	1113	("[\| l is_const; m is_const \|] ==>l n + m * n = (l + m) * n"*)
neuper@37974	1114	Thm ("real_num_collect_assoc",
neuper@37974	1115	num_str @{thm real_num_collect_assoc}),
neuper@37974	1116	(*"[\| l is_const; m is_const \|] ==>
neuper@37974	1117	l * n + (m * n + k) = (l + m) * n + k"*)
neuper@37974	1118	Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950	1119	("m is_const ==> n + m n = (1 + m) * n"*)
neuper@37974	1120	Thm ("real_one_collect_assoc",
neuper@37974	1121	num_str @{thm real_one_collect_assoc}),
neuper@37950	1122	("m is_const ==> k + (n + m n) = k + (1 + m) * n"*)
neuper@37950	1123
neuper@38014	1124	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@38034	1125	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1126	Calc ("Atools.pow", eval_binop "#power_")
neuper@37950	1127	],
neuper@37950	1128	scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
neuper@37950	1129	}:rls;
neuper@37950	1130
neuper@37950	1131
neuper@37950	1132	(. MG.03: make_polynomial_ ... uses SML-fun for ordering .)
neuper@37950	1133
neuper@37950	1134	(FIXME.0401: make SML-order local to make_polynomial(_) )
neuper@37950	1135	(FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) )
neuper@37950	1136	(* Polynom --> List von Monomen *)
neuper@38014	1137	fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
neuper@37950	1138	(poly2list t1) @ (poly2list t2)
neuper@37950	1139	\| poly2list t = [t];
neuper@37950	1140
neuper@37950	1141	(* Monom --> Liste von Variablen *)
neuper@38034	1142	fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
neuper@37950	1143	(monom2list t1) @ (monom2list t2)
neuper@37950	1144	\| monom2list t = [t];
neuper@37950	1145
neuper@37950	1146	(* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
neuper@37950	1147	fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
neuper@37950	1148	\| get_basStr (Free (str, _)) = str
neuper@37950	1149	\| get_basStr t = "\|\|\|"; (* gross gewichtet; für Brüch ect. *)
neuper@37950	1150	(*\| get_basStr t =
neuper@38031	1151	error("get_basStr: called with t= "^(term2str t));*)
neuper@37950	1152
neuper@37950	1153	(* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
neuper@37950	1154	fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
neuper@37950	1155	\| get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "\|\|\|" (* gross gewichtet *)
neuper@37950	1156	\| get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
neuper@37950	1157	\| get_potStr t = "\|\|\|\|\|\|"; (* gross gewichtet; für Brüch ect. *)
neuper@37950	1158	(*\| get_potStr t =
neuper@38031	1159	error("get_potStr: called with t= "^(term2str t));*)
neuper@37950	1160
neuper@37950	1161	(* Umgekehrte string_ord *)
neuper@37950	1162	val string_ord_rev = rev_order o string_ord;
neuper@37950	1163
neuper@37950	1164	(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
neuper@37950	1165	innerhalb eines Monomes:
neuper@37950	1166	- zuerst lexikographisch nach Variablenname
neuper@37950	1167	- wenn gleich: nach steigender Potenz *)
neuper@37950	1168	fun var_ord (a,b: term) = prod_ord string_ord string_ord
neuper@37950	1169	((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
neuper@37950	1170
neuper@37950	1171	(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
neuper@37950	1172	verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
neuper@37950	1173	- zuerst lexikographisch nach Variablenname
neuper@37950	1174	- wenn gleich: nach sinkender Potenz*)
neuper@37950	1175	fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
neuper@37950	1176	((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
neuper@37950	1177
neuper@37950	1178
neuper@37950	1179	(* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
neuper@37950	1180	val sort_varList = sort var_ord;
neuper@37950	1181
neuper@37950	1182	(* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
neuper@37950	1183	Argumente in eine Liste *)
neuper@37950	1184	fun args u : term list =
neuper@37950	1185	let fun stripc (f$t, ts) = stripc (f, t::ts)
neuper@37950	1186	\| stripc (t as Free _, ts) = (t::ts)
neuper@37950	1187	\| stripc (_, ts) = ts
neuper@37950	1188	in stripc (u, []) end;
neuper@37950	1189
neuper@37950	1190	(* liefert True, falls der Term (Liste von Termen) nur Zahlen
neuper@37950	1191	(keine Variablen) enthaelt *)
neuper@37950	1192	fun filter_num [] = true
neuper@37950	1193	\| filter_num [Free x] = if (is_num (Free x)) then true
neuper@37950	1194	else false
neuper@37950	1195	\| filter_num ((Free _)::_) = false
neuper@37950	1196	\| filter_num ts =
neuper@37950	1197	(filter_num o (filter_out is_num) o flat o (map args)) ts;
neuper@37950	1198
neuper@37950	1199	(* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
neuper@37950	1200	dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
neuper@37950	1201	fun is_nums t = filter_num [t];
neuper@37950	1202
neuper@37950	1203	(* Berechnet den Gesamtgrad eines Monoms *)
neuper@37950	1204	local
neuper@37950	1205	fun counter (n, []) = n
neuper@37950	1206	\| counter (n, x :: xs) =
neuper@37950	1207	if (is_nums x) then
neuper@37950	1208	counter (n, xs)
neuper@37950	1209	else
neuper@37950	1210	(case x of
neuper@37950	1211	(Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
neuper@37950	1212	if (is_nums (Free (str_h, T))) then
neuper@37950	1213	counter (n + (the (int_of_str str_h)), xs)
neuper@37950	1214	else counter (n + 1000, xs) (FIXME.MG?!)
neuper@37950	1215	\| (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
neuper@37950	1216	counter (n + 1000, xs) (FIXME.MG?!)
neuper@37950	1217	\| (Free (str, _)) => counter (n + 1, xs)
neuper@38031	1218	(\| _ => error("monom_degree: called with factor: "^(term2str x))))
neuper@37950	1219	\| _ => counter (n + 10000, xs)) (FIXME.MG?! ... Brüche ect.)
neuper@37950	1220	in
neuper@37950	1221	fun monom_degree l = counter (0, l)
neuper@37980	1222	end;(local)
neuper@37950	1223
neuper@37950	1224	(* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
neuper@37950	1225	der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
neuper@37950	1226	werden jedoch dabei ignoriert (uebersprungen) *)
neuper@37950	1227	fun dict_cond_ord _ _ ([], []) = EQUAL
neuper@37950	1228	\| dict_cond_ord _ _ ([], _ :: _) = LESS
neuper@37950	1229	\| dict_cond_ord _ _ (_ :: _, []) = GREATER
neuper@37950	1230	\| dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
neuper@37950	1231	(case (cond x, cond y) of
neuper@37950	1232	(false, false) => (case elem_ord (x, y) of
neuper@37950	1233	EQUAL => dict_cond_ord elem_ord cond (xs, ys)
neuper@37950	1234	\| ord => ord)
neuper@37950	1235	\| (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
neuper@37950	1236	\| (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
neuper@37950	1237	\| (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
neuper@37950	1238
neuper@37950	1239	(* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
neuper@37950	1240	zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
neuper@37950	1241	dabei werden Koeffizienten ignoriert (23a^^^24b gilt wie a^^^2b) )
neuper@37950	1242	fun degree_ord (xs, ys) =
neuper@37950	1243	prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
neuper@37950	1244	((monom_degree xs, xs), (monom_degree ys, ys));
neuper@37950	1245
neuper@37950	1246	fun hd_str str = substring (str, 0, 1);
neuper@37950	1247	fun tl_str str = substring (str, 1, (size str) - 1);
neuper@37950	1248
neuper@37950	1249	(* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
neuper@38031	1250	fun get_koeff_of_mon [] = error("get_koeff_of_mon: called with l = []")
neuper@37950	1251	\| get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
neuper@37950	1252	else NONE;
neuper@37950	1253
neuper@37950	1254	(* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
neuper@37950	1255	fun koeff2ordStr (SOME x) = (case x of
neuper@37950	1256	(Free (str, T)) =>
neuper@37950	1257	if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
neuper@37950	1258	else str
neuper@37950	1259	\| _ => "aaa") (* "num.Ausdruck" --> gross *)
neuper@37950	1260	\| koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
neuper@37950	1261
neuper@37950	1262	(* Order zum Vergleich von Koeffizienten (strings):
neuper@37950	1263	"kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
neuper@37950	1264	fun compare_koeff_ord (xs, ys) =
neuper@37950	1265	string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
neuper@37950	1266	(koeff2ordStr o get_koeff_of_mon) ys);
neuper@37950	1267
neuper@37950	1268	(* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
neuper@37950	1269	fun koeff_degree_ord (xs, ys) =
neuper@37950	1270	prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
neuper@37950	1271
neuper@37950	1272	(* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
neuper@37950	1273	Gesamtgradordnung *)
neuper@37950	1274	val sort_monList = sort koeff_degree_ord;
neuper@37950	1275
neuper@37950	1276	(* Alternativ zu degree_ord koennte auch die viel einfachere und
neuper@37950	1277	kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
neuper@37950	1278	fuer unsere Zwecke geeignet!
neuper@37950	1279
neuper@37950	1280	fun simple_ord (al,bl: term list) = dict_ord string_ord
neuper@37950	1281	(map get_basStr al, map get_basStr bl);
neuper@37950	1282
neuper@37950	1283	val sort_monList = sort simple_ord; *)
neuper@37950	1284
neuper@37950	1285	(* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
neuper@37950	1286	(mit gewuenschtem Typen T) *)
neuper@38014	1287	fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
neuper@38034	1288	fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
neuper@37950	1289	fun binop op_ t1 t2 = op_ $ t1 $ t2;
neuper@37950	1290	fun create_prod T (a,b) = binop (mult T) a b;
neuper@37950	1291	fun create_sum T (a,b) = binop (plus T) a b;
neuper@37950	1292
neuper@37950	1293	(* löscht letztes Element einer Liste *)
neuper@37950	1294	fun drop_last l = take ((length l)-1,l);
neuper@37950	1295
neuper@37950	1296	(* Liste von Variablen --> Monom *)
neuper@37950	1297	fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
neuper@37950	1298	(* Bemerkung:
neuper@37950	1299	foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
neuper@37950	1300	gleiche Monome zusammengefasst werden können (collect_numerals)!
neuper@37950	1301	zB: 2(x(yz)) + 3(x(yz)) --> (2+3)(x(yz)))
neuper@37950	1302
neuper@37950	1303	(* Liste von Monomen --> Polynom *)
neuper@37950	1304	fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
neuper@37950	1305	(* Bemerkung:
neuper@37950	1306	foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
neuper@37950	1307	bessere Darstellung, da keine Klammern sichtbar!
neuper@37950	1308	(und discard_parentheses in make_polynomial hat weniger zu tun) *)
neuper@37950	1309
neuper@37950	1310	(* sorts the variables (faktors) of an expanded polynomial lexicographical *)
neuper@37950	1311	fun sort_variables t =
neuper@37950	1312	let
neuper@37950	1313	val ll = map monom2list (poly2list t);
neuper@37950	1314	val lls = map sort_varList ll;
neuper@37950	1315	val T = type_of t;
neuper@37950	1316	val ls = map (create_monom T) lls;
neuper@37950	1317	in create_polynom T ls end;
neuper@37950	1318
neuper@37950	1319	(* sorts the monoms of an expanded and variable-sorted polynomial
neuper@37950	1320	by total_degree *)
neuper@37950	1321	fun sort_monoms t =
neuper@37950	1322	let
neuper@37950	1323	val ll = map monom2list (poly2list t);
neuper@37950	1324	val lls = sort_monList ll;
neuper@37950	1325	val T = type_of t;
neuper@37950	1326	val ls = map (create_monom T) lls;
neuper@37950	1327	in create_polynom T ls end;
neuper@37950	1328
neuper@37950	1329	(* auch Klammerung muss übereinstimmen;
neuper@37950	1330	sort_variables klammert Produkte rechtslastig*)
neuper@37950	1331	fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
neuper@37950	1332
neuper@37950	1333	fun eval_is_multUnordered (thmid:string) _
neuper@37950	1334	(t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
neuper@37950	1335	if is_multUnordered arg
neuper@37950	1336	then SOME (mk_thmid thmid ""
neuper@38053	1337	(Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	1338	(thy2ctxt thy)) arg) "",
neuper@37950	1339	Trueprop $ (mk_equality (t, HOLogic.true_const)))
neuper@37950	1340	else SOME (mk_thmid thmid ""
neuper@38053	1341	(Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	1342	(thy2ctxt thy)) arg) "",
neuper@37950	1343	Trueprop $ (mk_equality (t, HOLogic.false_const)))
neuper@37950	1344	\| eval_is_multUnordered _ _ _ _ = NONE;
neuper@37950	1345
neuper@37950	1346
neuper@37950	1347	fun attach_form (_:rule list list) (_:term) (_:term) = (still missing)
neuper@37950	1348	[]:(rule * (term * term list)) list;
neuper@37950	1349	fun init_state (_:term) = e_rrlsstate;
neuper@37950	1350	fun locate_rule (_:rule list list) (_:term) (_:rule) =
neuper@37950	1351	([]:(rule * (term * term list)) list);
neuper@37950	1352	fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
neuper@37950	1353	fun normal_form t = SOME (sort_variables t,[]:term list);
neuper@37950	1354
neuper@37950	1355	val order_mult_ =
neuper@37950	1356	Rrls {id = "order_mult_",
neuper@37950	1357	prepat =
neuper@38036	1358	(* ?p matched with the current term gives an environment,
neuper@38037	1359	which evaluates (the instantiated) "?p is_multUnordered" to true *)
neuper@38037	1360	[([parse_patt thy "?p is_multUnordered"],
neuper@38037	1361	parse_patt thy "?p :: real")],
neuper@37950	1362	rew_ord = ("dummy_ord", dummy_ord),
neuper@38037	1363	erls = append_rls "e_rls-is_multUnordered" e_rls
neuper@37976	1364	[Calc ("Poly.is'_multUnordered",
neuper@37976	1365	eval_is_multUnordered "")],
neuper@38036	1366	calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38036	1367	("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@38036	1368	("DIVIDE", ("Rings.inverse_class.divide",
neuper@38036	1369	eval_cancel "#divide_e")),
neuper@37976	1370	("POWER" , ("Atools.pow", eval_binop "#power_"))],
neuper@37950	1371	scr=Rfuns {init_state = init_state,
neuper@37950	1372	normal_form = normal_form,
neuper@37950	1373	locate_rule = locate_rule,
neuper@37950	1374	next_rule = next_rule,
neuper@37950	1375	attach_form = attach_form}};
neuper@37950	1376	val order_mult_rls_ =
neuper@37950	1377	Rls{id = "order_mult_rls_", preconds = [],
neuper@37950	1378	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	1379	erls = e_rls,srls = Erls,
neuper@37950	1380	calc = [],
neuper@37950	1381	rules = [Rls_ order_mult_
neuper@37950	1382	], scr = EmptyScr}:rls;
neuper@37950	1383
neuper@37950	1384	fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
neuper@37950	1385
neuper@37950	1386	(WN.18.6.03 )
neuper@37950	1387	(("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered "")))
neuper@37950	1388	fun eval_is_addUnordered (thmid:string) _
neuper@37950	1389	(t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
neuper@37950	1390	if is_addUnordered arg
neuper@37950	1391	then SOME (mk_thmid thmid ""
neuper@38053	1392	(Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	1393	(thy2ctxt thy)) arg) "",
neuper@37950	1394	Trueprop $ (mk_equality (t, HOLogic.true_const)))
neuper@37950	1395	else SOME (mk_thmid thmid ""
neuper@38053	1396	(Print_Mode.setmp [] (Syntax.string_of_term
neuper@38053	1397	(thy2ctxt thy)) arg) "",
neuper@37950	1398	Trueprop $ (mk_equality (t, HOLogic.false_const)))
neuper@37950	1399	\| eval_is_addUnordered _ _ _ _ = NONE;
neuper@37950	1400
neuper@37950	1401	fun attach_form (_:rule list list) (_:term) (_:term) = (still missing)
neuper@37950	1402	[]:(rule * (term * term list)) list;
neuper@37950	1403	fun init_state (_:term) = e_rrlsstate;
neuper@37950	1404	fun locate_rule (_:rule list list) (_:term) (_:rule) =
neuper@37950	1405	([]:(rule * (term * term list)) list);
neuper@37950	1406	fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
neuper@37950	1407	fun normal_form t = SOME (sort_monoms t,[]:term list);
neuper@37950	1408
neuper@37950	1409	val order_add_ =
neuper@37950	1410	Rrls {id = "order_add_",
neuper@37950	1411	prepat = (*WN.18.6.03 Preconditions und Pattern,
neuper@37950	1412	die beide passen muessen, damit das Rrls angewandt wird*)
neuper@38037	1413	[([parse_patt @{theory} "?p is_addUnordered"],
neuper@38037	1414	parse_patt @{theory} "?p :: real"
neuper@37950	1415	(*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
neuper@37950	1416	fuer die Evaluation der Precondition "p is_addUnordered"*))],
neuper@37950	1417	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	1418	erls = append_rls "e_rls-is_addUnordered" e_rls(MG: poly_erls)
neuper@38037	1419	[Calc ("Poly.is'_addUnordered",
neuper@38037	1420	eval_is_addUnordered "")],
neuper@38037	1421	calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38037	1422	("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
neuper@38037	1423	("DIVIDE",("Rings.inverse_class.divide",
neuper@38037	1424	eval_cancel "#divide_e")),
neuper@38037	1425	("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
neuper@37950	1426	(asm_thm=[],)
neuper@37950	1427	scr=Rfuns {init_state = init_state,
neuper@37950	1428	normal_form = normal_form,
neuper@37950	1429	locate_rule = locate_rule,
neuper@37950	1430	next_rule = next_rule,
neuper@37950	1431	attach_form = attach_form}};
neuper@37950	1432
neuper@37950	1433	val order_add_rls_ =
neuper@37950	1434	Rls{id = "order_add_rls_", preconds = [],
neuper@37950	1435	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	1436	erls = e_rls,srls = Erls,
neuper@37950	1437	calc = [],
neuper@37950	1438	(asm_thm = [],)
neuper@37950	1439	rules = [Rls_ order_add_
neuper@37950	1440	], scr = EmptyScr}:rls;
neuper@42398	1441	*}
neuper@37950	1442
neuper@42398	1443	text {* rule-set make_polynomial also named norm_Poly:
neuper@42398	1444	Rewrite order has not been implemented properly; the order is better in
neuper@42398	1445	make_polynomial_in (coded in SML).
neuper@42398	1446	Notes on state of development:
neuper@42398	1447	\# surprise 2006: test --- norm_Poly NOT COMPLETE ---
neuper@42398	1448	\# migration Isabelle2002 --> 2011 weakened the rule set, see test
neuper@42398	1449	--- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
neuper@42398	1450	*}
neuper@42398	1451	ML {*
neuper@37950	1452	(. see MG-DA.p.52ff .)
neuper@37950	1453	val make_polynomial(*MG.03, overwrites version from above,
neuper@37950	1454	previously 'make_polynomial_'*) =
neuper@37950	1455	Seq {id = "make_polynomial", preconds = []:term list,
neuper@37950	1456	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	1457	erls = Atools_erls, srls = Erls,calc = [],
neuper@37980	1458	rules = [Rls_ discard_minus,
neuper@37950	1459	Rls_ expand_poly_,
neuper@38034	1460	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1461	Rls_ order_mult_rls_,
neuper@37950	1462	Rls_ simplify_power_,
neuper@37950	1463	Rls_ calc_add_mult_pow_,
neuper@37950	1464	Rls_ reduce_012_mult_,
neuper@37950	1465	Rls_ order_add_rls_,
neuper@37950	1466	Rls_ collect_numerals_,
neuper@37950	1467	Rls_ reduce_012_,
neuper@37979	1468	Rls_ discard_parentheses1
neuper@37950	1469	],
neuper@37950	1470	scr = EmptyScr
neuper@37950	1471	}:rls;
neuper@37950	1472	val norm_Poly(=make_polynomial) =
neuper@37950	1473	Seq {id = "norm_Poly", preconds = []:term list,
neuper@37950	1474	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	1475	erls = Atools_erls, srls = Erls, calc = [],
neuper@37980	1476	rules = [Rls_ discard_minus,
neuper@37950	1477	Rls_ expand_poly_,
neuper@38034	1478	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1479	Rls_ order_mult_rls_,
neuper@37950	1480	Rls_ simplify_power_,
neuper@37950	1481	Rls_ calc_add_mult_pow_,
neuper@37950	1482	Rls_ reduce_012_mult_,
neuper@37950	1483	Rls_ order_add_rls_,
neuper@37950	1484	Rls_ collect_numerals_,
neuper@37950	1485	Rls_ reduce_012_,
neuper@37979	1486	Rls_ discard_parentheses1
neuper@37950	1487	],
neuper@37950	1488	scr = EmptyScr
neuper@37950	1489	}:rls;
neuper@37950	1490
neuper@37979	1491	(* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses1
neuper@37950	1492	and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
neuper@37950	1493	(* MG necessary for termination of norm_Rational(_mg) in Rational.ML*)
neuper@37950	1494	val make_rat_poly_with_parentheses =
neuper@37950	1495	Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
neuper@37950	1496	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950	1497	erls = Atools_erls, srls = Erls, calc = [],
neuper@37980	1498	rules = [Rls_ discard_minus,
neuper@37950	1499	Rls_ expand_poly_rat_,(ignors rationals)
neuper@38034	1500	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1501	Rls_ order_mult_rls_,
neuper@37950	1502	Rls_ simplify_power_,
neuper@37950	1503	Rls_ calc_add_mult_pow_,
neuper@37950	1504	Rls_ reduce_012_mult_,
neuper@37950	1505	Rls_ order_add_rls_,
neuper@37950	1506	Rls_ collect_numerals_,
neuper@37950	1507	Rls_ reduce_012_
neuper@37979	1508	(Rls_ discard_parentheses1 )
neuper@37950	1509	],
neuper@37950	1510	scr = EmptyScr
neuper@37950	1511	}:rls;
neuper@37950	1512
neuper@37950	1513	(*.a minimal ruleset for reverse rewriting of factions [2];
neuper@37950	1514	compare expand_binoms.*)
neuper@37950	1515	val rev_rew_p =
neuper@37950	1516	Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
neuper@37950	1517	erls = Atools_erls, srls = Erls,
neuper@38014	1518	calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
neuper@38034	1519	("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
neuper@37950	1520	("POWER", ("Atools.pow", eval_binop "#power_"))*)
neuper@37950	1521	],
neuper@37969	1522	rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
neuper@37950	1523	("(a + b)(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
neuper@37969	1524	Thm ("real_plus_binom_times1" ,num_str @{thm real_plus_binom_times1}),
neuper@37950	1525	("(a + 1b)(a + -1b) = a^^^2 + -1b^^^2")
neuper@37969	1526	Thm ("real_plus_binom_times2" ,num_str @{thm real_plus_binom_times2}),
neuper@37950	1527	("(a + -1b)(a + 1b) = a^^^2 + -1b^^^2")
neuper@37950	1528
neuper@37965	1529	Thm ("mult_1_left",num_str @{thm mult_1_left}),("1 z = z"*)
neuper@37950	1530
neuper@37965	1531	Thm ("left_distrib" ,num_str @{thm left_distrib}),
neuper@37950	1532	("(z1.0 + z2.0) w = z1.0 * w + z2.0 * w"*)
neuper@37974	1533	Thm ("right_distrib",num_str @{thm right_distrib}),
neuper@37950	1534	("w (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950	1535
neuper@37969	1536	Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}),
neuper@37950	1537	("?z1.1 ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
neuper@37950	1538	Rls_ order_mult_rls_,
neuper@37950	1539	(Rls_ order_add_rls_,)
neuper@37950	1540
neuper@38014	1541	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@38034	1542	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1543	Calc ("Atools.pow", eval_binop "#power_"),
neuper@37950	1544
neuper@37969	1545	Thm ("sym_realpow_twoI",
neuper@37969	1546	num_str (@{thm realpow_twoI} RS @{thm sym})),
neuper@37950	1547	("r1 r1 = r1 ^^^ 2"*)
neuper@37969	1548	Thm ("sym_real_mult_2",
neuper@37969	1549	num_str (@{thm real_mult_2} RS @{thm sym})),
neuper@37950	1550	("z1 + z1 = 2 z1"*)
neuper@37969	1551	Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
neuper@37950	1552	("z1 + (z1 + k) = 2 z1 + k"*)
neuper@37950	1553
neuper@37969	1554	Thm ("real_num_collect",num_str @{thm real_num_collect}),
neuper@37950	1555	("[\| l is_const; m is_const \|]==>l n + m * n = (l + m) * n"*)
neuper@37969	1556	Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
neuper@37950	1557	(*"[\| l is_const; m is_const \|] ==>
neuper@37950	1558	l * n + (m * n + k) = (l + m) * n + k"*)
neuper@37969	1559	Thm ("real_one_collect",num_str @{thm real_one_collect}),
neuper@37950	1560	("m is_const ==> n + m n = (1 + m) * n"*)
neuper@37969	1561	Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
neuper@37950	1562	("m is_const ==> k + (n + m n) = k + (1 + m) * n"*)
neuper@37950	1563
neuper@37969	1564	Thm ("realpow_multI", num_str @{thm realpow_multI}),
neuper@37950	1565	("(r s) ^^^ n = r ^^^ n * s ^^^ n"*)
neuper@37950	1566
neuper@38014	1567	Calc ("Groups.plus_class.plus", eval_binop "#add_"),
neuper@38034	1568	Calc ("Groups.times_class.times", eval_binop "#mult_"),
neuper@37950	1569	Calc ("Atools.pow", eval_binop "#power_"),
neuper@37950	1570
neuper@37965	1571	Thm ("mult_1_left",num_str @{thm mult_1_left}),("1 z = z"*)
neuper@37965	1572	Thm ("mult_zero_left",num_str @{thm mult_zero_left}),("0 z = 0"*)
neuper@37965	1573	Thm ("add_0_left",num_str @{thm add_0_left})(0 + z = z)
neuper@37950	1574
neuper@37950	1575	(Rls_ order_add_rls_)
neuper@37950	1576	],
neuper@37950	1577
neuper@37950	1578	scr = EmptyScr}:rls;
neuper@37950	1579
neuper@37950	1580	ruleset' :=
neuper@37967	1581	overwritelthy @{theory} (!ruleset',
neuper@37950	1582	[("norm_Poly", prep_rls norm_Poly),
neuper@37950	1583	("Poly_erls",Poly_erls)(FIXXXME:del with rls.rls'),
neuper@37950	1584	("expand", prep_rls expand),
neuper@37950	1585	("expand_poly", prep_rls expand_poly),
neuper@37950	1586	("simplify_power", prep_rls simplify_power),
neuper@37950	1587	("order_add_mult", prep_rls order_add_mult),
neuper@37950	1588	("collect_numerals", prep_rls collect_numerals),
neuper@37950	1589	("collect_numerals_", prep_rls collect_numerals_),
neuper@37950	1590	("reduce_012", prep_rls reduce_012),
neuper@37950	1591	("discard_parentheses", prep_rls discard_parentheses),
neuper@37950	1592	("make_polynomial", prep_rls make_polynomial),
neuper@37950	1593	("expand_binoms", prep_rls expand_binoms),
neuper@37950	1594	("rev_rew_p", prep_rls rev_rew_p),
neuper@37980	1595	("discard_minus", prep_rls discard_minus),
neuper@37950	1596	("expand_poly_", prep_rls expand_poly_),
neuper@37950	1597	("expand_poly_rat_", prep_rls expand_poly_rat_),
neuper@37950	1598	("simplify_power_", prep_rls simplify_power_),
neuper@37950	1599	("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
neuper@37950	1600	("reduce_012_mult_", prep_rls reduce_012_mult_),
neuper@37950	1601	("reduce_012_", prep_rls reduce_012_),
neuper@37979	1602	("discard_parentheses1",prep_rls discard_parentheses1),
neuper@37950	1603	("order_mult_rls_", prep_rls order_mult_rls_),
neuper@37950	1604	("order_add_rls_", prep_rls order_add_rls_),
neuper@37950	1605	("make_rat_poly_with_parentheses",
neuper@37950	1606	prep_rls make_rat_poly_with_parentheses)
neuper@37950	1607	]);
neuper@37950	1608
neuper@37950	1609	calclist':= overwritel (!calclist',
neuper@37950	1610	[("is_polyrat_in", ("Poly.is'_polyrat'_in",
neuper@37950	1611	eval_is_polyrat_in "#eval_is_polyrat_in")),
neuper@37950	1612	("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
neuper@37950	1613	("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
neuper@37950	1614	("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
neuper@37950	1615	("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
neuper@37950	1616	("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
neuper@37950	1617	("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
neuper@37950	1618	]);
neuper@37950	1619
neuper@37976	1620	val ------------------------------------------------------ = "11111";
neuper@37950	1621
neuper@37950	1622	( problems )
neuper@37950	1623
neuper@37950	1624	store_pbt
neuper@37972	1625	(prep_pbt thy "pbl_simp_poly" [] e_pblID
neuper@37950	1626	(["polynomial","simplification"],
neuper@38083	1627	[("#Given" ,["Term t_t"]),
neuper@37976	1628	("#Where" ,["t_t is_polyexp"]),
neuper@37976	1629	("#Find" ,["normalform n_n"])
neuper@37950	1630	],
neuper@37950	1631	append_rls "e_rls" e_rls [(for preds in where_)
neuper@37950	1632	Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
neuper@37976	1633	SOME "Simplify t_t",
neuper@37950	1634	[["simplification","for_polynomials"]]));
neuper@37950	1635
neuper@37950	1636	( methods )
neuper@37950	1637
neuper@37950	1638	store_met
neuper@37972	1639	(prep_met thy "met_simp_poly" [] e_metID
neuper@37950	1640	(["simplification","for_polynomials"],
neuper@38083	1641	[("#Given" ,["Term t_t"]),
neuper@37976	1642	("#Where" ,["t_t is_polyexp"]),
neuper@37976	1643	("#Find" ,["normalform n_n"])
neuper@37950	1644	],
neuper@37950	1645	{rew_ord'="tless_true",
neuper@37950	1646	rls' = e_rls,
neuper@37950	1647	calc = [],
neuper@37950	1648	srls = e_rls,
neuper@37950	1649	prls = append_rls "simplification_for_polynomials_prls" e_rls
neuper@37950	1650	[(for preds in where_)
neuper@37950	1651	Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
neuper@37950	1652	crls = e_rls, nrls = norm_Poly},
neuper@37976	1653	"Script SimplifyScript (t_t::real) = " ^
neuper@37976	1654	" ((Rewrite_Set norm_Poly False) t_t)"
neuper@37950	1655	));
neuper@37950	1656	*}
neuper@37950	1657
neuper@37906	1658	end

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 19 Mar 2012 09:48:03 +0100
changeset 42398	04d3f0133827
parent 42319	ffad491ba8f2
child 42407	81afb8eb9b03
permissions	-rw-r--r--