wneuper/isa: src/Tools/isac/Knowledge/PolyEq.thy@977788dfed26 (annotated)

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Sat, 17 Mar 2012 11:06:46 +0100
changeset 42394	977788dfed26
parent 42318	b4f9b188373e
child 42424	725f0c91bbc4
permissions	-rw-r--r--