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

author	Walther Neuper <wneuper@ist.tugraz.at>
	Tue, 19 Mar 2019 15:42:15 +0100
changeset 59522	3d40f6aec0b1
parent 59505	a1f223658994
child 59523	9d23aa91a9f2
permissions	-rw-r--r--