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

author	Thomas Leh <t.leh@gmx.at>
	Tue, 26 Jul 2011 15:25:28 +0200
branch	decompose-isar
changeset 42203	8e216c5001bd
parent 42197	7497ff20f1e8
child 42211	51c3c007d7fd
permissions	-rw-r--r--