wneuper/isa: src/Tools/isac/Knowledge/Poly.ML@22235e4dbe5f (annotated)

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 25 Aug 2010 16:20:07 +0200
branch	isac-update-Isa09-2
changeset 37947	22235e4dbe5f
parent 37938	src/Tools/isac/IsacKnowledge/Poly.ML@f6164be9280d
permissions	-rw-r--r--