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

author	Thomas Leh <t.leh@gmx.at>
	Tue, 26 Jul 2011 13:27:59 +0200
branch	decompose-isar
changeset 42197	7497ff20f1e8
parent 42133	f9a7294e6cd6
child 42203	8e216c5001bd
permissions	-rw-r--r--