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