walther@59632
|
1 |
(* Title: build the Isac-Kernel: MathEngine & Knowledge
|
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.
|
walther@59632
|
6 |
For debugging see text at begin below, e.g. theory dependencies:
|
walther@59632
|
7 |
~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf &
|
neuper@52062
|
8 |
|
wneuper@59586
|
9 |
ATTENTION: no errors in this theory do not mean that there are no errors in Isac ..
|
wneuper@59586
|
10 |
.. open theories collecting files from folders: CalcElements.thy, ProgLang.thy etc.
|
walther@59632
|
11 |
Errors are rigorously detected by isabelle build.
|
neuper@37906
|
12 |
*)
|
neuper@37906
|
13 |
|
wneuper@59347
|
14 |
theory Build_Isac
|
wneuper@59206
|
15 |
imports
|
walther@59632
|
16 |
(* theory KEStore imports Complex_Main
|
walther@59632
|
17 |
ML_file libraryC.sml
|
walther@59850
|
18 |
ML_file "rule-def.sml"
|
walther@59632
|
19 |
ML_file rule.sml
|
walther@59852
|
20 |
ML_file "rule-set.sml"
|
walther@59632
|
21 |
ML_file calcelems.sml
|
walther@59632
|
22 |
theory CalcElements imports KEStore
|
walther@59632
|
23 |
ML_file termC.sml
|
walther@59632
|
24 |
ML_file contextC.sml
|
walther@59687
|
25 |
ML_file environment.sml
|
wneuper@59586
|
26 |
*) "CalcElements/CalcElements"
|
wneuper@59586
|
27 |
|
walther@59632
|
28 |
(* theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements"
|
walther@59632
|
29 |
ML_file calculate.sml
|
walther@59773
|
30 |
|
walther@59632
|
31 |
theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"
|
walther@59632
|
32 |
theory Prog_Expr imports Calculate ListC
|
walther@59632
|
33 |
theory Program imports "~~/src/Tools/isac/CalcElements/CalcElements"
|
walther@59632
|
34 |
theory Prog_Tac imports "~~/src/Tools/isac/CalcElements/CalcElements"
|
walther@59632
|
35 |
theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements"
|
walther@59632
|
36 |
theory Auto_Prog imports Program Prog_Tac Tactical begin
|
walther@59632
|
37 |
theory ProgLang imports Prog_Expr Auto_Prog
|
walther@59632
|
38 |
ML_file rewrite.sml
|
neuper@52062
|
39 |
*) "ProgLang/ProgLang"
|
wneuper@59600
|
40 |
(*
|
walther@59674
|
41 |
theory MathEngBasic imports
|
walther@59674
|
42 |
"~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
|
walther@59674
|
43 |
ML_file "calc-tree-elem.sml"
|
walther@59632
|
44 |
ML_file model.sml
|
walther@59632
|
45 |
ML_file mstools.sml
|
walther@59632
|
46 |
ML_file "specification-elems.sml"
|
walther@59777
|
47 |
ML_file "istate-def.sml"
|
walther@59632
|
48 |
ML_file tactic.sml
|
walther@59777
|
49 |
ML_file position.sml
|
walther@59674
|
50 |
ML_file "ctree-basic.sml"
|
walther@59674
|
51 |
ML_file "ctree-access.sml"
|
walther@59674
|
52 |
ML_file "ctree-navi.sml"
|
walther@59674
|
53 |
ML_file ctree.sml
|
walther@59779
|
54 |
(*ML_file tactic.sml*)
|
walther@59777
|
55 |
ML_file calculation.sml
|
walther@59674
|
56 |
*) "MathEngBasic/MathEngBasic"
|
walther@59674
|
57 |
(*
|
walther@59674
|
58 |
theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements"
|
walther@59674
|
59 |
theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
|
walther@59632
|
60 |
ML_file ptyps.sml
|
walther@59632
|
61 |
ML_file generate.sml
|
walther@59632
|
62 |
ML_file calchead.sml
|
walther@59632
|
63 |
ML_file appl.sml
|
walther@59777
|
64 |
ML_file "step-specify.sml"
|
walther@59777
|
65 |
ML_file specify.sml
|
wneuper@59595
|
66 |
*) "Specify/Specify"
|
wneuper@59600
|
67 |
(*
|
walther@59632
|
68 |
theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
|
walther@59777
|
69 |
ML_file istate.sml
|
walther@59632
|
70 |
ML_file rewtools.sml
|
walther@59794
|
71 |
ML_file "li-tool.sml"
|
walther@59632
|
72 |
ML_file inform.sml
|
walther@59632
|
73 |
ML_file "lucas-interpreter.sml"
|
walther@59794
|
74 |
ML_file "step-solve.sml"
|
wneuper@59600
|
75 |
*) "Interpret/Interpret"
|
wneuper@59600
|
76 |
(*
|
walther@59632
|
77 |
theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
|
walther@59833
|
78 |
ML_file "fetch-tactics.sml"
|
walther@59632
|
79 |
ML_file solve.sml
|
walther@59794
|
80 |
ML_file step.sml
|
walther@59833
|
81 |
ML_file "detail-step.sml"
|
walther@59634
|
82 |
ML_file "mathengine-stateless.sml"
|
walther@59632
|
83 |
ML_file messages.sml
|
walther@59632
|
84 |
ML_file states.sml
|
wneuper@59600
|
85 |
*) "MathEngine/MathEngine"
|
wneuper@59600
|
86 |
(*
|
walther@59814
|
87 |
theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
|
walther@59814
|
88 |
ML_file "test-code.sml"
|
walther@59814
|
89 |
*) "Test_Code/Test_Code"
|
walther@59814
|
90 |
(*
|
walther@59632
|
91 |
theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
|
walther@59632
|
92 |
ML_file mathml.sml
|
walther@59632
|
93 |
ML_file datatypes.sml
|
walther@59632
|
94 |
ML_file "pbl-met-hierarchy.sml"
|
walther@59632
|
95 |
ML_file "thy-hierarchy.sml"
|
walther@59632
|
96 |
ML_file "interface-xml.sml"
|
walther@59632
|
97 |
ML_file interface.sml
|
walther@59614
|
98 |
*) "BridgeLibisabelle/BridgeLibisabelle"
|
wneuper@59147
|
99 |
|
walther@59612
|
100 |
"Knowledge/Build_Thydata" (*imports Isac.thy etc*)
|
wneuper@59469
|
101 |
|
wneuper@59601
|
102 |
(*//-----------------------------------------------------------------------------------------\\*)
|
wneuper@59601
|
103 |
(*\\-----------------------------------------------------------------------------------------//*)
|
neuper@48763
|
104 |
begin
|
neuper@48760
|
105 |
|
wneuper@59472
|
106 |
text \<open>
|
neuper@55276
|
107 |
show theory dependencies using the graph browser,
|
neuper@55276
|
108 |
open "browser_info/HOL/Isac/session.graph"
|
neuper@55276
|
109 |
and proceed from the ancestors towards the siblings.
|
wneuper@59472
|
110 |
\<close>
|
neuper@55276
|
111 |
|
wneuper@59472
|
112 |
section \<open>check presence of definitions from directories\<close>
|
neuper@48763
|
113 |
|
wneuper@59263
|
114 |
(*declare [[ML_print_depth = 999]]*)
|
wneuper@59472
|
115 |
ML \<open>
|
wneuper@59472
|
116 |
\<close> ML \<open>
|
walther@59637
|
117 |
parseNEW @{context} "xxx #> aaa bbb"
|
walther@59637
|
118 |
\<close> ML \<open>
|
walther@59637
|
119 |
#> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
|
wneuper@59587
|
120 |
\<close> ML \<open>
|
wneuper@59472
|
121 |
\<close>
|
walther@59773
|
122 |
ML \<open>Num_Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
|
wneuper@59472
|
123 |
ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
|
wneuper@59595
|
124 |
ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
|
walther@59814
|
125 |
ML \<open>Test_Code.me;\<close>
|
walther@59613
|
126 |
text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
|
walther@59801
|
127 |
ML \<open>prog_expr\<close>
|
wneuper@59562
|
128 |
|
walther@59603
|
129 |
ML \<open>Prog_Expr.eval_occurs_in\<close>
|
walther@59603
|
130 |
ML \<open>@{thm last_thmI}\<close>
|
wneuper@59472
|
131 |
ML \<open>@{thm Querkraft_Belastung}\<close>
|
neuper@41905
|
132 |
|
wneuper@59472
|
133 |
ML \<open>Celem.check_guhs_unique := false;\<close>
|
wneuper@59472
|
134 |
ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
|
wneuper@59592
|
135 |
ML \<open>@{theory "Isac_Knowledge"}\<close>
|
wneuper@59472
|
136 |
ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
|
wneuper@59472
|
137 |
ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)\<close>
|
neuper@42412
|
138 |
|
wneuper@59472
|
139 |
section \<open>State of approaching Isabelle by Isac\<close>
|
wneuper@59472
|
140 |
text \<open>
|
neuper@55431
|
141 |
Mathias Lehnfeld gives the following list in his thesis in section
|
neuper@55431
|
142 |
4.2.3 Relation to Ongoing Isabelle Development.
|
wneuper@59472
|
143 |
\<close>
|
wneuper@59472
|
144 |
subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
|
wneuper@59472
|
145 |
text \<open>
|
neuper@55433
|
146 |
REPLACE BY KEStore... (has been overlooked)
|
neuper@55433
|
147 |
calcelems.sml:val rew_ord' = Unsynchronized.ref ...
|
neuper@55433
|
148 |
KEEP FOR TRACING
|
neuper@55433
|
149 |
calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
|
neuper@55433
|
150 |
calcelems.sml:val depth = Unsynchronized.ref 99999;
|
neuper@55433
|
151 |
calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
|
neuper@55433
|
152 |
calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
|
walther@59845
|
153 |
Interpret/script.sml:val trace_LI = Unsynchronized.ref false;
|
neuper@55433
|
154 |
KEEP FOR EASIER DEVELOPMENT
|
neuper@55433
|
155 |
calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
|
neuper@55433
|
156 |
KEEP FOR DEMOS
|
neuper@55433
|
157 |
Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true;
|
neuper@55433
|
158 |
Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false;
|
neuper@55433
|
159 |
Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true;
|
wneuper@59472
|
160 |
\<close>
|
wneuper@59472
|
161 |
subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
|
wneuper@59472
|
162 |
subsection \<open>(2) Make Isac’s programming language usable\<close>
|
wneuper@59472
|
163 |
subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close>
|
wneuper@59472
|
164 |
text \<open>
|
neuper@55431
|
165 |
In 2002 isac already strived for floating point numbers. Since that time
|
neuper@55431
|
166 |
isac represents numerals as "Free", see below (*1*). These experiments are
|
neuper@55431
|
167 |
unsatisfactory with respect to logical soundness.
|
neuper@55431
|
168 |
Since Isabelle now has started to care about floating point numbers, it is high
|
neuper@55431
|
169 |
time to adopt these together with the other numerals. Isabelle2012/13's numerals
|
neuper@55431
|
170 |
are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
|
neuper@55431
|
171 |
|
neuper@55431
|
172 |
The transition from "Free" to standard numerals is a task to be scheduled for
|
neuper@55431
|
173 |
several weeks. The urgency of this task follows from the experience,
|
neuper@55431
|
174 |
that (1.2) for "thehier" is very hard, because "num_str" seems to destroy
|
neuper@55431
|
175 |
some of the long identifiers of theorems which would tremendously simplify
|
neuper@55431
|
176 |
building a hierarchy of theorems according to (1.2), see (*2*) below.
|
wneuper@59472
|
177 |
\<close>
|
wneuper@59472
|
178 |
ML \<open>(*1*) Free ("123.456", HOLogic.realT)\<close>
|
neuper@55484
|
179 |
|
wneuper@59472
|
180 |
subsection \<open>(4) Improve the efficiency of Isac’s rewrite-engine\<close>
|
wneuper@59472
|
181 |
subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
|
neuper@55431
|
182 |
|
neuper@37906
|
183 |
end
|