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@60602
|
62 |
ML_file "model-def.sml"
|
walther@59963
|
63 |
ML_file problem.sml
|
walther@59963
|
64 |
ML_file method.sml
|
walther@59963
|
65 |
ML_file "cas-command.sml"
|
walther@59963
|
66 |
|
walther@59865
|
67 |
ML_file rewrite.sml
|
walther@59963
|
68 |
|
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@60567
|
112 |
ML_file "li-tool.sml"
|
walther@59963
|
113 |
ML_file "solve-step.sml"
|
walther@59963
|
114 |
ML_file "error-pattern.sml"
|
walther@59963
|
115 |
ML_file derive.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@60638
|
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
|
Walther@60566
|
165 |
ML \<open>
|
Walther@60566
|
166 |
\<close> ML \<open>
|
Walther@60571
|
167 |
\<close> ML \<open>
|
Walther@60571
|
168 |
\<close> ML \<open>
|
Walther@60566
|
169 |
\<close>
|
Walther@60631
|
170 |
subsection \<open>make Minisubpbl independent from Thy_Info\<close>
|
Walther@60631
|
171 |
text \<open>
|
Walther@60631
|
172 |
We want Isac to become independent from sessions Specify, Interpret and Isac.
|
Walther@60631
|
173 |
This goal will be checked by the tests finally.
|
Walther@60631
|
174 |
As first step we go top down and make Minisubpbl independent form Thy_Info here
|
Walther@60631
|
175 |
and make sure, that the right ctxt is passed throughout the code.
|
Walther@60631
|
176 |
As next step we go bottom up from Thy_Info.get_theory and remove it.
|
Walther@60631
|
177 |
Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
|
Walther@60631
|
178 |
\<close>
|
Walther@60576
|
179 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
|
Walther@60576
|
180 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
|
Walther@60651
|
181 |
ML \<open>
|
Walther@60651
|
182 |
\<close> ML \<open>
|
Walther@60651
|
183 |
(* Title: 100-init-rootpbl.sml
|
Walther@60651
|
184 |
Author: Walther Neuper 1105
|
Walther@60651
|
185 |
(c) copyright due to lincense terms.
|
Walther@60651
|
186 |
*)
|
Walther@60651
|
187 |
|
Walther@60651
|
188 |
"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
|
Walther@60651
|
189 |
"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
|
Walther@60651
|
190 |
"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
|
Walther@60651
|
191 |
val (_(*example text*),
|
Walther@60651
|
192 |
(model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60651
|
193 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60651
|
194 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60651
|
195 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60651
|
196 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
|
Walther@60651
|
197 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60651
|
198 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60651
|
199 |
"ErrorBound (\<epsilon> = (0::real))" :: []),
|
Walther@60651
|
200 |
refs as ("Diff_App",
|
Walther@60651
|
201 |
["univariate_calculus", "Optimisation"],
|
Walther@60651
|
202 |
["Optimisation", "by_univariate_calculus"])))
|
Walther@60651
|
203 |
= Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
|
Walther@60651
|
204 |
|
Walther@60651
|
205 |
Test_Code.init_calc @{context} [(model, refs)];
|
Walther@60651
|
206 |
"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
|
Walther@60651
|
207 |
= (@{context}, [(model, refs)]);
|
Walther@60651
|
208 |
(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
|
Walther@60651
|
209 |
( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
|
Walther@60651
|
210 |
|
Walther@60651
|
211 |
(**)val return_nxt_specify_init_calc_PIDE =(**)
|
Walther@60651
|
212 |
Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);
|
Walther@60651
|
213 |
"~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
|
Walther@60651
|
214 |
|
Walther@60651
|
215 |
Step_Specify.initialise_PIDE thy (model, refs);
|
Walther@60651
|
216 |
"~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
|
Walther@60651
|
217 |
(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
|
Walther@60651
|
218 |
val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
|
Walther@60651
|
219 |
val (pI, (pors, pctxt), mI) =
|
Walther@60651
|
220 |
if mI = ["no_met"]
|
Walther@60651
|
221 |
then raise error "else not covered by test"
|
Walther@60651
|
222 |
else
|
Walther@60651
|
223 |
let
|
Walther@60651
|
224 |
(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
|
Walther@60651
|
225 |
(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
|
Walther@60651
|
226 |
(*old*) in (pI, (pors, pctxt), mI) end;
|
Walther@60651
|
227 |
( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
|
Walther@60651
|
228 |
in (pI, (pors, pctxt), mI) end;
|
Walther@60651
|
229 |
|
Walther@60651
|
230 |
(*/------------------- check result of O_Model.init_PIDE ------------------------------------\*)
|
Walther@60651
|
231 |
(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
|
Walther@60651
|
232 |
(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
|
Walther@60651
|
233 |
(*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
|
Walther@60651
|
234 |
|
Walther@60651
|
235 |
val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);
|
Walther@60651
|
236 |
"~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
|
Walther@60651
|
237 |
= ((pt, p), tacis);
|
Walther@60651
|
238 |
val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
|
Walther@60651
|
239 |
|
Walther@60651
|
240 |
Test_Code.TESTg_form ctxt (pt,p);
|
Walther@60651
|
241 |
"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
|
Walther@60651
|
242 |
val (form, _, _) = ME_Misc.pt_extract ctxt ptp;
|
Walther@60651
|
243 |
val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
|
Walther@60651
|
244 |
(*case*) form (*of*);
|
Walther@60651
|
245 |
val Pos.Pbl =
|
Walther@60651
|
246 |
(*case*) p_ (*of*);
|
Walther@60651
|
247 |
Test_Out.Problem [];
|
Walther@60651
|
248 |
Test_Out.MethodC [];
|
Walther@60651
|
249 |
|
Walther@60651
|
250 |
(*val return =*)
|
Walther@60651
|
251 |
Test_Out.PpcKF (Test_Out.Problem [],
|
Walther@60651
|
252 |
P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
|
Walther@60651
|
253 |
"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
|
Walther@60651
|
254 |
|
Walther@60651
|
255 |
(*//------------------ inserted hidden code ------------------------------------------------\\*)
|
Walther@60651
|
256 |
fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60651
|
257 |
| item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
|
Walther@60651
|
258 |
| item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
|
Walther@60651
|
259 |
| item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60651
|
260 |
| item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
|
Walther@60651
|
261 |
| item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
|
Walther@60651
|
262 |
| item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
|
Walther@60651
|
263 |
fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
|
Walther@60651
|
264 |
case sel of
|
Walther@60651
|
265 |
"#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
|
Walther@60651
|
266 |
| "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
|
Walther@60651
|
267 |
| "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
|
Walther@60651
|
268 |
| "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
|
Walther@60651
|
269 |
| "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
|
Walther@60651
|
270 |
| _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
|
Walther@60651
|
271 |
fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
|
Walther@60651
|
272 |
{Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
|
Walther@60651
|
273 |
fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term)
|
Walther@60651
|
274 |
| boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term);
|
Walther@60651
|
275 |
(*\\------------------ inserted hidden code ------------------------------------------------//*)
|
Walther@60651
|
276 |
|
Walther@60651
|
277 |
fun coll model [] = model
|
Walther@60651
|
278 |
| coll model ((_, _, _, field, itm_)::itms) =
|
Walther@60651
|
279 |
coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
|
Walther@60651
|
280 |
val gfr = coll P_Model.empty itms;
|
Walther@60651
|
281 |
|
Walther@60651
|
282 |
(*val return =*)
|
Walther@60651
|
283 |
add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
|
Walther@60651
|
284 |
"~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
|
Walther@60651
|
285 |
= (gfr, (map
|
Walther@60651
|
286 |
(boolterm2item ctxt) where_));
|
Walther@60651
|
287 |
"~~~~~ fun boolterm2item , args:"; val () = ();
|
Walther@60651
|
288 |
(*\\------------------ step into nxt_specify_init_calc -------------------------------------//*)
|
Walther@60651
|
289 |
\<close> ML \<open>
|
Walther@60651
|
290 |
\<close> ML \<open>
|
Walther@60651
|
291 |
\<close>
|
Walther@60580
|
292 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
|
Walther@60596
|
293 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
|
Walther@60596
|
294 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
|
Walther@60597
|
295 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
|
Walther@60598
|
296 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
|
Walther@60598
|
297 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml"
|
Walther@60608
|
298 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml"
|
Walther@60609
|
299 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/300-init-subpbl.sml"
|
Walther@60611
|
300 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml"
|
Walther@60576
|
301 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml"
|
Walther@60576
|
302 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml"
|
Walther@60576
|
303 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml"
|
Walther@60576
|
304 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/500-met-sub-to-root.sml"
|
Walther@60576
|
305 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml"
|
Walther@60576
|
306 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml"
|
Walther@60576
|
307 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/600-postcond.sml"
|
Walther@60627
|
308 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/700-interSteps.sml"
|
Walther@60627
|
309 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/710-interSteps-short.sml"
|
Walther@60629
|
310 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete-NEXT_STEP.sml"
|
Walther@60629
|
311 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
|
Walther@60629
|
312 |
ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
|
neuper@48760
|
313 |
|
neuper@55276
|
314 |
|
wneuper@59472
|
315 |
section \<open>check presence of definitions from directories\<close>
|
neuper@48763
|
316 |
|
wneuper@59263
|
317 |
(*declare [[ML_print_depth = 999]]*)
|
walther@59902
|
318 |
ML \<open>Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\<close>
|
wneuper@59472
|
319 |
ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
|
walther@59953
|
320 |
ML \<open>Input_Descript.for_real_list; (*from "Input_Descript.thy" *)\<close>
|
Walther@60557
|
321 |
ML \<open>(*Test_Code.me;*)\<close>
|
walther@59613
|
322 |
text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
|
walther@59801
|
323 |
ML \<open>prog_expr\<close>
|
wneuper@59562
|
324 |
|
walther@59603
|
325 |
ML \<open>Prog_Expr.eval_occurs_in\<close>
|
walther@59603
|
326 |
ML \<open>@{thm last_thmI}\<close>
|
walther@60077
|
327 |
(** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*)
|
neuper@41905
|
328 |
|
Walther@60502
|
329 |
declare [[check_unique = false]]
|
wneuper@59472
|
330 |
ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
|
wneuper@59592
|
331 |
ML \<open>@{theory "Isac_Knowledge"}\<close>
|
wneuper@59472
|
332 |
ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
|
walther@59997
|
333 |
ERROR: app_py: not found: ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]*)\<close>
|
neuper@42412
|
334 |
|
wneuper@59472
|
335 |
section \<open>State of approaching Isabelle by Isac\<close>
|
wneuper@59472
|
336 |
text \<open>
|
Walther@60551
|
337 |
Mathias Lehnfeld gives the following list in his thesis in section
|
neuper@55431
|
338 |
4.2.3 Relation to Ongoing Isabelle Development.
|
wneuper@59472
|
339 |
\<close>
|
wneuper@59472
|
340 |
subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
|
wneuper@59472
|
341 |
text \<open>
|
Walther@60507
|
342 |
DONE
|
wneuper@59472
|
343 |
\<close>
|
wneuper@59472
|
344 |
subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
|
wneuper@59472
|
345 |
subsection \<open>(2) Make Isac’s programming language usable\<close>
|
wneuper@59472
|
346 |
subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close>
|
wneuper@59472
|
347 |
text \<open>
|
neuper@55431
|
348 |
In 2002 isac already strived for floating point numbers. Since that time
|
neuper@55431
|
349 |
isac represents numerals as "Free", see below (*1*). These experiments are
|
neuper@55431
|
350 |
unsatisfactory with respect to logical soundness.
|
neuper@55431
|
351 |
Since Isabelle now has started to care about floating point numbers, it is high
|
neuper@55431
|
352 |
time to adopt these together with the other numerals. Isabelle2012/13's numerals
|
wenzelm@60217
|
353 |
are different from Isabelle2011, see "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/termC.sml".
|
neuper@55431
|
354 |
|
neuper@55431
|
355 |
The transition from "Free" to standard numerals is a task to be scheduled for
|
neuper@55431
|
356 |
several weeks. The urgency of this task follows from the experience,
|
neuper@55431
|
357 |
that (1.2) for "thehier" is very hard, because "num_str" seems to destroy
|
neuper@55431
|
358 |
some of the long identifiers of theorems which would tremendously simplify
|
neuper@55431
|
359 |
building a hierarchy of theorems according to (1.2), see (*2*) below.
|
wneuper@59472
|
360 |
\<close>
|
wneuper@59472
|
361 |
ML \<open>(*1*) Free ("123.456", HOLogic.realT)\<close>
|
neuper@55484
|
362 |
|
wneuper@59472
|
363 |
subsection \<open>(4) Improve the efficiency of Isac’s rewrite-engine\<close>
|
wneuper@59472
|
364 |
subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
|
neuper@55431
|
365 |
|
neuper@37906
|
366 |
end
|