1.1 --- a/src/Tools/isac/Build_Isac.thy Fri Jun 14 15:46:09 2013 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Jun 16 12:31:41 2013 +0200
1.3 @@ -4,9 +4,6 @@
1.4
1.5 create a new Isac heap (via ~~/ROOT.ML) with
1.6 $ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
1.7 -
1.8 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
1.9 - 10 20 30 40 50 60 70 80
1.10 *)
1.11
1.12 header {* Loading the isac mathengine *}
1.13 @@ -20,10 +17,10 @@
1.14 use "ProgLang/calculate.sml"
1.15 use "ProgLang/rewrite.sml"
1.16 "use_thy ProgLang/ListC"
1.17 - "use_thy ProgLang/Tools"
1.18 + "use_thy ProgLang/Tools"
1.19 "use_thy ProgLang/Script"
1.20 use "ProgLang/scrtools.sml"
1.21 -*) "ProgLang/ProgLang"
1.22 +*) "~~/src/Tools/isac/ProgLang/ProgLang"
1.23
1.24 (* use "Interpret/mstools.sml"
1.25 use "Interpret/ctree.sml"
1.26 @@ -36,24 +33,26 @@
1.27 use "Interpret/solve.sml"
1.28 use "Interpret/inform.sml"
1.29 use "Interpret/mathengine.sml"
1.30 -*) "Interpret/Interpret"
1.31 +*) "~~/src/Tools/isac/Interpret/Interpret"
1.32
1.33 (* use "xmlsrc/mathml.sml"
1.34 use "xmlsrc/datatypes.sml"
1.35 use "xmlsrc/pbl-met-hierarchy.sml"
1.36 use "xmlsrc/thy-hierarchy.sml"
1.37 use "xmlsrc/interface-xml.sml"
1.38 -*) "xmlsrc/xmlsrc"
1.39 +*) "~~/src/Tools/isac/xmlsrc/xmlsrc"
1.40
1.41 (* use "Frontend/messages.sml"
1.42 use "Frontend/states.sml"
1.43 use "Frontend/interface.sml"
1.44
1.45 use "print_exn_G.sml"
1.46 -*) "Frontend/Frontend"
1.47 +*) "~~/src/Tools/isac/Frontend/Frontend"
1.48
1.49 -(* "Knowledge/Isac"
1.50 -*) "Knowledge/Build_Thydata"
1.51 + "~~/src/Tools/isac/Knowledge/Isac"
1.52 +(*============ inhibit exn WN130615 ==============================================
1.53 + "~~/src/Tools/isac/Knowledge/Build_Thydata"
1.54 +============ inhibit exn WN130615 ==============================================*)
1.55
1.56 begin
1.57
1.58 @@ -63,17 +62,18 @@
1.59 ML {* me; (*from "Interpret/mathengine.sml"*) *}
1.60 ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
1.61 ML {* print_exn_unit *}
1.62 -ML {* list_rls (*from Atools.thy*) *}
1.63 +ML {* list_rls (*from Atools.thy WN130615??? or ProgLang???*) *}
1.64
1.65 -(*
1.66 ML {* eval_occurs_in (*from Atools.thy*) *}
1.67 ML {* @{thm last_thmI} (*from Atools.thy*) *}
1.68 ML {*@{thm Querkraft_Belastung}*}
1.69
1.70 ML {* check_guhs_unique := false; *}
1.71 -ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
1.72 +ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
1.73 ML {* @{theory "Isac"} *}
1.74 ML {* ! isab_thm_thy *}
1.75 -*)
1.76 +(*============ inhibit exn WN130616 ===========================================
1.77 +============ inhibit exn WN130616 ===========================================*)
1.78 +(*========== inhibit exn WN130616 ===========================================*)
1.79
1.80 end
2.1 --- a/src/Tools/isac/Build_Isac_2012.thy Fri Jun 14 15:46:09 2013 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,77 +0,0 @@
2.4 -(* Title: build and test isac
2.5 - Author: Walther Neuper, TU Graz, 100808
2.6 - (c) due to copyright terms
2.7 -
2.8 -create a new Isac heap (via ~~/ROOT.ML) with
2.9 -$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
2.10 -
2.11 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
2.12 - 10 20 30 40 50 60 70 80
2.13 -*)
2.14 -
2.15 -header {* Loading the isac mathengine *}
2.16 -
2.17 -theory Build_Isac imports Complex_Main
2.18 -
2.19 -(* use "library.sml"
2.20 - use "calcelems.sml"
2.21 -
2.22 - use "ProgLang/termC.sml"
2.23 - use "ProgLang/calculate.sml"
2.24 - use "ProgLang/rewrite.sml"
2.25 - "use_thy ProgLang/ListC"
2.26 - "use_thy ProgLang/Tools"
2.27 - "use_thy ProgLang/Script"
2.28 - use "ProgLang/scrtools.sml"
2.29 - "ProgLang/ProgLang"
2.30 -
2.31 - use "Interpret/mstools.sml"
2.32 - use "Interpret/ctree.sml"
2.33 - use "Interpret/ptyps.sml"
2.34 - use "Interpret/generate.sml"
2.35 - use "Interpret/calchead.sml"
2.36 - use "Interpret/appl.sml"
2.37 - use "Interpret/rewtools.sml"
2.38 - use "Interpret/script.sml"
2.39 - use "Interpret/solve.sml"
2.40 - use "Interpret/inform.sml"
2.41 - use "Interpret/mathengine.sml"
2.42 - "Interpret/Interpret"
2.43 -
2.44 - use "xmlsrc/mathml.sml"
2.45 - use "xmlsrc/datatypes.sml"
2.46 - use "xmlsrc/pbl-met-hierarchy.sml"
2.47 - use "xmlsrc/thy-hierarchy.sml"
2.48 - use "xmlsrc/interface-xml.sml"
2.49 - "xmlsrc/xmlsrc"
2.50 -
2.51 - use "Frontend/messages.sml"
2.52 - use "Frontend/states.sml"
2.53 - use "Frontend/interface.sml"
2.54 -
2.55 - use "print_exn_G.sml"
2.56 - "Frontend/Frontend"
2.57 -
2.58 - "Knowledge/Isac"
2.59 -
2.60 - "Knowledge/Build_Thydata"
2.61 -
2.62 -begin
2.63 -
2.64 -text {*check presence of definitions from directories*}
2.65 -ML {* is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
2.66 -ML {* me; (*from "Interpret/mathengine.sml"*) *}
2.67 -ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
2.68 -ML {* print_exn_unit *}
2.69 -ML {* list_rls (*from Atools.thy*) *}
2.70 -ML {* eval_occurs_in (*from Atools.thy*) *}
2.71 -ML {* @{thm last_thmI} (*from Atools.thy*) *}
2.72 -ML {*@{thm Querkraft_Belastung}*}
2.73 -
2.74 -ML {* check_guhs_unique := false; *}
2.75 -ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
2.76 -ML {* @{theory "Isac"} *}
2.77 -ML {* ! isab_thm_thy *}
2.78 -*)
2.79 -
2.80 -end
3.1 --- a/src/Tools/isac/Frontend/Frontend.thy Fri Jun 14 15:46:09 2013 +0200
3.2 +++ b/src/Tools/isac/Frontend/Frontend.thy Sun Jun 16 12:31:41 2013 +0200
3.3 @@ -3,15 +3,17 @@
3.4 (c) due to copyright terms
3.5 *)
3.6
3.7 -theory Frontend imports "../xmlsrc/xmlsrc"
3.8 - uses ("messages.sml") ("states.sml") ("interface.sml")
3.9 - ("../print_exn_G.sml")
3.10 +theory Frontend imports
3.11 + "~~/src/Tools/isac/xmlsrc/xmlsrc"
3.12 +uses
3.13 + ("~~/src/Tools/isac/Frontend/messages.sml")
3.14 + ("~~/src/Tools/isac/Frontend/states.sml")
3.15 + ("~~/src/Tools/isac/Frontend/interface.sml")
3.16 + ("~~/src/Tools/isac/print_exn_G.sml")
3.17 begin
3.18 + use "~~/src/Tools/isac/Frontend/messages.sml"
3.19 + use "~~/src/Tools/isac/Frontend/states.sml"
3.20 + use "~~/src/Tools/isac/Frontend/interface.sml"
3.21
3.22 - use "messages.sml"
3.23 - use "states.sml"
3.24 - use "interface.sml"
3.25 -
3.26 - use "../print_exn_G.sml"
3.27 -
3.28 + use "~~/src/Tools/isac/print_exn_G.sml"
3.29 end
3.30 \ No newline at end of file
4.1 --- a/src/Tools/isac/Interpret/Interpret.thy Fri Jun 14 15:46:09 2013 +0200
4.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Sun Jun 16 12:31:41 2013 +0200
4.3 @@ -4,22 +4,29 @@
4.4 *)
4.5
4.6 theory Interpret
4.7 -imports "../ProgLang/ProgLang"
4.8 -uses ("mstools.sml") ("ctree.sml") ("ptyps.sml") ("generate.sml")
4.9 - ("calchead.sml") ("appl.sml") ("rewtools.sml") ("script.sml")
4.10 - ("solve.sml") ("inform.sml") ("mathengine.sml")
4.11 +imports "~~/src/Tools/isac/ProgLang/ProgLang"
4.12 +uses
4.13 + ("~~/src/Tools/isac/Interpret/mstools.sml")
4.14 + ("~~/src/Tools/isac/Interpret/ctree.sml")
4.15 + ("~~/src/Tools/isac/Interpret/ptyps.sml")
4.16 + ("~~/src/Tools/isac/Interpret/generate.sml")
4.17 + ("~~/src/Tools/isac/Interpret/calchead.sml")
4.18 + ("~~/src/Tools/isac/Interpret/appl.sml")
4.19 + ("~~/src/Tools/isac/Interpret/rewtools.sml")
4.20 + ("~~/src/Tools/isac/Interpret/script.sml")
4.21 + ("~~/src/Tools/isac/Interpret/solve.sml")
4.22 + ("~~/src/Tools/isac/Interpret/inform.sml")
4.23 + ("~~/src/Tools/isac/Interpret/mathengine.sml")
4.24 begin
4.25 -
4.26 - use "mstools.sml"
4.27 - use "ctree.sml"
4.28 - use "ptyps.sml"
4.29 - use "generate.sml"
4.30 - use "calchead.sml"
4.31 - use "appl.sml"
4.32 - use "rewtools.sml"
4.33 - use "script.sml"
4.34 - use "solve.sml"
4.35 - use "inform.sml"
4.36 - use "mathengine.sml"
4.37 -
4.38 + use "~~/src/Tools/isac/Interpret/mstools.sml"
4.39 + use "~~/src/Tools/isac/Interpret/ctree.sml"
4.40 + use "~~/src/Tools/isac/Interpret/ptyps.sml"
4.41 + use "~~/src/Tools/isac/Interpret/generate.sml"
4.42 + use "~~/src/Tools/isac/Interpret/calchead.sml"
4.43 + use "~~/src/Tools/isac/Interpret/appl.sml"
4.44 + use "~~/src/Tools/isac/Interpret/rewtools.sml"
4.45 + use "~~/src/Tools/isac/Interpret/script.sml"
4.46 + use "~~/src/Tools/isac/Interpret/solve.sml"
4.47 + use "~~/src/Tools/isac/Interpret/inform.sml"
4.48 + use "~~/src/Tools/isac/Interpret/mathengine.sml"
4.49 end
4.50 \ No newline at end of file
5.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Jun 14 15:46:09 2013 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Sun Jun 16 12:31:41 2013 +0200
5.3 @@ -9,7 +9,7 @@
5.4 text {* This theory collects data of theorems and axioms defined and used in ISAC *}
5.5
5.6 ML {*
5.7 -(** set up a list for getting guh + theID for a thm (defined in isabelle) **)
5.8 +(** set up a list for getting guh + theID for a thm defined in isabelle (and NOT in isac) **)
5.9
5.10 (*local*)
5.11 val first_ProgLang_thy = @{theory ListC}
5.12 @@ -41,7 +41,7 @@
5.13 progthys := progthys';
5.14 theory' := rev ((map Context.theory_name isacthys') ~~ isacthys'); (*WN120320 easy to remove*)
5.15 val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms);
5.16 -(*end;*)
5.17 +(*end;(*local*)*)
5.18 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:
5.19 see tests
5.20 --- OLD compute rlsthmsNOTisac by eq_thmID ---
5.21 @@ -109,7 +109,8 @@
5.22 including thms from Isabelle used in rls;
5.23 elements store_*d in any *.thy are not overwritten.*)
5.24
5.25 -thehier := the_hier (! thehier) (collect_thydata ());
5.26 +(*========== inhibit exn WN130616: ME_Isa: thy 'Script' not in system =======*)
5.27 +thehier := the_hier (! thehier) (collect_thydata ()); (*ME_Isa: thy 'Script' not in system*)
5.28 tracing("----------------------------------\n" ^
5.29 "*** insert: not found ... IS OK : \n" ^
5.30 "comes from fill_parents \n" ^
5.31 @@ -119,6 +120,8 @@
5.32 text {* interface for dialog-authoring *}
5.33
5.34 ML {*
5.35 +(*========== inhibit exn WN130616:
5.36 + get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"] =======
5.37 insert_errpats ["diff","differentiate_on_R"]
5.38 ([("chain-rule-diff-both",
5.39 [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
5.40 @@ -219,6 +222,8 @@
5.41
5.42 (* ...and all other related rls by hand;
5.43 TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
5.44 +========== inhibit exn WN130616:
5.45 + get_pbt not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"] =======*)
5.46 *}
5.47 -
5.48 +ML {*"test"*}
5.49 end
6.1 --- a/src/Tools/isac/Knowledge/Isac.thy Fri Jun 14 15:46:09 2013 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Sun Jun 16 12:31:41 2013 +0200
6.3 @@ -3,7 +3,7 @@
6.4 *)
6.5
6.6 theory Isac
6.7 -imports "../Frontend/Frontend"
6.8 +imports "~~/src/Tools/isac/Frontend/Frontend"
6.9 PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin (*InsSort +*)
6.10 DiophantEq Inverse_Z_Transform Test
6.11 begin
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Jun 14 15:46:09 2013 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Jun 16 12:31:41 2013 +0200
7.3 @@ -5,8 +5,8 @@
7.4
7.5 depends on Poly (and not on Atools), because
7.6 fractions with _normalized_ polynomials are canceled, added, etc.
7.7 -1234567890123456789012345678901234567890123456789012345678901234567890123456789012345678901234567890
7.8 - 10 20 30 40 50 60 70 80 90 100
7.9 +
7.10 + ATTENTION WN130616: WITH Unsynchronized.ref Rational.thy TAKES ~1MIN FOR EVALUATION
7.11 *)
7.12
7.13 theory Rational imports Poly begin
7.14 @@ -3855,5 +3855,5 @@
7.15 " t_t)"));
7.16
7.17 *}
7.18 -
7.19 +ML {*"test"*}
7.20 end (* theory*)
8.1 --- a/src/Tools/isac/Knowledge/Trig.thy Fri Jun 14 15:46:09 2013 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Trig.thy Sun Jun 16 12:31:41 2013 +0200
8.3 @@ -1,3 +1,3 @@
8.4 theory Trig imports Real begin
8.5 -
8.6 +ML {*"test"*}
8.7 end
8.8 \ No newline at end of file
9.1 --- a/src/Tools/isac/ProgLang/ListC.thy Fri Jun 14 15:46:09 2013 +0200
9.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Sun Jun 16 12:31:41 2013 +0200
9.3 @@ -4,15 +4,17 @@
9.4 *)
9.5
9.6 theory ListC imports Complex_Main
9.7 -uses ("../library.sml")
9.8 - ("../calcelems.sml")
9.9 - ("termC.sml") ("calculate.sml") ("rewrite.sml")
9.10 +uses ("~~/src/Tools/isac/library.sml")
9.11 + ("~~/src/Tools/isac/calcelems.sml")
9.12 + ("~~/src/Tools/isac/ProgLang/termC.sml")
9.13 + ("~~/src/Tools/isac/ProgLang/calculate.sml")
9.14 + ("~~/src/Tools/isac/ProgLang/rewrite.sml")
9.15 begin
9.16 -use "../library.sml"
9.17 -use "../calcelems.sml"
9.18 -use "termC.sml"
9.19 -use "calculate.sml"
9.20 -use "rewrite.sml"
9.21 +use "~~/src/Tools/isac/library.sml"
9.22 +use "~~/src/Tools/isac/calcelems.sml"
9.23 +use "~~/src/Tools/isac/ProgLang/termC.sml"
9.24 +use "~~/src/Tools/isac/ProgLang/calculate.sml"
9.25 +use "~~/src/Tools/isac/ProgLang/rewrite.sml"
9.26
9.27 text {* 'nat' in List.thy replaced by 'real' *}
9.28
10.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy Fri Jun 14 15:46:09 2013 +0200
10.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Sun Jun 16 12:31:41 2013 +0200
10.3 @@ -4,9 +4,9 @@
10.4 *)
10.5
10.6 theory ProgLang imports Script
10.7 - uses ("../ProgLang/scrtools.sml")
10.8 + uses ("~~/src/Tools/isac/ProgLang/scrtools.sml")
10.9 begin
10.10
10.11 -use "../ProgLang/scrtools.sml"
10.12 +use "~~/src/Tools/isac/ProgLang/scrtools.sml"
10.13
10.14 -end
10.15 \ No newline at end of file
10.16 +end
10.17 \ No newline at end of file
11.1 --- a/src/Tools/isac/ProgLang/Script.thy Fri Jun 14 15:46:09 2013 +0200
11.2 +++ b/src/Tools/isac/ProgLang/Script.thy Sun Jun 16 12:31:41 2013 +0200
11.3 @@ -1,8 +1,6 @@
11.4 (* Title: tactics, tacticals etc. for scripts
11.5 Author: Walther Neuper 000224
11.6 (c) due to copyright terms
11.7 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
11.8 - 10 20 30 40 50 60 70 80
11.9 *)
11.10
11.11 theory Script imports Tools begin
12.1 --- a/src/Tools/isac/calcelems.sml Fri Jun 14 15:46:09 2013 +0200
12.2 +++ b/src/Tools/isac/calcelems.sml Sun Jun 16 12:31:41 2013 +0200
12.3 @@ -286,7 +286,7 @@
12.4 > thyID2theory' "Isac" (*abuse, goes ok...*);
12.5 val it = "Isac" : theory'
12.6 *)
12.7 -Global_
12.8 +
12.9 fun theory'2thyID (theory':theory') = theory';
12.10 (*
12.11 let val ss = Symbol.explode theory'
13.1 --- a/src/Tools/isac/xmlsrc/xmlsrc.thy Fri Jun 14 15:46:09 2013 +0200
13.2 +++ b/src/Tools/isac/xmlsrc/xmlsrc.thy Sun Jun 16 12:31:41 2013 +0200
13.3 @@ -3,15 +3,20 @@
13.4 (c) due to copyright terms
13.5 *)
13.6
13.7 -theory xmlsrc imports "../Interpret/Interpret"
13.8 - uses ("mathml.sml") ("datatypes.sml") ("pbl-met-hierarchy.sml")
13.9 - ("thy-hierarchy.sml") ("interface-xml.sml")
13.10 +theory xmlsrc imports
13.11 + "~~/src/Tools/isac/Interpret/Interpret"
13.12 +uses
13.13 + ("~~/src/Tools/isac/xmlsrc/mathml.sml")
13.14 + ("~~/src/Tools/isac/xmlsrc/datatypes.sml")
13.15 + ("~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml")
13.16 + ("~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml")
13.17 + ("~~/src/Tools/isac/xmlsrc/interface-xml.sml")
13.18 begin
13.19
13.20 - use "mathml.sml"
13.21 - use "datatypes.sml"
13.22 - use "pbl-met-hierarchy.sml"
13.23 - use "thy-hierarchy.sml"
13.24 - use "interface-xml.sml"
13.25 + use "~~/src/Tools/isac/xmlsrc/mathml.sml"
13.26 + use "~~/src/Tools/isac/xmlsrc/datatypes.sml"
13.27 + use "~~/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml"
13.28 + use "~~/src/Tools/isac/xmlsrc/thy-hierarchy.sml"
13.29 + use "~~/src/Tools/isac/xmlsrc/interface-xml.sml"
13.30
13.31 end
13.32 \ No newline at end of file