wneuper/isa: src/Tools/isac/Knowledge/PolyEq.thy@6f1d3415dc68 (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@42451	437	erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
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@48763	452	],scr = Prog ((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@42451	458	erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
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@48763	465	scr = Prog ((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@42451	473	calc = [], errpatts = [],
neuper@37969	474	rules = [Thm ("real_assoc_1",num_str @{thm real_assoc_1}),
neuper@37969	475	Thm ("real_assoc_2",num_str @{thm real_assoc_2}),
neuper@37969	476	Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
neuper@37969	477	Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
neuper@37969	478	Thm ("realpow_multI",num_str @{thm realpow_multI}),
neuper@38014	479	Calc ("Groups.plus_class.plus",eval_binop "#add_"),
neuper@38014	480	Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
neuper@38034	481	Calc ("Groups.times_class.times",eval_binop "#mult_"),
neuper@48789	482	Calc ("Fields.inverse_class.divide", eval_cancel "#divide_e"),
neuper@37982	483	Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
neuper@37954	484	Calc ("Atools.pow" ,eval_binop "#power_"),
neuper@37954	485	Rls_ reduce_012
neuper@37954	486	],
neuper@48763	487	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	488	}:rls);
neuper@37954	489
neuper@37967	490	ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954	491	[("cancel_leading_coeff",cancel_leading_coeff),
neuper@37954	492	("complete_square",complete_square),
neuper@37954	493	("PolyEq_erls",PolyEq_erls),(FIXXXME:del with rls.rls')
neuper@37954	494	("polyeq_simplify",polyeq_simplify)]);
neuper@37989	495	*}
neuper@52125	496	setup {* KEStore_Elems.add_rlss
neuper@52125	497	[("cancel_leading_coeff", (Context.theory_name @{theory}, cancel_leading_coeff)),
neuper@52125	498	("complete_square", (Context.theory_name @{theory}, complete_square)),
neuper@52125	499	("PolyEq_erls", (Context.theory_name @{theory}, PolyEq_erls)),
neuper@52125	500	("polyeq_simplify", (Context.theory_name @{theory}, polyeq_simplify))] *}
neuper@37989	501	ML{*
neuper@37954	502
neuper@37954	503	(* ------------- polySolve ------------------ *)
neuper@37954	504	(* -- d0 -- *)
neuper@37954	505	(isolate the bound variable in an d0 equation; 'bdv' is a meta-constant)
neuper@37954	506	val d0_polyeq_simplify = prep_rls(
neuper@37954	507	Rls {id = "d0_polyeq_simplify", preconds = [],
neuper@37954	508	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	509	erls = PolyEq_erls,
neuper@37954	510	srls = Erls,
neuper@42451	511	calc = [], errpatts = [],
neuper@37969	512	rules = [Thm("d0_true",num_str @{thm d0_true}),
neuper@37969	513	Thm("d0_false",num_str @{thm d0_false})
neuper@37954	514	],
neuper@48763	515	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	516	}:rls);
neuper@37954	517
neuper@37954	518	(* -- d1 -- *)
neuper@37954	519	(isolate the bound variable in an d1 equation; 'bdv' is a meta-constant)
neuper@37954	520	val d1_polyeq_simplify = prep_rls(
neuper@37954	521	Rls {id = "d1_polyeq_simplify", preconds = [],
neuper@37954	522	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	523	erls = PolyEq_erls,
neuper@37954	524	srls = Erls,
neuper@42451	525	calc = [], errpatts = [],
neuper@37954	526	rules = [
neuper@37969	527	Thm("d1_isolate_add1",num_str @{thm d1_isolate_add1}),
neuper@37954	528	(* a+bx=0 -> bx=-a *)
neuper@37969	529	Thm("d1_isolate_add2",num_str @{thm d1_isolate_add2}),
neuper@37954	530	(* a+ x=0 -> x=-a *)
neuper@37969	531	Thm("d1_isolate_div",num_str @{thm d1_isolate_div})
neuper@37954	532	(* bx=c -> x=c/b *)
neuper@37954	533	],
neuper@48763	534	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	535	}:rls);
neuper@37954	536
neuper@37989	537	*}
neuper@42394	538	subsection {* degree 2 *}
neuper@37989	539	ML{*
neuper@42394	540	(* isolate the bound variable in an d2 equation with bdv only;
neuper@42394	541	"bdv" is a meta-constant substituted for the "x" below by isac's rewriter. *)
neuper@37954	542	val d2_polyeq_bdv_only_simplify = prep_rls(
neuper@42394	543	Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
neuper@42451	544	erls = PolyEq_erls, srls = Erls, calc = [], errpatts = [],
neuper@42394	545	rules =
neuper@42394	546	[Thm ("d2_prescind1", num_str @{thm d2_prescind1}), (* ax+bx^2=0 -> x(a+bx)=0 *)
neuper@42394	547	Thm ("d2_prescind2", num_str @{thm d2_prescind2}), (* ax+ x^2=0 -> x(a+ x)=0 *)
neuper@42394	548	Thm ("d2_prescind3", num_str @{thm d2_prescind3}), (* x+bx^2=0 -> x(1+bx)=0 *)
neuper@42394	549	Thm ("d2_prescind4", num_str @{thm d2_prescind4}), (* x+ x^2=0 -> x(1+ x)=0 *)
neuper@42394	550	Thm ("d2_sqrt_equation1", num_str @{thm d2_sqrt_equation1}), (* x^2=c -> x=+-sqrt(c) *)
neuper@42394	551	Thm ("d2_sqrt_equation1_neg", num_str @{thm d2_sqrt_equation1_neg}), (* [0<c] x^2=c -> []*)
neuper@42394	552	Thm ("d2_sqrt_equation2", num_str @{thm d2_sqrt_equation2}), (* x^2=0 -> x=0 *)
neuper@42394	553	Thm ("d2_reduce_equation1", num_str @{thm d2_reduce_equation1}),(* x(a+bx)=0 -> x=0 \|a+bx=0*)
neuper@42394	554	Thm ("d2_reduce_equation2", num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 \|a+ x=0*)
neuper@42394	555	Thm ("d2_isolate_div", num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
neuper@42394	556	],
neuper@48763	557	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	558	}:rls);
neuper@37989	559	*}
neuper@37989	560	ML{*
neuper@37954	561	(* isolate the bound variable in an d2 equation with sqrt only;
neuper@37954	562	'bdv' is a meta-constant*)
neuper@37954	563	val d2_polyeq_sq_only_simplify = prep_rls(
neuper@37954	564	Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
neuper@37954	565	rew_ord = ("e_rew_ord",e_rew_ord),
neuper@37954	566	erls = PolyEq_erls,
neuper@37954	567	srls = Erls,
neuper@42451	568	calc = [], errpatts = [],
neuper@37954	569	(*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
neuper@37954	570	("d2_isolate_div","")],*)
neuper@37969	571	rules = [Thm("d2_isolate_add1",num_str @{thm d2_isolate_add1}),
neuper@37954	572	(* a+ bx^2=0 -> bx^2=(-1)a*)
neuper@37969	573	Thm("d2_isolate_add2",num_str @{thm d2_isolate_add2}),
neuper@37954	574	(* a+ x^2=0 -> x^2=(-1)a*)
neuper@37969	575	Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
neuper@37954	576	(* x^2=0 -> x=0 *)
neuper@37969	577	Thm("d2_sqrt_equation1",num_str @{thm d2_sqrt_equation1}),
neuper@37954	578	(* x^2=c -> x=+-sqrt(c)*)
neuper@37969	579	Thm("d2_sqrt_equation1_neg",num_str @{thm d2_sqrt_equation1_neg}),
neuper@37954	580	(* [c<0] x^2=c -> x=[] *)
neuper@37969	581	Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
neuper@37954	582	(* bx^2=c -> x^2=c/b*)
neuper@37954	583	],
neuper@48763	584	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	585	}:rls);
neuper@37989	586	*}
neuper@37989	587	ML{*
neuper@37954	588	(* isolate the bound variable in an d2 equation with pqFormula;
neuper@37954	589	'bdv' is a meta-constant*)
neuper@37954	590	val d2_polyeq_pqFormula_simplify = prep_rls(
neuper@37954	591	Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
neuper@37954	592	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@42451	593	srls = Erls, calc = [], errpatts = [],
neuper@37969	594	rules = [Thm("d2_pqformula1",num_str @{thm d2_pqformula1}),
neuper@37954	595	(* q+px+ x^2=0 *)
neuper@37969	596	Thm("d2_pqformula1_neg",num_str @{thm d2_pqformula1_neg}),
neuper@37954	597	(* q+px+ x^2=0 *)
neuper@37969	598	Thm("d2_pqformula2",num_str @{thm d2_pqformula2}),
neuper@37954	599	(* q+px+1x^2=0 *)
neuper@37969	600	Thm("d2_pqformula2_neg",num_str @{thm d2_pqformula2_neg}),
neuper@37954	601	(* q+px+1x^2=0 *)
neuper@37969	602	Thm("d2_pqformula3",num_str @{thm d2_pqformula3}),
neuper@37954	603	(* q+ x+ x^2=0 *)
neuper@37969	604	Thm("d2_pqformula3_neg",num_str @{thm d2_pqformula3_neg}),
neuper@37954	605	(* q+ x+ x^2=0 *)
neuper@37969	606	Thm("d2_pqformula4",num_str @{thm d2_pqformula4}),
neuper@37954	607	(* q+ x+1x^2=0 *)
neuper@37969	608	Thm("d2_pqformula4_neg",num_str @{thm d2_pqformula4_neg}),
neuper@37954	609	(* q+ x+1x^2=0 *)
neuper@37969	610	Thm("d2_pqformula5",num_str @{thm d2_pqformula5}),
neuper@37954	611	(* qx+ x^2=0 *)
neuper@37969	612	Thm("d2_pqformula6",num_str @{thm d2_pqformula6}),
neuper@37954	613	(* qx+1x^2=0 *)
neuper@37969	614	Thm("d2_pqformula7",num_str @{thm d2_pqformula7}),
neuper@37954	615	(* x+ x^2=0 *)
neuper@37969	616	Thm("d2_pqformula8",num_str @{thm d2_pqformula8}),
neuper@37954	617	(* x+1x^2=0 *)
neuper@37969	618	Thm("d2_pqformula9",num_str @{thm d2_pqformula9}),
neuper@37954	619	(* q +1x^2=0 *)
neuper@37969	620	Thm("d2_pqformula9_neg",num_str @{thm d2_pqformula9_neg}),
neuper@37954	621	(* q +1x^2=0 *)
neuper@37969	622	Thm("d2_pqformula10",num_str @{thm d2_pqformula10}),
neuper@37954	623	(* q + x^2=0 *)
neuper@37969	624	Thm("d2_pqformula10_neg",num_str @{thm d2_pqformula10_neg}),
neuper@37954	625	(* q + x^2=0 *)
neuper@37969	626	Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
neuper@37954	627	(* x^2=0 *)
neuper@37969	628	Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
neuper@37954	629	(* 1x^2=0 *)
neuper@48763	630	],scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	631	}:rls);
neuper@37989	632	*}
neuper@37989	633	ML{*
neuper@37954	634	(* isolate the bound variable in an d2 equation with abcFormula;
neuper@37954	635	'bdv' is a meta-constant*)
neuper@37954	636	val d2_polyeq_abcFormula_simplify = prep_rls(
neuper@37954	637	Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
neuper@37954	638	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@42451	639	srls = Erls, calc = [], errpatts = [],
neuper@37969	640	rules = [Thm("d2_abcformula1",num_str @{thm d2_abcformula1}),
neuper@37954	641	(c+bx+cx^2=0 )
neuper@37969	642	Thm("d2_abcformula1_neg",num_str @{thm d2_abcformula1_neg}),
neuper@37954	643	(c+bx+cx^2=0 )
neuper@37969	644	Thm("d2_abcformula2",num_str @{thm d2_abcformula2}),
neuper@37954	645	(c+ x+cx^2=0 )
neuper@37969	646	Thm("d2_abcformula2_neg",num_str @{thm d2_abcformula2_neg}),
neuper@37954	647	(c+ x+cx^2=0 )
neuper@37969	648	Thm("d2_abcformula3",num_str @{thm d2_abcformula3}),
neuper@37954	649	(c+bx+ x^2=0 )
neuper@37969	650	Thm("d2_abcformula3_neg",num_str @{thm d2_abcformula3_neg}),
neuper@37954	651	(c+bx+ x^2=0 )
neuper@37969	652	Thm("d2_abcformula4",num_str @{thm d2_abcformula4}),
neuper@37954	653	(c+ x+ x^2=0 )
neuper@37969	654	Thm("d2_abcformula4_neg",num_str @{thm d2_abcformula4_neg}),
neuper@37954	655	(c+ x+ x^2=0 )
neuper@37969	656	Thm("d2_abcformula5",num_str @{thm d2_abcformula5}),
neuper@37954	657	(c+ cx^2=0 )
neuper@37969	658	Thm("d2_abcformula5_neg",num_str @{thm d2_abcformula5_neg}),
neuper@37954	659	(c+ cx^2=0 )
neuper@37969	660	Thm("d2_abcformula6",num_str @{thm d2_abcformula6}),
neuper@37954	661	(c+ x^2=0 )
neuper@37969	662	Thm("d2_abcformula6_neg",num_str @{thm d2_abcformula6_neg}),
neuper@37954	663	(c+ x^2=0 )
neuper@37969	664	Thm("d2_abcformula7",num_str @{thm d2_abcformula7}),
neuper@37954	665	(* bx+ax^2=0 *)
neuper@37969	666	Thm("d2_abcformula8",num_str @{thm d2_abcformula8}),
neuper@37954	667	(* bx+ x^2=0 *)
neuper@37969	668	Thm("d2_abcformula9",num_str @{thm d2_abcformula9}),
neuper@37954	669	(* x+ax^2=0 *)
neuper@37969	670	Thm("d2_abcformula10",num_str @{thm d2_abcformula10}),
neuper@37954	671	(* x+ x^2=0 *)
neuper@37969	672	Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
neuper@37954	673	(* x^2=0 *)
neuper@37969	674	Thm("d2_sqrt_equation3",num_str @{thm d2_sqrt_equation3})
neuper@37954	675	(* bx^2=0 *)
neuper@37954	676	],
neuper@48763	677	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	678	}:rls);
neuper@37989	679	*}
neuper@37989	680	ML{*
neuper@37954	681
neuper@37954	682	(* isolate the bound variable in an d2 equation;
neuper@37954	683	'bdv' is a meta-constant*)
neuper@37954	684	val d2_polyeq_simplify = prep_rls(
neuper@37954	685	Rls {id = "d2_polyeq_simplify", preconds = [],
neuper@37954	686	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@42451	687	srls = Erls, calc = [], errpatts = [],
neuper@37969	688	rules = [Thm("d2_pqformula1",num_str @{thm d2_pqformula1}),
neuper@37954	689	(* p+qx+ x^2=0 *)
neuper@37969	690	Thm("d2_pqformula1_neg",num_str @{thm d2_pqformula1_neg}),
neuper@37954	691	(* p+qx+ x^2=0 *)
neuper@37969	692	Thm("d2_pqformula2",num_str @{thm d2_pqformula2}),
neuper@37954	693	(* p+qx+1x^2=0 *)
neuper@37969	694	Thm("d2_pqformula2_neg",num_str @{thm d2_pqformula2_neg}),
neuper@37954	695	(* p+qx+1x^2=0 *)
neuper@37969	696	Thm("d2_pqformula3",num_str @{thm d2_pqformula3}),
neuper@37954	697	(* p+ x+ x^2=0 *)
neuper@37969	698	Thm("d2_pqformula3_neg",num_str @{thm d2_pqformula3_neg}),
neuper@37954	699	(* p+ x+ x^2=0 *)
neuper@37969	700	Thm("d2_pqformula4",num_str @{thm d2_pqformula4}),
neuper@37954	701	(* p+ x+1x^2=0 *)
neuper@37969	702	Thm("d2_pqformula4_neg",num_str @{thm d2_pqformula4_neg}),
neuper@37954	703	(* p+ x+1x^2=0 *)
neuper@37969	704	Thm("d2_abcformula1",num_str @{thm d2_abcformula1}),
neuper@37954	705	(* c+bx+cx^2=0 *)
neuper@37969	706	Thm("d2_abcformula1_neg",num_str @{thm d2_abcformula1_neg}),
neuper@37954	707	(* c+bx+cx^2=0 *)
neuper@37969	708	Thm("d2_abcformula2",num_str @{thm d2_abcformula2}),
neuper@37954	709	(* c+ x+cx^2=0 *)
neuper@37969	710	Thm("d2_abcformula2_neg",num_str @{thm d2_abcformula2_neg}),
neuper@37954	711	(* c+ x+cx^2=0 *)
neuper@37969	712	Thm("d2_prescind1",num_str @{thm d2_prescind1}),
neuper@37954	713	(* ax+bx^2=0 -> x(a+bx)=0 *)
neuper@37969	714	Thm("d2_prescind2",num_str @{thm d2_prescind2}),
neuper@37954	715	(* ax+ x^2=0 -> x(a+ x)=0 *)
neuper@37969	716	Thm("d2_prescind3",num_str @{thm d2_prescind3}),
neuper@37954	717	(* x+bx^2=0 -> x(1+bx)=0 *)
neuper@37969	718	Thm("d2_prescind4",num_str @{thm d2_prescind4}),
neuper@37954	719	(* x+ x^2=0 -> x(1+ x)=0 *)
neuper@37969	720	Thm("d2_isolate_add1",num_str @{thm d2_isolate_add1}),
neuper@37954	721	(* a+ bx^2=0 -> bx^2=(-1)a*)
neuper@37969	722	Thm("d2_isolate_add2",num_str @{thm d2_isolate_add2}),
neuper@37954	723	(* a+ x^2=0 -> x^2=(-1)a*)
neuper@37969	724	Thm("d2_sqrt_equation1",num_str @{thm d2_sqrt_equation1}),
neuper@37954	725	(* x^2=c -> x=+-sqrt(c)*)
neuper@37969	726	Thm("d2_sqrt_equation1_neg",num_str @{thm d2_sqrt_equation1_neg}),
neuper@37954	727	(* [c<0] x^2=c -> x=[]*)
neuper@37969	728	Thm("d2_sqrt_equation2",num_str @{thm d2_sqrt_equation2}),
neuper@37954	729	(* x^2=0 -> x=0 *)
neuper@37969	730	Thm("d2_reduce_equation1",num_str @{thm d2_reduce_equation1}),
neuper@37954	731	(* x(a+bx)=0 -> x=0 \| a+bx=0*)
neuper@37969	732	Thm("d2_reduce_equation2",num_str @{thm d2_reduce_equation2}),
neuper@37954	733	(* x(a+ x)=0 -> x=0 \| a+ x=0*)
neuper@37969	734	Thm("d2_isolate_div",num_str @{thm d2_isolate_div})
neuper@37954	735	(* bx^2=c -> x^2=c/b*)
neuper@37954	736	],
neuper@48763	737	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	738	}:rls);
neuper@37989	739	*}
neuper@37989	740	ML{*
neuper@37954	741
neuper@37954	742	(* -- d3 -- *)
neuper@37954	743	(* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
neuper@37954	744	val d3_polyeq_simplify = prep_rls(
neuper@37954	745	Rls {id = "d3_polyeq_simplify", preconds = [],
neuper@37954	746	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@42451	747	srls = Erls, calc = [], errpatts = [],
neuper@37954	748	rules =
neuper@37969	749	[Thm("d3_reduce_equation1",num_str @{thm d3_reduce_equation1}),
neuper@37954	750	(abdv + bbdv^^^2 + cbdv^^^3=0) =
neuper@37954	751	(bdv=0 \| (a + bbdv + cbdv^^^2=0)*)
neuper@37969	752	Thm("d3_reduce_equation2",num_str @{thm d3_reduce_equation2}),
neuper@37954	753	(* bdv + bbdv^^^2 + cbdv^^^3=0) =
neuper@37954	754	(bdv=0 \| (1 + bbdv + cbdv^^^2=0)*)
neuper@37969	755	Thm("d3_reduce_equation3",num_str @{thm d3_reduce_equation3}),
neuper@37954	756	(abdv + bdv^^^2 + c*bdv^^^3=0) =
neuper@37954	757	(bdv=0 \| (a + bdv + cbdv^^^2=0))
neuper@37969	758	Thm("d3_reduce_equation4",num_str @{thm d3_reduce_equation4}),
neuper@37954	759	(* bdv + bdv^^^2 + c*bdv^^^3=0) =
neuper@37954	760	(bdv=0 \| (1 + bdv + cbdv^^^2=0))
neuper@37969	761	Thm("d3_reduce_equation5",num_str @{thm d3_reduce_equation5}),
neuper@37954	762	(abdv + b*bdv^^^2 + bdv^^^3=0) =
neuper@37954	763	(bdv=0 \| (a + bbdv + bdv^^^2=0))
neuper@37969	764	Thm("d3_reduce_equation6",num_str @{thm d3_reduce_equation6}),
neuper@37954	765	(* bdv + b*bdv^^^2 + bdv^^^3=0) =
neuper@37954	766	(bdv=0 \| (1 + bbdv + bdv^^^2=0))
neuper@37969	767	Thm("d3_reduce_equation7",num_str @{thm d3_reduce_equation7}),
neuper@37954	768	(abdv + bdv^^^2 + bdv^^^3=0) =
neuper@37954	769	(bdv=0 \| (1 + bdv + bdv^^^2=0)*)
neuper@37969	770	Thm("d3_reduce_equation8",num_str @{thm d3_reduce_equation8}),
neuper@37954	771	(* bdv + bdv^^^2 + bdv^^^3=0) =
neuper@37954	772	(bdv=0 \| (1 + bdv + bdv^^^2=0)*)
neuper@37969	773	Thm("d3_reduce_equation9",num_str @{thm d3_reduce_equation9}),
neuper@37954	774	(abdv + c*bdv^^^3=0) =
neuper@37954	775	(bdv=0 \| (a + cbdv^^^2=0))
neuper@37969	776	Thm("d3_reduce_equation10",num_str @{thm d3_reduce_equation10}),
neuper@37954	777	(* bdv + c*bdv^^^3=0) =
neuper@37954	778	(bdv=0 \| (1 + cbdv^^^2=0))
neuper@37969	779	Thm("d3_reduce_equation11",num_str @{thm d3_reduce_equation11}),
neuper@37954	780	(abdv + bdv^^^3=0) =
neuper@37954	781	(bdv=0 \| (a + bdv^^^2=0)*)
neuper@37969	782	Thm("d3_reduce_equation12",num_str @{thm d3_reduce_equation12}),
neuper@37954	783	(* bdv + bdv^^^3=0) =
neuper@37954	784	(bdv=0 \| (1 + bdv^^^2=0)*)
neuper@37969	785	Thm("d3_reduce_equation13",num_str @{thm d3_reduce_equation13}),
neuper@37954	786	(* bbdv^^^2 + cbdv^^^3=0) =
neuper@37954	787	(bdv=0 \| ( bbdv + cbdv^^^2=0)*)
neuper@37969	788	Thm("d3_reduce_equation14",num_str @{thm d3_reduce_equation14}),
neuper@37954	789	(* bdv^^^2 + c*bdv^^^3=0) =
neuper@37954	790	(bdv=0 \| ( bdv + cbdv^^^2=0))
neuper@37969	791	Thm("d3_reduce_equation15",num_str @{thm d3_reduce_equation15}),
neuper@37954	792	(* b*bdv^^^2 + bdv^^^3=0) =
neuper@37954	793	(bdv=0 \| ( bbdv + bdv^^^2=0))
neuper@37969	794	Thm("d3_reduce_equation16",num_str @{thm d3_reduce_equation16}),
neuper@37954	795	(* bdv^^^2 + bdv^^^3=0) =
neuper@37954	796	(bdv=0 \| ( bdv + bdv^^^2=0)*)
neuper@37969	797	Thm("d3_isolate_add1",num_str @{thm d3_isolate_add1}),
neuper@37954	798	([\|Not(bdv occurs_in a)\|] ==> (a + bbdv^^^3=0) =
neuper@37954	799	(bdv=0 \| (bbdv^^^3=a))
neuper@37969	800	Thm("d3_isolate_add2",num_str @{thm d3_isolate_add2}),
neuper@37954	801	(*[\|Not(bdv occurs_in a)\|] ==> (a + bdv^^^3=0) =
neuper@37954	802	(bdv=0 \| ( bdv^^^3=a)*)
neuper@37969	803	Thm("d3_isolate_div",num_str @{thm d3_isolate_div}),
neuper@37954	804	([\|Not(b=0)\|] ==> (bbdv^^^3=c) = (bdv^^^3=c/b*)
neuper@37969	805	Thm("d3_root_equation2",num_str @{thm d3_root_equation2}),
neuper@37954	806	((bdv^^^3=0) = (bdv=0) )
neuper@37969	807	Thm("d3_root_equation1",num_str @{thm d3_root_equation1})
neuper@37954	808	(bdv^^^3=c) = (bdv = nroot 3 c)
neuper@37954	809	],
neuper@48763	810	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	811	}:rls);
neuper@37989	812	*}
neuper@37989	813	ML{*
neuper@37954	814
neuper@37954	815	(* -- d4 -- *)
neuper@37954	816	(isolate the bound variable in an d4 equation; 'bdv' is a meta-constant)
neuper@37954	817	val d4_polyeq_simplify = prep_rls(
neuper@37954	818	Rls {id = "d4_polyeq_simplify", preconds = [],
neuper@37954	819	rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
neuper@42451	820	srls = Erls, calc = [], errpatts = [],
neuper@37954	821	rules =
neuper@37989	822	[Thm("d4_sub_u1",num_str @{thm d4_sub_u1})
neuper@37954	823	(* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
neuper@37954	824	],
neuper@48763	825	scr = Prog ((term_of o the o (parse thy)) "empty_script")
neuper@37954	826	}:rls);
neuper@37954	827
neuper@37954	828	ruleset' :=
neuper@37967	829	overwritelthy @{theory}
neuper@37954	830	(!ruleset',
neuper@37954	831	[("d0_polyeq_simplify", d0_polyeq_simplify),
neuper@37954	832	("d1_polyeq_simplify", d1_polyeq_simplify),
neuper@37954	833	("d2_polyeq_simplify", d2_polyeq_simplify),
neuper@37954	834	("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify),
neuper@37954	835	("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify),
neuper@52125	836
neuper@37954	837	("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify),
neuper@52125	838	("d2_polyeq_abcFormula_simplify", d2_polyeq_abcFormula_simplify),
neuper@37954	839	("d3_polyeq_simplify", d3_polyeq_simplify),
neuper@37954	840	("d4_polyeq_simplify", d4_polyeq_simplify)
neuper@37954	841	]);
neuper@37989	842	*}
neuper@52125	843	setup {* KEStore_Elems.add_rlss
neuper@52125	844	[("d0_polyeq_simplify", (Context.theory_name @{theory}, d0_polyeq_simplify)),
neuper@52125	845	("d1_polyeq_simplify", (Context.theory_name @{theory}, d1_polyeq_simplify)),
neuper@52125	846	("d2_polyeq_simplify", (Context.theory_name @{theory}, d2_polyeq_simplify)),
neuper@52125	847	("d2_polyeq_bdv_only_simplify", (Context.theory_name @{theory}, d2_polyeq_bdv_only_simplify)),
neuper@52125	848	("d2_polyeq_sq_only_simplify", (Context.theory_name @{theory}, d2_polyeq_sq_only_simplify)),
neuper@52125	849
neuper@52125	850	("d2_polyeq_pqFormula_simplify",
neuper@52125	851	(Context.theory_name @{theory}, d2_polyeq_pqFormula_simplify)),
neuper@52125	852	("d2_polyeq_abcFormula_simplify",
neuper@52125	853	(Context.theory_name @{theory}, d2_polyeq_abcFormula_simplify)),
neuper@52125	854	("d3_polyeq_simplify", (Context.theory_name @{theory}, d3_polyeq_simplify)),
neuper@52125	855	("d4_polyeq_simplify", (Context.theory_name @{theory}, d4_polyeq_simplify))] *}
neuper@37989	856	ML{*
neuper@37954	857
neuper@37954	858	(------------------------problems------------------------)
neuper@37954	859	(*
neuper@37954	860	(get_pbt ["degree_2","polynomial","univariate","equation"]);
neuper@37954	861	show_ptyps();
neuper@37954	862	*)
neuper@37954	863
neuper@37954	864	(-------------------------poly-----------------------)
neuper@37954	865	store_pbt
neuper@37972	866	(prep_pbt thy "pbl_equ_univ_poly" [] e_pblID
neuper@37954	867	(["polynomial","univariate","equation"],
neuper@37981	868	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37982	869	("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
neuper@37982	870	"~((lhs e_e) is_rootTerm_in (v_v::real))",
neuper@37982	871	"~((rhs e_e) is_rootTerm_in (v_v::real))"]),
neuper@38012	872	("#Find" ,["solutions v_v'i'"])
neuper@37954	873	],
neuper@37981	874	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	875	[]));
neuper@37954	876	(--- d0 ---)
neuper@37954	877	store_pbt
neuper@37972	878	(prep_pbt thy "pbl_equ_univ_poly_deg0" [] e_pblID
neuper@37954	879	(["degree_0","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 ) = 0"
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_d0_polyeq_equation"]]));
neuper@37954	889
neuper@37954	890	(--- d1 ---)
neuper@37954	891	store_pbt
neuper@37972	892	(prep_pbt thy "pbl_equ_univ_poly_deg1" [] e_pblID
neuper@37954	893	(["degree_1","polynomial","univariate","equation"],
neuper@37981	894	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	895	("#Where" ,["matches (?a = 0) e_e",
neuper@37981	896	"(lhs e_e) is_poly_in v_v",
neuper@37981	897	"((lhs e_e) has_degree_in v_v ) = 1"
neuper@37954	898	]),
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_d1_polyeq_equation"]]));
neuper@37989	903	*}
neuper@37989	904	ML{*
neuper@37954	905	(--- d2 ---)
neuper@37954	906	store_pbt
neuper@37972	907	(prep_pbt thy "pbl_equ_univ_poly_deg2" [] e_pblID
neuper@37954	908	(["degree_2","polynomial","univariate","equation"],
neuper@37981	909	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	910	("#Where" ,["matches (?a = 0) e_e",
neuper@37981	911	"(lhs e_e) is_poly_in v_v ",
neuper@37981	912	"((lhs e_e) has_degree_in v_v ) = 2"]),
neuper@38012	913	("#Find" ,["solutions v_v'i'"])
neuper@37954	914	],
neuper@37981	915	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	916	[["PolyEq","solve_d2_polyeq_equation"]]));
neuper@37954	917
neuper@37954	918	store_pbt
neuper@37972	919	(prep_pbt thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
neuper@37954	920	(["sq_only","degree_2","polynomial","univariate","equation"],
neuper@37981	921	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	922	("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_e \| " ^
neuper@37981	923	"matches ( ?a + ?b*?v_^^^2 = 0) e_e \| " ^
neuper@37981	924	"matches ( ?v_^^^2 = 0) e_e \| " ^
neuper@37981	925	"matches ( ?b*?v_^^^2 = 0) e_e" ,
neuper@37981	926	"Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_e) &" ^
neuper@37981	927	"Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
neuper@37981	928	"Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
neuper@37981	929	"Not (matches (?a + ?b?v_ + ?c?v_^^^2 = 0) e_e) &" ^
neuper@37981	930	"Not (matches ( ?v_ + ?v_^^^2 = 0) e_e) &" ^
neuper@37981	931	"Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_e) &" ^
neuper@37981	932	"Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_e) &" ^
neuper@37981	933	"Not (matches ( ?b?v_ + ?c?v_^^^2 = 0) e_e)"]),
neuper@38012	934	("#Find" ,["solutions v_v'i'"])
neuper@37954	935	],
neuper@37981	936	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	937	[["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
neuper@37954	938
neuper@37954	939	store_pbt
neuper@37972	940	(prep_pbt thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
neuper@37954	941	(["bdv_only","degree_2","polynomial","univariate","equation"],
neuper@37981	942	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	943	("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_e \| " ^
neuper@37981	944	"matches ( ?v_ + ?v_^^^2 = 0) e_e \| " ^
neuper@37981	945	"matches ( ?v_ + ?b*?v_^^^2 = 0) e_e \| " ^
neuper@37981	946	"matches (?a?v_ + ?b?v_^^^2 = 0) e_e \| " ^
neuper@37981	947	"matches ( ?v_^^^2 = 0) e_e \| " ^
neuper@37981	948	"matches ( ?b*?v_^^^2 = 0) e_e "]),
neuper@38012	949	("#Find" ,["solutions v_v'i'"])
neuper@37954	950	],
neuper@37981	951	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	952	[["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
neuper@37954	953
neuper@37954	954	store_pbt
neuper@37972	955	(prep_pbt thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
neuper@37954	956	(["pqFormula","degree_2","polynomial","univariate","equation"],
neuper@37981	957	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	958	("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_e \| " ^
neuper@37981	959	"matches (?a + ?v_^^^2 = 0) e_e"]),
neuper@38012	960	("#Find" ,["solutions v_v'i'"])
neuper@37954	961	],
neuper@37981	962	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	963	[["PolyEq","solve_d2_polyeq_pq_equation"]]));
neuper@37954	964
neuper@37954	965	store_pbt
neuper@37972	966	(prep_pbt thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
neuper@37954	967	(["abcFormula","degree_2","polynomial","univariate","equation"],
neuper@37981	968	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	969	("#Where" ,["matches (?a + ?v_^^^2 = 0) e_e \| " ^
neuper@37981	970	"matches (?a + ?b*?v_^^^2 = 0) e_e"]),
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_d2_polyeq_abc_equation"]]));
neuper@37989	975	*}
neuper@37989	976	ML{*
neuper@37954	977	(--- d3 ---)
neuper@37954	978	store_pbt
neuper@37972	979	(prep_pbt thy "pbl_equ_univ_poly_deg3" [] e_pblID
neuper@37954	980	(["degree_3","polynomial","univariate","equation"],
neuper@37981	981	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	982	("#Where" ,["matches (?a = 0) e_e",
neuper@37981	983	"(lhs e_e) is_poly_in v_v ",
neuper@37981	984	"((lhs e_e) has_degree_in v_v) = 3"]),
neuper@38012	985	("#Find" ,["solutions v_v'i'"])
neuper@37954	986	],
neuper@37981	987	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	988	[["PolyEq","solve_d3_polyeq_equation"]]));
neuper@37954	989
neuper@37954	990	(--- d4 ---)
neuper@37954	991	store_pbt
neuper@37972	992	(prep_pbt thy "pbl_equ_univ_poly_deg4" [] e_pblID
neuper@37954	993	(["degree_4","polynomial","univariate","equation"],
neuper@37981	994	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	995	("#Where" ,["matches (?a = 0) e_e",
neuper@37981	996	"(lhs e_e) is_poly_in v_v ",
neuper@37981	997	"((lhs e_e) has_degree_in v_v) = 4"]),
neuper@38012	998	("#Find" ,["solutions v_v'i'"])
neuper@37954	999	],
neuper@37981	1000	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	1001	[(["PolyEq","solve_d4_polyeq_equation"])]));
neuper@37954	1002
neuper@37954	1003	(--- normalize ---)
neuper@37954	1004	store_pbt
neuper@37972	1005	(prep_pbt thy "pbl_equ_univ_poly_norm" [] e_pblID
neuper@37954	1006	(["normalize","polynomial","univariate","equation"],
neuper@37981	1007	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1008	("#Where" ,["(Not((matches (?a = 0 ) e_e ))) \|" ^
neuper@37981	1009	"(Not(((lhs e_e) is_poly_in v_v)))"]),
neuper@38012	1010	("#Find" ,["solutions v_v'i'"])
neuper@37954	1011	],
neuper@37981	1012	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	1013	[["PolyEq","normalize_poly"]]));
neuper@37954	1014	(-------------------------expanded-----------------------)
neuper@37954	1015	store_pbt
neuper@37972	1016	(prep_pbt thy "pbl_equ_univ_expand" [] e_pblID
neuper@37954	1017	(["expanded","univariate","equation"],
neuper@37981	1018	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1019	("#Where" ,["matches (?a = 0) e_e",
neuper@37981	1020	"(lhs e_e) is_expanded_in v_v "]),
neuper@38012	1021	("#Find" ,["solutions v_v'i'"])
neuper@37954	1022	],
neuper@37981	1023	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	1024	[]));
neuper@37954	1025
neuper@37954	1026	(--- d2 ---)
neuper@37954	1027	store_pbt
neuper@37972	1028	(prep_pbt thy "pbl_equ_univ_expand_deg2" [] e_pblID
neuper@37954	1029	(["degree_2","expanded","univariate","equation"],
neuper@37981	1030	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1031	("#Where" ,["((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1032	("#Find" ,["solutions v_v'i'"])
neuper@37954	1033	],
neuper@37981	1034	PolyEq_prls, SOME "solve (e_e::bool, v_v)",
neuper@37954	1035	[["PolyEq","complete_square"]]));
neuper@37954	1036
neuper@37989	1037	*}
neuper@37989	1038	ML{*
neuper@37989	1039	val scr =
neuper@37989	1040	"Script Normalize_poly (e_e::bool) (v_v::real) = " ^
neuper@37989	1041	"(let e_e =((Try (Rewrite all_left False)) @@ " ^
neuper@37989	1042	" (Try (Repeat (Rewrite makex1_x False))) @@ " ^
neuper@37989	1043	" (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
neuper@37989	1044	" (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37989	1045	" make_ratpoly_in False))) @@ " ^
neuper@37989	1046	" (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
neuper@37989	1047	" in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
neuper@37989	1048	" [BOOL e_e, REAL v_v]))";
neuper@37989	1049	parse thy scr;
neuper@37989	1050	*}
neuper@37989	1051	ML{*
neuper@37954	1052	"-------------------------methods-----------------------";
neuper@37954	1053	store_met
neuper@37972	1054	(prep_met thy "met_polyeq" [] e_metID
neuper@37954	1055	(["PolyEq"],
neuper@37954	1056	[],
neuper@37954	1057	{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
neuper@42425	1058	crls=PolyEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"));
neuper@37954	1059
neuper@37954	1060	store_met
neuper@37972	1061	(prep_met thy "met_polyeq_norm" [] e_metID
neuper@37954	1062	(["PolyEq","normalize_poly"],
neuper@37981	1063	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1064	("#Where" ,["(Not((matches (?a = 0 ) e_e ))) \|" ^
neuper@37981	1065	"(Not(((lhs e_e) is_poly_in v_v)))"]),
neuper@38012	1066	("#Find" ,["solutions v_v'i'"])
neuper@37954	1067	],
neuper@37954	1068	{rew_ord'="termlessI",
neuper@37954	1069	rls'=PolyEq_erls,
neuper@37954	1070	srls=e_rls,
neuper@37954	1071	prls=PolyEq_prls,
neuper@37954	1072	calc=[],
neuper@42425	1073	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1074	"Script Normalize_poly (e_e::bool) (v_v::real) = " ^
neuper@37981	1075	"(let e_e =((Try (Rewrite all_left False)) @@ " ^
neuper@37954	1076	" (Try (Repeat (Rewrite makex1_x False))) @@ " ^
neuper@37954	1077	" (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
neuper@37989	1078	" (Try (Repeat (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1079	" make_ratpoly_in False))) @@ " ^
neuper@37981	1080	" (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_e " ^
neuper@37989	1081	" in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met]) " ^
neuper@37989	1082	" [BOOL e_e, REAL v_v]))"
neuper@37954	1083	));
neuper@37954	1084
neuper@37989	1085	*}
neuper@37989	1086	ML{*
neuper@37954	1087	store_met
neuper@37972	1088	(prep_met thy "met_polyeq_d0" [] e_metID
neuper@37954	1089	(["PolyEq","solve_d0_polyeq_equation"],
neuper@37981	1090	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1091	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1092	"((lhs e_e) has_degree_in v_v) = 0"]),
neuper@38012	1093	("#Find" ,["solutions v_v'i'"])
neuper@37954	1094	],
neuper@37954	1095	{rew_ord'="termlessI",
neuper@37954	1096	rls'=PolyEq_erls,
neuper@37954	1097	srls=e_rls,
neuper@37954	1098	prls=PolyEq_prls,
neuper@37982	1099	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1100	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1101	"Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
neuper@37989	1102	"(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37981	1103	" d0_polyeq_simplify False))) e_e " ^
neuper@37981	1104	" in ((Or_to_List e_e)::bool list))"
neuper@37954	1105	));
neuper@37989	1106	*}
neuper@37989	1107	ML{*
neuper@37954	1108	store_met
neuper@37972	1109	(prep_met thy "met_polyeq_d1" [] e_metID
neuper@37954	1110	(["PolyEq","solve_d1_polyeq_equation"],
neuper@37981	1111	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1112	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1113	"((lhs e_e) has_degree_in v_v) = 1"]),
neuper@38012	1114	("#Find" ,["solutions v_v'i'"])
neuper@37954	1115	],
neuper@37989	1116	{rew_ord'="termlessI", rls'=PolyEq_erls, srls=e_rls, prls=PolyEq_prls,
neuper@37982	1117	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1118	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1119	"Script Solve_d1_polyeq_equation (e_e::bool) (v_v::real) = " ^
neuper@37989	1120	"(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1121	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1122	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1123	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
neuper@37989	1124	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42133	1125	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1126	));
neuper@37989	1127	*}
neuper@37989	1128	ML{*
neuper@37954	1129	store_met
neuper@37972	1130	(prep_met thy "met_polyeq_d22" [] e_metID
neuper@37954	1131	(["PolyEq","solve_d2_polyeq_equation"],
neuper@37981	1132	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1133	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1134	"((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1135	("#Find" ,["solutions v_v'i'"])
neuper@37954	1136	],
neuper@37954	1137	{rew_ord'="termlessI",
neuper@37954	1138	rls'=PolyEq_erls,
neuper@37954	1139	srls=e_rls,
neuper@37954	1140	prls=PolyEq_prls,
neuper@37982	1141	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1142	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1143	"Script Solve_d2_polyeq_equation (e_e::bool) (v_v::real) = " ^
neuper@37989	1144	" (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1145	" d2_polyeq_simplify True)) @@ " ^
neuper@37954	1146	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1147	" (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1148	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1149	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1150	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
neuper@37989	1151	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42268	1152	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1153	));
neuper@37989	1154	*}
neuper@37989	1155	ML{*
neuper@37954	1156	store_met
neuper@37972	1157	(prep_met thy "met_polyeq_d2_bdvonly" [] e_metID
neuper@37954	1158	(["PolyEq","solve_d2_polyeq_bdvonly_equation"],
neuper@37981	1159	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1160	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1161	"((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1162	("#Find" ,["solutions v_v'i'"])
neuper@37954	1163	],
neuper@37954	1164	{rew_ord'="termlessI",
neuper@37954	1165	rls'=PolyEq_erls,
neuper@37954	1166	srls=e_rls,
neuper@37954	1167	prls=PolyEq_prls,
neuper@37982	1168	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1169	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1170	"Script Solve_d2_polyeq_bdvonly_equation (e_e::bool) (v_v::real) =" ^
neuper@37989	1171	" (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1172	" d2_polyeq_bdv_only_simplify True)) @@ " ^
neuper@37954	1173	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1174	" (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1175	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1176	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1177	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
neuper@37989	1178	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42268	1179	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1180	));
neuper@37989	1181	*}
neuper@37989	1182	ML{*
neuper@37954	1183	store_met
neuper@37972	1184	(prep_met thy "met_polyeq_d2_sqonly" [] e_metID
neuper@37954	1185	(["PolyEq","solve_d2_polyeq_sqonly_equation"],
neuper@37981	1186	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1187	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1188	"((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1189	("#Find" ,["solutions v_v'i'"])
neuper@37954	1190	],
neuper@37954	1191	{rew_ord'="termlessI",
neuper@37954	1192	rls'=PolyEq_erls,
neuper@37954	1193	srls=e_rls,
neuper@37954	1194	prls=PolyEq_prls,
neuper@37982	1195	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1196	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1197	"Script Solve_d2_polyeq_sqonly_equation (e_e::bool) (v_v::real) =" ^
neuper@37989	1198	" (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1199	" d2_polyeq_sq_only_simplify True)) @@ " ^
neuper@37954	1200	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1201	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
neuper@37989	1202	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42268	1203	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1204	));
neuper@37989	1205	*}
neuper@37989	1206	ML{*
neuper@37954	1207	store_met
neuper@37972	1208	(prep_met thy "met_polyeq_d2_pq" [] e_metID
neuper@37954	1209	(["PolyEq","solve_d2_polyeq_pq_equation"],
neuper@37981	1210	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1211	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1212	"((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1213	("#Find" ,["solutions v_v'i'"])
neuper@37954	1214	],
neuper@37954	1215	{rew_ord'="termlessI",
neuper@37954	1216	rls'=PolyEq_erls,
neuper@37954	1217	srls=e_rls,
neuper@37954	1218	prls=PolyEq_prls,
neuper@37982	1219	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1220	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1221	"Script Solve_d2_polyeq_pq_equation (e_e::bool) (v_v::real) = " ^
neuper@37989	1222	" (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1223	" d2_polyeq_pqFormula_simplify True)) @@ " ^
neuper@37954	1224	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1225	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
neuper@37989	1226	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42255	1227	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1228	));
neuper@37989	1229	*}
neuper@37989	1230	ML{*
neuper@37954	1231	store_met
neuper@37972	1232	(prep_met thy "met_polyeq_d2_abc" [] e_metID
neuper@37954	1233	(["PolyEq","solve_d2_polyeq_abc_equation"],
neuper@37981	1234	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1235	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1236	"((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1237	("#Find" ,["solutions v_v'i'"])
neuper@37954	1238	],
neuper@37954	1239	{rew_ord'="termlessI",
neuper@37954	1240	rls'=PolyEq_erls,
neuper@37954	1241	srls=e_rls,
neuper@37954	1242	prls=PolyEq_prls,
neuper@37982	1243	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1244	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1245	"Script Solve_d2_polyeq_abc_equation (e_e::bool) (v_v::real) = " ^
neuper@37989	1246	" (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1247	" d2_polyeq_abcFormula_simplify True)) @@ " ^
neuper@37954	1248	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1249	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
neuper@37989	1250	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42268	1251	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1252	));
neuper@37989	1253	*}
neuper@37989	1254	ML{*
neuper@37954	1255	store_met
neuper@37972	1256	(prep_met thy "met_polyeq_d3" [] e_metID
neuper@37954	1257	(["PolyEq","solve_d3_polyeq_equation"],
neuper@37981	1258	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1259	("#Where" ,["(lhs e_e) is_poly_in v_v ",
neuper@37981	1260	"((lhs e_e) has_degree_in v_v) = 3"]),
neuper@38012	1261	("#Find" ,["solutions v_v'i'"])
neuper@37954	1262	],
neuper@37954	1263	{rew_ord'="termlessI",
neuper@37954	1264	rls'=PolyEq_erls,
neuper@37954	1265	srls=e_rls,
neuper@37954	1266	prls=PolyEq_prls,
neuper@37982	1267	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1268	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37982	1269	"Script Solve_d3_polyeq_equation (e_e::bool) (v_v::real) = " ^
neuper@37989	1270	" (let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1271	" d3_polyeq_simplify True)) @@ " ^
neuper@37954	1272	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1273	" (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1274	" d2_polyeq_simplify True)) @@ " ^
neuper@37954	1275	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1276	" (Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
neuper@37954	1277	" d1_polyeq_simplify True)) @@ " ^
neuper@37954	1278	" (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
neuper@37989	1279	" (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
neuper@37989	1280	" (L_L::bool list) = ((Or_to_List e_e)::bool list) " ^
neuper@42268	1281	" in Check_elementwise L_L {(v_v::real). Assumptions} )"
neuper@37954	1282	));
neuper@37989	1283	*}
neuper@37989	1284	ML{*
neuper@37954	1285	(.solves all expanded (ie. normalized) terms of degree 2.)
neuper@37954	1286	(*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
neuper@37954	1287	by 'PolyEq_erls'; restricted until Float.thy is implemented*)
neuper@37954	1288	store_met
neuper@37972	1289	(prep_met thy "met_polyeq_complsq" [] e_metID
neuper@37954	1290	(["PolyEq","complete_square"],
neuper@37981	1291	[("#Given" ,["equality e_e","solveFor v_v"]),
neuper@37981	1292	("#Where" ,["matches (?a = 0) e_e",
neuper@37981	1293	"((lhs e_e) has_degree_in v_v) = 2"]),
neuper@38012	1294	("#Find" ,["solutions v_v'i'"])
neuper@37954	1295	],
neuper@37954	1296	{rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
neuper@37982	1297	calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))],
neuper@42425	1298	crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
neuper@37989	1299	"Script Complete_square (e_e::bool) (v_v::real) = " ^
neuper@37989	1300	"(let e_e = " ^
neuper@37989	1301	" ((Try (Rewrite_Set_Inst [(bdv,v_v)] cancel_leading_coeff True)) " ^
neuper@37989	1302	" @@ (Try (Rewrite_Set_Inst [(bdv,v_v)] complete_square True)) " ^
neuper@37954	1303	" @@ (Try (Rewrite square_explicit1 False)) " ^
neuper@37954	1304	" @@ (Try (Rewrite square_explicit2 False)) " ^
neuper@37954	1305	" @@ (Rewrite root_plus_minus True) " ^
neuper@37989	1306	" @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit1 False))) " ^
neuper@37989	1307	" @@ (Try (Repeat (Rewrite_Inst [(bdv,v_v)] bdv_explicit2 False))) " ^
neuper@37954	1308	" @@ (Try (Repeat " ^
neuper@37989	1309	" (Rewrite_Inst [(bdv,v_v)] bdv_explicit3 False))) " ^
neuper@37954	1310	" @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
neuper@37981	1311	" @@ (Try (Repeat (Calculate SQRT)))) e_e " ^
neuper@37981	1312	" in ((Or_to_List e_e)::bool list))"
neuper@37954	1313	));
neuper@37989	1314	*}
neuper@37989	1315	ML{*
neuper@37954	1316
neuper@37954	1317	(* termorder hacked by MG *)
neuper@37954	1318	local (. for make_polynomial_in .)
neuper@37954	1319
neuper@37954	1320	open Term; (* for type order = EQUAL \| LESS \| GREATER *)
neuper@37954	1321
neuper@37954	1322	fun pr_ord EQUAL = "EQUAL"
neuper@37954	1323	\| pr_ord LESS = "LESS"
neuper@37954	1324	\| pr_ord GREATER = "GREATER";
neuper@37954	1325
neuper@37954	1326	fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
neuper@37954	1327	\| dest_hd' x (t as Free (a, T)) =
neuper@37954	1328	if x = t then ((("\|\|\|\|\|\|\|\|\|\|\|\|\|", 0), T), 0) (WN)
neuper@37954	1329	else (((a, 0), T), 1)
neuper@37954	1330	\| dest_hd' x (Var v) = (v, 2)
neuper@37954	1331	\| dest_hd' x (Bound i) = ((("", i), dummyT), 3)
neuper@37954	1332	\| dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
neuper@37954	1333
neuper@37954	1334	fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =
neuper@37954	1335	(case x of (WN)
neuper@37954	1336	(Free (xstr,_)) =>
neuper@37954	1337	(if xstr = var then 1000*(the (int_of_str pot)) else 3)
neuper@38031	1338	\| _ => error ("size_of_term' called with subst = "^
neuper@37954	1339	(term2str x)))
neuper@37954	1340	\| size_of_term' x (Free (subst,_)) =
neuper@37954	1341	(case x of
neuper@37954	1342	(Free (xstr,_)) => (if xstr = subst then 1000 else 1)
neuper@38031	1343	\| _ => error ("size_of_term' called with subst = "^
neuper@37954	1344	(term2str x)))
neuper@37954	1345	\| size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
neuper@37954	1346	\| size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
neuper@37954	1347	\| size_of_term' x _ = 1;
neuper@37954	1348
neuper@37989	1349	fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
neuper@52070	1350	(case term_ord' x pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) \| ord => ord)
neuper@37989	1351	\| term_ord' x pr thy (t, u) =
neuper@52070	1352	(if pr
neuper@52070	1353	then
neuper@52070	1354	let
neuper@52070	1355	val (f, ts) = strip_comb t and (g, us) = strip_comb u;
neuper@52070	1356	val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
neuper@52070	1357	commas (map (term_to_string''' thy) ts) ^ "]\"");
neuper@52070	1358	val _ = tracing ("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
neuper@52070	1359	commas(map (term_to_string''' thy) us) ^ "]\"");
neuper@52070	1360	val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' x t) ^ ", " ^
neuper@52070	1361	string_of_int (size_of_term' x u) ^ ")");
neuper@52070	1362	val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o (hd_ord x)) (f,g));
neuper@52070	1363	val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o (terms_ord x) str false) (ts, us));
neuper@52070	1364	val _ = tracing ("-------");
neuper@52070	1365	in () end
neuper@52070	1366	else ();
neuper@52070	1367	case int_ord (size_of_term' x t, size_of_term' x u) of
neuper@52070	1368	EQUAL =>
neuper@52070	1369	let val (f, ts) = strip_comb t and (g, us) = strip_comb u
neuper@52070	1370	in
neuper@52070	1371	(case hd_ord x (f, g) of
neuper@52070	1372	EQUAL => (terms_ord x str pr) (ts, us)
neuper@52070	1373	\| ord => ord)
neuper@52070	1374	end
neuper@37954	1375	\| ord => ord)
neuper@37954	1376	and hd_ord x (f, g) = (* ~ term.ML *)
neuper@37989	1377	prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
neuper@37989	1378	int_ord (dest_hd' x f, dest_hd' x g)
neuper@37954	1379	and terms_ord x str pr (ts, us) =
neuper@37989	1380	list_ord (term_ord' x pr (assoc_thy "Isac"))(ts, us);
neuper@52070	1381
neuper@37954	1382	in
neuper@37954	1383
neuper@37954	1384	fun ord_make_polynomial_in (pr:bool) thy subst tu =
neuper@37954	1385	let
neuper@38015	1386	(* val _=tracing("*** subs variable is: "^(subst2str subst)); *)
neuper@37954	1387	in
neuper@37954	1388	case subst of
neuper@37954	1389	(_,x)::_ => (term_ord' x pr thy tu = LESS)
neuper@38031	1390	\| _ => error ("ord_make_polynomial_in called with subst = "^
neuper@37954	1391	(subst2str subst))
neuper@37954	1392	end;
neuper@37989	1393	end;(local)
neuper@37954	1394
neuper@37989	1395	*}
neuper@37989	1396	ML{*
neuper@37954	1397	val order_add_mult_in = prep_rls(
neuper@37954	1398	Rls{id = "order_add_mult_in", preconds = [],
neuper@37954	1399	rew_ord = ("ord_make_polynomial_in",
neuper@40836	1400	ord_make_polynomial_in false (Thy_Info.get_theory "Poly")),
neuper@37954	1401	erls = e_rls,srls = Erls,
neuper@42451	1402	calc = [], errpatts = [],
neuper@48763	1403	rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
neuper@37954	1404	(* z * w = w * z *)
neuper@37969	1405	Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
neuper@37954	1406	(z1.0 (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
neuper@48763	1407	Thm ("mult_assoc",num_str @{thm mult_assoc}),
neuper@37954	1408	(z1.0 z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
neuper@37965	1409	Thm ("add_commute",num_str @{thm add_commute}),
neuper@37954	1410	(z + w = w + z)
neuper@37965	1411	Thm ("add_left_commute",num_str @{thm add_left_commute}),
neuper@37954	1412	(x + (y + z) = y + (x + z))
neuper@37965	1413	Thm ("add_assoc",num_str @{thm add_assoc})
neuper@37954	1414	(z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0))
neuper@37954	1415	], scr = EmptyScr}:rls);
neuper@37954	1416
neuper@37989	1417	*}
neuper@37989	1418	ML{*
neuper@37954	1419	val collect_bdv = prep_rls(
neuper@37954	1420	Rls{id = "collect_bdv", preconds = [],
neuper@37954	1421	rew_ord = ("dummy_ord", dummy_ord),
neuper@37954	1422	erls = e_rls,srls = Erls,
neuper@42451	1423	calc = [], errpatts = [],
neuper@37969	1424	rules = [Thm ("bdv_collect_1",num_str @{thm bdv_collect_1}),
neuper@37969	1425	Thm ("bdv_collect_2",num_str @{thm bdv_collect_2}),
neuper@37969	1426	Thm ("bdv_collect_3",num_str @{thm bdv_collect_3}),
neuper@37954	1427
neuper@37969	1428	Thm ("bdv_collect_assoc1_1",num_str @{thm bdv_collect_assoc1_1}),
neuper@37969	1429	Thm ("bdv_collect_assoc1_2",num_str @{thm bdv_collect_assoc1_2}),
neuper@37969	1430	Thm ("bdv_collect_assoc1_3",num_str @{thm bdv_collect_assoc1_3}),
neuper@37954	1431
neuper@37969	1432	Thm ("bdv_collect_assoc2_1",num_str @{thm bdv_collect_assoc2_1}),
neuper@37969	1433	Thm ("bdv_collect_assoc2_2",num_str @{thm bdv_collect_assoc2_2}),
neuper@37969	1434	Thm ("bdv_collect_assoc2_3",num_str @{thm bdv_collect_assoc2_3}),
neuper@37954	1435
neuper@37954	1436
neuper@37969	1437	Thm ("bdv_n_collect_1",num_str @{thm bdv_n_collect_1}),
neuper@37969	1438	Thm ("bdv_n_collect_2",num_str @{thm bdv_n_collect_2}),
neuper@37969	1439	Thm ("bdv_n_collect_3",num_str @{thm bdv_n_collect_3}),
neuper@37954	1440
neuper@37969	1441	Thm ("bdv_n_collect_assoc1_1",num_str @{thm bdv_n_collect_assoc1_1}),
neuper@37969	1442	Thm ("bdv_n_collect_assoc1_2",num_str @{thm bdv_n_collect_assoc1_2}),
neuper@37969	1443	Thm ("bdv_n_collect_assoc1_3",num_str @{thm bdv_n_collect_assoc1_3}),
neuper@37954	1444
neuper@37969	1445	Thm ("bdv_n_collect_assoc2_1",num_str @{thm bdv_n_collect_assoc2_1}),
neuper@37969	1446	Thm ("bdv_n_collect_assoc2_2",num_str @{thm bdv_n_collect_assoc2_2}),
neuper@37989	1447	Thm ("bdv_n_collect_assoc2_3",num_str @{thm bdv_n_collect_assoc2_3})
neuper@37954	1448	], scr = EmptyScr}:rls);
neuper@37954	1449
neuper@37989	1450	*}
neuper@37989	1451	ML{*
neuper@37954	1452	(*.transforms an arbitrary term without roots to a polynomial [4]
neuper@37954	1453	according to knowledge/Poly.sml.*)
neuper@37954	1454	val make_polynomial_in = prep_rls(
neuper@37954	1455	Seq {id = "make_polynomial_in", preconds = []:term list,
neuper@37954	1456	rew_ord = ("dummy_ord", dummy_ord),
neuper@37954	1457	erls = Atools_erls, srls = Erls,
neuper@42451	1458	calc = [], errpatts = [],
neuper@37954	1459	rules = [Rls_ expand_poly,
neuper@37954	1460	Rls_ order_add_mult_in,
neuper@37954	1461	Rls_ simplify_power,
neuper@37954	1462	Rls_ collect_numerals,
neuper@37954	1463	Rls_ reduce_012,
neuper@37969	1464	Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
neuper@37954	1465	Rls_ discard_parentheses,
neuper@37954	1466	Rls_ collect_bdv
neuper@37954	1467	],
neuper@37954	1468	scr = EmptyScr
neuper@37954	1469	}:rls);
neuper@37954	1470
neuper@37989	1471	*}
neuper@37989	1472	ML{*
neuper@37954	1473	val separate_bdvs =
neuper@37954	1474	append_rls "separate_bdvs"
neuper@37954	1475	collect_bdv
neuper@37989	1476	[Thm ("separate_bdv", num_str @{thm separate_bdv}),
neuper@37954	1477	("?a ?bdv / ?b = ?a / ?b * ?bdv"*)
neuper@37989	1478	Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
neuper@37989	1479	Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
neuper@37954	1480	("?bdv / ?b = (1 / ?b) ?bdv"*)
neuper@37989	1481	Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n}),
neuper@37954	1482	("?bdv ^^^ ?n / ?b = 1 / ?b ?bdv ^^^ ?n"*)
neuper@37990	1483	Thm ("add_divide_distrib",
neuper@37989	1484	num_str @{thm add_divide_distrib})
neuper@37954	1485	(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
neuper@37954	1486	WN051031 DOES NOT BELONG TO HERE*)
neuper@37954	1487	];
neuper@37989	1488	*}
neuper@37989	1489	ML{*
neuper@37954	1490	val make_ratpoly_in = prep_rls(
neuper@37954	1491	Seq {id = "make_ratpoly_in", preconds = []:term list,
neuper@37954	1492	rew_ord = ("dummy_ord", dummy_ord),
neuper@37954	1493	erls = Atools_erls, srls = Erls,
neuper@42451	1494	calc = [], errpatts = [],
neuper@37954	1495	rules = [Rls_ norm_Rational,
neuper@37954	1496	Rls_ order_add_mult_in,
neuper@37954	1497	Rls_ discard_parentheses,
neuper@37954	1498	Rls_ separate_bdvs,
neuper@37954	1499	(* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
neuper@37954	1500	Rls_ cancel_p
neuper@48789	1501	(Calc ("Fields.inverse_class.divide" ,eval_cancel "#divide_e") too weak!)
neuper@37954	1502	],
neuper@37954	1503	scr = EmptyScr}:rls);
neuper@37954	1504
neuper@37954	1505
neuper@37967	1506	ruleset' := overwritelthy @{theory} (!ruleset',
neuper@37954	1507	[("order_add_mult_in", order_add_mult_in),
neuper@37954	1508	("collect_bdv", collect_bdv),
neuper@37954	1509	("make_polynomial_in", make_polynomial_in),
neuper@37954	1510	("make_ratpoly_in", make_ratpoly_in),
neuper@37954	1511	("separate_bdvs", separate_bdvs)
neuper@37954	1512	]);
neuper@37954	1513	*}
neuper@37954	1514
neuper@37906	1515	end
neuper@37906	1516
neuper@37906	1517
neuper@37906	1518
neuper@37906	1519
neuper@37906	1520
neuper@37906	1521

author	Walther Neuper <neuper@ist.tugraz.at>
	Sun, 22 Sep 2013 18:09:05 +0200
changeset 52125	6f1d3415dc68
parent 52070	77138c64f4f6
child 52130	012cfda9bd83
permissions	-rw-r--r--