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

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 26 Aug 2010 18:15:30 +0200
branch	isac-update-Isa09-2
changeset 37950	525a28152a67
parent 37947	22235e4dbe5f
child 37953	369b3012f6f6
permissions	-rw-r--r--