wneuper/isa: src/Tools/isac/Knowledge/PolyEq.thy@468809a52c9f (annotated)

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Wed, 08 Sep 2010 16:28:24 +0200
branch	isac-update-Isa09-2
changeset 37989	468809a52c9f
parent 37984	972a73d7c50b
child 37990	24609758d219
permissions	-rw-r--r--