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 ..
|
walther@59866
|
10 |
.. open theories collecting files from folders: BaseDefinitions.thy, ProgLang.thy etc.
|
walther@59632
|
11 |
Errors are rigorously detected by isabelle build.
|
neuper@37906
|
12 |
*)
|
neuper@37906
|
13 |
|
walther@59998
|
14 |
theory Build_Isac
|
wneuper@59206
|
15 |
imports
|
walther@59887
|
16 |
(* theory Know_Store imports Complex_Main
|
wenzelm@60192
|
17 |
$ISABELLE_ISAC/BaseDefinitions
|
walther@59632
|
18 |
ML_file libraryC.sml
|
walther@59865
|
19 |
ML_file theoryC.sml
|
walther@59963
|
20 |
ML_file unparseC.sml
|
walther@59850
|
21 |
ML_file "rule-def.sml"
|
walther@59963
|
22 |
ML_file "thmC-def.sml"
|
walther@59919
|
23 |
ML_file "eval-def.sml"
|
walther@59858
|
24 |
ML_file "rewrite-order.sml"
|
walther@59632
|
25 |
ML_file rule.sml
|
walther@59963
|
26 |
ML_file "error-pattern-def.sml"
|
walther@59852
|
27 |
ML_file "rule-set.sml"
|
walther@59963
|
28 |
|
walther@59963
|
29 |
ML_file "store.sml"
|
walther@59963
|
30 |
ML_file "check-unique.sml"
|
walther@59963
|
31 |
ML_file "specification.sml"
|
walther@59963
|
32 |
ML_file "model-pattern.sml"
|
walther@59963
|
33 |
ML_file "problem-def.sml"
|
walther@59963
|
34 |
ML_file "method-def.sml"
|
walther@59963
|
35 |
ML_file "cas-def.sml"
|
walther@59963
|
36 |
ML_file "thy-write.sml"
|
walther@59887
|
37 |
theory BaseDefinitions imports Know_Store
|
wenzelm@60192
|
38 |
$ISABELLE_ISAC/BaseDefinitions
|
walther@59632
|
39 |
ML_file termC.sml
|
walther@59963
|
40 |
ML_file substitution.sml
|
walther@59632
|
41 |
ML_file contextC.sml
|
walther@59687
|
42 |
ML_file environment.sml
|
walther@60077
|
43 |
( ** ) "BaseDefinitions/BaseDefinitions"( **)
|
walther@60317
|
44 |
(*
|
Walther@60516
|
45 |
theory Calc_Binop imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
walther@60317
|
46 |
at $ISABELLE_ISAC/ProgLang
|
walther@59902
|
47 |
ML_file evaluate.sml
|
wenzelm@60192
|
48 |
theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
wenzelm@60192
|
49 |
theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
Walther@60516
|
50 |
theory Prog_Expr imports Calc_Binop ListC Program
|
walther@60317
|
51 |
theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
wenzelm@60192
|
52 |
theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
walther@60317
|
53 |
theory Auto_Prog imports Prog_Tac Tactical
|
walther@59632
|
54 |
theory ProgLang imports Prog_Expr Auto_Prog
|
walther@60317
|
55 |
at $ISABELLE_ISAC/ProgLang
|
walther@60077
|
56 |
( ** ) "ProgLang/ProgLang"( **)
|
wneuper@59600
|
57 |
(*
|
walther@59674
|
58 |
theory MathEngBasic imports
|
wenzelm@60192
|
59 |
"$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
|
walther@60317
|
60 |
at $ISABELLE_ISAC/MathEngBasic
|
walther@59875
|
61 |
ML_file thmC.sml
|
walther@59963
|
62 |
ML_file problem.sml
|
walther@59963
|
63 |
ML_file method.sml
|
walther@59963
|
64 |
ML_file "cas-command.sml"
|
walther@59963
|
65 |
|
walther@59865
|
66 |
ML_file rewrite.sml
|
walther@59963
|
67 |
|
walther@59963
|
68 |
ML_file "model-def.sml"
|
walther@59963
|
69 |
ML_file "istate-def.sml"
|
walther@59674
|
70 |
ML_file "calc-tree-elem.sml"
|
walther@59963
|
71 |
ML_file "pre-conds-def.sml"
|
walther@59963
|
72 |
|
walther@59632
|
73 |
ML_file tactic.sml
|
walther@59963
|
74 |
ML_file applicable.sml
|
walther@59963
|
75 |
|
walther@59777
|
76 |
ML_file position.sml
|
walther@59674
|
77 |
ML_file "ctree-basic.sml"
|
walther@59674
|
78 |
ML_file "ctree-access.sml"
|
walther@59674
|
79 |
ML_file "ctree-navi.sml"
|
walther@59674
|
80 |
ML_file ctree.sml
|
walther@59963
|
81 |
|
walther@59963
|
82 |
ML_file "state-steps.sml"
|
walther@59777
|
83 |
ML_file calculation.sml
|
walther@60077
|
84 |
( ** ) "MathEngBasic/MathEngBasic"( **)
|
walther@59674
|
85 |
(*
|
wenzelm@60192
|
86 |
theory Input_Descript imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
|
wenzelm@60192
|
87 |
$ISABELLE_ISAC/Specify
|
wenzelm@60192
|
88 |
theory Specify imports "$ISABELLE_ISAC/ProgLang/ProgLang" Input_Descript
|
wenzelm@60192
|
89 |
$ISABELLE_ISAC/Specify
|
walther@59963
|
90 |
ML_file formalise.sml
|
walther@59963
|
91 |
ML_file "o-model.sml"
|
walther@59963
|
92 |
ML_file "i-model.sml"
|
walther@59963
|
93 |
ML_file "p-model.sml"
|
walther@59963
|
94 |
ML_file model.sml
|
walther@59963
|
95 |
ML_file "pre-conditions.sml"
|
walther@59963
|
96 |
ML_file refine.sml
|
walther@59963
|
97 |
ML_file "mstools.sml" (*..TODO review*)
|
walther@59963
|
98 |
ML_file ptyps.sml (*..TODO review*)
|
walther@59963
|
99 |
ML_file "test-out.sml"
|
walther@59963
|
100 |
ML_file "specify-step.sml"
|
walther@59963
|
101 |
ML_file calchead.sml (*..TODO review*)
|
walther@59963
|
102 |
ML_file "input-calchead.sml"
|
walther@59777
|
103 |
ML_file "step-specify.sml"
|
walther@59777
|
104 |
ML_file specify.sml
|
walther@60077
|
105 |
( ** ) "Specify/Specify"( **)
|
wneuper@59600
|
106 |
(*
|
wenzelm@60192
|
107 |
theory Interpret imports "$ISABELLE_ISAC/Specify/Specify"
|
wenzelm@60192
|
108 |
$ISABELLE_ISAC/Interpret
|
walther@59777
|
109 |
ML_file istate.sml
|
walther@59963
|
110 |
ML_file "sub-problem.sml"
|
walther@59963
|
111 |
ML_file "thy-read.sml"
|
walther@59963
|
112 |
ML_file "solve-step.sml"
|
walther@59963
|
113 |
ML_file "error-pattern.sml"
|
walther@59963
|
114 |
ML_file derive.sml
|
walther@59794
|
115 |
ML_file "li-tool.sml"
|
walther@59632
|
116 |
ML_file "lucas-interpreter.sml"
|
walther@59794
|
117 |
ML_file "step-solve.sml"
|
walther@60077
|
118 |
( ** ) "Interpret/Interpret"( **)
|
wneuper@59600
|
119 |
(*
|
walther@60077
|
120 |
theory MathEngine imports Interpret.Interpret
|
wenzelm@60192
|
121 |
$ISABELLE_ISAC/MathEngine
|
walther@59833
|
122 |
ML_file "fetch-tactics.sml"
|
walther@59632
|
123 |
ML_file solve.sml
|
walther@59794
|
124 |
ML_file step.sml
|
walther@59833
|
125 |
ML_file "detail-step.sml"
|
walther@59634
|
126 |
ML_file "mathengine-stateless.sml"
|
walther@59632
|
127 |
ML_file messages.sml
|
walther@59632
|
128 |
ML_file states.sml
|
walther@60077
|
129 |
( ** ) "MathEngine/MathEngine"( **)
|
wneuper@59600
|
130 |
(*
|
wenzelm@60192
|
131 |
theory Test_Code imports "$ISABELLE_ISAC/MathEngine/MathEngine"
|
wenzelm@60192
|
132 |
$ISABELLE_ISAC/Test_Code
|
walther@59814
|
133 |
ML_file "test-code.sml"
|
walther@60077
|
134 |
( ** ) "Test_Code/Test_Code"( **)
|
walther@59814
|
135 |
(*
|
wenzelm@60192
|
136 |
theory BridgeLibisabelle imports "$ISABELLE_ISAC/MathEngine/MathEngine"
|
wenzelm@60192
|
137 |
$ISABELLE_ISAC/BridgeLibisabelle
|
walther@59963
|
138 |
ML_file "thy-present.sml"
|
walther@59963
|
139 |
ML_file mathml.sml
|
walther@59632
|
140 |
ML_file datatypes.sml
|
walther@59632
|
141 |
ML_file "pbl-met-hierarchy.sml"
|
walther@59632
|
142 |
ML_file "thy-hierarchy.sml"
|
walther@59632
|
143 |
ML_file "interface-xml.sml"
|
walther@59632
|
144 |
ML_file interface.sml
|
walther@60077
|
145 |
( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **)
|
walther@60044
|
146 |
(*
|
walther@60181
|
147 |
theory Calculation imports Calculation (*preliminary for starting Isabelle/Isac*)
|
wenzelm@60192
|
148 |
$ISABELLE_ISAC/BridgeJEdit
|
walther@60181
|
149 |
ML_file parseC.sml
|
walther@60181
|
150 |
ML_file preliminary.sml
|
walther@60181
|
151 |
theory BridgeJEdit imports Calculation (*preliminary for starting Isabelle/Isac*)
|
wenzelm@60192
|
152 |
$ISABELLE_ISAC/BridgeJEdit
|
walther@60181
|
153 |
( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **)
|
walther@60181
|
154 |
(*
|
wenzelm@60192
|
155 |
theory Isac imports "$ISABELLE_ISAC/MathEngine/MathEngine"
|
walther@60044
|
156 |
ML_file parseC.sml
|
walther@60044
|
157 |
theory BridgeJEdit imports Isac
|
walther@60149
|
158 |
( **) "BridgeJEdit/BridgeJEdit" (*DEactivate after devel.of BridgeJEdit*)
|
wneuper@59147
|
159 |
|
walther@59612
|
160 |
"Knowledge/Build_Thydata" (*imports Isac.thy etc*)
|
wneuper@59469
|
161 |
|
wneuper@59601
|
162 |
(*//-----------------------------------------------------------------------------------------\\*)
|
wneuper@59601
|
163 |
(*\\-----------------------------------------------------------------------------------------//*)
|
neuper@48763
|
164 |
begin
|
neuper@48760
|
165 |
|
wneuper@59472
|
166 |
text \<open>
|
neuper@55276
|
167 |
show theory dependencies using the graph browser,
|
neuper@55276
|
168 |
open "browser_info/HOL/Isac/session.graph"
|
neuper@55276
|
169 |
and proceed from the ancestors towards the siblings.
|
wneuper@59472
|
170 |
\<close>
|
neuper@55276
|
171 |
|
wneuper@59472
|
172 |
section \<open>check presence of definitions from directories\<close>
|
neuper@48763
|
173 |
|
wneuper@59263
|
174 |
(*declare [[ML_print_depth = 999]]*)
|
walther@59902
|
175 |
ML \<open>Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\<close>
|
wneuper@59472
|
176 |
ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
|
walther@59953
|
177 |
ML \<open>Input_Descript.for_real_list; (*from "Input_Descript.thy" *)\<close>
|
Walther@60557
|
178 |
ML \<open>(*Test_Code.me;*)\<close>
|
walther@59613
|
179 |
text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
|
walther@59801
|
180 |
ML \<open>prog_expr\<close>
|
wneuper@59562
|
181 |
|
walther@59603
|
182 |
ML \<open>Prog_Expr.eval_occurs_in\<close>
|
walther@59603
|
183 |
ML \<open>@{thm last_thmI}\<close>
|
walther@60077
|
184 |
(** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*)
|
neuper@41905
|
185 |
|
Walther@60502
|
186 |
declare [[check_unique = false]]
|
wneuper@59472
|
187 |
ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
|
wneuper@59592
|
188 |
ML \<open>@{theory "Isac_Knowledge"}\<close>
|
wneuper@59472
|
189 |
ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
|
walther@59997
|
190 |
ERROR: app_py: not found: ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)\<close>
|
neuper@42412
|
191 |
|
wneuper@59472
|
192 |
section \<open>State of approaching Isabelle by Isac\<close>
|
wneuper@59472
|
193 |
text \<open>
|
Walther@60551
|
194 |
Mathias Lehnfeld gives the following list in his thesis in section
|
neuper@55431
|
195 |
4.2.3 Relation to Ongoing Isabelle Development.
|
wneuper@59472
|
196 |
\<close>
|
wneuper@59472
|
197 |
subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
|
wneuper@59472
|
198 |
text \<open>
|
Walther@60507
|
199 |
DONE
|
wneuper@59472
|
200 |
\<close>
|
wneuper@59472
|
201 |
subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
|
wneuper@59472
|
202 |
subsection \<open>(2) Make Isac’s programming language usable\<close>
|
wneuper@59472
|
203 |
subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close>
|
wneuper@59472
|
204 |
text \<open>
|
neuper@55431
|
205 |
In 2002 isac already strived for floating point numbers. Since that time
|
neuper@55431
|
206 |
isac represents numerals as "Free", see below (*1*). These experiments are
|
neuper@55431
|
207 |
unsatisfactory with respect to logical soundness.
|
neuper@55431
|
208 |
Since Isabelle now has started to care about floating point numbers, it is high
|
neuper@55431
|
209 |
time to adopt these together with the other numerals. Isabelle2012/13's numerals
|
wenzelm@60217
|
210 |
are different from Isabelle2011, see "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/termC.sml".
|
neuper@55431
|
211 |
|
neuper@55431
|
212 |
The transition from "Free" to standard numerals is a task to be scheduled for
|
neuper@55431
|
213 |
several weeks. The urgency of this task follows from the experience,
|
neuper@55431
|
214 |
that (1.2) for "thehier" is very hard, because "num_str" seems to destroy
|
neuper@55431
|
215 |
some of the long identifiers of theorems which would tremendously simplify
|
neuper@55431
|
216 |
building a hierarchy of theorems according to (1.2), see (*2*) below.
|
wneuper@59472
|
217 |
\<close>
|
wneuper@59472
|
218 |
ML \<open>(*1*) Free ("123.456", HOLogic.realT)\<close>
|
neuper@55484
|
219 |
|
wneuper@59472
|
220 |
subsection \<open>(4) Improve the efficiency of Isac’s rewrite-engine\<close>
|
wneuper@59472
|
221 |
subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
|
neuper@55431
|
222 |
|
neuper@37906
|
223 |
end
|