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@59182
|
15 |
theory KEStore
|
wneuper@59182
|
16 |
ML_file "~~/src/Tools/isac/library.sml"
|
wneuper@59182
|
17 |
ML_file "~~/src/Tools/isac/calcelems.sml"
|
wneuper@59182
|
18 |
theory ListC
|
wneuper@59206
|
19 |
imports "~~/src/Tools/isac/KEStore"
|
wneuper@59182
|
20 |
ML_file "~~/src/Tools/isac/ProgLang/termC.sml"
|
wneuper@59182
|
21 |
ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
|
wneuper@59182
|
22 |
ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
|
wneuper@59182
|
23 |
theory Tools imports ListC begin
|
wneuper@59182
|
24 |
theory Script imports Tools begin
|
wneuper@59182
|
25 |
theory ProgLang imports Script
|
wneuper@59182
|
26 |
ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
|
neuper@52062
|
27 |
*) "ProgLang/ProgLang"
|
neuper@48761
|
28 |
|
neuper@48763
|
29 |
(* use "Interpret/mstools.sml"
|
neuper@48763
|
30 |
use "Interpret/ctree.sml"
|
neuper@48763
|
31 |
use "Interpret/ptyps.sml"
|
wneuper@59106
|
32 |
use "Interpret/generate.sml"
|
neuper@48763
|
33 |
use "Interpret/calchead.sml"
|
neuper@48763
|
34 |
use "Interpret/appl.sml"
|
neuper@48763
|
35 |
use "Interpret/rewtools.sml"
|
neuper@48763
|
36 |
use "Interpret/script.sml"
|
neuper@48763
|
37 |
use "Interpret/solve.sml"
|
neuper@48763
|
38 |
use "Interpret/inform.sml"
|
neuper@48763
|
39 |
use "Interpret/mathengine.sml"
|
neuper@52062
|
40 |
*) "Interpret/Interpret"
|
neuper@48761
|
41 |
|
neuper@52062
|
42 |
(* use "xmlsrc/mathml.sml"
|
neuper@48762
|
43 |
use "xmlsrc/datatypes.sml"
|
neuper@41905
|
44 |
use "xmlsrc/pbl-met-hierarchy.sml"
|
neuper@48895
|
45 |
use "xmlsrc/thy-hierarchy.sml"
|
neuper@41905
|
46 |
use "xmlsrc/interface-xml.sml"
|
neuper@52062
|
47 |
*) "xmlsrc/xmlsrc"
|
neuper@41905
|
48 |
|
neuper@48763
|
49 |
(* use "Frontend/messages.sml"
|
neuper@41905
|
50 |
use "Frontend/states.sml"
|
neuper@41905
|
51 |
use "Frontend/interface.sml"
|
neuper@41905
|
52 |
|
neuper@41905
|
53 |
use "print_exn_G.sml"
|
neuper@52062
|
54 |
*) "Frontend/Frontend"
|
wneuper@59147
|
55 |
|
wneuper@59147
|
56 |
"Knowledge/Build_Thydata" (*imports Isac.thy etc*)
|
wneuper@59147
|
57 |
|
wneuper@59146
|
58 |
(* the Protocol for the connection isac-java -- Isabelle/Isac is built separately:
|
wneuper@59148
|
59 |
here we partly check consistency libisabelle/Isac -- Isabelle/Isac: *)
|
wneuper@59469
|
60 |
(*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol
|
wneuper@59469
|
61 |
|
neuper@48763
|
62 |
begin
|
neuper@48760
|
63 |
|
neuper@55276
|
64 |
text {*
|
neuper@55276
|
65 |
show theory dependencies using the graph browser,
|
neuper@55276
|
66 |
open "browser_info/HOL/Isac/session.graph"
|
neuper@55276
|
67 |
and proceed from the ancestors towards the siblings.
|
neuper@55276
|
68 |
*}
|
neuper@55276
|
69 |
|
neuper@55431
|
70 |
section {*check presence of definitions from directories*}
|
neuper@48763
|
71 |
|
wneuper@59263
|
72 |
(*declare [[ML_print_depth = 999]]*)
|
wneuper@59152
|
73 |
ML {*
|
wneuper@59152
|
74 |
*} ML {*
|
wneuper@59152
|
75 |
*}
|
wneuper@59382
|
76 |
|
wneuper@59382
|
77 |
(*==============================================================================================
|
wneuper@59382
|
78 |
The test below from calculate.sml raises an exception with the cleaned Rewrite.
|
wneuper@59382
|
79 |
The differences to the working 'fun rewrite' are that significant,
|
wneuper@59382
|
80 |
that we want to rely on 'hg revert'.
|
wneuper@59382
|
81 |
For that purpose we save this changeset with a broken 'fun rewrite' and tests not running.
|
wneuper@59382
|
82 |
*)
|
wneuper@59382
|
83 |
ML {*
|
wneuper@59382
|
84 |
*} ML {*
|
wneuper@59382
|
85 |
(*--------------(2): does divide work in Test_simplify ?: ------*)
|
wneuper@59382
|
86 |
val thy = @{theory Test};
|
wneuper@59389
|
87 |
val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
|
wneuper@59382
|
88 |
val rls = Test_simplify;
|
wneuper@59382
|
89 |
*} ML {*
|
wneuper@59386
|
90 |
val (t,_) = the (Rewrite.rewrite_set_ thy false rls t);
|
wneuper@59382
|
91 |
(*val t = Free ("3","Real.real") : term*)
|
wneuper@59382
|
92 |
*} ML {*
|
wneuper@59382
|
93 |
|
wneuper@59382
|
94 |
(*--------------(3): is_const works ?: -------------------------------------*)
|
wneuper@59389
|
95 |
val t = (Thm.term_of o the o (TermC.parse @{theory})) "2 is_const";
|
wneuper@59382
|
96 |
*} ML {*
|
wneuper@59386
|
97 |
Rewrite.rewrite_set_ @{theory Test} false tval_rls t;
|
wneuper@59382
|
98 |
|
wneuper@59383
|
99 |
(* exception TERM raised (line 270 of "~~/src/HOL/Tools/hologic.ML"):
|
wneuper@59382
|
100 |
dest_eq
|
wneuper@59382
|
101 |
0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True*)
|
wneuper@59382
|
102 |
*} ML {*
|
wneuper@59382
|
103 |
*}
|
wneuper@59382
|
104 |
(*==============================================================================================*)
|
wneuper@59382
|
105 |
|
wneuper@59388
|
106 |
ML {* Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *) *}
|
wneuper@59381
|
107 |
ML {* Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *) *}
|
wneuper@59374
|
108 |
ML {* LTool.is_reall_dsc; (*from "ProgLang/scrtools.sml" *) *}
|
wneuper@59261
|
109 |
ML {* Math_Engine.me; (*from "Interpret/mathengine.sml"*) *}
|
neuper@41905
|
110 |
ML {* contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*) *}
|
neuper@41905
|
111 |
ML {* print_exn_unit *}
|
neuper@48880
|
112 |
ML {* list_rls (*from Atools.thy WN130615??? or ProgLang???*) *}
|
neuper@48763
|
113 |
|
neuper@41905
|
114 |
ML {* eval_occurs_in (*from Atools.thy*) *}
|
neuper@41905
|
115 |
ML {* @{thm last_thmI} (*from Atools.thy*) *}
|
neuper@41931
|
116 |
ML {*@{thm Querkraft_Belastung}*}
|
neuper@41905
|
117 |
|
wneuper@59406
|
118 |
ML {* Celem.check_guhs_unique := false; *}
|
neuper@48880
|
119 |
ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
|
neuper@41943
|
120 |
ML {* @{theory "Isac"} *}
|
neuper@55454
|
121 |
ML {* (*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
|
neuper@55454
|
122 |
ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*) *}
|
neuper@42412
|
123 |
|
neuper@55431
|
124 |
section {* State of approaching Isabelle by Isac *}
|
neuper@55431
|
125 |
text {*
|
neuper@55431
|
126 |
Mathias Lehnfeld gives the following list in his thesis in section
|
neuper@55431
|
127 |
4.2.3 Relation to Ongoing Isabelle Development.
|
neuper@55431
|
128 |
*}
|
neuper@55431
|
129 |
subsection {* (0) Survey on remaining Unsynchronized.ref *}
|
neuper@55433
|
130 |
text {*
|
neuper@55433
|
131 |
REPLACE BY KEStore... (has been overlooked)
|
neuper@55433
|
132 |
calcelems.sml:val rew_ord' = Unsynchronized.ref ...
|
neuper@55433
|
133 |
KEEP FOR TRACING
|
neuper@55433
|
134 |
calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
|
neuper@55433
|
135 |
calcelems.sml:val depth = Unsynchronized.ref 99999;
|
neuper@55433
|
136 |
calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
|
neuper@55433
|
137 |
calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
|
neuper@55433
|
138 |
Interpret/script.sml:val trace_script = Unsynchronized.ref false;
|
neuper@55433
|
139 |
KEEP FOR EASIER DEVELOPMENT
|
neuper@55433
|
140 |
calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
|
neuper@55433
|
141 |
KEEP FOR DEMOS
|
neuper@55433
|
142 |
Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true;
|
neuper@55433
|
143 |
Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false;
|
neuper@55433
|
144 |
Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true;
|
neuper@55433
|
145 |
*}
|
neuper@55431
|
146 |
subsection {* (1) Exploit parallelism for concurrent session management *}
|
neuper@55431
|
147 |
subsection {* (2) Make Isac’s programming language usable *}
|
neuper@55431
|
148 |
subsection {* (3) Adopt Isabelle’s numeral computation for Isac *}
|
neuper@55431
|
149 |
text {*
|
neuper@55431
|
150 |
In 2002 isac already strived for floating point numbers. Since that time
|
neuper@55431
|
151 |
isac represents numerals as "Free", see below (*1*). These experiments are
|
neuper@55431
|
152 |
unsatisfactory with respect to logical soundness.
|
neuper@55431
|
153 |
Since Isabelle now has started to care about floating point numbers, it is high
|
neuper@55431
|
154 |
time to adopt these together with the other numerals. Isabelle2012/13's numerals
|
neuper@55431
|
155 |
are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml".
|
neuper@55431
|
156 |
|
neuper@55431
|
157 |
The transition from "Free" to standard numerals is a task to be scheduled for
|
neuper@55431
|
158 |
several weeks. The urgency of this task follows from the experience,
|
neuper@55431
|
159 |
that (1.2) for "thehier" is very hard, because "num_str" seems to destroy
|
neuper@55431
|
160 |
some of the long identifiers of theorems which would tremendously simplify
|
neuper@55431
|
161 |
building a hierarchy of theorems according to (1.2), see (*2*) below.
|
neuper@55431
|
162 |
*}
|
neuper@55431
|
163 |
ML {*(*1*) Free ("123.456", HOLogic.realT) *}
|
neuper@55484
|
164 |
|
neuper@55431
|
165 |
subsection {* (4) Improve the efficiency of Isac’s rewrite-engine *}
|
neuper@55431
|
166 |
subsection {* (5) Adopt Isabelle/jEdit for Isac *}
|
neuper@55431
|
167 |
|
neuper@37906
|
168 |
end
|