
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@59850:       ML_file "rule-def.sml"
walther@59853:       ML_file "exec-def.sml"
walther@59632:       ML_file rule.sml
walther@59852:       ML_file "rule-set.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
walther@59687:     ML_file environment.sml
wneuper@59586: *)        "CalcElements/CalcElements"
wneuper@59586: 
walther@59632: (*    theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements"
walther@59632:         ML_file calculate.sml
walther@59773: 
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@59674:   theory MathEngBasic imports
walther@59674:     "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
walther@59674:     ML_file "calc-tree-elem.sml"
walther@59632:     ML_file model.sml
walther@59632:     ML_file mstools.sml
walther@59632:     ML_file "specification-elems.sml"
walther@59777:     ML_file "istate-def.sml"
walther@59632:     ML_file tactic.sml
walther@59777:     ML_file position.sml
walther@59674:     ML_file "ctree-basic.sml"
walther@59674:     ML_file "ctree-access.sml"
walther@59674:     ML_file "ctree-navi.sml"
walther@59674:     ML_file ctree.sml
walther@59779:   (*ML_file tactic.sml*)
walther@59777:     ML_file calculation.sml
walther@59674: *)        "MathEngBasic/MathEngBasic"
walther@59674: (*
walther@59674:     theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements"
walther@59674:   theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
walther@59632:     ML_file ptyps.sml
walther@59632:     ML_file generate.sml
walther@59632:     ML_file calchead.sml
walther@59632:     ML_file appl.sml
walther@59777:     ML_file "step-specify.sml"
walther@59777:     ML_file specify.sml
wneuper@59595: *)        "Specify/Specify"
wneuper@59600: (*
walther@59632:   theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
walther@59777:     ML_file istate.sml
walther@59632:     ML_file rewtools.sml
walther@59794:     ML_file "li-tool.sml"
walther@59632:     ML_file inform.sml
walther@59632:     ML_file "lucas-interpreter.sml"
walther@59794:     ML_file "step-solve.sml"
wneuper@59600: *)        "Interpret/Interpret"
wneuper@59600: (*
walther@59632:   theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
walther@59833:     ML_file "fetch-tactics.sml"
walther@59632:     ML_file solve.sml
walther@59794:     ML_file step.sml
walther@59833:     ML_file "detail-step.sml"
walther@59634:     ML_file "mathengine-stateless.sml"
walther@59632:     ML_file messages.sml
walther@59632:     ML_file states.sml
wneuper@59600: *)        "MathEngine/MathEngine"
wneuper@59600: (*
walther@59814:   theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine"
walther@59814:     ML_file "test-code.sml"
walther@59814: *)        "Test_Code/Test_Code"
walther@59814: (*
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 \<open>
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: \<close>
neuper@55276: 
wneuper@59472: section \<open>check presence of definitions from directories\<close>
neuper@48763: 
wneuper@59263: (*declare [[ML_print_depth = 999]]*)
wneuper@59472: ML \<open>
wneuper@59472: \<close> ML \<open>
walther@59637: parseNEW @{context} "xxx #> aaa bbb"
walther@59637: \<close> ML \<open>
walther@59637: #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
wneuper@59587: \<close> ML \<open>
wneuper@59472: \<close>
walther@59773: ML \<open>Num_Calc.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
wneuper@59472: ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
wneuper@59595: ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
walther@59814: ML \<open>Test_Code.me;\<close>
walther@59613: text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close>
walther@59801: ML \<open>prog_expr\<close>
wneuper@59562:                                                          
walther@59603: ML \<open>Prog_Expr.eval_occurs_in\<close>
walther@59603: ML \<open>@{thm last_thmI}\<close>
wneuper@59472: ML \<open>@{thm Querkraft_Belastung}\<close>
neuper@41905: 
wneuper@59472: ML \<open>Celem.check_guhs_unique := false;\<close>
wneuper@59472: ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
wneuper@59592: ML \<open>@{theory "Isac_Knowledge"}\<close>
wneuper@59472: ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
wneuper@59472:   ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)\<close>
neuper@42412: 
wneuper@59472: section \<open>State of approaching Isabelle by Isac\<close>
wneuper@59472: text \<open>
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: \<close>
wneuper@59472: subsection \<open>(0) Survey on remaining Unsynchronized.ref\<close>
wneuper@59472: text \<open>
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;
walther@59845:     Interpret/script.sml:val trace_LI = 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: \<close>
wneuper@59472: subsection \<open>(1) Exploit parallelism for concurrent session management\<close>
wneuper@59472: subsection \<open>(2) Make Isac’s programming language usable\<close>
wneuper@59472: subsection \<open>(3) Adopt Isabelle’s numeral computation for Isac\<close>
wneuper@59472: text \<open>
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: \<close>
wneuper@59472: ML \<open>(*1*) Free ("123.456", HOLogic.realT)\<close>
neuper@55484: 
wneuper@59472: subsection \<open>(4) Improve the efficiency of Isac’s rewrite-engine\<close>
wneuper@59472: subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
neuper@55431: 
neuper@37906: end




