wneuper/isac: src/sml/IsacKnowledge/Poly.ML@de188f2995c6 (annotated)

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

author	wneuper
	Mon, 04 Sep 2006 14:08:09 +0200
branch	start_Take
changeset 643	de188f2995c6
parent 631	70ae02665749
child 660	c58b3d2ee7a9
permissions	-rw-r--r--