walther@59632: (* Title: build the Isac-Kernel: MathEngine & Knowledge neuper@38057: Author: Walther Neuper, TU Graz, 100808 neuper@38051: (c) due to copyright terms neuper@38051: neuper@52062: For creating a heap image of isac see ~~/ROOT. walther@59632: For debugging see text at begin below, e.g. theory dependencies: walther@59632: ~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf & neuper@52062: wneuper@59586: ATTENTION: no errors in this theory do not mean that there are no errors in Isac .. wneuper@59586: .. open theories collecting files from folders: CalcElements.thy, ProgLang.thy etc. walther@59632: Errors are rigorously detected by isabelle build. neuper@37906: *) neuper@37906: wneuper@59347: theory Build_Isac wneuper@59206: imports walther@59632: (* theory KEStore imports Complex_Main walther@59632: ML_file libraryC.sml walther@59632: ML_file rule.sml walther@59632: ML_file calcelems.sml walther@59632: theory CalcElements imports KEStore walther@59632: ML_file termC.sml walther@59632: ML_file contextC.sml wneuper@59586: *) "CalcElements/CalcElements" wneuper@59586: walther@59632: (* theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements" walther@59632: ML_file calculate.sml walther@59632: theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements" walther@59632: theory Prog_Expr imports Calculate ListC walther@59632: theory Program imports "~~/src/Tools/isac/CalcElements/CalcElements" walther@59632: theory Prog_Tac imports "~~/src/Tools/isac/CalcElements/CalcElements" walther@59632: theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements" walther@59632: theory Auto_Prog imports Program Prog_Tac Tactical begin walther@59632: theory ProgLang imports Prog_Expr Auto_Prog walther@59632: ML_file rewrite.sml neuper@52062: *) "ProgLang/ProgLang" wneuper@59600: (* walther@59632: theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements" walther@59632: theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript walther@59632: ML_file model.sml walther@59632: ML_file mstools.sml walther@59632: ML_file "specification-elems.sml" walther@59632: ML_file istate.sml walther@59632: ML_file tactic.sml walther@59632: ML_file "ctree-basic.sml" (*shift to base in common with Interpret*) walther@59632: ML_file "ctree-access.sml"(*shift to base in common with Interpret*) walther@59632: ML_file "ctree-navi.sml" (*shift to base in common with Interpret*) walther@59632: ML_file ctree.sml (*shift to base in common with Interpret*) walther@59632: ML_file ptyps.sml walther@59632: ML_file generate.sml walther@59632: ML_file calchead.sml walther@59632: ML_file appl.sml wneuper@59595: *) "Specify/Specify" wneuper@59600: (* walther@59632: theory Interpret imports "~~/src/Tools/isac/Specify/Specify" walther@59632: ML_file rewtools.sml walther@59632: ML_file script.sml walther@59632: ML_file inform.sml walther@59632: ML_file "lucas-interpreter.sml" wneuper@59600: *) "Interpret/Interpret" wneuper@59600: (* walther@59632: theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret" walther@59632: ML_file solve.sml walther@59632: ML_file mathengine.sml walther@59632: ML_file "~~/src/Tools/isac/Frontend/messages.sml" walther@59632: ML_file messages.sml walther@59632: ML_file states.sml wneuper@59600: *) "MathEngine/MathEngine" wneuper@59600: (* walther@59632: theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine" walther@59632: ML_file mathml.sml walther@59632: ML_file datatypes.sml walther@59632: ML_file "pbl-met-hierarchy.sml" walther@59632: ML_file "thy-hierarchy.sml" walther@59632: ML_file "interface-xml.sml" walther@59632: ML_file interface.sml walther@59614: *) "BridgeLibisabelle/BridgeLibisabelle" wneuper@59147: walther@59612: "Knowledge/Build_Thydata" (*imports Isac.thy etc*) wneuper@59469: wneuper@59601: (*//-----------------------------------------------------------------------------------------\\*) wneuper@59601: (*\\-----------------------------------------------------------------------------------------//*) neuper@48763: begin neuper@48760: wneuper@59472: text \ neuper@55276: show theory dependencies using the graph browser, neuper@55276: open "browser_info/HOL/Isac/session.graph" neuper@55276: and proceed from the ancestors towards the siblings. wneuper@59472: \ neuper@55276: wneuper@59472: section \check presence of definitions from directories\ neuper@48763: wneuper@59263: (*declare [[ML_print_depth = 999]]*) wneuper@59472: ML \ wneuper@59472: \ ML \ wneuper@59587: \ ML \ wneuper@59472: \ wneuper@59472: ML \Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\ wneuper@59472: ML \Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\ wneuper@59595: ML \Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\ walther@59603: ML \Math_Engine.me;\ walther@59613: text \contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\ walther@59603: ML \list_rls\ wneuper@59562: walther@59603: ML \Prog_Expr.eval_occurs_in\ walther@59603: ML \@{thm last_thmI}\ wneuper@59472: ML \@{thm Querkraft_Belastung}\ neuper@41905: wneuper@59472: ML \Celem.check_guhs_unique := false;\ wneuper@59472: ML \writeln "**** isac kernel = math-engine + Knowledge complete ******"\ wneuper@59592: ML \@{theory "Isac_Knowledge"}\ wneuper@59472: ML \(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] wneuper@59472: ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)\ neuper@42412: wneuper@59472: section \State of approaching Isabelle by Isac\ wneuper@59472: text \ neuper@55431: Mathias Lehnfeld gives the following list in his thesis in section neuper@55431: 4.2.3 Relation to Ongoing Isabelle Development. wneuper@59472: \ wneuper@59472: subsection \(0) Survey on remaining Unsynchronized.ref\ wneuper@59472: text \ neuper@55433: REPLACE BY KEStore... (has been overlooked) neuper@55433: calcelems.sml:val rew_ord' = Unsynchronized.ref ... neuper@55433: KEEP FOR TRACING neuper@55433: calcelems.sml:val trace_rewrite = Unsynchronized.ref false; neuper@55433: calcelems.sml:val depth = Unsynchronized.ref 99999; neuper@55433: calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999; neuper@55433: calcelems.sml:val lim_deriv = Unsynchronized.ref 100; neuper@55433: Interpret/script.sml:val trace_script = Unsynchronized.ref false; neuper@55433: KEEP FOR EASIER DEVELOPMENT neuper@55433: calcelems.sml:val check_guhs_unique = Unsynchronized.ref true; neuper@55433: KEEP FOR DEMOS neuper@55433: Knowledge/GCD_Poly_ML.thy: val trace_div = Unsynchronized.ref true; neuper@55433: Knowledge/GCD_Poly_ML.thy: val trace_div_invariant = Unsynchronized.ref false; neuper@55433: Knowledge/GCD_Poly_ML.thy: val trace_Euclid = Unsynchronized.ref true; wneuper@59472: \ wneuper@59472: subsection \(1) Exploit parallelism for concurrent session management\ wneuper@59472: subsection \(2) Make Isac’s programming language usable\ wneuper@59472: subsection \(3) Adopt Isabelle’s numeral computation for Isac\ wneuper@59472: text \ neuper@55431: In 2002 isac already strived for floating point numbers. Since that time neuper@55431: isac represents numerals as "Free", see below (*1*). These experiments are neuper@55431: unsatisfactory with respect to logical soundness. neuper@55431: Since Isabelle now has started to care about floating point numbers, it is high neuper@55431: time to adopt these together with the other numerals. Isabelle2012/13's numerals neuper@55431: are different from Isabelle2011, see "test/Tools/isac/ProgLang/termC.sml". neuper@55431: neuper@55431: The transition from "Free" to standard numerals is a task to be scheduled for neuper@55431: several weeks. The urgency of this task follows from the experience, neuper@55431: that (1.2) for "thehier" is very hard, because "num_str" seems to destroy neuper@55431: some of the long identifiers of theorems which would tremendously simplify neuper@55431: building a hierarchy of theorems according to (1.2), see (*2*) below. wneuper@59472: \ wneuper@59472: ML \(*1*) Free ("123.456", HOLogic.realT)\ neuper@55484: wneuper@59472: subsection \(4) Improve the efficiency of Isac’s rewrite-engine\ wneuper@59472: subsection \(5) Adopt Isabelle/jEdit for Isac\ neuper@55431: neuper@37906: end