wneuper/isa: src/Tools/isac/Knowledge/PolyEq.thy@9c11005c33b8 (annotated)

neuper@37906	1	(* theory collecting all knowledge
neuper@37906	2	(predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
neuper@37906	3	for PolynomialEquations.
neuper@37906	4	alternative dependencies see Isac.thy
neuper@37906	5	created by: rlang
neuper@37906	6	date: 02.07
neuper@37906	7	changed by: rlang
neuper@37906	8	last change by: rlang
neuper@37906	9	date: 03.06.03
neuper@37954	10	(c) by Richard Lang, 2003
neuper@37906	11	*)
neuper@37906	12
neuper@37954	13	theory PolyEq imports LinEq RootRatEq begin
neuper@37906	14
neuper@37906	15	consts
neuper@37906	16
neuper@37906	17	(---------scripts--------------------------)
neuper@37906	18	Complete'_square
neuper@37954	19	:: "[bool,real,
neuper@37954	20	bool list] => bool list"
neuper@37954	21	("((Script Complete'_square (_ _ =))//
neuper@37954	22	(_))" 9)
neuper@37906	23	(----- poly ----- )
neuper@37906	24	Normalize'_poly
neuper@37954	25	:: "[bool,real,
neuper@37954	26	bool list] => bool list"
neuper@37954	27	("((Script Normalize'_poly (_ _=))//
neuper@37954	28	(_))" 9)
neuper@37906	29	Solve'_d0'_polyeq'_equation
neuper@37954	30	:: "[bool,real,
neuper@37954	31	bool list] => bool list"
neuper@37954	32	("((Script Solve'_d0'_polyeq'_equation (_ _ =))//
neuper@37954	33	(_))" 9)
neuper@37906	34	Solve'_d1'_polyeq'_equation
neuper@37954	35	:: "[bool,real,
neuper@37954	36	bool list] => bool list"
neuper@37954	37	("((Script Solve'_d1'_polyeq'_equation (_ _ =))//
neuper@37954	38	(_))" 9)
neuper@37906	39	Solve'_d2'_polyeq'_equation
neuper@37954	40	:: "[bool,real,
neuper@37954	41	bool list] => bool list"
neuper@37954	42	("((Script Solve'_d2'_polyeq'_equation (_ _ =))//
neuper@37954	43	(_))" 9)
neuper@37906	44	Solve'_d2'_polyeq'_sqonly'_equation
neuper@37954	45	:: "[bool,real,
neuper@37954	46	bool list] => bool list"
neuper@37954	47	("((Script Solve'_d2'_polyeq'_sqonly'_equation (_ _ =))//
neuper@37954	48	(_))" 9)
neuper@37906	49	Solve'_d2'_polyeq'_bdvonly'_equation
neuper@37954	50	:: "[bool,real,
neuper@37954	51	bool list] => bool list"
neuper@37954	52	("((Script Solve'_d2'_polyeq'_bdvonly'_equation (_ _ =))//
neuper@37954	53	(_))" 9)
neuper@37906	54	Solve'_d2'_polyeq'_pq'_equation
neuper@37954	55	:: "[bool,real,
neuper@37954	56	bool list] => bool list"
neuper@37954	57	("((Script Solve'_d2'_polyeq'_pq'_equation (_ _ =))//
neuper@37954	58	(_))" 9)
neuper@37906	59	Solve'_d2'_polyeq'_abc'_equation
neuper@37954	60	:: "[bool,real,
neuper@37954	61	bool list] => bool list"
neuper@37954	62	("((Script Solve'_d2'_polyeq'_abc'_equation (_ _ =))//
neuper@37954	63	(_))" 9)
neuper@37906	64	Solve'_d3'_polyeq'_equation
neuper@37954	65	:: "[bool,real,
neuper@37954	66	bool list] => bool list"
neuper@37954	67	("((Script Solve'_d3'_polyeq'_equation (_ _ =))//
neuper@37954	68	(_))" 9)
neuper@37906	69	Solve'_d4'_polyeq'_equation
neuper@37954	70	:: "[bool,real,
neuper@37954	71	bool list] => bool list"
neuper@37954	72	("((Script Solve'_d4'_polyeq'_equation (_ _ =))//
neuper@37954	73	(_))" 9)
neuper@37906	74	Biquadrat'_poly
neuper@37954	75	:: "[bool,real,
neuper@37954	76	bool list] => bool list"
neuper@37954	77	("((Script Biquadrat'_poly (_ _=))//
neuper@37954	78	(_))" 9)
neuper@37906	79
neuper@37906	80	(-------------------- rules -------------------------------------------------)
neuper@37954	81	axioms
neuper@37906	82
neuper@37954	83	cancel_leading_coeff1 "Not (c =!= 0) ==> (a + bbdv + cbdv^^^2 = 0) =
neuper@37954	84	(a/c + b/c*bdv + bdv^^^2 = 0)"
neuper@37954	85	cancel_leading_coeff2 "Not (c =!= 0) ==> (a - bbdv + cbdv^^^2 = 0) =
neuper@37954	86	(a/c - b/c*bdv + bdv^^^2 = 0)"
neuper@37954	87	cancel_leading_coeff3 "Not (c =!= 0) ==> (a + bbdv - cbdv^^^2 = 0) =
neuper@37954	88	(a/c + b/c*bdv - bdv^^^2 = 0)"
neuper@37906	89
neuper@37954	90	cancel_leading_coeff4 "Not (c =!= 0) ==> (a + bdv + c*bdv^^^2 = 0) =
neuper@37954	91	(a/c + 1/c*bdv + bdv^^^2 = 0)"
neuper@37954	92	cancel_leading_coeff5 "Not (c =!= 0) ==> (a - bdv + c*bdv^^^2 = 0) =
neuper@37954	93	(a/c - 1/c*bdv + bdv^^^2 = 0)"
neuper@37954	94	cancel_leading_coeff6 "Not (c =!= 0) ==> (a + bdv - c*bdv^^^2 = 0) =
neuper@37954	95	(a/c + 1/c*bdv - bdv^^^2 = 0)"
neuper@37906	96
neuper@37954	97	cancel_leading_coeff7 "Not (c =!= 0) ==> ( bbdv + cbdv^^^2 = 0) =
neuper@37954	98	( b/c*bdv + bdv^^^2 = 0)"
neuper@37954	99	cancel_leading_coeff8 "Not (c =!= 0) ==> ( bbdv - cbdv^^^2 = 0) =
neuper@37954	100	( b/c*bdv - bdv^^^2 = 0)"
neuper@37906	101
neuper@37954	102	cancel_leading_coeff9 "Not (c =!= 0) ==> ( bdv + c*bdv^^^2 = 0) =
neuper@37954	103	( 1/c*bdv + bdv^^^2 = 0)"
neuper@37954	104	cancel_leading_coeff10"Not (c =!= 0) ==> ( bdv - c*bdv^^^2 = 0) =
neuper@37954	105	( 1/c*bdv - bdv^^^2 = 0)"
neuper@37906	106
neuper@37954	107	cancel_leading_coeff11"Not (c =!= 0) ==> (a + b*bdv^^^2 = 0) =
neuper@37954	108	(a/b + bdv^^^2 = 0)"
neuper@37954	109	cancel_leading_coeff12"Not (c =!= 0) ==> (a - b*bdv^^^2 = 0) =
neuper@37954	110	(a/b - bdv^^^2 = 0)"
neuper@37954	111	cancel_leading_coeff13"Not (c =!= 0) ==> ( b*bdv^^^2 = 0) =
neuper@37954	112	( bdv^^^2 = 0/b)"
neuper@37906	113
neuper@37954	114	complete_square1 "(q + p*bdv + bdv^^^2 = 0) =
neuper@37954	115	(q + (p/2 + bdv)^^^2 = (p/2)^^^2)"
neuper@37954	116	complete_square2 "( p*bdv + bdv^^^2 = 0) =
neuper@37954	117	( (p/2 + bdv)^^^2 = (p/2)^^^2)"
neuper@37954	118	complete_square3 "( bdv + bdv^^^2 = 0) =
neuper@37954	119	( (1/2 + bdv)^^^2 = (1/2)^^^2)"
neuper@37906	120
neuper@37954	121	complete_square4 "(q - p*bdv + bdv^^^2 = 0) =
neuper@37954	122	(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
neuper@37954	123	complete_square5 "(q + p*bdv - bdv^^^2 = 0) =
neuper@37954	124	(q + (p/2 - bdv)^^^2 = (p/2)^^^2)"
neuper@37906	125
neuper@37906	126	square_explicit1 "(a + b^^^2 = c) = ( b^^^2 = c - a)"
neuper@37906	127	square_explicit2 "(a - b^^^2 = c) = (-(b^^^2) = c - a)"
neuper@37906	128
neuper@37906	129	bdv_explicit1 "(a + bdv = b) = (bdv = - a + b)"
neuper@37906	130	bdv_explicit2 "(a - bdv = b) = ((-1)*bdv = - a + b)"
neuper@37906	131	bdv_explicit3 "((-1)bdv = b) = (bdv = (-1)b)"
neuper@37906	132
neuper@37906	133	plus_leq "(0 <= a + b) = ((-1)b <= a)"(Isa?*)
neuper@37906	134	minus_leq "(0 <= a - b) = ( b <= a)"(Isa?)
neuper@37906	135
neuper@37906	136	(-- normalize --)
neuper@37906	137	(WN0509 compare LinEq.all_left "[\|Not(b=!=0)\|] ==> (a=b) = (a+(-1)b=0)"*)
neuper@37954	138	all_left "[\|Not(b=!=0)\|] ==> (a = b) = (a - b = 0)"
neuper@37954	139	makex1_x "a^^^1 = a"
neuper@37954	140	real_assoc_1 "a+(b+c) = a+b+c"
neuper@37954	141	real_assoc_2 "a(bc) = abc"
neuper@37906	142
neuper@37906	143	(* ---- degree 0 ----*)
neuper@37954	144	d0_true "(0=0) = True"
neuper@37954	145	d0_false "[\|Not(bdv occurs_in a);Not(a=0)\|] ==> (a=0) = False"
neuper@37906	146	(* ---- degree 1 ----*)
neuper@37906	147	d1_isolate_add1
neuper@37906	148	"[\|Not(bdv occurs_in a)\|] ==> (a + bbdv = 0) = (bbdv = (-1)*a)"
neuper@37906	149	d1_isolate_add2
neuper@37906	150	"[\|Not(bdv occurs_in a)\|] ==> (a + bdv = 0) = ( bdv = (-1)*a)"
neuper@37906	151	d1_isolate_div
neuper@37906	152	"[\|Not(b=0);Not(bdv occurs_in c)\|] ==> (b*bdv = c) = (bdv = c/b)"
neuper@37906	153	(* ---- degree 2 ----*)
neuper@37906	154	d2_isolate_add1
neuper@37906	155	"[\|Not(bdv occurs_in a)\|] ==> (a + bbdv^^^2=0) = (bbdv^^^2= (-1)*a)"
neuper@37906	156	d2_isolate_add2
neuper@37906	157	"[\|Not(bdv occurs_in a)\|] ==> (a + bdv^^^2=0) = ( bdv^^^2= (-1)*a)"
neuper@37906	158	d2_isolate_div
neuper@37906	159	"[\|Not(b=0);Not(bdv occurs_in c)\|] ==> (b*bdv^^^2=c) = (bdv^^^2=c/b)"
neuper@37954	160
neuper@37954	161	d2_prescind1 "(abdv + bbdv^^^2 = 0) = (bdv(a +bbdv)=0)"
neuper@37954	162	d2_prescind2 "(abdv + bdv^^^2 = 0) = (bdv(a + bdv)=0)"
neuper@37954	163	d2_prescind3 "( bdv + bbdv^^^2 = 0) = (bdv(1+b*bdv)=0)"
neuper@37954	164	d2_prescind4 "( bdv + bdv^^^2 = 0) = (bdv*(1+ bdv)=0)"
neuper@37906	165	(* eliminate degree 2 *)
neuper@37906	166	(* thm for neg arguments in sqroot have postfix _neg *)
neuper@37954	167	d2_sqrt_equation1 "[\|(0<=c);Not(bdv occurs_in c)\|] ==>
neuper@37954	168	(bdv^^^2=c) = ((bdv=sqrt c) \| (bdv=(-1)*sqrt c ))"
neuper@37906	169	d2_sqrt_equation1_neg
neuper@37906	170	"[\|(c<0);Not(bdv occurs_in c)\|] ==> (bdv^^^2=c) = False"
neuper@37954	171	d2_sqrt_equation2 "(bdv^^^2=0) = (bdv=0)"
neuper@37954	172	d2_sqrt_equation3 "(b*bdv^^^2=0) = (bdv=0)"
neuper@37954	173	d2_reduce_equation1 "(bdv(a +bbdv)=0) = ((bdv=0)\|(a+b*bdv=0))"
neuper@37954	174	d2_reduce_equation2 "(bdv*(a + bdv)=0) = ((bdv=0)\|(a+ bdv=0))"
neuper@37954	175	d2_pqformula1 "[\|0<=p^^^2 - 4q\|] ==> (q+pbdv+ bdv^^^2=0) =
neuper@37954	176	((bdv= (-1)(p/2) + sqrt(p^^^2 - 4q)/2)
neuper@37954	177	\| (bdv= (-1)(p/2) - sqrt(p^^^2 - 4q)/2))"
neuper@37954	178	d2_pqformula1_neg "[\|p^^^2 - 4q<0\|] ==> (q+pbdv+ bdv^^^2=0) = False"
neuper@37954	179	d2_pqformula2 "[\|0<=p^^^2 - 4q\|] ==> (q+pbdv+1*bdv^^^2=0) =
neuper@37954	180	((bdv= (-1)(p/2) + sqrt(p^^^2 - 4q)/2)
neuper@37954	181	\| (bdv= (-1)(p/2) - sqrt(p^^^2 - 4q)/2))"
neuper@37954	182	d2_pqformula2_neg "[\|p^^^2 - 4q<0\|] ==> (q+pbdv+1*bdv^^^2=0) = False"
neuper@37954	183	d2_pqformula3 "[\|0<=1 - 4*q\|] ==> (q+ bdv+ bdv^^^2=0) =
neuper@37954	184	((bdv= (-1)(1/2) + sqrt(1 - 4q)/2)
neuper@37954	185	\| (bdv= (-1)(1/2) - sqrt(1 - 4q)/2))"
neuper@37954	186	d2_pqformula3_neg "[\|1 - 4*q<0\|] ==> (q+ bdv+ bdv^^^2=0) = False"
neuper@37954	187	d2_pqformula4 "[\|0<=1 - 4q\|] ==> (q+ bdv+1bdv^^^2=0) =
neuper@37954	188	((bdv= (-1)(1/2) + sqrt(1 - 4q)/2)
neuper@37954	189	\| (bdv= (-1)(1/2) - sqrt(1 - 4q)/2))"
neuper@37954	190	d2_pqformula4_neg "[\|1 - 4q<0\|] ==> (q+ bdv+1bdv^^^2=0) = False"
neuper@37954	191	d2_pqformula5 "[\|0<=p^^^2 - 0\|] ==> ( p*bdv+ bdv^^^2=0) =
neuper@37954	192	((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
neuper@37954	193	\| (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
neuper@37906	194	(* d2_pqformula5_neg not need p^2 never less zero in R *)
neuper@37954	195	d2_pqformula6 "[\|0<=p^^^2 - 0\|] ==> ( pbdv+1bdv^^^2=0) =
neuper@37954	196	((bdv= (-1)*(p/2) + sqrt(p^^^2 - 0)/2)
neuper@37954	197	\| (bdv= (-1)*(p/2) - sqrt(p^^^2 - 0)/2))"
neuper@37906	198	(* d2_pqformula6_neg not need p^2 never less zero in R *)
neuper@37954	199	d2_pqformula7 "[\|0<=1 - 0\|] ==> ( bdv+ bdv^^^2=0) =
neuper@37954	200	((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
neuper@37954	201	\| (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
neuper@37906	202	(* d2_pqformula7_neg not need, because 1<0 ==> False*)
neuper@37954	203	d2_pqformula8 "[\|0<=1 - 0\|] ==> ( bdv+1*bdv^^^2=0) =
neuper@37954	204	((bdv= (-1)*(1/2) + sqrt(1 - 0)/2)
neuper@37954	205	\| (bdv= (-1)*(1/2) - sqrt(1 - 0)/2))"
neuper@37906	206	(* d2_pqformula8_neg not need, because 1<0 ==> False*)
neuper@37954	207	d2_pqformula9 "[\|Not(bdv occurs_in q); 0<= (-1)4q\|] ==>
neuper@37954	208	(q+ 1bdv^^^2=0) = ((bdv= 0 + sqrt(0 - 4q)/2)
neuper@37954	209	\| (bdv= 0 - sqrt(0 - 4*q)/2))"
neuper@37906	210	d2_pqformula9_neg
neuper@37906	211	"[\|Not(bdv occurs_in q); (-1)4q<0\|] ==> (q+ 1*bdv^^^2=0) = False"
neuper@37906	212	d2_pqformula10
neuper@37906	213	"[\|Not(bdv occurs_in q); 0<= (-1)4q\|] ==> (q+ bdv^^^2=0) =
neuper@37906	214	((bdv= 0 + sqrt(0 - 4*q)/2)
neuper@37906	215	\| (bdv= 0 - sqrt(0 - 4*q)/2))"
neuper@37906	216	d2_pqformula10_neg
neuper@37906	217	"[\|Not(bdv occurs_in q); (-1)4q<0\|] ==> (q+ bdv^^^2=0) = False"
neuper@37906	218	d2_abcformula1
neuper@37906	219	"[\|0<=b^^^2 - 4ac\|] ==> (c + bbdv+abdv^^^2=0) =
neuper@37906	220	((bdv=( -b + sqrt(b^^^2 - 4ac))/(2*a))
neuper@37906	221	\| (bdv=( -b - sqrt(b^^^2 - 4ac))/(2*a)))"
neuper@37906	222	d2_abcformula1_neg
neuper@37906	223	"[\|b^^^2 - 4ac<0\|] ==> (c + bbdv+abdv^^^2=0) = False"
neuper@37906	224	d2_abcformula2
neuper@37906	225	"[\|0<=1 - 4ac\|] ==> (c+ bdv+a*bdv^^^2=0) =
neuper@37906	226	((bdv=( -1 + sqrt(1 - 4ac))/(2*a))
neuper@37906	227	\| (bdv=( -1 - sqrt(1 - 4ac))/(2*a)))"
neuper@37906	228	d2_abcformula2_neg
neuper@37906	229	"[\|1 - 4ac<0\|] ==> (c+ bdv+a*bdv^^^2=0) = False"
neuper@37906	230	d2_abcformula3
neuper@37906	231	"[\|0<=b^^^2 - 41c\|] ==> (c + b*bdv+ bdv^^^2=0) =
neuper@37906	232	((bdv=( -b + sqrt(b^^^2 - 41c))/(2*1))
neuper@37906	233	\| (bdv=( -b - sqrt(b^^^2 - 41c))/(2*1)))"
neuper@37906	234	d2_abcformula3_neg
neuper@37906	235	"[\|b^^^2 - 41c<0\|] ==> (c + b*bdv+ bdv^^^2=0) = False"
neuper@37906	236	d2_abcformula4
neuper@37906	237	"[\|0<=1 - 41c\|] ==> (c + bdv+ bdv^^^2=0) =
neuper@37906	238	((bdv=( -1 + sqrt(1 - 41c))/(2*1))
neuper@37906	239	\| (bdv=( -1 - sqrt(1 - 41c))/(2*1)))"
neuper@37906	240	d2_abcformula4_neg
neuper@37906	241	"[\|1 - 41c<0\|] ==> (c + bdv+ bdv^^^2=0) = False"
neuper@37906	242	d2_abcformula5
neuper@37906	243	"[\|Not(bdv occurs_in c); 0<=0 - 4ac\|] ==> (c + a*bdv^^^2=0) =
neuper@37906	244	((bdv=( 0 + sqrt(0 - 4ac))/(2*a))
neuper@37906	245	\| (bdv=( 0 - sqrt(0 - 4ac))/(2*a)))"
neuper@37906	246	d2_abcformula5_neg
neuper@37906	247	"[\|Not(bdv occurs_in c); 0 - 4ac<0\|] ==> (c + a*bdv^^^2=0) = False"
neuper@37906	248	d2_abcformula6
neuper@37906	249	"[\|Not(bdv occurs_in c); 0<=0 - 41c\|] ==> (c+ bdv^^^2=0) =
neuper@37906	250	((bdv=( 0 + sqrt(0 - 41c))/(2*1))
neuper@37906	251	\| (bdv=( 0 - sqrt(0 - 41c))/(2*1)))"
neuper@37906	252	d2_abcformula6_neg
neuper@37906	253	"[\|Not(bdv occurs_in c); 0 - 41c<0\|] ==> (c+ bdv^^^2=0) = False"
neuper@37906	254	d2_abcformula7
neuper@37906	255	"[\|0<=b^^^2 - 0\|] ==> ( bbdv+abdv^^^2=0) =
neuper@37906	256	((bdv=( -b + sqrt(b^^^2 - 0))/(2*a))
neuper@37906	257	\| (bdv=( -b - sqrt(b^^^2 - 0))/(2*a)))"
neuper@37906	258	(* d2_abcformula7_neg not need b^2 never less zero in R *)
neuper@37906	259	d2_abcformula8
neuper@37906	260	"[\|0<=b^^^2 - 0\|] ==> ( b*bdv+ bdv^^^2=0) =
neuper@37906	261	((bdv=( -b + sqrt(b^^^2 - 0))/(2*1))
neuper@37906	262	\| (bdv=( -b - sqrt(b^^^2 - 0))/(2*1)))"
neuper@37906	263	(* d2_abcformula8_neg not need b^2 never less zero in R *)
neuper@37906	264	d2_abcformula9
neuper@37906	265	"[\|0<=1 - 0\|] ==> ( bdv+a*bdv^^^2=0) =
neuper@37906	266	((bdv=( -1 + sqrt(1 - 0))/(2*a))
neuper@37906	267	\| (bdv=( -1 - sqrt(1 - 0))/(2*a)))"
neuper@37906	268	(* d2_abcformula9_neg not need, because 1<0 ==> False*)
neuper@37906	269	d2_abcformula10
neuper@37906	270	"[\|0<=1 - 0\|] ==> ( bdv+ bdv^^^2=0) =
neuper@37906	271	((bdv=( -1 + sqrt(1 - 0))/(2*1))
neuper@37906	272	\| (bdv=( -1 - sqrt(1 - 0))/(2*1)))"
neuper@37906	273	(* d2_abcformula10_neg not need, because 1<0 ==> False*)
neuper@37906	274
neuper@37906	275	(* ---- degree 3 ----*)
neuper@37906	276	d3_reduce_equation1
neuper@37906	277	"(abdv + bbdv^^^2 + cbdv^^^3=0) = (bdv=0 \| (a + bbdv + c*bdv^^^2=0))"
neuper@37906	278	d3_reduce_equation2
neuper@37906	279	"( bdv + bbdv^^^2 + cbdv^^^3=0) = (bdv=0 \| (1 + bbdv + cbdv^^^2=0))"
neuper@37906	280	d3_reduce_equation3
neuper@37906	281	"(abdv + bdv^^^2 + cbdv^^^3=0) = (bdv=0 \| (a + bdv + c*bdv^^^2=0))"
neuper@37906	282	d3_reduce_equation4
neuper@37906	283	"( bdv + bdv^^^2 + cbdv^^^3=0) = (bdv=0 \| (1 + bdv + cbdv^^^2=0))"
neuper@37906	284	d3_reduce_equation5
neuper@37906	285	"(abdv + bbdv^^^2 + bdv^^^3=0) = (bdv=0 \| (a + b*bdv + bdv^^^2=0))"
neuper@37906	286	d3_reduce_equation6
neuper@37906	287	"( bdv + bbdv^^^2 + bdv^^^3=0) = (bdv=0 \| (1 + bbdv + bdv^^^2=0))"
neuper@37906	288	d3_reduce_equation7
neuper@37906	289	"(a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 \| (1 + bdv + bdv^^^2=0))"
neuper@37906	290	d3_reduce_equation8
neuper@37906	291	"( bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 \| (1 + bdv + bdv^^^2=0))"
neuper@37906	292	d3_reduce_equation9
neuper@37906	293	"(abdv + cbdv^^^3=0) = (bdv=0 \| (a + c*bdv^^^2=0))"
neuper@37906	294	d3_reduce_equation10
neuper@37906	295	"( bdv + cbdv^^^3=0) = (bdv=0 \| (1 + cbdv^^^2=0))"
neuper@37906	296	d3_reduce_equation11
neuper@37906	297	"(a*bdv + bdv^^^3=0) = (bdv=0 \| (a + bdv^^^2=0))"
neuper@37906	298	d3_reduce_equation12
neuper@37906	299	"( bdv + bdv^^^3=0) = (bdv=0 \| (1 + bdv^^^2=0))"
neuper@37906	300	d3_reduce_equation13
neuper@37906	301	"( bbdv^^^2 + cbdv^^^3=0) = (bdv=0 \| ( bbdv + cbdv^^^2=0))"
neuper@37906	302	d3_reduce_equation14
neuper@37906	303	"( bdv^^^2 + cbdv^^^3=0) = (bdv=0 \| ( bdv + cbdv^^^2=0))"
neuper@37906	304	d3_reduce_equation15
neuper@37906	305	"( bbdv^^^2 + bdv^^^3=0) = (bdv=0 \| ( bbdv + bdv^^^2=0))"
neuper@37906	306	d3_reduce_equation16
neuper@37906	307	"( bdv^^^2 + bdv^^^3=0) = (bdv=0 \| ( bdv + bdv^^^2=0))"
neuper@37906	308	d3_isolate_add1
neuper@37906	309	"[\|Not(bdv occurs_in a)\|] ==> (a + bbdv^^^3=0) = (bbdv^^^3= (-1)*a)"
neuper@37906	310	d3_isolate_add2
neuper@37906	311	"[\|Not(bdv occurs_in a)\|] ==> (a + bdv^^^3=0) = ( bdv^^^3= (-1)*a)"
neuper@37906	312	d3_isolate_div
neuper@37906	313	"[\|Not(b=0);Not(bdv occurs_in a)\|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b)"
neuper@37906	314	d3_root_equation2
neuper@37906	315	"(bdv^^^3=0) = (bdv=0)"
neuper@37906	316	d3_root_equation1
neuper@37906	317	"(bdv^^^3=c) = (bdv = nroot 3 c)"
neuper@37906	318
neuper@37906	319	(* ---- degree 4 ----*)
neuper@37906	320	(* RL03.FIXME es wir nicht getestet ob u>0 *)
neuper@37906	321	d4_sub_u1
neuper@37906	322	"(c+bbdv^^^2+abdv^^^4=0) =
neuper@37906	323	((au^^^2+bu+c=0) & (bdv^^^2=u))"
neuper@37906	324
neuper@37906	325	(* ---- 7.3.02 von Termorder ---- *)
neuper@37906	326
neuper@37906	327	bdv_collect_1 "l * bdv + m * bdv = (l + m) * bdv"
neuper@37906	328	bdv_collect_2 "bdv + m * bdv = (1 + m) * bdv"
neuper@37906	329	bdv_collect_3 "l * bdv + bdv = (l + 1) * bdv"
neuper@37906	330
neuper@37906	331	(* bdv_collect_assoc0_1 "l * bdv + m * bdv + k = (l + m) * bdv + k"
neuper@37906	332	bdv_collect_assoc0_2 "bdv + m * bdv + k = (1 + m) * bdv + k"
neuper@37906	333	bdv_collect_assoc0_3 "l * bdv + bdv + k = (l + 1) * bdv + k"
neuper@37906	334	*)
neuper@37906	335	bdv_collect_assoc1_1 "l * bdv + (m * bdv + k) = (l + m) * bdv + k"
neuper@37906	336	bdv_collect_assoc1_2 "bdv + (m * bdv + k) = (1 + m) * bdv + k"
neuper@37906	337	bdv_collect_assoc1_3 "l * bdv + (bdv + k) = (l + 1) * bdv + k"
neuper@37906	338
neuper@37906	339	bdv_collect_assoc2_1 "k + l * bdv + m * bdv = k + (l + m) * bdv"
neuper@37906	340	bdv_collect_assoc2_2 "k + bdv + m * bdv = k + (1 + m) * bdv"
neuper@37906	341	bdv_collect_assoc2_3 "k + l * bdv + bdv = k + (l + 1) * bdv"
neuper@37906	342
neuper@37906	343
neuper@37906	344	bdv_n_collect_1 "l * bdv^^^n + m * bdv^^^n = (l + m) * bdv^^^n"
neuper@37906	345	bdv_n_collect_2 " bdv^^^n + m * bdv^^^n = (1 + m) * bdv^^^n"
neuper@37906	346	bdv_n_collect_3 "l * bdv^^^n + bdv^^^n = (l + 1) * bdv^^^n" (order!)
neuper@37906	347
neuper@37906	348	bdv_n_collect_assoc1_1 "l * bdv^^^n + (m * bdv^^^n + k) = (l + m) * bdv^^^n + k"
neuper@37906	349	bdv_n_collect_assoc1_2 "bdv^^^n + (m * bdv^^^n + k) = (1 + m) * bdv^^^n + k"
neuper@37906	350	bdv_n_collect_assoc1_3 "l * bdv^^^n + (bdv^^^n + k) = (l + 1) * bdv^^^n + k"
neuper@37906	351
neuper@37906	352	bdv_n_collect_assoc2_1 "k + l * bdv^^^n + m * bdv^^^n = k + (l + m) * bdv^^^n"
neuper@37906	353	bdv_n_collect_assoc2_2 "k + bdv^^^n + m * bdv^^^n = k + (1 + m) * bdv^^^n"
neuper@37906	354	bdv_n_collect_assoc2_3 "k + l * bdv^^^n + bdv^^^n = k + (l + 1) * bdv^^^n"
neuper@37906	355
neuper@37906	356	(WN.14.3.03)
neuper@37906	357	real_minus_div "- (a / b) = (-1 * a) / b"
neuper@37906	358
neuper@37906	359	separate_bdv "(a * bdv) / b = (a / b) * bdv"
neuper@37906	360	separate_bdv_n "(a * bdv ^^^ n) / b = (a / b) * bdv ^^^ n"
neuper@37906	361	separate_1_bdv "bdv / b = (1 / b) * bdv"
neuper@37906	362	separate_1_bdv_n "bdv ^^^ n / b = (1 / b) * bdv ^^^ n"
neuper@37906	363
neuper@37954	364	ML {*
neuper@37954	365	(-------------------------rulse-------------------------)
neuper@37954	366	val PolyEq_prls = (3.10.02:just the following order due to subterm evaluation)
neuper@37954	367	append_rls "PolyEq_prls" e_rls
neuper@37954	368	[Calc ("Atools.ident",eval_ident "#ident_"),
neuper@37954	369	Calc ("Tools.matches",eval_matches ""),
neuper@37954	370	Calc ("Tools.lhs" ,eval_lhs ""),
neuper@37954	371	Calc ("Tools.rhs" ,eval_rhs ""),
neuper@37954	372	Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
neuper@37954	373	Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
neuper@37954	374	Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
neuper@37954	375	Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
neuper@37954	376	(Calc ("Atools.occurs'_in",eval_occurs_in ""), )
neuper@37954	377	(Calc ("Atools.is'_const",eval_const "#is_const_"),)
neuper@37954	378	Calc ("op =",eval_equal "#equal_"),
neuper@37954	379	Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
neuper@37954	380	Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
neuper@37954	381	Thm ("not_true",num_str not_true),
neuper@37954	382	Thm ("not_false",num_str not_false),
neuper@37954	383	Thm ("and_true",num_str and_true),
neuper@37954	384	Thm ("and_false",num_str and_false),
neuper@37954	385	Thm ("or_true",num_str or_true),
neuper@37954	386	Thm ("or_false",num_str or_false)
neuper@37954	387	];
neuper@37954	388
neuper@37954	389	val PolyEq_erls =
neuper@37954	390	merge_rls "PolyEq_erls" LinEq_erls
neuper@37954	391	(append_rls "ops_preds" calculate_Rational
neuper@37954	392	[Calc ("op =",eval_equal "#equal_"),
neuper@37954	393	Thm ("plus_leq", num_str plus_leq),
neuper@37954	394	Thm ("minus_leq", num_str minus_leq),
neuper@37954	395	Thm ("rat_leq1", num_str rat_leq1),
neuper@37954	396	Thm ("rat_leq2", num_str rat_leq2),
neuper@37954	397	Thm ("rat_leq3", num_str rat_leq3)
neuper@37954	398	]);
neuper@37954	399
neuper@37954	400	val PolyEq_crls =
neuper@37954	401	merge_rls "PolyEq_crls" LinEq_crls
neuper@37954	402	(append_rls "ops_preds" calculate_Rational
neuper@37954	403	[Calc ("op =",eval_equal "#equal_"),
neuper@37954	404	Thm ("plus_leq", num_str plus_leq),
neuper@37954	405	Thm ("minus_leq", num_str minus_leq),
neuper@37954	406	Thm ("rat_leq1", num_str rat_leq1),
neuper@37954	407	Thm ("rat_leq2", num_str rat_leq2),
neuper@37954	408	Thm ("rat_leq3", num_str rat_leq3)
neuper@37954	409	]);
neuper@37954	410
neuper@37954	411	val cancel_leading_coeff = prep_rls(
neuper@37954	412	Rls {id = "cancel_leading_coeff", preconds = [],
neuper@37954	413	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	414	erls = PolyEq_erls, srls = Erls, calc = [], (asm_thm = [],)
neuper@37954	415	rules = [Thm ("cancel_leading_coeff1",num_str cancel_leading_coeff1),
neuper@37954	416	Thm ("cancel_leading_coeff2",num_str cancel_leading_coeff2),
neuper@37954	417	Thm ("cancel_leading_coeff3",num_str cancel_leading_coeff3),
neuper@37954	418	Thm ("cancel_leading_coeff4",num_str cancel_leading_coeff4),
neuper@37954	419	Thm ("cancel_leading_coeff5",num_str cancel_leading_coeff5),
neuper@37954	420	Thm ("cancel_leading_coeff6",num_str cancel_leading_coeff6),
neuper@37954	421	Thm ("cancel_leading_coeff7",num_str cancel_leading_coeff7),
neuper@37954	422	Thm ("cancel_leading_coeff8",num_str cancel_leading_coeff8),
neuper@37954	423	Thm ("cancel_leading_coeff9",num_str cancel_leading_coeff9),
neuper@37954	424	Thm ("cancel_leading_coeff10",num_str cancel_leading_coeff10),
neuper@37954	425	Thm ("cancel_leading_coeff11",num_str cancel_leading_coeff11),
neuper@37954	426	Thm ("cancel_leading_coeff12",num_str cancel_leading_coeff12),
neuper@37954	427	Thm ("cancel_leading_coeff13",num_str cancel_leading_coeff13)
neuper@37954	428	],
neuper@37954	429	scr = Script ((term_of o the o (parse thy))
neuper@37954	430	"empty_script")
neuper@37954	431	}:rls);
neuper@37954	432
neuper@37954	433	val complete_square = prep_rls(
neuper@37954	434	Rls {id = "complete_square", preconds = [],
neuper@37954	435	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	436	erls = PolyEq_erls, srls = Erls, calc = [], (asm_thm = [],)
neuper@37954	437	rules = [Thm ("complete_square1",num_str complete_square1),
neuper@37954	438	Thm ("complete_square2",num_str complete_square2),
neuper@37954	439	Thm ("complete_square3",num_str complete_square3),
neuper@37954	440	Thm ("complete_square4",num_str complete_square4),
neuper@37954	441	Thm ("complete_square5",num_str complete_square5)
neuper@37954	442	],
neuper@37954	443	scr = Script ((term_of o the o (parse thy))
neuper@37954	444	"empty_script")
neuper@37954	445	}:rls);
neuper@37954	446
neuper@37954	447	val polyeq_simplify = prep_rls(
neuper@37954	448	Rls {id = "polyeq_simplify", preconds = [],
neuper@37954	449	rew_ord = ("termlessI",termlessI),
neuper@37954	450	erls = PolyEq_erls,
neuper@37954	451	srls = Erls,
neuper@37954	452	calc = [],
neuper@37954	453	(asm_thm = [],)
neuper@37954	454	rules = [Thm ("real_assoc_1",num_str real_assoc_1),
neuper@37954	455	Thm ("real_assoc_2",num_str real_assoc_2),
neuper@37954	456	Thm ("real_diff_minus",num_str real_diff_minus),
neuper@37954	457	Thm ("real_unari_minus",num_str real_unari_minus),
neuper@37954	458	Thm ("realpow_multI",num_str realpow_multI),
neuper@37954	459	Calc ("op +",eval_binop "#add_"),
neuper@37954	460	Calc ("op -",eval_binop "#sub_"),
neuper@37954	461	Calc ("op *",eval_binop "#mult_"),
neuper@37954	462	Calc ("HOL.divide", eval_cancel "#divide_"),
neuper@37954	463	Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
neuper@37954	464	Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37954	465	Rls_ reduce_012
neuper@37954	466	],
neuper@37954	467	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	468	}:rls);
neuper@37954	469
neuper@37954	470	ruleset' := overwritelthy thy (!ruleset',
neuper@37954	471	[("cancel_leading_coeff",cancel_leading_coeff),
neuper@37954	472	("complete_square",complete_square),
neuper@37954	473	("PolyEq_erls",PolyEq_erls),(FIXXXME:del with rls.rls')
neuper@37954	474	("polyeq_simplify",polyeq_simplify)]);
neuper@37954	475
neuper@37954	476
neuper@37954	477	(* ------------- polySolve ------------------ *)
neuper@37954	478	(* -- d0 -- *)
neuper@37954	479	(isolate the bound variable in an d0 equation; 'bdv' is a meta-constant)
neuper@37954	480	val d0_polyeq_simplify = prep_rls(
neuper@37954	481	Rls {id = "d0_polyeq_simplify", preconds = [],
neuper@37954	482	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	483	erls = PolyEq_erls,
neuper@37954	484	srls = Erls,
neuper@37954	485	calc = [],
neuper@37954	486	(asm_thm = [],)
neuper@37954	487	rules = [Thm("d0_true",num_str d0_true),
neuper@37954	488	Thm("d0_false",num_str d0_false)
neuper@37954	489	],
neuper@37954	490	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	491	}:rls);
neuper@37954	492
neuper@37954	493	(* -- d1 -- *)
neuper@37954	494	(isolate the bound variable in an d1 equation; 'bdv' is a meta-constant)
neuper@37954	495	val d1_polyeq_simplify = prep_rls(
neuper@37954	496	Rls {id = "d1_polyeq_simplify", preconds = [],
neuper@37954	497	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	498	erls = PolyEq_erls,
neuper@37954	499	srls = Erls,
neuper@37954	500	calc = [],
neuper@37954	501	(asm_thm = [("d1_isolate_div","")],)
neuper@37954	502	rules = [
neuper@37954	503	Thm("d1_isolate_add1",num_str d1_isolate_add1),
neuper@37954	504	(* a+bx=0 -> bx=-a *)
neuper@37954	505	Thm("d1_isolate_add2",num_str d1_isolate_add2),
neuper@37954	506	(* a+ x=0 -> x=-a *)
neuper@37954	507	Thm("d1_isolate_div",num_str d1_isolate_div)
neuper@37954	508	(* bx=c -> x=c/b *)
neuper@37954	509	],
neuper@37954	510	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	511	}:rls);
neuper@37954	512
neuper@37954	513	(* -- d2 -- *)
neuper@37954	514	(* isolate the bound variable in an d2 equation with bdv only;
neuper@37954	515	'bdv' is a meta-constant*)
neuper@37954	516	val d2_polyeq_bdv_only_simplify = prep_rls(
neuper@37954	517	Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [],
neuper@37954	518	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	519	erls = PolyEq_erls,
neuper@37954	520	srls = Erls,
neuper@37954	521	calc = [],
neuper@37954	522	(*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
neuper@37954	523	("d2_isolate_div","")],*)
neuper@37954	524	rules = [Thm("d2_prescind1",num_str d2_prescind1),
neuper@37954	525	(* ax+bx^2=0 -> x(a+bx)=0 *)
neuper@37954	526	Thm("d2_prescind2",num_str d2_prescind2),
neuper@37954	527	(* ax+ x^2=0 -> x(a+ x)=0 *)
neuper@37954	528	Thm("d2_prescind3",num_str d2_prescind3),
neuper@37954	529	(* x+bx^2=0 -> x(1+bx)=0 *)
neuper@37954	530	Thm("d2_prescind4",num_str d2_prescind4),
neuper@37954	531	(* x+ x^2=0 -> x(1+ x)=0 *)
neuper@37954	532	Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
neuper@37954	533	(* x^2=c -> x=+-sqrt(c)*)
neuper@37954	534	Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
neuper@37954	535	(* [0<c] x^2=c -> [] *)
neuper@37954	536	Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
neuper@37954	537	(* x^2=0 -> x=0 *)
neuper@37954	538	Thm("d2_reduce_equation1",num_str d2_reduce_equation1),
neuper@37954	539	(* x(a+bx)=0 -> x=0 \| a+bx=0*)
neuper@37954	540	Thm("d2_reduce_equation2",num_str d2_reduce_equation2),
neuper@37954	541	(* x(a+ x)=0 -> x=0 \| a+ x=0*)
neuper@37954	542	Thm("d2_isolate_div",num_str d2_isolate_div)
neuper@37954	543	(* bx^2=c -> x^2=c/b*)
neuper@37954	544	],
neuper@37954	545	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	546	}:rls);
neuper@37954	547
neuper@37954	548	(* isolate the bound variable in an d2 equation with sqrt only;
neuper@37954	549	'bdv' is a meta-constant*)
neuper@37954	550	val d2_polyeq_sq_only_simplify = prep_rls(
neuper@37954	551	Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
neuper@37954	552	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	553	erls = PolyEq_erls,
neuper@37954	554	srls = Erls,
neuper@37954	555	calc = [],
neuper@37954	556	(*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
neuper@37954	557	("d2_isolate_div","")],*)
neuper@37954	558	rules = [Thm("d2_isolate_add1",num_str d2_isolate_add1),
neuper@37954	559	(* a+ bx^2=0 -> bx^2=(-1)a*)
neuper@37954	560	Thm("d2_isolate_add2",num_str d2_isolate_add2),
neuper@37954	561	(* a+ x^2=0 -> x^2=(-1)a*)
neuper@37954	562	Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
neuper@37954	563	(* x^2=0 -> x=0 *)
neuper@37954	564	Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
neuper@37954	565	(* x^2=c -> x=+-sqrt(c)*)
neuper@37954	566	Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
neuper@37954	567	(* [c<0] x^2=c -> x=[] *)
neuper@37954	568	Thm("d2_isolate_div",num_str d2_isolate_div)
neuper@37954	569	(* bx^2=c -> x^2=c/b*)
neuper@37954	570	],
neuper@37954	571	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	572	}:rls);
neuper@37954	573
neuper@37954	574	(* isolate the bound variable in an d2 equation with pqFormula;
neuper@37954	575	'bdv' is a meta-constant*)
neuper@37954	576	val d2_polyeq_pqFormula_simplify = prep_rls(
neuper@37954	577	Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
neuper@37954	578	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@37954	579	srls = Erls, calc = [],
neuper@37954	580	rules = [Thm("d2_pqformula1",num_str d2_pqformula1),
neuper@37954	581	(* q+px+ x^2=0 *)
neuper@37954	582	Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg),
neuper@37954	583	(* q+px+ x^2=0 *)
neuper@37954	584	Thm("d2_pqformula2",num_str d2_pqformula2),
neuper@37954	585	(* q+px+1x^2=0 *)
neuper@37954	586	Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg),
neuper@37954	587	(* q+px+1x^2=0 *)
neuper@37954	588	Thm("d2_pqformula3",num_str d2_pqformula3),
neuper@37954	589	(* q+ x+ x^2=0 *)
neuper@37954	590	Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg),
neuper@37954	591	(* q+ x+ x^2=0 *)
neuper@37954	592	Thm("d2_pqformula4",num_str d2_pqformula4),
neuper@37954	593	(* q+ x+1x^2=0 *)
neuper@37954	594	Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg),
neuper@37954	595	(* q+ x+1x^2=0 *)
neuper@37954	596	Thm("d2_pqformula5",num_str d2_pqformula5),
neuper@37954	597	(* qx+ x^2=0 *)
neuper@37954	598	Thm("d2_pqformula6",num_str d2_pqformula6),
neuper@37954	599	(* qx+1x^2=0 *)
neuper@37954	600	Thm("d2_pqformula7",num_str d2_pqformula7),
neuper@37954	601	(* x+ x^2=0 *)
neuper@37954	602	Thm("d2_pqformula8",num_str d2_pqformula8),
neuper@37954	603	(* x+1x^2=0 *)
neuper@37954	604	Thm("d2_pqformula9",num_str d2_pqformula9),
neuper@37954	605	(* q +1x^2=0 *)
neuper@37954	606	Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg),
neuper@37954	607	(* q +1x^2=0 *)
neuper@37954	608	Thm("d2_pqformula10",num_str d2_pqformula10),
neuper@37954	609	(* q + x^2=0 *)
neuper@37954	610	Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg),
neuper@37954	611	(* q + x^2=0 *)
neuper@37954	612	Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
neuper@37954	613	(* x^2=0 *)
neuper@37954	614	Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3)
neuper@37954	615	(* 1x^2=0 *)
neuper@37954	616	],
neuper@37954	617	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	618	}:rls);
neuper@37954	619
neuper@37954	620	(* isolate the bound variable in an d2 equation with abcFormula;
neuper@37954	621	'bdv' is a meta-constant*)
neuper@37954	622	val d2_polyeq_abcFormula_simplify = prep_rls(
neuper@37954	623	Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
neuper@37954	624	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@37954	625	srls = Erls, calc = [],
neuper@37954	626	rules = [Thm("d2_abcformula1",num_str d2_abcformula1),
neuper@37954	627	(c+bx+cx^2=0 )
neuper@37954	628	Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg),
neuper@37954	629	(c+bx+cx^2=0 )
neuper@37954	630	Thm("d2_abcformula2",num_str d2_abcformula2),
neuper@37954	631	(c+ x+cx^2=0 )
neuper@37954	632	Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg),
neuper@37954	633	(c+ x+cx^2=0 )
neuper@37954	634	Thm("d2_abcformula3",num_str d2_abcformula3),
neuper@37954	635	(c+bx+ x^2=0 )
neuper@37954	636	Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg),
neuper@37954	637	(c+bx+ x^2=0 )
neuper@37954	638	Thm("d2_abcformula4",num_str d2_abcformula4),
neuper@37954	639	(c+ x+ x^2=0 )
neuper@37954	640	Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg),
neuper@37954	641	(c+ x+ x^2=0 )
neuper@37954	642	Thm("d2_abcformula5",num_str d2_abcformula5),
neuper@37954	643	(c+ cx^2=0 )
neuper@37954	644	Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg),
neuper@37954	645	(c+ cx^2=0 )
neuper@37954	646	Thm("d2_abcformula6",num_str d2_abcformula6),
neuper@37954	647	(c+ x^2=0 )
neuper@37954	648	Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg),
neuper@37954	649	(c+ x^2=0 )
neuper@37954	650	Thm("d2_abcformula7",num_str d2_abcformula7),
neuper@37954	651	(* bx+ax^2=0 *)
neuper@37954	652	Thm("d2_abcformula8",num_str d2_abcformula8),
neuper@37954	653	(* bx+ x^2=0 *)
neuper@37954	654	Thm("d2_abcformula9",num_str d2_abcformula9),
neuper@37954	655	(* x+ax^2=0 *)
neuper@37954	656	Thm("d2_abcformula10",num_str d2_abcformula10),
neuper@37954	657	(* x+ x^2=0 *)
neuper@37954	658	Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
neuper@37954	659	(* x^2=0 *)
neuper@37954	660	Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3)
neuper@37954	661	(* bx^2=0 *)
neuper@37954	662	],
neuper@37954	663	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	664	}:rls);
neuper@37954	665
neuper@37954	666	(* isolate the bound variable in an d2 equation;
neuper@37954	667	'bdv' is a meta-constant*)
neuper@37954	668	val d2_polyeq_simplify = prep_rls(
neuper@37954	669	Rls {id = "d2_polyeq_simplify", preconds = [],
neuper@37954	670	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@37954	671	srls = Erls, calc = [],
neuper@37954	672	rules = [Thm("d2_pqformula1",num_str d2_pqformula1),
neuper@37954	673	(* p+qx+ x^2=0 *)
neuper@37954	674	Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg),
neuper@37954	675	(* p+qx+ x^2=0 *)
neuper@37954	676	Thm("d2_pqformula2",num_str d2_pqformula2),
neuper@37954	677	(* p+qx+1x^2=0 *)
neuper@37954	678	Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg),
neuper@37954	679	(* p+qx+1x^2=0 *)
neuper@37954	680	Thm("d2_pqformula3",num_str d2_pqformula3),
neuper@37954	681	(* p+ x+ x^2=0 *)
neuper@37954	682	Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg),
neuper@37954	683	(* p+ x+ x^2=0 *)
neuper@37954	684	Thm("d2_pqformula4",num_str d2_pqformula4),
neuper@37954	685	(* p+ x+1x^2=0 *)
neuper@37954	686	Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg),
neuper@37954	687	(* p+ x+1x^2=0 *)
neuper@37954	688	Thm("d2_abcformula1",num_str d2_abcformula1),
neuper@37954	689	(* c+bx+cx^2=0 *)
neuper@37954	690	Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg),
neuper@37954	691	(* c+bx+cx^2=0 *)
neuper@37954	692	Thm("d2_abcformula2",num_str d2_abcformula2),
neuper@37954	693	(* c+ x+cx^2=0 *)
neuper@37954	694	Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg),
neuper@37954	695	(* c+ x+cx^2=0 *)
neuper@37954	696	Thm("d2_prescind1",num_str d2_prescind1),
neuper@37954	697	(* ax+bx^2=0 -> x(a+bx)=0 *)
neuper@37954	698	Thm("d2_prescind2",num_str d2_prescind2),
neuper@37954	699	(* ax+ x^2=0 -> x(a+ x)=0 *)
neuper@37954	700	Thm("d2_prescind3",num_str d2_prescind3),
neuper@37954	701	(* x+bx^2=0 -> x(1+bx)=0 *)
neuper@37954	702	Thm("d2_prescind4",num_str d2_prescind4),
neuper@37954	703	(* x+ x^2=0 -> x(1+ x)=0 *)
neuper@37954	704	Thm("d2_isolate_add1",num_str d2_isolate_add1),
neuper@37954	705	(* a+ bx^2=0 -> bx^2=(-1)a*)
neuper@37954	706	Thm("d2_isolate_add2",num_str d2_isolate_add2),
neuper@37954	707	(* a+ x^2=0 -> x^2=(-1)a*)
neuper@37954	708	Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
neuper@37954	709	(* x^2=c -> x=+-sqrt(c)*)
neuper@37954	710	Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
neuper@37954	711	(* [c<0] x^2=c -> x=[]*)
neuper@37954	712	Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
neuper@37954	713	(* x^2=0 -> x=0 *)
neuper@37954	714	Thm("d2_reduce_equation1",num_str d2_reduce_equation1),
neuper@37954	715	(* x(a+bx)=0 -> x=0 \| a+bx=0*)
neuper@37954	716	Thm("d2_reduce_equation2",num_str d2_reduce_equation2),
neuper@37954	717	(* x(a+ x)=0 -> x=0 \| a+ x=0*)
neuper@37954	718	Thm("d2_isolate_div",num_str d2_isolate_div)
neuper@37954	719	(* bx^2=c -> x^2=c/b*)
neuper@37954	720	],
neuper@37954	721	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	722	}:rls);
neuper@37954	723
neuper@37954	724	(* -- d3 -- *)
neuper@37954	725	(* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
neuper@37954	726	val d3_polyeq_simplify = prep_rls(
neuper@37954	727	Rls {id = "d3_polyeq_simplify", preconds = [],
neuper@37954	728	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@37954	729	srls = Erls, calc = [],
neuper@37954	730	rules =
neuper@37954	731	[Thm("d3_reduce_equation1",num_str d3_reduce_equation1),
neuper@37954	732	(abdv + bbdv^^^2 + cbdv^^^3=0) =
neuper@37954	733	(bdv=0 \| (a + bbdv + cbdv^^^2=0)*)
neuper@37954	734	Thm("d3_reduce_equation2",num_str d3_reduce_equation2),
neuper@37954	735	(* bdv + bbdv^^^2 + cbdv^^^3=0) =
neuper@37954	736	(bdv=0 \| (1 + bbdv + cbdv^^^2=0)*)
neuper@37954	737	Thm("d3_reduce_equation3",num_str d3_reduce_equation3),
neuper@37954	738	(abdv + bdv^^^2 + c*bdv^^^3=0) =
neuper@37954	739	(bdv=0 \| (a + bdv + cbdv^^^2=0))
neuper@37954	740	Thm("d3_reduce_equation4",num_str d3_reduce_equation4),
neuper@37954	741	(* bdv + bdv^^^2 + c*bdv^^^3=0) =
neuper@37954	742	(bdv=0 \| (1 + bdv + cbdv^^^2=0))
neuper@37954	743	Thm("d3_reduce_equation5",num_str d3_reduce_equation5),
neuper@37954	744	(abdv + b*bdv^^^2 + bdv^^^3=0) =
neuper@37954	745	(bdv=0 \| (a + bbdv + bdv^^^2=0))
neuper@37954	746	Thm("d3_reduce_equation6",num_str d3_reduce_equation6),
neuper@37954	747	(* bdv + b*bdv^^^2 + bdv^^^3=0) =
neuper@37954	748	(bdv=0 \| (1 + bbdv + bdv^^^2=0))
neuper@37954	749	Thm("d3_reduce_equation7",num_str d3_reduce_equation7),
neuper@37954	750	(abdv + bdv^^^2 + bdv^^^3=0) =
neuper@37954	751	(bdv=0 \| (1 + bdv + bdv^^^2=0)*)
neuper@37954	752	Thm("d3_reduce_equation8",num_str d3_reduce_equation8),
neuper@37954	753	(* bdv + bdv^^^2 + bdv^^^3=0) =
neuper@37954	754	(bdv=0 \| (1 + bdv + bdv^^^2=0)*)
neuper@37954	755	Thm("d3_reduce_equation9",num_str d3_reduce_equation9),
neuper@37954	756	(abdv + c*bdv^^^3=0) =
neuper@37954	757	(bdv=0 \| (a + cbdv^^^2=0))
neuper@37954	758	Thm("d3_reduce_equation10",num_str d3_reduce_equation10),
neuper@37954	759	(* bdv + c*bdv^^^3=0) =
neuper@37954	760	(bdv=0 \| (1 + cbdv^^^2=0))
neuper@37954	761	Thm("d3_reduce_equation11",num_str d3_reduce_equation11),
neuper@37954	762	(abdv + bdv^^^3=0) =
neuper@37954	763	(bdv=0 \| (a + bdv^^^2=0)*)
neuper@37954	764	Thm("d3_reduce_equation12",num_str d3_reduce_equation12),
neuper@37954	765	(* bdv + bdv^^^3=0) =
neuper@37954	766	(bdv=0 \| (1 + bdv^^^2=0)*)
neuper@37954	767	Thm("d3_reduce_equation13",num_str d3_reduce_equation13),
neuper@37954	768	(* bbdv^^^2 + cbdv^^^3=0) =
neuper@37954	769	(bdv=0 \| ( bbdv + cbdv^^^2=0)*)
neuper@37954	770	Thm("d3_reduce_equation14",num_str d3_reduce_equation14),
neuper@37954	771	(* bdv^^^2 + c*bdv^^^3=0) =
neuper@37954	772	(bdv=0 \| ( bdv + cbdv^^^2=0))
neuper@37954	773	Thm("d3_reduce_equation15",num_str d3_reduce_equation15),
neuper@37954	774	(* b*bdv^^^2 + bdv^^^3=0) =
neuper@37954	775	(bdv=0 \| ( bbdv + bdv^^^2=0))
neuper@37954	776	Thm("d3_reduce_equation16",num_str d3_reduce_equation16),
neuper@37954	777	(* bdv^^^2 + bdv^^^3=0) =
neuper@37954	778	(bdv=0 \| ( bdv + bdv^^^2=0)*)
neuper@37954	779	Thm("d3_isolate_add1",num_str d3_isolate_add1),
neuper@37954	780	([\|Not(bdv occurs_in a)\|] ==> (a + bbdv^^^3=0) =
neuper@37954	781	(bdv=0 \| (bbdv^^^3=a))
neuper@37954	782	Thm("d3_isolate_add2",num_str d3_isolate_add2),
neuper@37954	783	(*[\|Not(bdv occurs_in a)\|] ==> (a + bdv^^^3=0) =
neuper@37954	784	(bdv=0 \| ( bdv^^^3=a)*)
neuper@37954	785	Thm("d3_isolate_div",num_str d3_isolate_div),
neuper@37954	786	([\|Not(b=0)\|] ==> (bbdv^^^3=c) = (bdv^^^3=c/b*)
neuper@37954	787	Thm("d3_root_equation2",num_str d3_root_equation2),
neuper@37954	788	((bdv^^^3=0) = (bdv=0) )
neuper@37954	789	Thm("d3_root_equation1",num_str d3_root_equation1)
neuper@37954	790	(bdv^^^3=c) = (bdv = nroot 3 c)
neuper@37954	791	],
neuper@37954	792	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	793	}:rls);
neuper@37954	794
neuper@37954	795	(* -- d4 -- *)
neuper@37954	796	(isolate the bound variable in an d4 equation; 'bdv' is a meta-constant)
neuper@37954	797	val d4_polyeq_simplify = prep_rls(
neuper@37954	798	Rls {id = "d4_polyeq_simplify", preconds = [],
neuper@37954	799	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@37954	800	srls = Erls, calc = [],
neuper@37954	801	rules =
neuper@37954	802	[Thm("d4_sub_u1",num_str d4_sub_u1)
neuper@37954	803	(* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
neuper@37954	804	],
neuper@37954	805	scr = Script ((term_of o the o (parse thy)) "empty_script")
neuper@37954	806	}:rls);
neuper@37954	807
neuper@37954	808	ruleset' :=
neuper@37954	809	overwritelthy thy
neuper@37954	810	(!ruleset',
neuper@37954	811	[("d0_polyeq_simplify", d0_polyeq_simplify),
neuper@37954	812	("d1_polyeq_simplify", d1_polyeq_simplify),
neuper@37954	813	("d2_polyeq_simplify", d2_polyeq_simplify),
neuper@37954	814	("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify),
neuper@37954	815	("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify),
neuper@37954	816	("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify),
neuper@37954	817	("d2_polyeq_abcFormula_simplify",
neuper@37954	818	d2_polyeq_abcFormula_simplify),
neuper@37954	819	("d3_polyeq_simplify", d3_polyeq_simplify),
neuper@37954	820	("d4_polyeq_simplify", d4_polyeq_simplify)
neuper@37954	821	]);
neuper@37954	822
neuper@37954	823	(------------------------problems------------------------)
neuper@37954	824	(*
neuper@37954	825	(get_pbt ["degree_2","polynomial","univariate","equation"]);
neuper@37954	826	show_ptyps();
neuper@37954	827	*)
neuper@37954	828
neuper@37954	829	(-------------------------poly-----------------------)
neuper@37954	830	store_pbt
neuper@37954	831	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly" [] e_pblID
neuper@37954	832	(["polynomial","univariate","equation"],
neuper@37954	833	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	834	("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))",
neuper@37954	835	"~((lhs e_) is_rootTerm_in (v_::real))",
neuper@37954	836	"~((rhs e_) is_rootTerm_in (v_::real))"]),
neuper@37954	837	("#Find" ,["solutions v_i_"])
neuper@37954	838	],
neuper@37954	839	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	840	[]));
neuper@37954	841	(--- d0 ---)
neuper@37954	842	store_pbt
neuper@37954	843	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg0" [] e_pblID
neuper@37954	844	(["degree_0","polynomial","univariate","equation"],
neuper@37954	845	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	846	("#Where" ,["matches (?a = 0) e_",
neuper@37954	847	"(lhs e_) is_poly_in v_",
neuper@37954	848	"((lhs e_) has_degree_in v_ ) = 0"
neuper@37954	849	]),
neuper@37954	850	("#Find" ,["solutions v_i_"])
neuper@37954	851	],
neuper@37954	852	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	853	[["PolyEq","solve_d0_polyeq_equation"]]));
neuper@37954	854
neuper@37954	855	(--- d1 ---)
neuper@37954	856	store_pbt
neuper@37954	857	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg1" [] e_pblID
neuper@37954	858	(["degree_1","polynomial","univariate","equation"],
neuper@37954	859	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	860	("#Where" ,["matches (?a = 0) e_",
neuper@37954	861	"(lhs e_) is_poly_in v_",
neuper@37954	862	"((lhs e_) has_degree_in v_ ) = 1"
neuper@37954	863	]),
neuper@37954	864	("#Find" ,["solutions v_i_"])
neuper@37954	865	],
neuper@37954	866	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	867	[["PolyEq","solve_d1_polyeq_equation"]]));
neuper@37954	868
neuper@37954	869	(--- d2 ---)
neuper@37954	870	store_pbt
neuper@37954	871	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2" [] e_pblID
neuper@37954	872	(["degree_2","polynomial","univariate","equation"],
neuper@37954	873	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	874	("#Where" ,["matches (?a = 0) e_",
neuper@37954	875	"(lhs e_) is_poly_in v_ ",
neuper@37954	876	"((lhs e_) has_degree_in v_ ) = 2"]),
neuper@37954	877	("#Find" ,["solutions v_i_"])
neuper@37954	878	],
neuper@37954	879	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	880	[["PolyEq","solve_d2_polyeq_equation"]]));
neuper@37954	881
neuper@37954	882	store_pbt
neuper@37954	883	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
neuper@37954	884	(["sq_only","degree_2","polynomial","univariate","equation"],
neuper@37954	885	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	886	("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ \| " ^
neuper@37954	887	"matches ( ?a + ?b*?v_^^^2 = 0) e_ \| " ^
neuper@37954	888	"matches ( ?v_^^^2 = 0) e_ \| " ^
neuper@37954	889	"matches ( ?b*?v_^^^2 = 0) e_" ,
neuper@37954	890	"Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &" ^
neuper@37954	891	"Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &" ^
neuper@37954	892	"Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &" ^
neuper@37954	893	"Not (matches (?a + ?b?v_ + ?c?v_^^^2 = 0) e_) &" ^
neuper@37954	894	"Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &" ^
neuper@37954	895	"Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &" ^
neuper@37954	896	"Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &" ^
neuper@37954	897	"Not (matches ( ?b?v_ + ?c?v_^^^2 = 0) e_)"]),
neuper@37954	898	("#Find" ,["solutions v_i_"])
neuper@37954	899	],
neuper@37954	900	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	901	[["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
neuper@37954	902
neuper@37954	903	store_pbt
neuper@37954	904	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
neuper@37954	905	(["bdv_only","degree_2","polynomial","univariate","equation"],
neuper@37954	906	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	907	("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ \| " ^
neuper@37954	908	"matches ( ?v_ + ?v_^^^2 = 0) e_ \| " ^
neuper@37954	909	"matches ( ?v_ + ?b*?v_^^^2 = 0) e_ \| " ^
neuper@37954	910	"matches (?a?v_ + ?b?v_^^^2 = 0) e_ \| " ^
neuper@37954	911	"matches ( ?v_^^^2 = 0) e_ \| " ^
neuper@37954	912	"matches ( ?b*?v_^^^2 = 0) e_ "]),
neuper@37954	913	("#Find" ,["solutions v_i_"])
neuper@37954	914	],
neuper@37954	915	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	916	[["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
neuper@37954	917
neuper@37954	918	store_pbt
neuper@37954	919	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_pq" [] e_pblID
neuper@37954	920	(["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37954	921	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	922	("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ \| " ^
neuper@37954	923	"matches (?a + ?v_^^^2 = 0) e_"]),
neuper@37954	924	("#Find" ,["solutions v_i_"])
neuper@37954	925	],
neuper@37954	926	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	927	[["PolyEq","solve_d2_polyeq_pq_equation"]]));
neuper@37954	928
neuper@37954	929	store_pbt
neuper@37954	930	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_abc" [] e_pblID
neuper@37954	931	(["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37954	932	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	933	("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ \| " ^
neuper@37954	934	"matches (?a + ?b*?v_^^^2 = 0) e_"]),
neuper@37954	935	("#Find" ,["solutions v_i_"])
neuper@37954	936	],
neuper@37954	937	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	938	[["PolyEq","solve_d2_polyeq_abc_equation"]]));
neuper@37954	939
neuper@37954	940	(--- d3 ---)
neuper@37954	941	store_pbt
neuper@37954	942	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg3" [] e_pblID
neuper@37954	943	(["degree_3","polynomial","univariate","equation"],
neuper@37954	944	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	945	("#Where" ,["matches (?a = 0) e_",
neuper@37954	946	"(lhs e_) is_poly_in v_ ",
neuper@37954	947	"((lhs e_) has_degree_in v_) = 3"]),
neuper@37954	948	("#Find" ,["solutions v_i_"])
neuper@37954	949	],
neuper@37954	950	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	951	[["PolyEq","solve_d3_polyeq_equation"]]));
neuper@37954	952
neuper@37954	953	(--- d4 ---)
neuper@37954	954	store_pbt
neuper@37954	955	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg4" [] e_pblID
neuper@37954	956	(["degree_4","polynomial","univariate","equation"],
neuper@37954	957	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	958	("#Where" ,["matches (?a = 0) e_",
neuper@37954	959	"(lhs e_) is_poly_in v_ ",
neuper@37954	960	"((lhs e_) has_degree_in v_) = 4"]),
neuper@37954	961	("#Find" ,["solutions v_i_"])
neuper@37954	962	],
neuper@37954	963	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	964	[(["PolyEq","solve_d4_polyeq_equation"])]));
neuper@37954	965
neuper@37954	966	(--- normalize ---)
neuper@37954	967	store_pbt
neuper@37954	968	(prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_norm" [] e_pblID
neuper@37954	969	(["normalize","polynomial","univariate","equation"],
neuper@37954	970	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	971	("#Where" ,["(Not((matches (?a = 0 ) e_ ))) \|" ^
neuper@37954	972	"(Not(((lhs e_) is_poly_in v_)))"]),
neuper@37954	973	("#Find" ,["solutions v_i_"])
neuper@37954	974	],
neuper@37954	975	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	976	[["PolyEq","normalize_poly"]]));
neuper@37954	977	(-------------------------expanded-----------------------)
neuper@37954	978	store_pbt
neuper@37954	979	(prep_pbt (theory "PolyEq") "pbl_equ_univ_expand" [] e_pblID
neuper@37954	980	(["expanded","univariate","equation"],
neuper@37954	981	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	982	("#Where" ,["matches (?a = 0) e_",
neuper@37954	983	"(lhs e_) is_expanded_in v_ "]),
neuper@37954	984	("#Find" ,["solutions v_i_"])
neuper@37954	985	],
neuper@37954	986	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	987	[]));
neuper@37954	988
neuper@37954	989	(--- d2 ---)
neuper@37954	990	store_pbt
neuper@37954	991	(prep_pbt (theory "PolyEq") "pbl_equ_univ_expand_deg2" [] e_pblID
neuper@37954	992	(["degree_2","expanded","univariate","equation"],
neuper@37954	993	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	994	("#Where" ,["((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	995	("#Find" ,["solutions v_i_"])
neuper@37954	996	],
neuper@37954	997	PolyEq_prls, SOME "solve (e_::bool, v_)",
neuper@37954	998	[["PolyEq","complete_square"]]));
neuper@37954	999
neuper@37954	1000
neuper@37954	1001	"-------------------------methods-----------------------";
neuper@37954	1002	store_met
neuper@37954	1003	(prep_met (theory "PolyEq") "met_polyeq" [] e_metID
neuper@37954	1004	(["PolyEq"],
neuper@37954	1005	[],
neuper@37954	1006	{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@37954	1007	crls=PolyEq_crls, nrls=norm_Rational}, "empty_script"));
neuper@37954	1008
neuper@37954	1009	store_met
neuper@37954	1010	(prep_met (theory "PolyEq") "met_polyeq_norm" [] e_metID
neuper@37954	1011	(["PolyEq","normalize_poly"],
neuper@37954	1012	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1013	("#Where" ,["(Not((matches (?a = 0 ) e_ ))) \|" ^
neuper@37954	1014	"(Not(((lhs e_) is_poly_in v_)))"]),
neuper@37954	1015	("#Find" ,["solutions v_i_"])
neuper@37954	1016	],
neuper@37954	1017	{rew_ord'="termlessI",
neuper@37954	1018	rls'=PolyEq_erls,
neuper@37954	1019	srls=e_rls,
neuper@37954	1020	prls=PolyEq_prls,
neuper@37954	1021	calc=[],
neuper@37954	1022	crls=PolyEq_crls, nrls=norm_Rational
neuper@37954	1023	"Script Normalize_poly (e_::bool) (v_::real) = " ^
neuper@37954	1024	"(let e_ =((Try (Rewrite all_left False)) @@ " ^
neuper@37954	1025	" (Try (Repeat (Rewrite makex1_x False))) @@ " ^
neuper@37954	1026	" (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
neuper@37954	1027	" (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1028	" make_ratpoly_in False))) @@ " ^
neuper@37954	1029	" (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_ " ^
neuper@37954	1030	" in (SubProblem (PolyEq_,[polynomial,univariate,equation], " ^
neuper@37954	1031	" [no_met]) [bool_ e_, real_ v_]))"
neuper@37954	1032	));
neuper@37954	1033
neuper@37954	1034	store_met
neuper@37954	1035	(prep_met (theory "PolyEq") "met_polyeq_d0" [] e_metID
neuper@37954	1036	(["PolyEq","solve_d0_polyeq_equation"],
neuper@37954	1037	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1038	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1039	"((lhs e_) has_degree_in v_) = 0"]),
neuper@37954	1040	("#Find" ,["solutions v_i_"])
neuper@37954	1041	],
neuper@37954	1042	{rew_ord'="termlessI",
neuper@37954	1043	rls'=PolyEq_erls,
neuper@37954	1044	srls=e_rls,
neuper@37954	1045	prls=PolyEq_prls,
neuper@37954	1046	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1047	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1048	"Script Solve_d0_polyeq_equation (e_::bool) (v_::real) = " ^
neuper@37954	1049	"(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1050	" d0_polyeq_simplify False))) e_ " ^
neuper@37954	1051	" in ((Or_to_List e_)::bool list))"
neuper@37954	1052	));
neuper@37954	1053
neuper@37954	1054	store_met
neuper@37954	1055	(prep_met (theory "PolyEq") "met_polyeq_d1" [] e_metID
neuper@37954	1056	(["PolyEq","solve_d1_polyeq_equation"],
neuper@37954	1057	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1058	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1059	"((lhs e_) has_degree_in v_) = 1"]),
neuper@37954	1060	("#Find" ,["solutions v_i_"])
neuper@37954	1061	],
neuper@37954	1062	{rew_ord'="termlessI",
neuper@37954	1063	rls'=PolyEq_erls,
neuper@37954	1064	srls=e_rls,
neuper@37954	1065	prls=PolyEq_prls,
neuper@37954	1066	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1067	crls=PolyEq_crls, nrls=norm_Rational(*,
neuper@37954	1068	(* asm_rls=["d1_polyeq_simplify"],*)
neuper@37954	1069	asm_rls=[],
neuper@37954	1070	asm_thm=[("d1_isolate_div","")]*)},
neuper@37954	1071	"Script Solve_d1_polyeq_equation (e_::bool) (v_::real) = " ^
neuper@37954	1072	"(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1073	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1074	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1075	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
neuper@37954	1076	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1077	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1078	));
neuper@37954	1079
neuper@37954	1080	store_met
neuper@37954	1081	(prep_met (theory "PolyEq") "met_polyeq_d22" [] e_metID
neuper@37954	1082	(["PolyEq","solve_d2_polyeq_equation"],
neuper@37954	1083	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1084	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1085	"((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	1086	("#Find" ,["solutions v_i_"])
neuper@37954	1087	],
neuper@37954	1088	{rew_ord'="termlessI",
neuper@37954	1089	rls'=PolyEq_erls,
neuper@37954	1090	srls=e_rls,
neuper@37954	1091	prls=PolyEq_prls,
neuper@37954	1092	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1093	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1094	"Script Solve_d2_polyeq_equation (e_::bool) (v_::real) = " ^
neuper@37954	1095	" (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1096	" d2_polyeq_simplify True)) @@ " ^
neuper@37954	1097	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1098	" (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1099	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1100	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1101	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
neuper@37954	1102	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1103	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1104	));
neuper@37954	1105
neuper@37954	1106	store_met
neuper@37954	1107	(prep_met (theory "PolyEq") "met_polyeq_d2_bdvonly" [] e_metID
neuper@37954	1108	(["PolyEq","solve_d2_polyeq_bdvonly_equation"],
neuper@37954	1109	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1110	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1111	"((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	1112	("#Find" ,["solutions v_i_"])
neuper@37954	1113	],
neuper@37954	1114	{rew_ord'="termlessI",
neuper@37954	1115	rls'=PolyEq_erls,
neuper@37954	1116	srls=e_rls,
neuper@37954	1117	prls=PolyEq_prls,
neuper@37954	1118	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1119	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1120	"Script Solve_d2_polyeq_bdvonly_equation (e_::bool) (v_::real) =" ^
neuper@37954	1121	" (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1122	" d2_polyeq_bdv_only_simplify True)) @@ " ^
neuper@37954	1123	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1124	" (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1125	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1126	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1127	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
neuper@37954	1128	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1129	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1130	));
neuper@37954	1131
neuper@37954	1132	store_met
neuper@37954	1133	(prep_met (theory "PolyEq") "met_polyeq_d2_sqonly" [] e_metID
neuper@37954	1134	(["PolyEq","solve_d2_polyeq_sqonly_equation"],
neuper@37954	1135	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1136	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1137	"((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	1138	("#Find" ,["solutions v_i_"])
neuper@37954	1139	],
neuper@37954	1140	{rew_ord'="termlessI",
neuper@37954	1141	rls'=PolyEq_erls,
neuper@37954	1142	srls=e_rls,
neuper@37954	1143	prls=PolyEq_prls,
neuper@37954	1144	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1145	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1146	"Script Solve_d2_polyeq_sqonly_equation (e_::bool) (v_::real) =" ^
neuper@37954	1147	" (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1148	" d2_polyeq_sq_only_simplify True)) @@ " ^
neuper@37954	1149	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1150	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_; " ^
neuper@37954	1151	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1152	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1153	));
neuper@37954	1154
neuper@37954	1155	store_met
neuper@37954	1156	(prep_met (theory "PolyEq") "met_polyeq_d2_pq" [] e_metID
neuper@37954	1157	(["PolyEq","solve_d2_polyeq_pq_equation"],
neuper@37954	1158	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1159	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1160	"((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	1161	("#Find" ,["solutions v_i_"])
neuper@37954	1162	],
neuper@37954	1163	{rew_ord'="termlessI",
neuper@37954	1164	rls'=PolyEq_erls,
neuper@37954	1165	srls=e_rls,
neuper@37954	1166	prls=PolyEq_prls,
neuper@37954	1167	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1168	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1169	"Script Solve_d2_polyeq_pq_equation (e_::bool) (v_::real) = " ^
neuper@37954	1170	" (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1171	" d2_polyeq_pqFormula_simplify True)) @@ " ^
neuper@37954	1172	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1173	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
neuper@37954	1174	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1175	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1176	));
neuper@37954	1177
neuper@37954	1178	store_met
neuper@37954	1179	(prep_met (theory "PolyEq") "met_polyeq_d2_abc" [] e_metID
neuper@37954	1180	(["PolyEq","solve_d2_polyeq_abc_equation"],
neuper@37954	1181	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1182	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1183	"((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	1184	("#Find" ,["solutions v_i_"])
neuper@37954	1185	],
neuper@37954	1186	{rew_ord'="termlessI",
neuper@37954	1187	rls'=PolyEq_erls,
neuper@37954	1188	srls=e_rls,
neuper@37954	1189	prls=PolyEq_prls,
neuper@37954	1190	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1191	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1192	"Script Solve_d2_polyeq_abc_equation (e_::bool) (v_::real) = " ^
neuper@37954	1193	" (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1194	" d2_polyeq_abcFormula_simplify True)) @@ " ^
neuper@37954	1195	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1196	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
neuper@37954	1197	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1198	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1199	));
neuper@37954	1200
neuper@37954	1201	store_met
neuper@37954	1202	(prep_met (theory "PolyEq") "met_polyeq_d3" [] e_metID
neuper@37954	1203	(["PolyEq","solve_d3_polyeq_equation"],
neuper@37954	1204	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1205	("#Where" ,["(lhs e_) is_poly_in v_ ",
neuper@37954	1206	"((lhs e_) has_degree_in v_) = 3"]),
neuper@37954	1207	("#Find" ,["solutions v_i_"])
neuper@37954	1208	],
neuper@37954	1209	{rew_ord'="termlessI",
neuper@37954	1210	rls'=PolyEq_erls,
neuper@37954	1211	srls=e_rls,
neuper@37954	1212	prls=PolyEq_prls,
neuper@37954	1213	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1214	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1215	"Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = " ^
neuper@37954	1216	" (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1217	" d3_polyeq_simplify True)) @@ " ^
neuper@37954	1218	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1219	" (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1220	" d2_polyeq_simplify True)) @@ " ^
neuper@37954	1221	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1222	" (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
neuper@37954	1223	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1224	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37954	1225	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
neuper@37954	1226	" (L_::bool list) = ((Or_to_List e_)::bool list) " ^
neuper@37954	1227	" in Check_elementwise L_ {(v_::real). Assumptions} )"
neuper@37954	1228	));
neuper@37954	1229
neuper@37954	1230	(.solves all expanded (ie. normalized) terms of degree 2.)
neuper@37954	1231	(*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
neuper@37954	1232	by 'PolyEq_erls'; restricted until Float.thy is implemented*)
neuper@37954	1233	store_met
neuper@37954	1234	(prep_met (theory "PolyEq") "met_polyeq_complsq" [] e_metID
neuper@37954	1235	(["PolyEq","complete_square"],
neuper@37954	1236	[("#Given" ,["equality e_","solveFor v_"]),
neuper@37954	1237	("#Where" ,["matches (?a = 0) e_",
neuper@37954	1238	"((lhs e_) has_degree_in v_) = 2"]),
neuper@37954	1239	("#Find" ,["solutions v_i_"])
neuper@37954	1240	],
neuper@37954	1241	{rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
neuper@37954	1242	calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
neuper@37954	1243	crls=PolyEq_crls, nrls=norm_Rational},
neuper@37954	1244	"Script Complete_square (e_::bool) (v_::real) = " ^
neuper@37954	1245	"(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))" ^
neuper@37954	1246	" @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) " ^
neuper@37954	1247	" @@ (Try (Rewrite square_explicit1 False)) " ^
neuper@37954	1248	" @@ (Try (Rewrite square_explicit2 False)) " ^
neuper@37954	1249	" @@ (Rewrite root_plus_minus True) " ^
neuper@37954	1250	" @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) " ^
neuper@37954	1251	" @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) " ^
neuper@37954	1252	" @@ (Try (Repeat " ^
neuper@37954	1253	" (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) " ^
neuper@37954	1254	" @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
neuper@37954	1255	" @@ (Try (Repeat (Calculate sqrt_)))) e_ " ^
neuper@37954	1256	" in ((Or_to_List e_)::bool list))"
neuper@37954	1257	));
neuper@37954	1258
neuper@37954	1259
neuper@37954	1260	(* termorder hacked by MG *)
neuper@37954	1261	local (. for make_polynomial_in .)
neuper@37954	1262
neuper@37954	1263	open Term; (* for type order = EQUAL \| LESS \| GREATER *)
neuper@37954	1264
neuper@37954	1265	fun pr_ord EQUAL = "EQUAL"
neuper@37954	1266	\| pr_ord LESS = "LESS"
neuper@37954	1267	\| pr_ord GREATER = "GREATER";
neuper@37954	1268
neuper@37954	1269	fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
neuper@37954	1270	\| dest_hd' x (t as Free (a, T)) =
neuper@37954	1271	if x = t then ((("\|\|\|\|\|\|\|\|\|\|\|\|\|", 0), T), 0) (WN)
neuper@37954	1272	else (((a, 0), T), 1)
neuper@37954	1273	\| dest_hd' x (Var v) = (v, 2)
neuper@37954	1274	\| dest_hd' x (Bound i) = ((("", i), dummyT), 3)
neuper@37954	1275	\| dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
neuper@37954	1276
neuper@37954	1277	fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =
neuper@37954	1278	(case x of (WN)
neuper@37954	1279	(Free (xstr,_)) =>
neuper@37954	1280	(if xstr = var then 1000*(the (int_of_str pot)) else 3)
neuper@37954	1281	\| _ => raise error ("size_of_term' called with subst = "^
neuper@37954	1282	(term2str x)))
neuper@37954	1283	\| size_of_term' x (Free (subst,_)) =
neuper@37954	1284	(case x of
neuper@37954	1285	(Free (xstr,_)) => (if xstr = subst then 1000 else 1)
neuper@37954	1286	\| _ => raise error ("size_of_term' called with subst = "^
neuper@37954	1287	(term2str x)))
neuper@37954	1288	\| size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
neuper@37954	1289	\| size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
neuper@37954	1290	\| size_of_term' x _ = 1;
neuper@37954	1291
neuper@37954	1292
neuper@37954	1293	fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
neuper@37954	1294	(case term_ord' x pr thy (t, u) of EQUAL => typ_ord (T, U) \| ord => ord)
neuper@37954	1295	\| term_ord' x pr thy (t, u) =
neuper@37954	1296	(if pr then
neuper@37954	1297	let
neuper@37954	1298	val (f, ts) = strip_comb t and (g, us) = strip_comb u;
neuper@37954	1299	val _=writeln("t= f@ts= \""^
neuper@37954	1300	((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
neuper@37954	1301	(commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
neuper@37954	1302	val _=writeln("u= g@us= \""^
neuper@37954	1303	((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
neuper@37954	1304	(commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
neuper@37954	1305	val _=writeln("size_of_term(t,u)= ("^
neuper@37954	1306	(string_of_int(size_of_term' x t))^", "^
neuper@37954	1307	(string_of_int(size_of_term' x u))^")");
neuper@37954	1308	val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
neuper@37954	1309	val _=writeln("terms_ord(ts,us) = "^
neuper@37954	1310	((pr_ord o (terms_ord x) str false)(ts,us)));
neuper@37954	1311	val _=writeln("-------");
neuper@37954	1312	in () end
neuper@37954	1313	else ();
neuper@37954	1314	case int_ord (size_of_term' x t, size_of_term' x u) of
neuper@37954	1315	EQUAL =>
neuper@37954	1316	let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
neuper@37954	1317	(case hd_ord x (f, g) of EQUAL => (terms_ord x str pr) (ts, us)
neuper@37954	1318	\| ord => ord)
neuper@37954	1319	end
neuper@37954	1320	\| ord => ord)
neuper@37954	1321	and hd_ord x (f, g) = (* ~ term.ML *)
neuper@37954	1322	prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' x f,
neuper@37954	1323	dest_hd' x g)
neuper@37954	1324	and terms_ord x str pr (ts, us) =
neuper@37954	1325	list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us);
neuper@37954	1326	in
neuper@37954	1327
neuper@37954	1328	fun ord_make_polynomial_in (pr:bool) thy subst tu =
neuper@37954	1329	let
neuper@37954	1330	(* val _=writeln("*** subs variable is: "^(subst2str subst)); *)
neuper@37954	1331	in
neuper@37954	1332	case subst of
neuper@37954	1333	(_,x)::_ => (term_ord' x pr thy tu = LESS)
neuper@37954	1334	\| _ => raise error ("ord_make_polynomial_in called with subst = "^
neuper@37954	1335	(subst2str subst))
neuper@37954	1336	end;
neuper@37954	1337	end;
neuper@37954	1338
neuper@37954	1339	val order_add_mult_in = prep_rls(
neuper@37954	1340	Rls{id = "order_add_mult_in", preconds = [],
neuper@37954	1341	rew_ord = ("ord_make_polynomial_in",
neuper@37954	1342	ord_make_polynomial_in false Poly.thy),
neuper@37954	1343	erls = e_rls,srls = Erls,
neuper@37954	1344	calc = [],
neuper@37954	1345	(asm_thm = [],)
neuper@37954	1346	rules = [Thm ("real_mult_commute",num_str real_mult_commute),
neuper@37954	1347	(* z * w = w * z *)
neuper@37954	1348	Thm ("real_mult_left_commute",num_str real_mult_left_commute),
neuper@37954	1349	(z1.0 (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@37954	1350	Thm ("real_mult_assoc",num_str real_mult_assoc),
neuper@37954	1351	(z1.0 z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37965	1352	Thm ("add_commute",num_str @{thm add_commute}),
neuper@37954	1353	(z + w = w + z)
neuper@37965	1354	Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37954	1355	(x + (y + z) = y + (x + z))
neuper@37965	1356	Thm ("add_assoc",num_str @{thm add_assoc})
neuper@37954	1357	(z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0))
neuper@37954	1358	], scr = EmptyScr}:rls);
neuper@37954	1359
neuper@37954	1360	val collect_bdv = prep_rls(
neuper@37954	1361	Rls{id = "collect_bdv", preconds = [],
neuper@37954	1362	rew_ord = ("dummy_ord", dummy_ord),
neuper@37954	1363	erls = e_rls,srls = Erls,
neuper@37954	1364	calc = [],
neuper@37954	1365	(asm_thm = [],)
neuper@37954	1366	rules = [Thm ("bdv_collect_1",num_str bdv_collect_1),
neuper@37954	1367	Thm ("bdv_collect_2",num_str bdv_collect_2),
neuper@37954	1368	Thm ("bdv_collect_3",num_str bdv_collect_3),
neuper@37954	1369
neuper@37954	1370	Thm ("bdv_collect_assoc1_1",num_str bdv_collect_assoc1_1),
neuper@37954	1371	Thm ("bdv_collect_assoc1_2",num_str bdv_collect_assoc1_2),
neuper@37954	1372	Thm ("bdv_collect_assoc1_3",num_str bdv_collect_assoc1_3),
neuper@37954	1373
neuper@37954	1374	Thm ("bdv_collect_assoc2_1",num_str bdv_collect_assoc2_1),
neuper@37954	1375	Thm ("bdv_collect_assoc2_2",num_str bdv_collect_assoc2_2),
neuper@37954	1376	Thm ("bdv_collect_assoc2_3",num_str bdv_collect_assoc2_3),
neuper@37954	1377
neuper@37954	1378
neuper@37954	1379	Thm ("bdv_n_collect_1",num_str bdv_n_collect_1),
neuper@37954	1380	Thm ("bdv_n_collect_2",num_str bdv_n_collect_2),
neuper@37954	1381	Thm ("bdv_n_collect_3",num_str bdv_n_collect_3),
neuper@37954	1382
neuper@37954	1383	Thm ("bdv_n_collect_assoc1_1",num_str bdv_n_collect_assoc1_1),
neuper@37954	1384	Thm ("bdv_n_collect_assoc1_2",num_str bdv_n_collect_assoc1_2),
neuper@37954	1385	Thm ("bdv_n_collect_assoc1_3",num_str bdv_n_collect_assoc1_3),
neuper@37954	1386
neuper@37954	1387	Thm ("bdv_n_collect_assoc2_1",num_str bdv_n_collect_assoc2_1),
neuper@37954	1388	Thm ("bdv_n_collect_assoc2_2",num_str bdv_n_collect_assoc2_2),
neuper@37954	1389	Thm ("bdv_n_collect_assoc2_3",num_str bdv_n_collect_assoc2_3)
neuper@37954	1390	], scr = EmptyScr}:rls);
neuper@37954	1391
neuper@37954	1392	(*.transforms an arbitrary term without roots to a polynomial [4]
neuper@37954	1393	according to knowledge/Poly.sml.*)
neuper@37954	1394	val make_polynomial_in = prep_rls(
neuper@37954	1395	Seq {id = "make_polynomial_in", preconds = []:term list,
neuper@37954	1396	rew_ord = ("dummy_ord", dummy_ord),
neuper@37954	1397	erls = Atools_erls, srls = Erls,
neuper@37954	1398	calc = [], (asm_thm = [],)
neuper@37954	1399	rules = [Rls_ expand_poly,
neuper@37954	1400	Rls_ order_add_mult_in,
neuper@37954	1401	Rls_ simplify_power,
neuper@37954	1402	Rls_ collect_numerals,
neuper@37954	1403	Rls_ reduce_012,
neuper@37954	1404	Thm ("realpow_oneI",num_str realpow_oneI),
neuper@37954	1405	Rls_ discard_parentheses,
neuper@37954	1406	Rls_ collect_bdv
neuper@37954	1407	],
neuper@37954	1408	scr = EmptyScr
neuper@37954	1409	}:rls);
neuper@37954	1410
neuper@37954	1411	val separate_bdvs =
neuper@37954	1412	append_rls "separate_bdvs"
neuper@37954	1413	collect_bdv
neuper@37954	1414	[Thm ("separate_bdv", num_str separate_bdv),
neuper@37954	1415	("?a ?bdv / ?b = ?a / ?b * ?bdv"*)
neuper@37954	1416	Thm ("separate_bdv_n", num_str separate_bdv_n),
neuper@37954	1417	Thm ("separate_1_bdv", num_str separate_1_bdv),
neuper@37954	1418	("?bdv / ?b = (1 / ?b) ?bdv"*)
neuper@37954	1419	Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
neuper@37954	1420	("?bdv ^^^ ?n / ?b = 1 / ?b ?bdv ^^^ ?n"*)
neuper@37965	1421	Thm ("nadd_divide_distrib",
neuper@37965	1422	num_str @{thm nadd_divide_distrib})
neuper@37954	1423	(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
neuper@37954	1424	WN051031 DOES NOT BELONG TO HERE*)
neuper@37954	1425	];
neuper@37954	1426	val make_ratpoly_in = prep_rls(
neuper@37954	1427	Seq {id = "make_ratpoly_in", preconds = []:term list,
neuper@37954	1428	rew_ord = ("dummy_ord", dummy_ord),
neuper@37954	1429	erls = Atools_erls, srls = Erls,
neuper@37954	1430	calc = [], (asm_thm = [],)
neuper@37954	1431	rules = [Rls_ norm_Rational,
neuper@37954	1432	Rls_ order_add_mult_in,
neuper@37954	1433	Rls_ discard_parentheses,
neuper@37954	1434	Rls_ separate_bdvs,
neuper@37954	1435	(* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
neuper@37954	1436	Rls_ cancel_p
neuper@37954	1437	(Calc ("HOL.divide" ,eval_cancel "#divide_") too weak!)
neuper@37954	1438	],
neuper@37954	1439	scr = EmptyScr}:rls);
neuper@37954	1440
neuper@37954	1441
neuper@37954	1442	ruleset' := overwritelthy thy (!ruleset',
neuper@37954	1443	[("order_add_mult_in", order_add_mult_in),
neuper@37954	1444	("collect_bdv", collect_bdv),
neuper@37954	1445	("make_polynomial_in", make_polynomial_in),
neuper@37954	1446	("make_ratpoly_in", make_ratpoly_in),
neuper@37954	1447	("separate_bdvs", separate_bdvs)
neuper@37954	1448	]);
neuper@37954	1449	*}
neuper@37954	1450
neuper@37906	1451	end
neuper@37906	1452
neuper@37906	1453
neuper@37906	1454
neuper@37906	1455
neuper@37906	1456
neuper@37906	1457

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 31 Aug 2010 15:36:57 +0200
branch	isac-update-Isa09-2
changeset 37965	9c11005c33b8
parent 37954	4022d670753c
child 37966	78938fc8e022
permissions	-rw-r--r--