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

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 21 Oct 2013 09:03:50 +0200
changeset 52148	aabc6c8e930a
parent 52140	b7cdced159f1
child 52155	e4ddf21390fd
permissions	-rw-r--r--