wneuper/isa: test/Tools/isac/Test_Isac.thy@19a172de0bb5 (annotated)

neuper@52065	1	(* Title: All tests on isac (some outcommented since Isabelle2002-->2009-2)
neuper@41943	2	Author: Walther Neuper 101001
wneuper@59258	3	(c) copyright due to license terms.
neuper@41943	4
neuper@52101	5	Isac's tests are organised parallel to sources:
wenzelm@60192	6	$ISABELLE_ISAC_TEST has same directory structure as $ISABELLE_ISAC
neuper@52101	7	plus
wenzelm@60217	8	$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS
wenzelm@60217	9	$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
walther@59957	10
walther@59957	11	Note, that only the first error in a file is shown here.
neuper@41943	12	*)
neuper@41943	13
walther@59623	14	section \<open>Notes on running tests\<close>
walther@59623	15	subsection \<open>Switch between running tests and updating code\<close>
wneuper@59258	16	text \<open>
walther@59623	17	Isac encapsulates code as much as possible in structures without open.
walther@59623	18	This policy conflicts with those tests, which go into functions to details
walther@59623	19	not declared in the signatures.
walther@59623	20	\<close>
walther@59623	21	subsection \<open>Decide between running Test_Isac_Short.thy and Test_Isac.thy\<close>
walther@59623	22	text \<open>
walther@59623	23	Some tests raise exception Size raised (line 171 of "./basis/LibrarySupport.sml")
walther@59623	24	if run in x86_64_32 mode of Poly/ML 5.8 (which is set as default).
walther@59626	25	This exception can be avoided by ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
walther@59626	26	A model is in the repository at ~~/etc/preferences.
walther@59623	27	These preferences have drawbacks, however:
walther@59623	28	* they claim more memory such that Isabelle instances canNOT run in parallel.
walther@59623	29	* they do NOT reach Build_Isac.thy hanging in Build_Thydata.thy, see there.
wneuper@59323	30
walther@59623	31	So default for Build_Isac.thy and for general testing is Test_Isac_Short.thy is x86_64_32 mode.
walther@59623	32	From time to time full testing in Test_Isac.thy is recommended. For that purpose
walther@59626	33	* set ML_system_64 = "true" in ~/.isabelle/isabisac/etc/preferences.
wneuper@59323	34
walther@59967	35	\\***************** don't forget to re-set defaults BEFORE updating code *****************//
walther@59623	36
walther@59626	37	Note that Isabelle/jEdit re-generates the preferences file on shutdown, thus always use
walther@59626	38	***************** $ gedit ~/.isabelle/isabisac/etc/preferences &
wneuper@59258	39	\<close>
wneuper@59258	40
wneuper@59258	41	section \<open>Run the tests\<close>
wneuper@59258	42	text \<open>
wneuper@59258	43	* say "OK" to the popup asking for theories to be loaded
wneuper@59258	44	* watch the <Theories> window for errors in the "imports" below
wneuper@59258	45	\<close>
neuper@52073	46
walther@59623	47	theory Test_Isac
walther@59623	48	imports Isac.Build_Isac (* note that imports are WITHOUT open struct ..*)
walther@60028	49	(* in case of ERROR Bad theory import "Draft.Thy_All"..., open each theory one by one
walther@60028	50	and find out, which ML_file or *.thy causes an error (might be ONLY one).
walther@60028	51	Also backup files (#* ) recognised by jEdit cause this trouble *)
wneuper@59465	52	(/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\)
Walther@60424	53	(* "$ISABELLE_ISAC_TEST/ADDTESTS/accumulate-val/Thy_All"(but ok in editor)*)
Walther@60424	54	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter"
wenzelm@60217	55	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Ctxt"
wenzelm@60217	56	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/test-depend/Build_Test"
wenzelm@60217	57	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/All_Ctxt"
wenzelm@60217	58	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/Test_Units"
wenzelm@60217	59	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T1_Basics"
wenzelm@60217	60	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting"
wenzelm@60217	61	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine"
wenzelm@60217	62	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/file-depend/BuildC_Test"
wenzelm@60217	63	(**)"$ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory/Foo"
wneuper@59144	64	(*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
wneuper@59144	65	ADDTESTS/------------------------------------------- see end of tests *)
Walther@60424	66	(*/~~~ these work directly from Pure, but create problems here ..
wenzelm@60217	67	"$ISABELLE_ISAC_TEST/Pure/Isar/Keyword_ISAC.thy" (* Malformed theory import, "keywords" ?!? *)
wenzelm@60217	68	"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parse_Isac.thy" (* Malformed theory import, "keywords" ?!? *)
wenzelm@60217	69	"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers_Cookbook.thy" (* Malformed theory import ?!? *)
wenzelm@60217	70	"$ISABELLE_ISAC_TEST/Pure/Isar/Theory_Commands" (* Duplicate outer syntax command "ISAC" *)
wenzelm@60217	71	"$ISABELLE_ISAC_TEST/Pure/Isar/Downto_Synchronized" (* re-defines / breaks structures !!! *)
Walther@60424	72	\~~~ .. these work independently, but create problems here *)
wenzelm@60217	73	(**)"$ISABELLE_ISAC_TEST/Pure/Isar/Test_Parsers"
Walther@60424	74	(**)"$ISABELLE_ISAC_TEST/HOL/Tools/Sledgehammer/Try_Sledgehammer"
wneuper@59364	75	(/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\)
wenzelm@60217	76	"$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
wenzelm@60217	77	"$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
wenzelm@60217	78	"$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
Walther@60424	79	(**)
wneuper@59364	80	(\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/)
Walther@60519	81	"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (not imported by Isac.thy) (Test_Isac_Short)
Walther@60519	82	"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (not imported by Isac.thy) (Test_Isac_Short)
wneuper@59364	83	(\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/)
Walther@60424	84	(**)
neuper@52168	85
neuper@41943	86	begin
s1210629013@55442	87
Walther@60424	88	declare [[ML_print_depth = 20]]
Walther@60424	89
walther@59659	90	ML \<open>open ML_System\<close>
wneuper@59472	91	ML \<open>
wneuper@59261	92	open Kernel;
walther@59814	93	open Math_Engine;
Walther@60571	94	open Test_Code; Test_Code.init_calc @{context};
walther@59848	95	open LItool; arguments_from_model;
walther@59817	96	open Sub_Problem;
walther@59823	97	open Fetch_Tacs;
walther@59814	98	open Step
walther@59659	99	open Env;
walther@59814	100	open LI; scan_dn;
wneuper@59600	101	open Istate;
walther@59909	102	open Error_Pattern;
walther@59909	103	open Error_Pattern_Def;
walther@59977	104	open Specification;
wneuper@59276	105	open Ctree; append_problem;
walther@59722	106	open Pos;
walther@59618	107	open Program;
wneuper@59601	108	open Prog_Tac;
walther@59603	109	open Tactical;
walther@59603	110	open Prog_Expr;
walther@59618	111	open Auto_Prog; rule2stac;
walther@59617	112	open Input_Descript;
walther@59971	113	open Specify;
walther@59976	114	open Specify;
walther@59763	115	open Step_Specify;
walther@59763	116	open Step_Solve;
walther@59763	117	open Step;
wneuper@59316	118	open Solve; (* NONE *)
wneuper@59577	119	open ContextC; transfer_asms_from_to;
walther@59814	120	open Tactic; (* NONE *)
walther@60126	121	open I_Model;
walther@60126	122	open O_Model;
walther@60126	123	open P_Model; (* NONE *)
walther@59892	124	open Rewrite;
walther@59878	125	open Eval; get_pair;
wneuper@59410	126	open TermC; atomt;
walther@59858	127	open Rule;
walther@59892	128	open Rule_Set; Sequence;
walther@59919	129	open Eval_Def
walther@59858	130	open ThyC
walther@59865	131	open ThmC_Def
walther@59858	132	open ThmC
walther@59858	133	open Rewrite_Ord
walther@59865	134	open UnparseC
wenzelm@60223	135	\<close>
wneuper@59366	136
wneuper@59462	137	ML \<open>
walther@59674	138	"~~~~~ fun xxx , args:"; val () = ();
walther@59674	139	"~~~~~ and xxx , args:"; val () = ();
Walther@60424	140	"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
Walther@60424	141	(if) (then); (else); (case) (of); (return value); (in) (end);
walther@59674	142	"xx"
Walther@60567	143	^ "xxx" (+) (+++) (* keep for continuation) (isa) (isa2) (*)
Walther@60567	144	\<close> ML \<open> (//----------- adhoc inserted n ----------------------------------------------------\\)
Walther@60567	145	(//----------------- adhoc inserted n ----------------------------------------------------\\)
Walther@60567	146	(\\------------------ adhoc inserted n ----------------------------------------------------//)
Walther@60567	147	\<close> ML \<open> (\\----------- adhoc inserted n ----------------------------------------------------//)
walther@59763	148	\<close>
walther@59763	149	ML \<open>
walther@59763	150	\<close> ML \<open>
wneuper@59462	151	\<close> ML \<open>
walther@59858	152	\<close> ML \<open>
walther@59858	153	\<close> ML \<open>
wneuper@59462	154	\<close>
wneuper@59356	155
wneuper@59472	156	ML \<open>
s1210629013@55446	157	KEStore_Elems.set_ref_thy @{theory};
wneuper@59248	158	(fun autoCalculate' cI auto = autoCalculate cI auto (\|> Future.join));
wneuper@59472	159	\<close>
s1210629013@55442	160
wneuper@59472	161	section \<open>trials with Isabelle's functions\<close>
wneuper@59472	162	ML \<open>"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";\<close>
wenzelm@60217	163	ML_file "$ISABELLE_ISAC_TEST/Pure/General/alist.ML"
wenzelm@60217	164	ML_file "$ISABELLE_ISAC_TEST/Pure/General/basics.ML"
wenzelm@60217	165	ML_file "$ISABELLE_ISAC_TEST/Pure/General/scan.ML"
wenzelm@60217	166	ML_file "$ISABELLE_ISAC_TEST/Pure/PIDE/xml.ML"
wneuper@59472	167	ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
neuper@52119	168
wneuper@59472	169	section \<open>test ML Code of isac\<close>
wneuper@59600	170	subsection \<open>basic code first\<close>
wneuper@59472	171	ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
Walther@60424	172	ML_file "BaseDefinitions/base-definitions.sml"
walther@59866	173	ML_file "BaseDefinitions/libraryC.sml"
walther@59866	174	ML_file "BaseDefinitions/rule-def.sml"
walther@59919	175	ML_file "BaseDefinitions/eval-def.sml"
walther@59866	176	ML_file "BaseDefinitions/rewrite-order.sml"
walther@59866	177	ML_file "BaseDefinitions/theoryC.sml"
walther@59866	178	ML_file "BaseDefinitions/rule.sml"
walther@59866	179	ML_file "BaseDefinitions/thmC-def.sml"
walther@59866	180	ML_file "BaseDefinitions/error-fill-def.sml"
walther@59866	181	ML_file "BaseDefinitions/rule-set.sml"
walther@59892	182	ML_file "BaseDefinitions/check-unique.sml"
walther@59957	183	(called by Know_Store..)
walther@59866	184	ML_file "BaseDefinitions/calcelems.sml"
walther@59866	185	ML_file "BaseDefinitions/termC.sml"
walther@59917	186	ML_file "BaseDefinitions/substitution.sml"
Walther@60558	187	ML_file "BaseDefinitions/contextC.sml"(sometimes needs separation into ML blocks for evaluation)
walther@59866	188	ML_file "BaseDefinitions/environment.sml"
Walther@60424	189	(** )ML_file "BaseDefinitions/kestore.sml"( setup in ADDTEST/accumulate-val/lucas_interpreter.sml)
wneuper@59356	190	(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
wneuper@59388	191	---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
walther@59957	192
Walther@60519	193	ML_file "ProgLang/calculate.sml"
walther@59967	194	ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
walther@59659	195	ML_file "ProgLang/listC.sml"
walther@59659	196	ML_file "ProgLang/prog_expr.sml"
walther@59659	197	ML_file "ProgLang/program.sml"
walther@59659	198	ML_file "ProgLang/prog_tac.sml"
walther@59659	199	ML_file "ProgLang/tactical.sml"
walther@59659	200	ML_file "ProgLang/auto_prog.sml"
wneuper@59362	201	(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
wneuper@59366	202	---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
wneuper@59600	203
wneuper@59600	204	subsection \<open>basic functionality on simple example first\<close>
neuper@52065	205	ML_file "Minisubpbl/000-comments.sml"
neuper@52065	206	ML_file "Minisubpbl/100-init-rootpbl.sml"
neuper@52065	207	ML_file "Minisubpbl/150-add-given.sml"
walther@59781	208	ML_file "Minisubpbl/200-start-method-NEXT_STEP.sml"
neuper@52065	209	ML_file "Minisubpbl/200-start-method.sml"
wneuper@59411	210	ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
walther@59722	211	ML_file "Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
neuper@52065	212	ML_file "Minisubpbl/300-init-subpbl.sml"
neuper@52065	213	ML_file "Minisubpbl/400-start-meth-subpbl.sml"
wneuper@59492	214	ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
walther@59722	215	ML_file "Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
neuper@52065	216	ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
neuper@52065	217	ML_file "Minisubpbl/500-met-sub-to-root.sml"
neuper@52065	218	ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
walther@59781	219	ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml"
neuper@52065	220	ML_file "Minisubpbl/600-postcond.sml"
wneuper@59493	221	ML_file "Minisubpbl/700-interSteps.sml"
walther@59820	222	ML_file "Minisubpbl/710-interSteps-short.sml"
walther@59722	223	ML_file "Minisubpbl/790-complete-NEXT_STEP.sml"
walther@59686	224	ML_file "Minisubpbl/790-complete.sml"
walther@59817	225	ML_file "Minisubpbl/800-append-on-Frm.sml"
wneuper@59600	226
wneuper@59600	227	subsection \<open>further functionality alongside batch build sequence\<close>
walther@59865	228	ML_file "MathEngBasic/thmC.sml"
walther@59865	229	ML_file "MathEngBasic/rewrite.sml"
walther@59763	230	ML_file "MathEngBasic/tactic.sml"
Walther@60558	231	ML_file "MathEngBasic/ctree.sml"
walther@59817	232	ML_file "MathEngBasic/calculation.sml"
walther@59674	233
walther@59996	234	ML_file "Specify/formalise.sml"
walther@59957	235	ML_file "Specify/o-model.sml"
walther@59957	236	ML_file "Specify/i-model.sml"
walther@59996	237	ML_file "Specify/pre-conditions.sml"
walther@59996	238	ML_file "Specify/p-model.sml"
walther@59985	239	ML_file "Specify/m-match.sml"
walther@59967	240	ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
walther@59996	241	ML_file "Specify/test-out.sml"
walther@59996	242	ML_file "Specify/specify-step.sml"
walther@59996	243	ML_file "Specify/specification.sml"
walther@59996	244	ML_file "Specify/cas-command.sml"
walther@59996	245	ML_file "Specify/p-spec.sml"
walther@59996	246	ML_file "Specify/specify.sml"
walther@59817	247	ML_file "Specify/step-specify.sml"
wneuper@59600	248
walther@59865	249	ML_file "Interpret/istate.sml"
walther@59817	250	ML_file "Interpret/sub-problem.sml"
walther@59909	251	ML_file "Interpret/error-pattern.sml"
walther@59817	252	ML_file "Interpret/li-tool.sml"
wneuper@59561	253	ML_file "Interpret/lucas-interpreter.sml"
walther@59763	254	ML_file "Interpret/step-solve.sml"
wneuper@59600	255
walther@59996	256	ML_file "MathEngine/me-misc.sml"
walther@59823	257	ML_file "MathEngine/fetch-tactics.sml"
wneuper@59600	258	ML_file "MathEngine/solve.sml"
walther@59763	259	ML_file "MathEngine/step.sml"
Walther@60558	260	ML_file "MathEngine/mathengine-stateless.sml"
wneuper@59600	261	ML_file "MathEngine/messages.sml"
wneuper@59600	262	ML_file "MathEngine/states.sml"
wneuper@59600	263
walther@59919	264	ML_file "BridgeLibisabelle/thy-present.sml"
wneuper@59600	265	ML_file "BridgeLibisabelle/mathml.sml" (part.)
Walther@60519	266	ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
wneuper@59600	267	ML_file "BridgeLibisabelle/thy-hierarchy.sml"
wneuper@59600	268	ML_file "BridgeLibisabelle/interface-xml.sml" (TODO after 2009-2)
wneuper@59600	269	ML_file "BridgeLibisabelle/interface.sml"
walther@60090	270	ML_file "BridgeJEdit/parseC.sml"
Walther@60465	271	ML_file "BridgeJEdit/preliminary.sml"
Walther@60465	272	ML_file "BridgeJEdit/vscode-example.sml"
walther@60090	273
neuper@52065	274	ML_file "Knowledge/delete.sml"
neuper@52065	275	ML_file "Knowledge/descript.sml"
neuper@52065	276	ML_file "Knowledge/simplify.sml"
Walther@60519	277	ML_file "Knowledge/poly-1.sml"
Walther@60521	278	ML_file "Knowledge/poly-2.sml" (Test_Isac_Short)
wneuper@59370	279	ML_file "Knowledge/gcd_poly_ml.sml"
Walther@60424	280	ML_file "Knowledge/rational-1.sml"
Walther@60424	281	ML_file "Knowledge/rational-2.sml" (Test_Isac_Short)
wneuper@59370	282	ML_file "Knowledge/equation.sml"
wneuper@59370	283	ML_file "Knowledge/root.sml"
wneuper@59370	284	ML_file "Knowledge/lineq.sml"
wneuper@59370	285	(ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 )
walther@59628	286	ML_file "Knowledge/rateq.sml" (some complicated equations not recovered----Test_Isac_Short)
wneuper@59370	287	ML_file "Knowledge/rootrat.sml"
wneuper@59370	288	ML_file "Knowledge/rootrateq.sml"(ome complicated equations not recovered from 2002 )
walther@59628	289	(ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short)
walther@59627	290	ML_file "Knowledge/polyeq-1.sml"
walther@59628	291	ML_file "Knowledge/polyeq-2.sml" (Test_Isac_Short)
neuper@52105	292	(ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files )
neuper@52065	293	ML_file "Knowledge/calculus.sml"
neuper@52065	294	ML_file "Knowledge/trig.sml"
neuper@52065	295	(ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring)
neuper@52065	296	ML_file "Knowledge/diff.sml"
neuper@52065	297	ML_file "Knowledge/integrate.sml"
Walther@60424	298	ML_file "Knowledge/eqsystem-1.sml"
Walther@60556	299	ML_file "Knowledge/eqsystem-1a.sml"
Walther@60424	300	ML_file "Knowledge/eqsystem-2.sml"
neuper@52065	301	ML_file "Knowledge/test.sml"
neuper@52065	302	ML_file "Knowledge/polyminus.sml"
neuper@52065	303	ML_file "Knowledge/vect.sml"
Walther@60458	304	ML_file "Knowledge/diff-app.sml" (* postponed to dev. specification \| TP-prog. *)
walther@59627	305	ML_file "Knowledge/biegelinie-1.sml"
walther@59628	306	ML_file "Knowledge/biegelinie-2.sml" (Test_Isac_Short)
walther@59628	307	ML_file "Knowledge/biegelinie-3.sml" (Test_Isac_Short)
walther@60024	308	ML_file "Knowledge/biegelinie-4.sml"
neuper@52065	309	ML_file "Knowledge/algein.sml"
neuper@52065	310	ML_file "Knowledge/diophanteq.sml"
walther@59628	311	(ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short)
wneuper@59232	312	ML_file "Knowledge/inssort.sml"
neuper@52065	313	ML_file "Knowledge/isac.sml"
neuper@52065	314	ML_file "Knowledge/build_thydata.sml"
wneuper@59600	315
walther@59817	316	ML_file "Test_Code/test-code.sml"
walther@59817	317
walther@59617	318	section \<open>further tests additional to src/.. files\<close>
wneuper@59600	319	ML_file "BridgeLibisabelle/use-cases.sml"
Walther@60558	320	ML \<open>
Walther@60558	321	\<close> ML \<open>
Walther@60558	322	\<close> ML \<open>
Walther@60571	323	(* Title: tests the interface of isac's SML-kernel in accordance to
Walther@60571	324	java-tests/isac.bridge.
Walther@60571	325	Author: Walther Neuper
Walther@60571	326	(c) copyright due to lincense terms.
Walther@60571	327
Walther@60571	328	Tests the interface of isac's SML-kernel in accordance to java-tests/isac.bridge.
Walther@60571	329	Some tests are outcommented since "eliminate ThmC.numerals_to_Free";
Walther@60571	330	these are considered irrelevant for Isabelle/Isac.
Walther@60571	331
Walther@60571	332	WN050707 ... if true, the test ist marked with a \label referring
Walther@60571	333	to the same UC in isac-docu.tex as the JUnit testcase.
Walther@60571	334	WN120210?not ME: added some labels, which are not among the above,
Walther@60571	335	repaired lost \label (s).
Walther@60571	336
Walther@60571	337	theory Test_Some imports Isac.Build_Thydata begin
Walther@60571	338	ML {* KEStore_Elems.set_ref_thy @{theory};
Walther@60571	339	fun autoCalculate' cI auto = autoCalculate cI auto (\|> Future.join) *}
Walther@60571	340	ML_file "Frontend/use-cases.sml"
Walther@60571	341	*)
Walther@60571	342
Walther@60571	343	"--------------------------------------------------------";
Walther@60571	344	"table of contents --------------------------------------";
Walther@60571	345	"--------------------------------------------------------";
Walther@60571	346	"within struct ------------------------------------------";
Walther@60571	347	"--------------------------------------------------------";
Walther@60571	348	"--------- encode ^ -> ^^ ------------------------------";
Walther@60571	349	"--------------------------------------------------------";
Walther@60571	350	"exported from struct -----------------------------------";
Walther@60571	351	"--------------------------------------------------------";
Walther@60571	352	("--------- empty rootpbl --------------------------------";)
Walther@60571	353	"--------- solve_linear as rootpbl FE -------------------";
Walther@60571	354	"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
Walther@60571	355	"--------- miniscript with mini-subpbl ------------------";
Walther@60571	356	"--------- mini-subpbl AUTOCALCULATE Steps 1 ------------";
Walther@60571	357	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
Walther@60571	358	"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
Walther@60571	359	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
Walther@60571	360	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
Walther@60571	361	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
Walther@60571	362	"--------- setContext..Thy ------------------------------";
Walther@60571	363	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
Walther@60571	364	"--------- rat-eq + subpbl: no_met, NO solution dropped - WITH fun me IN test/../solve.sml";
Walther@60571	365	"--------- tryMatchProblem, tryRefineProblem ------------";
Walther@60571	366	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
Walther@60571	367	"--------- maximum-example, UC: Modeling an example -----";
Walther@60571	368	"--------- solve_linear from pbl-hierarchy --------------";
Walther@60571	369	"--------- solve_linear as in an algebra system (CAS)----";
Walther@60571	370	"--------- interSteps: on 'miniscript with mini-subpbl' -";
Walther@60571	371	"--------- getTactic, fetchApplicableTactics ------------";
Walther@60571	372	"--------- getAssumptions, getAccumulatedAsms -----------";
Walther@60571	373	"--------- arbitrary combinations of steps --------------";
Walther@60571	374	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
Walther@60571	375	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
Walther@60571	376	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
Walther@60571	377	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
Walther@60571	378	"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
Walther@60571	379	"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
Walther@60571	380	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
Walther@60571	381	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
Walther@60571	382	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
Walther@60571	383	"--------- UC errpat add-fraction, fillpat by input --------------";
Walther@60571	384	"--------- UC errpat, fillpat step to Rewrite --------------------";
Walther@60571	385	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
Walther@60571	386	"--------------------------------------------------------";
Walther@60571	387
Walther@60571	388	"within struct ---------------------------------------------------";
Walther@60571	389	"within struct ---------------------------------------------------";
Walther@60571	390	"within struct ---------------------------------------------------";
Walther@60571	391	(*==================================================================
Walther@60571	392
Walther@60571	393	==================================================================*)
Walther@60571	394	"exported from struct --------------------------------------------";
Walther@60571	395	"exported from struct --------------------------------------------";
Walther@60571	396	"exported from struct --------------------------------------------";
Walther@60571	397
Walther@60571	398
Walther@60571	399	(------------ set at startup of the Kernel ----------------------)
Walther@60571	400	States.reset (); (resets all state information in Kernel )
Walther@60571	401	(----------------------------------------------------------------)
Walther@60571	402
Walther@60571	403	(*---------------------------------------------------- postpone to Outer_Syntax..Example -----
Walther@60571	404	"--------- empty rootpbl --------------------------------";
Walther@60571	405	"--------- empty rootpbl --------------------------------";
Walther@60571	406	"--------- empty rootpbl --------------------------------";
Walther@60571	407	CalcTree @{context} [([], ("", [], []))];
Walther@60571	408	Iterator 1;
Walther@60571	409	moveActiveRoot 1;
Walther@60571	410	refFormula 1 (States.get_pos 1 1);
Walther@60571	411	(WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???)
Walther@60571	412	DEconstrCalcTree 1;
Walther@60571	413	------------------------------------------------------ postpone to Outer_Syntax..Example -----*)
Walther@60571	414
Walther@60571	415	"--------- solve_linear as rootpbl FE -------------------";
Walther@60571	416	"--------- solve_linear as rootpbl FE -------------------";
Walther@60571	417	"--------- solve_linear as rootpbl FE -------------------";
Walther@60571	418	States.reset ();
Walther@60571	419
Walther@60571	420	CalcTree @{context} (start of calculation, return No.1)
Walther@60571	421	[(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
Walther@60571	422	("Test",
Walther@60571	423	["LINEAR", "univariate", "equation", "test"],
Walther@60571	424	["Test", "solve_linear"]))];
Walther@60571	425	Iterator 1; (create an active Iterator on CalcTree @{context} No.1)
Walther@60571	426
Walther@60571	427	moveActiveRoot 1;(sets the CalcIterator No.1 at the root of CalcTree @{context} No.1);
Walther@60571	428	refFormula 1 (States.get_pos 1 1) (gets CalcHead; model is still empty);
Walther@60571	429
Walther@60571	430
Walther@60571	431	(1) fetchProposedTactic 1 (by using Iterator No.1);
Walther@60571	432	setNextTactic 1 (Model_Problem); (by using Iterator No.1)
Walther@60571	433	autoCalculate 1 (Steps 1);
Walther@60571	434	refFormula 1 (States.get_pos 1 1) (model contains descriptions for all items);
Walther@60571	435	autoCalculate 1 (Steps 1);
Walther@60571	436	(-----since Model_Problem + complete_mod_ in case cas of SOME-----
Walther@60571	437	(2) fetchProposedTactic 1;
Walther@60571	438	setNextTactic 1 (Add_Given "equality (1 + - 1 * 2 + x = 0)");
Walther@60571	439	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (equality added);
Walther@60571	440
Walther@60571	441	(3) fetchProposedTactic 1;
Walther@60571	442	setNextTactic 1 (Add_Given "solveFor x");
Walther@60571	443	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	444
Walther@60571	445	(4) fetchProposedTactic 1;
Walther@60571	446	setNextTactic 1 (Add_Find "solutions L");
Walther@60571	447	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	448
Walther@60571	449	(5) fetchProposedTactic 1;
Walther@60571	450	setNextTactic 1 (Specify_Theory "Test");
Walther@60571	451	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	452	-----since Model_Problem + complete_mod_ in case cas of SOME-----)
Walther@60571	453
Walther@60571	454	(6) fetchProposedTactic 1;
Walther@60571	455	setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
Walther@60571	456	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	457	(-------------------------------------------------------------------------)
Walther@60571	458	(7) fetchProposedTactic 1;
Walther@60571	459	val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
Walther@60571	460
Walther@60571	461	setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
Walther@60571	462	val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
Walther@60571	463
Walther@60571	464	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	465	val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
Walther@60571	466
Walther@60571	467	(-------------------------------------------------------------------------)
Walther@60571	468	(8) fetchProposedTactic 1;
Walther@60571	469	val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
Walther@60571	470
Walther@60571	471	(8) setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
Walther@60571	472	(ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation)
Walther@60571	473	val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1;
Walther@60571	474	SpecificationC.is_complete ptp;
Walther@60571	475	References.are_complete ptp;
Walther@60571	476
Walther@60571	477	(8) autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1); (<---------------------- orig. test code)
Walther@60571	478
Walther@60571	479	val (ptp as (pt,p), tacis) = States.get_calc 1; States.get_pos 1 1; (<---------------------- orig. test code)
Walther@60571	480	(+isa=REP) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + - 1 * 2 + x = 0"
Walther@60571	481	andalso Istate.string_of (get_istate_LI pt p)
Walther@60571	482	= "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
Walther@60571	483	then () else error "refFormula = 1 + - 1 * 2 + x = 0 changed";
Walther@60571	484	(-------------------------------------------------------------------------)
Walther@60571	485
Walther@60571	486	(9) fetchProposedTactic 1; (<----------------------------------------------------- orig. test code)
Walther@60571	487	(+\\------------------------------------------ isa == REP -----------------------------------// )
Walther@60571	488	(+//========================================== isa <> REP (1) ===============================\\)
Walther@60571	489	(9) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( <------- orig. test code)
Walther@60571	490
Walther@60571	491	"~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
Walther@60571	492	val ((pt'''''_', _), _) = States.get_calc cI
Walther@60571	493	val ip'''''_' = States.get_pos cI 1;
Walther@60571	494
Walther@60571	495	val xxxxx_x("ok", (tacis, _, _)) = (case) Step.by_tactic tac (pt'''''_', ip'''''_') (of);
Walther@60571	496	(+isa+REP)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
Walther@60571	497	Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
Walther@60571	498
Walther@60571	499	(//**************** Step.by_tactic returns tac_ + istate + cstate **************************\\)
Walther@60571	500	Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
Walther@60571	501	if Istate.string_of istate
Walther@60571	502	= "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
Walther@60571	503	then () else error "from Step.by_tactic return --- changed 1";
Walther@60571	504
Walther@60571	505	if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
Walther@60571	506	= "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
Walther@60571	507	then () else error "from Step.by_tactic return --- changed 2";
Walther@60571	508	(\\**************** Step.by_tactic returns tac_ + istate + cstate **************************//)
Walther@60571	509
Walther@60571	510	"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
Walther@60571	511	val Applicable.Yes m = (case) Step.check tac (pt, p) (of);
Walther@60571	512	(if) Tactic.for_specify' m; (false)
Walther@60571	513
Walther@60571	514	Step_Solve.by_tactic m (pt, p);
Walther@60571	515	"~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
Walther@60571	516	(if) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p); (else)
Walther@60571	517	val thy' = get_obj g_domID pt (par_pblobj pt p);
Walther@60571	518	val (is, sc) = LItool.resume_prog (p,p_) pt;
Walther@60571	519	val Safe_Step (istate, _, tac) =
Walther@60571	520	(case) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (of);
Walther@60571	521
Walther@60571	522	(+)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
Walther@60571	523	(********************* locate_input_tactic returns cstate * istate * Proof.context *************)
Walther@60571	524	(+)if Istate.string_of istate
Walther@60571	525	(+isa) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
Walther@60571	526	then case m of Rewrite_Set_Inst' _ => ()
Walther@60571	527	else error "from locate_input_tactic return --- changed";
Walther@60571	528
Walther@60571	529	val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
Walther@60571	530	"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
Walther@60571	531	(\\=========================================== isa <> REP (1) ===============================//)
Walther@60571	532	(//=========================================== isa <> REP (2) ===============================\\)
Walther@60571	533	(9 ) autoCalculate 1 (Steps 1); (<-------------------------------------------------- orig. test code)
Walther@60571	534	( isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>)
Walther@60571	535
Walther@60571	536	"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
Walther@60571	537	val pold = States.get_pos cI 1;
Walther@60571	538	val xxx = (States.get_calc cI);
Walther@60571	539	(isa) val ()xxxx() () = ()
Walther@60571	540	(case) Math_Engine.autocalc [] pold (xxx) auto (of);
Walther@60571	541	"~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
Walther@60571	542	(if) s <= 1; (then)
Walther@60571	543	(val (str, (_, c', ptp)) =)
Walther@60571	544
Walther@60571	545	Step.do_next ip cs;
Walther@60571	546	"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
Walther@60571	547
Walther@60571	548	(+isa==REP)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
Walther@60571	549	Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
Walther@60571	550	(+)if pos' = ([1], Res) andalso Istate.string_of istate
Walther@60571	551	= "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
Walther@60571	552	then () else error "init. step 1 + - 1 * 2 + x = 0 changed";
Walther@60571	553
Walther@60571	554	val pIopt = get_pblID (pt,ip);
Walther@60571	555	(if) ip = ([], Pos.Res);(else)
Walther@60571	556	val (_::_) = (case) tacis (of);
Walther@60571	557	(isa==REP) (if) ip = p;(then)
Walther@60571	558	(val (pt',c',p') =) Solve_Step.s_add_general tacis (pt,[],p);
Walther@60571	559	(//------------------------------------- final test -----------------------------------------\\)
Walther@60571	560	val ("ok", [], ptp as (pt, p)) = xxxx;
Walther@60571	561
Walther@60571	562	if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> \<up> \<up> \<up> \<up> ^*)
Walther@60571	563	(REP) = "Pstate ([\"\n(e_e, 1 + - 1 * 2 + x = 0)\", \"\n(v_v, x)\"], [R, L, R, L, R, L, R], empty, SOME e_e, \nx = 0 + - 1 * (1 + - 1 * 2), ORundef, true, true)"
Walther@60571	564	then () else error "REP autoCalculate on (e_e, 1 + - 1 * 2 + x = 0) changed"
Walther@60571	565
Walther@60571	566	"~~~~~ from TOPLEVEL to states return:"; States.upd_calc cI (ptp, []); States.upd_ipos cI 1 p;
Walther@60571	567	(\\=========================================== isa <> REP (2) ===============================//)
Walther@60571	568
Walther@60571	569	(10) fetchProposedTactic 1;
Walther@60571	570	setNextTactic 1 (Rewrite_Set "Test_simplify");
Walther@60571	571	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	572
Walther@60571	573	(11) fetchProposedTactic 1;
Walther@60571	574	setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
Walther@60571	575	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	576
Walther@60571	577	(======= final test ==================================================)
Walther@60571	578	val ((pt,_),_) = States.get_calc 1;
Walther@60571	579	val ip = States.get_pos 1 1;
Walther@60571	580
Walther@60571	581	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
Walther@60571	582	(exception just above means: 'ModSpec' has been returned: error anyway)
Walther@60571	583	if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
Walther@60571	584	error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
Walther@60571	585
Walther@60571	586
Walther@60571	587	"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
Walther@60571	588	"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
Walther@60571	589	"--------- inspect the CalcTree @{context} No.1 with Iterator No.2 -";
Walther@60571	590	(WN041118: inspection shifted to Iterator No.1, because others need pos')
Walther@60571	591	(*-------- WN190723: doesnt work since changeset 59474 21d4d2868b83
Walther@60571	592	moveActiveRoot 1;
Walther@60571	593	refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(Error)
Walther@60571	594	moveActiveDown 1;
Walther@60571	595	refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(Error)
Walther@60571	596	moveActiveDown 1 ;
Walther@60571	597	refFormula 1 ([1],Res); getTactic 1 ([1],Res);(OK)
Walther@60571	598	(getAssumption 1 ([1],Res); TODO.WN041217)
Walther@60571	599	moveActiveDown 1 ; refFormula 1 ([2],Res);
Walther@60571	600	moveActiveCalcHead 1; refFormula 1 ([],Pbl);
Walther@60571	601	moveActiveDown 1;
Walther@60571	602	moveActiveDown 1;
Walther@60571	603	moveActiveDown 1;
Walther@60571	604	if States.get_pos 1 1 = ([2], Res) then () else
Walther@60571	605	error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
Walther@60571	606	moveActiveDown 1; refFormula 1 ([], Res);
Walther@60571	607	if States.get_pos 1 1 = ([], Res) then () else
Walther@60571	608	error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
Walther@60571	609	moveActiveCalcHead 1; refFormula 1 ([],Pbl);
Walther@60571	610	DEconstrCalcTree 1;
Walther@60571	611	------------------------------------------------------------------------------------------------*)
Walther@60571	612
Walther@60571	613	"--------- miniscript with mini-subpbl ------------------";
Walther@60571	614	"--------- miniscript with mini-subpbl ------------------";
Walther@60571	615	"--------- miniscript with mini-subpbl ------------------";
Walther@60571	616	(WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE)
Walther@60571	617	"=== this sequence of fun-calls resembles fun me ===";
Walther@60571	618	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	619	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	620	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	621	Iterator 1;
Walther@60571	622
Walther@60571	623	moveActiveRoot 1;
Walther@60571	624	refFormula 1 (States.get_pos 1 1);
Walther@60571	625	fetchProposedTactic 1;
Walther@60571	626	setNextTactic 1 (Model_Problem);
Walther@60571	627	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(gets ModSpec;model is still empty)
Walther@60571	628
Walther@60571	629	fetchProposedTactic 1; (<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR> )
Walther@60571	630	setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
Walther@60571	631	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	632
Walther@60571	633	fetchProposedTactic 1;
Walther@60571	634	setNextTactic 1 (Add_Given "solveFor x");
Walther@60571	635	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	636
Walther@60571	637	fetchProposedTactic 1;
Walther@60571	638	setNextTactic 1 (Add_Find "solutions L");
Walther@60571	639	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	640
Walther@60571	641	fetchProposedTactic 1;
Walther@60571	642	setNextTactic 1 (Specify_Theory "Test");
Walther@60571	643	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	644
Walther@60571	645	fetchProposedTactic 1;
Walther@60571	646	setNextTactic 1 (Specify_Problem
Walther@60571	647	["sqroot-test", "univariate", "equation", "test"]);
Walther@60571	648	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	649	"1-----------------------------------------------------------------";
Walther@60571	650
Walther@60571	651	fetchProposedTactic 1;
Walther@60571	652	setNextTactic 1 (Specify_Method ["Test", "squ-equ-test-subpbl1"]);
Walther@60571	653	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	654
Walther@60571	655	fetchProposedTactic 1;
Walther@60571	656	setNextTactic 1 (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
Walther@60571	657	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	658
Walther@60571	659	fetchProposedTactic 1;
Walther@60571	660	setNextTactic 1 (Rewrite_Set "norm_equation");
Walther@60571	661	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	662
Walther@60571	663	fetchProposedTactic 1;
Walther@60571	664	setNextTactic 1 (Rewrite_Set "Test_simplify");
Walther@60571	665	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	666
Walther@60571	667	fetchProposedTactic 1;(----------------Subproblem--------------------);
Walther@60571	668	setNextTactic 1 (Subproblem ("Test",
Walther@60571	669	["LINEAR", "univariate", "equation", "test"]));
Walther@60571	670	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	671
Walther@60571	672	fetchProposedTactic 1;
Walther@60571	673	setNextTactic 1 (Model_Problem );
Walther@60571	674	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	675
Walther@60571	676	fetchProposedTactic 1;
Walther@60571	677	setNextTactic 1 (Add_Given "equality (- 1 + x = 0)");
Walther@60571	678	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	679
Walther@60571	680	fetchProposedTactic 1;
Walther@60571	681	setNextTactic 1 (Add_Given "solveFor x");
Walther@60571	682	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	683
Walther@60571	684	fetchProposedTactic 1;
Walther@60571	685	setNextTactic 1 (Add_Find "solutions x_i");
Walther@60571	686	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	687
Walther@60571	688	fetchProposedTactic 1;
Walther@60571	689	setNextTactic 1 (Specify_Theory "Test");
Walther@60571	690	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	691
Walther@60571	692	fetchProposedTactic 1;
Walther@60571	693	setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation", "test"]);
Walther@60571	694	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	695	"2-----------------------------------------------------------------";
Walther@60571	696
Walther@60571	697	fetchProposedTactic 1;
Walther@60571	698	setNextTactic 1 (Specify_Method ["Test", "solve_linear"]);
Walther@60571	699	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	700
Walther@60571	701	fetchProposedTactic 1;
Walther@60571	702	setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
Walther@60571	703	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	704
Walther@60571	705	fetchProposedTactic 1;
Walther@60571	706	setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
Walther@60571	707	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	708
Walther@60571	709	fetchProposedTactic 1;
Walther@60571	710	setNextTactic 1 (Rewrite_Set "Test_simplify");
Walther@60571	711	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	712
Walther@60571	713	fetchProposedTactic 1;
Walther@60571	714	setNextTactic 1 (Check_Postcond ["LINEAR", "univariate", "equation", "test"]);
Walther@60571	715	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	716
Walther@60571	717	fetchProposedTactic 1;
Walther@60571	718	setNextTactic 1 (Check_elementwise "Assumptions");
Walther@60571	719	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	720
Walther@60571	721	val xml = fetchProposedTactic 1;
Walther@60571	722	setNextTactic 1 (Check_Postcond
Walther@60571	723	["sqroot-test", "univariate", "equation", "test"]);
Walther@60571	724	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	725
Walther@60571	726	val ((pt,_),_) = States.get_calc 1;
Walther@60571	727	val str = pr_ctree pr_short pt;
Walther@60571	728	writeln str;
Walther@60571	729	val ip = States.get_pos 1 1;
Walther@60571	730	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
Walther@60571	731	(exception just above means: 'ModSpec' has been returned: error anyway)
Walther@60571	732	if UnparseC.term f = "[x = 1]" then () else
Walther@60571	733	error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
Walther@60571	734	(*)-------------------------------------------------------------------------------------------)
Walther@60571	735	DEconstrCalcTree 1;
Walther@60571	736
Walther@60571	737	"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
Walther@60571	738	"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
Walther@60571	739	"--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
Walther@60571	740	(WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176)
Walther@60571	741	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	742	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	743	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	744	Iterator 1;
Walther@60571	745	moveActiveRoot 1;
Walther@60571	746	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	747	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	748	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	749	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	750	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	751	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	752	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	753	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	754	(here the solve-phase starts)
Walther@60571	755	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	756	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	757	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	758	(------------------------------------)
Walther@60571	759	(* (default_print_depth 13) States.get_calc 1;
Walther@60571	760	*)
Walther@60571	761	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	762	(calc-head of subproblem)
Walther@60571	763	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	764	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	765	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	766	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	767	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	768	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	769	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	770	(solve-phase of the subproblem)
Walther@60571	771	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	772	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	773	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	774	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	775	(finish subproblem)
Walther@60571	776	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	777	(finish problem)
Walther@60571	778	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	779
Walther@60571	780	(this checks the test for correctness..)
Walther@60571	781	val ((pt,_),_) = States.get_calc 1;
Walther@60571	782	val p = States.get_pos 1 1;
Walther@60571	783	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	784	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
Walther@60571	785	error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
Walther@60571	786	DEconstrCalcTree 1;
Walther@60571	787
Walther@60571	788
Walther@60571	789	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
Walther@60571	790	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
Walther@60571	791	"--------- solve_linear as rootpbl AUTO CompleteCalc ----";
Walther@60571	792	(WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174)
Walther@60571	793	CalcTree @{context}
Walther@60571	794	[(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
Walther@60571	795	("Test",
Walther@60571	796	["LINEAR", "univariate", "equation", "test"],
Walther@60571	797	["Test", "solve_linear"]))];
Walther@60571	798	Iterator 1;
Walther@60571	799	moveActiveRoot 1;
Walther@60571	800	getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
Walther@60571	801
Walther@60571	802	autoCalculate 1 CompleteCalc;
Walther@60571	803	val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
Walther@60571	804	getFormulaeFromTo 1 unc gen 1 (only level 1) false;
Walther@60571	805
Walther@60571	806	val ((pt,_),_) = States.get_calc 1;
Walther@60571	807	val p = States.get_pos 1 1;
Walther@60571	808	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	809	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
Walther@60571	810	error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
Walther@60571	811	DEconstrCalcTree 1;
Walther@60571	812
Walther@60571	813	"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
Walther@60571	814	"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
Walther@60571	815	"--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
Walther@60571	816	(* ERROR: error in kernel ?? *)
Walther@60571	817	CalcTree @{context}
Walther@60571	818	[(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
Walther@60571	819	("Test",
Walther@60571	820	["LINEAR", "univariate", "equation", "test"],
Walther@60571	821	["Test", "solve_linear"]))];
Walther@60571	822	Iterator 1;
Walther@60571	823	moveActiveRoot 1;
Walther@60571	824
Walther@60571	825	autoCalculate 1 CompleteCalcHead;
Walther@60571	826	refFormula 1 (States.get_pos 1 1);
Walther@60571	827	val ((pt,p),_) = States.get_calc 1;
Walther@60571	828
Walther@60571	829	autoCalculate 1 CompleteCalc;
Walther@60571	830	val ((pt,p),_) = States.get_calc 1;
Walther@60571	831	if p=([], Res) then () else
Walther@60571	832	error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
Walther@60571	833	DEconstrCalcTree 1;
Walther@60571	834
Walther@60571	835	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
Walther@60571	836	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
Walther@60571	837	"--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
Walther@60571	838	(WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174)
Walther@60571	839	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	840	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	841	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	842	Iterator 1;
Walther@60571	843	moveActiveRoot 1;
Walther@60571	844	autoCalculate 1 CompleteCalc;
Walther@60571	845	val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
Walther@60571	846	(*
Walther@60571	847	getTactic 1 ([1],Frm);
Walther@60571	848	getTactic 1 ([1],Res);
Walther@60571	849	initContext 1 Ptool.Thy_ ([1],Res);
Walther@60571	850	*)
Walther@60571	851	(... returns calcChangedEvent with)
Walther@60571	852	val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
Walther@60571	853	getFormulaeFromTo 1 unc gen 0 (only result) false;
Walther@60571	854	getFormulaeFromTo 1 unc gen 1 (only level 1) false;
Walther@60571	855	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
Walther@60571	856
Walther@60571	857	val ((pt,_),_) = States.get_calc 1;
Walther@60571	858	val p = States.get_pos 1 1;
Walther@60571	859	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	860	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
Walther@60571	861	error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
Walther@60571	862	DEconstrCalcTree 1;
Walther@60571	863
Walther@60571	864	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
Walther@60571	865	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
Walther@60571	866	"--------- mini-subpbl AUTO CompleteCalcHead ------------";
Walther@60571	867	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	868	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	869	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	870	Iterator 1;
Walther@60571	871	moveActiveRoot 1;
Walther@60571	872	autoCalculate 1 CompleteCalcHead;
Walther@60571	873
Walther@60571	874	val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
Walther@60571	875	meth, probl,
Walther@60571	876	spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	877	["Test", "squ-equ-test-subpbl1"]),
Walther@60571	878	branch = TransitiveB, ostate = Incomplete (!?\<forall>), ...}, []),
Walther@60571	879	([], Met)), []) = States.get_calc 1;
Walther@60571	880	if length meth = 3 andalso length probl = 3 (just some items tested) then ()
Walther@60571	881	else error "--- mini-subpbl AUTO CompleteCalcHead ---";
Walther@60571	882	DEconstrCalcTree 1;
Walther@60571	883
Walther@60571	884	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
Walther@60571	885	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
Walther@60571	886	"--------- solve_linear as rootpbl AUTO CompleteModel ---";
Walther@60571	887	States.reset ();
Walther@60571	888	CalcTree @{context}
Walther@60571	889	[(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
Walther@60571	890	("Test",
Walther@60571	891	["LINEAR", "univariate", "equation", "test"],
Walther@60571	892	["Test", "solve_linear"]))];
Walther@60571	893	Iterator 1;
Walther@60571	894	moveActiveRoot 1;
Walther@60571	895	autoCalculate 1 CompleteModel;
Walther@60571	896	refFormula 1 (States.get_pos 1 1);
Walther@60571	897
Walther@60571	898	setProblem 1 ["LINEAR", "univariate", "equation", "test"];
Walther@60571	899	val pos = States.get_pos 1 1;
Walther@60571	900	(setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR", "univariate", "equation", "test"]);)
Walther@60571	901	refFormula 1 (States.get_pos 1 1);
Walther@60571	902
Walther@60571	903	setMethod 1 ["Test", "solve_linear"];
Walther@60571	904	(setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test", "solve_linear"]);)
Walther@60571	905	refFormula 1 (States.get_pos 1 1);
Walther@60571	906	val ((pt,_),_) = States.get_calc 1;
Walther@60571	907	if get_obj g_spec pt [] = (ThyC.id_empty,
Walther@60571	908	["LINEAR", "univariate", "equation", "test"],
Walther@60571	909	["Test", "solve_linear"]) then ()
Walther@60571	910	else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
Walther@60571	911
Walther@60571	912	autoCalculate 1 CompleteCalcHead;
Walther@60571	913	refFormula 1 (States.get_pos 1 1);
Walther@60571	914	autoCalculate 1 CompleteCalc;
Walther@60571	915	moveActiveDown 1;
Walther@60571	916	moveActiveDown 1;
Walther@60571	917	moveActiveDown 1;
Walther@60571	918	refFormula 1 (States.get_pos 1 1);
Walther@60571	919	val ((pt,_),_) = States.get_calc 1;
Walther@60571	920	val p = States.get_pos 1 1;
Walther@60571	921	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	922	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
Walther@60571	923	error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
Walther@60571	924	DEconstrCalcTree 1;
Walther@60571	925
Walther@60571	926	"--------- setContext..Thy ------------------------------";
Walther@60571	927	"--------- setContext..Thy ------------------------------";
Walther@60571	928	"--------- setContext..Thy ------------------------------";
Walther@60571	929	States.reset ();
Walther@60571	930	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	931	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	932	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	933	Iterator 1; moveActiveRoot 1;
Walther@60571	934	autoCalculate 1 CompleteCalcHead;
Walther@60571	935	autoCalculate 1 (Steps 1);
Walther@60571	936	val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (2 lines, OK)
Walther@60571	937	(*
Walther@60571	938	setNextTactic 1 (Rewrite_Set "Test_simplify"); (--> "thy_isac_Test-rls-Test_simplify")
Walther@60571	939	autoCalculate 1 (Steps 1);
Walther@60571	940	val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
Walther@60571	941	*)
Walther@60571	942	"----- \<up> ^^ and vvvvv do the same -----";
Walther@60571	943	(setContext 1 p "thy_isac_Test-rls-Test_simplify";)
Walther@60571	944	val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt; (2 lines, OK)
Walther@60571	945
Walther@60571	946	autoCalculate 1 (Steps 1);
Walther@60571	947	(setContext 1 p "thy_isac_Test-rls-Test_simplify";)
Walther@60571	948	val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
Walther@60571	949	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	950	if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + - 1 * 2 = 0"
Walther@60571	951	then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
Walther@60571	952
Walther@60571	953	autoCalculate 1 CompleteCalc;
Walther@60571	954	val (((pt,_),_), p) = (States.get_calc 1, States.get_pos 1 1);
Walther@60571	955	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	956
Walther@60571	957	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
Walther@60571	958	else error "--- setContext..Thy --- autoCalculate CompleteCalc";
Walther@60571	959	DEconstrCalcTree 1;
Walther@60571	960
Walther@60571	961	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
Walther@60571	962	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
Walther@60571	963	"--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
Walther@60571	964	States.reset ();
Walther@60571	965	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	966	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	967	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	968	Iterator 1; moveActiveRoot 1;
Walther@60571	969	autoCalculate 1 CompleteToSubpbl;
Walther@60571	970	refFormula 1 (States.get_pos 1 1); (<ISA> - 1 + x = 0 </ISA>);
Walther@60571	971	val ((pt,_),_) = States.get_calc 1;
Walther@60571	972	val str = pr_ctree pr_short pt;
Walther@60571	973	writeln str;
Walther@60571	974	if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n"
Walther@60571	975	then () else
Walther@60571	976	error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl- 1";
Walther@60571	977
Walther@60571	978	autoCalculate 1 (Steps 1); (proceeds only, if NOT 1 step before subplb)
Walther@60571	979	autoCalculate 1 CompleteToSubpbl;
Walther@60571	980	val ((pt,_),_) = States.get_calc 1;
Walther@60571	981	val str = pr_ctree pr_short pt;
Walther@60571	982	writeln str;
Walther@60571	983	autoCalculate 1 CompleteCalc; (das geht ohnehin !);
Walther@60571	984	val ((pt,_),_) = States.get_calc 1;
Walther@60571	985	val p = States.get_pos 1 1;
Walther@60571	986
Walther@60571	987	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	988	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
Walther@60571	989	error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
Walther@60571	990	DEconstrCalcTree 1;
Walther@60571	991
Walther@60571	992	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
Walther@60571	993	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
Walther@60571	994	"--------- rat-eq + subpbl: no_met, NO solution dropped -";
Walther@60571	995	"--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";
Walther@60571	996	(*--- THIS IS RE-USED WITH fun me IN test/../MathEngine/solve.sml -------------------
Walther@60571	997	---- rat-eq + subpbl: set_found in check_tac1 ----*)
Walther@60571	998	CalcTree @{context}
Walther@60571	999	[(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x", "solutions L"],
Walther@60571	1000	(( )"RatEq"( )"PolyEq"(required for "make_ratpoly_in"),
Walther@60571	1001	["univariate", "equation"], ["no_met"]))];
Walther@60571	1002	Iterator 1;
Walther@60571	1003	moveActiveRoot 1;
Walther@60571	1004	fetchProposedTactic 1;
Walther@60571	1005
Walther@60571	1006	setNextTactic 1 (Model_Problem);
Walther@60571	1007	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1008
Walther@60571	1009	setNextTactic 1 (Specify_Theory "RatEq");
Walther@60571	1010	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1011	setNextTactic 1 (Specify_Problem ["rational", "univariate", "equation"]);
Walther@60571	1012	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1013	setNextTactic 1 (Specify_Method ["RatEq", "solve_rat_equation"]);
Walther@60571	1014	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1015	setNextTactic 1 (Apply_Method ["RatEq", "solve_rat_equation"]);
Walther@60571	1016	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1017	setNextTactic 1 (Rewrite_Set "RatEq_simplify");
Walther@60571	1018	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1019	setNextTactic 1 (Rewrite_Set "norm_Rational");
Walther@60571	1020	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1021	setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
Walther@60571	1022	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1023	(* __________ for "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)"*)
Walther@60571	1024	setNextTactic 1 (Subproblem ("PolyEq", ["normalise", "polynomial",
Walther@60571	1025	"univariate", "equation"]));
Walther@60571	1026	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1027	setNextTactic 1 (Model_Problem );
Walther@60571	1028	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1029	setNextTactic 1 (Specify_Theory "PolyEq");
Walther@60571	1030	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1031	setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
Walther@60571	1032	"univariate", "equation"]);
Walther@60571	1033	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1034	setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
Walther@60571	1035	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1036	setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
Walther@60571	1037	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1038	setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
Walther@60571	1039	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1040	setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
Walther@60571	1041	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1042	(* __________ for "16 + 12 * x = 0"*)
Walther@60571	1043	setNextTactic 1 (Subproblem ("PolyEq",
Walther@60571	1044	["degree_1", "polynomial", "univariate", "equation"]));
Walther@60571	1045	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1046	setNextTactic 1 (Model_Problem );
Walther@60571	1047	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1048	setNextTactic 1 (Specify_Theory "PolyEq");
Walther@60571	1049	(------------- some trials in the problem-hierarchy ---------------)
Walther@60571	1050	setNextTactic 1 (Specify_Problem ["LINEAR", "univariate", "equation"]);
Walther@60571	1051	autoCalculate 1 (Steps 1); fetchProposedTactic 1; (<ERROR> helpless </ERROR> !!!)
Walther@60571	1052	setNextTactic 1 (Refine_Problem ["univariate", "equation"]);
Walther@60571	1053	(------------------------------------------------------------------)
Walther@60571	1054	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1055	setNextTactic 1 (Specify_Method ["PolyEq", "solve_d1_polyeq_equation"]);
Walther@60571	1056	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1057	setNextTactic 1 (Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]);
Walther@60571	1058	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1059	setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
Walther@60571	1060	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1061	setNextTactic 1 (Rewrite_Set "polyeq_simplify");
Walther@60571	1062	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1063	setNextTactic 1 Or_to_List;
Walther@60571	1064	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1065	setNextTactic 1 (Check_elementwise "Assumptions");
Walther@60571	1066	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1067	setNextTactic 1 (Check_Postcond ["degree_1", "polynomial",
Walther@60571	1068	"univariate", "equation"]);
Walther@60571	1069	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1070	setNextTactic 1 (Check_Postcond ["normalise", "polynomial",
Walther@60571	1071	"univariate", "equation"]);
Walther@60571	1072	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1073	setNextTactic 1 (Check_Postcond ["rational", "univariate", "equation"]);
Walther@60571	1074	val (ptp,_) = States.get_calc 1;
Walther@60571	1075	val (Form t,_,_) = ME_Misc.pt_extract ptp;
Walther@60571	1076	if States.get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
Walther@60571	1077	else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
Walther@60571	1078	DEconstrCalcTree 1;
Walther@60571	1079
Walther@60571	1080
Walther@60571	1081	\<close> ML \<open>
Walther@60571	1082	"--------- tryMatchProblem, tryRefineProblem ------------";
Walther@60571	1083	"--------- tryMatchProblem, tryRefineProblem ------------";
Walther@60571	1084	"--------- tryMatchProblem, tryRefineProblem ------------";
Walther@60571	1085	(*{\bf\UC{Having \isac{} Refine the Problem
Walther@60571	1086	* Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
Walther@60571	1087	* x \<up>2 + 4*x + 5 = 2
Walther@60571	1088	see isac.bridge.TestSpecify#testMatchRefine*)
Walther@60571	1089	States.reset ();
Walther@60571	1090	CalcTree @{context}
Walther@60571	1091	[(["equality (x \<up> 2 + 4*x + 5 = (2::real))", "solveFor x", "solutions L"],
Walther@60571	1092	("Isac_Knowledge",
Walther@60571	1093	["univariate", "equation"],
Walther@60571	1094	["no_met"]))];
Walther@60571	1095	Iterator 1;
Walther@60571	1096	moveActiveRoot 1;
Walther@60571	1097
Walther@60571	1098	fetchProposedTactic 1;
Walther@60571	1099	setNextTactic 1 (Model_Problem );
Walther@60571	1100	(..this tactic should be done 'tacitly', too !)
Walther@60571	1101
Walther@60571	1102	(*
Walther@60571	1103	autoCalculate 1 CompleteCalcHead;
Walther@60571	1104	checkContext 1 ([],Pbl) "pbl_equ_univ";
Walther@60571	1105	checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
Walther@60571	1106	*)
Walther@60571	1107
Walther@60571	1108	autoCalculate 1 (Steps 1);
Walther@60571	1109
Walther@60571	1110	fetchProposedTactic 1;
Walther@60571	1111	setNextTactic 1 (Add_Given "equality (x \<up> 2 + 4 * x + 5 = (2::real))");
Walther@60571	1112	autoCalculate 1 (Steps 1);
Walther@60571	1113
Walther@60571	1114	"--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
Walther@60571	1115	(initContext 1 Ptool.Pbl_ ([],Pbl);)
Walther@60571	1116	(* this would break if a calculation would be inserted before: CALCID...
Walther@60571	1117	and pattern matching is not available in *.java.
Walther@60571	1118	if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . TermC.matches (?a = ?b) (x \<up> ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"
Walther@60571	1119	then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
Walther@60571	1120	*)
Walther@60571	1121	(initContext 1 Ptool.Met_ ([],Pbl);)
Walther@60571	1122	(<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>)
Walther@60571	1123
Walther@60571	1124	"--------- this match will show some incomplete items: ---------";
Walther@60571	1125
Walther@60571	1126	(*checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);
Walther@60571	1127	checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);*)
Walther@60571	1128
Walther@60571	1129
Walther@60571	1130	fetchProposedTactic 1;
Walther@60571	1131	setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Steps 1);
Walther@60571	1132
Walther@60571	1133	fetchProposedTactic 1;
Walther@60571	1134	setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
Walther@60571	1135
Walther@60571	1136	"--------- this is a matching model (all items correct): -------";
Walther@60571	1137	(checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate", "equation"]);)
Walther@60571	1138	"--------- this is a NOT matching model (some 'false': ---------";
Walther@60571	1139	(checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR", "univariate", "equation"]);)
Walther@60571	1140
Walther@60571	1141	"--------- find out a matching problem: ------------------------";
Walther@60571	1142	"--------- find out a matching problem (FAILING: no new pbl) ---";
Walther@60571	1143	refineProblem 1 ([],Pbl)(Ptool.pblID2guh @{context} ["LINEAR", "univariate", "equation"]);
Walther@60571	1144
Walther@60571	1145	"--------- find out a matching problem (SUCCESSFUL) ------------";
Walther@60571	1146	refineProblem 1 ([],Pbl) (Ptool.pblID2guh @{context} ["univariate", "equation"]);
Walther@60571	1147
Walther@60571	1148	"--------- tryMatch, tryRefine did not change the calculation -";
Walther@60571	1149	"--------- this is done by <TRANSFER> on the pbl-browser: ------";
Walther@60571	1150	setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
Walther@60571	1151	"univariate", "equation"]);
Walther@60571	1152	autoCalculate 1 (Steps 1);
Walther@60571	1153	(*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",...
Walther@60571	1154	and Specify_Theory skipped in comparison to below --- \<up> -inserted *)
Walther@60571	1155	(------------vvv-inserted-----------------------------------------------)
Walther@60571	1156	fetchProposedTactic 1;
Walther@60571	1157	(/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\ )
Walther@60571	1158	setNextTactic 1 (Specify_Problem ["normalise", "polynomial",
Walther@60571	1159	"univariate", "equation"]);
Walther@60571	1160	autoCalculate 1 (Steps 1);
Walther@60571	1161
Walther@60571	1162	(and Specify_Theory skipped by fetchProposedTactic ?!?)
Walther@60571	1163
Walther@60571	1164	fetchProposedTactic 1;
Walther@60571	1165	setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
Walther@60571	1166	autoCalculate 1 (Steps 1);
Walther@60571	1167
Walther@60571	1168	fetchProposedTactic 1;
Walther@60571	1169	setNextTactic 1 (Apply_Method ["PolyEq", "normalise_poly"]);
Walther@60571	1170
Walther@60571	1171	autoCalculate 1 CompleteCalc;
Walther@60571	1172
Walther@60571	1173	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1174	Test_Tool.show_pt pt;
Walther@60571	1175	val p = States.get_pos 1 1;
Walther@60571	1176	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1177	if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
Walther@60571	1178	error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
Walther@60571	1179
Walther@60571	1180	(------------ \<up> -inserted-----------------------------------------------)
Walther@60571	1181	(*WN050904 the fetchProposedTactic's below may not have worked like that
Walther@60571	1182	before, too, because there was no check*)
Walther@60571	1183	fetchProposedTactic 1;
Walther@60571	1184	setNextTactic 1 (Specify_Theory "PolyEq");
Walther@60571	1185	autoCalculate 1 (Steps 1);
Walther@60571	1186
Walther@60571	1187	fetchProposedTactic 1;
Walther@60571	1188	setNextTactic 1 (Specify_Method ["PolyEq", "normalise_poly"]);
Walther@60571	1189	autoCalculate 1 (Steps 1);
Walther@60571	1190
Walther@60571	1191	fetchProposedTactic 1;
Walther@60571	1192	"--------- now the calc-header is ready for enter 'solving' ----";
Walther@60571	1193	autoCalculate 1 CompleteCalc;
Walther@60571	1194
Walther@60571	1195	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1196	rootthy pt;
Walther@60571	1197	Test_Tool.show_pt pt;
Walther@60571	1198	val p = States.get_pos 1 1;
Walther@60571	1199	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1200	if UnparseC.term f = "[x = - 1, x = -3]" andalso p = ([], Res) then () else
Walther@60571	1201	error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
Walther@60571	1202	DEconstrCalcTree 1;
Walther@60571	1203	( \-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/)
Walther@60571	1204
Walther@60571	1205	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
Walther@60571	1206	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
Walther@60571	1207	"--------- modifyCalcHead, resetCalcHead, modelProblem --";
Walther@60571	1208	States.reset ();
Walther@60571	1209	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1210	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1211	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1212	Iterator 1;
Walther@60571	1213	moveActiveRoot 1;
Walther@60571	1214
Walther@60571	1215	modifyCalcHead 1 (([],Pbl),(the position from refFormula)
Walther@60571	1216	"solve (x+1=2, x)",(the headline)
Walther@60571	1217	[P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
Walther@60571	1218	P_Spec.Find ["solutions L"](,P_Spec.Relate [])],
Walther@60571	1219	Pbl,
Walther@60571	1220	("Test",
Walther@60571	1221	["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1222	["Test", "squ-equ-test-subpbl1"]));
Walther@60571	1223
Walther@60571	1224	val ((Nd (PblObj {fmz = (fm, tpm),
Walther@60571	1225	loc = (SOME scrst_ctxt, NONE),
Walther@60571	1226	ctxt,
Walther@60571	1227	meth,
Walther@60571	1228	spec = (thy,
Walther@60571	1229	["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1230	["Test", "squ-equ-test-subpbl1"]),
Walther@60571	1231	probl,
Walther@60571	1232	branch = TransitiveB,
Walther@60571	1233	origin,
Walther@60571	1234	ostate = Incomplete,
Walther@60571	1235	result},
Walther@60571	1236	[]),
Walther@60571	1237	([], Pbl)),
Walther@60571	1238	[]) = States.get_calc 1;
Walther@60571	1239	(WN110622: is the same as in 2002, but shouldn't be probl = [3 items?])
Walther@60571	1240	if length meth = 0 andalso length probl = 0 (just some items tested) then ()
Walther@60571	1241	else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
Walther@60571	1242
Walther@60571	1243	resetCalcHead 1;
Walther@60571	1244	modelProblem 1;
Walther@60571	1245
Walther@60571	1246	States.get_calc 1;
Walther@60571	1247	val ((Nd (PblObj {fmz = (fm, tpm),
Walther@60571	1248	loc = (SOME scrst_ctxt, NONE),
Walther@60571	1249	ctxt,
Walther@60571	1250	meth,
Walther@60571	1251	spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
Walther@60571	1252	probl,
Walther@60571	1253	branch = TransitiveB,
Walther@60571	1254	origin,
Walther@60571	1255	ostate = Incomplete,
Walther@60571	1256	result},
Walther@60571	1257	[]),
Walther@60571	1258	([], Pbl)),
Walther@60571	1259	[]) = States.get_calc 1;
Walther@60571	1260	if length meth = 3 andalso length probl = 3 (just some items tested) then ()
Walther@60571	1261	else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
Walther@60571	1262
Walther@60571	1263	"--------- maximum-example, UC: Modeling an example -----";
Walther@60571	1264	"--------- maximum-example, UC: Modeling an example -----";
Walther@60571	1265	"--------- maximum-example, UC: Modeling an example -----";
Walther@60571	1266	(* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
Walther@60571	1267	see isac.bridge.TestModel#testEditItems
Walther@60571	1268	*)
Walther@60571	1269	val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
Walther@60571	1270	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
Walther@60571	1271	"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
Walther@60571	1272	"relations [A=ab, a/2=rsin alpha, b/2=r*cos (alpha::real)]",
Walther@60571	1273	(* \<up> these are the elements for the root-problem (in variants)*)
Walther@60571	1274	(vvv these are elements required for subproblems)
Walther@60571	1275	"boundVariable a", "boundVariable b", "boundVariable alpha",
Walther@60571	1276	"interval {x::real. 0 <= x & x <= 2*r}",
Walther@60571	1277	"interval {x::real. 0 <= x & x <= 2*r}",
Walther@60571	1278	"interval {x::real. 0 <= x & x <= pi}",
Walther@60571	1279	"errorBound (eps=(0::real))"]
Walther@60571	1280	(specifying is not interesting for this example)
Walther@60571	1281	val spec = ("Diff_App", ["maximum_of", "function"],
Walther@60571	1282	["Diff_App", "max_by_calculus"]);
Walther@60571	1283	(the empty model with descriptions for user-guidance by Model_Problem)
Walther@60571	1284	val empty_model = [P_Spec.Given ["fixedValues []"],
Walther@60571	1285	P_Spec.Find ["maximum", "valuesFor"],
Walther@60571	1286	P_Spec.Relate ["relations []"]];
Walther@60571	1287	DEconstrCalcTree 1;
Walther@60571	1288
Walther@60571	1289	"#################################################################";
Walther@60571	1290	States.reset ();
Walther@60571	1291	CalcTree @{context} [(elems, spec)];
Walther@60571	1292	Iterator 1;
Walther@60571	1293	moveActiveRoot 1;
Walther@60571	1294	refFormula 1 (States.get_pos 1 1);
Walther@60571	1295	(this gives a completely empty model)
Walther@60571	1296
Walther@60571	1297	fetchProposedTactic 1;
Walther@60571	1298	(fill the CalcHead with Descriptions...)
Walther@60571	1299	setNextTactic 1 (Model_Problem );
Walther@60571	1300	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	1301
Walther@60571	1302	(*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
Walther@60571	1303	!!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
Walther@60571	1304	(input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...)
Walther@60571	1305	modifyCalcHead 1 (([],Pbl) (position, from previous refFormula),
Walther@60571	1306	"Problem (Diff_App.thy, [maximum_of, function])",
Walther@60571	1307	(the head-form \<up> is not used for input here)
Walther@60571	1308	[P_Spec.Given ["fixedValues [r=Arbfix]"(new input)],
Walther@60571	1309	P_Spec.Find ["maximum b"(new input), "valuesFor"],
Walther@60571	1310	P_Spec.Relate ["relations"]],
Walther@60571	1311	(input (Arbfix will dissappear soon))
Walther@60571	1312	Pbl (belongsto),
Walther@60571	1313	References.empty (no input to the specification));
Walther@60571	1314
Walther@60571	1315	(*the user does not know, what 'superfluous' for 'maximum b' may mean
Walther@60571	1316	and asks what to do next*)
Walther@60571	1317	fetchProposedTactic 1;
Walther@60571	1318	(the student follows the advice)
Walther@60571	1319	setNextTactic 1 (Add_Find "maximum A"); (FIXME.17.11.03: does not yet work)
Walther@60571	1320	autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);
Walther@60571	1321
Walther@60571	1322	(this input completes the model)
Walther@60571	1323	modifyCalcHead 1 (([],Pbl), "not used here",
Walther@60571	1324	[P_Spec.Given ["fixedValues [r=Arbfix]"],
Walther@60571	1325	P_Spec.Find ["maximum A", "valuesFor [a,b]"(new input)],
Walther@60571	1326	P_Spec.Relate ["relations [A=a*b, \
Walther@60571	1327	\(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl, References.empty);
Walther@60571	1328
Walther@60571	1329	(*specification is not interesting and should be skipped by the dialogguide;
Walther@60571	1330	!!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
Walther@60571	1331	modifyCalcHead 1 (([],Pbl), "not used here",
Walther@60571	1332	[P_Spec.Given ["fixedValues [r=Arbfix]"],
Walther@60571	1333	P_Spec.Find ["maximum A", "valuesFor [a,b]"(new input)],
Walther@60571	1334	P_Spec.Relate ["relations [A=a*b, \
Walther@60571	1335	\(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
Walther@60571	1336	("Diff_App", Problem.id_empty, MethodC.id_empty));
Walther@60571	1337	modifyCalcHead 1 (([],Pbl), "not used here",
Walther@60571	1338	[P_Spec.Given ["fixedValues [r=Arbfix]"],
Walther@60571	1339	P_Spec.Find ["maximum A", "valuesFor [a,b]"(new input)],
Walther@60571	1340	P_Spec.Relate ["relations [A=a*b, \
Walther@60571	1341	\(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
Walther@60571	1342	("Diff_App", ["maximum_of", "function"],
Walther@60571	1343	MethodC.id_empty));
Walther@60571	1344	modifyCalcHead 1 (([],Pbl), "not used here",
Walther@60571	1345	[P_Spec.Given ["fixedValues [r=Arbfix]"],
Walther@60571	1346	P_Spec.Find ["maximum A", "valuesFor [a,b]"(new input)],
Walther@60571	1347	P_Spec.Relate ["relations [A=a*b, \
Walther@60571	1348	\(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]], Pbl,
Walther@60571	1349	("Diff_App", ["maximum_of", "function"],
Walther@60571	1350	["Diff_App", "max_by_calculus"]));
Walther@60571	1351	(this final calcHead now has STATUS 'complete' !)
Walther@60571	1352	DEconstrCalcTree 1;
Walther@60571	1353
Walther@60571	1354	(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
Walther@60571	1355	"--------- solve_linear from pbl-hierarchy --------------";
Walther@60571	1356	"--------- solve_linear from pbl-hierarchy --------------";
Walther@60571	1357	"--------- solve_linear from pbl-hierarchy --------------";
Walther@60571	1358	States.reset ();
Walther@60571	1359	val (fmz, sp) = ([], ("", ["LINEAR", "univariate", "equation", "test"], []));
Walther@60571	1360	CalcTree @{context} [(fmz, sp)];
Walther@60571	1361	Iterator 1; moveActiveRoot 1;
Walther@60571	1362	refFormula 1 (States.get_pos 1 1);
Walther@60571	1363	modifyCalcHead 1 (([],Pbl),"solve (1+- 1*2+x=(0::real))",
Walther@60571	1364	[P_Spec.Given ["equality (1+- 1*2+x=(0::real))", "solveFor x"],
Walther@60571	1365	P_Spec.Find ["solutions L"]],
Walther@60571	1366	Pbl,
Walther@60571	1367	("Test", ["LINEAR", "univariate", "equation", "test"],
Walther@60571	1368	["Test", "solve_linear"]));
Walther@60571	1369	autoCalculate 1 CompleteCalc;
Walther@60571	1370	refFormula 1 (States.get_pos 1 1);
Walther@60571	1371	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1372	val p = States.get_pos 1 1;
Walther@60571	1373	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1374	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
Walther@60571	1375	else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
Walther@60571	1376	DEconstrCalcTree 1;
Walther@60571	1377
Walther@60571	1378	"--------- solve_linear as in an algebra system (CAS)----";
Walther@60571	1379	"--------- solve_linear as in an algebra system (CAS)----";
Walther@60571	1380	"--------- solve_linear as in an algebra system (CAS)----";
Walther@60571	1381	(WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168)
Walther@60571	1382	States.reset ();
Walther@60571	1383	val (fmz, sp) = ([], ("", [], []));
Walther@60571	1384	CalcTree @{context} [(fmz, sp)];
Walther@60571	1385	Iterator 1; moveActiveRoot 1;
Walther@60571	1386	modifyCalcHead 1 (([],Pbl),"solveTest (1+- 1*2+x=0,x)", [], Pbl, ("", [], []));
Walther@60571	1387	autoCalculate 1 CompleteCalc;
Walther@60571	1388	refFormula 1 (States.get_pos 1 1);
Walther@60571	1389	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1390	val p = States.get_pos 1 1;
Walther@60571	1391	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1392	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
Walther@60571	1393	else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
Walther@60571	1394	DEconstrCalcTree 1;
Walther@60571	1395	*)
Walther@60571	1396
Walther@60571	1397	"--------- interSteps: on 'miniscript with mini-subpbl' -";
Walther@60571	1398	"--------- interSteps: on 'miniscript with mini-subpbl' -";
Walther@60571	1399	"--------- interSteps: on 'miniscript with mini-subpbl' -";
Walther@60571	1400	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1401	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1402	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1403	Iterator 1;
Walther@60571	1404	moveActiveRoot 1;
Walther@60571	1405	autoCalculate 1 CompleteCalc;
Walther@60571	1406	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1407	Test_Tool.show_pt pt;
Walther@60571	1408
Walther@60571	1409	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
Walther@60571	1410	interSteps 1 ([2],Res);
Walther@60571	1411	val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (new ([2,1],Frm)..([2,6],Res));
Walther@60571	1412	val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
Walther@60571	1413	getFormulaeFromTo 1 unc gen 1 false;
Walther@60571	1414
Walther@60571	1415	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
Walther@60571	1416	interSteps 1 ([3,2],Res);
Walther@60571	1417	val ((pt,_),_) = States.get_calc 1; Test_Tool.show_pt pt (new ([3,2,1],Frm)..([3,2,2],Res));
Walther@60571	1418	val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
Walther@60571	1419	getFormulaeFromTo 1 unc gen 1 false;
Walther@60571	1420
Walther@60571	1421	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
Walther@60571	1422	interSteps 1 ([3],Res) (no new steps in subproblems);
Walther@60571	1423	val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
Walther@60571	1424	getFormulaeFromTo 1 unc gen 1 false;
Walther@60571	1425
Walther@60571	1426	(UC\label{UC:inter-steps} UC 30.3.5.5 p.178)
Walther@60571	1427	interSteps 1 ([],Res) (no new steps in subproblems);
Walther@60571	1428	val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
Walther@60571	1429	getFormulaeFromTo 1 unc gen 1 false;
Walther@60571	1430	DEconstrCalcTree 1;
Walther@60571	1431
Walther@60571	1432	"--------- getTactic, fetchApplicableTactics ------------";
Walther@60571	1433	"--------- getTactic, fetchApplicableTactics ------------";
Walther@60571	1434	"--------- getTactic, fetchApplicableTactics ------------";
Walther@60571	1435	(* compare test/../script.sml
Walther@60571	1436	"----------- fun from_prog ---------------------------------------";
Walther@60571	1437	*)
Walther@60571	1438	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1439	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1440	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1441	Iterator 1; moveActiveRoot 1;
Walther@60571	1442	autoCalculate 1 CompleteCalc;
Walther@60571	1443	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1444	Test_Tool.show_pt pt;
Walther@60571	1445
Walther@60571	1446	(*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
Walther@60571	1447	WN120210 not impl. in FE*)
Walther@60571	1448	getTactic 1 ([],Pbl);
Walther@60571	1449	getTactic 1 ([1],Res);
Walther@60571	1450	getTactic 1 ([3],Pbl);
Walther@60571	1451	getTactic 1 ([3,1],Frm);
Walther@60571	1452	getTactic 1 ([3],Res);
Walther@60571	1453	getTactic 1 ([],Res);
Walther@60571	1454
Walther@60571	1455	(UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175)
Walther@60571	1456	fetchApplicableTactics 1 99999 ([],Pbl);
Walther@60571	1457	fetchApplicableTactics 1 99999 ([1],Res);
Walther@60571	1458	fetchApplicableTactics 1 99999 ([3],Pbl);
Walther@60571	1459	fetchApplicableTactics 1 99999 ([3,1],Res);
Walther@60571	1460	fetchApplicableTactics 1 99999 ([3],Res);
Walther@60571	1461	fetchApplicableTactics 1 99999 ([],Res);
Walther@60571	1462	DEconstrCalcTree 1;
Walther@60571	1463
Walther@60571	1464	(SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------\\ )
Walther@60571	1465	"--------- getAssumptions, getAccumulatedAsms -----------";
Walther@60571	1466	"--------- getAssumptions, getAccumulatedAsms -----------";
Walther@60571	1467	"--------- getAssumptions, getAccumulatedAsms -----------";
Walther@60571	1468	States.reset ();
Walther@60571	1469	CalcTree @{context}
Walther@60571	1470	[(["equality (x/(x \<up> 2 - 6x+9) - 1/(x \<up> 2 - 3x) =1/x)",
Walther@60571	1471	"solveFor x", "solutions L"],
Walther@60571	1472	("RatEq",["univariate", "equation"],["no_met"]))];
Walther@60571	1473	Iterator 1; moveActiveRoot 1;
Walther@60571	1474	autoCalculate 1 CompleteCalc;
Walther@60571	1475	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1476	val p = States.get_pos 1 1;
Walther@60571	1477	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1478	(*============ inhibit exn WN120316 compare 2002-- 2011 ===========================
Walther@60571	1479	if map UnparseC.term asms =
Walther@60571	1480	["True \|\n~ lhs ((3 + - 1 * x + x \<up> 2) * x =\n" ^
Walther@60571	1481	" 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)) is_poly_in x", "-6 * x + 5 * x \<up>\<up> 2 = 0",
Walther@60571	1482	"lhs (-6 * x + 5 * x \<up> 2 = 0) is_poly_in x",
Walther@60571	1483	"lhs (-6 * x + 5 * x \<up>\<up> 2 = 0) has_degree_in x = 2",
Walther@60571	1484	"9 * x + -6 * x \<up> 2 + x \<up> 3 ~= 0"]
Walther@60571	1485	andalso UnparseC.term f = "[-6 * x + 5 * x \<up> 2 = 0]" andalso p = ([], Res) then ()
Walther@60571	1486	else error "TODO compare 2002-- 2011"; (...data during test --- x / (x \<up> 2 - 6 x + 9) - 1...*)
Walther@60571	1487	============ inhibit exn WN120316 compare 2002-- 2011 ===========================*)
Walther@60571	1488
Walther@60571	1489	if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"
Walther@60571	1490	andalso map UnparseC.term asms = []
Walther@60571	1491	then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
Walther@60571	1492
Walther@60571	1493	(UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178)
Walther@60571	1494	getAssumptions 1 ([3], Res);
Walther@60571	1495	getAssumptions 1 ([5], Res);
Walther@60571	1496	(*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
Walther@60571	1497	WN0502 still without positions*)
Walther@60571	1498	getAccumulatedAsms 1 ([3], Res);
Walther@60571	1499	getAccumulatedAsms 1 ([5], Res);
Walther@60571	1500	DEconstrCalcTree 1;
Walther@60571	1501	( SINCE eliminate ThmC.numerals_to_Free: loops ---------------------------------------------//)
Walther@60571	1502
Walther@60571	1503	\<close> ML \<open>
Walther@60571	1504	"--------- arbitrary combinations of steps --------------";
Walther@60571	1505	"--------- arbitrary combinations of steps --------------";
Walther@60571	1506	"--------- arbitrary combinations of steps --------------";
Walther@60571	1507	CalcTree @{context} (start of calculation, return No.1)
Walther@60571	1508	[(["equality (1+- 1*2+x=(0::real))", "solveFor x", "solutions L"],
Walther@60571	1509	("Test",
Walther@60571	1510	["LINEAR", "univariate", "equation", "test"],
Walther@60571	1511	["Test", "solve_linear"]))];
Walther@60571	1512	Iterator 1; moveActiveRoot 1;
Walther@60571	1513
Walther@60571	1514	fetchProposedTactic 1;
Walther@60571	1515	(ERROR States.get_calc 1 not existent)
Walther@60571	1516	setNextTactic 1 (Model_Problem );
Walther@60571	1517	autoCalculate 1 (Steps 1);
Walther@60571	1518	fetchProposedTactic 1;
Walther@60571	1519	fetchProposedTactic 1;
Walther@60571	1520
Walther@60571	1521	setNextTactic 1 (Add_Find "solutions L");
Walther@60571	1522	setNextTactic 1 (Add_Find "solutions L");
Walther@60571	1523
Walther@60571	1524	autoCalculate 1 (Steps 1);
Walther@60571	1525	autoCalculate 1 (Steps 1);
Walther@60571	1526
Walther@60571	1527	setNextTactic 1 (Specify_Theory "Test");
Walther@60571	1528	fetchProposedTactic 1;
Walther@60571	1529	autoCalculate 1 (Steps 1);
Walther@60571	1530
Walther@60571	1531	autoCalculate 1 (Steps 1);
Walther@60571	1532	autoCalculate 1 (Steps 1);
Walther@60571	1533	autoCalculate 1 (Steps 1);
Walther@60571	1534	autoCalculate 1 (Steps 1);
Walther@60571	1535	(------------------------- end calc-head)
Walther@60571	1536
Walther@60571	1537	fetchProposedTactic 1;
Walther@60571	1538	setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
Walther@60571	1539	autoCalculate 1 (Steps 1);
Walther@60571	1540
Walther@60571	1541	setNextTactic 1 (Rewrite_Set "Test_simplify");
Walther@60571	1542	fetchProposedTactic 1;
Walther@60571	1543	autoCalculate 1 (Steps 1);
Walther@60571	1544
Walther@60571	1545	autoCalculate 1 CompleteCalc;
Walther@60571	1546	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1547	val p = States.get_pos 1 1;
Walther@60571	1548	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1549	if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
Walther@60571	1550	error "FE-interface.sml: diff.behav. in combinations of steps";
Walther@60571	1551	DEconstrCalcTree 1;
Walther@60571	1552
Walther@60571	1553	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (UC 30.3.2.4 p.175)
Walther@60571	1554	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
Walther@60571	1555	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
Walther@60571	1556	States.reset ();
Walther@60571	1557	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1558	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1559	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1560	Iterator 1;
Walther@60571	1561	moveActiveRoot 1;
Walther@60571	1562	autoCalculate 1 CompleteCalcHead;
Walther@60571	1563	autoCalculate 1 (Steps 1);
Walther@60571	1564	autoCalculate 1 (Steps 1);
Walther@60571	1565	appendFormula 1 "- 1 + x = 0" (\|> Future.join);
Walther@60571	1566	(... returns calcChangedEvent with)
Walther@60571	1567	val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
Walther@60571	1568	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
Walther@60571	1569
Walther@60571	1570	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1571	val p = States.get_pos 1 1;
Walther@60571	1572	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1573	if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
Walther@60571	1574	error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
Walther@60571	1575	DEconstrCalcTree 1;
Walther@60571	1576
Walther@60571	1577	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (UC 30.3.2.4 p.175)
Walther@60571	1578	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
Walther@60571	1579	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
Walther@60571	1580	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1581	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1582	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1583	Iterator 1;
Walther@60571	1584	moveActiveRoot 1;
Walther@60571	1585	autoCalculate 1 CompleteCalcHead;
Walther@60571	1586	autoCalculate 1 (Steps 1);
Walther@60571	1587	autoCalculate 1 (Steps 1);
Walther@60571	1588	appendFormula 1 "x - 1 = 0" (\|> Future.join);
Walther@60571	1589	val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
Walther@60571	1590	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
Walther@60571	1591	(11 elements !!!)
Walther@60571	1592
Walther@60571	1593	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1594	val p = States.get_pos 1 1;
Walther@60571	1595	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1596	if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
Walther@60571	1597	error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
Walther@60571	1598	DEconstrCalcTree 1;
Walther@60571	1599
Walther@60571	1600	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (UC 30.3.2.4 p.175)
Walther@60571	1601	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
Walther@60571	1602	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
Walther@60571	1603	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1604	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1605	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1606	Iterator 1;
Walther@60571	1607	moveActiveRoot 1;
Walther@60571	1608	autoCalculate 1 CompleteCalcHead;
Walther@60571	1609	autoCalculate 1 (Steps 1);
Walther@60571	1610	autoCalculate 1 (Steps 1);
Walther@60571	1611	appendFormula 1 "x = 1" (\|> Future.join);
Walther@60571	1612	(... returns calcChangedEvent with)
Walther@60571	1613	val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
Walther@60571	1614	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
Walther@60571	1615	(6 elements !!!)
Walther@60571	1616
Walther@60571	1617	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1618	val p = States.get_pos 1 1;
Walther@60571	1619	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1620	if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
Walther@60571	1621	error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
Walther@60571	1622	DEconstrCalcTree 1;
Walther@60571	1623
Walther@60571	1624	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (UC 30.3.2.4 p.175)
Walther@60571	1625	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
Walther@60571	1626	"--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
Walther@60571	1627	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1628	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1629	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1630	Iterator 1;
Walther@60571	1631	moveActiveRoot 1;
Walther@60571	1632	autoCalculate 1 CompleteCalcHead;
Walther@60571	1633	autoCalculate 1 (Steps 1);
Walther@60571	1634	autoCalculate 1 (Steps 1);
Walther@60571	1635	appendFormula 1 "x - 4711 = 0" (\|> Future.join);
Walther@60571	1636	(... returns <ERROR> no derivation found </ERROR>)
Walther@60571	1637
Walther@60571	1638	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1639	val p = States.get_pos 1 1;
Walther@60571	1640	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1641	if UnparseC.term f = "x + 1 + - 1 * 2 = 0" andalso p = ([1], Res) then () else
Walther@60571	1642	error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
Walther@60571	1643	DEconstrCalcTree 1;
Walther@60571	1644
Walther@60571	1645	"--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (UC 30.3.2.5 p.176)
Walther@60571	1646	"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
Walther@60571	1647	"--------- replaceFormula {SOL:MAN:FOR:replace} right----";
Walther@60571	1648	(\label{SOLVE:MANUAL:FORMULA:replace})
Walther@60571	1649	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1650	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1651	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1652	Iterator 1;
Walther@60571	1653	moveActiveRoot 1;
Walther@60571	1654	autoCalculate 1 CompleteCalc;
Walther@60571	1655	moveActiveFormula 1 ([2],Res);
Walther@60571	1656	replaceFormula 1 "- 1 + x = 0" (i.e. repeats input);
Walther@60571	1657	(... returns <ERROR> formula not changed </ERROR>)
Walther@60571	1658
Walther@60571	1659	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1660	val p = States.get_pos 1 1;
Walther@60571	1661	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1662	if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
Walther@60571	1663	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
Walther@60571	1664	if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
Walther@60571	1665	[([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
Walther@60571	1666	([3], Res), ([4], Res), ([], Res)] then () (nothing deleted!) else
Walther@60571	1667	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
Walther@60571	1668
Walther@60571	1669	(WN050211 replaceFormula didn't work on second ctree: thus now tested...)
Walther@60571	1670	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1671	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1672	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1673	Iterator 2; (! ! ! 1 CalcTree @{context} inbetween States.reset (); )
Walther@60571	1674	moveActiveRoot 2;
Walther@60571	1675	autoCalculate 2 CompleteCalc;
Walther@60571	1676	moveActiveFormula 2 ([2],Res);
Walther@60571	1677	replaceFormula 2 "- 1 + x = 0" (i.e. repeats input);
Walther@60571	1678	(... returns <ERROR> formula not changed </ERROR>)
Walther@60571	1679
Walther@60571	1680	val ((pt,_),_) = States.get_calc 2;
Walther@60571	1681	val p = States.get_pos 2 1;
Walther@60571	1682	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1683	if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
Walther@60571	1684	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
Walther@60571	1685	if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
Walther@60571	1686	[([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
Walther@60571	1687	([3], Res), ([4], Res), ([], Res)] then () (nothing deleted!) else
Walther@60571	1688	error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
Walther@60571	1689	DEconstrCalcTree 1;
Walther@60571	1690
Walther@60571	1691	"--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (UC 30.3.2.5 p.176)
Walther@60571	1692	"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
Walther@60571	1693	"--------- replaceFormula {SOL:MAN:FOR:replace} other----";
Walther@60571	1694	(\label{SOLVE:MANUAL:FORMULA:replace})
Walther@60571	1695	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1696	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1697	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1698	Iterator 1;
Walther@60571	1699	moveActiveRoot 1;
Walther@60571	1700	autoCalculate 1 CompleteCalc;
Walther@60571	1701	moveActiveFormula 1 ([2],Res); (there is "- 1 + x = 0")
Walther@60571	1702	replaceFormula 1 "x - 1 = 0"; (<-------------------------------------)
Walther@60571	1703	(... returns calcChangedEvent with)
Walther@60571	1704	val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
Walther@60571	1705	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
Walther@60571	1706
Walther@60571	1707	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1708	Test_Tool.show_pt pt;
Walther@60571	1709	val p = States.get_pos 1 1;
Walther@60571	1710	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1711	if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
Walther@60571	1712	error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
Walther@60571	1713	(* for getting the list in whole length ...
Walther@60571	1714	(default_print_depth 99) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (default_print_depth 3)
Walther@60571	1715	*)
Walther@60571	1716	if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
Walther@60571	1717	[([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
Walther@60571	1718	([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
Walther@60571	1719	([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
Walther@60571	1720	error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
Walther@60571	1721	DEconstrCalcTree 1;
Walther@60571	1722
Walther@60571	1723	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (UC 30.3.2.5 p.176)
Walther@60571	1724	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
Walther@60571	1725	"--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
Walther@60571	1726	(\label{SOLVE:MANUAL:FORMULA:replace})
Walther@60571	1727	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1728	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1729	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1730	Iterator 1;
Walther@60571	1731	moveActiveRoot 1;
Walther@60571	1732	autoCalculate 1 CompleteCalc;
Walther@60571	1733	moveActiveFormula 1 ([2],Res); (there is "- 1 + x = 0")
Walther@60571	1734	replaceFormula 1 "x = 1"; (<-------------------------------------)
Walther@60571	1735	(... returns calcChangedEvent with ...)
Walther@60571	1736	val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
Walther@60571	1737	getFormulaeFromTo 1 unc gen 99999 (all levels) false;
Walther@60571	1738	(9 elements !!!)
Walther@60571	1739
Walther@60571	1740	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1741	Test_Tool.show_pt pt; (error: ...ME_Misc.get_interval drops ([3,2],Res) ...)
Walther@60571	1742	val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
Walther@60571	1743	if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
Walther@60571	1744	[([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
Walther@60571	1745	([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
Walther@60571	1746	([3,2],Res)] then () else
Walther@60571	1747	error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
Walther@60571	1748
Walther@60571	1749	val p = States.get_pos 1 1;
Walther@60571	1750	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1751	if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
Walther@60571	1752	error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
Walther@60571	1753	DEconstrCalcTree 1;
Walther@60571	1754
Walther@60571	1755	\<close> ML \<open>
Walther@60571	1756	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (UC 30.3.2.5 p.176)
Walther@60571	1757	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
Walther@60571	1758	"--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
Walther@60571	1759	(\label{SOLVE:MANUAL:FORMULA:replace})
Walther@60571	1760	CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
Walther@60571	1761	("Test", ["sqroot-test", "univariate", "equation", "test"],
Walther@60571	1762	["Test", "squ-equ-test-subpbl1"]))];
Walther@60571	1763	Iterator 1;
Walther@60571	1764	moveActiveRoot 1;
Walther@60571	1765	autoCalculate 1 CompleteCalc;
Walther@60571	1766	moveActiveFormula 1 ([2],Res); (there is "- 1 + x = 0")
Walther@60571	1767	replaceFormula 1 "x - 4711 = 0";
Walther@60571	1768	(... returns <ERROR> no derivation found </ERROR>)
Walther@60571	1769
Walther@60571	1770	val ((pt,_),_) = States.get_calc 1;
Walther@60571	1771	Test_Tool.show_pt pt;
Walther@60571	1772	val p = States.get_pos 1 1;
Walther@60571	1773	val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1774	if UnparseC.term f = "- 1 + x = 0" andalso p = ([2], Res) then () else
Walther@60571	1775	error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
Walther@60571	1776	DEconstrCalcTree 1;
Walther@60571	1777
Walther@60571	1778	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
Walther@60571	1779	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
Walther@60571	1780	"--------- UC errpat chain-rule-diff-both, fillpat by input ------";
Walther@60571	1781	CalcTree @{context}
Walther@60571	1782	[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
Walther@60571	1783	("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
Walther@60571	1784	Iterator 1;
Walther@60571	1785	moveActiveRoot 1;
Walther@60571	1786	autoCalculate 1 CompleteCalcHead;
Walther@60571	1787	autoCalculate 1 (Steps 1);
Walther@60571	1788	autoCalculate 1 (Steps 1);(([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)))
Walther@60571	1789	appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (\|> Future.join); (<<<<<<<=========================)
Walther@60571	1790	(* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
Walther@60571	1791	would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
Walther@60571	1792	results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
Walther@60571	1793	instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
Walther@60571	1794	val ((pt,pos), _) = States.get_calc 1;
Walther@60571	1795	val p = States.get_pos 1 1;
Walther@60571	1796	val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1797
Walther@60571	1798	if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
Walther@60571	1799	then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
Walther@60571	1800	("diff_sum", thm)) => () \| _ => error "embed fun fill_form changed 0"
Walther@60571	1801	\| _ => error "embed fun fill_form changed 1"
Walther@60571	1802	else error "embed fun fill_form changed 2";
Walther@60571	1803
Walther@60571	1804	(*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
Walther@60571	1805	findFillpatterns 1 "chain-rule-diff-both"; (<<<<<<<=================================)
Walther@60571	1806	(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
Walther@60571	1807	d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
Walther@60571	1808	val ((pt,pos),_) = States.get_calc 1;
Walther@60571	1809	val p = States.get_pos 1 1;
Walther@60571	1810
Walther@60571	1811	val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1812	if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
Walther@60571	1813	get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(?!?)))
Walther@60571	1814	then ()
Walther@60571	1815	else error "embed fun fill_form changed 2";
Walther@60571	1816
Walther@60571	1817	(* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
Walther@60571	1818	and the last has no gaps, then the number of fill-patterns would suffice
Walther@60571	1819	for the DialogGuide to select appropriately. *)
Walther@60571	1820	requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(<<<<<<<============)
Walther@60571	1821	(<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>)
Walther@60571	1822	val ((pt,pos),_) = States.get_calc 1;
Walther@60571	1823	val p = States.get_pos 1 1;
Walther@60571	1824	val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1825	if p = ([1], Res) andalso existpt [2] pt andalso
Walther@60571	1826	UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up>\<up> 4))" andalso
Walther@60571	1827	get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
Walther@60571	1828	then () else error "embed fun fill_form changed 3";
Walther@60571	1829
Walther@60571	1830	inputFillFormula 1 "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)";(<<<<<<<=====)
Walther@60571	1831	val ((pt, _),_) = States.get_calc 1;
Walther@60571	1832	val p = States.get_pos 1 1;
Walther@60571	1833	val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1834	if p = ([2], Res) andalso
Walther@60571	1835	UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)" andalso
Walther@60571	1836	get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
Walther@60571	1837	then () else error "inputFillFormula changed 11";
Walther@60571	1838
Walther@60571	1839	autoCalculate 1 CompleteCalc;
Walther@60571	1840
Walther@60571	1841	"~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
Walther@60571	1842	val ((pt, _),_) = States.get_calc 1;
Walther@60571	1843	val p = States.get_pos 1 1;
Walther@60571	1844	val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
Walther@60571	1845	if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3"
Walther@60571	1846	then () else error "inputFillFormula changed 12";
Walther@60571	1847	Test_Tool.show_pt pt;
Walther@60571	1848	(*[
Walther@60571	1849	(([], Frm), Diff (x \<up> 2 + sin (x \<up> 4), x)),
Walther@60571	1850	(([1], Frm), d_d x (x \<up> 2 + sin (x \<up> 4))),
Walther@60571	1851	(([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))),
Walther@60571	1852	(([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)), (<<<<<<<=====)
Walther@60571	1853	(([3], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
Walther@60571	1854	(([4], Res), 2 * x \<up> (2 - 1) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))),
Walther@60571	1855	(([5], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3),
Walther@60571	1856	(([], Res), 2 * x + cos (x \<up> 4) * 4 * x \<up> 3)] *)
Walther@60571	1857	============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
Walther@60571	1858	DEconstrCalcTree 1;
Walther@60571	1859
Walther@60571	1860	\<close> ML \<open>
Walther@60571	1861	(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd ?)
Walther@60571	1862	"--------- UC errpat add-fraction, fillpat by input --------------";
Walther@60571	1863	"--------- UC errpat add-fraction, fillpat by input --------------";
Walther@60571	1864	"--------- UC errpat add-fraction, fillpat by input --------------";
Walther@60571	1865	(cp from BridgeLog Java <=> SML)
Walther@60571	1866	CalcTree @{context} [([], References.empty)];
Walther@60571	1867	Iterator 1;
Walther@60571	1868	moveActiveRoot 1;
Walther@60571	1869	moveActiveFormula 1 ([],Pbl);
Walther@60571	1870	replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
Walther@60571	1871	autoCalculate 1 CompleteCalcHead;
Walther@60571	1872	autoCalculate 1 (Steps 1);
Walther@60571	1873	appendFormula 1 "8 * x / (8 * y)" (\|> Future.join);
Walther@60571	1874	(*<CALCMESSAGE> no derivation found </CALCMESSAGE>
Walther@60571	1875	--- but in BridgeLog Java <=> SML:
Walther@60571	1876	<CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
Walther@60571	1877	DEconstrCalcTree 1;
Walther@60571	1878	-----------------------------------------------------------------------------------------------*)
Walther@60571	1879
Walther@60571	1880	\<close> ML \<open>
Walther@60571	1881	"--------- UC errpat, fillpat step to Rewrite --------------------";
Walther@60571	1882	"--------- UC errpat, fillpat step to Rewrite --------------------";
Walther@60571	1883	"--------- UC errpat, fillpat step to Rewrite --------------------";
Walther@60571	1884	(TODO)
Walther@60571	1885	CalcTree @{context}
Walther@60571	1886	[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
Walther@60571	1887	"differentiateFor x", "derivative f_f'"],
Walther@60571	1888	("Isac_Knowledge", ["derivative_of", "function"],
Walther@60571	1889	["diff", "differentiate_on_R"]))]; (<<<======= EP is directly in script)
Walther@60571	1890	Iterator 1;
Walther@60571	1891	moveActiveRoot 1;
Walther@60571	1892	autoCalculate 1 CompleteCalc;
Walther@60571	1893	val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
Walther@60571	1894	DEconstrCalcTree 1;
Walther@60571	1895
Walther@60571	1896	\<close> ML \<open>
Walther@60571	1897	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
Walther@60571	1898	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
Walther@60571	1899	"--------- UC errpat, fillpat step to Rewrite_Set ----------------";
Walther@60571	1900	CalcTree @{context}
Walther@60571	1901	[(["functionTerm ((x \<up> 2) \<up> 3 + sin (x \<up> 4))",
Walther@60571	1902	"differentiateFor x", "derivative f_f'"],
Walther@60571	1903	("Isac_Knowledge", ["derivative_of", "function"],
Walther@60571	1904	["diff", "after_simplification"]))]; (<<<======= EP is in a ruleset)
Walther@60571	1905	Iterator 1;
Walther@60571	1906	moveActiveRoot 1;
Walther@60571	1907	autoCalculate 1 CompleteCalcHead;
Walther@60571	1908	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1909	autoCalculate 1 (Steps 1); fetchProposedTactic 1;
Walther@60571	1910	(*
Walther@60571	1911	<NEXTTAC>
Walther@60571	1912	<CALCID> 1 </CALCID>
Walther@60571	1913	<TACTICERRORPATTERNS>
Walther@60571	1914	<STRINGLIST>
Walther@60571	1915	<STRING> chain-rule-diff-both </STRING>
Walther@60571	1916	<STRING> cancel </STRING>
Walther@60571	1917	</STRINGLIST>
Walther@60571	1918	<REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
Walther@60571	1919	<RULESET> norm_diff </RULESET>
Walther@60571	1920	<SUBSTITUTION>
Walther@60571	1921	<PAIR>
Walther@60571	1922	<VARIABLE>
Walther@60571	1923	<MATHML>
Walther@60571	1924	<ISA> bdv </ISA>
Walther@60571	1925	</MATHML>
Walther@60571	1926	</VARIABLE>
Walther@60571	1927	<VALUE>
Walther@60571	1928	<MATHML>
Walther@60571	1929	<ISA> x </ISA>
Walther@60571	1930	</MATHML>
Walther@60571	1931	</VALUE>
Walther@60571	1932	</PAIR>
Walther@60571	1933	</SUBSTITUTION>
Walther@60571	1934	</REWRITESETINSTTACTIC>
Walther@60571	1935	</TACTICERRORPATTERNS>
Walther@60571	1936	</NEXTTAC>
Walther@60571	1937
Walther@60571	1938
Walther@60571	1939	(WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_))
Walther@60571	1940	stepToErrorPatterns 1; (--> calcChanged, rule immediately calls... )
Walther@60571	1941	stepOnErrorPatterns 1; (--> calcChanged, rule calls getTactic and displays it )
Walther@60571	1942	(* then --- UC errpat, fillpat by input ---*)
Walther@60571	1943	*)
Walther@60571	1944	autoCalculate 1 CompleteCalc;
Walther@60571	1945	val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
Walther@60571	1946	(WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_))
Walther@60571	1947	DEconstrCalcTree 1;
Walther@60571	1948
Walther@60558	1949	\<close> ML \<open>
Walther@60558	1950	\<close> ML \<open>
Walther@60558	1951	\<close>
wneuper@59600	1952
wneuper@59472	1953	ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59472	1954	ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59472	1955	ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
wneuper@59559	1956	ML \<open>
wneuper@59559	1957	\<close> ML \<open>
wneuper@59559	1958	\<close> ML \<open>
walther@59817	1959	\<close> ML \<open>
walther@59817	1960	\<close> ML \<open>
wneuper@59559	1961	\<close>
neuper@41943	1962
wneuper@59472	1963	section \<open>history of tests\<close>
wneuper@59472	1964	text \<open>
neuper@48895	1965	Systematic regression tests have been introduced to isac development in 2003.
neuper@52139	1966	Sanity of the regression tests suffers from updates following Isabelle development,
neuper@48895	1967	which mostly exceeded the resources available in isac's development.
neuper@48895	1968
neuper@48895	1969	The survey below shall support to efficiently use the tests for isac
neuper@48895	1970	on different Isabelle versions. Conclusion in most cases will be:
neuper@48895	1971
neuper@48895	1972	!!! Use most recent tests or go back to the old notebook
neuper@48895	1973	with isac on Isabelle2002. !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
wneuper@59472	1974	\<close>
neuper@48895	1975
wneuper@59323	1976
wneuper@59472	1977	subsection \<open>isac on Isabelle2017\<close>
wneuper@59472	1978	subsubsection \<open>Summary of development\<close>
wneuper@59472	1979	text \<open>
wneuper@59449	1980	* Add further signatures, separate structures and cleanup respective files.
wneuper@59449	1981	* Show feasibility of moving Isac programs to partial_function, i.e. to the function package.
wneuper@59449	1982	* Clean theory dependencies.
wneuper@59449	1983	* Start preparing shift from isac-java to Isabelle/jEdit.
wneuper@59472	1984	\<close>
wneuper@59472	1985	subsubsection \<open>State of tests: unchanged\<close>
wneuper@59472	1986	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	1987	text \<open>
wneuper@59449	1988	last changeset with Test_Isac 925fef0f4c81
wneuper@59449	1989	first changeset with Test_Isac bbb414976dfe
wneuper@59472	1990	\<close>
wneuper@59449	1991
wneuper@59472	1992	subsection \<open>isac on Isabelle2015\<close>
wneuper@59472	1993	subsubsection \<open>Summary of development\<close>
wneuper@59472	1994	text \<open>
wneuper@59373	1995	* Add signatures from top of thy-hierarchy down to Interpret (not ProgLang).
wneuper@59323	1996	This complicates Test_Isac, see "Prepare running tests" above.
wneuper@59323	1997	* Remove TTY interface.
wneuper@59323	1998	* Re-activate insertion sort.
wneuper@59472	1999	\<close>
wneuper@59472	2000	subsubsection \<open>State of tests: unchanged\<close>
wneuper@59472	2001	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2002	text \<open>
wneuper@59323	2003	last changeset with Test_Isac 2f1b2854927a
wneuper@59323	2004	first changeset with Test_Isac ???
wneuper@59472	2005	\<close>
wneuper@59323	2006
wneuper@59472	2007	subsection \<open>isac on Isabelle2014\<close>
wneuper@59472	2008	subsubsection \<open>Summary of development\<close>
wneuper@59472	2009	text \<open>
wneuper@59120	2010	migration from "isabelle tty" --> libisabelle
wneuper@59472	2011	\<close>
wneuper@59120	2012
wneuper@59472	2013	subsection \<open>isac on Isabelle2013-2\<close>
wneuper@59472	2014	subsubsection \<open>Summary of development\<close>
wneuper@59472	2015	text \<open>
wneuper@55500	2016	reactivated context_thy
wneuper@59472	2017	\<close>
wneuper@59472	2018	subsubsection \<open>State of tests\<close>
wneuper@59472	2019	text \<open>
neuper@55319	2020	TODO
wneuper@59472	2021	\<close>
wneuper@59472	2022	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2023	text \<open>
neuper@55319	2024	TODO
neuper@55319	2025	:
neuper@55319	2026	: isac on Isablle2013-2
neuper@55319	2027	:
neuper@55319	2028	Changeset: 55318 (03826ceb24da) merged
neuper@55319	2029	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@55319	2030	Date: 2013-12-12 14:27:37 +0100 (7 minutes)
wneuper@59472	2031	\<close>
neuper@55319	2032
wneuper@59472	2033	subsection \<open>isac on Isabelle2013-1\<close>
wneuper@59472	2034	subsubsection \<open>Summary of development\<close>
wneuper@59472	2035	text \<open>
neuper@55284	2036	Isabelle2013-1 was replaced within a few weeks due to problems with the document model;
neuper@55284	2037	no significant development steps for ISAC.
wneuper@59472	2038	\<close>
wneuper@59472	2039	subsubsection \<open>State of tests\<close>
wneuper@59472	2040	text \<open>
neuper@55284	2041	See points in subsection "isac on Isabelle2011", "State of tests".
wneuper@59472	2042	\<close>
wneuper@59472	2043	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2044	text \<open>
neuper@55284	2045	Changeset: 55283 (d6e9a34e7142) notes for resuming work on Polynomial.thy
neuper@55284	2046	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@55284	2047	Date: 2013-12-03 18:13:31 +0100 (8 days)
neuper@55284	2048	:
neuper@55284	2049	: isac on Isablle2013-1
neuper@55284	2050	:
neuper@55284	2051	Changeset: 55279 (130688f277ba) Isabelle2013 --> 2013-1: Test_Isac perfect
neuper@55284	2052	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@55284	2053	Date: 2013-11-21 18:12:17 +0100 (2 weeks)
neuper@55284	2054
wneuper@59472	2055	\<close>
neuper@55284	2056
wneuper@59472	2057	subsection \<open>isac on Isabelle2013\<close>
wneuper@59472	2058	subsubsection \<open>Summary of development\<close>
wneuper@59472	2059	text \<open>
neuper@52150	2060	# Oct.13: replaced "axioms" by "axiomatization"
neuper@52150	2061	# Oct.13: Mathias Lehnfeld started removing Unsynchornized.ref
neuper@52106	2062	# Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
neuper@52106	2063	simplification of multivariate rationals (without improving the rulesets involved).
wneuper@59472	2064	\<close>
wneuper@59472	2065	subsubsection \<open>Run tests\<close>
wneuper@59472	2066	text \<open>
neuper@52150	2067	Is standard now; this subsection will be discontinued under Isabelle2013-1
wneuper@59472	2068	\<close>
wneuper@59472	2069	subsubsection \<open>State of tests\<close>
wneuper@59472	2070	text \<open>
neuper@52150	2071	See points in subsection "isac on Isabelle2011", "State of tests".
neuper@52150	2072	# re-activated listC.sml
wneuper@59472	2073	\<close>
wneuper@59472	2074	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2075	text \<open>
neuper@52175	2076	changeset 52174:8b055b17bd84 --- removed all code concerned with "castab = Unsynchronized.ref"
neuper@52175	2077	User: Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
neuper@52175	2078	Date: Tue Nov 19 22:23:30 2013 +0000
neuper@52079	2079	:
neuper@52079	2080	: isac on Isablle2013
neuper@52079	2081	:
neuper@52079	2082	Changeset: 52061 (4ecea2fcdc2c) --- Build_Isac.thy runs on Isabelle2013
neuper@52079	2083	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@52079	2084	Date: 2013-07-15 08:28:50 +0200 (4 weeks)
wneuper@59472	2085	\<close>
neuper@48895	2086
wneuper@59472	2087	subsection \<open>isac on Isabelle2012\<close>
wneuper@59472	2088	subsubsection \<open>Summary of development\<close>
wneuper@59472	2089	text \<open>
neuper@48895	2090	isac on Isabelle2012 is considered just a transitional stage
neuper@48895	2091	within the update from Isabelle2011 to Isabelle2013; thus no further development of isac;
neuper@48895	2092	For considerations on the transition see
wenzelm@60192	2093	$ISABELLE_ISAC/Knowledge/Build_Thydata/thy, section "updating isac..".
wneuper@59472	2094	\<close>
wneuper@59472	2095	subsubsection \<open>Run tests\<close>
wneuper@59472	2096	text \<open>
neuper@48895	2097	$ cd /usr/local/isabisac12/
neuper@48895	2098	$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
neuper@48895	2099	$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
wneuper@59472	2100	\<close>
wneuper@59472	2101	subsubsection \<open>State of tests\<close>
wneuper@59472	2102	text \<open>
neuper@48895	2103	At least the tests from isac on Isabelle2011 run again.
neuper@48895	2104	However, Test_Isac.thy shows erratic behaviour; no errors are obtained when scrolling
neuper@48895	2105	in parallel with evaluation.
neuper@48895	2106
neuper@48895	2107	Counting "error in kernel" for Frontend/interface.sml (the tests considered most significant)
neuper@48895	2108	yields 69 hits, some of which were already present before Isabelle2002-->2009-2
neuper@48895	2109	(i.e. on the old notebook from 2002).
neuper@48895	2110
neuper@48895	2111	Now many tests with (...=== inhibit exn ...) give a reason or at least the origin:
neuper@48895	2112	# === inhibit exn WN1130621 Isabelle2012-->13 !thehier! === ...see Build_Thydata.thy
neuper@48895	2113	# === inhibit exn AK110726 === ...reliable work by Alexander Kargl, most likely go back to 2002
neuper@48895	2114	# === inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 === , most likely go back to 2002
neuper@48895	2115	Reasons for outcommented tests are also found in Test_Isac.thy near the respective file.sml.
neuper@48895	2116
neuper@48895	2117	Some tests have been re-activated (e.g. error patterns, fill patterns).
wneuper@59472	2118	\<close>
wneuper@59472	2119	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2120	text \<open>
neuper@52079	2121	Changeset: 52051 (35751d90365e) end of improving tests for isac on Isabelle2012
neuper@52079	2122	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@52079	2123	Date: 2013-07-11 16:58:31 +0200 (4 weeks)
neuper@48895	2124	:
neuper@48895	2125	: isac on Isablle2012
neuper@48895	2126	:
neuper@48895	2127	Changeset: 48757 (74eb3dfc33cc) updated src from Isabelle2011 to Isabelle2012
neuper@48895	2128	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@48895	2129	Date: 2012-09-24 18:35:13 +0200 (8 months)
neuper@48895	2130	------------------------------------------------------------------------------
neuper@48895	2131	Changeset: 48756 (7443906996a8) merged
neuper@48895	2132	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@48895	2133	Date: 2012-09-24 18:15:49 +0200 (8 months)
wneuper@59472	2134	\<close>
neuper@48895	2135
wneuper@59472	2136	subsection \<open>isac on Isabelle2011\<close>
wneuper@59472	2137	subsubsection \<open>Summary of development\<close>
wneuper@59472	2138	text \<open>
neuper@48895	2139	isac's mathematics engine has been extended by two developments:
neuper@48895	2140	(1) Isabelle's contexts were introduced by Mathias Lehnfeld
neuper@52150	2141	(2) Z_Transform was introduced by Jan Rocnik, which revealed
neuper@52150	2142	further errors introduced by (1).
neuper@52150	2143	(3) "error patterns" were introduced by Gabriella Daroczy
neuper@52150	2144	Regressions tests have been added for all of these.
wneuper@59472	2145	\<close>
wneuper@59472	2146	subsubsection \<open>Run tests\<close>
wneuper@59472	2147	text \<open>
neuper@48895	2148	$ cd /usr/local/isabisac11/
neuper@48895	2149	$ ./bin/isabelle jedit -l HOL src/Tools/isac/Build_Isac.thy
neuper@48895	2150	$ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy
wneuper@59472	2151	\<close>
wneuper@59472	2152	subsubsection \<open>State of tests\<close>
wneuper@59472	2153	text \<open>
neuper@48895	2154	Systematic efforts outcommented less significant tests by (...=== inhibit exn ...)
neuper@48895	2155	and sometimes give reasons for failing tests.
neuper@48895	2156	(...=== inhibit exn AK...) was done by Alexander Kargl; this is reliable
neuper@48895	2157	work, some of which couldn't be revised (and renamed) by WN and thus survived some time.
neuper@48895	2158
neuper@48895	2159	The most signification tests (in particular Frontend/interface.sml) run,
neuper@48895	2160	however, many "error in kernel" are not caught by an exception.
neuper@48895	2161	------------------------------------------------------------------------------
neuper@48895	2162	After the changeset below Test_Isac worked with check_unsynchronized_ref ():
neuper@48895	2163	------------------------------------------------------------------------------
neuper@48895	2164	Changeset: 42457 (ca691a84b81a) PROVISIONALLY MADE TESTS RUN with Unsynchronized.ref
neuper@48895	2165	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@48895	2166	Date: 2012-08-06 10:38:11 +0200 (11 months)
neuper@52150	2167
neuper@52150	2168
neuper@52150	2169	The list below records TODOs while producing an ISAC kernel for
neuper@52150	2170	gdaroczy and jrocnik, wich could NOT be done before all tests are RUNNING
neuper@52150	2171	(so to be resumed with Isabelle2013-1):
neuper@52150	2172	############## WNxxxxxx.TODO can be found in sources ##############
neuper@52150	2173	--------------------------------------------------------------------------------
neuper@52150	2174	WN111013.TODO: lots of cleanup/removal in test/../Test.thy
neuper@52150	2175	--------------------------------------------------------------------------------
walther@59845	2176	WN111013.TODO: remove concept around "fun implicit_take", lots of troubles with
neuper@52150	2177	this special case (see) --- why not nxt = Model_Problem here ? ---
neuper@52150	2178	--------------------------------------------------------------------------------
neuper@52150	2179	WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
neuper@52150	2180	... FIRST redesign
neuper@52150	2181	# simplify_* , _simp_
neuper@52150	2182	# norm_*
neuper@52150	2183	# calc_* , calculate_* ... require iteration over all rls ...
neuper@52150	2184	... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
neuper@52150	2185	--------------------------------------------------------------------------------
neuper@52150	2186	WN111014.TODO fun prep_rls \| !!!use this function in ruleset' := !!!
neuper@52150	2187	--------------------------------------------------------------------------------
neuper@52150	2188	WN120314 changeset a393bb9f5e9f drops root equations.
neuper@52150	2189	see test/Tools/isac/Knowledge/rootrateq.sml
neuper@52150	2190	--------------------------------------------------------------------------------
neuper@52150	2191	WN120317.TODO changeset 977788dfed26 dropped rateq:
neuper@52150	2192	# test --- repair NO asms from rls RatEq_eliminate --- shows error from 2002
neuper@52150	2193	# test --- solve (1/x = 5, x) by me --- and --- x / (x ^ 2 - 6 * x + 9) - ...:
neuper@52150	2194	investigation Check_elementwise stopped due to too much effort finding out,
neuper@52150	2195	why Check_elementwise worked in 2002 in spite of the error.
neuper@52150	2196	--------------------------------------------------------------------------------
neuper@52150	2197	WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl
neuper@52150	2198	--------------------------------------------------------------------------------
neuper@52150	2199	WN120317.TODO found by test --- interSteps for Schalk 299a --- that
neuper@52150	2200	NO test with 'interSteps' is checked properly (with exn on changed behaviour)
neuper@52150	2201	--------------------------------------------------------------------------------
neuper@52150	2202	WN120317.TODO test --- Matthias Goldgruber 2003 rewrite orders --- has
neuper@52150	2203	a newly outcommented test where rewrite_set_ make_polynomial --> NONE
neuper@52150	2204	--------------------------------------------------------------------------------
neuper@52150	2205	WN120320.TODO check-improve rlsthmsNOTisac:
neuper@52150	2206	DONE make test --- old compute rlsthmsNOTisac by eq_thmI'
neuper@52150	2207	DONE compare rlsthmsNOTisac in thms-survey-Isa02-Isa09-2.sml .. Isac.thy
neuper@52150	2208	FOUND 120321: Theory.axioms_of doesnt find LENGTH_CONS etc, thus are in Isab
neuper@52150	2209	# mark twice thms (in isac + (later) in Isabelle) in Isac.thy
neuper@52150	2210	--------------------------------------------------------------------------------
neuper@52150	2211	WN120320.TODO rlsthmsNOTisac: replace twice thms ^
neuper@52150	2212	--------------------------------------------------------------------------------
neuper@52150	2213	WN120320.TODO rlsthmsNOTisac: reconsider design of sym_* thms, see test
neuper@52150	2214	--- OLD compute rlsthmsNOTisac by eq_thmID ---: some are in isab, some in isac.
neuper@52150	2215	--------------------------------------------------------------------------------
neuper@52150	2216	WN120321.TODO rearrange theories:
neuper@52150	2217	Knowledge
neuper@52150	2218	:
walther@59603	2219	Prog_Expr.thy
walther@60125	2220	///Input_Descript.thy --> ProgLang
walther@59603	2221	Delete.thy <--- first_Knowledge_thy (mv to Prog_Expr.thy)
neuper@52150	2222	ProgLang: restructure Build_Isac.thy such that no xmlsrc.thy, ProgLang.thy
neuper@52150	2223	Interpret.thy are generated (simplifies xml structure for theories)
wneuper@59585	2224	Program.thy
neuper@52150	2225	Tools.thy
neuper@52150	2226	ListC.thy <--- first_Proglang_thy
neuper@52150	2227	--------------------------------------------------------------------------------
neuper@52150	2228	WN120321.TODO reanimate test/../simplify.sml: CAS-command Simplify
neuper@52150	2229	EXN "simplify.sml: diff.behav. CAScmd: Simplify (2a + 3a)"
neuper@52150	2230	broken during work on thy-hierarchy
neuper@52150	2231	--------------------------------------------------------------------------------
neuper@52150	2232	WN120321.TODO LAST in IsacScripts + in IsacKnowledge, see
neuper@55421	2233	test --- the_hier (get_thes ()) (collect_thydata ())---
neuper@52150	2234	--------------------------------------------------------------------------------
neuper@52150	2235	WN120405a.TODO src/../pbl-met-hierarchy.sml: fun pbl2term--> Isac' instead Isac_
neuper@52150	2236	!!add mutual crossreferences to ?fun headline??? where the same has to be done:
neuper@52150	2237	!!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
neuper@52150	2238	--------------------------------------------------------------------------------
neuper@52150	2239	WN120411 scanning html representation of newly generated knowledge:
neuper@52150	2240	* thy:
neuper@52150	2241	** Theorems: only "Proof of the theorem" (correct!)
neuper@52150	2242	and "(c) isac-team (math-autor)"
neuper@52150	2243	** Rulesets: only "Identifier:///"
neuper@52150	2244	and "(c) isac-team (math-autor)"
neuper@52150	2245	** IsacKnowledge: link to dependency graph (which needs to be created first)
neuper@52150	2246	** IsacScripts --> ProgramLanguage
neuper@52150	2247	*** Tools: Theorems: arity_type_cp, arity_type_nam, ... wegnehmen
neuper@52150	2248
neuper@52150	2249	* pbl: OK !?!
neuper@52150	2250	* met: OK !?!
neuper@52150	2251	* exp:
neuper@52150	2252	** Z-Transform is missing !!!
neuper@52150	2253	** type-constraints !!!
neuper@52150	2254	--------------------------------------------------------------------------------
neuper@52150	2255	WN120417: merging xmldata revealed:
neuper@52150	2256	..............NEWLY generated:........................................
neuper@52150	2257	<THEOREMDATA>
neuper@52150	2258	<GUH> thy_isab_Fun-thm-o_apply </GUH>
neuper@52150	2259	<STRINGLIST>
neuper@52150	2260	<STRING> Isabelle </STRING>
neuper@52150	2261	<STRING> Fun </STRING>
neuper@52150	2262	<STRING> Theorems </STRING>
neuper@52150	2263	<STRING> o_apply </STRING>
neuper@52150	2264	</STRINGLIST>
neuper@52150	2265	<MATHML>
neuper@52150	2266	<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
neuper@52150	2267	</MATHML> <PROOF>
neuper@52150	2268	<EXTREF>
neuper@52150	2269	<TEXT> Proof of the theorem </TEXT>
neuper@52150	2270	<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
neuper@52150	2271	</EXTREF>
neuper@52150	2272	</PROOF>
neuper@52150	2273	<EXPLANATIONS> </EXPLANATIONS>
neuper@52150	2274	<MATHAUTHORS>
neuper@52150	2275	<STRING> Isabelle team, TU Munich </STRING>
neuper@52150	2276	</MATHAUTHORS>
neuper@52150	2277	<COURSEDESIGNS>
neuper@52150	2278	</COURSEDESIGNS>
neuper@52150	2279	</THEOREMDATA>
neuper@52150	2280	..............OLD FORMAT:.............................................
neuper@52150	2281	<THEOREMDATA>
neuper@52150	2282	<GUH> thy_isab_Fun-thm-o_apply </GUH>
neuper@52150	2283	<STRINGLIST>
neuper@52150	2284	<STRING> Isabelle </STRING>
neuper@52150	2285	<STRING> Fun </STRING>
neuper@52150	2286	<STRING> Theorems </STRING>
neuper@52150	2287	<STRING> o_apply </STRING>
neuper@52150	2288	</STRINGLIST>
neuper@52150	2289	<THEOREM>
neuper@52150	2290	<ID> o_apply </ID>
neuper@52150	2291	<MATHML>
neuper@52150	2292	<ISA> (?f o ?g) ?x = ?f (?g ?x) </ISA>
neuper@52150	2293	</MATHML>
neuper@52150	2294	</THEOREM>
neuper@52150	2295	<PROOF>
neuper@52150	2296	<EXTREF>
neuper@52150	2297	<TEXT> Proof of the theorem </TEXT>
neuper@52150	2298	<URL> http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser_info/HOL/HOL-Real/Isac/Fun.html </URL>
neuper@52150	2299	</EXTREF>
neuper@52150	2300	</PROOF>
neuper@52150	2301	<EXPLANATIONS> </EXPLANATIONS>
neuper@52150	2302	<MATHAUTHORS>
neuper@52150	2303	<STRING> Isabelle team, TU Munich </STRING>
neuper@52150	2304	</MATHAUTHORS>
neuper@52150	2305	<COURSEDESIGNS>
neuper@52150	2306	</COURSEDESIGNS>
neuper@52150	2307	</THEOREMDATA>
neuper@52150	2308	--------------------------------------------------------------------------------
wneuper@59472	2309	\<close>
wneuper@59472	2310	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2311	text \<open>
neuper@48895	2312	isac development was done between these changesets:
neuper@48895	2313	------------------------------------------------------------------------------
neuper@48895	2314	Changeset: 42519 (1f3b4270363e) meeting dmeindl: added missing files
neuper@48895	2315	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@48895	2316	Date: 2012-09-24 16:39:30 +0200 (8 months)
neuper@48895	2317	:
neuper@48895	2318	: isac on Isablle2011
neuper@48895	2319	:
neuper@48895	2320	Changeset:41897 (355be7f60389) merged isabisac with Isabelle2011
neuper@48895	2321	Branch: decompose-isar
neuper@48895	2322	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@48895	2323	Date: 2011-02-25 13:04:56 +0100 (2011-02-25)
neuper@48895	2324	------------------------------------------------------------------------------
wneuper@59472	2325	\<close>
neuper@48895	2326
wneuper@59472	2327	subsection \<open>isac on Isabelle2009-2\<close>
wneuper@59472	2328	subsubsection \<open>Summary of development\<close>
wneuper@59472	2329	text \<open>
neuper@48895	2330	In 2009 the update of isac from Isabelle2002 started with switching from CVS to hg.
neuper@48895	2331	The update was painful (bridging 7 years of Isabelle development) and cut short
neuper@48895	2332	due to the start of introducing Isabelle's contexts (Mathias Lehnfeld) and
neuper@48895	2333	going on to Isabelle2011 although most of the tests did not run.
wneuper@59472	2334	\<close>
wneuper@59472	2335	subsubsection \<open>Run tests\<close>
wneuper@59472	2336	text \<open>
neuper@52150	2337	WN131021 this is broken by installation of Isabelle2011/12/13,
neuper@52150	2338	because all these write their binaries to ~/.isabelle/heaps/..
neuper@52150	2339
neuper@48895	2340	$ cd /usr/local/isabisac09-2/
neuper@48895	2341	$ ./bin/isabelle emacs -l HOL src/Tools/isac/Build_Isac.thy
neuper@48895	2342	$ ./bin/isabelle emacs -l Isac src/Tools/isac/Test_Isac.thy
neuper@48895	2343	NOT THE RIGHT VERSION..... test/Tools/isac/Test_Isac.thy !!!
wneuper@59472	2344	\<close>
wneuper@59472	2345	subsubsection \<open>State of tests\<close>
wneuper@59472	2346	text \<open>
neuper@48895	2347	Most tests are broken by the update from Isabelle2002 to Isabelle2009-2.
wneuper@59472	2348	\<close>
wneuper@59472	2349	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2350	text \<open>
neuper@48895	2351	isac development was done between these changesets:
neuper@48895	2352	------------------------------------------------------------------------------
neuper@48895	2353	Changeset: 38115 (940a5feea094) Little improvements of isac-plugin
neuper@48895	2354	Branch: decompose-isar
neuper@48895	2355	User: Marco Steger <m.steger@student.tugraz.at>
neuper@48895	2356	Date: 2011-02-06 18:30:28 +0100 (2011-02-06)
neuper@48895	2357	:
neuper@48895	2358	: isac on Isablle2009-2
neuper@48895	2359	:
neuper@48895	2360	Changeset: 37870 (5100a9c3abf8) created branch isac-from-Isabelle2009-2
neuper@48895	2361	Branch: isac-from-Isabelle2009-2
neuper@48895	2362	User: Walther Neuper <neuper@ist.tugraz.at>
neuper@48895	2363	Date: 2010-07-21 09:59:35 +0200 (2010-07-21)
neuper@48895	2364	------------------------------------------------------------------------------
wneuper@59472	2365	\<close>
neuper@48895	2366
wneuper@59472	2367	subsection \<open>isac on Isabelle2002\<close>
wneuper@59472	2368	subsubsection \<open>Summary of development\<close>
wneuper@59472	2369	text \<open>
neuper@48895	2370	From 1999 to 2010 all the basic functionality (except "ctxt" and "error pattern")
neuper@48895	2371	of isac's mathematics engine has been implemented.
wneuper@59472	2372	\<close>
wneuper@59472	2373	subsubsection \<open>Run tests\<close>
wneuper@59472	2374	subsubsection \<open>State of tests\<close>
wneuper@59472	2375	text \<open>
neuper@48895	2376	All tests work on an old notebook (the right PolyML coudn't be upgraded to more
neuper@48895	2377	recent Linux versions)
wneuper@59472	2378	\<close>
wneuper@59472	2379	subsubsection \<open>Changesets of begin and end\<close>
wneuper@59472	2380	text \<open>
neuper@48895	2381	Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
neuper@48895	2382	see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
wneuper@59472	2383	\<close>
neuper@48895	2384
neuper@41943	2385	end
neuper@52065	2386	(*========== inhibit exn 130719 Isabelle2013 ===================================
neuper@52065	2387	============ inhibit exn 130719 Isabelle2013 =================================*)
neuper@41943	2388
neuper@41943	2389	(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
neuper@48895	2390	-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
neuper@41975	2391

author	wneuper <Walther.Neuper@jku.at>
	Thu, 20 Oct 2022 10:23:38 +0200
changeset 60571	19a172de0bb5
parent 60567	bb3140a02f3d
child 60572	5bbcda519d27
permissions	-rw-r--r--