# HG changeset patch # User Walther Neuper # Date 1288250687 -7200 # Node ID 549ae735517e555776a5d765e1ed668a65817ef6 # Parent 356e0272d5651c78986701301e5bd80ba6a9ca1f intermed. repair thehier, the hierarchy of thy/thm for access by isac. Problem with Theory.thms_of dropped from 2002 to 2009. Now used Theory.axioms_of returning terms, which will cause problems, when isac's Knowledge will prove axioms to thms. intermed.: PureThy.all_thms_of cannot replace Theory.thms_of, but Thm.derivation_name contains all data required ...TODO. diff -r 356e0272d565 -r 549ae735517e src/Tools/isac/Interpret/rewtools.sml --- a/src/Tools/isac/Interpret/rewtools.sml Mon Oct 11 14:22:50 2010 +0200 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 28 09:24:47 2010 +0200 @@ -351,13 +351,13 @@ (**.set up isab_thm_thy in Isac.ML.**) -fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm)); -fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm)); +fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, prop_of thm)); +fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term)); (*.lookup the missing theorems in some thy (of Isabelle).*) fun make_isa missthms thy = map (pair (theory2thyID thy)) - ((inter eq_thmI) missthms (PureThy.all_thms_of thy)) + ((inter eq_thmI) missthms [] (*PureThy.all_thms_of thy*)) : (thyID * (thmID * Thm.thm)) list; (*.separate handling of sym_thms.*) @@ -375,14 +375,15 @@ ((apsnd o apsnd) sym_thm)) symsym_isab val isab = notsym_isab @ symsym_isab @ sym_isab - in ((map rearrange) o (gen_sort les)) isab - : (thmID * (thyID * Thm.thm)) list + in ((map rearrange) o (gen_sort les)) isab : (thmID * (thyID * term)) list end; +(* (* version with term instead of thm, for Theory.axioms_of in isa02*) fun make_isa missthms thy = map (pair (theory2thyID thy)) ((inter eq_thmI') missthms (Theory.axioms_of thy)) : (thyID * (thmID * term)) list; +(* separate handling of sym_thms *) fun make_isab rlsthmsNOTisac isab_thys = let fun les ((s1,_), (s2,_)) = (s1 : string) < s2 val notsym = filter_out (is_sym o #1) rlsthmsNOTisac @@ -400,6 +401,7 @@ in ((map rearrange) o (gen_sort les)) isab : (thmID * (thyID * term)) list end; +*) (*.which theory below thy' contains a theorem; this can be in isabelle ! get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*) diff -r 356e0272d565 -r 549ae735517e src/Tools/isac/Knowledge/Isac.thy --- a/src/Tools/isac/Knowledge/Isac.thy Mon Oct 11 14:22:50 2010 +0200 +++ b/src/Tools/isac/Knowledge/Isac.thy Thu Oct 28 09:24:47 2010 +0200 @@ -26,9 +26,8 @@ val isabthys = Theory.ancestors_of first_isac_thy; val isacthys = subtract Theory.eq_thy isabthys allthys; - val isacrlsthms = ((map (apsnd prop_of)) o - (gen_distinct eq_thmI) o (map rep_thm_G') o flat o - (map (thms_of_rls o #2 o #2))) (!ruleset'); + val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o + (map (thms_of_rls o #2 o #2))) (! ruleset'); val isacthms = (flat o (map Theory.axioms_of)) isacthys : (thmID * term) list; (*in*) diff -r 356e0272d565 -r 549ae735517e src/Tools/isac/Test_Isac.thy --- a/src/Tools/isac/Test_Isac.thy Mon Oct 11 14:22:50 2010 +0200 +++ b/src/Tools/isac/Test_Isac.thy Thu Oct 28 09:24:47 2010 +0200 @@ -31,11 +31,12 @@ cd "../.."; *) ML{* writeln "**** run systests complete ******************************" *}; + +use"../../../test/Tools/isac/calcelems.sml"; (*complete*) + (* cd"smltest/Scripts"; *) - - use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*) @@ -53,8 +54,9 @@ *) use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*) use "../../../test/Tools/isac/Interpret/calchead.sml"; +ML {*print_depth 999*} +use "../../../test/Tools/isac/Interpret/rewtools.sml"; (**) (* - use"rewtools.sml"; use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *); use"inform.sml"; use"me.sml"; @@ -63,10 +65,9 @@ cd"smltest/xmlsrc"; use"datatypes.sml"; use"pbl-met-hierarchy.sml"; - use"thy-hierarchy.sml"; - cd "../.."; -cd"smltest/FE-interface"; +use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"; (**) *) + use"../../../test/Tools/isac/Frontend/interface.sml"; (**) (* cd "../.."; @@ -107,8 +108,12 @@ use"biegelinie.sml"; use"algein.sml"; *) -ML {*print_depth 999*} +ML {* +val thm = @{thm refl}; +prop_of thm; +*} use "../../../test/Tools/isac/Knowledge/isac.sml"; (**) +ML {*print_depth 3*} ML {*111*} @@ -122,7 +127,9 @@ *** Theory loader: the error(s) above occurred while examining theory "Foo_Language" use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test" -*) +*)use "../../../test/Pure/library.sml" (**) +use_thy "../../../test/Pure/General/Basics" + use_thy "../../../test/Pure/Isar/Test_Parse_Term" use_thy "../../../test/Pure/Isar/Test_Parsers" diff -r 356e0272d565 -r 549ae735517e src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Mon Oct 11 14:22:50 2010 +0200 +++ b/src/Tools/isac/calcelems.sml Thu Oct 28 09:24:47 2010 +0200 @@ -7,7 +7,10 @@ (c) isac-team 2003 *) - +(* +structure CalcElems = +struct +*) val linefeed = (curry op^) "\n"; type authors = string list; @@ -146,11 +149,15 @@ fun thm_of_thm (Thm (_, thm)) = thm | thm_of_thm _ = error "thm_of_thm"; fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); + +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); +fun thyID_of_derivation_name dn = hd (space_explode "." dn); + fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) = (strip_thy thmid1) = (strip_thy thmid2); (*version typed weaker WN100910*) fun eq_thmI' ((thmid1, _), (thmid2, _)) = - (strip_thy thmid1) = (strip_thy thmid2); + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); val string_of_thm = Thm.get_name_hint; (*FIXME.2009*) @@ -355,6 +362,7 @@ -> (term * term) (*(t1, t2) to be compared *) -> bool)) (*if t1 <= t2 then true else false *) list); (*association list *) + rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord), ("dummy_ord", dummy_ord)]); @@ -406,9 +414,11 @@ val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""}; type thehier = (thydata ptyp) list; -val thehier = Unsynchronized.ref ([] : thehier); +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*) -(*.an association list, gets the value once in Isac.ML.*) +(* an association list, gets the value once in Isac.ML. + stores Isabelle's thms as terms for compatibility with Theory.axioms_of. + WN1-1-28 make this data arguments and del ref ?*) val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list); @@ -668,3 +678,6 @@ | ldr2str D = "D"; fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k; +(* +end (*struct*) +*) diff -r 356e0272d565 -r 549ae735517e test/Pure/General/Basics.thy --- a/test/Pure/General/Basics.thy Mon Oct 11 14:22:50 2010 +0200 +++ b/test/Pure/General/Basics.thy Thu Oct 28 09:24:47 2010 +0200 @@ -1,8 +1,5 @@ (* Title: ~~~/isac/smltest/Pure/General/Basics.thy - Author: Walther Neuper, TU Graz - -$ cd /usr/local/Isabelle2009-1/src/Pure/isac/smltest/Pure/General -$ /usr/local/isabisac/bin/isabelle emacs Scan.thy & + Author: Walther Neuper, TU Graz, 101027 *) header {* testing combinators from src/Pure/General/basics diff -r 356e0272d565 -r 549ae735517e test/Pure/library.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Pure/library.sml Thu Oct 28 09:24:47 2010 +0200 @@ -0,0 +1,23 @@ +(* Title: trials on library.ML + Author: Walther Neuper, TU Graz, 101027 +*) + +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- fun foldl_map ------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; + + +"----------- fun foldl_map ------------------------------"; +"----------- fun foldl_map ------------------------------"; +"----------- fun foldl_map ------------------------------"; +fun arg1 (a, b) = (a, b + 10); +val arg2 = [("a1", 1), ("a2", 2), ("a3", 3)]; +(*========== inhibit exn ======================================================= +foldl_map arg1 arg2; (*why is this not known here, but the others below ?*) +============ inhibit exn =====================================================*) +random; +last_elem; diff -r 356e0272d565 -r 549ae735517e test/Tools/isac/Interpret/rewtools.sml --- a/test/Tools/isac/Interpret/rewtools.sml Mon Oct 11 14:22:50 2010 +0200 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Oct 28 09:24:47 2010 +0200 @@ -1,51 +1,107 @@ (* test for sml/ME/rewtools.sml authors: Walther Neuper 2000, 2006 - (c) due to copyright terms - -use"../smltest/ME/rewtools.sml"; -use"rewtools.sml"; *) -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"----------- fun collect_isab_thys -------------------------------"; -"----------- fun thy_containing_thm ------------------------------"; -"----------- fun thy_containing_rls ------------------------------"; -"----------- fun thy_containing_cal ------------------------------"; -"----------- initContext Thy_ Integration-demo -------------------"; -"----------- initContext..Thy_, fun context_thm ------------------"; -"----------- initContext..Thy_, fun context_rls ------------------"; -"----------- checkContext..Thy_, fun context_thy -----------------"; -"----------- checkContext..Thy_, fun context_rls -----------------"; -"----------- checkContext..Thy_ on last formula ------------------"; -"----------- fun guh2theID ---------------------------------------"; -"----------- debugging on Tests/solve_linear_as_rootpbl ----------"; -"-----------------------------------------------------------------"; -"----------- fun string_of_thmI for_[.]_) ------------------------"; -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; -"-----------------------------------------------------------------"; -"----------- fun filter_appl_rews --------------------------------"; -"----------- fun is_contained_in ---------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- fun make_isa -------------------------------"; +"----------- fun collect_isab_thys ----------------------"; +"----------- fun thy_containing_thm ---------------------"; +"----------- fun thy_containing_rls ---------------------"; +"----------- fun thy_containing_cal ---------------------"; +"----------- initContext Thy_ Integration-demo ----------"; +"----------- initContext..Thy_, fun context_thm ---------"; +"----------- initContext..Thy_, fun context_rls ---------"; +"----------- checkContext..Thy_, fun context_thy --------"; +"----------- checkContext..Thy_, fun context_rls --------"; +"----------- checkContext..Thy_ on last formula ---------"; +"----------- fun guh2theID ------------------------------"; +"----------- debugging on Tests/solve_linear_as_rootpbl -"; +"--------------------------------------------------------"; +"----------- fun string_of_thmI for_[.]_) ---------------"; +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._["; +"--------------------------------------------------------"; +"----------- fun filter_appl_rews -----------------------"; +"----------- fun is_contained_in ------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"----------- fun make_isa -------------------------------"; +"----------- fun make_isa -------------------------------"; +"----------- fun make_isa -------------------------------"; +map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*) +["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL", + "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False", + "sym_real_mult_minus1", "left_distrib", "right_distrib", + "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right", + "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right", + "add_0_left", "add_0_right", "divide_zero_left", "sym_real_mult_assoc", + "real_le_refl", "minus_minus", "real_mult_commute", "real_mult_assoc", + "add_commute", "add_left_commute", "add_assoc", "minus_mult_left", + "right_minus", "sym_add_assoc", "left_diff_distrib", + "right_diff_distrib", "minus_divide_left", "times_divide_eq_right", + "times_divide_eq_left", "divide_divide_eq_left", + "divide_divide_eq_right", "divide_1", "add_divide_distrib", + "sym_rmult_assoc"]; +if length rlsthmsNOTisac > 40 then () +else error "rewtools.sml: some rlsthmsNOTisac dropped"; -"----------- fun collect_isab_thys -------------------------------"; -"----------- fun collect_isab_thys -------------------------------"; -"----------- fun collect_isab_thys -------------------------------"; -val thy = first_isac_thy (*def. in Script/ListG.ML*); -val {ancestors,...} = rep_theory thy; -print_depth 99; map string_of_thy ancestors; print_depth 3; -length ancestors; -val ancestors = (#ancestors o rep_theory) first_isac_thy; -length ancestors; -print_depth 99; map theory2theory' ancestors; print_depth 3; -val isabthms = (flat o (map PureThy.all_thms_of)) ancestors; -length isabthms; +"----- find the respectiv"; -val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset'); + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +val thys = ["thy1","thy2","thy3","thy4","thy5"]; +val thms = [("thm1", 1),("thm2", 21),"thm3","thm4","thm5"]; + + +val (missthms, thy) = (rlsthmsNOTisac, theory "Rings"); +"--- step into make_isa --"; +map (strip_thy o #1) (Theory.axioms_of thy); +map (strip_thy o #1) (Theory.all_axioms_of thy); + +inter (op =) (map #1 rlsthmsNOTisac) + (map (strip_thy o #1) (Theory.axioms_of thy)); +"--------------------------------------------------------"; + +map (strip_thy o #1) (Theory.axioms_of (theory "ListC")); +map (strip_thy o #1) (Theory.all_axioms_of (theory "ListC")); +"--------------------------------------------------------"; + +PureThy.get_thms thy "divide_zero_left"; + +"--------------------------------------------------------"; +map (strip_thy o #1) (PureThy.all_thms_of (theory "Groebner_Basis")); +"--------------------------------------------------------"; +Theory.ancestors_of (theory "Groebner_Basis"); +"===================="; +"----- this thm has the current theory as thy_ref ---"; +rep_thm @{thm "divide_zero_left"}; +"--------------------------------------------------------"; +"----- this thm has 'Rings' as thy_ref ---"; +rep_thm (hd (PureThy.get_thms (theory "Rings") "divide_zero_left")); +"--------------------------------------------------------"; +#thy_ref (rep_thm (hd (PureThy.get_thms (theory "Rings") "divide_zero_left"))); +"--------------------------------------------------------"; +theory_of_thm (hd (PureThy.get_thms (theory "Rings") "divide_zero_left")); + +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) + +1111111; + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +GOON: isabelle-dev: Theory.thms_of ??? + + +"----------- fun collect_isab_thys ----------------------"; +"----------- fun collect_isab_thys ----------------------"; +"----------- fun collect_isab_thys ----------------------"; +val ancestors = Theory.ancestors_of (theory "Complex_Main"); +val isabthms = (flat o (map Theory.axioms_of)) ancestors; + +val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset'); (*thms from rulesets*) val isacrlsthms = ((map rep_thm_G') o flat o (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset'); @@ -96,10 +152,12 @@ print_depth 99; isab_thm_thy; print_depth 3; *) +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) -"----------- fun thy_containing_thm ------------------------------"; -"----------- fun thy_containing_thm ------------------------------"; -"----------- fun thy_containing_thm ------------------------------"; +(*=== inhibit exn ?============================================================= +"----------- fun thy_containing_thm ---------------------"; +"----------- fun thy_containing_thm ---------------------"; +"----------- fun thy_containing_thm ---------------------"; val (str, (thy', thy)) = ("real_diff_minus",("Root", Root.thy)); if thy_contains_thm str ("XXX",thy) then () else error "rewtools.sml: NOT thy_contains_thm \ @@ -136,9 +194,9 @@ \thy_containing_thm Test radd_commute"; -"----------- fun thy_containing_rls ------------------------------"; -"----------- fun thy_containing_rls ------------------------------"; -"----------- fun thy_containing_rls ------------------------------"; +"----------- fun thy_containing_rls ---------------------"; +"----------- fun thy_containing_rls ---------------------"; +"----------- fun thy_containing_rls ---------------------"; val thy' = "Biegelinie"; val dropthys = takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory')) @@ -149,7 +207,10 @@ dropthys; print_depth 99; dropthy's; print_depth 3; -(*WN100819======================================================== +(*WN100819======================================================= +WN100819 THIS DATE MUST BE WRONG: at this date changeset 37934:56f10b13005e +finished update ME/calchead.sml + pushed updates over all sml+test + "Isac" mem dropthy's; op mem ("Isac", dropthy's); (op mem) o swap; @@ -173,9 +234,9 @@ else error "rewtools.sml: diff.behav. in thy_containing_rls 3"; -"----------- fun thy_containing_cal ------------------------------"; -"----------- fun thy_containing_cal ------------------------------"; -"----------- fun thy_containing_cal ------------------------------"; +"----------- fun thy_containing_cal ---------------------"; +"----------- fun thy_containing_cal ---------------------"; +"----------- fun thy_containing_cal ---------------------"; val thy' = "Atools"; val dropthys = takewhile [] (not o (curry op= thy') o (#1:theory' * theory -> theory')) @@ -189,11 +250,11 @@ map (#1 : calc -> string) (rev (!calclist')); val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o (#1 : calc -> string)) (rev (!calclist')); -========================================================WN100819*) +WN100819 =====================================================*) -"----------- initContext Thy_ Integration-demo -------------------"; -"----------- initContext Thy_ Integration-demo -------------------"; -"----------- initContext Thy_ Integration-demo -------------------"; +"----------- initContext Thy_ Integration-demo ----------"; +"----------- initContext Thy_ Integration-demo ----------"; +"----------- initContext Thy_ Integration-demo ----------"; states:=[]; CalcTree [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"], @@ -212,9 +273,9 @@ initContext 1 Thy_ ([1,1,1], Frm); --------------------TODO.new_c: cvs before 071227, 11:50*) -"----------- initContext..Thy_, fun context_thm ------------------"; -"----------- initContext..Thy_, fun context_thm ------------------"; -"----------- initContext..Thy_, fun context_thm ------------------"; +"----------- initContext..Thy_, fun context_thm ---------"; +"----------- initContext..Thy_, fun context_thm ---------"; +"----------- initContext..Thy_, fun context_thm ---------"; states:=[]; CalcTree (*start of calculation, return No.1*) [(["equality (x+1=2)", "solveFor x","solutions L"], @@ -258,9 +319,9 @@ --- in initContext..Thy_ ---*) -"----------- initContext..Thy_, fun context_rls ------------------"; -"----------- initContext..Thy_, fun context_rls ------------------"; -"----------- initContext..Thy_, fun context_rls ------------------"; +"----------- initContext..Thy_, fun context_rls ---------"; +"----------- initContext..Thy_, fun context_rls ---------"; +"----------- initContext..Thy_, fun context_rls ---------"; (*using pt from above*) val p = ([1], Res); val tac = Rewrite_Set "Test_simplify"; @@ -283,10 +344,9 @@ else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add"; - -"----------- checkContext..Thy_, fun context_thy -----------------"; -"----------- checkContext..Thy_, fun context_thy -----------------"; -"----------- checkContext..Thy_, fun context_thy -----------------"; +"----------- checkContext..Thy_, fun context_thy --------"; +"----------- checkContext..Thy_, fun context_thy --------"; +"----------- checkContext..Thy_, fun context_thy --------"; (*using pt from above*) val p = ([2,4], Res); @@ -318,9 +378,9 @@ --- in checkContext..Thy_ ---*) -"----------- checkContext..Thy_, fun context_rls -----------------"; -"----------- checkContext..Thy_, fun context_rls -----------------"; -"----------- checkContext..Thy_, fun context_rls -----------------"; +"----------- checkContext..Thy_, fun context_rls --------"; +"----------- checkContext..Thy_, fun context_rls --------"; +"----------- checkContext..Thy_, fun context_rls --------"; (*using pt from above*) show_pt pt; @@ -343,9 +403,9 @@ else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv"; -"----------- checkContext..Thy_ on last formula ------------------"; -"----------- checkContext..Thy_ on last formula ------------------"; -"----------- checkContext..Thy_ on last formula ------------------"; +"----------- checkContext..Thy_ on last formula ---------"; +"----------- checkContext..Thy_ on last formula ---------"; +"----------- checkContext..Thy_ on last formula ---------"; states:=[]; CalcTree (*start of calculation, return No.1*) [(["equality (x+1=2)", "solveFor x","solutions L"], @@ -366,10 +426,9 @@ checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify"; - -"----------- fun guh2theID ---------------------------------------"; -"----------- fun guh2theID ---------------------------------------"; -"----------- fun guh2theID ---------------------------------------"; +"----------- fun guh2theID ------------------------------"; +"----------- fun guh2theID ------------------------------"; +"----------- fun guh2theID ------------------------------"; val guh = "thy_scri_ListG-thm-zip_Nil"; take_fromto 1 4 (explode guh); @@ -390,10 +449,10 @@ else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed"; -"----------- debugging on Tests/solve_linear_as_rootpbl ----------"; -"----------- debugging on Tests/solve_linear_as_rootpbl ----------"; -"----------- debugging on Tests/solve_linear_as_rootpbl ----------"; -"----- initContext -----"; +"----------- debugging on Tests/solve_linear_as_rootpbl -"; +"----------- debugging on Tests/solve_linear_as_rootpbl -"; +"----------- debugging on Tests/solve_linear_as_rootpbl -"; +----- initContext -----"; states:=[]; CalcTree [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"], @@ -436,9 +495,9 @@ checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify"; -"----------- fun string_of_thmI for_[.]_) ------------------------"; -"----------- fun string_of_thmI for_[.]_) ------------------------"; -"----------- fun string_of_thmI for_[.]_) ------------------------"; +"----------- fun string_of_thmI for_[.]_) ---------------"; +"----------- fun string_of_thmI for_[.]_) ---------------"; +"----------- fun string_of_thmI for_[.]_) ---------------"; "----- these work ?!?"; val th = sym_thm real_minus_eq_cancel; val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel)); @@ -477,9 +536,9 @@ " = " ^ string_of_thmI thm); -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----"; +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._["; +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._["; +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._["; states:=[]; CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y", "RandbedingungenBiegung [y 0 = 0, y L = 0]", @@ -500,9 +559,9 @@ getTactic 1 ([1],Frm); -"----------- fun filter_appl_rews --------------------------------"; -"----------- fun filter_appl_rews --------------------------------"; -"----------- fun filter_appl_rews --------------------------------"; +"----------- fun filter_appl_rews -----------------------"; +"----------- fun filter_appl_rews -----------------------"; +"----------- fun filter_appl_rews -----------------------"; val f = str2term "a + z + 2*a + 3*z + 5 + 6"; val thy = assoc_thy "Isac"; val subst = [(*TODO.WN071231 test Rewrite_Inst*)]; @@ -517,9 +576,9 @@ else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6"; -"----------- fun is_contained_in ---------------------------------"; -"----------- fun is_contained_in ---------------------------------"; -"----------- fun is_contained_in ---------------------------------"; +"----------- fun is_contained_in ------------------------"; +"----------- fun is_contained_in ------------------------"; +"----------- fun is_contained_in ------------------------"; val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus}); if contains_rule r1 Test_simplify then () else error "rewtools.sml contains_rule Thm"; @@ -531,3 +590,4 @@ val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_"); if not (contains_rule r1 Test_simplify) then () else error "rewtools.sml contains_rule Calc"; +===== inhibit exn ?===========================================================*) diff -r 356e0272d565 -r 549ae735517e test/Tools/isac/Knowledge/isac.sml --- a/test/Tools/isac/Knowledge/isac.sml Mon Oct 11 14:22:50 2010 +0200 +++ b/test/Tools/isac/Knowledge/isac.sml Thu Oct 28 09:24:47 2010 +0200 @@ -11,6 +11,7 @@ "table of contents --------------------------------------"; "--------------------------------------------------------"; "-------- fill ! theory' with data ----------------------"; +"-------- val rlsthmsNOTisac ----------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; "--------------------------------------------------------"; @@ -19,7 +20,7 @@ "-------- fill ! theory' with data ----------------------"; "-------- fill ! theory' with data ----------------------"; "-------- fill ! theory' with data ----------------------"; - val allthys = theory "Isac"(**@{theory}*) :: + val allthys = theory "Isac" (*@{theory}*) :: Theory.ancestors_of (*@{theory}*) (theory "Isac"); val isabthys = Theory.ancestors_of first_isac_thy; val isacthys = subtract Theory.eq_thy isabthys allthys; @@ -34,8 +35,37 @@ "Language", "Script", "Tools", "ListC"] then () else error "isac.sml: names of isac theories changed"; "--------------------------------------------------------"; - val _ = theory' := (map Context.theory_name isacthys) ~~ isacthys; +(* val _ = theory' :=*) (map Context.theory_name isacthys) ~~ isacthys; -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) +"-------- val rlsthmsNOTisac ----------------------------"; +"-------- val rlsthmsNOTisac ----------------------------"; +"-------- val rlsthmsNOTisac ----------------------------"; + val isacthms = (flat o (map Theory.axioms_of)) isacthys + : (thmID * term) list; +if length isacthms > 300 then () else error "isac.sml some isacthms dropped"; +"--------------------------------------------------------"; +val all_ListC_thms = PureThy.all_thms_of (theory "ListC"); +val all_Complex_Main_thms = PureThy.all_thms_of (theory "Complex_Main"); +(* delivers [] after 100 secs ... +subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms); +... because ListC contains no thms, but axioms only.*) +"----- so we cannot get isacthms as thm, only as term ---"; + +"----- but we can retain isacrlsthms as thm ---"; + val isacrlsthms = ((*(map (apsnd prop_of)) o*) + (gen_distinct eq_thmI) o (map rep_thm_G') o flat o + (map (thms_of_rls o #2 o #2))) (! ruleset'); +val thm = @{thm radd_0}; +val dn = Thm.derivation_name thm (*= "Test.radd_0"*); +(* +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn); +fun thyID_of_derivation_name dn = hd (space_explode "." dn); +*) +val thmID = thmID_of_derivation_name dn; +val thyID = thyID_of_derivation_name dn; +(* +fun eq_thmI' ((thmid1, _), (thmid2, _)) = + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2); +*) + val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); diff -r 356e0272d565 -r 549ae735517e test/Tools/isac/calcelems.sml --- a/test/Tools/isac/calcelems.sml Mon Oct 11 14:22:50 2010 +0200 +++ b/test/Tools/isac/calcelems.sml Thu Oct 28 09:24:47 2010 +0200 @@ -1,7 +1,33 @@ (* tests for sml/calcelems.sml author: Walther Neuper 060113 - (c) isac-team 2006 +*) -use"../smltest/calcelems.sml"; -use"calcelems.sml"; -*) +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"-------- fun thmID_of_derivation_name ----------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; + +"-------- fun thmID_of_derivation_name ----------------"; +"-------- fun thmID_of_derivation_name ----------------"; +"-------- fun thmID_of_derivation_name ----------------"; +val thm = @{thm radd_0}; +val dn = Thm.derivation_name thm; +if dn = "Test.radd_0" then () +else error "calcelems.sml Thm.derivation_name changed 1"; + +val thmID = thmID_of_derivation_name dn; +val thyID = thyID_of_derivation_name dn; +if thmID = "radd_0" andalso thyID = "Test" then () +else error "calcelems.sml Thm.derivation_name changed 2"; + +"--- thm2 --"; +val thm = @{thm add_divide_distrib} +val dn = Thm.derivation_name thm; +val thmID = thmID_of_derivation_name dn; +val thyID = thyID_of_derivation_name dn; +if thmID = "add_divide_distrib" andalso thyID = "Rings" then () +else error "calcelems.sml Thm.derivation_name changed 3";