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.
1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Oct 11 14:22:50 2010 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Thu Oct 28 09:24:47 2010 +0200
1.3 @@ -351,13 +351,13 @@
1.4
1.5 (**.set up isab_thm_thy in Isac.ML.**)
1.6
1.7 -fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, thm));
1.8 -fun rearrange_inv (thmID, (thyID, thm)) = (thyID, (thmID, thm));
1.9 +fun rearrange (thyID, (thmID, thm)) = (thmID, (thyID, prop_of thm));
1.10 +fun rearrange_inv (thmID, (thyID, term)) = (thyID, (thmID, term));
1.11
1.12 (*.lookup the missing theorems in some thy (of Isabelle).*)
1.13 fun make_isa missthms thy =
1.14 map (pair (theory2thyID thy))
1.15 - ((inter eq_thmI) missthms (PureThy.all_thms_of thy))
1.16 + ((inter eq_thmI) missthms [] (*PureThy.all_thms_of thy*))
1.17 : (thyID * (thmID * Thm.thm)) list;
1.18
1.19 (*.separate handling of sym_thms.*)
1.20 @@ -375,14 +375,15 @@
1.21 ((apsnd o apsnd) sym_thm)) symsym_isab
1.22
1.23 val isab = notsym_isab @ symsym_isab @ sym_isab
1.24 - in ((map rearrange) o (gen_sort les)) isab
1.25 - : (thmID * (thyID * Thm.thm)) list
1.26 + in ((map rearrange) o (gen_sort les)) isab : (thmID * (thyID * term)) list
1.27 end;
1.28 +(*
1.29 (* version with term instead of thm, for Theory.axioms_of in isa02*)
1.30 fun make_isa missthms thy =
1.31 map (pair (theory2thyID thy))
1.32 ((inter eq_thmI') missthms (Theory.axioms_of thy))
1.33 : (thyID * (thmID * term)) list;
1.34 +(* separate handling of sym_thms *)
1.35 fun make_isab rlsthmsNOTisac isab_thys =
1.36 let fun les ((s1,_), (s2,_)) = (s1 : string) < s2
1.37 val notsym = filter_out (is_sym o #1) rlsthmsNOTisac
1.38 @@ -400,6 +401,7 @@
1.39 in ((map rearrange) o (gen_sort les)) isab
1.40 : (thmID * (thyID * term)) list
1.41 end;
1.42 +*)
1.43
1.44 (*.which theory below thy' contains a theorem; this can be in isabelle !
1.45 get the occurence _after_ in the _list_ (is up to asking TUM) theory'.*)
2.1 --- a/src/Tools/isac/Knowledge/Isac.thy Mon Oct 11 14:22:50 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Thu Oct 28 09:24:47 2010 +0200
2.3 @@ -26,9 +26,8 @@
2.4 val isabthys = Theory.ancestors_of first_isac_thy;
2.5 val isacthys = subtract Theory.eq_thy isabthys allthys;
2.6
2.7 - val isacrlsthms = ((map (apsnd prop_of)) o
2.8 - (gen_distinct eq_thmI) o (map rep_thm_G') o flat o
2.9 - (map (thms_of_rls o #2 o #2))) (!ruleset');
2.10 + val isacrlsthms = ((gen_distinct eq_thmI) o (map rep_thm_G') o flat o
2.11 + (map (thms_of_rls o #2 o #2))) (! ruleset');
2.12 val isacthms =
2.13 (flat o (map Theory.axioms_of)) isacthys : (thmID * term) list;
2.14 (*in*)
3.1 --- a/src/Tools/isac/Test_Isac.thy Mon Oct 11 14:22:50 2010 +0200
3.2 +++ b/src/Tools/isac/Test_Isac.thy Thu Oct 28 09:24:47 2010 +0200
3.3 @@ -31,11 +31,12 @@
3.4 cd "../..";
3.5 *)
3.6 ML{* writeln "**** run systests complete ******************************" *};
3.7 +
3.8 +use"../../../test/Tools/isac/calcelems.sml"; (*complete*)
3.9 +
3.10 (*
3.11 cd"smltest/Scripts";
3.12 *)
3.13 -
3.14 -
3.15 use"../../../test/Tools/isac/ProgLang/termC.sml"; (*part.*)
3.16
3.17
3.18 @@ -53,8 +54,9 @@
3.19 *)
3.20 use "../../../test/Tools/isac/Interpret/ptyps.sml"; (*TODO*)
3.21 use "../../../test/Tools/isac/Interpret/calchead.sml";
3.22 +ML {*print_depth 999*}
3.23 +use "../../../test/Tools/isac/Interpret/rewtools.sml"; (**)
3.24 (*
3.25 - use"rewtools.sml";
3.26 use"solve.sml"; (*detailrls can notyet ackn. 'Rewrite_Set "cancel"' *);
3.27 use"inform.sml";
3.28 use"me.sml";
3.29 @@ -63,10 +65,9 @@
3.30 cd"smltest/xmlsrc";
3.31 use"datatypes.sml";
3.32 use"pbl-met-hierarchy.sml";
3.33 - use"thy-hierarchy.sml";
3.34 - cd "../..";
3.35 -cd"smltest/FE-interface";
3.36 +use"../../../test/Tools/isac/xmlsrc/thy-hierarchy.sml"; (**)
3.37 *)
3.38 +
3.39 use"../../../test/Tools/isac/Frontend/interface.sml"; (**)
3.40 (*
3.41 cd "../..";
3.42 @@ -107,8 +108,12 @@
3.43 use"biegelinie.sml";
3.44 use"algein.sml";
3.45 *)
3.46 -ML {*print_depth 999*}
3.47 +ML {*
3.48 +val thm = @{thm refl};
3.49 +prop_of thm;
3.50 +*}
3.51 use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)
3.52 +ML {*print_depth 3*}
3.53
3.54 ML {*111*}
3.55
3.56 @@ -122,7 +127,9 @@
3.57 *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
3.58
3.59 use_thy "../../Tools/isac/ADDTESTS/trace-rewrite/Build_Test"
3.60 -*)
3.61 +*)use "../../../test/Pure/library.sml" (**)
3.62 +use_thy "../../../test/Pure/General/Basics"
3.63 +
3.64 use_thy "../../../test/Pure/Isar/Test_Parse_Term"
3.65 use_thy "../../../test/Pure/Isar/Test_Parsers"
3.66
4.1 --- a/src/Tools/isac/calcelems.sml Mon Oct 11 14:22:50 2010 +0200
4.2 +++ b/src/Tools/isac/calcelems.sml Thu Oct 28 09:24:47 2010 +0200
4.3 @@ -7,7 +7,10 @@
4.4 (c) isac-team 2003
4.5 *)
4.6
4.7 -
4.8 +(*
4.9 +structure CalcElems =
4.10 +struct
4.11 +*)
4.12 val linefeed = (curry op^) "\n";
4.13 type authors = string list;
4.14
4.15 @@ -146,11 +149,15 @@
4.16 fun thm_of_thm (Thm (_, thm)) = thm
4.17 | thm_of_thm _ = error "thm_of_thm";
4.18 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);
4.19 +
4.20 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
4.21 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
4.22 +
4.23 fun eq_thmI ((thmid1 : thmID, _ : thm), (thmid2 : thmID, _ : thm)) =
4.24 (strip_thy thmid1) = (strip_thy thmid2);
4.25 (*version typed weaker WN100910*)
4.26 fun eq_thmI' ((thmid1, _), (thmid2, _)) =
4.27 - (strip_thy thmid1) = (strip_thy thmid2);
4.28 + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
4.29
4.30
4.31 val string_of_thm = Thm.get_name_hint; (*FIXME.2009*)
4.32 @@ -355,6 +362,7 @@
4.33 -> (term * term) (*(t1, t2) to be compared *)
4.34 -> bool)) (*if t1 <= t2 then true else false *)
4.35 list); (*association list *)
4.36 +
4.37 rew_ord' := overwritel (!rew_ord', [("e_rew_ord", e_rew_ord),
4.38 ("dummy_ord", dummy_ord)]);
4.39
4.40 @@ -406,9 +414,11 @@
4.41 val e_thydata = Html {guh="e_guh", coursedesign=[], mathauthors=[], html=""};
4.42
4.43 type thehier = (thydata ptyp) list;
4.44 -val thehier = Unsynchronized.ref ([] : thehier);
4.45 +val thehier = Unsynchronized.ref ([] : thehier); (*WN101011 make argument, del*)
4.46
4.47 -(*.an association list, gets the value once in Isac.ML.*)
4.48 +(* an association list, gets the value once in Isac.ML.
4.49 + stores Isabelle's thms as terms for compatibility with Theory.axioms_of.
4.50 + WN1-1-28 make this data arguments and del ref ?*)
4.51 val isab_thm_thy = Unsynchronized.ref ([] : (thmID * (thyID * term)) list);
4.52
4.53
4.54 @@ -668,3 +678,6 @@
4.55 | ldr2str D = "D";
4.56 fun loc_2str (k:loc_) = (strs2str' o (map ldr2str)) k;
4.57
4.58 +(*
4.59 +end (*struct*)
4.60 +*)
5.1 --- a/test/Pure/General/Basics.thy Mon Oct 11 14:22:50 2010 +0200
5.2 +++ b/test/Pure/General/Basics.thy Thu Oct 28 09:24:47 2010 +0200
5.3 @@ -1,8 +1,5 @@
5.4 (* Title: ~~~/isac/smltest/Pure/General/Basics.thy
5.5 - Author: Walther Neuper, TU Graz
5.6 -
5.7 -$ cd /usr/local/Isabelle2009-1/src/Pure/isac/smltest/Pure/General
5.8 -$ /usr/local/isabisac/bin/isabelle emacs Scan.thy &
5.9 + Author: Walther Neuper, TU Graz, 101027
5.10 *)
5.11
5.12 header {* testing combinators from src/Pure/General/basics
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/test/Pure/library.sml Thu Oct 28 09:24:47 2010 +0200
6.3 @@ -0,0 +1,23 @@
6.4 +(* Title: trials on library.ML
6.5 + Author: Walther Neuper, TU Graz, 101027
6.6 +*)
6.7 +
6.8 +"--------------------------------------------------------";
6.9 +"--------------------------------------------------------";
6.10 +"table of contents --------------------------------------";
6.11 +"--------------------------------------------------------";
6.12 +"----------- fun foldl_map ------------------------------";
6.13 +"--------------------------------------------------------";
6.14 +"--------------------------------------------------------";
6.15 +
6.16 +
6.17 +"----------- fun foldl_map ------------------------------";
6.18 +"----------- fun foldl_map ------------------------------";
6.19 +"----------- fun foldl_map ------------------------------";
6.20 +fun arg1 (a, b) = (a, b + 10);
6.21 +val arg2 = [("a1", 1), ("a2", 2), ("a3", 3)];
6.22 +(*========== inhibit exn =======================================================
6.23 +foldl_map arg1 arg2; (*why is this not known here, but the others below ?*)
6.24 +============ inhibit exn =====================================================*)
6.25 +random;
6.26 +last_elem;
7.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Oct 11 14:22:50 2010 +0200
7.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Oct 28 09:24:47 2010 +0200
7.3 @@ -1,51 +1,107 @@
7.4 (* test for sml/ME/rewtools.sml
7.5 authors: Walther Neuper 2000, 2006
7.6 - (c) due to copyright terms
7.7 -
7.8 -use"../smltest/ME/rewtools.sml";
7.9 -use"rewtools.sml";
7.10 *)
7.11
7.12 -"-----------------------------------------------------------------";
7.13 -"table of contents -----------------------------------------------";
7.14 -"-----------------------------------------------------------------";
7.15 -"----------- fun collect_isab_thys -------------------------------";
7.16 -"----------- fun thy_containing_thm ------------------------------";
7.17 -"----------- fun thy_containing_rls ------------------------------";
7.18 -"----------- fun thy_containing_cal ------------------------------";
7.19 -"----------- initContext Thy_ Integration-demo -------------------";
7.20 -"----------- initContext..Thy_, fun context_thm ------------------";
7.21 -"----------- initContext..Thy_, fun context_rls ------------------";
7.22 -"----------- checkContext..Thy_, fun context_thy -----------------";
7.23 -"----------- checkContext..Thy_, fun context_rls -----------------";
7.24 -"----------- checkContext..Thy_ on last formula ------------------";
7.25 -"----------- fun guh2theID ---------------------------------------";
7.26 -"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
7.27 -"-----------------------------------------------------------------";
7.28 -"----------- fun string_of_thmI for_[.]_) ------------------------";
7.29 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.30 -"-----------------------------------------------------------------";
7.31 -"----------- fun filter_appl_rews --------------------------------";
7.32 -"----------- fun is_contained_in ---------------------------------";
7.33 -"-----------------------------------------------------------------";
7.34 -"-----------------------------------------------------------------";
7.35 +"--------------------------------------------------------";
7.36 +"--------------------------------------------------------";
7.37 +"table of contents --------------------------------------";
7.38 +"--------------------------------------------------------";
7.39 +"----------- fun make_isa -------------------------------";
7.40 +"----------- fun collect_isab_thys ----------------------";
7.41 +"----------- fun thy_containing_thm ---------------------";
7.42 +"----------- fun thy_containing_rls ---------------------";
7.43 +"----------- fun thy_containing_cal ---------------------";
7.44 +"----------- initContext Thy_ Integration-demo ----------";
7.45 +"----------- initContext..Thy_, fun context_thm ---------";
7.46 +"----------- initContext..Thy_, fun context_rls ---------";
7.47 +"----------- checkContext..Thy_, fun context_thy --------";
7.48 +"----------- checkContext..Thy_, fun context_rls --------";
7.49 +"----------- checkContext..Thy_ on last formula ---------";
7.50 +"----------- fun guh2theID ------------------------------";
7.51 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
7.52 +"--------------------------------------------------------";
7.53 +"----------- fun string_of_thmI for_[.]_) ---------------";
7.54 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
7.55 +"--------------------------------------------------------";
7.56 +"----------- fun filter_appl_rews -----------------------";
7.57 +"----------- fun is_contained_in ------------------------";
7.58 +"--------------------------------------------------------";
7.59 +"--------------------------------------------------------";
7.60
7.61
7.62 +"----------- fun make_isa -------------------------------";
7.63 +"----------- fun make_isa -------------------------------";
7.64 +"----------- fun make_isa -------------------------------";
7.65 +map #1 (rlsthmsNOTisac : (string * term) list) = (*WN101011, Isabelle2009-2*)
7.66 +["refl", "o_apply", "del_base", "del_rec", "LENGTH_CONS", "LENGTH_NIL",
7.67 + "list_diff_def", "take_Nil", "take_Cons", "if_True", "if_False",
7.68 + "sym_real_mult_minus1", "left_distrib", "right_distrib",
7.69 + "sym_realpow_twoI", "sym_realpow_addI", "mult_1_right",
7.70 + "sym_real_mult_2", "mult_1_left", "mult_zero_left", "mult_zero_right",
7.71 + "add_0_left", "add_0_right", "divide_zero_left", "sym_real_mult_assoc",
7.72 + "real_le_refl", "minus_minus", "real_mult_commute", "real_mult_assoc",
7.73 + "add_commute", "add_left_commute", "add_assoc", "minus_mult_left",
7.74 + "right_minus", "sym_add_assoc", "left_diff_distrib",
7.75 + "right_diff_distrib", "minus_divide_left", "times_divide_eq_right",
7.76 + "times_divide_eq_left", "divide_divide_eq_left",
7.77 + "divide_divide_eq_right", "divide_1", "add_divide_distrib",
7.78 + "sym_rmult_assoc"];
7.79 +if length rlsthmsNOTisac > 40 then ()
7.80 +else error "rewtools.sml: some rlsthmsNOTisac dropped";
7.81
7.82 -"----------- fun collect_isab_thys -------------------------------";
7.83 -"----------- fun collect_isab_thys -------------------------------";
7.84 -"----------- fun collect_isab_thys -------------------------------";
7.85 -val thy = first_isac_thy (*def. in Script/ListG.ML*);
7.86 -val {ancestors,...} = rep_theory thy;
7.87 -print_depth 99; map string_of_thy ancestors; print_depth 3;
7.88 -length ancestors;
7.89 -val ancestors = (#ancestors o rep_theory) first_isac_thy;
7.90 -length ancestors;
7.91 -print_depth 99; map theory2theory' ancestors; print_depth 3;
7.92 -val isabthms = (flat o (map PureThy.all_thms_of)) ancestors;
7.93 -length isabthms;
7.94 +"----- find the respectiv";
7.95
7.96 -val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (!ruleset');
7.97 +
7.98 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
7.99 +val thys = ["thy1","thy2","thy3","thy4","thy5"];
7.100 +val thms = [("thm1", 1),("thm2", 21),"thm3","thm4","thm5"];
7.101 +
7.102 +
7.103 +val (missthms, thy) = (rlsthmsNOTisac, theory "Rings");
7.104 +"--- step into make_isa --";
7.105 +map (strip_thy o #1) (Theory.axioms_of thy);
7.106 +map (strip_thy o #1) (Theory.all_axioms_of thy);
7.107 +
7.108 +inter (op =) (map #1 rlsthmsNOTisac)
7.109 + (map (strip_thy o #1) (Theory.axioms_of thy));
7.110 +"--------------------------------------------------------";
7.111 +
7.112 +map (strip_thy o #1) (Theory.axioms_of (theory "ListC"));
7.113 +map (strip_thy o #1) (Theory.all_axioms_of (theory "ListC"));
7.114 +"--------------------------------------------------------";
7.115 +
7.116 +PureThy.get_thms thy "divide_zero_left";
7.117 +
7.118 +"--------------------------------------------------------";
7.119 +map (strip_thy o #1) (PureThy.all_thms_of (theory "Groebner_Basis"));
7.120 +"--------------------------------------------------------";
7.121 +Theory.ancestors_of (theory "Groebner_Basis");
7.122 +"====================";
7.123 +"----- this thm has the current theory as thy_ref ---";
7.124 +rep_thm @{thm "divide_zero_left"};
7.125 +"--------------------------------------------------------";
7.126 +"----- this thm has 'Rings' as thy_ref ---";
7.127 +rep_thm (hd (PureThy.get_thms (theory "Rings") "divide_zero_left"));
7.128 +"--------------------------------------------------------";
7.129 +#thy_ref (rep_thm (hd (PureThy.get_thms (theory "Rings") "divide_zero_left")));
7.130 +"--------------------------------------------------------";
7.131 +theory_of_thm (hd (PureThy.get_thms (theory "Rings") "divide_zero_left"));
7.132 +
7.133 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
7.134 +
7.135 +1111111;
7.136 +
7.137 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
7.138 +GOON: isabelle-dev: Theory.thms_of ???
7.139 +
7.140 +
7.141 +"----------- fun collect_isab_thys ----------------------";
7.142 +"----------- fun collect_isab_thys ----------------------";
7.143 +"----------- fun collect_isab_thys ----------------------";
7.144 +val ancestors = Theory.ancestors_of (theory "Complex_Main");
7.145 +val isabthms = (flat o (map Theory.axioms_of)) ancestors;
7.146 +
7.147 +val isacrules = (flat o (map (thms_of_rls o #2 o #2))) (! ruleset');
7.148 (*thms from rulesets*)
7.149 val isacrlsthms = ((map rep_thm_G') o flat o
7.150 (map (PureThy.all_thms_of_rls o #2 o #2))) (!ruleset');
7.151 @@ -96,10 +152,12 @@
7.152 print_depth 99; isab_thm_thy; print_depth 3;
7.153 *)
7.154
7.155 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
7.156
7.157 -"----------- fun thy_containing_thm ------------------------------";
7.158 -"----------- fun thy_containing_thm ------------------------------";
7.159 -"----------- fun thy_containing_thm ------------------------------";
7.160 +(*=== inhibit exn ?=============================================================
7.161 +"----------- fun thy_containing_thm ---------------------";
7.162 +"----------- fun thy_containing_thm ---------------------";
7.163 +"----------- fun thy_containing_thm ---------------------";
7.164 val (str, (thy', thy)) = ("real_diff_minus",("Root", Root.thy));
7.165 if thy_contains_thm str ("XXX",thy) then ()
7.166 else error "rewtools.sml: NOT thy_contains_thm \
7.167 @@ -136,9 +194,9 @@
7.168 \thy_containing_thm Test radd_commute";
7.169
7.170
7.171 -"----------- fun thy_containing_rls ------------------------------";
7.172 -"----------- fun thy_containing_rls ------------------------------";
7.173 -"----------- fun thy_containing_rls ------------------------------";
7.174 +"----------- fun thy_containing_rls ---------------------";
7.175 +"----------- fun thy_containing_rls ---------------------";
7.176 +"----------- fun thy_containing_rls ---------------------";
7.177 val thy' = "Biegelinie";
7.178 val dropthys = takewhile [] (not o (curry op= thy') o
7.179 (#1:theory' * theory -> theory'))
7.180 @@ -149,7 +207,10 @@
7.181 dropthys;
7.182 print_depth 99; dropthy's; print_depth 3;
7.183
7.184 -(*WN100819========================================================
7.185 +(*WN100819=======================================================
7.186 +WN100819 THIS DATE MUST BE WRONG: at this date changeset 37934:56f10b13005e
7.187 +finished update ME/calchead.sml + pushed updates over all sml+test
7.188 +
7.189 "Isac" mem dropthy's;
7.190 op mem ("Isac", dropthy's);
7.191 (op mem) o swap;
7.192 @@ -173,9 +234,9 @@
7.193 else error "rewtools.sml: diff.behav. in thy_containing_rls 3";
7.194
7.195
7.196 -"----------- fun thy_containing_cal ------------------------------";
7.197 -"----------- fun thy_containing_cal ------------------------------";
7.198 -"----------- fun thy_containing_cal ------------------------------";
7.199 +"----------- fun thy_containing_cal ---------------------";
7.200 +"----------- fun thy_containing_cal ---------------------";
7.201 +"----------- fun thy_containing_cal ---------------------";
7.202 val thy' = "Atools";
7.203 val dropthys = takewhile [] (not o (curry op= thy') o
7.204 (#1:theory' * theory -> theory'))
7.205 @@ -189,11 +250,11 @@
7.206 map (#1 : calc -> string) (rev (!calclist'));
7.207 val startsearch = filter_out ((curry ((op mem) o swap) dropthy's) o
7.208 (#1 : calc -> string)) (rev (!calclist'));
7.209 -========================================================WN100819*)
7.210 +WN100819 =====================================================*)
7.211
7.212 -"----------- initContext Thy_ Integration-demo -------------------";
7.213 -"----------- initContext Thy_ Integration-demo -------------------";
7.214 -"----------- initContext Thy_ Integration-demo -------------------";
7.215 +"----------- initContext Thy_ Integration-demo ----------";
7.216 +"----------- initContext Thy_ Integration-demo ----------";
7.217 +"----------- initContext Thy_ Integration-demo ----------";
7.218 states:=[];
7.219 CalcTree
7.220 [(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
7.221 @@ -212,9 +273,9 @@
7.222 initContext 1 Thy_ ([1,1,1], Frm);
7.223 --------------------TODO.new_c: cvs before 071227, 11:50*)
7.224
7.225 -"----------- initContext..Thy_, fun context_thm ------------------";
7.226 -"----------- initContext..Thy_, fun context_thm ------------------";
7.227 -"----------- initContext..Thy_, fun context_thm ------------------";
7.228 +"----------- initContext..Thy_, fun context_thm ---------";
7.229 +"----------- initContext..Thy_, fun context_thm ---------";
7.230 +"----------- initContext..Thy_, fun context_thm ---------";
7.231 states:=[];
7.232 CalcTree (*start of calculation, return No.1*)
7.233 [(["equality (x+1=2)", "solveFor x","solutions L"],
7.234 @@ -258,9 +319,9 @@
7.235 --- in initContext..Thy_ ---*)
7.236
7.237
7.238 -"----------- initContext..Thy_, fun context_rls ------------------";
7.239 -"----------- initContext..Thy_, fun context_rls ------------------";
7.240 -"----------- initContext..Thy_, fun context_rls ------------------";
7.241 +"----------- initContext..Thy_, fun context_rls ---------";
7.242 +"----------- initContext..Thy_, fun context_rls ---------";
7.243 +"----------- initContext..Thy_, fun context_rls ---------";
7.244 (*using pt from above*)
7.245 val p = ([1], Res);
7.246 val tac = Rewrite_Set "Test_simplify";
7.247 @@ -283,10 +344,9 @@
7.248 else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
7.249
7.250
7.251 -
7.252 -"----------- checkContext..Thy_, fun context_thy -----------------";
7.253 -"----------- checkContext..Thy_, fun context_thy -----------------";
7.254 -"----------- checkContext..Thy_, fun context_thy -----------------";
7.255 +"----------- checkContext..Thy_, fun context_thy --------";
7.256 +"----------- checkContext..Thy_, fun context_thy --------";
7.257 +"----------- checkContext..Thy_, fun context_thy --------";
7.258 (*using pt from above*)
7.259
7.260 val p = ([2,4], Res);
7.261 @@ -318,9 +378,9 @@
7.262 --- in checkContext..Thy_ ---*)
7.263
7.264
7.265 -"----------- checkContext..Thy_, fun context_rls -----------------";
7.266 -"----------- checkContext..Thy_, fun context_rls -----------------";
7.267 -"----------- checkContext..Thy_, fun context_rls -----------------";
7.268 +"----------- checkContext..Thy_, fun context_rls --------";
7.269 +"----------- checkContext..Thy_, fun context_rls --------";
7.270 +"----------- checkContext..Thy_, fun context_rls --------";
7.271 (*using pt from above*)
7.272 show_pt pt;
7.273
7.274 @@ -343,9 +403,9 @@
7.275 else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
7.276
7.277
7.278 -"----------- checkContext..Thy_ on last formula ------------------";
7.279 -"----------- checkContext..Thy_ on last formula ------------------";
7.280 -"----------- checkContext..Thy_ on last formula ------------------";
7.281 +"----------- checkContext..Thy_ on last formula ---------";
7.282 +"----------- checkContext..Thy_ on last formula ---------";
7.283 +"----------- checkContext..Thy_ on last formula ---------";
7.284 states:=[];
7.285 CalcTree (*start of calculation, return No.1*)
7.286 [(["equality (x+1=2)", "solveFor x","solutions L"],
7.287 @@ -366,10 +426,9 @@
7.288 checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
7.289
7.290
7.291 -
7.292 -"----------- fun guh2theID ---------------------------------------";
7.293 -"----------- fun guh2theID ---------------------------------------";
7.294 -"----------- fun guh2theID ---------------------------------------";
7.295 +"----------- fun guh2theID ------------------------------";
7.296 +"----------- fun guh2theID ------------------------------";
7.297 +"----------- fun guh2theID ------------------------------";
7.298 val guh = "thy_scri_ListG-thm-zip_Nil";
7.299
7.300 take_fromto 1 4 (explode guh);
7.301 @@ -390,10 +449,10 @@
7.302 else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
7.303
7.304
7.305 -"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
7.306 -"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
7.307 -"----------- debugging on Tests/solve_linear_as_rootpbl ----------";
7.308 -"----- initContext -----";
7.309 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
7.310 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
7.311 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
7.312 +----- initContext -----";
7.313 states:=[];
7.314 CalcTree
7.315 [(["equality (1+-1*2+x=0)", "solveFor x", "solutions L"],
7.316 @@ -436,9 +495,9 @@
7.317 checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
7.318
7.319
7.320 -"----------- fun string_of_thmI for_[.]_) ------------------------";
7.321 -"----------- fun string_of_thmI for_[.]_) ------------------------";
7.322 -"----------- fun string_of_thmI for_[.]_) ------------------------";
7.323 +"----------- fun string_of_thmI for_[.]_) ---------------";
7.324 +"----------- fun string_of_thmI for_[.]_) ---------------";
7.325 +"----------- fun string_of_thmI for_[.]_) ---------------";
7.326 "----- these work ?!?";
7.327 val th = sym_thm real_minus_eq_cancel;
7.328 val Th = sym_Thm (Thm ("real_minus_eq_cancel", real_minus_eq_cancel));
7.329 @@ -477,9 +536,9 @@
7.330 " = " ^ string_of_thmI thm);
7.331
7.332
7.333 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.334 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.335 -"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[.]_)-----";
7.336 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
7.337 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
7.338 +"----------- (sym_real_minus_eq_cancel, (?b1 = ?a1) ..._[";
7.339 states:=[];
7.340 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
7.341 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
7.342 @@ -500,9 +559,9 @@
7.343
7.344 getTactic 1 ([1],Frm);
7.345
7.346 -"----------- fun filter_appl_rews --------------------------------";
7.347 -"----------- fun filter_appl_rews --------------------------------";
7.348 -"----------- fun filter_appl_rews --------------------------------";
7.349 +"----------- fun filter_appl_rews -----------------------";
7.350 +"----------- fun filter_appl_rews -----------------------";
7.351 +"----------- fun filter_appl_rews -----------------------";
7.352 val f = str2term "a + z + 2*a + 3*z + 5 + 6";
7.353 val thy = assoc_thy "Isac";
7.354 val subst = [(*TODO.WN071231 test Rewrite_Inst*)];
7.355 @@ -517,9 +576,9 @@
7.356 else error "rewtools.sml filter_appl_rews a + z + 2*a + 3*z + 5 + 6";
7.357
7.358
7.359 -"----------- fun is_contained_in ---------------------------------";
7.360 -"----------- fun is_contained_in ---------------------------------";
7.361 -"----------- fun is_contained_in ---------------------------------";
7.362 +"----------- fun is_contained_in ------------------------";
7.363 +"----------- fun is_contained_in ------------------------";
7.364 +"----------- fun is_contained_in ------------------------";
7.365 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});
7.366 if contains_rule r1 Test_simplify then ()
7.367 else error "rewtools.sml contains_rule Thm";
7.368 @@ -531,3 +590,4 @@
7.369 val r1 = Calc ("Groups.minus_class.minus", eval_binop "#add_");
7.370 if not (contains_rule r1 Test_simplify) then ()
7.371 else error "rewtools.sml contains_rule Calc";
7.372 +===== inhibit exn ?===========================================================*)
8.1 --- a/test/Tools/isac/Knowledge/isac.sml Mon Oct 11 14:22:50 2010 +0200
8.2 +++ b/test/Tools/isac/Knowledge/isac.sml Thu Oct 28 09:24:47 2010 +0200
8.3 @@ -11,6 +11,7 @@
8.4 "table of contents --------------------------------------";
8.5 "--------------------------------------------------------";
8.6 "-------- fill ! theory' with data ----------------------";
8.7 +"-------- val rlsthmsNOTisac ----------------------------";
8.8 "--------------------------------------------------------";
8.9 "--------------------------------------------------------";
8.10 "--------------------------------------------------------";
8.11 @@ -19,7 +20,7 @@
8.12 "-------- fill ! theory' with data ----------------------";
8.13 "-------- fill ! theory' with data ----------------------";
8.14 "-------- fill ! theory' with data ----------------------";
8.15 - val allthys = theory "Isac"(**@{theory}*) ::
8.16 + val allthys = theory "Isac" (*@{theory}*) ::
8.17 Theory.ancestors_of (*@{theory}*) (theory "Isac");
8.18 val isabthys = Theory.ancestors_of first_isac_thy;
8.19 val isacthys = subtract Theory.eq_thy isabthys allthys;
8.20 @@ -34,8 +35,37 @@
8.21 "Language", "Script", "Tools", "ListC"] then ()
8.22 else error "isac.sml: names of isac theories changed";
8.23 "--------------------------------------------------------";
8.24 - val _ = theory' := (map Context.theory_name isacthys) ~~ isacthys;
8.25 +(* val _ = theory' :=*) (map Context.theory_name isacthys) ~~ isacthys;
8.26
8.27
8.28 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
8.29 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
8.30 +"-------- val rlsthmsNOTisac ----------------------------";
8.31 +"-------- val rlsthmsNOTisac ----------------------------";
8.32 +"-------- val rlsthmsNOTisac ----------------------------";
8.33 + val isacthms = (flat o (map Theory.axioms_of)) isacthys
8.34 + : (thmID * term) list;
8.35 +if length isacthms > 300 then () else error "isac.sml some isacthms dropped";
8.36 +"--------------------------------------------------------";
8.37 +val all_ListC_thms = PureThy.all_thms_of (theory "ListC");
8.38 +val all_Complex_Main_thms = PureThy.all_thms_of (theory "Complex_Main");
8.39 +(* delivers [] after 100 secs ...
8.40 +subtract Thm.eq_thm (map #2 all_ListC_thms) (map #2 all_Complex_Main_thms);
8.41 +... because ListC contains no thms, but axioms only.*)
8.42 +"----- so we cannot get isacthms as thm, only as term ---";
8.43 +
8.44 +"----- but we can retain isacrlsthms as thm ---";
8.45 + val isacrlsthms = ((*(map (apsnd prop_of)) o*)
8.46 + (gen_distinct eq_thmI) o (map rep_thm_G') o flat o
8.47 + (map (thms_of_rls o #2 o #2))) (! ruleset');
8.48 +val thm = @{thm radd_0};
8.49 +val dn = Thm.derivation_name thm (*= "Test.radd_0"*);
8.50 +(*
8.51 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
8.52 +fun thyID_of_derivation_name dn = hd (space_explode "." dn);
8.53 +*)
8.54 +val thmID = thmID_of_derivation_name dn;
8.55 +val thyID = thyID_of_derivation_name dn;
8.56 +(*
8.57 +fun eq_thmI' ((thmid1, _), (thmid2, _)) =
8.58 + (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
8.59 +*)
8.60 + val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
9.1 --- a/test/Tools/isac/calcelems.sml Mon Oct 11 14:22:50 2010 +0200
9.2 +++ b/test/Tools/isac/calcelems.sml Thu Oct 28 09:24:47 2010 +0200
9.3 @@ -1,7 +1,33 @@
9.4 (* tests for sml/calcelems.sml
9.5 author: Walther Neuper 060113
9.6 - (c) isac-team 2006
9.7 +*)
9.8
9.9 -use"../smltest/calcelems.sml";
9.10 -use"calcelems.sml";
9.11 -*)
9.12 +"--------------------------------------------------------";
9.13 +"--------------------------------------------------------";
9.14 +"table of contents --------------------------------------";
9.15 +"--------------------------------------------------------";
9.16 +"-------- fun thmID_of_derivation_name ----------------";
9.17 +"--------------------------------------------------------";
9.18 +"--------------------------------------------------------";
9.19 +"--------------------------------------------------------";
9.20 +
9.21 +"-------- fun thmID_of_derivation_name ----------------";
9.22 +"-------- fun thmID_of_derivation_name ----------------";
9.23 +"-------- fun thmID_of_derivation_name ----------------";
9.24 +val thm = @{thm radd_0};
9.25 +val dn = Thm.derivation_name thm;
9.26 +if dn = "Test.radd_0" then ()
9.27 +else error "calcelems.sml Thm.derivation_name changed 1";
9.28 +
9.29 +val thmID = thmID_of_derivation_name dn;
9.30 +val thyID = thyID_of_derivation_name dn;
9.31 +if thmID = "radd_0" andalso thyID = "Test" then ()
9.32 +else error "calcelems.sml Thm.derivation_name changed 2";
9.33 +
9.34 +"--- thm2 --";
9.35 +val thm = @{thm add_divide_distrib}
9.36 +val dn = Thm.derivation_name thm;
9.37 +val thmID = thmID_of_derivation_name dn;
9.38 +val thyID = thyID_of_derivation_name dn;
9.39 +if thmID = "add_divide_distrib" andalso thyID = "Rings" then ()
9.40 +else error "calcelems.sml Thm.derivation_name changed 3";