wneuper@59459
|
1 |
(* Title: build the Isac Mathengine
|
neuper@38057
|
2 |
Author: Walther Neuper, TU Graz, 100808
|
neuper@38051
|
3 |
(c) due to copyright terms
|
neuper@38051
|
4 |
|
neuper@52062
|
5 |
For creating a heap image of isac see ~~/ROOT.
|
wneuper@59344
|
6 |
For debugging see text at begin (theory dependencies!)
|
neuper@52062
|
7 |
|
neuper@52062
|
8 |
ATTENTION: no errors in this theory do not mean that there are no errors in Isac;
|
neuper@52062
|
9 |
errors are rigorously detected when creating a heap.
|
neuper@37906
|
10 |
*)
|
neuper@37906
|
11 |
|
wneuper@59347
|
12 |
theory Build_Isac
|
wneuper@59206
|
13 |
imports
|
wneuper@59182
|
14 |
(* structure inherited from migration which began with Isabelle2009. improve?
|
wneuper@59486
|
15 |
theory KEStore
|
wneuper@59486
|
16 |
ML_file "~~/src/Tools/isac/library.sml"
|
wneuper@59562
|
17 |
ML_file "~~/src/Tools/isac/ThydataC/rule.sml"
|
wneuper@59486
|
18 |
ML_file "~~/src/Tools/isac/calcelems.sml"
|
wneuper@59486
|
19 |
theory ListC
|
wneuper@59486
|
20 |
imports "~~/src/Tools/isac/KEStore"
|
wneuper@59486
|
21 |
ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
|
wneuper@59486
|
22 |
ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
|
wneuper@59486
|
23 |
ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
|
wneuper@59486
|
24 |
theory Tools imports ListC begin
|
wneuper@59486
|
25 |
theory Script imports Tools begin
|
wneuper@59486
|
26 |
theory Atools imports Descript Script
|
wneuper@59486
|
27 |
ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
|
wneuper@59486
|
28 |
theory ProgLang imports Atools
|
neuper@52062
|
29 |
*) "ProgLang/ProgLang"
|
neuper@48761
|
30 |
|
neuper@48763
|
31 |
(* use "Interpret/mstools.sml"
|
neuper@48763
|
32 |
use "Interpret/ctree.sml"
|
neuper@48763
|
33 |
use "Interpret/ptyps.sml"
|
wneuper@59106
|
34 |
use "Interpret/generate.sml"
|
neuper@48763
|
35 |
use "Interpret/calchead.sml"
|
neuper@48763
|
36 |
use "Interpret/appl.sml"
|
neuper@48763
|
37 |
use "Interpret/rewtools.sml"
|
neuper@48763
|
38 |
use "Interpret/script.sml"
|
neuper@48763
|
39 |
use "Interpret/solve.sml"
|
neuper@48763
|
40 |
use "Interpret/inform.sml"
|
neuper@48763
|
41 |
use "Interpret/mathengine.sml"
|
neuper@52062
|
42 |
*) "Interpret/Interpret"
|
neuper@48761
|
43 |
|
neuper@52062
|
44 |
(* use "xmlsrc/mathml.sml"
|
neuper@48762
|
45 |
use "xmlsrc/datatypes.sml"
|
neuper@41905
|
46 |
use "xmlsrc/pbl-met-hierarchy.sml"
|
neuper@48895
|
47 |
use "xmlsrc/thy-hierarchy.sml"
|
neuper@41905
|
48 |
use "xmlsrc/interface-xml.sml"
|
neuper@52062
|
49 |
*) "xmlsrc/xmlsrc"
|
neuper@41905
|
50 |
|
neuper@48763
|
51 |
(* use "Frontend/messages.sml"
|
neuper@41905
|
52 |
use "Frontend/states.sml"
|
neuper@41905
|
53 |
use "Frontend/interface.sml"
|
neuper@41905
|
54 |
|
neuper@41905
|
55 |
use "print_exn_G.sml"
|
neuper@52062
|
56 |
*) "Frontend/Frontend"
|
wneuper@59147
|
57 |
|
wneuper@59147
|
58 |
"Knowledge/Build_Thydata" (*imports Isac.thy etc*)
|
wneuper@59147
|
59 |
|
wneuper@59146
|
60 |
(* the Protocol for the connection isac-java -- Isabelle/Isac is built separately:
|
wneuper@59148
|
61 |
here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *)
|
wneuper@59470
|
62 |
Protocol.Protocol
|
wneuper@59469
|
63 |
|
neuper@48763
|
64 |
begin
|
neuper@48760
|
65 |
|
wneuper@59472
|
66 |
text \<open>
|
neuper@55276
|
67 |
show theory dependencies using the graph browser,
|
neuper@55276
|
68 |
open "browser_info/HOL/Isac/session.graph"
|
neuper@55276
|
69 |
and proceed from the ancestors towards the siblings.
|
wneuper@59472
|
70 |
\<close>
|
neuper@55276
|
71 |
|
wneuper@59472
|
72 |
section \<open>check presence of definitions from directories\<close>
|
neuper@48763
|
73 |
|
wneuper@59263
|
74 |
(*declare [[ML_print_depth = 999]]*)
|
wneuper@59472
|
75 |
ML \<open>
|
wneuper@59472
|
76 |
\<close> ML \<open>
|
wneuper@59472
|
77 |
\<close>
|
wneuper@59472
|
78 |
ML \<open>Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
|
wneuper@59472
|
79 |
ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
|
wneuper@59472
|
80 |
ML \<open>LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
|
wneuper@59472
|
81 |
ML \<open>Math_Engine.me; (*from "Interpret/mathengine.sml"*)\<close>
|
wneuper@59472
|
82 |
ML \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
|
wneuper@59472
|
83 |
ML \<open>print_exn_unit\<close>
|
wneuper@59472
|
84 |
ML \<open>list_rls (*from Atools.thy WN130615??? or ProgLang???*)\<close>
|
wneuper@59562
|
85 |
|
wneuper@59472
|
86 |
ML \<open>eval_occurs_in (*from Atools.thy*)\<close>
|
wneuper@59472
|
87 |
ML \<open>@{thm last_thmI} (*from Atools.thy*)\<close>
|
wneuper@59472
|
88 |
ML \<open>@{thm Querkraft_Belastung}\<close>
|
neuper@41905
|
89 |
|
wneuper@59472
|
90 |
ML \<open>Celem.check_guhs_unique := false;\<close>
|
wneuper@59472
|
91 |
ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
|
wneuper@59472
|
92 |
ML \<open>@{theory "Isac"}\<close>
|
wneuper@59472
|
93 |
ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
|
wneuper@59472
|
94 |
ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)\<close>
|
neuper@42412
|
95 |
|
wneuper@59472
|
96 |
section \<open>State of approaching Isabelle by Isac\<close>
|
wneuper@59472
|
97 |
text \<open>
|
neuper@55431
|
98 |
Mathias Lehnfeld gives the following list in his thesis in section
|
neuper@55431
|
99 |
4.2.3 Relation to Ongoing Isabelle Development.
|
wneuper@59472
|
100 |
\<close>
|
wneuper@59472
|
101 |
subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
|
wneuper@59472
|
102 |
text \<open>
|
neuper@55433
|
103 |
REPLACE BY KEStore... (has been overlooked)
|
neuper@55433
|
104 |
calcelems.sml:val rew_ord' = Unsynchronized.ref ...
|
neuper@55433
|
105 |
KEEP FOR TRACING
|
neuper@55433
|
106 |
calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
|
neuper@55433
|
107 |
calcelems.sml:val depth = Unsynchronized.ref 99999;
|
neuper@55433
|
108 |
calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
|
neuper@55433
|
109 |
calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
|
neuper@55433
|
110 |
Interpret/script.sml:val trace_script = Unsynchronized.ref false;
|
neuper@55433
|
111 |
KEEP FOR EASIER DEVELOPMENT
|
neuper@55433
|
112 |
calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
|
neuper@55433
|
113 |
KEEP FOR DEMOS
|
neuper@55433
|
114 |
Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true;
|
neuper@55433
|
115 |
Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false;
|
neuper@55433
|
116 |
Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true;
|
wneuper@59472
|
117 |
\<close>
|
wneuper@59472
|
118 |
subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
|
wneuper@59472
|
119 |
subsection \<open>(2) Make Isac’s programming language usable\<close>
|
wneuper@59472
|
120 |
subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close>
|
wneuper@59472
|
121 |
text \<open>
|
neuper@55431
|
122 |
In 2002 isac already strived for floating point numbers. Since that time
|
neuper@55431
|
123 |
isac represents numerals as "Free", see below (*1*). These experiments are
|
neuper@55431
|
124 |
unsatisfactory with respect to logical soundness.
|
neuper@55431
|
125 |
Since Isabelle now has started to care about floating point numbers, it is high
|
neuper@55431
|
126 |
time to adopt these together with the other numerals. Isabelle2012/13's numerals
|
neuper@55431
|
127 |
are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
|
neuper@55431
|
128 |
|
neuper@55431
|
129 |
The transition from "Free" to standard numerals is a task to be scheduled for
|
neuper@55431
|
130 |
several weeks. The urgency of this task follows from the experience,
|
neuper@55431
|
131 |
that (1.2) for "thehier" is very hard, because "num_str" seems to destroy
|
neuper@55431
|
132 |
some of the long identifiers of theorems which would tremendously simplify
|
neuper@55431
|
133 |
building a hierarchy of theorems according to (1.2), see (*2*) below.
|
wneuper@59472
|
134 |
\<close>
|
wneuper@59472
|
135 |
ML \<open>(*1*) Free ("123.456", HOLogic.realT)\<close>
|
neuper@55484
|
136 |
|
wneuper@59472
|
137 |
subsection \<open>(4) Improve the efficiency of Isac’s rewrite-engine\<close>
|
wneuper@59472
|
138 |
subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
|
neuper@55431
|
139 |
|
neuper@37906
|
140 |
end
|